Grace/Cumulus/Real/HarmonicSeries.g17

Open in Workbench Download source

Imports

TriangularSum · RationalEmbedding

Declarations

Source

1-- The harmonic series diverges: doubling the number of terms adds at least a2-- half, so the partial sums pass every real number and have no limit. The3-- Archimedean property of the reals is proved on the way4-- Part of Cumulus, the Grace17 mathematics library.5-- Copyright (c) 2026 Grant Passmore.6-- Released under the Apache License 2.0. See LICENSE in the repository root.7-- Authors: Grant Passmore89module Grace.Cumulus.Real.HarmonicSeries10import TriangularSum11import RationalEmbedding1213-- Every real lies below some natural number.14theorem Real.below_natural (M : Real)15  shows ∃ n, Nat(n) ∧ M < realNat(n)16proof17  have realM : Real(M) by typecheck18  have cut := Real.characterization.forward with realM19  obtain ⟨u, uInQ, uPositive, uMissing⟩ := DedekindCut.exists_positive_upper with cut20  have uRational : Rational(u) by typecheck21  have vRational : Rational(u + rationalOne) by typecheck22  have uLessV : u < u + rationalOne23    have zeroLtOne := Grace.Cumulus.Rat.OrderedOperations.rationalZero.lt_one24    have step := rationalLess.add_left at rationalZero, rationalOne, u with zeroLtOne25    have zero := rationalAddValue.zero_right at u26    rwa zero at step27  have cutReal := rationalCut.real with vRational28  have subset := DedekindCut.subset_rationals with cut29  have below : RealLess(M, rationalCut(u + rationalOne))30    constructor31    . exact realM32    . constructor33      . exact cutReal34      . constructor35        . intros a ha36          have aLess := DedekindCut.lt_missing with cut, ha, uInQ, uMissing37          have aInQ := subset with a, ha38          have aLessV := rationalLess.transitive with aLess, uLessV39          apply rationalCut.membership.backward40          exact ⟨aInQ, aLessV⟩41        . intro equal42          have uInCut : u ∈ rationalCut(u + rationalOne)43            apply rationalCut.membership.backward44            exact ⟨uInQ, uLessV⟩45          rw equal at uMissing46          exact uMissing with uInCut47  have first := realLess.characterization.backward with below48  obtain ⟨n, nNat, vBelow⟩ := Rational.below_natural at u + rationalOne49  have class := rationalNat.class at n50  have vBelowNat : u + rationalOne < rationalNat(n) by rwa class51  have mono := rationalCut.strict_mono with vBelowNat52  have natural := rationalCut.natural at n53  rw natural at mono54  have second := realLess.characterization.backward with mono55  witness n56  exact realLess.transitive with first, second5758-- Reciprocation reverses order on the positive reals.59theorem realInvValue.antitone_le (A B : Real)60  requires positive : 0 < A61  requires le : A ≤ B62  shows realInvValue(B) ≤ realInvValue(A)63proof64  have cases := realLess.trichotomy at A, B65  cases cases with less | rest66  . have strict := realInvValue.antitone_positive with positive, less67    exact realLess.implies_le with strict68  . cases rest with equal | greater69    . rw equal70      linarith71    . exfalso72      linarith7374theorem realNat.monotone (m n : Nat)75  requires bound : m ≤ n76  shows realNat(m) ≤ realNat(n)77proof78  have less : m < succ(n) by arith79  have inSucc := membership.of_Less with less80  have split := bootstrap.succ.membership.forward with inSucc81  cases split with below | same82  . have strict := realNat.lt_of_lt with (Less.of_membership with below)83    exact realLess.implies_le with strict84  . rw same85    linarith8687-- A constant sequence sums to the count times the constant.88theorem realPartialSum.constant (C : Real) (m : Nat)89  shows ∑ i < m, constantSequence(C)(i) = (realNat(m):R) * C90proof91  induction m92  | zero =>93    rw [realPartialSum.zero, realNat.zero]94    ring95  | succ(k) using ih =>96    have count := realNat.real at k97    have value := constantSequence.value at C, k98    rw [realPartialSum.succ, value, realNat.succ]99    linear_combination ih100101-- The harmonic terms 1, 1/2, 1/3, …102defgraph harmonicTerms (n ∈ ℕ) : ℝ := realInvValue((realNat(n):R) + (1:R))103proof104  have typedN := nat.omega.backward with member105  have count := realNat.real with typedN106  exact realInvValue.real at (realNat(n):R) + (1:R)107108theorem harmonicTerms.sequence109  shows RealSequence(harmonicTerms)110proof111  exact harmonicTerms.function112113theorem harmonicTerms.positive (n : Nat)114  shows (0:R) < harmonicTerms(n)115proof116  have value := harmonicTerms.value at n117  rw value118  exact realInvValue.positive with (realNat.successor_positive at n)119120-- Each of the m terms after the first m is at least 1/(2m).121theorem harmonicTerms.tail_bound (m j : Nat)122  requires below : j < m123  shows realInvValue((2:R) * (realNat(m):R)) ≤ harmonicTerms(add(m, j))124proof125  have value := harmonicTerms.value at add(m, j)126  have split := realNat.add at m, j127  have succLe : succ(j) ≤ m by arith128  have mono := realNat.monotone with succLe129  have succValue := realNat.succ_add at j130  rw succValue at mono131  have jNonneg := realNat.nonnegative at j132  have argPositive : (0:R) < (realNat(add(m, j)):R) + (1:R)133    rw split134    linarith135  have two : (2:R) * (realNat(m):R) = (realNat(m):R) + (realNat(m):R) by ring136  have argLe : (realNat(add(m, j)):R) + (1:R) ≤ (2:R) * (realNat(m):R)137    rw [split, two]138    linarith139  rw value140  exact realInvValue.antitone_le with argPositive, argLe141142-- Doubling the number of terms adds at least one half to the sum.143theorem harmonicSeries.doubling (m : Nat)144  requires positive : 0 < m145  shows (2:R) * (∑ i < m, harmonicTerms(i):R) + (1:R) ≤ (2:R) * (realPartialSum(harmonicTerms, add(m, m)):R)146proof147  have sequence := harmonicTerms.sequence148  have split := realPartialSum.split_at with sequence149  have shifted := shiftedRealSequence.sequence with sequence150  have mReal := realNat.real at m151  have mPositive : (0:R) < realNat(m)152    have strict := realNat.lt_of_lt with positive153    rwa realNat.zero at strict154  have two : (2:R) * (realNat(m):R) = (realNat(m):R) + (realNat(m):R) by ring155  have twoM : (0:R) < (2:R) * (realNat(m):R)156    rw two157    linarith158  have invReal := realInvValue.real at (2:R) * (realNat(m):R)159  have constant := constantSequence.sequence at realInvValue((2:R) * (realNat(m):R))160  have bounded : ∀ k ∈ ℕ, k < m → (constantSequence(realInvValue((2:R) * (realNat(m):R)))(k):R) ≤ (shiftedRealSequence(harmonicTerms, m)(k):R)161    intros k hk hkm162    have kNat : Nat(k) by typecheck163    have cValue := constantSequence.value at realInvValue((2:R) * (realNat(m):R)), k164    have sValue := shiftedRealSequence.value at harmonicTerms, m, k with sequence165    rw [cValue, sValue]166    exact harmonicTerms.tail_bound with hkm167  have mono := realPartialSum.monotone_prefix with constant, shifted, bounded168  have constSum := realPartialSum.constant at realInvValue((2:R) * (realNat(m):R)), m169  rw constSum at mono170  have nonzero : (2:R) * (realNat(m):R) ≠ (0:R)171    intro zero172    rw zero at twoM173    linarith174  have cancel := realInvValue.mul_right with nonzero175  have expand : (2:R) * ((realNat(m):R) * realInvValue((2:R) * (realNat(m):R))) = (1:R)176    have rearrange : (2:R) * ((realNat(m):R) * realInvValue((2:R) * (realNat(m):R))) = ((2:R) * (realNat(m):R)) * realInvValue((2:R) * (realNat(m):R))177      ring178    rw [rearrange, cancel]179    rfl180  have doubleTerm : (2:R) * ((realNat(m):R) * realInvValue((2:R) * (realNat(m):R))) = (realNat(m):R) * realInvValue((2:R) * (realNat(m):R)) + (realNat(m):R) * realInvValue((2:R) * (realNat(m):R))181    ring182  rw doubleTerm at expand183  have doubleSum : (2:R) * (∑ i < m, harmonicTerms(i):R) = (∑ i < m, harmonicTerms(i):R) + (∑ i < m, harmonicTerms(i):R)184    ring185  have doubleTotal : (2:R) * ((∑ i < m, harmonicTerms(i):R) + (∑ i < m, shiftedRealSequence(harmonicTerms, m)(i):R)) = (∑ i < m, harmonicTerms(i):R) + (∑ i < m, harmonicTerms(i):R) + (∑ i < m, shiftedRealSequence(harmonicTerms, m)(i):R) + (∑ i < m, shiftedRealSequence(harmonicTerms, m)(i):R)186    ring187  rw [split, doubleSum, doubleTotal]188  linarith189190-- Some partial sum reaches 1 + k/2, for every k.191theorem harmonicSeries.lower_bound (k : Nat)192  shows ∃ m, Nat(m) ∧ 0 < m ∧ (2:R) + (realNat(k):R) ≤ (2:R) * (∑ l < m, harmonicTerms(l):R)193proof194  induction k195  | zero =>196    have sequence := harmonicTerms.sequence197    have step := realPartialSum.succ at harmonicTerms, 0198    have zeroSum := realPartialSum.zero at harmonicTerms199    have value := harmonicTerms.value at 0200    have oneNonzero : (1:R) ≠ (0:R)201      intro equal202      linarith203    have cancel := realInvValue.mul_right at (1:R) with oneNonzero204    have one := realMulValue.one_left at realInvValue((1:R))205    rw one at cancel206    have shift := realAddValue.zero_left at (1:R)207    rw [realNat.zero, shift, cancel] at value208    have sumReal := realPartialSum.real at harmonicTerms, 0 with sequence209    have termReal := RealSequence.value at harmonicTerms, 0 with sequence210    have total : realPartialSum(harmonicTerms, succ(0)) = (1:R)211      rw step212      linarith213    have positive : 0 < succ(0) by arith214    have twoReal : (2:R) ∈ ℝ by typecheck215    have twoOne := realMulValue.one_right at (2:R)216    have twoZero := realAddValue.zero_right at (2:R)217    witness succ(0)218    constructor219    . exact positive220    . rw [total, realNat.zero, twoOne, twoZero]221      exact realLe.reflexive at (2:R)222  | succ(j) using ih =>223    obtain ⟨m, mNat, mPositive, bound⟩ := ih224    have doubling := harmonicSeries.doubling at m with mPositive225    have jReal := realNat.real at j226    have sequence := harmonicTerms.sequence227    have sumReal := realPartialSum.real at harmonicTerms, m with sequence228    have doubleReal := realPartialSum.real at harmonicTerms, add(m, m) with sequence229    have positive : 0 < add(m, m) by arith230    witness add(m, m)231    constructor232    . exact positive233    . rw realNat.succ234      linarith235236-- The partial sums pass every real number.237theorem harmonicSeries.unbounded (M : Real)238  shows ∃ N, Nat(N) ∧ M < ∑ i < N, harmonicTerms(i)239proof240  obtain ⟨k, kNat, above⟩ := Real.below_natural at (2:R) * M241  obtain ⟨m, mNat, mPositive, bound⟩ := harmonicSeries.lower_bound at k242  have doubleM : (2:R) * M = M + M by ring243  have doubleSum : (2:R) * (∑ i < m, harmonicTerms(i):R) = (∑ i < m, harmonicTerms(i):R) + (∑ i < m, harmonicTerms(i):R)244    ring245  rw doubleM at above246  rw doubleSum at bound247  witness m248  linarith249250-- The harmonic series has no limit.251theorem harmonicSeries.diverges252  shows ¬∃ L ∈ ℝ, ConvergesTo(prefixSums(harmonicTerms), L)253proof254  intro converges255  obtain ⟨L, LReal, limit⟩ := converges256  have sequence := harmonicTerms.sequence257  obtain ⟨N, NIn, close⟩ := ConvergesTo.eventually with limit, realZero.lt_one258  have NNat : Nat(N) by typecheck259  have shiftReal : L + (1:R) ∈ ℝ by typecheck260  obtain ⟨m, mNat, above⟩ := harmonicSeries.unbounded at L + (1:R)261  have nNat : Nat(add(m, N)) by typecheck262  have nIn := nat.omega.forward with nNat263  have le : N ≤ add(m, N) by arith264  have inBall := close with nIn, le265  have parts := openBall.membership.forward with inBall266  have value := prefixSums.value at harmonicTerms, add(m, N) with *267  have split := realPartialSum.split_at at harmonicTerms, m, N with sequence268  have shifted := shiftedRealSequence.sequence at harmonicTerms, m with sequence269  have sumReal := realPartialSum.real at harmonicTerms, m with sequence270  have tailReal := realPartialSum.real at shiftedRealSequence(harmonicTerms, m), N with shifted271  have tailNonneg : (0:R) ≤ (∑ i < N, shiftedRealSequence(harmonicTerms, m)(i):R)272    have constant := constantSequence.sequence at (0:R)273    have bounded : ∀ k ∈ ℕ, k < N → (constantSequence((0:R))(k):R) ≤ (shiftedRealSequence(harmonicTerms, m)(k):R)274      intros k hk hkN275      have kNat : Nat(k) by typecheck276      have cValue := constantSequence.value at (0:R), k277      have sValue := shiftedRealSequence.value at harmonicTerms, m, k with sequence278      rw [cValue, sValue]279      exact realLess.implies_le with (harmonicTerms.positive at add(m, k))280    have mono := realPartialSum.monotone_prefix with constant, shifted, bounded281    have constSum := realPartialSum.constant at (0:R), N282    have zero := realMulValue.zero_right at realNat(N)283    rwa [constSum, zero] at mono284  have distance := parts.right285  rw [value, split] at distance286  have same : dist((∑ i < m, harmonicTerms(i):R) + (∑ i < N, shiftedRealSequence(harmonicTerms, m)(i):R), L) = abs((∑ i < m, harmonicTerms(i):R) + (∑ i < N, shiftedRealSequence(harmonicTerms, m)(i):R) - L)287    unfold dist288    rfl289  rw same at distance290  have upper := abs.upper at (∑ i < m, harmonicTerms(i):R) + (∑ i < N, shiftedRealSequence(harmonicTerms, m)(i):R) - L291  linarith292