Grace/Cumulus/Topology/Real/PerfectSets.g17

Open in Workbench Download source

Imports

NestedChoice · CantorBendixson

Declarations

Source

1-- Perfect sets of reals are uncountable: Cantor's nested intervals keep2-- out every point of a would-be enumeration, so a closed set of reals is3-- countable or contains an uncountable perfect set4-- Part of Cumulus, the Grace17 mathematics library.5-- Copyright (c) 2026 Grant Passmore.6-- Released under the Apache License 2.0. See LICENSE in the repository root.7-- Authors: Grant Passmore89module Grace.Cumulus.Topology.Real.PerfectSets10import NestedChoice11import CantorBendixson1213-- Section: Steps14-- Every ball around a point of a perfect set meets the set elsewhere.15theorem Perfect.ball_meets (P : Set) (C E : Real)16  requires perfect : Perfect(ℝ, realTopology, P)17  requires hC : C ∈ P18  requires positive : 0 < E19  shows ∃ D ∈ P, D ∈ openBall(C, E) ∧ D ≠ C20proof21  obtain ⟨closed, fixed⟩ := perfect22  have limit : C ∈ derivedSet(ℝ, realTopology, P)23    rw fixed24    exact hC25  have parts := derivedSet.membership.forward with limit26  have ballOpen := openBall.open at C, E27  have center := openBall.center at C, E with positive28  obtain ⟨D, hD⟩ := parts.right with openBall(C, E), ballOpen, center29  have both := intersection.membership.forward with hD30  have away := difference.membership.forward with both.right31  witness D32  refine ⟨away.left, both.left, ?_⟩33  intro same34  apply away.right35  rw same36  exact singleton.self at C3738-- Near any point of a perfect set there is a point of the set that no39-- point of code n equals: the point itself unless its code is n, and40-- then another point of the ball.41theorem Perfect.free_centre (P f : Set, n : Nat) (C E : Real)42  requires perfect : Perfect(ℝ, realTopology, P)43  requires injective : InjectiveBetween(f, P, ℕ)44  requires hC : C ∈ P45  requires positive : 0 < E46  shows ∃ D ∈ P, D ∈ openBall(C, E) ∧47    (∀ y ∈ P, f(y) = n → y ≠ D)48proof49  have split : f(C) = n ∨ f(C) ≠ n by tauto50  cases split with coded | free51  . obtain ⟨D, hD, near, distinct⟩ :=52      Perfect.ball_meets with perfect, hC, positive53    witness D54    refine ⟨hD, near, ?_⟩55    intros y hy code same56    have sameCode : f(y) = f(C)57      rw [code, coded]58      rfl59    have equal := Injective.apply_cancel with injective, hy, hC, sameCode60    rw same at equal61    exact distinct with equal62  . have center := openBall.center at C, E with positive63    witness C64    refine ⟨hC, center, ?_⟩65    intros y hy code same66    apply free67    rw ← same68    exact code6970-- A positive radius below the distance from D to the point of code n.71theorem Injective.free_radius (P f : Set, n : Nat) (D : Real)72  requires injective : InjectiveBetween(f, P, ℕ)73  requires subset : P ⊆ ℝ74  requires free : ∀ y ∈ P, f(y) = n → y ≠ D75  shows ∃ R ∈ ℝ, 0 < R ∧ (∀ y ∈ P, f(y) = n → R < dist(y, D))76proof77  have split : (∃ p ∈ P, f(p) = n) ∨ ¬(∃ p ∈ P, f(p) = n) by tauto78  cases split with coded | none79  . obtain ⟨p, hp, code⟩ := coded80    have realP := subset with p, hp81    have distinct := free with p, hp, code82    have positive := dist.positive_of_ne with distinct83    have halfPositive := half.positive with positive84    have halfLess := half.lt_self with positive85    have halfReal : half(dist(p, D)) ∈ ℝ by typecheck86    witness half(dist(p, D))87    refine ⟨halfReal, halfPositive, ?_⟩88    intros y hy codeY89    have sameCode : f(y) = f(p)90      rw [codeY, code]91      rfl92    have equal := Injective.apply_cancel with injective, hy, hp, sameCode93    rw equal94    exact halfLess95  . have one : (1:R) ∈ ℝ by typecheck96    have positive : (0:R) < 1 by linarith97    witness (1:R)98    refine ⟨one, positive, ?_⟩99    intros y hy code100    exfalso101    apply none102    exact ⟨y, hy, code⟩103104-- Inside any interval around a point of a perfect set there is a105-- candidate of stage n: an interval around a point of the set, as small106-- as stage n asks, keeping out the point of code n.107theorem Perfect.shrink_candidate (P f I : Set, n : Nat) (C E : Real)108  requires perfect : Perfect(ℝ, realTopology, P)109  requires injective : InjectiveBetween(f, P, ℕ)110  requires hC : C ∈ P111  requires positive : 0 < E112  requires inside : centeredInterval(C, E) ⊆ I113  shows Nonempty(shrinkCandidates(P, f, I, n))114proof115  have subset : P ⊆ ℝ := perfect.left.left116  obtain ⟨D, hD, near, free⟩ :=117    Perfect.free_centre with perfect, injective, hC, positive118  have realD := subset with D, hD119  obtain ⟨R1, realR1, positive1, apart⟩ :=120    Injective.free_radius with injective, subset, free121  obtain ⟨realD2, close⟩ := openBall.membership.forward with near122  have distReal := dist.real at D, C123  have gapReal : E - dist(D, C) ∈ ℝ by typecheck124  have gapPositive : (0:R) < E - dist(D, C) by linarith125  have sequence := harmonicTerms.sequence126  have termReal := RealSequence.value at harmonicTerms, n with sequence127  have termPositive := harmonicTerms.positive at n128  obtain ⟨R2, realR2, positive2, leApart, leGap⟩ :=129    positiveRadius.common with positive1, gapPositive130  obtain ⟨R, realR, positiveR, leR2, leTerm⟩ :=131    positiveRadius.common with positive2, termPositive132  have nested : centeredInterval(D, R) ⊆ centeredInterval(C, E)133    apply centeredInterval.nested134    linarith135  have insideI := Subset.transitive with nested, inside136  have avoids : ∀ y ∈ P, y ∈ centeredInterval(D, R) → f(y) ≠ n137    intros y hy hIn code138    obtain ⟨realY, within⟩ :=139      centeredInterval.dist_membership.forward with hIn140    have far := apart with y, hy, code141    have distYD := dist.real at y, D142    linarith143  witness (D, R)144  exact shrinkCandidates.pair with hD, positiveR, leTerm, insideI, avoids145146-- The step hypotheses of the shrinking hold for a nonempty perfect set.147theorem Perfect.shrink_steps (P f : Set)148  requires perfect : Perfect(ℝ, realTopology, P)149  requires injective : InjectiveBetween(f, P, ℕ)150  requires nonempty : Nonempty(P)151  shows ShrinkSteps(P, f)152proof153  have subset : P ⊆ ℝ := perfect.left.left154  constructor155  . obtain ⟨C, hC⟩ := nonempty156    have realC := subset with C, hC157    have one : (0:R) < 1 by linarith158    have inside := centeredInterval.subset_reals at C, (1:R)159    exact Perfect.shrink_candidate at P, f, ℝ, 0, C, (1:R) with160      perfect, injective, hC, one, inside161  . intros n hn C hC E hE positive162    have typedN := nat.omega.backward with hn163    have realC := subset with C, hC164    have reflexive := Subset.reflexive at centeredInterval(C, E)165    exact Perfect.shrink_candidate at166      P, f, centeredInterval(C, E), succ(n), C, E with167        perfect, injective, hC, positive, reflexive168169-- Section: Uncountable170-- A nonempty perfect set of reals is uncountable: an injection into ℕ171-- would let the stages keep out every point of the set, yet their common172-- point lies in the closed set P, since the centres are points of P that173-- come arbitrarily close to it.174theorem perfect.uncountable (P : Set)175  requires perfect : Perfect(ℝ, realTopology, P)176  requires nonempty : Nonempty(P)177  shows ¬Countable(P)178proof179  intro countable180  obtain ⟨f, injective⟩ := countable181  obtain ⟨c, choice⟩ := SubsetChoice.exists at ℝ × ℝ182  have steps := Perfect.shrink_steps with perfect, injective, nonempty183  have function : f : P → ℕ := injective.left184  obtain ⟨L, realL, inside⟩ := shrink.common_point with choice, steps185  have outside := shrink.escapes with function, choice, steps, inside186  obtain ⟨closed, fixed⟩ := perfect187  have inComplement : L ∈ complement(ℝ, P) :=188    complement.membership.backward with ⟨realL, outside⟩189  have parts := realTopology.membership.forward with closed.right190  obtain ⟨E, realE, positive, ballOutside⟩ :=191    parts.right with L, inComplement192  obtain ⟨n, hn, small⟩ := harmonicTerms.below with positive193  have typedN := nat.omega.backward with hn194  have centreIn := shrinkCentre.member at P, f, c, n with choice, steps195  have realCentre := shrinkCentre.real at P, f, c, n with choice, steps196  have realRadius := shrinkRadius.real at P, f, c, n with choice, steps197  have bound := shrinkRadius.small at P, f, c, n with choice, steps198  have sequence := harmonicTerms.sequence199  have termReal := RealSequence.value at harmonicTerms, n with sequence200  have atStage := inside with n, hn201  have centered := shrinkInterval.centered at P, f, c, n202  rw centered at atStage203  obtain ⟨realL2, lower, upper⟩ :=204    centeredInterval.membership.forward with atStage205  have near : shrinkCentre(P, f, c, n) ∈ openBall(L, E)206    apply openBall.order_characterization.backward207    constructor208    . linarith209    . linarith210  have out := ballOutside with shrinkCentre(P, f, c, n), near211  have parts2 := complement.membership.forward with out212  exact parts2.right with centreIn213214-- The perfect kernel of a closed set of reals is empty or uncountable.215theorem reals.kernel_uncountable (A : Set)216  requires closed : IsClosed(ℝ, realTopology, A)217  requires nonempty : Nonempty(perfectKernel(ℝ, realTopology, A))218  shows ¬Countable(perfectKernel(ℝ, realTopology, A))219proof220  have perfect := reals.kernel_perfect with closed221  exact perfect.uncountable with perfect, nonempty222223-- Cantor's picture of the closed sets of reals: countable, or containing224-- a nonempty perfect set, which is uncountable.225theorem closed.countable_or_uncountable_perfect (A : Set)226  requires closed : IsClosed(ℝ, realTopology, A)227  shows Countable(A) ∨228    (∃ P, Nonempty(P) ∧ Perfect(ℝ, realTopology, P) ∧ P ⊆ A ∧229      ¬Countable(P))230proof231  have split := closed.countable_or_perfect_part with closed232  cases split with countable | perfectPart233  . left234    exact countable235  . right236    obtain ⟨P, nonempty, perfect, inside⟩ := perfectPart237    have uncountable := perfect.uncountable with perfect, nonempty238    exact ⟨P, nonempty, perfect, inside, uncountable⟩239