Grace/Cumulus/Real/Analysis/TriangularSeries.g17

Imports

Declarations

triangularSeries.partial_sums theorem derivation
triangularReciprocals.sums_to theorem derivation
Source

1-- The reciprocals of the triangular numbers sum to 22-- 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.TriangularSeries8import ArchimedeanLimits910-- The partial sums 2n/(n + 1) are twice the successor ratios.11theorem triangularSeries.partial_sums (n : Nat)12  shows prefixSums(triangularReciprocals)[n] =13    mulSequence(constantSequence((2:R)), successorRatios)[n]14proof15  have sequence := triangularReciprocals.sequence16  have ratios := successorRatios.sequence17  have constants := constantSequence.sequence at (2:R)18  have constantReal := RealSequence.value at constantSequence((2:R)), n with19    constants20  have ratioReal := RealSequence.value at successorRatios, n with ratios21  have product := mulSequence.value at22    constantSequence((2:R)), successorRatios, n with23      constants, ratios, constantReal, ratioReal24  have constant := constantSequence.value at (2:R), n with *25  have ratio := successorRatios.value at n26  have value := prefixSums.value at triangularReciprocals, n with sequence27  have formula := realPartialSum.triangular_reciprocals at n28  have countReal := realNat.real at n29  have numeratorReal : (2:R) * (realNat(n):R) ∈ ℝ by typecheck30  have denominatorReal : (realNat(n):R) + 1 ∈ ℝ by typecheck31  have inverseReal := realInvValue.real at (realNat(n):R) + 132  have regroup : (2:R) * (realNat(n):R) / ((realNat(n):R) + 1) =33      (2:R) * ((realNat(n):R) / ((realNat(n):R) + 1))34    have first := realDiv.eq_mul_inv at35      (2:R) * (realNat(n):R), (realNat(n):R) + 1 with *36    have second := realDiv.eq_mul_inv at37      (realNat(n):R), (realNat(n):R) + 1 with *38    rw [first, second]39    ring40  rw [value, formula, product, constant, ratio, regroup]41  rfl4243-- Σ_{k=1}^{∞} 1/T_k = 2, where T_k = k(k + 1)/2.44theorem triangularReciprocals.sums_to45  shows SumsTo(triangularReciprocals, (2:R))46proof47  have sequence := triangularReciprocals.sequence48  have prefixes := prefixSums.sequence with sequence49  have constants := constantSequence.converges at (2:R)50  have limit := ConvergesTo.mul with constants, successorRatios.converges_one51  have one := realMulValue.one_right at (2:R)52  rw one at limit53  have equal : ∀ n ∈ ℕ, prefixSums(triangularReciprocals)[n] =54      mulSequence(constantSequence((2:R)), successorRatios)[n]55    intros n naturalN56    have typedN : Nat(n) by exact nat.omega.backward at n with naturalN57    exact triangularSeries.partial_sums at n58  have converges := ConvergesTo.of_equal_terms with prefixes, limit, equal59  exact SumsTo.of_converges with sequence, converges60