Grace/Cumulus/Real/FiniteSum.g17

Open in Workbench Download source

Imports

Analysis.Sequences · Power

Declarations

Source

1-- Finite real sums2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Real.FiniteSum8import Analysis.Sequences9import Power1011-- FiniteSums12def realPartialSum (u : Set) (n : Nat) → Set13  | u, zero => realZero14  | u, succ(k) => realAddValue(realPartialSum(u, k), uₖ)1516notation binder "∑" => realPartialSum for Real1718theorem realPartialSum.zero (u : Set)19  shows realPartialSum(u, 0) = (0:R)20proof21  rw realPartialSum22  rfl2324theorem realPartialSum.succ (u : Set, n : Nat)25  shows ∑ i < succ(n), u(i) = realAddValue(∑ i < n, u(i), uₙ)26proof27  rw realPartialSum28  rfl2930theorem realPartialSum.real (u : Set, n : Nat)31  requires sequence : RealSequence(u)32  shows Real(∑ i < n, u(i))33proof34  induction n35  | zero =>36    rw realPartialSum37    exact realZero.real38  | succ(k) using ih =>39    rw realPartialSum40    have termReal := RealSequence.value with sequence41    have sumReal := realAddValue.real with ih, termReal42    unfold call2 at sumReal43    unfold realAddValue44    exact sumReal4546-- Linearity makes finite sums usable independently of the integration proofs.47theorem realPartialSum.add (u v : Set, n : Nat)48  requires sequenceU : RealSequence(u)49  requires sequenceV : RealSequence(v)50  shows ∑ i < n, addSequence(u, v)(i) =51    (∑ i < n, u(i)) + ∑ i < n, v(i)52proof53  induction n54  | zero =>55    rw [realPartialSum.zero, realPartialSum.zero, realPartialSum.zero]56    ring57  | succ(k) using ih =>58    have valueU := RealSequence.value with sequenceU59    have valueV := RealSequence.value with sequenceV60    have sumUV := addSequence.sequence with sequenceU, sequenceV61    have value := addSequence.value with sequenceU, sequenceV, valueU, valueV62    rw [realPartialSum.succ, realPartialSum.succ, realPartialSum.succ, ih, value]63    ring6465-- Scalar multiplication commutes with a finite sum.66theorem realPartialSum.scale (u : Set, n : Nat, C : Real)67  requires sequence : RealSequence(u)68  shows ∑ k < n, mulSequence(constantSequence(C), u)(k) =69    C * (∑ i < n, u(i):R)70proof71  induction n72  | zero =>73    rw [realPartialSum.zero, realPartialSum.zero]74    ring75  | succ(k) using ih =>76    have constants := constantSequence.sequence at C77    have scaled := mulSequence.sequence with constants, sequence78    have constantValue := RealSequence.value with constants79    have valueU := RealSequence.value with sequence80    have value := mulSequence.value with constants, sequence, constantValue, valueU81    have constant := constantSequence.value at C, k with *82    rw [realPartialSum.succ, realPartialSum.succ, ih, value, constant]83    ring8485theorem realPartialSum.neg (u : Set, n : Nat)86  requires sequence : RealSequence(u)87  shows ∑ i < n, negSequence(u)(i) = -(∑ i < n, u(i):R)88proof89  induction n90  | zero =>91    rw [realPartialSum.zero, realPartialSum.zero]92    ring93  | succ(k) using ih =>94    have valueU := RealSequence.value with sequence95    have negated := negSequence.sequence with sequence96    have value := negSequence.value with sequence, valueU97    rw [realPartialSum.succ, realPartialSum.succ, ih, value]98    ring99100theorem realPartialSum.sub (u v : Set, n : Nat)101  requires sequenceU : RealSequence(u)102  requires sequenceV : RealSequence(v)103  shows ∑ i < n, subSequence(u, v)(i) =104    (∑ i < n, u(i):R) - (∑ i < n, v(i):R)105proof106  have negated := negSequence.sequence with sequenceV107  unfold subSequence108  rw [realPartialSum.add, realPartialSum.neg]109  unfold realSubValue110  rfl111112-- Pointwise bounds pass to half-open finite sums, including the empty sum.113theorem realPartialSum.monotone (u v : Set, n : Nat)114  requires sequenceU : RealSequence(u)115  requires sequenceV : RealSequence(v)116  requires bounded : ∀ k ∈ ℕ, (u[k]:R) ≤ (v[k]:R)117  shows (∑ i < n, u(i):R) ≤ (∑ i < n, v(i):R)118proof119  induction n120  | zero =>121    rw [realPartialSum.zero, realPartialSum.zero]122    exact realLe.reflexive with realZero.real123  | succ(k) using ih =>124    rw [realPartialSum.succ, realPartialSum.succ]125    have uk := RealSequence.value with sequenceU126    have vk := RealSequence.value with sequenceV127    have sumU := realPartialSum.real with sequenceU128    have sumV := realPartialSum.real with sequenceV129    have naturalK := nat.omega.forward at k with assumption130    have bound := bounded with k, naturalK131    unfold realAddValue132    have added := realLe.add with sumU, sumV, uk, vk, ih, bound133    unfold call2 at added134    exact added135136-- Induct before introducing the bound, so it can be specialized to each137-- smaller prefix of the current partition.138theorem realPartialSum.monotone_prefix_aux (n : Nat)139  shows ∀ u, ∀ v, RealSequence(u) → RealSequence(v) →140    (∀ k ∈ ℕ, k < n → (u[k]:R) ≤ (v[k]:R)) →141      (∑ i < n, u(i):R) ≤ (∑ i < n, v(i):R)142proof143  induction n144  | zero =>145    intros u v sequenceU sequenceV bounded146    rw [realPartialSum.zero, realPartialSum.zero]147    exact realLe.reflexive with realZero.real148  | succ(k) using ih =>149    intros u v sequenceU sequenceV bounded150    have naturalK := nat.omega.forward at k with assumption151    have before : k < succ(k)152      unfold Less153      exact LessEqual.reflexive at succ(k) with154        Naturals.constructor.succ at k with assumption155    have termBound := bounded with k, naturalK, before156    have prefix : ∀ j ∈ ℕ, j < k → (u[j]:R) ≤ (v[j]:R)157      intros j naturalJ smaller158      have typedJ := nat.omega.backward with naturalJ159      have below := Less.transitive_LessEqual at j, k, succ(k) with160        typedJ, assumption, Naturals.constructor.succ at k with assumption,161        smaller, LessEqual.successor at k with assumption162      exact bounded with j, naturalJ, below163    have sumBound := ih with u, v, sequenceU, sequenceV, prefix164    rw [realPartialSum.succ, realPartialSum.succ]165    have uk := RealSequence.value with sequenceU166    have vk := RealSequence.value with sequenceV167    have sumU := realPartialSum.real with sequenceU168    have sumV := realPartialSum.real with sequenceV169    unfold realAddValue170    have added := realLe.add with sumU, sumV, uk, vk, sumBound, termBound171    unfold call2 at added172    exact added173174-- Only the first n terms need bounds; later values of the sequences do not175-- affect a finite sum.176theorem realPartialSum.monotone_prefix (u v : Set, n : Nat)177  requires sequenceU : RealSequence(u)178  requires sequenceV : RealSequence(v)179  requires bounded : ∀ k ∈ ℕ, k < n → (u[k]:R) ≤ (v[k]:R)180  shows (∑ i < n, u(i):R) ≤ (∑ i < n, v(i):R)181proof182  exact realPartialSum.monotone_prefix_aux at n with183    u, v, sequenceU, sequenceV, bounded184185-- A finite sum only observes its first n terms, even if its sequences differ186-- at every later index.187theorem realPartialSum.eq_prefix_aux (n : Nat)188  shows ∀ u, ∀ v, RealSequence(u) → RealSequence(v) →189    (∀ k ∈ ℕ, k < n → u[k] = v[k]) →190      ∑ i < n, u(i) = ∑ i < n, v(i)191proof192  induction n193  | zero =>194    intros u v sequenceU sequenceV equal195    rw [realPartialSum.zero, realPartialSum.zero]196    rfl197  | succ(k) using ih =>198    intros u v sequenceU sequenceV equal199    have naturalK := nat.omega.forward at k with assumption200    have before : k < succ(k)201      unfold Less202      exact LessEqual.reflexive at succ(k) with203        Naturals.constructor.succ at k with assumption204    have termEqual := equal with k, naturalK, before205    have prefix : ∀ j ∈ ℕ, j < k → u[j] = v[j]206      intros j naturalJ smaller207      have typedJ := nat.omega.backward with naturalJ208      have below := Less.transitive_LessEqual at j, k, succ(k) with209        typedJ, assumption, Naturals.constructor.succ at k with assumption,210        smaller, LessEqual.successor at k with assumption211      exact equal with j, naturalJ, below212    have sumEqual := ih with u, v, sequenceU, sequenceV, prefix213    rw [realPartialSum.succ, realPartialSum.succ, sumEqual, termEqual]214    rfl215216theorem realPartialSum.eq_prefix (u v : Set, n : Nat)217  requires sequenceU : RealSequence(u)218  requires sequenceV : RealSequence(v)219  requires equal : ∀ k ∈ ℕ, k < n → u[k] = v[k]220  shows ∑ i < n, u(i) = ∑ i < n, v(i)221proof222  exact realPartialSum.eq_prefix_aux at n with223    u, v, sequenceU, sequenceV, equal224225-- ShiftedSums226defgraph shiftedRealSequence (u : Set, k : Nat) (n ∈ ℕ) : ℝ := u[add(k, n)]227requires sequence : RealSequence(u)228proof229  have typedN := nat.omega.backward with member230  exact RealSequence.value at u, add(k, n) with sequence231232theorem shiftedRealSequence.sequence (u : Set, k : Nat)233  requires sequence : RealSequence(u)234  shows RealSequence(shiftedRealSequence(u, k))235proof236  unfold RealSequence237  exact shiftedRealSequence.function with sequence238239-- Prefix and suffix sums agree on their shared boundary. This is the finite240-- sum operation needed for concatenating local refinements.241theorem realPartialSum.split_at (u : Set, n m : Nat)242  requires sequence : RealSequence(u)243  shows realPartialSum(u, add(n, m)) =244    (∑ i < n, u(i)) + ∑ i < m, shiftedRealSequence(u, n)(i)245proof246  induction m247  | zero =>248    rw [add.right_unit, realPartialSum.zero]249    have prefix := realPartialSum.real with sequence250    have zero := realAddValue.zero_right with prefix251    rw zero252    rfl253  | succ(k) using ih =>254    have shifted := shiftedRealSequence.sequence at u, n with sequence255    have step := realPartialSum.succ at u, add(n, k)256    have suffixStep := realPartialSum.succ at shiftedRealSequence(u, n), k257    have value := shiftedRealSequence.value at u, n, k with sequence258    rw [add.succ_right, step, ih, suffixStep, value]259    have term := RealSequence.value at u, add(n, k) with sequence260    ring261262-- The geometric sequence is a set-theoretic function on naturals.263defgraph geometricTerms (X : Real) (n ∈ ℕ) : ℝ := realPow(X, n)264proof265  have typedN := nat.omega.backward with member266  exact realPow.real with typedN267268theorem geometricTerms.sequence (X : Real)269  shows RealSequence(geometricTerms(X))270proof271  unfold RealSequence272  exact geometricTerms.function with assumption273274theorem geometricTerms.shifted (X : Real, m k : Nat)275  shows shiftedRealSequence(geometricTerms(X), m)[k] =276    (X ^ m) * (geometricTerms(X)[k]:R)277proof278  have sequence := geometricTerms.sequence at X279  have shifted := shiftedRealSequence.value at geometricTerms(X), m, k with sequence280  have index := add.closed at k, m with *281  have value := geometricTerms.value with assumption, index282  have valueK := geometricTerms.value at X, k with *283  have power := realPow.add at X, m, k with *284  rwa [shifted, value, valueK]285286-- Concatenation of prefixes, with the second block rescaled by X^m.287theorem realPartialSum.geometric_split (X : Real, m n : Nat)288  shows realPartialSum(geometricTerms(X), add(m, n)) =289    (∑ i < m, geometricTerms(X)(i):R) +290      (X ^ m) * (∑ i < n, geometricTerms(X)(i):R)291proof292  have sequence := geometricTerms.sequence at X293  have power := realPow.real at X, m with *294  have constants := constantSequence.sequence with power295  have scaled := mulSequence.sequence with constants, sequence296  have shifted := shiftedRealSequence.sequence at geometricTerms(X), m with sequence297  have equal : ∀ j ∈ ℕ, j < n →298      shiftedRealSequence(geometricTerms(X), m)[j] =299        mulSequence(constantSequence(X ^ m), geometricTerms(X))[j]300    intros j naturalJ before301    have typedJ := nat.omega.backward with naturalJ302    have constant := constantSequence.value with power, typedJ303    have term := RealSequence.value at geometricTerms(X), j with sequence304    have constantTerm := RealSequence.value at constantSequence(X ^ m), j with constants305    have product := mulSequence.value with constants, sequence, constantTerm, term306    have shiftedTerm := geometricTerms.shifted at X, m, j with307      *{2}, typedJ308    rwa [product, constant]309  have suffix := realPartialSum.eq_prefix with shifted, scaled, equal310  have split := realPartialSum.split_at at geometricTerms(X), m, n with sequence311  have scale := realPartialSum.scale at geometricTerms(X), n, X ^ m with sequence312  calc313    realPartialSum(geometricTerms(X), add(m, n)) =314        (∑ i < m, geometricTerms(X)(i):R) +315          ∑ k < n, shiftedRealSequence(geometricTerms(X), m)(k) := split316    _ = (∑ i < m, geometricTerms(X)(i):R) +317          ∑ k < n, mulSequence(constantSequence(X ^ m), geometricTerms(X))(k) := by cc318    _ = (∑ i < m, geometricTerms(X)(i):R) +319          (X ^ m) * (∑ i < n, geometricTerms(X)(i):R) := by cc320321-- Division-free geometric sum identity, valid also at X = 1.322theorem realPartialSum.geometric (X : Real, n : Nat)323  shows ((1:R) - X) * (∑ j < n, geometricTerms(X)(j):R) =324    (1:R) - X ^ n325proof326  induction n327  | zero =>328    rw [realPartialSum.zero, realPow.zero]329    ring330  | succ(k) using ih =>331    have sequence := geometricTerms.sequence at X332    have value := geometricTerms.value at X, k with *333    rw [realPartialSum.succ, value, realPow.succ]334    calc335      ((1:R) - X) * realAddValue(∑ j < k, geometricTerms(X)(j), X ^ k) =336          ((1:R) - X) * (∑ j < k, geometricTerms(X)(j):R) +337              ((1:R) - X) * X ^ k := by ring338      _ = ((1:R) - X ^ k) + ((1:R) - X) * X ^ k := by cc339      _ = (1:R) - X * X ^ k := by ring340341theorem realPartialSum.geometric_quotient (X : Real, n : Nat)342  requires nonzero : ((1:R) - X) ≠ (0:R)343  shows ∑ i < n, geometricTerms(X)(i) =344    ((1:R) - X ^ n) / ((1:R) - X)345proof346  have denominator := realSubValue.real with realOne.real347  have power := realPow.real at X, n with *348  have numerator := realSubValue.real with realOne.real, power349  have sequence := geometricTerms.sequence at X350  have inverseReal := realInvValue.real with denominator351  have inverse := realInvValue.mul_right with nonzero352  have identity := realPartialSum.geometric at X, n353  have division := realDiv.eq_mul_inv with numerator, denominator354  have commute := realMulValue.commutative with inverseReal, numerator355  calc356    ∑ i < n, geometricTerms(X)(i) =357        (1:R) * (∑ i < n, geometricTerms(X)(i):R) := by ring358    _ = (((1:R) - X) * realInvValue((1:R) - X)) *359          (∑ i < n, geometricTerms(X)(i):R) := by cc360    _ = realInvValue((1:R) - X) *361          (((1:R) - X) * (∑ i < n, geometricTerms(X)(i):R)) := by ring362    _ = realInvValue((1:R) - X) * ((1:R) - X ^ n) := by simp [identity]363    _ = ((1:R) - X ^ n) / ((1:R) - X) := by cc364365-- The generic forward difference sequence of a real sequence.366defgraph adjacentDifferences (u : Set) (n ∈ ℕ) : ℝ :=367  realSubValue(u[succ(n)], u[n])368requires sequence : RealSequence(u)369proof370  have typedN := nat.omega.backward with member371  have atN := RealSequence.value with sequence372  have atNext := RealSequence.value at u, succ(n) with sequence373  exact realSubValue.real with atNext, atN374375theorem adjacentDifferences.sequence (u : Set)376  requires sequence : RealSequence(u)377  shows RealSequence(adjacentDifferences(u))378proof379  unfold RealSequence380  exact adjacentDifferences.function with sequence381382theorem realPartialSum.telescoping (u : Set, n : Nat)383  requires sequence : RealSequence(u)384  shows ∑ i < n, adjacentDifferences(u)(i) = (u[n]:R) - (u[0]:R)385proof386  induction n387  | zero =>388    rw realPartialSum.zero389    have atZero := RealSequence.value at u, 0 with sequence390    ring391  | succ(k) using ih =>392    have atZero := RealSequence.value with sequence393    have atK := RealSequence.value with sequence394    have atNext := RealSequence.value with sequence395    have difference := adjacentDifferences.value with sequence396    rw [realPartialSum.succ, difference, ih]397    ring398399-- Discrete Leibniz rule. The first factor is sampled at the next index.400theorem adjacentDifferences.product (u v : Set, n : Nat)401  requires sequenceU : RealSequence(u)402  requires sequenceV : RealSequence(v)403  shows adjacentDifferences(mulSequence(u, v))[n] =404    (u[succ(n)]:R) * (adjacentDifferences(v)[n]:R) +405      (v[n]:R) * (adjacentDifferences(u)[n]:R)406proof407  have productSequence := mulSequence.sequence with sequenceU, sequenceV408  have un := RealSequence.value with sequenceU409  have vn := RealSequence.value with sequenceV410  have unext := RealSequence.value at u, succ(n) with sequenceU411  have vnext := RealSequence.value at v, succ(n) with sequenceV412  have productN := mulSequence.value with sequenceU, sequenceV, un, vn413  have productNext := mulSequence.value with sequenceU, sequenceV, unext, vnext414  have differenceProduct := adjacentDifferences.value with productSequence415  have differenceU := adjacentDifferences.value with sequenceU416  have differenceV := adjacentDifferences.value with sequenceV417  rw [differenceProduct, productNext, productN, differenceU, differenceV]418  ring419420-- The two terms in the discrete product rule are sequences in their own right.421defgraph forwardProductIncrements (u v : Set) (n ∈ ℕ) : ℝ :=422  realMulValue(u[succ(n)], realSubValue(v[succ(n)], v[n]))423requires sequenceU : RealSequence(u)424requires sequenceV : RealSequence(v)425proof426  have typedN := nat.omega.backward with member427  have unext := RealSequence.value at u, succ(n) with sequenceU428  have vn := RealSequence.value with sequenceV429  have vnext := RealSequence.value at v, succ(n) with sequenceV430  have difference := realSubValue.real with vnext, vn431  have product := realMulValue.real with unext, difference432  unfold realMulValue433  unfold call2 at product434  exact product435436defgraph backwardProductIncrements (u v : Set) (n ∈ ℕ) : ℝ :=437  realMulValue(v[n], realSubValue(u[succ(n)], u[n]))438requires sequenceU : RealSequence(u)439requires sequenceV : RealSequence(v)440proof441  have typedN := nat.omega.backward with member442  have un := RealSequence.value with sequenceU443  have unext := RealSequence.value at u, succ(n) with sequenceU444  have vn := RealSequence.value with sequenceV445  have difference := realSubValue.real with unext, un446  have product := realMulValue.real with vn, difference447  unfold realMulValue448  unfold call2 at product449  exact product450451theorem forwardProductIncrements.sequence (u v : Set)452  requires sequenceU : RealSequence(u)453  requires sequenceV : RealSequence(v)454  shows RealSequence(forwardProductIncrements(u, v))455proof456  unfold RealSequence457  exact forwardProductIncrements.function with sequenceU, sequenceV458459theorem backwardProductIncrements.sequence (u v : Set)460  requires sequenceU : RealSequence(u)461  requires sequenceV : RealSequence(v)462  shows RealSequence(backwardProductIncrements(u, v))463proof464  unfold RealSequence465  exact backwardProductIncrements.function with sequenceU, sequenceV466467theorem adjacentDifferences.product_terms (u v : Set, n : Nat)468  requires sequenceU : RealSequence(u)469  requires sequenceV : RealSequence(v)470  shows adjacentDifferences(mulSequence(u, v))[n] =471    addSequence(forwardProductIncrements(u, v), backwardProductIncrements(u, v))[n]472proof473  have forward := forwardProductIncrements.sequence with sequenceU, sequenceV474  have backward := backwardProductIncrements.sequence with sequenceU, sequenceV475  have forwardReal := RealSequence.value with forward476  have backwardReal := RealSequence.value with backward477  have added := addSequence.value with forward, backward, forwardReal, backwardReal478  have forwardValue := forwardProductIncrements.value with sequenceU, sequenceV479  have backwardValue := backwardProductIncrements.value with sequenceU, sequenceV480  have product := adjacentDifferences.product with sequenceU, sequenceV481  rw [added, forwardValue, backwardValue]482  have differenceU := adjacentDifferences.value with sequenceU483  have differenceV := adjacentDifferences.value with sequenceV484  rw [differenceU, differenceV] at product485  simp [realMulValue, call2]486487-- Finite summation by parts, expressed without choosing an interval or grid.488theorem realPartialSum.product_telescoping (u v : Set, n : Nat)489  requires sequenceU : RealSequence(u)490  requires sequenceV : RealSequence(v)491  shows (∑ i < n, forwardProductIncrements(u, v)(i):R) +492      (∑ i < n, backwardProductIncrements(u, v)(i):R) =493    (u[n]:R) * (v[n]:R) - (u[0]:R) * (v[0]:R)494proof495  have forward := forwardProductIncrements.sequence with sequenceU, sequenceV496  have backward := backwardProductIncrements.sequence with sequenceU, sequenceV497  have productSequence := mulSequence.sequence with sequenceU, sequenceV498  have differences := adjacentDifferences.sequence with productSequence499  have added := addSequence.sequence with forward, backward500  have equal : ∀ k ∈ ℕ, k < n →501      adjacentDifferences(mulSequence(u, v))[k] =502        addSequence(forwardProductIncrements(u, v), backwardProductIncrements(u, v))[k]503    intros k naturalK before504    have typedK := nat.omega.backward with naturalK505    exact adjacentDifferences.product_terms with sequenceU, sequenceV506  have sameSum := realPartialSum.eq_prefix with differences, added, equal507  have sumAdd := realPartialSum.add with forward, backward508  have telescope := realPartialSum.telescoping with productSequence509  have un := RealSequence.value with sequenceU510  have vn := RealSequence.value with sequenceV511  have u0 := RealSequence.value at u, 0 with sequenceU512  have v0 := RealSequence.value at v, 0 with sequenceV513  have productN := mulSequence.value with sequenceU, sequenceV, un, vn514  have productZero := mulSequence.value with sequenceU, sequenceV, u0, v0515  rw [productN, productZero] at telescope516  calc517    (∑ i < n, forwardProductIncrements(u, v)(i):R) +518        (∑ i < n, backwardProductIncrements(u, v)(i):R) =519      realPartialSum(addSequence(forwardProductIncrements(u, v),520        backwardProductIncrements(u, v)), n) := by cc521    _ = ∑ k < n, adjacentDifferences(mulSequence(u, v))(k) := by cc522    _ = (u[n]:R) * (v[n]:R) - (u[0]:R) * (v[0]:R) := telescope523524theorem realPartialSum.summation_by_parts (u v : Set, n : Nat)525  requires sequenceU : RealSequence(u)526  requires sequenceV : RealSequence(v)527  shows ∑ i < n, forwardProductIncrements(u, v)(i) =528    ((u[n]:R) * (v[n]:R) - (u[0]:R) * (v[0]:R)) -529      (∑ i < n, backwardProductIncrements(u, v)(i):R)530proof531  have forward := forwardProductIncrements.sequence with sequenceU, sequenceV532  have backward := backwardProductIncrements.sequence with sequenceU, sequenceV533  have un := RealSequence.value with sequenceU534  have vn := RealSequence.value with sequenceV535  have u0 := RealSequence.value with sequenceU536  have v0 := RealSequence.value with sequenceV537  have identity := realPartialSum.product_telescoping with sequenceU, sequenceV538  calc539    ∑ i < n, forwardProductIncrements(u, v)(i) =540      ((∑ i < n, forwardProductIncrements(u, v)(i):R) +541        (∑ i < n, backwardProductIncrements(u, v)(i):R)) -542          (∑ i < n, backwardProductIncrements(u, v)(i):R) := by ring543    _ = ((u[n]:R) * (v[n]:R) - (u[0]:R) * (v[0]:R)) -544      (∑ i < n, backwardProductIncrements(u, v)(i):R) := by cc545546-- Prefix sums themselves form a sequence; their adjacent difference is the547-- original sequence. This is the discrete fundamental theorem of calculus.548defgraph prefixSums (u : Set) (n ∈ ℕ) : ℝ := ∑ i < n, u(i)549requires sequence : RealSequence(u)550proof551  have typedN := nat.omega.backward with member552  exact realPartialSum.real with sequence553554theorem prefixSums.sequence (u : Set)555  requires sequence : RealSequence(u)556  shows RealSequence(prefixSums(u))557proof558  unfold RealSequence559  exact prefixSums.function with sequence560561theorem prefixSums.zero (u : Set)562  requires sequence : RealSequence(u)563  shows prefixSums(u)[0] = (0:R)564proof565  have value := prefixSums.value at u, 0 with sequence566  rwa realPartialSum.zero at value567568theorem prefixSums.difference (u : Set, n : Nat)569  requires sequence : RealSequence(u)570  shows adjacentDifferences(prefixSums(u))[n] = u[n]571proof572  have prefixes := prefixSums.sequence with sequence573  have delta := adjacentDifferences.value with prefixes574  have next := prefixSums.value at u, succ(n) with sequence575  have current := prefixSums.value with sequence576  have term := RealSequence.value with sequence577  rw [delta, next, current, realPartialSum.succ]578  ring579580-- Abel's finite summation formula: move the difference from prefix sums to v.581theorem realPartialSum.abel (u v : Set, n : Nat)582  requires sequenceU : RealSequence(u)583  requires sequenceV : RealSequence(v)584  shows ∑ i < n, mulSequence(u, v)(i) =585    (∑ i < n, u(i):R) * (v[n]:R) -586      (∑ k < n, forwardProductIncrements(prefixSums(u), v)(k):R)587proof588  have prefixes := prefixSums.sequence with sequenceU589  have products := mulSequence.sequence with sequenceU, sequenceV590  have backward := backwardProductIncrements.sequence with prefixes, sequenceV591  have forward := forwardProductIncrements.sequence with prefixes, sequenceV592  have equal : ∀ k ∈ ℕ, k < n →593      backwardProductIncrements(prefixSums(u), v)[k] = mulSequence(u, v)[k]594    intros k naturalK before595    have typedK := nat.omega.backward with naturalK596    have uk := RealSequence.value at u, k with sequenceU597    have vk := RealSequence.value at v, k with sequenceV598    have backwardValue := backwardProductIncrements.value at prefixSums(u), v, k with599      prefixes, sequenceV600    have productValue := mulSequence.value with sequenceU, sequenceV, uk, vk601    have delta := adjacentDifferences.value at prefixSums(u), k with prefixes602    have difference := prefixSums.difference at u, k with sequenceU603    rw delta at difference604    rw [backwardValue, difference, productValue]605    have commute := realMulValue.commutative with vk, uk606    unfold realMulValue607    unfold call2608    unfold call2 at commute609    exact commute610  have sameSum := realPartialSum.eq_prefix with backward, products, equal611  have telescope := realPartialSum.product_telescoping with prefixes, sequenceV612  have prefixN := prefixSums.value with sequenceU613  have prefixZero := prefixSums.zero with sequenceU614  rw [prefixN, prefixZero] at telescope615  have vn := RealSequence.value with sequenceV616  have v0 := RealSequence.value with sequenceV617  calc618    ∑ i < n, mulSequence(u, v)(i) =619      ∑ k < n, backwardProductIncrements(prefixSums(u), v)(k) := by cc620    _ = ((∑ k < n, forwardProductIncrements(prefixSums(u), v)(k):R) +621        (∑ k < n, backwardProductIncrements(prefixSums(u), v)(k):R)) -622          (∑ k < n, forwardProductIncrements(prefixSums(u), v)(k):R) := by ring623    _ = ((∑ i < n, u(i):R) * (v[n]:R) - (0:R) * (v[0]:R)) -624          (∑ k < n, forwardProductIncrements(prefixSums(u), v)(k):R) := by cc625    _ = (∑ i < n, u(i):R) * (v[n]:R) -626          (∑ k < n, forwardProductIncrements(prefixSums(u), v)(k):R) := by ring627