Grace/Cumulus/Real/Analysis/Sequences.g17

Open in Workbench Download source

Imports

Metric

Declarations

Source

1-- Real analysis: Sequences2-- 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.Sequences8import Metric910-- Section: Sequences11predicate RealSequence (u : Set) := FunctionBetween(u, ℕ, ℝ)1213-- The epsilon definition: eventually every term lies in the open14-- ball of radius E around L.15predicate ConvergesTo (u : Set) (L : Real) :=16  RealSequence(u) ∧17  (∀ E ∈ ℝ, 0 < E →18    ∃ N ∈ ℕ, ∀ n ∈ ℕ, N ≤ n →19      uₙ ∈ openBall(L, E))2021predicate EventuallyEqual (u v : Set) :=22  ∃ N ∈ ℕ, ∀ n ∈ ℕ, N ≤ n → uₙ = vₙ2324def negSequence (u : Set) : Set :=25  compose(realNeg, u, ℕ, ℝ, ℝ)2627def addSequence (u v : Set) : Set :=28  compose(realAdd, pairFunctions(u, v, ℕ, ℝ, ℝ), ℕ, ℝ × ℝ, ℝ)2930def subSequence (u v : Set) : Set :=31  addSequence(u, negSequence(v))3233def mulSequence (u v : Set) : Set :=34  compose(realMul, pairFunctions(u, v, ℕ, ℝ, ℝ), ℕ, ℝ × ℝ, ℝ)3536def invSequence (u : Set) : Set :=37  compose(realInv, u, ℕ, ℝ, ℝ)3839def divSequence (u v : Set) : Set :=40  compose(realDiv, pairFunctions(u, v, ℕ, ℝ, ℝ), ℕ, ℝ × ℝ, ℝ)4142-- A positive scale strictly larger than |A|.43def limitScale (A : Real) : Real := abs(A) + 14445-- The radius E/(2C), named so epsilon proofs need not expose the concrete46-- implementation of division by a positive real.47def scaledRadius (E C : Real) : Real := half(E) / C4849-- A uniform bound for the reciprocal factors near a nonzero limit L.50def inverseScale (L : Real) : Real :=51  realInvValue(half(abs(L))) * abs(realInvValue(L))5253theorem limitScale.real (A : Real)54  shows Real(limitScale(A))55proof56  unfold limitScale57  exact realAddValue.real at abs(A), realOne with58    abs.real at A with assumption, realOne.real5960theorem limitScale.positive (A : Real)61  shows 0 < limitScale(A)62proof63  have absReal := abs.real at A64  have oneStep := realLess.add_left with realZero.real, realOne.real, absReal, realZero.lt_one65  have scaleReal := realAddValue.real with absReal, realOne.real66  have zero := realAddValue.zero_right with absReal67  rw zero at oneStep68  unfold limitScale69  exact realLe.transitive_less at realZero, abs(A), abs(A) + 1 with70    realZero.real, absReal, scaleReal,71    abs.nonnegative at A with assumption, oneStep7273theorem abs.lt_limitScale (A : Real)74  shows abs(A) < limitScale(A)75proof76  have absReal := abs.real at A77  have step := realLess.add_left with realZero.real, realOne.real, absReal, realZero.lt_one78  have zero := realAddValue.zero_right with absReal79  rw zero at step80  unfold limitScale81  exact step8283theorem scaledRadius.real (E C : Real)84  shows Real(scaledRadius(E, C))85proof86  unfold scaledRadius87  typecheck8889theorem scaledRadius.positive (E C : Real)90  requires positiveE : 0 < E91  requires positiveC : 0 < C92  shows 0 < scaledRadius(E, C)93proof94  have inversePositive := IsOrderedField.positive_inverse with reals.ordered_field, positiveC95  have halfPositive := half.positive with positiveE96  have inverseReal := realInvValue.real at C97  unfold scaledRadius98  rw realDiv.eq_mul_inv99  unfold realInvValue100  unfold realInvValue at inverseReal101  exact realMulValue.positive at half(E), realInv(C) with102    half.real at E with assumption,103    inverseReal,104    halfPositive, inversePositive105106theorem scaledRadius.cancel (E C : Real)107  requires positiveC : 0 < C108  shows C * scaledRadius(E, C) = half(E)109proof110  have halfReal := half.real at E111  have inverseReal := realInvValue.real at C112  have nonzero : C ≠ 0113    intro equal114    rw equal at positiveC115    exact IsOrderedField.irreflexive with reals.ordered_field, positiveC116  have inverse := realInvValue.mul_right with nonzero117  have inverseLaw : C * realInvValue(C) = 1 by exact inverse118  have commute := realMulValue.commutative at C, half(E) with119    assumption, halfReal120  have firstAssoc := realMulValue.associative at121    C, half(E), realInvValue(C) with assumption, halfReal, inverseReal122  have secondAssoc := realMulValue.associative at123    half(E), C, realInvValue(C) with halfReal, assumption, inverseReal124  have one := realMulValue.one_right with halfReal125  unfold scaledRadius126  rw realDiv.eq_mul_inv127  calc128    C * (half(E) * realInvValue(C)) =129        (C * half(E)) * realInvValue(C) := by cc130    _ = (half(E) * C) * realInvValue(C) := by cc131    _ = half(E) * (C * realInvValue(C)) := secondAssoc132    _ = half(E) * 1 := by cc133    _ = half(E) := one134135theorem inverseScale.real (L : Real)136  shows Real(inverseScale(L))137proof138  unfold inverseScale139  exact realMulValue.real at140    realInvValue(half(abs(L))), abs(realInvValue(L)) with141      realInvValue.real at half(abs(L)) with142        half.real at abs(L) with abs.real at L with assumption,143      abs.real at realInvValue(L) with realInvValue.real at L with assumption144145theorem inverseScale.positive (L : Real)146  requires nonzero : L ≠ 0147  shows 0 < inverseScale(L)148proof149  have absLReal := abs.real at L150  have absLPositive := abs.positive_of_ne with nonzero151  have halfReal := half.real with absLReal152  have halfPositive := half.positive with absLPositive153  have inverseHalfPositive := realInvValue.positive with halfPositive154  have inverseLReal := realInvValue.real at L155  have inverseLNonzero := realInvValue.nonzero with nonzero156  have absInversePositive := abs.positive_of_ne with inverseLNonzero157  unfold inverseScale158  exact realMulValue.positive at159    realInvValue(half(abs(L))), abs(realInvValue(L)) with160      realInvValue.real at half(abs(L)) with halfReal,161      abs.real at realInvValue(L) with inverseLReal,162      inverseHalfPositive, absInversePositive163164theorem ConvergesTo.sequence (u : Set) (L : Real)165  requires converges : ConvergesTo(u, L)166  shows RealSequence(u)167proof168  simp [ConvergesTo]169170theorem ConvergesTo.eventually (u : Set) (L E : Real)171  requires converges : ConvergesTo(u, L)172  requires positive : 0 < E173  shows ∃ N ∈ ℕ, ∀ n ∈ ℕ, N ≤ n →174    uₙ ∈ openBall(L, E)175proof176  rcases converges with ⟨sequence, eventually⟩177  exact eventually with E, positive178179-- Two eventual properties hold together on a common tail. This packages the180-- elementary maximum-index argument for one or two sequences.181theorem ConvergesTo.common_eventually (u v : Set) (L M E D : Real)182  requires convergesL : ConvergesTo(u, L)183  requires convergesM : ConvergesTo(v, M)184  requires positiveE : 0 < E185  requires positiveD : 0 < D186  shows ∃ N ∈ ℕ, ∀ n ∈ ℕ, N ≤ n →187    (uₙ ∈ openBall(L, E) ∧ vₙ ∈ openBall(M, D))188proof189  obtain ⟨N, nNatural, closeL⟩ := ConvergesTo.eventually with convergesL, positiveE190  obtain ⟨M0, mNatural, closeM⟩ := ConvergesTo.eventually with convergesM, positiveD191  have typedN : Nat(N) by exact nat.omega.backward at N with nNatural192  have typedM : Nat(M0) by exact nat.omega.backward at M0 with mNatural193  have comparison := Less.trichotomy with typedN, typedM194  cases comparison with nLessM | rest195  . have nLeM := Less.implies_LessEqual at N, M0 with196      typedN, typedM, nLessM197    witness M0198    constructor199    . exact mNatural200    . intros n nInNaturals mLeN201      have nLeLittleN := LessEqual.transitive with nLeM, mLeN202      constructor203      . exact closeL with n, nInNaturals, nLeLittleN204      . exact closeM with n, nInNaturals, mLeN205  . cases rest with equal | mLessN206    . witness N207      constructor208      . exact nNatural209      . intros n nInNaturals nLeLittleN210        have mLeLittleN : M0 ≤ n by rwa ← equal211        constructor212        . exact closeL with n, nInNaturals, nLeLittleN213        . exact closeM with n, nInNaturals, mLeLittleN214    . have mLeN := Less.implies_LessEqual at M0, N with215        typedM, typedN, mLessN216      witness N217      constructor218      . exact nNatural219      . intros n nInNaturals nLeLittleN220        have mLeLittleN := LessEqual.transitive with mLeN, nLeLittleN221        constructor222        . exact closeL with n, nInNaturals, nLeLittleN223        . exact closeM with n, nInNaturals, mLeLittleN224225theorem RealSequence.value (u : Set, n : Nat)226  requires sequence : RealSequence(u)227  shows Real(uₙ)228proof229  unfold RealSequence at sequence230  have nInNaturals : n ∈ ℕ by simp [Nat]231  obtain ⟨A, realA, mapped⟩ := FunctionBetween.exists_value with sequence, nInNaturals232  have applied := FunctionBetween.apply_value with sequence, mapped233  rw applied234  exact realA235236instance RealSequence.value_type (u : Set, n : Nat)237  requires sequence : RealSequence(u)238  shows Real(uₙ)239proof240  exact RealSequence.value with sequence241242theorem negSequence.sequence (u : Set)243  requires sequence : RealSequence(u)244  shows RealSequence(negSequence(u))245proof246  unfold RealSequence at sequence247  unfold RealSequence248  unfold negSequence249  exact compose.function with sequence, realNeg.function250251theorem negSequence.value (u : Set, n : Nat)252  requires sequence : RealSequence(u)253  requires valueReal : Real(uₙ)254  shows negSequence(u)[n] = -uₙ255proof256  have nNatural : n ∈ ℕ by simp [Nat]257  have function : u : ℕ → ℝ by exact sequence258  have value := compose.apply with function, realNeg.function, nNatural259  simp [negSequence]260261theorem addSequence.sequence (u v : Set)262  requires sequenceU : RealSequence(u)263  requires sequenceV : RealSequence(v)264  shows RealSequence(addSequence(u, v))265proof266  have functionU : u : ℕ → ℝ by exact sequenceU267  have functionV : v : ℕ → ℝ by exact sequenceV268  have paired := pairFunctions.function with functionU, functionV269  unfold RealSequence270  unfold addSequence271  exact compose.function with paired, realAdd.function272273theorem addSequence.value (u v : Set, n : Nat)274  requires sequenceU : RealSequence(u)275  requires sequenceV : RealSequence(v)276  requires valueUReal : Real(uₙ)277  requires valueVReal : Real(vₙ)278  shows addSequence(u, v)[n] = uₙ + vₙ279proof280  have nNatural : n ∈ ℕ by simp [Nat]281  have functionU : u : ℕ → ℝ by exact sequenceU282  have functionV : v : ℕ → ℝ by exact sequenceV283  have paired := pairFunctions.function with functionU, functionV284  have outer := compose.apply with paired, realAdd.function, nNatural285  have pairValue := pairFunctions.apply with functionU, functionV, nNatural286  unfold addSequence287  rw pairValue at outer288  simp [call2]289290theorem mulSequence.sequence (u v : Set)291  requires sequenceU : RealSequence(u)292  requires sequenceV : RealSequence(v)293  shows RealSequence(mulSequence(u, v))294proof295  have functionU : u : ℕ → ℝ by exact sequenceU296  have functionV : v : ℕ → ℝ by exact sequenceV297  have paired := pairFunctions.function with functionU, functionV298  unfold RealSequence299  unfold mulSequence300  exact compose.function with paired, realMul.function301302theorem mulSequence.value (u v : Set, n : Nat)303  requires sequenceU : RealSequence(u)304  requires sequenceV : RealSequence(v)305  requires valueUReal : Real(uₙ)306  requires valueVReal : Real(vₙ)307  shows mulSequence(u, v)[n] = uₙ * vₙ308proof309  have nNatural : n ∈ ℕ by simp [Nat]310  have functionU : u : ℕ → ℝ by exact sequenceU311  have functionV : v : ℕ → ℝ by exact sequenceV312  have paired := pairFunctions.function with functionU, functionV313  have outer := compose.apply with paired, realMul.function, nNatural314  have pairValue := pairFunctions.apply with functionU, functionV, nNatural315  unfold mulSequence316  rw pairValue at outer317  simp [call2]318319theorem invSequence.sequence (u : Set)320  requires sequence : RealSequence(u)321  shows RealSequence(invSequence(u))322proof323  unfold RealSequence at sequence324  unfold RealSequence325  unfold invSequence326  exact compose.function with sequence, realInv.function327328theorem invSequence.value (u : Set, n : Nat)329  requires sequence : RealSequence(u)330  shows invSequence(u)[n] = realInvValue(uₙ)331proof332  have nNatural : n ∈ ℕ by simp [Nat]333  have function : u : ℕ → ℝ by exact sequence334  have value := compose.apply with function, realInv.function, nNatural335  simp [invSequence, realInvValue]336337theorem divSequence.sequence (u v : Set)338  requires sequenceU : RealSequence(u)339  requires sequenceV : RealSequence(v)340  shows RealSequence(divSequence(u, v))341proof342  have functionU : u : ℕ → ℝ by exact sequenceU343  have functionV : v : ℕ → ℝ by exact sequenceV344  have paired := pairFunctions.function with functionU, functionV345  unfold RealSequence346  unfold divSequence347  exact compose.function with paired, realDiv.function348349theorem divSequence.value (u v : Set, n : Nat)350  requires sequenceU : RealSequence(u)351  requires sequenceV : RealSequence(v)352  shows divSequence(u, v)[n] = uₙ / vₙ353proof354  have nNatural : n ∈ ℕ by simp [Nat]355  have functionU : u : ℕ → ℝ by exact sequenceU356  have functionV : v : ℕ → ℝ by exact sequenceV357  have paired := pairFunctions.function with functionU, functionV358  have outer := compose.apply with paired, realDiv.function, nNatural359  have pairValue := pairFunctions.apply with functionU, functionV, nNatural360  unfold divSequence361  rw pairValue at outer362  simp [call2]363364theorem subSequence.sequence (u v : Set)365  requires sequenceU : RealSequence(u)366  requires sequenceV : RealSequence(v)367  shows RealSequence(subSequence(u, v))368proof369  have negSequenceV := negSequence.sequence with sequenceV370  unfold subSequence371  exact addSequence.sequence with sequenceU, negSequenceV372373theorem subSequence.value (u v : Set, n : Nat)374  requires sequenceU : RealSequence(u)375  requires sequenceV : RealSequence(v)376  requires valueUReal : Real(uₙ)377  requires valueVReal : Real(vₙ)378  shows subSequence(u, v)[n] = uₙ - vₙ379proof380  have negSequenceV := negSequence.sequence with sequenceV381  have negValueReal := RealSequence.value with negSequenceV382  have sumValue := addSequence.value with sequenceU, negSequenceV, valueUReal, negValueReal383  have negValue := negSequence.value with sequenceV, valueVReal384  unfold subSequence385  unfold realSubValue386  rw negValue at sumValue387  exact sumValue388389theorem ConvergesTo.neg (u : Set) (L : Real)390  requires converges : ConvergesTo(u, L)391  shows ConvergesTo(negSequence(u), -L)392proof393  have sequence := ConvergesTo.sequence with converges394  have negLimitReal := realNegValue.real at L395  constructor396  . exact negSequence.sequence with sequence397  . intros E realE positive398    have typedE : Real(E) by exact realE399    obtain ⟨N, nNatural, close⟩ := ConvergesTo.eventually with converges, positive400    witness N401    constructor402    . exact nNatural403    . intros n nInNaturals nAfterN404      have typedN : Nat(n) by exact nat.omega.backward at n with nInNaturals405      have valueInReals := RealSequence.value with sequence406      have typedValue : Real(u(n)) by exact valueInReals407      have near := close with n, nInNaturals, nAfterN408      have nearData := openBall.membership.forward at409        L, E, u(n) with near410      rcases nearData with ⟨realValue, within⟩411      have valueShape := negSequence.value with sequence412      have negValueReal := realNegValue.real with typedValue413      have negDistance := dist.neg at u(n), L with414        typedValue, assumption415      apply openBall.membership.backward416      constructor417      . rw valueShape418        exact negValueReal419      . rw valueShape420        rwa negDistance421422theorem ConvergesTo.add (u v : Set) (L M : Real)423  requires convergesU : ConvergesTo(u, L)424  requires convergesV : ConvergesTo(v, M)425  shows ConvergesTo(addSequence(u, v), L + M)426proof427  have sequenceU := ConvergesTo.sequence with convergesU428  have sequenceV := ConvergesTo.sequence with convergesV429  have sumLimitReal := realAddValue.real at L, M with *430  constructor431  . exact addSequence.sequence with sequenceU, sequenceV432  . intros E realE positive433    have typedE : Real(E) by exact realE434    have radiusReal := half.real with typedE435    have radiusPositive := half.positive with positive436    obtain ⟨N, nNatural, closeBoth⟩ := ConvergesTo.common_eventually with437      convergesU, convergesV, radiusPositive, radiusPositive438    witness N439    constructor440    . exact nNatural441    . intros n nInNaturals nAfterN442      have typedN : Nat(n) by exact nat.omega.backward at n with nInNaturals443      obtain ⟨nearU, nearV⟩ := closeBoth with n, nInNaturals, nAfterN444      have uInReals := RealSequence.value with sequenceU445      have vInReals := RealSequence.value with sequenceV446      have typedU : Real(u(n)) by exact uInReals447      have typedV : Real(v(n)) by exact vInReals448      have uData := openBall.membership.forward at449        L, half(E), u(n) with nearU450      have vData := openBall.membership.forward at451        M, half(E), v(n) with nearV452      rcases uData with ⟨realU, closeU⟩453      rcases vData with ⟨realV, closeV⟩454      have sumValueReal := realAddValue.real with typedU, typedV455      have firstDistanceReal := dist.real at u(n), L with456        typedU, assumption457      have secondDistanceReal := dist.real at v(n), M with458        typedV, assumption459      have distanceSumReal := realAddValue.real with firstDistanceReal, secondDistanceReal460      have totalDistanceReal := dist.real with sumValueReal, sumLimitReal461      have distanceBound := dist.add_add at462        u(n), v(n), L, M with463          typedU, typedV, *{2}464      have radiusSumBound := realLess.add with465        firstDistanceReal, radiusReal, secondDistanceReal, radiusReal, closeU, closeV466      have doubled := half.add_self with typedE467      rw doubled at radiusSumBound468      have within := realLe.transitive_less with469        totalDistanceReal, distanceSumReal, typedE, distanceBound, radiusSumBound470      have valueShape := addSequence.value with sequenceU, sequenceV471      apply openBall.membership.backward472      constructor473      . rw valueShape474        unfold call2475        unfold call2 at sumValueReal476        exact sumValueReal477      . rw valueShape478        unfold call2479        unfold call2 at within480        exact within481482-- Products of convergent real sequences converge to the product of their483-- limits.  The estimate is the one used in a handwritten proof:484--485--   |uₙvₙ - LM| ≤ |uₙ| |vₙ - M| + |M| |uₙ - L|.486--487-- First make uₙ locally bounded, then assign half of epsilon to each term.488theorem ConvergesTo.mul (u v : Set) (L M : Real)489  requires convergesU : ConvergesTo(u, L)490  requires convergesV : ConvergesTo(v, M)491  shows ConvergesTo(mulSequence(u, v), L * M)492proof493  have sequenceU := ConvergesTo.sequence with convergesU494  have sequenceV := ConvergesTo.sequence with convergesV495  have productLimitReal := realMulValue.real at L, M with496    *{2}497  constructor498  . exact mulSequence.sequence with sequenceU, sequenceV499  . intros E realE positiveE500    have typedE : Real(E) by exact realE501    have scaleMReal := limitScale.real at M502    have scaleMPositive := limitScale.positive at M503    have radiusUReal := scaledRadius.real with typedE, scaleMReal504    have radiusUPositive := scaledRadius.positive with positiveE, scaleMPositive505    have absLReal := abs.real at L506    have boundReal := realAddValue.real with radiusUReal, absLReal507    have radiusAboveAbsL := realLess.add_right with realZero.real, radiusUReal, absLReal, radiusUPositive508    have zeroPlusAbsL := realAddValue.zero_left with absLReal509    rw zeroPlusAbsL at radiusAboveAbsL510    have boundPositive := realLe.transitive_less at511      realZero, abs(L), scaledRadius(E, limitScale(M)) + abs(L) with512        realZero.real, absLReal, boundReal,513        abs.nonnegative at L with assumption, radiusAboveAbsL514    have radiusVReal := scaledRadius.real with typedE, boundReal515    have radiusVPositive := scaledRadius.positive with positiveE, boundPositive516    obtain ⟨N, nNatural, closeBoth⟩ := ConvergesTo.common_eventually with517      convergesU, convergesV, radiusUPositive, radiusVPositive518    witness N519    constructor520    . exact nNatural521    . intros n nInNaturals nAfterN522      have typedN : Nat(n) by exact nat.omega.backward at n with nInNaturals523      obtain ⟨nearU, nearV⟩ := closeBoth with n, nInNaturals, nAfterN524      have typedU := RealSequence.value with sequenceU525      have typedV := RealSequence.value with sequenceV526      have uData := openBall.membership.forward at527        L, scaledRadius(E, limitScale(M)), uₙ with nearU528      have vData := openBall.membership.forward at529        M, scaledRadius(E, scaledRadius(E, limitScale(M)) + abs(L)), vₙ530        with nearV531      rcases uData with ⟨realU, closeU⟩532      rcases vData with ⟨realV, closeV⟩533534      -- Closeness to L supplies the local bound |uₙ| < radiusU + |L|.535      have absUReal := abs.real with typedU536      have distUReal := dist.real at uₙ, L with typedU537      have distVReal := dist.real at vₙ, M with typedV538      have absUBound := abs.le_dist_add_abs at uₙ, L with539        typedU, assumption540      have closeUWithAbsL := realLess.add_right with distUReal, radiusUReal, absLReal, closeU541      have distPlusAbsReal := realAddValue.real with distUReal, absLReal542      have uBounded := realLe.transitive_less with543        absUReal, distPlusAbsReal, boundReal, absUBound, closeUWithAbsL544545      -- Each summand in the product estimate is strictly below E/2.546      have uBoundedLe := realLess.implies_le with absUReal, boundReal, uBounded547      have distVNonnegative := dist.nonnegative at vₙ, M with548        typedV, assumption549      have firstWeak := realLe.mul_right_of_nonnegative with550        absUReal, boundReal, distVReal, uBoundedLe, distVNonnegative551      have firstStrict := realLess.mul_left_of_positive with552        distVReal, radiusVReal, boundReal, closeV, boundPositive553      have firstTermReal := realMulValue.real with absUReal, distVReal554      have firstMiddleReal := realMulValue.real with boundReal, distVReal555      have firstUpperReal := realMulValue.real with boundReal, radiusVReal556      have firstBelowProduct := realLe.transitive_less with557        firstTermReal, firstMiddleReal, firstUpperReal, firstWeak, firstStrict558      have firstCancellation := scaledRadius.cancel with typedE, boundReal, boundPositive559      rw firstCancellation at firstBelowProduct560561      have absMReal := abs.real at M562      have absMLess := abs.lt_limitScale at M563      have absMLe := realLess.implies_le with absMReal, scaleMReal, absMLess564      have distUNonnegative := dist.nonnegative at uₙ, L with565        typedU, assumption566      have secondWeak := realLe.mul_right_of_nonnegative with567        absMReal, scaleMReal, distUReal, absMLe, distUNonnegative568      have secondStrict := realLess.mul_left_of_positive with569        distUReal, radiusUReal, scaleMReal, closeU, scaleMPositive570      have secondTermReal := realMulValue.real with absMReal, distUReal571      have secondMiddleReal := realMulValue.real with scaleMReal, distUReal572      have secondUpperReal := realMulValue.real with scaleMReal, radiusUReal573      have secondBelowProduct := realLe.transitive_less with574        secondTermReal, secondMiddleReal, secondUpperReal, secondWeak, secondStrict575      have secondCancellation := scaledRadius.cancel with typedE, scaleMReal, scaleMPositive576      rw secondCancellation at secondBelowProduct577578      have estimate := dist.mul_mul at uₙ, vₙ, L, M with579        typedU, typedV, *{2}580      have halfReal := half.real with typedE581      have sumBelow := realLess.add with582        firstTermReal, halfReal, secondTermReal, halfReal, firstBelowProduct, secondBelowProduct583      have doubled := half.add_self with typedE584      rw doubled at sumBelow585      have productValueReal := realMulValue.real with typedU, typedV586      have totalDistanceReal := dist.real with productValueReal, productLimitReal587      have estimateSumReal := realAddValue.real with firstTermReal, secondTermReal588      have within := realLe.transitive_less with589        totalDistanceReal, estimateSumReal, typedE, estimate, sumBelow590      have valueShape := mulSequence.value with sequenceU, sequenceV, typedU, typedV591      apply openBall.membership.backward592      constructor593      . rw valueShape594        exact productValueReal595      . rw valueShape596        exact within597598-- A convergent sequence may be inverted when its limit is nonzero.  The599-- proof is the textbook one: first keep the sequence at least |L|/2 away600-- from zero, then use601--602--   |uₙ⁻¹ - L⁻¹| = |uₙ - L| |uₙ⁻¹| |L⁻¹|.603theorem ConvergesTo.inv (u : Set) (L : Real)604  requires converges : ConvergesTo(u, L)605  requires nonzero : L ≠ 0606  shows ConvergesTo(invSequence(u), realInvValue(L))607proof608  have sequence := ConvergesTo.sequence with converges609  have inverseLimitReal := realInvValue.real at L610  constructor611  . exact invSequence.sequence with sequence612  . intros E realE positiveE613    have typedE : Real(E) by exact realE614    have absLReal := abs.real at L615    have absLPositive := abs.positive_of_ne with nonzero616    have halfAbsLReal := half.real with absLReal617    have halfAbsLPositive := half.positive with absLPositive618    have scaleReal := inverseScale.real at L619    have scalePositive := inverseScale.positive with nonzero620    have radiusReal := scaledRadius.real with typedE, scaleReal621    have radiusPositive := scaledRadius.positive with positiveE, scalePositive622    obtain ⟨N, nNatural, closeBoth⟩ := ConvergesTo.common_eventually with623      converges, converges, halfAbsLPositive, radiusPositive624    witness N625    constructor626    . exact nNatural627    . intros n nInNaturals nAfterN628      have typedN : Nat(n) by exact nat.omega.backward at n with nInNaturals629      obtain ⟨nearZero, nearE⟩ := closeBoth with n, nInNaturals, nAfterN630      have typedU := RealSequence.value with sequence631      have zeroData := openBall.membership.forward at632        L, half(abs(L)), uₙ with nearZero633      have epsilonData := openBall.membership.forward at634        L, scaledRadius(E, inverseScale(L)), uₙ with nearE635      rcases zeroData with ⟨realU, closeZero⟩636      rcases epsilonData with ⟨realUAgain, closeE⟩637638      have lower := abs.half_lt_of_dist_lt_half with typedU, nonzero, closeZero639      have nonzeroU : uₙ ≠ 0640        intro equal641        have absoluteZero := abs.zero642        rw [equal, absoluteZero] at lower643        have irreflexive := realLess.irreflexive_on644        have cycle := realLess.transitive with645          realZero.real, halfAbsLReal, realZero.real, halfAbsLPositive, lower646        exact irreflexive with realZero, cycle647648      -- Reciprocation reverses the lower bound |L|/2 < |uₙ|.649      have inverseBound := realInvValue.antitone_positive with halfAbsLReal, halfAbsLPositive, lower650      have absInverseU := abs.inv with typedU, nonzeroU651      rw ← absInverseU at inverseBound652653      have inverseLReal := realInvValue.real at L654      have inverseLNonzero := realInvValue.nonzero with nonzero655      have absInverseLReal := abs.real with inverseLReal656      have absInverseLPositive := abs.positive_of_ne with inverseLNonzero657      have factorBound := realLess.mul_right_of_positive at658        abs(realInvValue(uₙ)), realInvValue(half(abs(L))),659        abs(realInvValue(L)) with660          abs.real at realInvValue(uₙ) with661            realInvValue.real at uₙ with typedU,662          realInvValue.real at half(abs(L)) with halfAbsLReal,663          absInverseLReal, inverseBound, absInverseLPositive664      have factorBoundScale : abs(realInvValue(uₙ)) *665          abs(realInvValue(L)) < inverseScale(L)666        unfold inverseScale667        exact factorBound668669      -- Multiply the two strict estimates, using nonnegativity of distance670      -- for the weak first step.671      have distanceReal := dist.real at uₙ, L with typedU672      have factorReal := realMulValue.real at673        abs(realInvValue(uₙ)), abs(realInvValue(L)) with674          abs.real at realInvValue(uₙ) with675            realInvValue.real at uₙ with typedU,676          absInverseLReal677      have distanceNonnegative := dist.nonnegative at uₙ, L with678        typedU, assumption679      have factorLe := realLess.implies_le with factorReal, scaleReal, factorBoundScale680      have weakProduct := realLe.mul_left_of_nonnegative with681        factorReal, scaleReal, distanceReal, factorLe, distanceNonnegative682      have strictProduct := realLess.mul_right_of_positive with683        distanceReal, radiusReal, scaleReal, closeE, scalePositive684      have lowerProductReal := realMulValue.real with distanceReal, factorReal685      have middleProductReal := realMulValue.real with distanceReal, scaleReal686      have upperProductReal := realMulValue.real with radiusReal, scaleReal687      have productBelow := realLe.transitive_less with688        lowerProductReal, middleProductReal, upperProductReal, weakProduct, strictProduct689      have cancellation := scaledRadius.cancel with typedE, scaleReal, scalePositive690      have commute := realMulValue.commutative with radiusReal, scaleReal691      rw [commute, cancellation] at productBelow692      have halfBelowE := half.lt_self with typedE, positiveE693      have halfReal := half.real with typedE694      have productBelowE := realLess.transitive with695        lowerProductReal, halfReal, typedE, productBelow, halfBelowE696      have inverseDistance := dist.inv_inv with typedU, nonzeroU, nonzero697      rw ← inverseDistance at productBelowE698699      have valueShape := invSequence.value with sequence700      apply openBall.membership.backward701      constructor702      . rw valueShape703        exact realInvValue.real with typedU704      . rw valueShape705        exact productBelowE706707theorem ConvergesTo.sub (u v : Set) (L M : Real)708  requires convergesU : ConvergesTo(u, L)709  requires convergesV : ConvergesTo(v, M)710  shows ConvergesTo(subSequence(u, v), L - M)711proof712  have negConverges := ConvergesTo.neg with convergesV713  have sumConverges := ConvergesTo.add with convergesU, negConverges714  unfold subSequence715  unfold realSubValue716  exact sumConverges717718-- A real sequence has at most one limit. The proof uses the ball of radius719-- half the distance between two proposed limits.720theorem ConvergesTo.unique (u : Set) (L M : Real)721  requires convergesL : ConvergesTo(u, L)722  requires convergesM : ConvergesTo(u, M)723  shows L = M724proof725  by_contra unequal726  have distancePositive := dist.positive_of_ne with unequal727  have radiusPositive := half.positive with distancePositive728  obtain ⟨n, nNatural, closeBoth⟩ := ConvergesTo.common_eventually with729    convergesL, convergesM, radiusPositive, radiusPositive730  have typedN : Nat(n) by exact nat.omega.backward at n with nNatural731  have nLeN := LessEqual.reflexive with typedN732  obtain ⟨nearL, nearM⟩ := closeBoth with n, nNatural, nLeN733  have sequence := ConvergesTo.sequence with convergesL734  have valueInReals := RealSequence.value with sequence735  have equal := openBall.half_radius_unique with nearL, nearM736  exact unequal with equal737738def constantSequence (L : Real) : Set :=739  { p ∈ ℕ × ℝ | ∃ n ∈ ℕ, p = (n ↦ L) }740741theorem constantSequence.relates (L : Real, n : Nat)742  shows relates(constantSequence(L), n, L)743proof744  have nInNaturals : n ∈ ℕ by simp [Nat]745  have lInReals : L ∈ ℝ by simp [Real]746  unfold relates747  apply constantSequence.membership.backward748  constructor749  . exact product.pair with nInNaturals, lInReals750  . refine ⟨n, nInNaturals, rfl⟩751752theorem constantSequence.function (L : Real)753  shows constantSequence(L) : ℕ → ℝ754proof755  constructor756    intros p member757    obtain ⟨bounded, witnesses⟩ := constantSequence.membership.forward with member758    exact bounded759  . constructor760      intros n A nA B nB761      unfold relates at nA762      obtain ⟨_, i, iNatural, firstShape⟩ := constantSequence.membership.forward with nA763      unfold relates at nB764      obtain ⟨_, j, jNatural, secondShape⟩ := constantSequence.membership.forward with nB765      have firstCoordinates := orderedPair.injective with firstShape766      have secondCoordinates := orderedPair.injective with secondShape767      rcases firstCoordinates with ⟨_, equalA⟩768      rcases secondCoordinates with ⟨_, equalB⟩769      rw [equalA, equalB]770      rfl771    . intros n nNatural772      witness L773      constructor774      . settle with Real775      . have typedN : Nat(n)776          exact nNatural777        exact constantSequence.relates with assumption, typedN778779theorem constantSequence.sequence (L : Real)780  shows RealSequence(constantSequence(L))781proof782  unfold RealSequence783  exact constantSequence.function with assumption784785theorem constantSequence.value (L : Real, n : Nat)786  shows constantSequence(L)(n) = L787proof788  have function := constantSequence.function at L789  have mapped := constantSequence.relates with *790  exact FunctionBetween.apply_value with function, mapped791792theorem constantSequence.converges (L : Real)793  shows ConvergesTo(constantSequence(L), L)794proof795  constructor796  . exact constantSequence.sequence at L797  . intros E realE positive798    witness 0799    constructor800    . exact nat.omega.forward at 0 with Naturals.constructor.zero801    . intros n nNatural zeroLeN802      have typedN : Nat(n) by exact nNatural803      have value := constantSequence.value with assumption, typedN804      rw value805      exact openBall.center with positive806807-- Changing finitely many terms cannot change the limit of a sequence.808theorem ConvergesTo.eventually_equal (u v : Set) (L : Real)809  requires converges : ConvergesTo(u, L)810  requires sequenceV : RealSequence(v)811  requires eventuallyEqual : EventuallyEqual(u, v)812  shows ConvergesTo(v, L)813proof814  rcases converges with ⟨sequenceU, eventuallyClose⟩815  obtain ⟨M, mNatural, equalAfterM⟩ := eventuallyEqual816  have typedM : Nat(M) by exact nat.omega.backward at M with mNatural817  constructor818  . exact sequenceV819  . intros E realE positive820    obtain ⟨N, nNatural, closeAfterN⟩ :=821      eventuallyClose with E, realE, positive822    have typedN : Nat(N) by exact nat.omega.backward at N with nNatural823    have comparison := Less.trichotomy with typedN, typedM824    cases comparison with nLessM | rest825    . witness M826      constructor827      . exact mNatural828      . intros n nInNaturals mLeN829        have nLeM := Less.implies_LessEqual with nLessM830        have nLeLittleN := LessEqual.transitive with nLeM, mLeN831        have close := closeAfterN with n, nInNaturals, nLeLittleN832        have equal := equalAfterM with n, nInNaturals, mLeN833        rwa equal at close834    . cases rest with equalNM | mLessN835      . witness N836        constructor837        . exact nNatural838        . intros n nInNaturals nLeLittleN839          have close := closeAfterN with n, nInNaturals, nLeLittleN840          have mLeLittleN : M ≤ n by rwa ← equalNM841          have equal := equalAfterM with n, nInNaturals, mLeLittleN842          rwa equal at close843844      . witness N845        constructor846        . exact nNatural847        . intros n nInNaturals nLeLittleN848          have mLeN := Less.implies_LessEqual with typedM, typedN, mLessN849          have mLeLittleN := LessEqual.transitive with typedM, typedN, mLeN, nLeLittleN850          have close := closeAfterN with n, nInNaturals, nLeLittleN851          have equal := equalAfterM with n, nInNaturals, mLeLittleN852          rwa equal at close853854-- Quotients now follow from the product and reciprocal rules.  The short855-- proof is precisely the payoff of treating `/` as the field operation.856theorem ConvergesTo.div (u v : Set) (L M : Real)857  requires convergesU : ConvergesTo(u, L)858  requires convergesV : ConvergesTo(v, M)859  requires nonzeroM : M ≠ 0860  shows ConvergesTo(divSequence(u, v), L / M)861proof862  have sequenceU := ConvergesTo.sequence with convergesU863  have sequenceV := ConvergesTo.sequence with convergesV864  have inverseConverges := ConvergesTo.inv with convergesV, nonzeroM865  have productConverges := ConvergesTo.mul with convergesU, inverseConverges866  have limitShape := realDiv.eq_mul_inv at L, M with *867  rw limitShape868  apply ConvergesTo.eventually_equal with productConverges869  . exact divSequence.sequence with sequenceU, sequenceV870    witness 0871    constructor872    . exact nat.omega.forward at 0 with Naturals.constructor.zero873    . intros n nNatural zeroLeN874      have typedN : Nat(n) by exact nat.omega.backward at n with nNatural875      have inverseSequence := invSequence.sequence with sequenceV876      have inverseValueReal := RealSequence.value with inverseSequence877      have valueUReal := RealSequence.value with sequenceU878      have valueVReal := RealSequence.value with sequenceV879      have mulValue := mulSequence.value with sequenceU, inverseSequence, valueUReal, inverseValueReal880      have invValue := invSequence.value with sequenceV881      have divValue := divSequence.value with sequenceU, sequenceV882      have quotientValue := realDiv.eq_mul_inv with valueUReal, valueVReal883      rw [mulValue, invValue, divValue, quotientValue]884      rfl885886-- Section: OrderLimits887theorem openBall.order_characterization (X C E : Real)888  shows X ∈ openBall(C, E) ↔ (C - E < X ∧ X < C + E)889proof890  have differenceReal := realSubValue.real at X, C with *891  have negDifferenceReal := realNegValue.real with differenceReal892  have negDifference : -(X - C) = C - X893    unfold realSubValue894    have negCReal := realNegValue.real at C895    have negXReal := realNegValue.real at X896    have distributed := realNegValue.add at X, -C with897      assumption, negCReal898    have involutive := realNegValue.involutive at C899    have commute := realAddValue.commutative at -X, C with900      negXReal, assumption901    cc902  constructor903  . intro member904    obtain ⟨_, within⟩ := openBall.membership.forward with member905    unfold dist at within906    have upperDifference := realLe.transitive_less at907      X - C, abs(X - C), E with908        differenceReal, abs.real at X - C with differenceReal, assumption,909        abs.upper at X - C with differenceReal, within910    have lowerDifference := realLe.transitive_less at911      -(X - C), abs(X - C), E with912        negDifferenceReal, abs.real at X - C with differenceReal, assumption,913        abs.upper_neg at X - C with differenceReal, within914    have upper := realLess.add_right at X - C, E, C with915      differenceReal, *{2}, upperDifference916    have lower := realLess.add_right at -(X - C), E, X with917      negDifferenceReal, *{2}, lowerDifference918    have upperLeft := realSubValue.add_right_cancel at X, C with919      *{2}920    have upperRight := realAddValue.commutative at E, C with921      *{2}922    rw [upperLeft, upperRight] at upper923    rw negDifference at lower924    have lowerLeft := realSubValue.add_right_cancel at C, X with925      *{2}926    rw lowerLeft at lower927    have lowerRight := realAddValue.commutative at E, X with928      *{2}929    rw lowerRight at lower930    have lowerShifted : (C - E) + E < X + E931      have cancel := realSubValue.add_right_cancel at C, E with932        *{2}933      rwa cancel934    have cMinusEReal := realSubValue.real at C, E with *935    have lowerFinal := realLess.add_right_iff.forward with lowerShifted936    constructor937    . exact lowerFinal938    . exact upper939  . intro bounds940    rcases bounds with ⟨lower, upper⟩941    have sumCEReal := realAddValue.real at C, E with *942    have sumXEReal := realAddValue.real at X, E with *943    have negCReal := realNegValue.real at C944    have negXReal := realNegValue.real at X945    have cMinusEReal := realSubValue.real at C, E with *946    have upperDifference := realLess.add_right at X, C + E, -C with947      assumption, sumCEReal, negCReal, upper948    have lowerDifference := realLess.add_right at C - E, X, E with949      cMinusEReal, *{2}, lower950    have cancelCE := realSubValue.add_right_cancel at C, E with951      *{2}952    rw cancelCE at lowerDifference953    have lowerDifferenceAgain := realLess.add_right at954      C, X + E, -X with955        assumption, sumXEReal, negXReal, lowerDifference956    have commuteCE := realAddValue.commutative at C, E with957      *{2}958    rw commuteCE at upperDifference959    have cancelEC := realSubValue.add_cancel_right at E, C with960      *{2}961    unfold realSubValue at cancelEC962    rw cancelEC at upperDifference963    have commuteXE := realAddValue.commutative at X, E with964      *{2}965    rw commuteXE at lowerDifferenceAgain966    have cancelEX := realSubValue.add_cancel_right at E, X with967      *{2}968    unfold realSubValue at cancelEX969    rw cancelEX at lowerDifferenceAgain970    have sign := Real.sign_cases with differenceReal971    apply openBall.membership.backward972    constructor973    . settle with Real974    . unfold dist975      cases sign with nonpositive | nonnegative976      . have nonpositiveLe := realLe.of_subset at X - C, realZero with977          differenceReal, realZero.real, nonpositive978        have absolute := abs.of_nonpositive with nonpositiveLe979        rw [absolute, negDifference]980        unfold realSubValue981        exact lowerDifferenceAgain982      . have nonnegativeLe := realLe.of_subset at realZero, X - C with983          realZero.real, differenceReal, nonnegative984        have absolute := abs.of_nonnegative with nonnegativeLe985        rw absolute986        unfold realSubValue987        exact upperDifference988989-- A sequence is eventually bounded when one positive real bounds the990-- absolute values of all terms in a tail.991predicate EventuallyBounded (u : Set) :=992  RealSequence(u) ∧993  (∃ B ∈ ℝ, 0 < B ∧994    (∃ N ∈ ℕ, (∀ n ∈ ℕ, N ≤ n →995      u(n) ∈ openBall(realZero, B))))996997predicate NonnegativeTerms (u : Set) :=998  ∀ n ∈ ℕ, RealLe(realZero, u(n))9991000predicate PointwiseLE (u v : Set) :=1001  ∀ n ∈ ℕ, RealLe(u(n), v(n))10021003predicate BoundedAboveBy (u : Set) (B : Real) :=1004  ∀ n ∈ ℕ, RealLe(u(n), B)10051006predicate BoundedBelowBy (u : Set) (A : Real) :=1007  ∀ n ∈ ℕ, RealLe(A, u(n))10081009predicate UnitIntervalTerms (u : Set) :=1010  ∀ n ∈ ℕ,1011    RealLe(realZero, u(n)) ∧ RealLe(u(n), realOne)10121013-- Every convergent sequence is bounded on a tail.  The familiar estimate1014-- |uₙ| ≤ |uₙ - L| + |L| gives the explicit bound |L| + 1.1015-- A value within half of E of C on both sides lies in the open E-ball around C.1016theorem openBall.of_half_bounds (Q C E : Real)1017  requires positive : 0 < E1018  requires low : C - half(E) ≤ Q1019  requires high : Q ≤ C + half(E)1020  shows Q ∈ openBall(C, E)1021proof1022  have halfLess := half.lt_self with *1023  have bounds : C - E < Q ∧ Q < C + E1024    constructor1025    . linarith1026    . linarith1027  exact openBall.order_characterization.backward with bounds10281029theorem ConvergesTo.eventually_bounded (u : Set) (L : Real)1030  requires converges : ConvergesTo(u, L)1031  shows EventuallyBounded(u)1032proof1033  have boundReal := limitScale.real at L1034  have boundPositive := limitScale.positive at L1035  obtain ⟨N, nNatural, close⟩ := ConvergesTo.eventually with converges, realZero.lt_one1036  constructor1037  . exact ConvergesTo.sequence with converges1038  . witness limitScale(L)1039    constructor1040      exact boundReal1041    . constructor1042      . exact boundPositive1043      . witness N1044        constructor1045        . exact nNatural1046        . intros n nInNaturals nAfterN1047          have sequence := ConvergesTo.sequence with converges1048          have typedN : Nat(n) by exact nat.omega.backward at n with nInNaturals1049          have typedValue := RealSequence.value with sequence1050          have near := close with n, nInNaturals, nAfterN1051          have nearData := openBall.membership.forward at1052            L, realOne, uₙ with near1053          rcases nearData with ⟨_, distanceLessOne⟩1054          have distanceReal := dist.real at uₙ, L with typedValue1055          have absLReal := abs.real at L1056          have sumReal := realAddValue.real with distanceReal, absLReal1057          have absoluteBound := abs.le_dist_add_abs at uₙ, L with1058            typedValue, assumption1059          have sumBelow := realLess.add_right with distanceReal, realOne.real, absLReal, distanceLessOne1060          have absValueReal := abs.real with typedValue1061          have onePlusAbsReal := realAddValue.real with realOne.real, absLReal1062          have strictBound := realLe.transitive_less with1063            absValueReal, sumReal, onePlusAbsReal, absoluteBound, sumBelow1064          have commute := realAddValue.commutative with realOne.real, absLReal1065          unfold limitScale1066          rw commute at strictBound1067          apply openBall.membership.backward1068          constructor1069            exact typedValue1070          . unfold dist1071            have zero := realSubValue.zero_right with typedValue1072            rwa zero10731074-- A nonnegative sequence cannot converge to a negative number.  The proof1075-- chooses the ball of radius -L/2 around a hypothetical negative limit L;1076-- every point in that ball is still negative.1077theorem ConvergesTo.nonnegative_of_nonnegative_terms (u : Set) (L : Real)1078  requires converges : ConvergesTo(u, L)1079  requires nonnegative : NonnegativeTerms(u)1080  shows 0 ≤ L1081proof1082  have sign := Real.sign_cases at L1083  cases sign with nonpositive | nonnegativeCut1084  . by_contra notNonnegative1085    have unequalZero : L ≠ 01086      intro equalZero1087      apply notNonnegative1088      rw equalZero1089      exact realLe.reflexive with realZero.real1090    have negative : L < 01091        apply realLess.characterization.backward1092        unfold RealLess1093        refine ⟨assumption, realZero.real, _⟩1094        unfold ProperSubset1095        refine ⟨nonpositive, unequalZero⟩1096    have negativeView := realLess.characterization.forward with negative1097    have reversed := RealLess.neg_reverse at L, realZero with1098        assumption, realZero.real, negativeView1099    have positiveNeg : 0 < -L1100      apply realLess.characterization.backward1101      rwa realNegValue.zero at reversed1102    have negLReal := realNegValue.real at L1103    have radiusReal := half.real with negLReal1104    have radiusPositive := half.positive with positiveNeg1105    obtain ⟨N, nNatural, close⟩ := ConvergesTo.eventually with converges, radiusPositive1106    have typedN : Nat(N) by exact nat.omega.backward at N with nNatural1107    have nLeN := LessEqual.reflexive with typedN1108    have near := close with N, nNatural, nLeN1109    have sequence := ConvergesTo.sequence with converges1110    have typedValue := RealSequence.value with sequence1111    have nearData := openBall.membership.forward at1112      L, half(-L), u[N] with near1113    rcases nearData with ⟨_, distanceBelowHalf⟩1114    have halfBelowNeg := half.lt_self with positiveNeg1115    have distanceReal := dist.real at u[N], L with typedValue1116    have distanceBelowNeg := realLess.transitive with1117      distanceReal, radiusReal, negLReal, distanceBelowHalf, halfBelowNeg1118    have differenceReal := realSubValue.real at u[N], L with1119      typedValue, assumption1120    have differenceAbsoluteReal := abs.real with differenceReal1121    have differenceUpper := abs.upper with differenceReal1122    unfold dist at distanceBelowNeg1123    have differenceBelowNeg := realLe.transitive_less with1124      differenceReal, differenceAbsoluteReal, negLReal, differenceUpper, distanceBelowNeg1125    have shifted := realLess.add_right at1126      u[N] - L, -L, L with1127        differenceReal, negLReal, assumption, differenceBelowNeg1128    have cancel := realSubValue.add_right_cancel at u[N], L with1129      typedValue, assumption1130    have inverse := realAddValue.neg_left at L1131    rw [cancel, inverse] at shifted1132    have termNonnegativeView := nonnegative with N, nNatural1133    have termNonnegative := realLe.characterization.backward with termNonnegativeView1134    have impossible := realLe.transitive_less with1135      realZero.real, typedValue, realZero.real, termNonnegative, shifted1136    exact IsOrderedField.irreflexive with reals.ordered_field, impossible1137  . exact realLe.of_subset at realZero, L with1138      realZero.real, assumption, nonnegativeCut11391140-- Termwise order passes to limits.  Apply the preceding theorem to the1141-- convergent difference vₙ - uₙ, then translate 0 ≤ M - L by L.1142theorem ConvergesTo.le_of_le_terms (u v : Set) (L M : Real)1143  requires convergesU : ConvergesTo(u, L)1144  requires convergesV : ConvergesTo(v, M)1145  requires ordered : PointwiseLE(u, v)1146  shows L ≤ M1147proof1148  have sequenceU := ConvergesTo.sequence with convergesU1149  have sequenceV := ConvergesTo.sequence with convergesV1150  have differenceConverges := ConvergesTo.sub with convergesV, convergesU1151  have differenceNonnegative : NonnegativeTerms(subSequence(v, u))1152    intros n nNatural1153    have typedN : Nat(n) by exact nat.omega.backward at n with nNatural1154    have typedU := RealSequence.value with sequenceU1155    have typedV := RealSequence.value with sequenceV1156    have value := subSequence.value with sequenceV, sequenceU, typedV, typedU1157    have termOrderView := ordered with n, nNatural1158    have termOrder := realLe.characterization.backward with termOrderView1159    have subset := realLe.subset with typedU, typedV, termOrder1160    have nonnegativeDifference := realSubValue.nonnegative_of_subset with typedU, typedV, subset1161    have differenceReal := realSubValue.real with typedV, typedU1162    rw value1163    have nonnegativeLe := realLe.of_subset with realZero.real, nonnegativeDifference1164    exact realLe.characterization.forward with nonnegativeLe1165  have limitDifferenceNonnegative := ConvergesTo.nonnegative_of_nonnegative_terms with1166    differenceConverges, differenceNonnegative1167  have differenceReal := realSubValue.real at M, L with *1168  have translated := realLe.add_right at1169    realZero, M - L, L with1170      realZero.real, differenceReal, assumption,1171      limitDifferenceNonnegative1172  have zero := realAddValue.zero_left at L1173  have cancel := realSubValue.add_right_cancel at M, L with1174    *{2}1175  rwa [zero, cancel] at translated11761177theorem ConvergesTo.le_constant (u : Set) (L B : Real)1178  requires converges : ConvergesTo(u, L)1179  requires bounded : BoundedAboveBy(u, B)1180  shows L ≤ B1181proof1182  have constantConverges := constantSequence.converges at B1183  apply ConvergesTo.le_of_le_terms with converges, constantConverges1184  intros n nNatural1185  have typedN : Nat(n) by exact nat.omega.backward at n with nNatural1186  have value := constantSequence.value at B, n with assumption, typedN1187  rw value1188  exact bounded with n, nNatural11891190theorem ConvergesTo.ge_constant (u : Set) (L A : Real)1191  requires converges : ConvergesTo(u, L)1192  requires bounded : BoundedBelowBy(u, A)1193  shows A ≤ L1194proof1195  have constantConverges := constantSequence.converges at A1196  apply ConvergesTo.le_of_le_terms with constantConverges, converges1197  intros n nNatural1198  have typedN : Nat(n) by exact nat.omega.backward at n with nNatural1199  have value := constantSequence.value at A, n with assumption, typedN1200  rw value1201  exact bounded with n, nNatural12021203-- The squeeze theorem now has its textbook order-theoretic proof: pass both1204-- inequalities to the limit and use antisymmetry.1205theorem ConvergesTo.squeeze (u v w : Set) (L : Real)1206  requires convergesU : ConvergesTo(u, L)1207  requires sequenceV : RealSequence(v)1208  requires convergesW : ConvergesTo(w, L)1209  requires lower : PointwiseLE(u, v)1210  requires upper : PointwiseLE(v, w)1211  shows ConvergesTo(v, L)1212proof1213  constructor1214  . exact sequenceV1215  . intros E realE positiveE1216    have typedE : Real(E) by exact realE1217    obtain ⟨N, nNatural, close⟩ := ConvergesTo.common_eventually with1218      convergesU, convergesW, positiveE, positiveE1219    witness N1220    constructor1221    . exact nNatural1222    . intros n nInNaturals nAfterN1223      have typedN : Nat(n) by exact nat.omega.backward at n with nInNaturals1224      have sequenceU := ConvergesTo.sequence with convergesU1225      have sequenceW := ConvergesTo.sequence with convergesW1226      have typedU := RealSequence.value with sequenceU1227      have typedV := RealSequence.value with sequenceV1228      have typedW := RealSequence.value with sequenceW1229      obtain ⟨nearU, nearW⟩ := close with n, nInNaturals, nAfterN1230      have intervalU := openBall.order_characterization.forward at1231        uₙ, L, E with typedU, assumption, typedE, nearU1232      have intervalW := openBall.order_characterization.forward at1233        wₙ, L, E with typedW, assumption, typedE, nearW1234      rcases intervalU with ⟨lowerU, _⟩1235      rcases intervalW with ⟨_, upperW⟩1236      have uLeVView := lower with n, nInNaturals1237      have vLeWView := upper with n, nInNaturals1238      have uLeV := realLe.characterization.backward with uLeVView1239      have vLeW := realLe.characterization.backward with vLeWView1240      have lowerEndpointReal := realSubValue.real at L, E with1241        assumption, typedE1242      have lowerV := realLess.transitive_le with lowerEndpointReal, typedU, typedV, lowerU, uLeV1243      have upperV := realLe.transitive_less with typedV, typedW, vLeW, upperW1244      apply openBall.order_characterization.backward with typedV1245      constructor1246      . exact lowerV1247      . exact upperV1248