-- Real analysis: HeineCantor -- Part of Cumulus, the Grace17 mathematics library. -- Copyright (c) 2026 Grant Passmore. -- Released under the Apache License 2.0. See LICENSE in the repository root. -- Authors: Grant Passmore module Grace.Cumulus.Real.Analysis.HeineCantor import Set.Choice import ExtremeValue -- Section: UniformFirstWitnessGraph defchoose failureFirst (f S : Set, E : Real, n : Nat) (X ∈ ℝ) := ∃ Y ∈ ℝ, UniformFailurePair(f, S, E, dyadicRadius(n), X, Y) requires witnesses : ∀ D ∈ ℝ, (0 < D → ∃ X ∈ ℝ, ∃ Y ∈ ℝ, UniformFailurePair(f, S, E, D, X, Y)) proof have radiusReal := dyadicRadius.real at n with assumption have radiusMember : dyadicRadius(n) ∈ ℝ unfold Real at radiusReal exact radiusReal have positive := dyadicRadius.positive at n with assumption exact witnesses with dyadicRadius(n), radiusMember, positive defchoose failureSecond (f S : Set, E : Real, n : Nat) (Y ∈ ℝ) := UniformFailurePair(f, S, E, dyadicRadius(n), failureFirst(f, S, E, n), Y) requires witnesses : ∀ D ∈ ℝ, (0 < D → ∃ X ∈ ℝ, ∃ Y ∈ ℝ, UniformFailurePair(f, S, E, D, X, Y)) proof obtain ⟨firstReal, Y, realY, bad⟩ := failureFirst.selected at f, S, E, n with witnesses witness Y refine ⟨realY, bad⟩ -- UniformChoicePair theorem failureWitnesses.pair (f S : Set, E : Real, n : Nat) requires witnesses : ∀ D ∈ ℝ, (0 < D → ∃ X ∈ ℝ, ∃ Y ∈ ℝ, UniformFailurePair(f, S, E, D, X, Y)) shows failureFirst(f, S, E, n) ∈ ℝ ∧ failureSecond(f, S, E, n) ∈ ℝ ∧ UniformFailurePair(f, S, E, dyadicRadius(n), failureFirst(f, S, E, n), failureSecond(f, S, E, n)) proof have first := failureFirst.selected with witnesses have second := failureSecond.selected with witnesses rcases first with ⟨firstReal, availableSecond⟩ rcases second with ⟨secondReal, bad⟩ refine ⟨firstReal, secondReal, bad⟩ -- UniformChoice defgraph failureFirstSequence (f S : Set, E : Real) (n ∈ ℕ) : ℝ := failureFirst(f, S, E, n) requires witnesses : ∀ D ∈ ℝ, (0 < D → ∃ X ∈ ℝ, ∃ Y ∈ ℝ, UniformFailurePair(f, S, E, D, X, Y)) proof obtain ⟨realFirst, realSecond, bad⟩ := failureWitnesses.pair with witnesses exact realFirst defgraph failureSecondSequence (f S : Set, E : Real) (n ∈ ℕ) : ℝ := failureSecond(f, S, E, n) requires witnesses : ∀ D ∈ ℝ, (0 < D → ∃ X ∈ ℝ, ∃ Y ∈ ℝ, UniformFailurePair(f, S, E, D, X, Y)) proof obtain ⟨realFirst, realSecond, bad⟩ := failureWitnesses.pair with witnesses exact realSecond -- UniformFirstWitnessGraph theorem failureFirstSequence.sequence (f S : Set, E : Real) requires witnesses : ∀ D ∈ ℝ, (0 < D → ∃ X ∈ ℝ, ∃ Y ∈ ℝ, UniformFailurePair(f, S, E, D, X, Y)) shows RealSequence(failureFirstSequence(f, S, E)) proof unfold RealSequence exact failureFirstSequence.function with witnesses -- Section: HeineCantor theorem failureSecondSequence.sequence (f S : Set, E : Real) requires witnesses : ∀ D ∈ ℝ, (0 < D → ∃ X ∈ ℝ, ∃ Y ∈ ℝ, UniformFailurePair(f, S, E, D, X, Y)) shows RealSequence(failureSecondSequence(f, S, E)) proof unfold RealSequence exact failureSecondSequence.function with witnesses -- UniformWitnesses theorem failureWitnesses.properties (f S : Set, E : Real) requires witnesses : ∀ D ∈ ℝ, (0 < D → ∃ X ∈ ℝ, ∃ Y ∈ ℝ, UniformFailurePair(f, S, E, D, X, Y)) shows TermsIn(failureFirstSequence(f, S, E), S) ∧ TermsIn(failureSecondSequence(f, S, E), S) ∧ AsymptoticallyClose(failureSecondSequence(f, S, E), failureFirstSequence(f, S, E)) ∧ (∀ n ∈ ℕ, ¬(f(failureFirstSequence(f, S, E)[n]) ∈ openBall(f(failureSecondSequence(f, S, E)[n]), E))) proof constructor intros n naturalN have typedN : Nat(n) by exact nat.omega.backward at n with naturalN obtain ⟨realFirst, realSecond, bad⟩ := failureWitnesses.pair with witnesses rcases bad with ⟨memberFirst, memberSecond, near, far⟩ have value := failureFirstSequence.value with witnesses rwa value . constructor intros n naturalN have typedN : Nat(n) by exact nat.omega.backward at n with naturalN obtain ⟨realFirst, realSecond, bad⟩ := failureWitnesses.pair with witnesses rcases bad with ⟨memberFirst, memberSecond, near, far⟩ have value := failureSecondSequence.value with witnesses rwa value . constructor constructor . exact failureSecondSequence.sequence with witnesses . constructor . exact failureFirstSequence.sequence with witnesses . intros D realD positiveD obtain ⟨N, naturalN, small⟩ := dyadicRadii.eventually_below with positiveD witness N constructor . exact naturalN . intros n indexNatural afterN obtain ⟨realFirst, realSecond, bad⟩ := failureWitnesses.pair at f, S, E, n with witnesses rcases bad with ⟨memberFirst, memberSecond, near, far⟩ have radiusSmall := small with n, indexNatural, afterN have weak := realLess.implies_le with radiusSmall have enlarged := openBall.mono with near, weak have firstValue := failureFirstSequence.value at f, S, E, n with witnesses have secondValue := failureSecondSequence.value at f, S, E, n with witnesses rwa [firstValue, secondValue] . intros n naturalN obtain ⟨realFirst, realSecond, bad⟩ := failureWitnesses.pair at f, S, E, n with witnesses rcases bad with ⟨memberFirst, memberSecond, near, far⟩ have firstValue := failureFirstSequence.value at f, S, E, n with witnesses have secondValue := failureSecondSequence.value at f, S, E, n with witnesses rwa [firstValue, secondValue] -- CompactUniformContinuity theorem ContinuousOn.uniform_of_sequentially_compact (f S : Set) requires continuous : ContinuousOn(f, S) requires compact : SequentiallyCompact(S) shows UniformContinuousOn(f, S) proof by_contra notUniform obtain ⟨E, realE, positiveE, witnesses⟩ := ContinuousOn.nonuniform_pairs with continuous, notUniform obtain ⟨termsFirst, termsSecond, close, far⟩ := failureWitnesses.properties with witnesses have sequenceSecond := failureSecondSequence.sequence with witnesses obtain ⟨k, increasing, L, realL, memberL, mapsSecond, mapsFirst⟩ := ContinuousOn.nearby_compact_images with continuous, compact, sequenceSecond, termsSecond, termsFirst, close have function : f : ℝ → ℝ rcases continuous with ⟨function, subset, atPoints⟩ exact function obtain ⟨N, naturalN, near⟩ := ConvergesTo.eventually_near_each_other with mapsSecond, mapsFirst, positiveE have typedN : Nat(N) by exact nat.omega.backward at N with naturalN have afterN := LessEqual.reflexive with typedN have selectedNear := near with N, naturalN, afterN have selectedSecondSequence := subsequence.sequence with sequenceSecond, increasing have sequenceFirst := failureFirstSequence.sequence with witnesses have selectedFirstSequence := subsequence.sequence with sequenceFirst, increasing have mappedSecond := compose.apply at f, subsequence(failureSecondSequence(f, S, E), k), ℕ, ℝ, ℝ, N with selectedSecondSequence, function, naturalN have mappedFirst := compose.apply at f, subsequence(failureFirstSequence(f, S, E), k), ℕ, ℝ, ℝ, N with selectedFirstSequence, function, naturalN rw [mappedFirst, mappedSecond] at selectedNear have chosenSecond := subsequence.value with sequenceSecond, increasing have chosenFirst := subsequence.value with sequenceFirst, increasing rw [chosenFirst, chosenSecond] at selectedNear have selectorFunction := StrictlyIncreasingNat.function with increasing have selectedNatural := FunctionBetween.apply_closed with selectorFunction, naturalN have contradiction := far with k[N], selectedNatural exact contradiction with selectedNear -- HeineCantor theorem closedInterval.heine_cantor (f : Set, A B : Real) requires continuous : ContinuousOn(f, closedInterval(A, B)) shows UniformContinuousOn(f, closedInterval(A, B)) proof have compact := closedInterval.sequentially_compact at A, B with *{2} exact ContinuousOn.uniform_of_sequentially_compact with continuous, compact -- Section: DomainSequentialContinuity predicate RealFunctionOn (f S : Set) := ∃ D, D ⊆ ℝ ∧ S ⊆ D ∧ FunctionBetween(f, D, ℝ) predicate ContinuousWithinDomainAt (f S : Set) (A : Real) := RealFunctionOn(f, S) ∧ S ⊆ ℝ ∧ A ∈ S ∧ (∀ E ∈ ℝ, 0 < E → ∃ D ∈ ℝ, 0 < D ∧ ∀ X ∈ ℝ, (X ∈ S → (X ∈ openBall(A, D) → f(X) ∈ openBall(f(A), E)))) predicate ContinuousOnDomain (f S : Set) := RealFunctionOn(f, S) ∧ S ⊆ ℝ ∧ (∀ A ∈ S, ContinuousWithinDomainAt(f, S, A)) predicate UniformContinuousOnDomain (f S : Set) := RealFunctionOn(f, S) ∧ S ⊆ ℝ ∧ (∀ E ∈ ℝ, 0 < E → ∃ D ∈ ℝ, 0 < D ∧ ∀ X ∈ ℝ, (X ∈ S → ∀ Y ∈ ℝ, (Y ∈ S → (X ∈ openBall(Y, D) → f(X) ∈ openBall(f(Y), E))))) theorem RealFunctionOn.of_function_between (f D S : Set) requires function : f : D → ℝ requires domainReal : D ⊆ ℝ requires subset : S ⊆ D shows RealFunctionOn(f, S) proof witness D refine ⟨domainReal, subset, function⟩ theorem RealFunctionOn.apply_real (f S : Set, X : Real) requires function : RealFunctionOn(f, S) requires member : X ∈ S shows Real(f(X)) proof rcases function with ⟨D, domainReal, subset, graphFunction⟩ have memberD := subset with X, member exact FunctionBetween.apply_closed with graphFunction, memberD theorem ContinuousOn.domain (f S : Set) requires continuous : ContinuousOn(f, S) shows ContinuousOnDomain(f, S) proof rcases continuous with ⟨function, subset, atPoints⟩ have realFunction : RealFunctionOn(f, S) exact RealFunctionOn.of_function_between at f, ℝ, S with function, Subset.reflexive at ℝ, subset unfold ContinuousOnDomain refine ⟨realFunction, subset, _⟩ intros A member obtain ⟨functionAt, subsetAt, control⟩ := atPoints with A, member have typedA : Real(A) have realA := subset with A, member unfold Real exact realA unfold ContinuousWithinDomainAt refine ⟨realFunction, subset, member, control⟩ theorem UniformContinuousOn.domain (f S : Set) requires uniform : UniformContinuousOn(f, S) shows UniformContinuousOnDomain(f, S) proof rcases uniform with ⟨function, subset, control⟩ have realFunction : RealFunctionOn(f, S) exact RealFunctionOn.of_function_between at f, ℝ, S with function, Subset.reflexive at ℝ, subset unfold UniformContinuousOnDomain refine ⟨realFunction, subset, control⟩ -- A graph with domain S is admitted directly; no extension to all -- of ℝ is needed, even when S is a closed interval. theorem constantFunction.continuous_on_domain (S : Set) (L : Real) requires subset : S ⊆ ℝ shows ContinuousOnDomain(constantFunction(S, ℝ, L), S) proof have realL : L ∈ ℝ by simp [Real] have function := constantFunction.function at S, ℝ, L with realL have realFunction := RealFunctionOn.of_function_between at constantFunction(S, ℝ, L), S, S with function, subset, Subset.reflexive at S unfold ContinuousOnDomain refine ⟨realFunction, subset, _⟩ intros A memberA have realA : Real(A) have inReals := subset with A, memberA unfold Real exact inReals unfold ContinuousWithinDomainAt refine ⟨realFunction, subset, memberA, _⟩ intros E realE positive witness E refine ⟨realE, positive, _⟩ intros X realX memberX near have valueX := constantFunction.apply with memberX, realL have valueA := constantFunction.apply with memberA, realL rw [valueX, valueA] exact openBall.center with positive -- DomainSequentialContinuity theorem ContinuousWithinDomainAt.converges_in (f u S D : Set) (L : Real) requires continuous : ContinuousWithinDomainAt(f, S, L) requires function : f : D → ℝ requires subset : S ⊆ D requires converges : ConvergesTo(u, L) requires terms : TermsIn(u, S) shows ConvergesTo(compose(f, u, ℕ, D, ℝ), f(L)) proof rcases continuous with ⟨domainFunction, subsetReal, memberL, control⟩ have sequence := ConvergesTo.sequence with converges unfold RealSequence at sequence have values : ∀ j ∈ ℕ, u(j) ∈ D intros j naturalJ have termS := terms with j, naturalJ exact subset with u(j), termS have sequenceD := FunctionBetween.codomain_of_values with sequence, values have limitD : L ∈ D by exact subset with L, memberL have imageReal := FunctionBetween.apply_closed with function, limitD constructor . unfold RealSequence exact compose.function with sequenceD, function . intros E realE positive obtain ⟨R, realR, positiveR, maps⟩ := control with E, realE, positive obtain ⟨N, naturalN, close⟩ := ConvergesTo.eventually with converges, positiveR witness N constructor . exact naturalN . intros n indexNatural afterN have termReal := FunctionBetween.apply_closed with sequence, indexNatural have member := terms with n, indexNatural have near := close with n, indexNatural, afterN have mapped := maps with u(n), termReal, member, near have value : compose(f, u, ℕ, D, ℝ)(n) = f(u(n)) exact compose.apply with sequenceD, function, indexNatural rwa value theorem ContinuousOnDomain.converges_in (f u S D : Set) (L : Real) requires continuous : ContinuousOnDomain(f, S) requires function : f : D → ℝ requires subset : S ⊆ D requires limitMember : L ∈ S requires converges : ConvergesTo(u, L) requires terms : TermsIn(u, S) shows ConvergesTo(compose(f, u, ℕ, D, ℝ), f(L)) proof rcases continuous with ⟨domainFunction, subsetReal, atPoints⟩ have atLimit := atPoints with L, limitMember exact ContinuousWithinDomainAt.converges_in with atLimit, function, subset, converges, terms theorem ContinuousOnDomain.nearby_compact_images (f S D u v : Set) requires continuous : ContinuousOnDomain(f, S) requires function : f : D → ℝ requires subset : S ⊆ D requires compact : SequentiallyCompact(S) requires sequence : RealSequence(u) requires termsU : TermsIn(u, S) requires termsV : TermsIn(v, S) requires close : AsymptoticallyClose(u, v) shows ∃ k, StrictlyIncreasingNat(k) ∧ ∃ L ∈ ℝ, L ∈ S ∧ ConvergesTo(compose(f, subsequence(u, k), ℕ, D, ℝ), f(L)) ∧ ConvergesTo(compose(f, subsequence(v, k), ℕ, D, ℝ), f(L)) proof obtain ⟨k, increasing, L, realL, member, convergesU, convergesV⟩ := SequentiallyCompact.nearby_subsequences with compact, sequence, termsU, close have selectedU := TermsIn.subsequence with sequence, termsU, increasing rcases close with ⟨sequenceAgain, sequenceV, eventually⟩ have selectedV := TermsIn.subsequence with sequenceV, termsV, increasing have mappedU := ContinuousOnDomain.converges_in with continuous, function, subset, member, convergesU, selectedU have mappedV := ContinuousOnDomain.converges_in with continuous, function, subset, member, convergesV, selectedV witness k constructor . exact increasing . witness L refine ⟨realL, member, mappedU, mappedV⟩ -- Section: DomainHeineCantor theorem ContinuousOnDomain.nonuniform_tolerance (f S : Set) requires continuous : ContinuousOnDomain(f, S) requires notUniform : ¬UniformContinuousOnDomain(f, S) shows ∃ E ∈ ℝ, (0 < E ∧ ∀ D ∈ ℝ, (0 < D → ¬(∀ X ∈ ℝ, (X ∈ S → ∀ Y ∈ ℝ, (Y ∈ S → (X ∈ openBall(Y, D) → f(X) ∈ openBall(f(Y), E))))))) proof rcases continuous with ⟨function, subset, atPoints⟩ by_contra noTolerance apply notUniform constructor . exact function . constructor . exact subset . intros E realE positive have radiusExists : ∃ D ∈ ℝ, (0 < D ∧ ∀ X ∈ ℝ, (X ∈ S → ∀ Y ∈ ℝ, (Y ∈ S → (X ∈ openBall(Y, D) → f(X) ∈ openBall(f(Y), E))))) by_contra noRadius apply noTolerance witness E constructor . exact realE . constructor . exact positive . intros D realD positiveD maps apply noRadius witness D refine ⟨realD, positiveD, maps⟩ exact radiusExists -- This is the textbook epsilon that defeats every delta, with the real -- witnesses and interval membership written out. theorem ContinuousOnDomain.nonuniform_pairs (f S : Set) requires continuous : ContinuousOnDomain(f, S) requires notUniform : ¬UniformContinuousOnDomain(f, S) shows ∃ E ∈ ℝ, (0 < E ∧ ∀ D ∈ ℝ, (0 < D → ∃ X ∈ ℝ, ∃ Y ∈ ℝ, UniformFailurePair(f, S, E, D, X, Y))) proof obtain ⟨E, realE, positiveE, noRadius⟩ := ContinuousOnDomain.nonuniform_tolerance with continuous, notUniform witness E constructor . exact realE . constructor . exact positiveE . intros D realD positiveD have noMaps := noRadius with D, realD, positiveD have bad : ∃ X ∈ ℝ, ∃ Y ∈ ℝ, ( X ∈ S ∧ Y ∈ S ∧ X ∈ openBall(Y, D) ∧ ¬(f(X) ∈ openBall(f(Y), E))) by_contra noBad apply noMaps intros P realP memberP Q realQ memberQ near by_contra notNear apply noBad witness P constructor . exact realP . witness Q refine ⟨realQ, memberP, memberQ, near, notNear⟩ obtain ⟨X, realX, Y, realY, memberX, memberY, near, far⟩ := bad witness X constructor . exact realX . witness Y constructor . exact realY . unfold UniformFailurePair refine ⟨memberX, memberY, near, far⟩ -- DomainHeineCantor theorem ContinuousOnDomain.uniform_of_sequentially_compact (f S : Set) requires continuous : ContinuousOnDomain(f, S) requires compact : SequentiallyCompact(S) shows UniformContinuousOnDomain(f, S) proof by_contra notUniform obtain ⟨E, realE, positiveE, witnesses⟩ := ContinuousOnDomain.nonuniform_pairs with continuous, notUniform have continuousAgain := continuous rcases continuous with ⟨domainFunction, subsetReal, atPoints⟩ rcases domainFunction with ⟨D, domainReal, subset, graphFunction⟩ obtain ⟨termsFirst, termsSecond, close, far⟩ := failureWitnesses.properties with witnesses have sequenceSecond := failureSecondSequence.sequence with witnesses obtain ⟨k, increasing, L, realL, memberL, mapsSecond, mapsFirst⟩ := ContinuousOnDomain.nearby_compact_images with continuousAgain, graphFunction, subset, compact, sequenceSecond, termsSecond, termsFirst, close have function : f : D → ℝ by exact graphFunction have memberD : L ∈ D by exact subset with L, memberL have mappedReal : Real(f(L)) have realImage := FunctionBetween.apply_closed with function, memberD unfold Real exact realImage obtain ⟨N, naturalN, near⟩ := ConvergesTo.eventually_near_each_other with mapsSecond, mapsFirst, positiveE have typedN : Nat(N) by exact nat.omega.backward at N with naturalN have afterN := LessEqual.reflexive with typedN have selectedNear := near with N, naturalN, afterN have selectedSecondSequence := subsequence.sequence with sequenceSecond, increasing have termsSelectedSecond := TermsIn.subsequence with sequenceSecond, termsSecond, increasing have secondValues : ∀ j ∈ ℕ, subsequence(failureSecondSequence(f, S, E), k)(j) ∈ D intros j naturalJ have memberS := termsSelectedSecond with j, naturalJ exact subset with subsequence(failureSecondSequence(f, S, E), k)(j), memberS unfold RealSequence at selectedSecondSequence have selectedSecondDomain := FunctionBetween.codomain_of_values with selectedSecondSequence, secondValues have sequenceFirst := failureFirstSequence.sequence with witnesses have selectedFirstSequence := subsequence.sequence with sequenceFirst, increasing have termsSelectedFirst := TermsIn.subsequence with sequenceFirst, termsFirst, increasing have firstValues : ∀ j ∈ ℕ, subsequence(failureFirstSequence(f, S, E), k)(j) ∈ D intros j naturalJ have memberS := termsSelectedFirst with j, naturalJ exact subset with subsequence(failureFirstSequence(f, S, E), k)(j), memberS unfold RealSequence at selectedFirstSequence have selectedFirstDomain := FunctionBetween.codomain_of_values with selectedFirstSequence, firstValues have mappedSecond := compose.apply with selectedSecondDomain, function, naturalN have mappedFirst := compose.apply with selectedFirstDomain, function, naturalN rw [mappedFirst, mappedSecond] at selectedNear have chosenSecond := subsequence.value with sequenceSecond, increasing have chosenFirst := subsequence.value with sequenceFirst, increasing rw [chosenFirst, chosenSecond] at selectedNear have selectorFunction := StrictlyIncreasingNat.function with increasing have selectedNatural := FunctionBetween.apply_closed with selectorFunction, naturalN have contradiction := far with k[N], selectedNatural exact contradiction with selectedNear theorem closedInterval.heine_cantor_on_domain (f : Set, A B : Real) requires continuous : ContinuousOnDomain(f, closedInterval(A, B)) shows UniformContinuousOnDomain(f, closedInterval(A, B)) proof have compact := closedInterval.sequentially_compact at A, B with *{2} exact ContinuousOnDomain.uniform_of_sequentially_compact with continuous, compact