Grace/Cumulus/Real/Analysis/ExtremeValue.g17

Open in Workbench Download source

Imports

Set.Choice · SequentialCompactness

Declarations

Source

1-- Real analysis: ExtremeValue2-- 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.ExtremeValue8import Set.Choice9import SequentialCompactness1011-- Section: ShrinkingRadii12def realFunctionImage (f S : Set) : Set := { f(X) | X ∈ S }1314theorem realFunctionImage.subset_reals (f S : Set)15  requires function : f : ℝ → ℝ16  requires subset : S ⊆ ℝ17  shows realFunctionImage(f, S) ⊆ ℝ18proof19  intros Y member20  obtain ⟨X, inS, value⟩ := realFunctionImage.membership.forward with member21  have realX := subset with X, inS22  have realY := FunctionBetween.apply_closed with function, realX23  rwa value at realY2425defchoose imagePreimage (f S u : Set, n : Nat) (X ∈ ℝ) :=26  X ∈ S ∧ f(X) = u[n]27requires subset : S ⊆ ℝ28requires terms : TermsIn(u, realFunctionImage(f, S))29proof30  have naturalN := nat.omega.forward at n with assumption31  have member := terms with n, naturalN32  obtain ⟨X, inS, value⟩ := realFunctionImage.membership.forward at33    f, S, u[n] with member34  have realX := subset with X, inS35  witness X36  refine ⟨realX, inS, value⟩3738defgraph imagePreimages (f S u : Set) (n ∈ ℕ) : ℝ :=39  imagePreimage(f, S, u, n)40requires subset : S ⊆ ℝ41requires terms : TermsIn(u, realFunctionImage(f, S))42proof43  obtain ⟨realX, inS, value⟩ := imagePreimage.selected with subset, terms44  exact realX4546theorem imagePreimages.terms (f S u : Set)47  requires subset : S ⊆ ℝ48  requires terms : TermsIn(u, realFunctionImage(f, S))49  shows TermsIn(imagePreimages(f, S, u), S)50proof51  intros n naturalN52  have typedN := nat.omega.backward with naturalN53  have value := imagePreimages.value with subset, terms54  obtain ⟨realX, inS, equation⟩ := imagePreimage.selected with subset, terms55  rwa value5657theorem imagePreimages.maps (f S u : Set, n : Nat)58  requires subset : S ⊆ ℝ59  requires terms : TermsIn(u, realFunctionImage(f, S))60  shows f(imagePreimages(f, S, u)[n]) = u[n]61proof62  have value := imagePreimages.value with subset, terms63  obtain ⟨realX, inS, equation⟩ := imagePreimage.selected with subset, terms64  rwa value6566-- CompactImage67theorem ConvergesTo.of_equal_terms (u v : Set) (L : Real)68  requires sequence : RealSequence(u)69  requires converges : ConvergesTo(v, L)70  requires equal : ∀ n ∈ ℕ, u[n] = v[n]71  shows ConvergesTo(u, L)72proof73  constructor74  . exact sequence75  . intros E realE positive76    obtain ⟨N, naturalN, close⟩ := ConvergesTo.eventually with converges, positive77    witness N78    constructor79    . exact naturalN80    . intros n naturalIndex after81      have same := equal with n, naturalIndex82      rw same83      exact close with n, naturalIndex, after8485theorem realFunctionImage.sequentially_compact (f S : Set)86  requires continuous : ContinuousOn(f, S)87  requires compact : SequentiallyCompact(S)88  shows SequentiallyCompact(realFunctionImage(f, S))89proof90  rcases continuous with ⟨function, subset, atPoints⟩91  have continuousAgain : ContinuousOn(f, S) by refine ⟨function, subset, atPoints⟩92  constructor93  . exact realFunctionImage.subset_reals with function, subset94  . intros u sequence terms95    have preimages := imagePreimages.terms with subset, terms96    have preimageSequence : RealSequence(imagePreimages(f, S, u))97      unfold RealSequence98      exact imagePreimages.function with subset, terms99    obtain ⟨k, increasing, L, realL, member, mapped⟩ := ContinuousOn.compact_subsequence with100      continuousAgain, compact, preimageSequence, preimages101    have selectedSequence := subsequence.sequence with sequence, increasing102    have mappedConverges : ConvergesTo(subsequence(u, k), f(L))103      apply ConvergesTo.of_equal_terms with selectedSequence, mapped104      intros n naturalN105      have typedN := nat.omega.backward with naturalN106      have selector := StrictlyIncreasingNat.function with increasing107      have selectedNatural := FunctionBetween.apply_closed with selector, naturalN108      have typedSelected := nat.omega.backward with selectedNatural109      have imageValue := imagePreimages.maps at f, S, u, k[n] with110        subset, terms111      have selectedInput := subsequence.value at112        imagePreimages(f, S, u), k, n with preimageSequence, increasing113      have selectedOutput := subsequence.value at u, k, n with114        sequence, increasing115      have inputSequence := subsequence.sequence with preimageSequence, increasing116      have inputFunction : subsequence(imagePreimages(f, S, u), k) : ℕ → ℝ by exact inputSequence117      have composed := compose.apply with inputFunction, function, naturalN118      rw [composed, selectedInput, selectedOutput, imageValue]119      rfl120    have imageMember : f(L) ∈ realFunctionImage(f, S)121      apply realFunctionImage.membership.backward122      witness L123      refine ⟨member, rfl⟩124    witness k125    constructor126    . exact increasing127    . witness f(L)128      have realLValue := FunctionBetween.apply_closed with function, realL129      refine ⟨realLValue, imageMember, mappedConverges⟩130131theorem closedInterval.continuous_image_compact (f : Set) (A B : Real)132  requires continuous : ContinuousOn(f, closedInterval(A, B))133  shows SequentiallyCompact(realFunctionImage(f, closedInterval(A, B)))134proof135  have compact := closedInterval.sequentially_compact at A, B with136    *{2}137  exact realFunctionImage.sequentially_compact with continuous, compact138139-- NearbySequences140predicate AsymptoticallyClose (u v : Set) :=141  RealSequence(u) ∧ RealSequence(v) ∧142  (∀ E ∈ ℝ, 0 < E →143    ∃ N ∈ ℕ, ∀ n ∈ ℕ, N ≤ n →144      vₙ ∈ openBall(uₙ, E))145146theorem AsymptoticallyClose.eventually (u v : Set) (E : Real)147  requires close : AsymptoticallyClose(u, v)148  requires positive : 0 < E149  shows ∃ N ∈ ℕ, ∀ n ∈ ℕ, N ≤ n →150    vₙ ∈ openBall(uₙ, E)151proof152  rcases close with ⟨sequenceU, sequenceV, eventual⟩153  exact eventual with E, positive154155theorem AsymptoticallyClose.symmetric (u v : Set)156  requires close : AsymptoticallyClose(u, v)157  shows AsymptoticallyClose(v, u)158proof159  rcases close with ⟨sequenceU, sequenceV, eventual⟩160  unfold AsymptoticallyClose161  refine ⟨sequenceV, sequenceU, _⟩162  intros E realE positive163  obtain ⟨N, naturalN, near⟩ := eventual with E, realE, positive164  witness N165  constructor166  . exact naturalN167  . intros n littleNatural afterN168    have typedN : Nat(n) by exact nat.omega.backward at n with littleNatural169    have realU := RealSequence.value with sequenceU170    have realV := RealSequence.value with sequenceV171    have nearVU := near with n, littleNatural, afterN172    exact openBall.symmetric.forward with realV, realU, nearVU173174theorem ConvergesTo.of_asymptotically_close (u v : Set) (L : Real)175  requires converges : ConvergesTo(u, L)176  requires close : AsymptoticallyClose(u, v)177  shows ConvergesTo(v, L)178proof179  rcases close with ⟨sequenceU, sequenceV, closeness⟩180  constructor181  . exact sequenceV182  . intros E realE positive183    have typedE : Real(E) by exact realE184    have halfReal := half.real with typedE185    have halfPositive := half.positive with positive186    obtain ⟨N, nNatural, nearL⟩ := ConvergesTo.eventually with converges, halfPositive187    obtain ⟨M, mNatural, nearU⟩ :=188      closeness with half(E), halfPositive189    have typedN : Nat(N) by exact nat.omega.backward at N with nNatural190    have typedM : Nat(M) by exact nat.omega.backward at M with mNatural191    have comparison := Less.trichotomy with typedN, typedM192    cases comparison with nLessM | rest193    . have nLeM := Less.implies_LessEqual at N, M with194        typedN, typedM, nLessM195      witness M196      constructor197      . exact mNatural198      . intros n naturalN mLeN199        have nLeLittleN := LessEqual.transitive with nLeM, mLeN200        have closeL := nearL with n, naturalN, nLeLittleN201        have closeU := nearU with n, naturalN, mLeN202        have realU := RealSequence.value at u, n with sequenceU203        have realV := RealSequence.value at v, n with sequenceV204        have double := openBall.triangle at205          vₙ, uₙ, L, half(E), half(E) with206            realV, realU, assumption, halfReal, halfReal, closeU, closeL207        have halves := half.add_self with typedE208        rwa halves at double209    . cases rest with equal | mLessN210      . witness N211        constructor212        . exact nNatural213        . intros n naturalN nLeLittleN214          have mLeLittleN : M ≤ n by rwa ← equal215          have closeL := nearL with n, naturalN, nLeLittleN216          have closeU := nearU with n, naturalN, mLeLittleN217          have realU := RealSequence.value at u, n with sequenceU218          have realV := RealSequence.value at v, n with sequenceV219          have double := openBall.triangle at220            vₙ, uₙ, L, half(E), half(E) with221              realV, realU, assumption, halfReal, halfReal, closeU, closeL222          have halves := half.add_self with typedE223          rwa halves at double224      . have mLeN := Less.implies_LessEqual at M, N with225          typedM, typedN, mLessN226        witness N227        constructor228        . exact nNatural229        . intros n naturalN nLeLittleN230          have mLeLittleN := LessEqual.transitive with mLeN, nLeLittleN231          have closeL := nearL with n, naturalN, nLeLittleN232          have closeU := nearU with n, naturalN, mLeLittleN233          have realU := RealSequence.value at u, n with sequenceU234          have realV := RealSequence.value at v, n with sequenceV235          have double := openBall.triangle at236            vₙ, uₙ, L, half(E), half(E) with237              realV, realU, assumption, halfReal, halfReal, closeU, closeL238          have halves := half.add_self with typedE239          rwa halves at double240241theorem AsymptoticallyClose.subsequence (u v k : Set)242  requires close : AsymptoticallyClose(u, v)243  requires increasing : StrictlyIncreasingNat(k)244  shows AsymptoticallyClose(subsequence(u, k), subsequence(v, k))245proof246  rcases close with ⟨sequenceU, sequenceV, eventually⟩247  constructor248  . exact subsequence.sequence with sequenceU, increasing249  . constructor250    . exact subsequence.sequence with sequenceV, increasing251    . intros E realE positive252      obtain ⟨N, nNatural, near⟩ := eventually with E, realE, positive253      witness N254      constructor255      . exact nNatural256      . intros n littleNatural afterN257        have typedN : Nat(n) by exact nat.omega.backward at n with littleNatural258        have typedThreshold : Nat(N) by exact nat.omega.backward at N with nNatural259        have selectedNatural := FunctionBetween.apply_closed at260          k, ℕ, ℕ, n with261            StrictlyIncreasingNat.function at k with increasing,262            littleNatural263        have typedSelected : Nat(kₙ) by exact nat.omega.backward at kₙ with selectedNatural264        have aboveIndex := StrictlyIncreasingNat.index_le_value at265          k, n with increasing266        have aboveThreshold := LessEqual.transitive with267          typedThreshold, typedN, typedSelected, afterN, aboveIndex268        have selectedNear := near with kₙ, selectedNatural, aboveThreshold269        have uValue := subsequence.value at u, k, n with270          sequenceU, increasing271        have vValue := subsequence.value at v, k, n with272          sequenceV, increasing273        rwa [vValue, uValue]274275-- In a sequentially compact set, one extracted subsequence of u makes276-- both u and every asymptotically close companion v converge to its limit.277theorem SequentiallyCompact.nearby_subsequences (S u v : Set)278  requires compact : SequentiallyCompact(S)279  requires sequence : RealSequence(u)280  requires terms : TermsIn(u, S)281  requires close : AsymptoticallyClose(u, v)282  shows ∃ k, StrictlyIncreasingNat(k) ∧283    ∃ L ∈ ℝ, L ∈ S ∧284      ConvergesTo(subsequence(u, k), L) ∧285      ConvergesTo(subsequence(v, k), L)286proof287  rcases compact with ⟨subset, extract⟩288  obtain ⟨k, increasing, L, realL, member, converges⟩ :=289    extract with u, sequence, terms290  have selectedClose := AsymptoticallyClose.subsequence with close, increasing291  have companion := ConvergesTo.of_asymptotically_close with converges, selectedClose292  witness k293  constructor294  . exact increasing295  . witness L296    refine ⟨realL, member, converges, companion⟩297298theorem ContinuousOn.nearby_compact_images (f S u v : Set)299  requires continuous : ContinuousOn(f, S)300  requires compact : SequentiallyCompact(S)301  requires sequence : RealSequence(u)302  requires termsU : TermsIn(u, S)303  requires termsV : TermsIn(v, S)304  requires close : AsymptoticallyClose(u, v)305  shows ∃ k, StrictlyIncreasingNat(k) ∧306    ∃ L ∈ ℝ, L ∈ S ∧307      ConvergesTo(compose(f, subsequence(u, k), ℕ, ℝ, ℝ), f(L)) ∧308      ConvergesTo(compose(f, subsequence(v, k), ℕ, ℝ, ℝ), f(L))309proof310  obtain ⟨k, increasing, L, realL, member, convergesU, convergesV⟩ := SequentiallyCompact.nearby_subsequences with311    compact, sequence, termsU, close312  have selectedU := TermsIn.subsequence with sequence, termsU, increasing313  obtain ⟨uSequence, vSequence, eventually⟩ := close314  have selectedV := TermsIn.subsequence with vSequence, termsV, increasing315  have mappedU := ContinuousOn.converges_in with continuous, member, convergesU, selectedU316  have mappedV := ContinuousOn.converges_in with continuous, member, convergesV, selectedV317  witness k318  constructor319  . exact increasing320  . witness L321    refine ⟨realL, member, mappedU, mappedV⟩322323-- Images that share a limit cannot remain a fixed positive distance apart.324theorem ConvergesTo.eventually_near_each_other (u v : Set) (L E : Real)325  requires convergesU : ConvergesTo(u, L)326  requires convergesV : ConvergesTo(v, L)327  requires positive : 0 < E328  shows ∃ N ∈ ℕ, ∀ n ∈ ℕ, N ≤ n →329    vₙ ∈ openBall(uₙ, E)330proof331  have halfReal := half.real at E332  have halfPositive := half.positive with positive333  obtain ⟨N, naturalN, both⟩ := ConvergesTo.common_eventually with334    convergesU, convergesV, halfPositive, halfPositive335  witness N336  constructor337  . exact naturalN338  . intros n littleNatural afterN339    have typedN : Nat(n) by exact nat.omega.backward at n with littleNatural340    obtain ⟨nearU, nearV⟩ := both with n, littleNatural, afterN341    have sequenceU := ConvergesTo.sequence with convergesU342    have realU := RealSequence.value with sequenceU343    have sequenceV := ConvergesTo.sequence with convergesV344    have realV := RealSequence.value with sequenceV345    have fromLimit := openBall.symmetric.forward at346      uₙ, L, half(E) with realU, assumption, halfReal, nearU347    have together := openBall.triangle at348      vₙ, L, uₙ, half(E), half(E) with349        realV, assumption, realU, halfReal, halfReal, nearV, fromLimit350    have halves := half.add_self at E351    rwa halves at together352353-- UniformFailure354predicate UniformFailurePair (f S : Set) (E D : Real, X Y : Real) :=355  X ∈ S ∧ Y ∈ S ∧356  X ∈ openBall(Y, D) ∧357  ¬(f(X) ∈ openBall(f(Y), E))358359-- Under the function and carrier assumptions supplied by continuity,360-- negating uniform continuity fixes one output tolerance once and for all.361theorem ContinuousOn.nonuniform_tolerance (f S : Set)362  requires continuous : ContinuousOn(f, S)363  requires notUniform : ¬UniformContinuousOn(f, S)364  shows ∃ E ∈ ℝ, (0 < E ∧365    ∀ D ∈ ℝ, (0 < D →366      ¬(∀ X ∈ ℝ, (X ∈ S →367        ∀ Y ∈ ℝ, (Y ∈ S →368          (X ∈ openBall(Y, D) →369            f(X) ∈ openBall(f(Y), E)))))))370proof371  rcases continuous with ⟨function, subset, atPoints⟩372  by_contra noTolerance373  apply notUniform374  constructor375  . exact function376  . constructor377    . exact subset378    . intros E realE positive379      have radiusExists : ∃ D ∈ ℝ, (0 < D ∧380          ∀ X ∈ ℝ, (X ∈ S →381            ∀ Y ∈ ℝ, (Y ∈ S →382              (X ∈ openBall(Y, D) →383                f(X) ∈ openBall(f(Y), E)))))384        by_contra noRadius385        apply noTolerance386        witness E387        constructor388        . exact realE389        . constructor390          . exact positive391          . intros D realD positiveD maps392            apply noRadius393            witness D394            refine ⟨realD, positiveD, maps⟩395      exact radiusExists396397-- This is the textbook epsilon that defeats every delta, with the real398-- witnesses and interval membership written out.399theorem ContinuousOn.nonuniform_pairs (f S : Set)400  requires continuous : ContinuousOn(f, S)401  requires notUniform : ¬UniformContinuousOn(f, S)402  shows ∃ E ∈ ℝ, (0 < E ∧403    ∀ D ∈ ℝ, (0 < D →404      ∃ X ∈ ℝ, ∃ Y ∈ ℝ, UniformFailurePair(f, S, E, D, X, Y)))405proof406  obtain ⟨E, realE, positiveE, noRadius⟩ := ContinuousOn.nonuniform_tolerance with continuous, notUniform407  witness E408  constructor409  . exact realE410  . constructor411    . exact positiveE412    . intros D realD positiveD413      have noMaps := noRadius with D, realD, positiveD414      have bad : ∃ X ∈ ℝ, ∃ Y ∈ ℝ, (415          X ∈ S ∧ Y ∈ S ∧ X ∈ openBall(Y, D) ∧416            ¬(f(X) ∈ openBall(f(Y), E)))417        by_contra noBad418        apply noMaps419        intros P realP memberP Q realQ memberQ near420        by_contra notNear421        apply noBad422        witness P423        constructor424        . exact realP425        . witness Q426          refine ⟨realQ, memberP, memberQ, near, notNear⟩427      obtain ⟨X, realX, Y, realY, memberX, memberY, near, far⟩ := bad428      witness X429      constructor430      . exact realX431      . witness Y432        constructor433        . exact realY434        . unfold UniformFailurePair435          refine ⟨memberX, memberY, near, far⟩436437-- ShrinkingRadii438def dyadicRadius (n : Nat) → Real439  | 0 => realOne440  | succ(n) => half(dyadicRadius(n))441442theorem dyadicRadius.real (n : Nat)443  shows Real(dyadicRadius(n))444proof445  induction n446  | zero =>447    rw dyadicRadius448    exact realOne.real449  | succ(j) using ih =>450    rw dyadicRadius451    exact half.real with ih452453theorem dyadicRadius.positive (n : Nat)454  shows 0 < dyadicRadius(n)455proof456  induction n457  | zero =>458    rw dyadicRadius459    exact realZero.lt_one460  | succ(j) using ih =>461    rw dyadicRadius462    exact half.positive with ih463464theorem dyadicRadius.strictly_decreasing (n : Nat)465  shows dyadicRadius(succ(n)) < dyadicRadius(n)466proof467  have positive := dyadicRadius.positive at n468  rw dyadicRadius469  exact half.lt_self with positive470471-- Replacement constructs the bounded graph; defgraph checks its real-valued472-- closure and derives its function, relation, and application laws.473defgraph dyadicRadii (n : Nat) : Real := dyadicRadius(n)474475theorem dyadicRadii.sequence476  shows RealSequence(dyadicRadii)477proof478  exact dyadicRadii.function479480theorem dyadicRadii.nonincreasing481  shows Nonincreasing(dyadicRadii)482proof483  have step : StepwiseNonincreasing(dyadicRadii)484    intros n naturalN485    have typedN : Nat(n) by exact nat.omega.backward at n with naturalN486    have typedNext := Naturals.constructor.succ with typedN487    have less := dyadicRadius.strictly_decreasing with typedN488    have weak := realLess.implies_le with less489    have valueN := dyadicRadii.value with typedN490    have valueNext := dyadicRadii.value with typedNext491    rw [valueNext, valueN]492    exact realLe.characterization.forward with weak493  exact StepwiseNonincreasing.nonincreasing with dyadicRadii.sequence, step494495theorem dyadicRadii.bounded_below496  shows BoundedBelowBy(dyadicRadii, realZero)497proof498  intros n naturalN499  have typedN : Nat(n) by exact nat.omega.backward at n with naturalN500  have positive := dyadicRadius.positive with typedN501  have weak := realLess.implies_le with positive502  have value := dyadicRadii.value with typedN503  rw value504  exact realLe.characterization.forward with weak505506theorem dyadicRadii.has_limit507  shows ∃ L ∈ ℝ, ConvergesTo(dyadicRadii, L)508proof509  exact Nonincreasing.has_limit with510    dyadicRadii.sequence, dyadicRadii.nonincreasing, dyadicRadii.bounded_below511512-- A positive limiting value L is impossible: eventually a radius r lies513-- below L + L, while the next radius is r/2 and must still lie above L.514theorem dyadicRadii.limit_zero515  shows realSequenceInfimum(dyadicRadii) = realZero516proof517  have converges := Nonincreasing.converges_to_infimum with518    dyadicRadii.sequence, dyadicRadii.nonincreasing, dyadicRadii.bounded_below519  have limitReal : Real(realSequenceInfimum(dyadicRadii))520    exact realSequenceInfimum.real with dyadicRadii.sequence, dyadicRadii.bounded_below521  have nonnegative := ConvergesTo.ge_constant with converges, dyadicRadii.bounded_below522  have nonpositive : realSequenceInfimum(dyadicRadii) ≤ realZero523    by_contra notLe524    have positive := realLess.of_not_le with notLe525    obtain ⟨N, naturalN, eventually⟩ := ConvergesTo.eventually with converges, positive526    have typedN : Nat(N) by exact nat.omega.backward at N with naturalN527    have typedNext := Naturals.constructor.succ with typedN528    have reflexive := LessEqual.reflexive with typedN529    have near := eventually with N, naturalN, reflexive530    have lower := Nonincreasing.infimum_le_term at531      dyadicRadii, realZero, succ(N) with532        dyadicRadii.sequence, dyadicRadii.bounded_below533    have valueN := dyadicRadii.value with typedN534    have valueNext := dyadicRadii.value with typedNext535    rw [valueNext, dyadicRadius] at lower536    have radiusReal := dyadicRadius.real with typedN537    have doubled := realLe.add with lower, lower538    have halves := half.add_self with radiusReal539    rw halves at doubled540    rw valueN at near541    obtain ⟨lowerNear, upperNear⟩ := openBall.order_characterization.forward with near542    have impossible := realLe.transitive_less with doubled, upperNear543    exact IsOrderedField.irreflexive with reals.ordered_field, impossible544  have lowerView := realLe.characterization.forward with nonnegative545  have upperView := realLe.characterization.forward with nonpositive546  exact RealLe.antisymmetric with upperView, lowerView547548theorem dyadicRadii.converges_zero549  shows ConvergesTo(dyadicRadii, realZero)550proof551  have converges := Nonincreasing.converges_to_infimum with552    dyadicRadii.sequence, dyadicRadii.nonincreasing, dyadicRadii.bounded_below553  rwa dyadicRadii.limit_zero at converges554555theorem dyadicRadii.eventually_below (E : Real)556  requires positive : 0 < E557  shows ∃ N ∈ ℕ, ∀ n ∈ ℕ, N ≤ n → dyadicRadius(n) < E558proof559  obtain ⟨N, naturalN, close⟩ := ConvergesTo.eventually with dyadicRadii.converges_zero, positive560  witness N561  constructor562  . exact naturalN563  . intros n littleNatural afterN564    have typedN : Nat(n) by exact nat.omega.backward at n with littleNatural565    have near := close with n, littleNatural, afterN566    have value := dyadicRadii.value with typedN567    rw value at near568    obtain ⟨lower, upper⟩ := openBall.order_characterization.forward with near569    have zero := realAddValue.zero_left at E570    rwa zero at upper571572-- Section: ExtremeValue573defchoose nearSupremumPoint (S : Set, U : Real, n : Nat) (X ∈ ℝ) :=574  X ∈ S ∧ U - dyadicRadius(n) < X575requires least : RealLeastUpperBound(S, U)576proof577  have radius := dyadicRadius.positive at n578  obtain ⟨X, inS, near⟩ := RealLeastUpperBound.approached with least, radius579  have upper : RealUpperBound(S, U)580    rcases least with ⟨bound, minimal⟩581    exact bound582  rcases upper with ⟨realU, subset, bounds⟩583  have realX := subset with X, inS584  witness X585  refine ⟨realX, inS, near⟩586587defgraph nearSupremumSequence (S : Set, U : Real) (n ∈ ℕ) : ℝ :=588  nearSupremumPoint(S, U, n)589requires least : RealLeastUpperBound(S, U)590proof591  obtain ⟨realX, inS, near⟩ := nearSupremumPoint.selected with least592  exact realX593594theorem nearSupremumSequence.terms (S : Set) (U : Real)595  requires least : RealLeastUpperBound(S, U)596  shows TermsIn(nearSupremumSequence(S, U), S)597proof598  intros n naturalN599  have typedN := nat.omega.backward with naturalN600  have value := nearSupremumSequence.value with least601  obtain ⟨realX, member, near⟩ := nearSupremumPoint.selected with least602  rwa value603604theorem nearSupremumSequence.bounds (S : Set) (U : Real, n : Nat)605  requires least : RealLeastUpperBound(S, U)606  shows U - dyadicRadii[n] < nearSupremumSequence(S, U)[n] ∧607    nearSupremumSequence(S, U)[n] ≤ U608proof609  have value := nearSupremumSequence.value with least610  have radius := dyadicRadii.value at n611  obtain ⟨realX, member, near⟩ := nearSupremumPoint.selected with least612  have upper : RealUpperBound(S, U)613    rcases least with ⟨bound, minimal⟩614    exact bound615  rcases upper with ⟨realU, subset, bounds⟩616  have bound := bounds with nearSupremumPoint(S, U, n), member617  have realPoint : Real(nearSupremumPoint(S, U, n)) by exact realX618  have weak := realLe.of_subset with realPoint, realU, bound619  constructor620  . rw [value, radius]621    exact near622  . rw value623    exact weak624625theorem nearSupremumSequence.converges (S : Set) (U : Real)626  requires least : RealLeastUpperBound(S, U)627  shows ConvergesTo(nearSupremumSequence(S, U), U)628proof629  have upperConverges := constantSequence.converges at U630  have lowerConverges := ConvergesTo.sub with upperConverges, dyadicRadii.converges_zero631  have zero : U - realZero = U by ring632  rw zero at lowerConverges633  have upperSequence := ConvergesTo.sequence with upperConverges634  have lowerSequence := ConvergesTo.sequence with lowerConverges635  have nearSequence : RealSequence(nearSupremumSequence(S, U))636    unfold RealSequence637    exact nearSupremumSequence.function with least638  have lower : PointwiseLE(subSequence(constantSequence(U), dyadicRadii),639      nearSupremumSequence(S, U))640    intros n naturalN641    have typedN := nat.omega.backward with naturalN642    obtain ⟨strict, weak⟩ := nearSupremumSequence.bounds with least643    have constantValue := constantSequence.value at U, n644    have radiusValue := dyadicRadii.value at n645    have realConstant := RealSequence.value with upperSequence646    have realRadius := RealSequence.value with dyadicRadii.sequence647    have lowerAtN := subSequence.value with upperSequence, dyadicRadii.sequence, realConstant, realRadius648    rw constantValue at lowerAtN649    rw lowerAtN650    have lowerWeak := realLess.implies_le with strict651    exact realLe.characterization.forward with lowerWeak652  have upper : PointwiseLE(nearSupremumSequence(S, U), constantSequence(U))653    intros j naturalJ654    have typedJ := nat.omega.backward with naturalJ655    obtain ⟨strict, weak⟩ := nearSupremumSequence.bounds with least656    have constantValue := constantSequence.value at U, j657    rw constantValue658    exact realLe.characterization.forward with weak659  exact ConvergesTo.squeeze with lowerConverges, nearSequence, upperConverges, lower, upper660661-- CompactExtrema662theorem SequentiallyCompact.contains_supremum (S : Set) (U : Real)663  requires compact : SequentiallyCompact(S)664  requires least : RealLeastUpperBound(S, U)665  shows U ∈ S666proof667  have sequence : RealSequence(nearSupremumSequence(S, U))668    unfold RealSequence669    exact nearSupremumSequence.function with least670  have terms := nearSupremumSequence.terms with least671  rcases compact with ⟨subset, extract⟩672  obtain ⟨k, increasing, L, realL, member, converges⟩ :=673    extract with nearSupremumSequence(S, U), sequence, terms674  have limit := nearSupremumSequence.converges with least675  have selected := ConvergesTo.subsequence with limit, increasing676  have same := ConvergesTo.unique with converges, selected677  rwa ← same678679theorem SequentiallyCompact.has_maximum_of_upper_bound (S : Set) (B : Real)680  requires compact : SequentiallyCompact(S)681  requires inhabited : Nonempty(S)682  requires upper : RealUpperBound(S, B)683  shows ∃ U ∈ S, ∀ X ∈ S, (X:R) ≤ (U:R)684proof685  have least := realSup.least_upper_bound with inhabited, upper686  have typedSup : Real(realSup(S))687    rcases least with ⟨bound, minimal⟩688    rcases bound with ⟨realSupremum, reals, below⟩689    exact realSupremum690  have member := SequentiallyCompact.contains_supremum with compact, least691  witness realSup(S)692  constructor693  . exact member694  . intros X inS695    rcases least with ⟨bound, minimal⟩696    rcases bound with ⟨realSupremum, reals, below⟩697    have included := below with X, inS698    have realX := reals with X, inS699    exact realLe.of_subset with realSupremum, included700701theorem ContinuousOn.closed_interval_maximum_of_upper_bound (f : Set) (A B M : Real)702  requires ordered : A ≤ B703  requires continuous : ContinuousOn(f, closedInterval(A, B))704  requires upper : RealUpperBound(realFunctionImage(f, closedInterval(A, B)), M)705  shows ∃ T ∈ closedInterval(A, B),706    ∀ X ∈ closedInterval(A, B),707      (f(X):R) ≤ (f(T):R)708proof709  have compact := closedInterval.continuous_image_compact with continuous710  have left := closedInterval.left_mem with ordered711  have function : f : ℝ → ℝ712    rcases continuous with ⟨graph, subset, points⟩713    exact graph714  have imageLeft : f(A) ∈ realFunctionImage(f, closedInterval(A, B))715    apply realFunctionImage.membership.backward716    witness A717    refine ⟨left, rfl⟩718  have inhabited : Nonempty(realFunctionImage(f, closedInterval(A, B))) := ⟨f(A), imageLeft⟩719  obtain ⟨V, inImage, greatest⟩ := SequentiallyCompact.has_maximum_of_upper_bound with720    compact, inhabited, upper721  obtain ⟨T, inInterval, value⟩ := realFunctionImage.membership.forward with inImage722  witness T723  constructor724  . exact inInterval725  . intros X inIntervalX726    have imageX : f(X) ∈ realFunctionImage(f, closedInterval(A, B))727      apply realFunctionImage.membership.backward728      witness X729      refine ⟨inIntervalX, rfl⟩730    have bound := greatest with f(X), imageX731    rwa value732733-- EscapingSequence734predicate UnboundedAbove (S : Set) :=735  ∀ B ∈ ℝ, ∃ X ∈ S, (B:R) < (X:R)736737defchoose nextAbove (S : Set, B : Real) (X ∈ ℝ) :=738  X ∈ S ∧ B + 1 < X739requires subset : S ⊆ ℝ740requires unbounded : UnboundedAbove(S)741proof742  have threshold := realAddValue.real at B, realOne with743    assumption, realOne.real744  have memberThreshold : B + 1 ∈ ℝ745    unfold Real at threshold746    exact threshold747  unfold UnboundedAbove at unbounded748  obtain ⟨X, inS, above⟩ := unbounded with B + 1, memberThreshold749  unfold Subset at subset750  have realX := subset with X, inS751  witness X752  refine ⟨realX, inS, above⟩753754def escapingPoint (S : Set, A : Real, n : Nat) → Set755  | S, A, zero => A756  | S, A, succ(k) => nextAbove(S, escapingPoint(S, A, k))757758theorem escapingPoint.real (S : Set) (A : Real, n : Nat)759  requires subset : S ⊆ ℝ760  requires unbounded : UnboundedAbove(S)761  shows Real(escapingPoint(S, A, n))762proof763  induction n764  | zero =>765    rwa escapingPoint766  | succ(k) using ih =>767    rw escapingPoint768    have selected := nextAbove.selected at769      S, escapingPoint(S, A, k) with subset, unbounded770    rcases selected with ⟨realX, inS, above⟩771    exact realX772773defgraph escapingSequence (S : Set, A : Real) (n ∈ ℕ) : ℝ :=774  escapingPoint(S, A, n)775requires subset : S ⊆ ℝ776requires unbounded : UnboundedAbove(S)777proof778  exact escapingPoint.real with subset, unbounded779780theorem escapingPoint.member (S : Set) (A : Real, n : Nat)781  requires subset : S ⊆ ℝ782  requires unbounded : UnboundedAbove(S)783  requires start : A ∈ S784  shows escapingPoint(S, A, n) ∈ S785proof786  induction n787  | zero =>788    rwa escapingPoint789  | succ(k) using ih =>790    rw escapingPoint791    have selected := nextAbove.selected at792      S, escapingPoint(S, A, k) with subset, unbounded793    rcases selected with ⟨realX, inS, above⟩794    exact inS795796theorem escapingSequence.terms (S : Set) (A : Real)797  requires subset : S ⊆ ℝ798  requires unbounded : UnboundedAbove(S)799  requires start : A ∈ S800  shows TermsIn(escapingSequence(S, A), S)801proof802  intros n naturalN803  have typedN := nat.omega.backward with naturalN804  have value := escapingSequence.value with subset, unbounded805  rw value806  exact escapingPoint.member with subset, unbounded, start807808theorem escapingSequence.step (S : Set) (A : Real, n : Nat)809  requires subset : S ⊆ ℝ810  requires unbounded : UnboundedAbove(S)811  shows escapingSequence(S, A)[n] + 1 < escapingSequence(S, A)[succ(n)]812proof813  have selected := nextAbove.selected at814    S, escapingPoint(S, A, n) with subset, unbounded815  rcases selected with ⟨realX, inS, above⟩816  have atN := escapingSequence.value with subset, unbounded817  have atNext := escapingSequence.value at S, A, succ(n) with818    subset, unbounded819  rw escapingPoint at atNext820  rwa [atN, atNext]821822theorem escapingSequence.nondecreasing (S : Set) (A : Real)823  requires subset : S ⊆ ℝ824  requires unbounded : UnboundedAbove(S)825  shows Nondecreasing(escapingSequence(S, A))826proof827  have sequence : RealSequence(escapingSequence(S, A))828    unfold RealSequence829    exact escapingSequence.function with subset, unbounded830  have stepwise : StepwiseNondecreasing(escapingSequence(S, A))831    intros n naturalN832    have typedN := nat.omega.backward with naturalN833    have step := escapingSequence.step with subset, unbounded834    have realN := RealSequence.value with sequence835    have realNext := RealSequence.value at escapingSequence(S, A), succ(n) with sequence836    have positive := realLess.add_left with realZero.real, realOne.real, realN, realZero.lt_one837    have zero := realAddValue.zero_right with realN838    rw zero at positive839    have realPlus := realAddValue.real with realN, realOne.real840    have strict : escapingSequence(S, A)[n] < escapingSequence(S, A)[succ(n)]841      exact realLess.transitive with realN, realPlus, realNext, positive, step842    have weak := realLess.implies_le with strict843    exact realLe.characterization.forward with weak844  exact StepwiseNondecreasing.nondecreasing with sequence, stepwise845846theorem escapingSequence.gap (S : Set) (A : Real, i j : Nat)847  requires subset : S ⊆ ℝ848  requires unbounded : UnboundedAbove(S)849  requires before : i < j850  shows escapingSequence(S, A)[i] + 1 < escapingSequence(S, A)[j]851proof852  have sequence : RealSequence(escapingSequence(S, A))853    unfold RealSequence854    exact escapingSequence.function with subset, unbounded855  have increasing := escapingSequence.nondecreasing with subset, unbounded856  have naturalNext := nat.omega.forward at succ(i) with857    Naturals.constructor.succ at i with assumption858  have naturalJ := nat.omega.forward at j with assumption859  have after := increasing with succ(i), naturalNext, j, naturalJ, before860  have weak := realLe.characterization.backward with after861  have step := escapingSequence.step at S, A, i with subset, unbounded862  have realI := RealSequence.value at escapingSequence(S, A), i with sequence863  have realNext := RealSequence.value at escapingSequence(S, A), succ(i) with sequence864  have realJ := RealSequence.value at escapingSequence(S, A), j with sequence865  exact realLess.transitive_le with realNext, realJ, step, weak866867-- CompactBounded868theorem SequentiallyCompact.not_unbounded_above (S : Set)869  requires compact : SequentiallyCompact(S)870  requires inhabited : Nonempty(S)871  shows ¬UnboundedAbove(S)872proof873  intro unbounded874  obtain ⟨A, start⟩ := inhabited875  rcases compact with ⟨subset, extract⟩876  have realA : Real(A)877    unfold Real878    have subsetView := subset879    exact subsetView with A, start880  have sequence : RealSequence(escapingSequence(S, A))881    unfold RealSequence882    exact escapingSequence.function with subset, unbounded883  have terms := escapingSequence.terms with subset, unbounded, start884  obtain ⟨k, increasing, L, realL, member, converges⟩ :=885    extract with escapingSequence(S, A), sequence, terms886  have halfReal := half.real with realOne.real887  have halfPositive := half.positive with realOne.real, realZero.lt_one888  obtain ⟨N, naturalN, close⟩ := ConvergesTo.eventually with converges, halfPositive889  have typedN := nat.omega.backward with naturalN890  have nextN := Naturals.constructor.succ with typedN891  have nextNatural := nat.omega.forward with nextN892  have order : N ≤ succ(N) by exact LessEqual.successor at N with typedN893  have orderNext := LessEqual.reflexive with nextN894  have nearFirst := close with N, naturalN,895    LessEqual.reflexive with typedN896  have nearSecond := close with succ(N), nextNatural, order897  have selector := StrictlyIncreasingNat.function with increasing898  have indexFirst := FunctionBetween.apply_closed with selector, naturalN899  have indexSecond := FunctionBetween.apply_closed with selector, nextNatural900  have typedFirst := nat.omega.backward with indexFirst901  have typedSecond := nat.omega.backward with indexSecond902  have increasingAgain := increasing903  rcases increasing with ⟨selectorAgain, strict⟩904  have beforeNext : N < succ(N)905    unfold Less906    exact LessEqual.reflexive with nextN907  have firstBeforeSecond := strict with908    N, naturalN, succ(N), nextNatural, beforeNext909  have gap := escapingSequence.gap at S, A, k[N], k[succ(N)] with910    subset, unbounded, firstBeforeSecond911  have firstValue := subsequence.value at escapingSequence(S, A), k, N with912    sequence, increasingAgain913  have secondValue := subsequence.value at escapingSequence(S, A), k, succ(N) with914    sequence, increasingAgain915  rw firstValue at nearFirst916  rw secondValue at nearSecond917  have firstReal := RealSequence.value at escapingSequence(S, A), k[N] with sequence918  have secondReal := RealSequence.value at escapingSequence(S, A), k[succ(N)] with sequence919  have symmetric := openBall.symmetric.forward at920    escapingSequence(S, A)[k[N]], L, half(realOne) with921      firstReal, assumption, halfReal, nearFirst922  have across := openBall.triangle at923    escapingSequence(S, A)[k[succ(N)]], L,924    escapingSequence(S, A)[k[N]], half(realOne), half(realOne) with925      secondReal, assumption, firstReal, halfReal, halfReal,926      nearSecond, symmetric927  have doubled := half.add_self with realOne.real928  rw doubled at across929  obtain ⟨lower, upper⟩ := openBall.order_characterization.forward with across930  have cycle := realLess.transitive with gap, upper931  have impossible := realLess.characterization.forward with cycle932  exact RealLess.irreflexive with impossible933934theorem SequentiallyCompact.bounded_above (S : Set)935  requires compact : SequentiallyCompact(S)936  requires inhabited : Nonempty(S)937  shows ∃ B ∈ ℝ, RealUpperBound(S, B)938proof939  have notUnbounded := SequentiallyCompact.not_unbounded_above with compact, inhabited940  by_contra noBound941  have unbounded : UnboundedAbove(S)942    intros B realB943    by_contra noAbove944    have upper : RealUpperBound(S, B)945      constructor946        exact realB947      . constructor948        . rcases compact with ⟨subset, extract⟩949          exact subset950        . intros X inS951          have realX : Real(X)952            rcases compact with ⟨subset, extract⟩953            unfold Real954            exact subset with X, inS955          have typedB : Real(B) by exact realB956          have weak : X ≤ B957            by_contra notWeak958            have strict := realLess.of_not_le with notWeak959            apply noAbove960            witness X961            refine ⟨inS, strict⟩962          have view := realLe.characterization.forward with weak963          rcases view with ⟨typedX, typedB, included⟩964          exact included965    apply noBound966    witness B967    refine ⟨realB, upper⟩968  exact notUnbounded with unbounded969970-- ExtremeValue971theorem ContinuousOn.closed_interval_maximum (f : Set) (A B : Real)972  requires ordered : A ≤ B973  requires continuous : ContinuousOn(f, closedInterval(A, B))974  shows ∃ T ∈ closedInterval(A, B),975    ∀ X ∈ closedInterval(A, B),976      (f(X):R) ≤ (f(T):R)977proof978  have compact := closedInterval.continuous_image_compact with continuous979  have left := closedInterval.left_mem with ordered980  have imageLeft : f(A) ∈ realFunctionImage(f, closedInterval(A, B))981    apply realFunctionImage.membership.backward982    witness A983    refine ⟨left, rfl⟩984  have inhabited : Nonempty(realFunctionImage(f, closedInterval(A, B))) := ⟨f(A), imageLeft⟩985  obtain ⟨M, realM, upper⟩ := SequentiallyCompact.bounded_above with compact, inhabited986  exact ContinuousOn.closed_interval_maximum_of_upper_bound with ordered, continuous, upper987988theorem SequentiallyCompact.has_minimum (S : Set)989  requires compact : SequentiallyCompact(S)990  requires inhabited : Nonempty(S)991  shows ∃ U ∈ S, ∀ X ∈ S, (U:R) ≤ (X:R)992proof993  rcases compact with ⟨subset, extract⟩994  have compactAgain : SequentiallyCompact(S) by refine ⟨subset, extract⟩995  have continuous := Continuous.continuous_on with realNeg.continuous, subset996  have negativeCompact := realFunctionImage.sequentially_compact with continuous, compactAgain997  obtain ⟨A, memberA⟩ := inhabited998  have negativeA : realNeg(A) ∈ realFunctionImage(realNeg, S)999    apply realFunctionImage.membership.backward1000    witness A1001    refine ⟨memberA, rfl⟩1002  have negativeInhabited : Nonempty(realFunctionImage(realNeg, S)) := ⟨realNeg(A), negativeA⟩1003  obtain ⟨B, realB, upper⟩ := SequentiallyCompact.bounded_above with negativeCompact, negativeInhabited1004  obtain ⟨V, negativeMember, greatest⟩ := SequentiallyCompact.has_maximum_of_upper_bound with1005    negativeCompact, negativeInhabited, upper1006  obtain ⟨U, memberU, valueU⟩ := realFunctionImage.membership.forward with negativeMember1007  witness U1008  constructor1009  . exact memberU1010  . intros X memberX1011    have negativeX : realNeg(X) ∈ realFunctionImage(realNeg, S)1012      apply realFunctionImage.membership.backward1013      witness X1014      refine ⟨memberX, rfl⟩1015    have bound := greatest with realNeg(X), negativeX1016    have subsetView := subset1017    have realU : Real(U)1018      unfold Real1019      exact subsetView with U, memberU1020    have realX : Real(X)1021      unfold Real1022      exact subsetView with X, memberX1023    have boundApplied : (realNeg(X):R) ≤ (realNeg(U):R) by rwa valueU1024    have negView : -X ≤ -U1025      exact boundApplied1026    have reversed := realLe.neg_reverse at -X, -U with1027      realNegValue.real at X with realX,1028      realNegValue.real at U with realU,1029      negView1030    have involutiveU := realNegValue.involutive with realU1031    have involutiveX := realNegValue.involutive with realX1032    rwa [involutiveU, involutiveX] at reversed10331034theorem ContinuousOn.closed_interval_minimum (f : Set) (A B : Real)1035  requires ordered : A ≤ B1036  requires continuous : ContinuousOn(f, closedInterval(A, B))1037  shows ∃ T ∈ closedInterval(A, B),1038    ∀ X ∈ closedInterval(A, B),1039      (f(T):R) ≤ (f(X):R)1040proof1041  have compact := closedInterval.continuous_image_compact with continuous1042  have left := closedInterval.left_mem with ordered1043  have imageLeft : f(A) ∈ realFunctionImage(f, closedInterval(A, B))1044    apply realFunctionImage.membership.backward1045    witness A1046    refine ⟨left, rfl⟩1047  have inhabited : Nonempty(realFunctionImage(f, closedInterval(A, B))) := ⟨f(A), imageLeft⟩1048  obtain ⟨V, inImage, least⟩ := SequentiallyCompact.has_minimum with compact, inhabited1049  obtain ⟨T, inInterval, value⟩ := realFunctionImage.membership.forward with inImage1050  witness T1051  constructor1052  . exact inInterval1053  . intros X inIntervalX1054    have imageX : f(X) ∈ realFunctionImage(f, closedInterval(A, B))1055      apply realFunctionImage.membership.backward1056      witness X1057      refine ⟨inIntervalX, rfl⟩1058    have bound := least with f(X), imageX1059    rwa value1060