Grace/Cumulus/Real/TriangularSum.g17

Open in Workbench Download source

Imports

FiniteSum · RootTwo

Declarations

Source

1-- The reciprocals of the triangular numbers sum to 2n/(n+1)2-- 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.TriangularSum8import FiniteSum9import RootTwo1011-- A quotient is determined by multiplying through its denominator.12theorem realDiv.of_mul_right (X Y D : Real)13  requires nonzero : D ≠ 014  requires product : X * D = Y15  shows X = Y / D16proof17  have inverse := realInvValue.mul_right with *18  have quotient := realDiv.eq_mul_inv at Y, D with *19  rw quotient20  linear_combination realInvValue(D) * product - X * inverse2122theorem realNat.succ_add (k : Nat)23  shows realNat(succ(k)) = (realNat(k):R) + 124proof25  rw realNat.succ26  unfold realAddValue27  unfold call228  rfl2930theorem realNat.successor_positive (k : Nat)31  shows 0 < (realNat(k):R) + 132proof33  have nonnegative := realNat.nonnegative with *34  have one := realZero.lt_one35  linarith3637theorem realNat.successor_nonzero (k : Nat)38  shows (realNat(k):R) + 1 ≠ 039proof40  have positive := realNat.successor_positive with *41  intro zero42  rw zero at positive43  exact realLess.not_self with *, positive4445-- The k-th term is 1/T_{k+1} = 2/((k+1)(k+2)).46defgraph triangularReciprocals (k ∈ ℕ) : ℝ :=47  (2:R) / ((realNat(k) + 1) * (realNat(k) + 2))48proof49  have typedK := nat.omega.backward with member50  exact realDiv.real at (2:R), (realNat(k) + 1) * (realNat(k) + 2) with *5152theorem triangularReciprocals.sequence53  shows RealSequence(triangularReciprocals)54proof55  exact triangularReciprocals.function5657-- The sequence whose adjacent differences are the reciprocals: -2/(k+1).58defgraph triangularTails (k ∈ ℕ) : ℝ := -((2:R) / (realNat(k) + 1))59proof60  have typedK := nat.omega.backward with member61  have quotient := realDiv.real at (2:R), (realNat(k):R) + 1 with *62  exact realNegValue.real with quotient6364theorem triangularTails.sequence65  shows RealSequence(triangularTails)66proof67  exact triangularTails.function6869-- 2/(k+1) - 2/(k+2) = 2/((k+1)(k+2)).70theorem triangularReciprocals.difference (k : Nat)71  shows triangularReciprocals[k] = adjacentDifferences(triangularTails)[k]72proof73  have sequence := triangularTails.sequence74  have term := triangularReciprocals.value at k with *75  have difference := adjacentDifferences.value with sequence76  have tailK := triangularTails.value at k with *77  have tailNext := triangularTails.value at succ(k) with *78  rw [term, difference, tailNext, tailK]79  have next := realNat.succ_add with *80  rw next81  have firstNonzero := realNat.successor_nonzero with *82  have secondPositive : 0 < (realNat(k):R) + 283    have nonnegative := realNat.nonnegative with *84    have one := realZero.lt_one85    linarith86  have secondNonzero : (realNat(k):R) + 2 ≠ 087    intro zero88    rw zero at secondPositive89    exact realLess.not_self with *, secondPositive90  have productPositive : 0 < (realNat(k) + 1) * (realNat(k) + 2)91    have firstPositive := realNat.successor_positive with *92    exact realMulValue.positive with *93  have productNonzero : (realNat(k) + 1) * (realNat(k) + 2) ≠ 094    intro zero95    rw zero at productPositive96    exact realLess.not_self with *, productPositive97  have shifted : (realNat(k):R) + 1 + 1 = (realNat(k):R) + 2 by ring98  rw shifted99  have firstQuotient := realDiv.mul_right at (2:R), (realNat(k):R) + 1 with *100  have secondQuotient := realDiv.mul_right at (2:R), (realNat(k):R) + 2 with *101  have product : (-((2:R) / (realNat(k) + 2)) - -((2:R) / (realNat(k) + 1))) * ((realNat(k) + 1) * (realNat(k) + 2)) = (2:R)102    linear_combination (realNat(k) + 2) * firstQuotient - (realNat(k) + 1) * secondQuotient103  have quotient := realDiv.of_mul_right with product104  symm at quotient105  exact quotient106107theorem triangularTails.zero108  shows triangularTails[0] = -(2:R)109proof110  have value := triangularTails.value at 0 with *111  rw [value, realNat.zero]112  have sum : (0:R) + 1 = (1:R) by ring113  rw sum114  have oneNonzero : (1:R) ≠ 0115    intro zero116    have one := realZero.lt_one117    rw zero at one118    exact realLess.not_self with *, one119  have quotient := realDiv.mul_right at (2:R), (1:R) with *120  have simplified : (2:R) / (1:R) = (2:R) by linear_combination quotient121  rw simplified122  rfl123124-- Σ_{k=1}^{n} 1/T_k = 2n/(n+1).125theorem realPartialSum.triangular_reciprocals (n : Nat)126  shows ∑ i < n, triangularReciprocals(i) = (2:R) * (realNat(n):R) / (realNat(n) + 1)127proof128  have sequence := triangularReciprocals.sequence129  have tails := triangularTails.sequence130  have differences := adjacentDifferences.sequence with tails131  have agree : ∀ k ∈ ℕ, k < n → triangularReciprocals[k] = adjacentDifferences(triangularTails)[k]132    intros k kMember less133    have kNat := nat.omega.backward with kMember134    exact triangularReciprocals.difference at k with *135  have same := realPartialSum.eq_prefix at triangularReciprocals, adjacentDifferences(triangularTails), n with *136  have telescoped := realPartialSum.telescoping at triangularTails, n with *137  have tailN := triangularTails.value at n with *138  have tailZero := triangularTails.zero139  rw [same, telescoped, tailN, tailZero]140  have nonzero := realNat.successor_nonzero at n with *141  have quotient := realDiv.mul_right at (2:R), (realNat(n):R) + 1 with *142  have product : (-((2:R) / (realNat(n) + 1)) - -(2:R)) * (realNat(n) + 1) = (2:R) * (realNat(n):R)143    have expand : (-((2:R) / ((realNat(n):R) + 1)) - -(2:R)) * ((realNat(n):R) + 1) = (2:R) * ((realNat(n):R) + 1) - ((2:R) / ((realNat(n):R) + 1)) * ((realNat(n):R) + 1)144      ring145    rw [expand, quotient]146    ring147  exact realDiv.of_mul_right at -((2:R) / (realNat(n) + 1)) - -(2:R), (2:R) * (realNat(n):R), (realNat(n):R) + 1 with *148