Grace/Cumulus/Real/Analysis/SequentialCompactness.g17

Open in Workbench Download source

Imports

Nat.Least · Sequences · Intervals

Declarations

Source

1-- Real analysis: SequentialCompactness2-- 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.SequentialCompactness8import Nat.Least9import Sequences10import Intervals1112-- Section: Monotone13predicate Nondecreasing (u : Set) :=14  ∀ m ∈ ℕ, ∀ n ∈ ℕ, m ≤ n →15    RealLe(u(m), u(n))1617predicate Nonincreasing (u : Set) :=18  ∀ m ∈ ℕ, ∀ n ∈ ℕ, m ≤ n →19    RealLe(u(n), u(m))2021predicate StepwiseNondecreasing (u : Set) :=22  ∀ n ∈ ℕ, RealLe(u[n], u[succ(n)])2324predicate StepwiseNonincreasing (u : Set) :=25  ∀ n ∈ ℕ, RealLe(u[succ(n)], u[n])2627theorem StepwiseNondecreasing.offset (u : Set, m k : Nat)28  requires sequence : RealSequence(u)29  requires stepwise : StepwiseNondecreasing(u)30  shows RealLe(u[m], u[m + k])31proof32  induction k33  | zero =>34    have shape := add.right_unit at m with assumption35    rw shape36    have realM := RealSequence.value with sequence37    exact RealLe.reflexive with realM38  | succ(j) using ih =>39    have sumNatural := add.closed at j, m with h_j40    have sumInNaturals := nat.omega.forward with sumNatural41    have next := stepwise with m + j, sumInNaturals42    have combined := RealLe.transitive at u[m], u[m + j], u[succ(m + j)] with43      ih, next44    have shape := add.succ_right at j, m45    rw shape46    exact combined4748theorem StepwiseNondecreasing.nondecreasing (u : Set)49  requires sequence : RealSequence(u)50  requires stepwise : StepwiseNondecreasing(u)51  shows Nondecreasing(u)52proof53  intros m mNatural n nNatural order54  obtain ⟨k, kNatural, shape⟩ := order55  have offset := StepwiseNondecreasing.offset at u, m, k with sequence, stepwise56  rw shape at offset57  exact offset5859theorem StepwiseNonincreasing.offset (u : Set, m k : Nat)60  requires sequence : RealSequence(u)61  requires stepwise : StepwiseNonincreasing(u)62  shows RealLe(u[m + k], u[m])63proof64  induction k65  | zero =>66    have shape := add.right_unit at m with assumption67    rw shape68    have realM := RealSequence.value with sequence69    exact RealLe.reflexive with realM70  | succ(j) using ih =>71    have sumNatural := add.closed at j, m with h_j72    have sumInNaturals := nat.omega.forward with sumNatural73    have next := stepwise with m + j, sumInNaturals74    have combined := RealLe.transitive at u[succ(m + j)], u[m + j], u[m] with75      next, ih76    have shape := add.succ_right at j, m77    rw shape78    exact combined7980theorem StepwiseNonincreasing.nonincreasing (u : Set)81  requires sequence : RealSequence(u)82  requires stepwise : StepwiseNonincreasing(u)83  shows Nonincreasing(u)84proof85  intros m mNatural n nNatural order86  obtain ⟨k, kNatural, shape⟩ := order87  have offset := StepwiseNonincreasing.offset at u, m, k with sequence, stepwise88  rw shape at offset89  exact offset9091-- The range of a real sequence is exactly the family to which completeness92-- should be applied.  These small bridges keep the main proof mathematical.93theorem RealSequence.range_nonempty (u : Set)94  requires sequence : RealSequence(u)95  shows Nonempty(range(u))96proof97  have zeroNatural := nat.omega.forward with Naturals.constructor.zero98  have mapped := FunctionBetween.relates_apply at u, ℕ, ℝ, 0 with99    sequence, zeroNatural100  witness u₀101  unfold relates at mapped102  exact range.contains with mapped103104theorem RealSequence.range_subset_reals (u : Set)105  requires sequence : RealSequence(u)106  shows range(u) ⊆ ℝ107proof108  intros A member109  obtain ⟨_, n, pairInU⟩ := range.membership.forward with member110  rcases sequence with ⟨relation, functional, total⟩111  unfold RelationBetween at relation112  have boundedPair := relation with (n, A), pairInU113  obtain ⟨_, i, iNatural, B, bReal, shape⟩ := product.membership.forward with boundedPair114  obtain ⟨_, equalA⟩ := orderedPair.injective with shape115  rwa equalA116117theorem BoundedAboveBy.range_upper_bound (u : Set) (B : Real)118  requires sequence : RealSequence(u)119  requires bounded : BoundedAboveBy(u, B)120  shows RealUpperBound(range(u), B)121proof122  have typedB : Real(B) by typecheck123  constructor124  . exact typedB125  constructor126  . exact RealSequence.range_subset_reals with sequence127  . intros A member128    unfold RealSequence at sequence129    obtain ⟨_, n, pairInU⟩ := range.membership.forward with member130    obtain ⟨relation, functional, total⟩ := sequence131    unfold RelationBetween at relation132    have boundedPair := relation with (n, A), pairInU133    obtain ⟨_, i, iNatural, C, cReal, shape⟩ := product.membership.forward with boundedPair134    obtain ⟨equalN, equalA⟩ := orderedPair.injective with shape135    have nNatural : n ∈ ℕ by rwa equalN136    have mapped : relates(u, n, A) by exact pairInU137    have value := FunctionBetween.apply_value with sequence, mapped138    obtain ⟨_, _, subset⟩ := bounded with n, nNatural139    rwa ← value140141-- A least upper bound is approached from below.  If no member lay above142-- U - E, then U - E itself would be a smaller upper bound.143theorem RealLeastUpperBound.approached (S : Set) (U E : Real)144  requires least : RealLeastUpperBound(S, U)145  requires positiveE : 0 < E146  shows ∃ A ∈ S, U - E < A147proof148  have realE : Real(E) by typecheck149  have upperU : RealUpperBound(S, U) by simp [RealLeastUpperBound]150  have leastU : ∀ B, RealUpperBound(S, B) → U ⊆ B by simp [RealLeastUpperBound]151  rcases upperU with ⟨realU, reals, bounds⟩152  have differenceReal := realSubValue.real with realU, realE153  have positiveView := realLess.characterization.forward with positiveE154  have reversedView := RealLess.neg_reverse with positiveView155  have negative : -E < -realZero by exact realLess.characterization.backward at -E, -realZero with reversedView156  rw realNegValue.zero at negative157  have differenceBelow := realLess.add_left at -E, realZero, U with158    realNegValue.real at E with realE, realZero.real, realU, negative159  have zeroRight := realAddValue.zero_right with realU160  rw zeroRight at differenceBelow161  have differenceBelowSub : U - E < U162    unfold realSubValue163    exact differenceBelow164  by_contra noApproach165  have candidateUpper : RealUpperBound(S, U - E)166    constructor167    . exact differenceReal168    constructor169    . exact reals170    . intros A member171      have aInReals := reals with A, member172      have realA : Real(A) by exact aInReals173      have cutA := Real.characterization.forward with realA174      have cutDifference := Real.characterization.forward with differenceReal175      have comparison := DedekindCut.comparable with cutA, cutDifference176      cases comparison with aBelow | differenceBelowA177      . exact aBelow178      . by_contra notBelow179        have unequal : U - E ≠ A180          intro equal181          apply notBelow182          rw equal183          exact Subset.reflexive184        have proper : U - E ⊂ A185          constructor186          . exact differenceBelowA187          . exact unequal188        have tooClose : U - E < A189          apply realLess.characterization.backward190          unfold RealLess191          refine ⟨differenceReal, realA, proper⟩192        apply noApproach193        witness A194        refine ⟨member, tooClose⟩195  have upperBelow := leastU with U - E, candidateUpper196  obtain ⟨_, _, properBelow⟩ := realLess.characterization.forward with differenceBelowSub197  have belowSubset := ProperSubset.subset with properBelow198  have equal := Subset.antisymmetric with belowSubset, upperBelow199  exact ProperSubset.ne with properBelow, equal200201-- The bounded monotone convergence theorem, with the limit displayed as the202-- supremum of the range.203theorem Nondecreasing.converges_to_supremum (u : Set) (B : Real)204  requires sequence : RealSequence(u)205  requires increasing : Nondecreasing(u)206  requires bounded : BoundedAboveBy(u, B)207  shows ConvergesTo(u, realSup(range(u)))208proof209  have inhabited := RealSequence.range_nonempty with sequence210  have rangeUpper := BoundedAboveBy.range_upper_bound with sequence, bounded211  have least := realSup.least_upper_bound with inhabited, rangeUpper212  have supUpper : RealUpperBound(range(u), realSup(range(u))) by simp [RealLeastUpperBound]213  rcases supUpper with ⟨supReal, rangeReals, supBounds⟩214  have typedSup : Real(realSup(range(u))) by exact supReal215  constructor216  . exact sequence217  . intros E eInReals positiveE218    have typedE : Real(E) by exact eInReals219    obtain ⟨A, aInRange, closeA⟩ := RealLeastUpperBound.approached with least, positiveE220    unfold RealSequence at sequence221    obtain ⟨_, N, pairInU⟩ := range.membership.forward with aInRange222    obtain ⟨relation, functional, total⟩ := sequence223    unfold RelationBetween at relation224    have boundedPair := relation with (N, A), pairInU225    obtain ⟨_, i, iNatural, C, cReal, shape⟩ := product.membership.forward with boundedPair226    obtain ⟨equalN, equalA⟩ := orderedPair.injective with shape227    have nNatural : N ∈ ℕ by rwa equalN228    have mapped : relates(u, N, A) by exact pairInU229    have valueAtN := FunctionBetween.apply_value with sequence, mapped230    rw ← valueAtN at closeA231    have supBelowPlus := realLess.add_left with realZero.real, typedE, typedSup, positiveE232    have supZero := realAddValue.zero_right with typedSup233    rw supZero at supBelowPlus234    witness N235    constructor236    . exact nNatural237    . intros n littleNInNaturals nAfterN238      have valueNReal := FunctionBetween.apply_closed with sequence, littleNInNaturals239      have valueAtNReal := FunctionBetween.apply_closed with sequence, nNatural240      have monotoneView := increasing with241        N, nNatural, n, littleNInNaturals, nAfterN242      have monotoneLe := realLe.characterization.backward with monotoneView243      have lower := realLess.transitive_le with closeA, monotoneLe244      have mappedN := FunctionBetween.relates_apply with sequence, littleNInNaturals245      unfold relates at mappedN246      have valueInRange := range.contains with mappedN247      have valueSubsetSup := supBounds with uₙ, valueInRange248      have valueLeSup := realLe.of_subset with valueSubsetSup249      have upper := realLe.transitive_less with valueLeSup, supBelowPlus250      have interval : (realSup(range(u)) - E < uₙ ∧ uₙ < realSup(range(u)) + E)251        constructor252        . exact lower253        . exact upper254      exact openBall.order_characterization.backward with interval255256theorem Nonincreasing.neg_nondecreasing (u : Set)257  requires sequence : RealSequence(u)258  requires decreasing : Nonincreasing(u)259  shows Nondecreasing(negSequence(u))260proof261  intros m mNatural n nNatural order262  have descendsView := decreasing with m, mNatural, n, nNatural, order263  have descends := realLe.characterization.backward with descendsView264  have reversed := realLe.neg_reverse with descends265  have reversedView := realLe.characterization.forward with reversed266  have realM := RealSequence.value at u, m with sequence267  have realN := RealSequence.value at u, n with sequence268  have valueM := negSequence.value with sequence, realM269  have valueN := negSequence.value with sequence, realN270  rwa [valueM, valueN]271272theorem BoundedBelowBy.neg_bounded_above (u : Set) (A : Real)273  requires sequence : RealSequence(u)274  requires bounded : BoundedBelowBy(u, A)275  shows BoundedAboveBy(negSequence(u), -A)276proof277  intros n nNatural278  have typedN : Nat(n) by exact nat.omega.backward at n with nNatural279  have lowerView := bounded with n, nNatural280  have lower := realLe.characterization.backward with lowerView281  have reversed := realLe.neg_reverse with lower282  have reversedView := realLe.characterization.forward with reversed283  have realN := RealSequence.value with sequence284  have value := negSequence.value with sequence, realN285  rwa value286287-- The canonical infimum of a real sequence, displayed as the negative of288-- the supremum of its negated range.289def realSequenceInfimum (u : Set) : Set :=290  realNeg(realSup(range(negSequence(u))))291292theorem realSequenceInfimum.real (u : Set) (A : Real)293  requires sequence : RealSequence(u)294  requires bounded : BoundedBelowBy(u, A)295  shows Real(realSequenceInfimum(u))296proof297  have negative := negSequence.sequence with sequence298  have negBounded := BoundedBelowBy.neg_bounded_above with sequence, bounded299  have inhabited := RealSequence.range_nonempty with negative300  have rangeUpper := BoundedAboveBy.range_upper_bound with negative, negBounded301  have least := realSup.least_upper_bound with inhabited, rangeUpper302  have supUpper : RealUpperBound(303      range(negSequence(u)), realSup(range(negSequence(u))))304    simp [RealLeastUpperBound]305  rcases supUpper with ⟨supReal, rangeReals, bounds⟩306  have negativeReal := realNegValue.real with supReal307  unfold realSequenceInfimum308  exact negativeReal309310-- The decreasing half of monotone convergence is the increasing theorem311-- applied to the negated sequence.312theorem Nonincreasing.converges_to_infimum (u : Set) (A : Real)313  requires sequence : RealSequence(u)314  requires decreasing : Nonincreasing(u)315  requires bounded : BoundedBelowBy(u, A)316  shows ConvergesTo(u, realSequenceInfimum(u))317proof318  unfold realSequenceInfimum319  have negSequenceReal := negSequence.sequence with sequence320  have negIncreasing := Nonincreasing.neg_nondecreasing with sequence, decreasing321  have negBounded := BoundedBelowBy.neg_bounded_above with sequence, bounded322  have negConverges := Nondecreasing.converges_to_supremum with negSequenceReal, negIncreasing, negBounded323  have inhabited := RealSequence.range_nonempty with negSequenceReal324  have rangeUpper := BoundedAboveBy.range_upper_bound with negSequenceReal, negBounded325  have least := realSup.least_upper_bound with inhabited, rangeUpper326  have supUpper : RealUpperBound(327      range(negSequence(u)), realSup(range(negSequence(u))))328    simp [RealLeastUpperBound]329  rcases supUpper with ⟨supReal, rangeReals, bounds⟩330  have typedSup : Real(realSup(range(negSequence(u)))) by exact supReal331  have limitReal := realNegValue.real with typedSup332  constructor333  . exact sequence334  . intros E eInReals positiveE335    have typedE : Real(E) by exact eInReals336    obtain ⟨N, nNatural, close⟩ := ConvergesTo.eventually with negConverges, positiveE337    witness N338    constructor339    . exact nNatural340    . intros n littleNatural afterN341      have typedN : Nat(n) by exact nat.omega.backward at n with littleNatural342      have realValue := RealSequence.value with sequence343      have realNegValue := RealSequence.value with negSequenceReal344      have near := close with n, littleNatural, afterN345      obtain ⟨negValueReal, within⟩ := openBall.membership.forward with near346      have valueShape := negSequence.value with sequence, realValue347      rw valueShape at within348      have distanceNeg := dist.neg with realValue, limitReal349      have involutive := realNegValue.involutive with typedSup350      rw involutive at distanceNeg351      apply openBall.membership.backward352      constructor353        exact realValue354      . rw ← distanceNeg355        exact within356357theorem Nonincreasing.infimum_le_term (u : Set) (A : Real, n : Nat)358  requires sequence : RealSequence(u)359  requires bounded : BoundedBelowBy(u, A)360  shows (realSequenceInfimum(u) : R) ≤ (u[n] : R)361proof362  have negative := negSequence.sequence with sequence363  have negBounded := BoundedBelowBy.neg_bounded_above with sequence, bounded364  have inhabited := RealSequence.range_nonempty with negative365  have rangeUpper := BoundedAboveBy.range_upper_bound with negative, negBounded366  have least := realSup.least_upper_bound with inhabited, rangeUpper367  have supUpper : RealUpperBound(368      range(negSequence(u)), realSup(range(negSequence(u))))369    simp [RealLeastUpperBound]370  rcases supUpper with ⟨supReal, rangeReals, bounds⟩371  have naturalN : n ∈ ℕ by simp [Nat]372  have negativeFunction := negative373  unfold RealSequence at negativeFunction374  have mapped := FunctionBetween.relates_apply with negativeFunction, naturalN375  unfold relates at mapped376  have inRange := range.contains with mapped377  have view := bounds with negSequence(u)[n], inRange378  have realN := RealSequence.value with sequence379  have negValue := negSequence.value with sequence, realN380  rw negValue at view381  have negReal := realNegValue.real with realN382  have upper := realLe.of_subset with negReal, supReal, view383  have reversed := realLe.neg_reverse with upper384  have involutive := realNegValue.involutive with realN385  rw involutive at reversed386  unfold realSequenceInfimum387  exact reversed388389-- The usual existential form follows from the displayed infimum.390theorem Nonincreasing.has_limit (u : Set) (A : Real)391  requires sequence : RealSequence(u)392  requires decreasing : Nonincreasing(u)393  requires bounded : BoundedBelowBy(u, A)394  shows ∃ L ∈ ℝ, ConvergesTo(u, L)395proof396  have converges := Nonincreasing.converges_to_infimum with sequence, decreasing, bounded397  unfold realSequenceInfimum at converges398  have negSequenceReal := negSequence.sequence with sequence399  have inhabited := RealSequence.range_nonempty with negSequenceReal400  have negBounded := BoundedBelowBy.neg_bounded_above with sequence, bounded401  have rangeUpper := BoundedAboveBy.range_upper_bound with negSequenceReal, negBounded402  have least := realSup.least_upper_bound with inhabited, rangeUpper403  have supUpper : RealUpperBound(404      range(negSequence(u)), realSup(range(negSequence(u))))405    simp [RealLeastUpperBound]406  rcases supUpper with ⟨supReal, rangeReals, bounds⟩407  have limitReal := realNegValue.real with supReal408  witness -realSup(range(negSequence(u)))409  constructor410    exact limitReal411  . exact converges412413-- Section: SequentialCompactness414predicate NestedClosedIntervals (a b : Set) :=415  RealSequence(a) ∧ RealSequence(b) ∧416  Nondecreasing(a) ∧ Nonincreasing(b) ∧ PointwiseLE(a, b)417418theorem NestedClosedIntervals.lower_sequence (a b : Set)419  requires nested : NestedClosedIntervals(a, b)420  shows RealSequence(a)421proof422  simp [NestedClosedIntervals]423424theorem NestedClosedIntervals.upper_sequence (a b : Set)425  requires nested : NestedClosedIntervals(a, b)426  shows RealSequence(b)427proof428  simp [NestedClosedIntervals]429430theorem NestedClosedIntervals.intervals_nested (a b : Set) (m n : Nat)431  requires nested : NestedClosedIntervals(a, b)432  requires order : m ≤ n433  shows closedInterval(a[n], b[n]) ⊆ closedInterval(a[m], b[m])434proof435  rcases nested with436    ⟨sequenceA, sequenceB, increasing, decreasing, ordered⟩437  have lowerView := increasing with m, n, order438  have upperView := decreasing with m, n, order439  have lower := realLe.characterization.backward with lowerView440  have upper := realLe.characterization.backward with upperView441  have realAN := RealSequence.value at a, n with sequenceA442  have realBN := RealSequence.value at b, n with sequenceB443  have realAM := RealSequence.value at a, m with sequenceA444  have realBM := RealSequence.value at b, m with sequenceB445  exact closedInterval.nested with realAN, realBN, realAM, realBM, lower, upper446447-- Every left endpoint lies below every later or earlier right endpoint.448-- This is the order-theoretic heart of the nested interval theorem.449theorem NestedClosedIntervals.lower_bounded_by_upper (a b : Set) (n : Nat)450  requires nested : NestedClosedIntervals(a, b)451  shows BoundedAboveBy(a, b[n])452proof453  rcases nested with454    ⟨sequenceA, sequenceB, increasing, decreasing, ordered⟩455  intros m mNatural456  have nNatural : n ∈ ℕ by simp [Nat]457  have typedM : Nat(m) by exact nat.omega.backward at m with mNatural458  have comparison := Less.trichotomy at m, n with typedM, assumption459  cases comparison with mBefore | rest460  . have mLeN := Less.implies_LessEqual at m, n with mBefore461    have leftOrder := increasing with m, mNatural, n, mLeN462    have intervalOrder := ordered with n, nNatural463    exact RealLe.transitive with leftOrder, intervalOrder464  . cases rest with equal | nBefore465    . rw equal466      exact ordered with n, nNatural467    . have nLeM := Less.implies_LessEqual at n, m with nBefore468      have intervalOrder := ordered with m, mNatural469      have rightOrder := decreasing with n, m, mNatural, nLeM470      exact RealLe.transitive with intervalOrder, rightOrder471472theorem NestedClosedIntervals.lower_bounded (a b : Set)473  requires nested : NestedClosedIntervals(a, b)474  shows BoundedAboveBy(a, b[0])475proof476  exact NestedClosedIntervals.lower_bounded_by_upper with nested477478theorem NestedClosedIntervals.supremum_real (a b : Set)479  requires nested : NestedClosedIntervals(a, b)480  shows Real(realSup(range(a)))481proof482  have sequenceA := NestedClosedIntervals.lower_sequence with nested483  have sequenceB := NestedClosedIntervals.upper_sequence with nested484  have inhabited := RealSequence.range_nonempty with sequenceA485  have bounded := NestedClosedIntervals.lower_bounded with nested486  have realB0 := RealSequence.value at b, 0 with sequenceB487  have upper := BoundedAboveBy.range_upper_bound with sequenceA, bounded488  have least := realSup.least_upper_bound with inhabited, upper489  have supremumUpper : RealUpperBound(range(a), realSup(range(a))) by simp [RealLeastUpperBound]490  rcases supremumUpper with ⟨realSupremum, reals, bounds⟩491  exact realSupremum492493-- The left endpoints approach the canonical point in the intersection.494theorem NestedClosedIntervals.lower_converges (a b : Set)495  requires nested : NestedClosedIntervals(a, b)496  shows ConvergesTo(a, realSup(range(a)))497proof498  have system := nested499  rcases nested with500    ⟨sequenceA, sequenceB, increasing, decreasing, ordered⟩501  have bounded := NestedClosedIntervals.lower_bounded with system502  exact Nondecreasing.converges_to_supremum with sequenceA, increasing, bounded503504theorem NestedClosedIntervals.lower_le_supremum (a b : Set) (n : Nat)505  requires nested : NestedClosedIntervals(a, b)506  shows RealLe(a[n], realSup(range(a)))507proof508  have sequenceA := NestedClosedIntervals.lower_sequence with nested509  have sequenceB := NestedClosedIntervals.upper_sequence with nested510  have inhabited := RealSequence.range_nonempty with sequenceA511  have bounded := NestedClosedIntervals.lower_bounded with nested512  have realB0 := RealSequence.value with sequenceB513  have upper := BoundedAboveBy.range_upper_bound with sequenceA, bounded514  have least := realSup.least_upper_bound with inhabited, upper515  have supremumUpper : RealUpperBound(range(a), realSup(range(a))) by simp [RealLeastUpperBound]516  rcases supremumUpper with ⟨realSupremum, reals, bounds⟩517  have nNatural : n ∈ ℕ by simp [Nat]518  have functionA := sequenceA519  unfold RealSequence at functionA520  have mapped := FunctionBetween.relates_apply with functionA, nNatural521  unfold relates at mapped522  have member := range.contains with mapped523  have subset := bounds with a[n], member524  have realAN := RealSequence.value with sequenceA525  constructor526  . exact realAN527  . constructor528    . exact realSupremum529    . exact subset530531theorem NestedClosedIntervals.supremum_le_upper (a b : Set) (n : Nat)532  requires nested : NestedClosedIntervals(a, b)533  shows RealLe(realSup(range(a)), b[n])534proof535  have sequenceA := NestedClosedIntervals.lower_sequence with nested536  have sequenceB := NestedClosedIntervals.upper_sequence with nested537  have boundedN := NestedClosedIntervals.lower_bounded_by_upper with nested538  have realBN := RealSequence.value with sequenceB539  have upperN := BoundedAboveBy.range_upper_bound with sequenceA, boundedN540  have subset := realSup.subset_upper with upperN541  have realSupremum := NestedClosedIntervals.supremum_real with nested542  constructor543  . exact realSupremum544  . constructor545    . exact realBN546    . exact subset547548-- Cantor's nested interval theorem, with the common point displayed549-- canonically as the supremum of the left endpoints.550theorem NestedClosedIntervals.contains_supremum (a b : Set) (n : Nat)551  requires nested : NestedClosedIntervals(a, b)552  shows realSup(range(a)) ∈ closedInterval(a[n], b[n])553proof554  have realSupremum := NestedClosedIntervals.supremum_real with nested555  have lowerView := NestedClosedIntervals.lower_le_supremum with nested556  have upperView := NestedClosedIntervals.supremum_le_upper with nested557  have lower := realLe.characterization.backward with lowerView558  have upper := realLe.characterization.backward with upperView559  have realMember : realSup(range(a)) ∈ ℝ by exact realSupremum560  have data : realSup(range(a)) ∈ ℝ ∧ a[n] ≤ realSup(range(a)) ∧ realSup(range(a)) ≤ b[n]561    constructor562    . exact realMember563    . constructor564      . exact lower565      . exact upper566  have sequenceA := NestedClosedIntervals.lower_sequence with nested567  have sequenceB := NestedClosedIntervals.upper_sequence with nested568  have realAN := RealSequence.value with sequenceA569  have realBN := RealSequence.value with sequenceB570  exact closedInterval.membership.backward with data571572theorem NestedClosedIntervals.nonempty_intersection (a b : Set)573  requires nested : NestedClosedIntervals(a, b)574  shows ∃ L ∈ ℝ, ∀ n ∈ ℕ, L ∈ closedInterval(a[n], b[n])575proof576  witness realSup(range(a))577  constructor578  . exact NestedClosedIntervals.supremum_real with nested579  . intros n nNatural580    exact NestedClosedIntervals.contains_supremum with nested581582-- SequentialCompactness583predicate StrictlyIncreasingNat (k : Set) :=584  FunctionBetween(k, ℕ, ℕ) ∧585  (∀ m ∈ ℕ, ∀ n ∈ ℕ, m < n → Less(kₘ, kₙ))586587def subsequence (u k : Set) : Set :=588  compose(u, k, ℕ, ℕ, ℝ)589590predicate TermsIn (u S : Set) :=591  ∀ n ∈ ℕ, uₙ ∈ S592593predicate SequentiallyCompact (S : Set) :=594  S ⊆ ℝ ∧595  (∀ u, RealSequence(u) → TermsIn(u, S) →596    ∃ k, StrictlyIncreasingNat(k) ∧597      ∃ L ∈ ℝ, L ∈ S ∧ ConvergesTo(subsequence(u, k), L))598599theorem StrictlyIncreasingNat.function (k : Set)600  requires increasing : StrictlyIncreasingNat(k)601  shows k : ℕ → ℕ602proof603  simp [StrictlyIncreasingNat]604605theorem identity.strictly_increasing_nat606  shows StrictlyIncreasingNat(identity(ℕ))607proof608  constructor609  . exact identity.function at ℕ610  . intros m mNatural n nNatural less611    have valueM := identity.apply with mNatural612    have valueN := identity.apply with nNatural613    rwa [valueM, valueN]614615-- A strictly increasing selector has passed its own index by stage n.616theorem StrictlyIncreasingNat.index_le_value (k : Set, n : Nat)617  requires increasing : StrictlyIncreasingNat(k)618  shows n ≤ kₙ619proof620  induction n621  | zero =>622    have function := StrictlyIncreasingNat.function with increasing623    have zeroNatural : 0 ∈ ℕ by exact nat.omega.forward at 0 with Naturals.constructor.zero624    have valueNatural := FunctionBetween.apply_closed with function, zeroNatural625    have typedValue : Nat(k₀) by exact nat.omega.backward at k₀ with valueNatural626    exact Grace.Core.Nat.Order.LessEqual.zero at k₀ with typedValue627  | succ(j) using ih =>628    have function := StrictlyIncreasingNat.function with increasing629    obtain ⟨functionAgain, strict⟩ := increasing630    have jNatural : j ∈ ℕ by simp [Nat]631    have nextNatural : succ(j) ∈ ℕ632      have typedNext := Naturals.constructor.succ at j633      exact nat.omega.forward with typedNext634    have jBeforeNext : j < succ(j)635      unfold Less636      exact LessEqual.reflexive with assumption637    have valuesStrict := strict with638      j, jNatural, succ(j), nextNatural, jBeforeNext639    have typedJValue : Nat(kⱼ)640      have valueNatural := FunctionBetween.apply_closed with function, jNatural641      exact nat.omega.backward with valueNatural642    have typedNextValue : Nat(k[succ(j)])643      have valueNatural := FunctionBetween.apply_closed with function, nextNatural644      exact nat.omega.backward with valueNatural645    have jBeforeValue := LessEqual.transitive_Less at646      j, kⱼ, k[succ(j)] with647        assumption, typedJValue, typedNextValue, ih, valuesStrict648    exact jBeforeValue649650theorem subsequence.function (u k : Set)651  requires sequence : RealSequence(u)652  requires increasing : StrictlyIncreasingNat(k)653  shows subsequence(u, k) : ℕ → ℝ654proof655  unfold RealSequence at sequence656  have selector := StrictlyIncreasingNat.function with increasing657  unfold subsequence658  exact compose.function with selector, sequence659660theorem subsequence.sequence (u k : Set)661  requires sequence : RealSequence(u)662  requires increasing : StrictlyIncreasingNat(k)663  shows RealSequence(subsequence(u, k))664proof665  unfold RealSequence666  exact subsequence.function with sequence, increasing667668theorem subsequence.value (u k : Set, n : Nat)669  requires sequence : RealSequence(u)670  requires increasing : StrictlyIncreasingNat(k)671  shows subsequence(u, k)(n) = u(kₙ)672proof673  have selector := StrictlyIncreasingNat.function with increasing674  have nNatural : n ∈ ℕ by simp [Nat]675  unfold RealSequence at sequence676  have value := compose.apply with selector, sequence, nNatural677  simp [subsequence]678679theorem subsequence.identity (u : Set)680  requires sequence : RealSequence(u)681  shows subsequence(u, identity(ℕ)) = u682proof683  unfold RealSequence at sequence684  unfold subsequence685  exact compose.identity_right with sequence686687theorem TermsIn.subsequence (u k S : Set)688  requires sequence : RealSequence(u)689  requires terms : TermsIn(u, S)690  requires increasing : StrictlyIncreasingNat(k)691  shows TermsIn(subsequence(u, k), S)692proof693  intros n nNatural694  have typedN : Nat(n) by exact nat.omega.backward at n with nNatural695  have selector := StrictlyIncreasingNat.function with increasing696  have selectedNatural := FunctionBetween.apply_closed with selector, nNatural697  have member := terms with kₙ, selectedNatural698  have value := subsequence.value with sequence, increasing699  rwa value700701-- Every subsequence of a convergent sequence has the same limit.702theorem ConvergesTo.subsequence (u k : Set) (L : Real)703  requires converges : ConvergesTo(u, L)704  requires increasing : StrictlyIncreasingNat(k)705  shows ConvergesTo(subsequence(u, k), L)706proof707  have sequence := ConvergesTo.sequence with converges708  constructor709  . exact subsequence.sequence with sequence, increasing710  . intros E realE positive711    obtain ⟨N, nNatural, close⟩ := ConvergesTo.eventually with converges, positive712    witness N713    constructor714    . exact nNatural715    . intros n littleNatural nAfterN716      have nBeforeValue := StrictlyIncreasingNat.index_le_value at717        k, n with increasing718      have valueNatural := FunctionBetween.apply_closed at719        k, ℕ, ℕ, n with720          StrictlyIncreasingNat.function at k with increasing,721          littleNatural722      have indexAfterN := LessEqual.transitive with nAfterN, nBeforeValue723      have near := close with kₙ, valueNatural, indexAfterN724      have value := subsequence.value at u, k, n with sequence, increasing725      rwa value726727theorem ConvergesTo.has_convergent_subsequence (u : Set) (L : Real)728  requires converges : ConvergesTo(u, L)729  shows ∃ k, StrictlyIncreasingNat(k) ∧730    ConvergesTo(subsequence(u, k), L)731proof732  witness identity(ℕ)733  constructor734  . exact identity.strictly_increasing_nat735  . exact ConvergesTo.subsequence at u, identity(ℕ), L with736      converges, identity.strictly_increasing_nat737738-- Closed intervals contain limits of sequences whose terms stay inside them.739theorem closedInterval.contains_limit (u : Set) (L A B : Real)740  requires converges : ConvergesTo(u, L)741  requires terms : TermsIn(u, closedInterval(A, B))742  shows L ∈ closedInterval(A, B)743proof744  have sequence := ConvergesTo.sequence with converges745  have lowerBound : BoundedBelowBy(u, A)746    intros n nNatural747    have member := terms with n, nNatural748    obtain ⟨realValue, lower, upper⟩ := closedInterval.membership.forward with member749    exact realLe.characterization.forward with lower750  have upperBound : BoundedAboveBy(u, B)751    intros n nNatural752    have member := terms with n, nNatural753    obtain ⟨realValue, lower, upper⟩ := closedInterval.membership.forward with member754    exact realLe.characterization.forward with upper755  have lower := ConvergesTo.ge_constant with converges, lowerBound756  have upper := ConvergesTo.le_constant with converges, upperBound757  have realL : L ∈ ℝ by simp [Real]758  have data : L ∈ ℝ ∧ A ≤ L ∧ L ≤ B759    constructor760    . exact realL761    . constructor762      . exact lower763      . exact upper764  exact closedInterval.membership.backward with data765766theorem closedInterval.contains_subsequence_limit (u k : Set) (L A B : Real)767  requires sequence : RealSequence(u)768  requires terms : TermsIn(u, closedInterval(A, B))769  requires increasing : StrictlyIncreasingNat(k)770  requires converges : ConvergesTo(subsequence(u, k), L)771  shows L ∈ closedInterval(A, B)772proof773  have selectedTerms := TermsIn.subsequence with sequence, terms, increasing774  exact closedInterval.contains_limit with converges, selectedTerms775776-- Section: CompactContinuity777predicate SequencePeak (u : Set, n : Nat) :=778  ∀ m ∈ ℕ, n < m → RealLe(u[m], u[n])779780predicate UnboundedSequencePeaks (u : Set) :=781  ∀ N ∈ ℕ, ∃ n ∈ ℕ, N ≤ n ∧ SequencePeak(u, n)782783predicate EventuallyNoSequencePeaks (u : Set, N : Nat) :=784  ∀ n ∈ ℕ, N ≤ n → ¬SequencePeak(u, n)785786-- At stage zero we choose either a peak, or a point beyond which no peaks787-- remain.  Subsequent stages choose a later peak in the first case and a788-- later, strictly larger value in the second.789def monotoneStartCandidates (u : Set) : Set :=790  { n ∈ ℕ |791    (UnboundedSequencePeaks(u) ∧ SequencePeak(u, n)) ∨792    (¬UnboundedSequencePeaks(u) ∧ EventuallyNoSequencePeaks(u, n)) }793794def monotoneNextCandidates (u k : Set) : Set :=795  { n ∈ ℕ | Less(k, n) ∧796    ((UnboundedSequencePeaks(u) ∧ SequencePeak(u, n)) ∨797     (¬UnboundedSequencePeaks(u) ∧ RealLess(u[k], u[n]))) }798799theorem monotoneStartCandidates.naturals (u : Set)800  shows monotoneStartCandidates(u) ⊆ ℕ801proof802  simp803804theorem monotoneNextCandidates.naturals (u k : Set)805  shows monotoneNextCandidates(u, k) ⊆ ℕ806proof807  simp808809def monotoneIndex (u : Set, n : Nat) → Set810  | u, 0 => leastNatural(monotoneStartCandidates(u))811  | u, succ(n) => leastNatural(monotoneNextCandidates(u, monotoneIndex(u, n)))812813def monotoneSelector (u : Set) : Set :=814  { p ∈ ℕ × ℕ | ∃ n ∈ ℕ, p = (n, monotoneIndex(u, n)) }815816theorem not_unbounded_sequence_peaks.eventually_none (u : Set)817  requires bounded : ¬UnboundedSequencePeaks(u)818  shows ∃ N ∈ ℕ, EventuallyNoSequencePeaks(u, N)819proof820  by_contra noThreshold821  apply bounded822  intros N nNatural823  by_contra noLaterPeak824  apply noThreshold825  witness N826  constructor827  . exact nNatural828    intros n littleNatural afterN peak829    apply noLaterPeak830    witness n831    refine ⟨littleNatural, afterN, peak⟩832833theorem UnboundedSequencePeaks.or_not (u : Set)834  shows UnboundedSequencePeaks(u) ∨ ¬UnboundedSequencePeaks(u)835proof836  tauto837838theorem monotoneStartCandidates.nonempty (u : Set)839  shows Nonempty(monotoneStartCandidates(u))840proof841  have alternatives : UnboundedSequencePeaks(u) ∨ ¬UnboundedSequencePeaks(u) by tauto842  cases alternatives with unbounded | bounded843  . have unboundedPeaks := unbounded844    have zeroNatural : 0 ∈ ℕ by exact nat.omega.forward at 0 with Naturals.constructor.zero845    obtain ⟨n, nNatural, afterZero, peak⟩ :=846      unbounded with 0, zeroNatural847    witness n848    apply monotoneStartCandidates.membership.backward849    refine ⟨nNatural, _⟩850    left851    refine ⟨unboundedPeaks, peak⟩852  . obtain ⟨N, nNatural, noPeaks⟩ :=853      not_unbounded_sequence_peaks.eventually_none at u with bounded854    witness N855    apply monotoneStartCandidates.membership.backward856    refine ⟨nNatural, _⟩857    right858    refine ⟨bounded, noPeaks⟩859860theorem EventuallyNoSequencePeaks.tail (u : Set, k m : Nat)861  requires none : EventuallyNoSequencePeaks(u, k)862  requires later : k ≤ m863  shows EventuallyNoSequencePeaks(u, m)864proof865  intros n nNatural afterM866  have afterK := LessEqual.transitive with later, afterM867  exact none with n, nNatural, afterK868869theorem monotoneNextCandidates.nonempty (u : Set, k : Nat)870  requires sequence : RealSequence(u)871  requires position :872    (UnboundedSequencePeaks(u) ∧ SequencePeak(u, k)) ∨873    (¬UnboundedSequencePeaks(u) ∧ EventuallyNoSequencePeaks(u, k))874  shows Nonempty(monotoneNextCandidates(u, k))875proof876  cases position with peakCase | risingCase877  . rcases peakCase with ⟨unbounded, peak⟩878    have unboundedPeaks := unbounded879    have nextNatural := Naturals.constructor.succ at k880    have nextInNaturals := nat.omega.forward with nextNatural881    obtain ⟨n, nNatural, afterNext, laterPeak⟩ :=882      unbounded with succ(k), nextInNaturals883    have later : k < n by exact afterNext884    witness n885    apply monotoneNextCandidates.membership.backward886    refine ⟨nNatural, later, _⟩887    left888    refine ⟨unboundedPeaks, laterPeak⟩889  . rcases risingCase with ⟨bounded, noPeaks⟩890    have reflexive := LessEqual.reflexive at k891    have notPeak := noPeaks with k, reflexive892    have laterViolation : ∃ n ∈ ℕ, k < n ∧ ¬RealLe(u[n], u[k])893      by_contra noViolation894      apply notPeak895      intros m mNatural later896      by_contra notLe897      apply noViolation898      witness m899      refine ⟨mNatural, later, notLe⟩900    obtain ⟨next, nextNatural, later, notLe⟩ := laterViolation901    have realK := RealSequence.value with sequence902    have realNext := RealSequence.value with sequence903    have notOrdered : ¬(u[next] ≤ u[k])904      intro ordered905      apply notLe906      exact realLe.characterization.forward with ordered907    have rises := realLess.of_not_le with notOrdered908    have risesView := realLess.characterization.forward with rises909    witness next910    apply monotoneNextCandidates.membership.backward911    refine ⟨nextNatural, later, _⟩912    right913    refine ⟨bounded, risesView⟩914915-- Every recursively chosen index is natural and remains in the branch chosen916-- at stage zero.  In the no-peaks branch it also remains beyond the threshold.917theorem monotoneIndex.position (u : Set, n : Nat)918  requires sequence : RealSequence(u)919  shows Nat(monotoneIndex(u, n)) ∧920    ((UnboundedSequencePeaks(u) ∧921        SequencePeak(u, monotoneIndex(u, n))) ∨922     (¬UnboundedSequencePeaks(u) ∧923        EventuallyNoSequencePeaks(u, monotoneIndex(u, n))))924proof925  induction n926  | zero =>927    have inhabited := monotoneStartCandidates.nonempty at u928    have chosen := leastNatural.member with inhabited, monotoneStartCandidates.naturals at u929    have data := monotoneStartCandidates.membership.forward with chosen930    rw monotoneIndex931    rcases data with ⟨natural, position⟩932    have typed : Nat(leastNatural(monotoneStartCandidates(u))) by exact nat.omega.backward with natural933    constructor934    . exact typed935    . exact position936  | succ(j) using ih =>937    rcases ih with ⟨oldNatural, oldPosition⟩938    have inhabited := monotoneNextCandidates.nonempty with sequence, oldPosition939    have naturals := monotoneNextCandidates.naturals at u, monotoneIndex(u, j)940    have chosen := leastNatural.member with inhabited, naturals941    obtain ⟨natural, later, branch⟩ := monotoneNextCandidates.membership.forward with chosen942    have typed : Nat(leastNatural(monotoneNextCandidates(u, monotoneIndex(u, j))))943      exact nat.omega.backward with natural944    rw monotoneIndex945    constructor946    . exact typed947    . cases branch with peakBranch | risingBranch948      . left949        exact peakBranch950      . rcases risingBranch with ⟨bounded, rises⟩951        right952        constructor953        . exact bounded954        . cases oldPosition with oldPeak | oldRising955          . rcases oldPeak with ⟨unbounded, oldPeak⟩956            contradiction957          . rcases oldRising with ⟨boundedAgain, oldTail⟩958            have weak := Less.implies_LessEqual with oldNatural, later959            exact EventuallyNoSequencePeaks.tail with oldTail, weak960961theorem monotoneIndex.natural (u : Set, n : Nat)962  requires sequence : RealSequence(u)963  shows Nat(monotoneIndex(u, n))964proof965  have data := monotoneIndex.position with sequence966  simp967968theorem monotoneIndex.step (u : Set, n : Nat)969  requires sequence : RealSequence(u)970  shows Less(monotoneIndex(u, n), monotoneIndex(u, succ(n)))971proof972  obtain ⟨oldNatural, position⟩ := monotoneIndex.position with sequence973  have inhabited := monotoneNextCandidates.nonempty with sequence, position974  have naturals := monotoneNextCandidates.naturals at u, monotoneIndex(u, n)975  have chosen := leastNatural.member with inhabited, naturals976  obtain ⟨natural, later, branch⟩ := monotoneNextCandidates.membership.forward with chosen977  rwa monotoneIndex978979theorem monotoneIndex.offset (u : Set, m k : Nat)980  requires sequence : RealSequence(u)981  shows LessEqual(monotoneIndex(u, m), monotoneIndex(u, m + k))982proof983  induction k984  | zero =>985    have shape := add.right_unit at m986    rw shape987    have indexNatural := monotoneIndex.natural with sequence988    exact LessEqual.reflexive with indexNatural989  | succ(j) using ih =>990    have step := monotoneIndex.step at u, m + j with sequence991    have weak := Less.implies_LessEqual with step992    have combined := LessEqual.transitive with ih, weak993    have shape := add.succ_right at j, m994    rwa shape995996theorem monotoneIndex.monotone (u : Set, m n : Nat)997  requires sequence : RealSequence(u)998  requires order : m ≤ n999  shows LessEqual(monotoneIndex(u, m), monotoneIndex(u, n))1000proof1001  obtain ⟨k, kNatural, shape⟩ := order1002  have offset := monotoneIndex.offset at u, m, k with sequence1003  rwa shape at offset10041005theorem monotoneIndex.strict (u : Set, m n : Nat)1006  requires sequence : RealSequence(u)1007  requires order : m < n1008  shows Less(monotoneIndex(u, m), monotoneIndex(u, n))1009proof1010  unfold Less at order1011  have tail := monotoneIndex.monotone with sequence, order1012  have first := monotoneIndex.step at u, m with sequence1013  exact Less.transitive_LessEqual with first, tail10141015theorem monotoneSelector.relates (u : Set, n : Nat)1016  requires sequence : RealSequence(u)1017  shows relates(monotoneSelector(u), n, monotoneIndex(u, n))1018proof1019  unfold relates1020  have nInNaturals := nat.omega.forward at n with assumption1021  have indexNatural := monotoneIndex.natural with sequence1022  have indexInNaturals := nat.omega.forward with indexNatural1023  apply monotoneSelector.membership.backward1024  constructor1025  . exact product.pair at n, monotoneIndex(u, n), ℕ, ℕ with1026      nInNaturals, indexInNaturals1027  . witness n1028    refine ⟨nInNaturals, rfl⟩10291030theorem monotoneSelector.function (u : Set)1031  requires sequence : RealSequence(u)1032  shows monotoneSelector(u) : ℕ → ℕ1033proof1034  constructor1035    intros p member1036    have data := monotoneSelector.membership.forward with member1037    simp1038  . constructor1039      intros n first mappedFirst second mappedSecond1040      unfold relates at mappedFirst1041      unfold relates at mappedSecond1042      have firstData := monotoneSelector.membership.forward with mappedFirst1043      have secondData := monotoneSelector.membership.forward with mappedSecond1044      rcases firstData with ⟨_, i, iNatural, firstShape⟩1045      rcases secondData with ⟨_, j, jNatural, secondShape⟩1046      have firstCoordinates := orderedPair.injective with firstShape1047      have secondCoordinates := orderedPair.injective with secondShape1048      rcases firstCoordinates with ⟨nEqualsI, firstValue⟩1049      rcases secondCoordinates with ⟨nEqualsJ, secondValue⟩1050      rw ← nEqualsI at firstValue1051      rw ← nEqualsJ at secondValue1052      rw [firstValue, secondValue]1053      rfl1054    . intros n nNatural1055      have typedN : Nat(n) by exact nat.omega.backward at n with nNatural1056      have indexNatural := monotoneIndex.natural with sequence1057      have indexInNaturals := nat.omega.forward with indexNatural1058      witness monotoneIndex(u, n)1059      constructor1060      . exact indexInNaturals1061      . exact monotoneSelector.relates at u, n with sequence10621063theorem monotoneSelector.value (u : Set, n : Nat)1064  requires sequence : RealSequence(u)1065  shows monotoneSelector(u)[n] = monotoneIndex(u, n)1066proof1067  have function := monotoneSelector.function with sequence1068  have nNatural := nat.omega.forward at n with assumption1069  have mapped := monotoneSelector.relates with sequence1070  exact FunctionBetween.apply_value with function, nNatural, mapped10711072theorem monotoneSelector.strictly_increasing (u : Set)1073  requires sequence : RealSequence(u)1074  shows StrictlyIncreasingNat(monotoneSelector(u))1075proof1076  constructor1077  . exact monotoneSelector.function with sequence1078  . intros m mNatural n nNatural order1079    have strict := monotoneIndex.strict with sequence, order1080    have valueM := monotoneSelector.value at u, m with sequence1081    have valueN := monotoneSelector.value at u, n with sequence1082    rwa [valueM, valueN]10831084theorem monotoneIndex.rises_without_peaks (u : Set, n : Nat)1085  requires sequence : RealSequence(u)1086  requires noUnbounded : ¬UnboundedSequencePeaks(u)1087  shows RealLess(u[monotoneIndex(u, n)], u[monotoneIndex(u, succ(n))])1088proof1089  obtain ⟨oldNatural, oldPosition⟩ := monotoneIndex.position with sequence1090  have inhabited := monotoneNextCandidates.nonempty with sequence, oldPosition1091  have naturals := monotoneNextCandidates.naturals at u, monotoneIndex(u, n)1092  have chosen := leastNatural.member with inhabited, naturals1093  obtain ⟨nextNatural, later, branch⟩ := monotoneNextCandidates.membership.forward with chosen1094  cases branch with peakBranch | risingBranch1095  . rcases peakBranch with ⟨unbounded, peak⟩1096    contradiction1097  . rcases risingBranch with ⟨bounded, rises⟩1098    rwa monotoneIndex10991100-- The selected values are monotone.  Arbitrarily late peaks give a1101-- nonincreasing subsequence; once peaks cease, every chosen value rises.1102theorem RealSequence.has_monotone_subsequence (u : Set)1103  requires sequence : RealSequence(u)1104  shows ∃ k, StrictlyIncreasingNat(k) ∧1105    (Nondecreasing(subsequence(u, k)) ∨1106     Nonincreasing(subsequence(u, k)))1107proof1108  witness monotoneSelector(u)1109  constructor1110  . exact monotoneSelector.strictly_increasing at u with sequence1111  . have alternatives := UnboundedSequencePeaks.or_not at u1112    cases alternatives with unbounded | noUnbounded1113    . right1114      have selectedSequence := subsequence.sequence at1115        u, monotoneSelector(u) with1116          sequence, monotoneSelector.strictly_increasing at u with sequence1117      apply StepwiseNonincreasing.nonincreasing1118      . exact selectedSequence1119        intros n nNatural1120        have typedN : Nat(n) by exact nat.omega.backward at n with nNatural1121        obtain ⟨currentNatural, position⟩ := monotoneIndex.position with sequence1122        have peak : SequencePeak(u, monotoneIndex(u, n))1123          cases position with peakBranch | risingBranch1124          . settle1125          . rcases risingBranch with ⟨bounded, tail⟩1126            contradiction1127        have nextIndexNatural := monotoneIndex.natural at u, succ(n) with sequence1128        have nextIndexInNaturals := nat.omega.forward with nextIndexNatural1129        have later := monotoneIndex.step at u, n with sequence1130        have decreases := peak with1131          monotoneIndex(u, succ(n)), nextIndexInNaturals, later1132        have valueNow := subsequence.value at1133          u, monotoneSelector(u), n with1134            sequence, monotoneSelector.strictly_increasing at u with sequence1135        have valueNext := subsequence.value at1136          u, monotoneSelector(u), succ(n) with1137            sequence, monotoneSelector.strictly_increasing at u with sequence1138        have selectorNow := monotoneSelector.value at u, n with sequence1139        have selectorNext := monotoneSelector.value at u, succ(n) with sequence1140        rwa [valueNow, valueNext, selectorNow, selectorNext]1141    . left1142      have selectedSequence := subsequence.sequence at1143        u, monotoneSelector(u) with1144          sequence, monotoneSelector.strictly_increasing at u with sequence1145      apply StepwiseNondecreasing.nondecreasing1146      . exact selectedSequence1147        intros n nNatural1148        have typedN : Nat(n) by exact nat.omega.backward at n with nNatural1149        have risesView := monotoneIndex.rises_without_peaks with sequence, noUnbounded1150        have rises := realLess.characterization.backward with risesView1151        have weak := realLess.implies_le with rises1152        have weakView := realLe.characterization.forward with weak1153        have valueNow := subsequence.value at1154          u, monotoneSelector(u), n with1155            sequence, monotoneSelector.strictly_increasing at u with sequence1156        have valueNext := subsequence.value at1157          u, monotoneSelector(u), succ(n) with1158            sequence, monotoneSelector.strictly_increasing at u with sequence1159        have selectorNow := monotoneSelector.value with sequence1160        have selectorNext := monotoneSelector.value at u, succ(n) with sequence1161        rwa [valueNow, valueNext, selectorNow, selectorNext]11621163theorem TermsIn.closedInterval_bounded_above (u : Set) (A B : Real)1164  requires terms : TermsIn(u, closedInterval(A, B))1165  shows BoundedAboveBy(u, B)1166proof1167  intros n nNatural1168  have member := terms with n, nNatural1169  have data := closedInterval.membership.forward with member1170  simp [RealLe, realLe.characterization]11711172theorem TermsIn.closedInterval_bounded_below (u : Set) (A B : Real)1173  requires terms : TermsIn(u, closedInterval(A, B))1174  shows BoundedBelowBy(u, A)1175proof1176  intros n nNatural1177  have member := terms with n, nNatural1178  have data := closedInterval.membership.forward with member1179  simp [RealLe, realLe.characterization]11801181-- Bolzano-Weierstrass for a sequence in a closed interval.  The proof first1182-- extracts a monotone subsequence, then invokes the appropriate half of the1183-- monotone convergence theorem.1184theorem closedInterval.bolzano_weierstrass (u : Set) (A B : Real)1185  requires sequence : RealSequence(u)1186  requires terms : TermsIn(u, closedInterval(A, B))1187  shows ∃ k, StrictlyIncreasingNat(k) ∧1188    ∃ L ∈ ℝ, L ∈ closedInterval(A, B) ∧1189      ConvergesTo(subsequence(u, k), L)1190proof1191  obtain ⟨k, increasing, monotone⟩ := RealSequence.has_monotone_subsequence with sequence1192  have selectedSequence := subsequence.sequence with sequence, increasing1193  have selectedTerms := TermsIn.subsequence with sequence, terms, increasing1194  witness k1195  constructor1196  . exact increasing1197  . cases monotone with nondecreasing | nonincreasing1198    . have boundedAbove := TermsIn.closedInterval_bounded_above at1199        subsequence(u, k), A, B with selectedTerms1200      have converges := Nondecreasing.converges_to_supremum with selectedSequence, nondecreasing, boundedAbove1201      have inhabited := RealSequence.range_nonempty with selectedSequence1202      have rangeUpper := BoundedAboveBy.range_upper_bound with selectedSequence, boundedAbove1203      have least := realSup.least_upper_bound with inhabited, rangeUpper1204      have supUpper : RealUpperBound(1205          range(subsequence(u, k)), realSup(range(subsequence(u, k))))1206        simp [RealLeastUpperBound]1207      rcases supUpper with ⟨limitReal, rangeReals, bounds⟩1208      witness realSup(range(subsequence(u, k)))1209      constructor1210        exact limitReal1211      . constructor1212        . exact closedInterval.contains_subsequence_limit at1213            u, k, realSup(range(subsequence(u, k))), A, B with1214              sequence, terms, increasing, converges1215        . exact converges1216    . have boundedBelow := TermsIn.closedInterval_bounded_below at1217        subsequence(u, k), A, B with selectedTerms1218      obtain ⟨L, realL, converges⟩ := Nonincreasing.has_limit with1219        selectedSequence, nonincreasing, boundedBelow1220      witness L1221      constructor1222      . exact realL1223      . constructor1224        . exact closedInterval.contains_subsequence_limit at1225            u, k, L, A, B with1226              sequence, terms, increasing, converges1227        . exact converges12281229theorem closedInterval.sequentially_compact (A B : Real)1230  shows SequentiallyCompact(closedInterval(A, B))1231proof1232  constructor1233  . exact closedInterval.subset_reals with *{2}1234  . intros u sequence terms1235    exact closedInterval.bolzano_weierstrass with sequence, terms12361237-- CompactContinuity1238theorem ContinuousWithinAt.converges_in (f u S : Set) (L : Real)1239  requires continuous : ContinuousWithinAt(f, S, L)1240  requires converges : ConvergesTo(u, L)1241  requires terms : TermsIn(u, S)1242  shows ConvergesTo(compose(f, u, ℕ, ℝ, ℝ), f(L))1243proof1244  rcases continuous with ⟨function, subset, control⟩1245  have sequence := ConvergesTo.sequence with converges1246  unfold RealSequence at sequence1247  have realL : L ∈ ℝ by simp [Real]1248  have fLReal := FunctionBetween.apply_closed with function1249  constructor1250  . unfold RealSequence1251    exact compose.function with sequence, function1252  . intros E realE positive1253    obtain ⟨D, realD, positiveD, maps⟩ :=1254      control with E, realE, positive1255    obtain ⟨N, naturalN, close⟩ := ConvergesTo.eventually with converges, positiveD1256    witness N1257    constructor1258    . exact naturalN1259    . intros n indexNatural nAfterN1260      have unReal := FunctionBetween.apply_closed with sequence, indexNatural1261      have member := terms1262      have inS := member with n, indexNatural1263      have near := close with n, indexNatural, nAfterN1264      have mapped := maps with u(n), unReal, inS, near1265      have value := compose.apply with sequence, function, indexNatural1266      rwa value12671268theorem ContinuousOn.converges_in (f u S : Set) (L : Real)1269  requires continuous : ContinuousOn(f, S)1270  requires limitMember : L ∈ S1271  requires converges : ConvergesTo(u, L)1272  requires terms : TermsIn(u, S)1273  shows ConvergesTo(compose(f, u, ℕ, ℝ, ℝ), f(L))1274proof1275  rcases continuous with ⟨function, subset, atEveryPoint⟩1276  have atLimit := atEveryPoint with L, limitMember1277  exact ContinuousWithinAt.converges_in with atLimit, converges, terms12781279-- Compactness supplies the convergent input subsequence; relative continuity1280-- transfers its limit through f, including when the limit is an endpoint.1281theorem ContinuousOn.compact_subsequence (f u S : Set)1282  requires continuous : ContinuousOn(f, S)1283  requires compact : SequentiallyCompact(S)1284  requires sequence : RealSequence(u)1285  requires terms : TermsIn(u, S)1286  shows ∃ k, StrictlyIncreasingNat(k) ∧1287    ∃ L ∈ ℝ, L ∈ S ∧1288      ConvergesTo(compose(f, subsequence(u, k), ℕ, ℝ, ℝ), f(L))1289proof1290  rcases compact with ⟨subset, extract⟩1291  obtain ⟨k, increasing, L, realL, member, converges⟩ :=1292    extract with u, sequence, terms1293  have selected := TermsIn.subsequence with sequence, terms, increasing1294  have mapped := ContinuousOn.converges_in with continuous, member, converges, selected1295  witness k1296  constructor1297  . exact increasing1298  . witness L1299    refine ⟨realL, member, mapped⟩13001301theorem closedInterval.continuous_subsequence (f u : Set) (A B : Real)1302  requires continuous : ContinuousOn(f, closedInterval(A, B))1303  requires sequence : RealSequence(u)1304  requires terms : TermsIn(u, closedInterval(A, B))1305  shows ∃ k, StrictlyIncreasingNat(k) ∧1306    ∃ L ∈ ℝ, L ∈ closedInterval(A, B) ∧1307      ConvergesTo(compose(f, subsequence(u, k), ℕ, ℝ, ℝ), f(L))1308proof1309  have compact := closedInterval.sequentially_compact at A, B with1310    *{2}1311  exact ContinuousOn.compact_subsequence with continuous, compact, sequence, terms1312