Grace/Cumulus/Real/Analysis/ArchimedeanLimits.g17

Open in Workbench Download source

Imports

Series · HarmonicSeries

Declarations

Source

1-- Archimedean limits: reciprocals, successor ratios, and powers below one2-- 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.ArchimedeanLimits8import Series9import HarmonicSeries1011-- Section: NullSequences12-- A sequence whose absolute values are eventually below every positive13-- radius converges to zero.14theorem ConvergesTo.zero_of_abs_bounds (u : Set)15  requires sequence : RealSequence(u)16  requires small : ∀ E ∈ ℝ, 0 < E →17    ∃ N ∈ ℕ, ∀ n ∈ ℕ, N ≤ n → abs(u[n]) < E18  shows ConvergesTo(u, (0:R))19proof20  constructor21  . exact sequence22  . intros E realE positive23    have typedE : Real(E) by exact realE24    obtain ⟨N, naturalN, close⟩ := small with E, realE, positive25    witness N26    constructor27    . exact naturalN28    . intros n naturalIndex after29      have typedN : Nat(n) by exact nat.omega.backward at n with naturalIndex30      have typedValue := RealSequence.value at u, n with sequence31      have bound := close with n, naturalIndex, after32      have zero := realSubValue.zero_right with typedValue33      apply openBall.membership.backward34      constructor35      . exact typedValue36      . unfold dist37        rwa zero3839theorem realInvValue.involutive (A : Real)40  requires nonzero : A ≠ 041  shows realInvValue(realInvValue(A)) = A42proof43  have inverseNonzero := realInvValue.nonzero with nonzero44  have law := realInvValue.mul_left with nonzero45  have equal := realInvValue.eq_of_mul_right with inverseNonzero, law46  symm at equal47  exact equal4849-- Section: Reciprocals50-- The reciprocals 1/(n + 1) tend to zero: this is the Archimedean property.51theorem harmonicTerms.converges_zero52  shows ConvergesTo(harmonicTerms, (0:R))53proof54  have sequence := harmonicTerms.sequence55  apply ConvergesTo.zero_of_abs_bounds with sequence56  intros E realE positive57  have typedE : Real(E) by exact realE58  have nonzeroE : E ≠ 059    intro zero60    rw zero at positive61    linarith62  have scaleReal := realInvValue.real at E63  have scalePositive := realInvValue.positive with positive64  have unscaled := realInvValue.involutive with nonzeroE65  obtain ⟨N, typedN, above⟩ := Real.below_natural at realInvValue(E)66  have naturalN := nat.omega.forward with typedN67  witness N68  constructor69  . exact naturalN70  . intros n naturalIndex after71    have typedIndex : Nat(n) by exact nat.omega.backward at n with naturalIndex72    have countReal := realNat.real at n73    have denominatorReal : (realNat(n):R) + 1 ∈ ℝ by typecheck74    have monotone := realNat.monotone with after75    have one := realZero.lt_one76    have denominatorAbove : realInvValue(E) < (realNat(n):R) + 1 by linarith77    have termReal := RealSequence.value at harmonicTerms, n with sequence78    have value := harmonicTerms.value at n79    have termPositive := harmonicTerms.positive at n80    have termNonnegative := realLess.implies_le with termPositive81    have absolute := abs.of_nonnegative with termNonnegative82    have inverted := realInvValue.antitone_positive at83      realInvValue(E), (realNat(n):R) + 1 with scalePositive, denominatorAbove84    rw unscaled at inverted85    rw [absolute, value]86    exact inverted8788-- The harmonic series is the standard example of a series that fails to sum.89theorem harmonicSeries.not_summable90  shows ¬Summable(harmonicTerms)91proof92  intro summable93  obtain ⟨L, realL, sums⟩ := summable94  have converges := SumsTo.converges with sums95  have limit : ∃ L ∈ ℝ, ConvergesTo(prefixSums(harmonicTerms), L)96    witness L97    constructor98    . exact realL99    . exact converges100  exact harmonicSeries.diverges with limit101102-- Section: SuccessorRatios103-- The ratios n/(n + 1).104defgraph successorRatios (n ∈ ℕ) : ℝ :=105  (realNat(n):R) / ((realNat(n):R) + 1)106proof107  have typedN := nat.omega.backward with member108  have countReal := realNat.real at n109  exact realDiv.real at (realNat(n):R), (realNat(n):R) + 1 with *110111theorem successorRatios.sequence112  shows RealSequence(successorRatios)113proof114  exact successorRatios.function115116-- n/(n + 1) = 1 - 1/(n + 1).117theorem successorRatios.sub_harmonic (n : Nat)118  shows successorRatios[n] = (1:R) - harmonicTerms(n)119proof120  have countReal := realNat.real at n121  have denominatorReal : (realNat(n):R) + 1 ∈ ℝ by typecheck122  have nonzero := realNat.successor_nonzero at n123  have inverseReal := realInvValue.real at (realNat(n):R) + 1124  have law := realInvValue.mul_left with nonzero125  have product : ((1:R) - realInvValue((realNat(n):R) + 1)) *126      ((realNat(n):R) + 1) = (realNat(n):R)127    have expand : ((1:R) - realInvValue((realNat(n):R) + 1)) *128        ((realNat(n):R) + 1) =129      ((realNat(n):R) + 1) -130        realInvValue((realNat(n):R) + 1) * ((realNat(n):R) + 1) by ring131    rw [expand, law]132    ring133  have quotient := realDiv.of_mul_right with nonzero, product134  have value := successorRatios.value at n135  have termValue := harmonicTerms.value at n136  rw [value, termValue]137  symm at quotient138  exact quotient139140theorem successorRatios.converges_one141  shows ConvergesTo(successorRatios, (1:R))142proof143  have sequence := successorRatios.sequence144  have harmonics := harmonicTerms.sequence145  have constants := constantSequence.sequence at (1:R) with realOne.real146  have constantConverges := constantSequence.converges at (1:R) with147    realOne.real148  have limit := ConvergesTo.sub with149    constantConverges, harmonicTerms.converges_zero150  have zero := realSubValue.zero_right with realOne.real151  rw zero at limit152  have equal : ∀ n ∈ ℕ, successorRatios[n] =153      subSequence(constantSequence((1:R)), harmonicTerms)[n]154    intros n naturalN155    have typedN : Nat(n) by exact nat.omega.backward at n with naturalN156    have constantReal := RealSequence.value at157      constantSequence((1:R)), n with constants158    have termReal := RealSequence.value at harmonicTerms, n with harmonics159    have difference := subSequence.value at160      constantSequence((1:R)), harmonicTerms, n with161        constants, harmonics, constantReal, termReal162    have constant := constantSequence.value at (1:R), n with *163    have ratio := successorRatios.sub_harmonic at n164    rw [difference, constant, ratio]165    rfl166  exact ConvergesTo.of_equal_terms with sequence, limit, equal167168-- Section: Powers169theorem realPow.nonnegative (A : Real, n : Nat)170  requires nonnegative : 0 ≤ A171  shows 0 ≤ A ^ n172proof173  induction n174  | zero =>175    rw realPow.zero176    exact realLess.implies_le with realZero.lt_one177  | succ(k) using ih =>178    have power := realPow.real at A, k179    rw realPow.succ180    exact realMulValue.nonnegative with nonnegative, ih181182theorem realPow.le_one (A : Real, n : Nat)183  requires nonnegative : 0 ≤ A184  requires bounded : A ≤ 1185  shows A ^ n ≤ 1186proof187  induction n188  | zero =>189    rw realPow.zero190    exact realLe.reflexive with realOne.real191  | succ(k) using ih =>192    have power := realPow.real at A, k193    have scaled := realLe.mul_left_of_nonnegative with ih, nonnegative194    have one := realMulValue.one_right at A195    rw one at scaled196    rw realPow.succ197    exact realLe.transitive with scaled, bounded198199theorem realPow.abs (A : Real, n : Nat)200  shows abs(A ^ n) = abs(A) ^ n201proof202  induction n203  | zero =>204    rw [realPow.zero, realPow.zero]205    have oneNonnegative := realLess.implies_le with realZero.lt_one206    exact abs.of_nonnegative with oneNonnegative207  | succ(k) using ih =>208    have power := realPow.real at A, k209    have product := abs.mul at A, A ^ k with assumption, power210    rw [realPow.succ, realPow.succ, product, ih]211    rfl212213-- Bernoulli's inequality.214theorem realPow.bernoulli (H : Real, n : Nat)215  requires nonnegative : 0 ≤ H216  shows (1:R) + (realNat(n):R) * H ≤ ((1:R) + H) ^ n217proof218  induction n219  | zero =>220    rw [realPow.zero, realNat.zero]221    have zeroProduct : (1:R) + (0:R) * H = (1:R) by ring222    rw zeroProduct223    exact realLe.reflexive with realOne.real224  | succ(k) using ih =>225    have countReal := realNat.real at k226    have baseReal : (1:R) + H ∈ ℝ by typecheck227    have one := realZero.lt_one228    have baseNonnegative : 0 ≤ (1:R) + H by linarith229    have power := realPow.real at (1:R) + H, k230    have scaled := realLe.mul_left_of_nonnegative with ih, baseNonnegative231    have countNonnegative := realNat.nonnegative at k232    have square := realMulValue.square_nonnegative at H233    have cross := realMulValue.nonnegative with countNonnegative, square234    have expand : ((1:R) + H) * ((1:R) + (realNat(k):R) * H) =235        (1:R) + ((realNat(k):R) + 1) * H + (realNat(k):R) * (H * H) by ring236    rw [realPow.succ, realNat.succ_add]237    rw expand at scaled238    linarith239240-- For 0 ≤ A < 1 the powers decay at least like 1/(1 + n(1 - A)).241theorem realPow.decay_bound (A : Real, n : Nat)242  requires nonnegative : 0 ≤ A243  requires below : A < 1244  shows A ^ n * ((1:R) + (realNat(n):R) * ((1:R) - A)) ≤ 1245proof246  have gapReal := realSubValue.real at (1:R), A with realOne.real, assumption247  have gapPositive := realLess.iff_pos_sub.forward with below248  have gapNonnegative := realLess.implies_le with gapPositive249  have countReal := realNat.real at n250  have power := realPow.real at A, n251  have powerNonnegative := realPow.nonnegative at A, n with nonnegative252  have bernoulli := realPow.bernoulli at (1:R) - A, n with gapNonnegative253  have baseReal : (1:R) + ((1:R) - A) ∈ ℝ by typecheck254  have basePower := realPow.real at (1:R) + ((1:R) - A), n255  have factorReal : (1:R) + (realNat(n):R) * ((1:R) - A) ∈ ℝ by typecheck256  have scaled := realLe.mul_left_of_nonnegative with bernoulli, powerNonnegative257  have combined := realPow.mul at A, (1:R) + ((1:R) - A), n258  have productReal : A * ((1:R) + ((1:R) - A)) ∈ ℝ by typecheck259  have one := realZero.lt_one260  have baseNonnegative : 0 ≤ (1:R) + ((1:R) - A) by linarith261  have productNonnegative := realMulValue.nonnegative with262    nonnegative, baseNonnegative263  have productBounded : A * ((1:R) + ((1:R) - A)) ≤ 1264    have square := realMulValue.square_nonnegative at (1:R) - A265    have expand : A * ((1:R) + ((1:R) - A)) =266        (1:R) - ((1:R) - A) * ((1:R) - A) by ring267    rw expand268    linarith269  have small := realPow.le_one at A * ((1:R) + ((1:R) - A)), n with270    productNonnegative, productBounded271  rw combined at small272  exact realLe.transitive with scaled, small273274-- Powers of a number in [0, 1) eventually fall below every positive bound.275theorem realPow.eventually_small (A E : Real)276  requires nonnegative : 0 ≤ A277  requires below : A < 1278  requires positive : 0 < E279  shows ∃ N ∈ ℕ, ∀ n ∈ ℕ, N ≤ n → A ^ n < E280proof281  have gapReal := realSubValue.real at (1:R), A with realOne.real, assumption282  have gapPositive := realLess.iff_pos_sub.forward with below283  have gapNonnegative := realLess.implies_le with gapPositive284  have scaleReal := realMulValue.real at E, (1:R) - A with assumption, gapReal285  have scalePositive := realMulValue.positive with positive, gapPositive286  have scaleNonzero : E * ((1:R) - A) ≠ 0287    intro zero288    rw zero at scalePositive289    linarith290  have thresholdReal := realInvValue.real at E * ((1:R) - A)291  have law := realInvValue.mul_left with scaleNonzero292  obtain ⟨N, typedN, above⟩ :=293    Real.below_natural at realInvValue(E * ((1:R) - A))294  have naturalN := nat.omega.forward with typedN295  witness N296  constructor297  . exact naturalN298  . intros n naturalIndex after299    have typedIndex : Nat(n) by exact nat.omega.backward at n with naturalIndex300    have countReal := realNat.real at n301    have monotone := realNat.monotone with after302    have aboveIndex : realInvValue(E * ((1:R) - A)) < realNat(n) by linarith303    have multiplied := realLess.mul_right_of_positive with304      aboveIndex, scalePositive305    rw law at multiplied306    have power := realPow.real at A, n307    have bound := realPow.decay_bound at A, n with nonnegative, below308    have factorReal : (1:R) + (realNat(n):R) * ((1:R) - A) ∈ ℝ by typecheck309    have countNonnegative := realNat.nonnegative at n310    have cross := realMulValue.nonnegative with countNonnegative, gapNonnegative311    have one := realZero.lt_one312    have factorNonnegative : 0 ≤ (1:R) + (realNat(n):R) * ((1:R) - A) by313      linarith314    by_contra notLess315    have reversed := realLe.of_not_less with notLess316    have scaledReverse := realLe.mul_right_of_nonnegative with317      reversed, factorNonnegative318    have expand : E * ((1:R) + (realNat(n):R) * ((1:R) - A)) =319        E + (realNat(n):R) * (E * ((1:R) - A)) by ring320    rw expand at scaledReverse321    linarith322323-- The geometric sequence X^n tends to zero when |X| < 1.324theorem geometricTerms.converges_zero (X : Real)325  requires small : abs(X) < 1326  shows ConvergesTo(geometricTerms(X), (0:R))327proof328  have sequence := geometricTerms.sequence at X329  have absReal := abs.real at X330  have absNonnegative := abs.nonnegative at X331  apply ConvergesTo.zero_of_abs_bounds with sequence332  intros E realE positive333  have typedE : Real(E) by exact realE334  obtain ⟨N, naturalN, eventually⟩ := realPow.eventually_small at335    abs(X), E with absNonnegative, small, positive336  witness N337  constructor338  . exact naturalN339  . intros n naturalIndex after340    have typedN : Nat(n) by exact nat.omega.backward at n with naturalIndex341    have value := geometricTerms.value at X, n with *342    have absolute := realPow.abs at X, n343    have bound := eventually with n, naturalIndex, after344    rw [value, absolute]345    exact bound346