Grace/Cumulus/Real/Analysis/GeometricSeries.g17

Open in Workbench Download source

Imports

ArchimedeanLimits

Declarations

Source

1-- The geometric series: Σ X^k = 1/(1 - X) for |X| < 12-- 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.GeometricSeries8import ArchimedeanLimits910-- The partial sums (1 - X^n)/(1 - X), read as a quotient of sequences.11theorem geometricSeries.partial_sums (X : Real, n : Nat)12  requires nonzero : (1:R) - X ≠ 013  shows prefixSums(geometricTerms(X))[n] =14    divSequence(subSequence(constantSequence((1:R)), geometricTerms(X)),15      constantSequence((1:R) - X))[n]16proof17  have sequence := geometricTerms.sequence at X18  have ones := constantSequence.sequence at (1:R) with realOne.real19  have denominatorReal := realSubValue.real at (1:R), X with20    realOne.real, assumption21  have denominators := constantSequence.sequence at (1:R) - X with22    denominatorReal23  have differences := subSequence.sequence with ones, sequence24  have oneReal := RealSequence.value at constantSequence((1:R)), n with ones25  have termReal := RealSequence.value at geometricTerms(X), n with sequence26  have quotient := divSequence.value at27    subSequence(constantSequence((1:R)), geometricTerms(X)),28    constantSequence((1:R) - X), n with29      differences, denominators30  have difference := subSequence.value at31    constantSequence((1:R)), geometricTerms(X), n with32      ones, sequence, oneReal, termReal33  have one := constantSequence.value at (1:R), n with realOne.real, assumption34  have denominator := constantSequence.value at (1:R) - X, n with35    denominatorReal, assumption36  have term := geometricTerms.value at X, n with *37  have value := prefixSums.value at geometricTerms(X), n with sequence38  have formula := realPartialSum.geometric_quotient at X, n with nonzero39  rw [value, formula, quotient, difference, one, denominator, term]40  rfl4142-- Σ_{k=0}^{∞} X^k = 1/(1 - X) for |X| < 1.43theorem geometricSeries.sums_to (X : Real)44  requires small : abs(X) < 145  shows SumsTo(geometricTerms(X), (1:R) / ((1:R) - X))46proof47  have sequence := geometricTerms.sequence at X48  have prefixes := prefixSums.sequence with sequence49  have absReal := abs.real at X50  have upper := abs.upper at X51  have belowOne : X < 1 by linarith52  have denominatorPositive := realLess.iff_pos_sub.forward with belowOne53  have denominatorReal := realSubValue.real at (1:R), X with54    realOne.real, assumption55  have nonzero : (1:R) - X ≠ 056    intro zero57    rw zero at denominatorPositive58    linarith59  have ones := constantSequence.converges at (1:R) with realOne.real60  have powers := geometricTerms.converges_zero with small61  have numerators := ConvergesTo.sub with ones, powers62  have denominators := constantSequence.converges at (1:R) - X with63    denominatorReal64  have limit := ConvergesTo.div with numerators, denominators, nonzero65  have zero := realSubValue.zero_right with realOne.real66  rw zero at limit67  have equal : ∀ n ∈ ℕ, prefixSums(geometricTerms(X))[n] =68      divSequence(subSequence(constantSequence((1:R)), geometricTerms(X)),69        constantSequence((1:R) - X))[n]70    intros n naturalN71    have typedN : Nat(n) by exact nat.omega.backward at n with naturalN72    exact geometricSeries.partial_sums at X, n with nonzero73  have converges := ConvergesTo.of_equal_terms with prefixes, limit, equal74  exact SumsTo.of_converges with sequence, converges7576-- The classic instance: 1 + 1/2 + 1/4 + ⋯ = 2.77theorem geometricSeries.half_sums_to_two78  shows SumsTo(geometricTerms(half((1:R))), (2:R))79proof80  have halfReal := half.real with realOne.real81  have halfPositive := half.positive with realZero.lt_one82  have halfBelow := half.lt_self with realOne.real, realZero.lt_one83  have halfNonnegative := realLess.implies_le with halfPositive84  have absolute := abs.of_nonnegative with halfNonnegative85  have small : abs(half((1:R))) < 1 by rwa absolute86  have sums := geometricSeries.sums_to with small87  have doubled := half.add_self with realOne.real88  have gapReal := realSubValue.real at (1:R), half((1:R)) with89    realOne.real, halfReal90  have gapNonzero : (1:R) - half((1:R)) ≠ 091    intro zero92    linarith93  have product : (2:R) * ((1:R) - half((1:R))) = (1:R)94    have expand : (2:R) * ((1:R) - half((1:R))) =95        (2:R) - (half((1:R)) + half((1:R))) by ring96    rw [expand, doubled]97    ring98  have quotient := realDiv.of_mul_right with gapNonzero, product99  rw ← quotient at sums100  exact sums101