Grace/Cumulus/Real/Analysis/Series.g17

Open in Workbench Download source

Imports

FiniteSum · ExtremeValue

Declarations

Source

1-- Infinite series as limits of partial 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.Analysis.Series8import FiniteSum9import ExtremeValue1011-- Section: Series12-- A series sums to S when its sequence of partial sums converges to S.13predicate SumsTo (u : Set) (S : Real) :=14  RealSequence(u) ∧ ConvergesTo(prefixSums(u), S)1516predicate Summable (u : Set) := ∃ S ∈ ℝ, SumsTo(u, S)1718theorem SumsTo.sequence (u : Set) (S : Real)19  requires sums : SumsTo(u, S)20  shows RealSequence(u)21proof22  simp [SumsTo]2324theorem SumsTo.converges (u : Set) (S : Real)25  requires sums : SumsTo(u, S)26  shows ConvergesTo(prefixSums(u), S)27proof28  simp [SumsTo]2930theorem SumsTo.of_converges (u : Set) (S : Real)31  requires sequence : RealSequence(u)32  requires converges : ConvergesTo(prefixSums(u), S)33  shows SumsTo(u, S)34proof35  constructor36  . exact sequence37  . exact converges3839theorem SumsTo.unique (u : Set) (S T : Real)40  requires sumsS : SumsTo(u, S)41  requires sumsT : SumsTo(u, T)42  shows S = T43proof44  have convergesS := SumsTo.converges with sumsS45  have convergesT := SumsTo.converges with sumsT46  exact ConvergesTo.unique with convergesS, convergesT4748theorem SumsTo.summable (u : Set) (S : Real)49  requires sums : SumsTo(u, S)50  shows Summable(u)51proof52  have realS : S ∈ ℝ by simp [Real]53  witness S54  constructor55  . exact realS56  . exact sums5758-- Section: PartialSumAlgebra59-- The partial sums of a termwise sum are the sums of the partial sums.60theorem prefixSums.add (u v : Set, n : Nat)61  requires sequenceU : RealSequence(u)62  requires sequenceV : RealSequence(v)63  shows prefixSums(addSequence(u, v))[n] =64    addSequence(prefixSums(u), prefixSums(v))[n]65proof66  have added := addSequence.sequence with sequenceU, sequenceV67  have prefixesU := prefixSums.sequence with sequenceU68  have prefixesV := prefixSums.sequence with sequenceV69  have sumU := RealSequence.value at prefixSums(u), n with prefixesU70  have sumV := RealSequence.value at prefixSums(v), n with prefixesV71  have valueAdded := prefixSums.value at addSequence(u, v), n with added72  have valueU := prefixSums.value at u, n with sequenceU73  have valueV := prefixSums.value at v, n with sequenceV74  have combined := addSequence.value at prefixSums(u), prefixSums(v), n with75    prefixesU, prefixesV, sumU, sumV76  have linear := realPartialSum.add at u, v, n with sequenceU, sequenceV77  rw [valueAdded, combined, valueU, valueV, linear]78  rfl7980theorem prefixSums.neg (u : Set, n : Nat)81  requires sequence : RealSequence(u)82  shows prefixSums(negSequence(u))[n] = negSequence(prefixSums(u))[n]83proof84  have negated := negSequence.sequence with sequence85  have prefixes := prefixSums.sequence with sequence86  have sumReal := RealSequence.value at prefixSums(u), n with prefixes87  have valueNegated := prefixSums.value at negSequence(u), n with negated88  have valueU := prefixSums.value at u, n with sequence89  have combined := negSequence.value at prefixSums(u), n with prefixes, sumReal90  have linear := realPartialSum.neg at u, n with sequence91  rw [valueNegated, combined, valueU, linear]92  rfl9394theorem prefixSums.scale (u : Set, n : Nat, C : Real)95  requires sequence : RealSequence(u)96  shows prefixSums(mulSequence(constantSequence(C), u))[n] =97    mulSequence(constantSequence(C), prefixSums(u))[n]98proof99  have constants := constantSequence.sequence at C100  have scaled := mulSequence.sequence with constants, sequence101  have prefixes := prefixSums.sequence with sequence102  have constantReal := RealSequence.value at constantSequence(C), n with103    constants104  have sumReal := RealSequence.value at prefixSums(u), n with prefixes105  have valueScaled := prefixSums.value at106    mulSequence(constantSequence(C), u), n with scaled107  have valueU := prefixSums.value at u, n with sequence108  have combined := mulSequence.value at109    constantSequence(C), prefixSums(u), n with110      constants, prefixes, constantReal, sumReal111  have constant := constantSequence.value at C, n with *112  have linear := realPartialSum.scale at u, n, C with sequence113  rw [valueScaled, combined, valueU, linear, constant]114  rfl115116-- Section: SeriesAlgebra117theorem SumsTo.add (u v : Set) (S T : Real)118  requires sumsU : SumsTo(u, S)119  requires sumsV : SumsTo(v, T)120  shows SumsTo(addSequence(u, v), S + T)121proof122  have sequenceU := SumsTo.sequence with sumsU123  have sequenceV := SumsTo.sequence with sumsV124  have convergesU := SumsTo.converges with sumsU125  have convergesV := SumsTo.converges with sumsV126  have added := addSequence.sequence with sequenceU, sequenceV127  have prefixes := prefixSums.sequence with added128  have limit := ConvergesTo.add with convergesU, convergesV129  have equal : ∀ n ∈ ℕ, prefixSums(addSequence(u, v))[n] =130      addSequence(prefixSums(u), prefixSums(v))[n]131    intros n naturalN132    have typedN : Nat(n) by exact nat.omega.backward at n with naturalN133    exact prefixSums.add with sequenceU, sequenceV134  have converges := ConvergesTo.of_equal_terms with prefixes, limit, equal135  exact SumsTo.of_converges with added, converges136137theorem SumsTo.neg (u : Set) (S : Real)138  requires sums : SumsTo(u, S)139  shows SumsTo(negSequence(u), -S)140proof141  have sequence := SumsTo.sequence with sums142  have converges := SumsTo.converges with sums143  have negated := negSequence.sequence with sequence144  have prefixes := prefixSums.sequence with negated145  have limit := ConvergesTo.neg with converges146  have equal : ∀ n ∈ ℕ, prefixSums(negSequence(u))[n] =147      negSequence(prefixSums(u))[n]148    intros n naturalN149    have typedN : Nat(n) by exact nat.omega.backward at n with naturalN150    exact prefixSums.neg with sequence151  have convergesNegated := ConvergesTo.of_equal_terms with152    prefixes, limit, equal153  exact SumsTo.of_converges with negated, convergesNegated154155theorem SumsTo.sub (u v : Set) (S T : Real)156  requires sumsU : SumsTo(u, S)157  requires sumsV : SumsTo(v, T)158  shows SumsTo(subSequence(u, v), S - T)159proof160  have negated := SumsTo.neg with sumsV161  have added := SumsTo.add with sumsU, negated162  unfold subSequence163  unfold realSubValue164  exact added165166theorem SumsTo.scale (u : Set) (S C : Real)167  requires sums : SumsTo(u, S)168  shows SumsTo(mulSequence(constantSequence(C), u), C * S)169proof170  have sequence := SumsTo.sequence with sums171  have converges := SumsTo.converges with sums172  have constants := constantSequence.sequence at C173  have scaled := mulSequence.sequence with constants, sequence174  have prefixes := prefixSums.sequence with scaled175  have constantConverges := constantSequence.converges at C176  have limit := ConvergesTo.mul with constantConverges, converges177  have equal : ∀ n ∈ ℕ,178      prefixSums(mulSequence(constantSequence(C), u))[n] =179        mulSequence(constantSequence(C), prefixSums(u))[n]180    intros n naturalN181    have typedN : Nat(n) by exact nat.omega.backward at n with naturalN182    exact prefixSums.scale with sequence183  have convergesScaled := ConvergesTo.of_equal_terms with184    prefixes, limit, equal185  exact SumsTo.of_converges with scaled, convergesScaled186187-- Section: FiniteSeries188-- Beyond the index N the partial sums of a vanishing sequence stay fixed.189theorem realPartialSum.eventually_zero (u : Set, N m : Nat)190  requires sequence : RealSequence(u)191  requires vanishing : ∀ n ∈ ℕ, N ≤ n → u[n] = (0:R)192  shows realPartialSum(u, add(N, m)) = ∑ i < N, u(i)193proof194  induction m195  | zero =>196    rw add.right_unit197    rfl198  | succ(k) using ih =>199    have index : Nat(add(N, k)) by typecheck200    have indexNatural := nat.omega.forward with index201    have after : N ≤ add(N, k) by exact LessEqual.add_right at N, k202    have term := vanishing with add(N, k), indexNatural, after203    have termReal := RealSequence.value at u, add(N, k) with sequence204    have prefixReal := realPartialSum.real at u, N with sequence205    rw [add.succ_right, realPartialSum.succ, ih]206    linarith207208theorem SumsTo.of_eventually_zero (u : Set, N : Nat)209  requires sequence : RealSequence(u)210  requires vanishing : ∀ n ∈ ℕ, N ≤ n → u[n] = (0:R)211  shows SumsTo(u, ∑ i < N, u(i))212proof213  have prefixes := prefixSums.sequence with sequence214  have sumReal := realPartialSum.real at u, N with sequence215  have naturalN := nat.omega.forward at N with assumption216  apply SumsTo.of_converges with sequence217  constructor218  . exact prefixes219  . intros E realE positive220    witness N221    constructor222    . exact naturalN223    . intros n naturalIndex after224      have typedN : Nat(n) by exact nat.omega.backward at n with naturalIndex225      obtain ⟨m, typedM, split⟩ := after226      have value := prefixSums.value at u, n with sequence227      have fixed := realPartialSum.eventually_zero at u, N, m with228        sequence, vanishing229      rw split at fixed230      rw [value, fixed]231      exact openBall.center with positive232233theorem SumsTo.zero234  shows SumsTo(constantSequence((0:R)), (0:R))235proof236  have sequence := constantSequence.sequence at (0:R)237  have vanishing : ∀ n ∈ ℕ, 0 ≤ n → constantSequence(0)[n] = (0:R)238    intros n naturalN after239    have typedN : Nat(n) by exact nat.omega.backward at n with naturalN240    exact constantSequence.value at (0:R), n with *241  have sums := SumsTo.of_eventually_zero at constantSequence(0), 0 with242    sequence, vanishing243  rwa realPartialSum.zero at sums244245-- Section: Comparison246theorem SumsTo.le_of_le_terms (u v : Set) (S T : Real)247  requires sumsU : SumsTo(u, S)248  requires sumsV : SumsTo(v, T)249  requires ordered : PointwiseLE(u, v)250  shows S ≤ T251proof252  have sequenceU := SumsTo.sequence with sumsU253  have sequenceV := SumsTo.sequence with sumsV254  have convergesU := SumsTo.converges with sumsU255  have convergesV := SumsTo.converges with sumsV256  have bounded : ∀ k ∈ ℕ, (u[k]:R) ≤ (v[k]:R)257    intros k naturalK258    have view := ordered with k, naturalK259    exact realLe.characterization.backward with view260  have prefixOrdered : PointwiseLE(prefixSums(u), prefixSums(v))261    intros n naturalN262    have typedN : Nat(n) by exact nat.omega.backward at n with naturalN263    have valueU := prefixSums.value at u, n with sequenceU264    have valueV := prefixSums.value at v, n with sequenceV265    have comparison := realPartialSum.monotone at u, v, n with266      sequenceU, sequenceV, bounded267    rw [valueU, valueV]268    exact realLe.characterization.forward with comparison269  exact ConvergesTo.le_of_le_terms with convergesU, convergesV, prefixOrdered270271theorem SumsTo.nonnegative (u : Set) (S : Real)272  requires sums : SumsTo(u, S)273  requires nonnegative : NonnegativeTerms(u)274  shows 0 ≤ S275proof276  have sequence := SumsTo.sequence with sums277  have ordered : PointwiseLE(constantSequence(0), u)278    intros n naturalN279    have typedN : Nat(n) by exact nat.omega.backward at n with naturalN280    have value := constantSequence.value at (0:R), n with *281    rw value282    exact nonnegative with n, naturalN283  exact SumsTo.le_of_le_terms with SumsTo.zero, sums, ordered284285-- Section: Summability286theorem Summable.add (u v : Set)287  requires summableU : Summable(u)288  requires summableV : Summable(v)289  shows Summable(addSequence(u, v))290proof291  obtain ⟨S, realS, sumsU⟩ := summableU292  obtain ⟨T, realT, sumsV⟩ := summableV293  have typedS : Real(S) by exact realS294  have typedT : Real(T) by exact realT295  have sums := SumsTo.add with sumsU, sumsV296  exact SumsTo.summable with sums297298theorem Summable.neg (u : Set)299  requires summable : Summable(u)300  shows Summable(negSequence(u))301proof302  obtain ⟨S, realS, sums⟩ := summable303  have typedS : Real(S) by exact realS304  have negated := SumsTo.neg with sums305  exact SumsTo.summable with negated306307theorem Summable.sub (u v : Set)308  requires summableU : Summable(u)309  requires summableV : Summable(v)310  shows Summable(subSequence(u, v))311proof312  obtain ⟨S, realS, sumsU⟩ := summableU313  obtain ⟨T, realT, sumsV⟩ := summableV314  have typedS : Real(S) by exact realS315  have typedT : Real(T) by exact realT316  have sums := SumsTo.sub with sumsU, sumsV317  exact SumsTo.summable with sums318319theorem Summable.scale (u : Set) (C : Real)320  requires summable : Summable(u)321  shows Summable(mulSequence(constantSequence(C), u))322proof323  obtain ⟨S, realS, sums⟩ := summable324  have typedS : Real(S) by exact realS325  have scaled := SumsTo.scale at u, S, C with sums326  exact SumsTo.summable with scaled327328-- Section: Tails329-- Dropping the first k terms of a convergent sequence keeps its limit.330theorem ConvergesTo.shifted (u : Set) (L : Real, k : Nat)331  requires converges : ConvergesTo(u, L)332  shows ConvergesTo(shiftedRealSequence(u, k), L)333proof334  have sequence := ConvergesTo.sequence with converges335  have shifted := shiftedRealSequence.sequence at u, k with sequence336  constructor337  . exact shifted338  . intros E realE positive339    obtain ⟨N, naturalN, close⟩ := ConvergesTo.eventually with340      converges, positive341    witness N342    constructor343    . exact naturalN344    . intros n naturalIndex after345      have typedN : Nat(n) by exact nat.omega.backward at n with naturalIndex346      have typedBound : Nat(N) by exact nat.omega.backward at N with naturalN347      have index : Nat(add(k, n)) by typecheck348      have indexNatural := nat.omega.forward with index349      have below : N ≤ add(k, n) by arith350      have value := shiftedRealSequence.value at u, k, n with sequence351      rw value352      exact close with add(k, n), indexNatural, below353354-- The terms of a convergent series tend to zero: each term is the355-- difference of two consecutive partial sums.356theorem SumsTo.terms_converge_zero (u : Set) (S : Real)357  requires sums : SumsTo(u, S)358  shows ConvergesTo(u, (0:R))359proof360  have sequence := SumsTo.sequence with sums361  have converges := SumsTo.converges with sums362  have prefixes := prefixSums.sequence with sequence363  have shifted := ConvergesTo.shifted at prefixSums(u), S, 1 with converges364  have limit := ConvergesTo.sub with shifted, converges365  have zero := realSubValue.self at S366  rw zero at limit367  have shiftedSequence := shiftedRealSequence.sequence at368    prefixSums(u), 1 with prefixes369  have equal : ∀ n ∈ ℕ, u[n] =370      subSequence(shiftedRealSequence(prefixSums(u), 1), prefixSums(u))[n]371    intros n naturalN372    have typedN : Nat(n) by exact nat.omega.backward at n with naturalN373    have shiftedReal := RealSequence.value at374      shiftedRealSequence(prefixSums(u), 1), n with shiftedSequence375    have prefixReal := RealSequence.value at prefixSums(u), n with prefixes376    have difference := subSequence.value at377      shiftedRealSequence(prefixSums(u), 1), prefixSums(u), n with378        shiftedSequence, prefixes, shiftedReal, prefixReal379    have shiftedValue := shiftedRealSequence.value at380      prefixSums(u), 1, n with prefixes381    have swap := add.commutative at n, 1382    have successor := add.right_one at n383    have next := prefixSums.value at u, succ(n) with sequence384    have current := prefixSums.value at u, n with sequence385    have term := RealSequence.value at u, n with sequence386    have sumReal := realPartialSum.real at u, n with sequence387    rw [difference, shiftedValue, swap, successor, next, current,388      realPartialSum.succ]389    ring390  exact ConvergesTo.of_equal_terms with sequence, limit, equal391