-- Perfect sets of reals are uncountable: Cantor's nested intervals keep
-- out every point of a would-be enumeration, so a closed set of reals is
-- countable or contains an uncountable perfect set
-- 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.Topology.Real.PerfectSets
import NestedChoice
import CantorBendixson

-- Section: Steps
-- Every ball around a point of a perfect set meets the set elsewhere.
theorem Perfect.ball_meets (P : Set) (C E : Real)
  requires perfect : Perfect(ℝ, realTopology, P)
  requires hC : C ∈ P
  requires positive : 0 < E
  shows ∃ D ∈ P, D ∈ openBall(C, E) ∧ D ≠ C
proof
  obtain ⟨closed, fixed⟩ := perfect
  have limit : C ∈ derivedSet(ℝ, realTopology, P)
    rw fixed
    exact hC
  have parts := derivedSet.membership.forward with limit
  have ballOpen := openBall.open at C, E
  have center := openBall.center at C, E with positive
  obtain ⟨D, hD⟩ := parts.right with openBall(C, E), ballOpen, center
  have both := intersection.membership.forward with hD
  have away := difference.membership.forward with both.right
  witness D
  refine ⟨away.left, both.left, ?_⟩
  intro same
  apply away.right
  rw same
  exact singleton.self at C

-- Near any point of a perfect set there is a point of the set that no
-- point of code n equals: the point itself unless its code is n, and
-- then another point of the ball.
theorem Perfect.free_centre (P f : Set, n : Nat) (C E : Real)
  requires perfect : Perfect(ℝ, realTopology, P)
  requires injective : InjectiveBetween(f, P, ℕ)
  requires hC : C ∈ P
  requires positive : 0 < E
  shows ∃ D ∈ P, D ∈ openBall(C, E) ∧
    (∀ y ∈ P, f(y) = n → y ≠ D)
proof
  have split : f(C) = n ∨ f(C) ≠ n by tauto
  cases split with coded | free
  . obtain ⟨D, hD, near, distinct⟩ :=
      Perfect.ball_meets with perfect, hC, positive
    witness D
    refine ⟨hD, near, ?_⟩
    intros y hy code same
    have sameCode : f(y) = f(C)
      rw [code, coded]
      rfl
    have equal := Injective.apply_cancel with injective, hy, hC, sameCode
    rw same at equal
    exact distinct with equal
  . have center := openBall.center at C, E with positive
    witness C
    refine ⟨hC, center, ?_⟩
    intros y hy code same
    apply free
    rw ← same
    exact code

-- A positive radius below the distance from D to the point of code n.
theorem Injective.free_radius (P f : Set, n : Nat) (D : Real)
  requires injective : InjectiveBetween(f, P, ℕ)
  requires subset : P ⊆ ℝ
  requires free : ∀ y ∈ P, f(y) = n → y ≠ D
  shows ∃ R ∈ ℝ, 0 < R ∧ (∀ y ∈ P, f(y) = n → R < dist(y, D))
proof
  have split : (∃ p ∈ P, f(p) = n) ∨ ¬(∃ p ∈ P, f(p) = n) by tauto
  cases split with coded | none
  . obtain ⟨p, hp, code⟩ := coded
    have realP := subset with p, hp
    have distinct := free with p, hp, code
    have positive := dist.positive_of_ne with distinct
    have halfPositive := half.positive with positive
    have halfLess := half.lt_self with positive
    have halfReal : half(dist(p, D)) ∈ ℝ by typecheck
    witness half(dist(p, D))
    refine ⟨halfReal, halfPositive, ?_⟩
    intros y hy codeY
    have sameCode : f(y) = f(p)
      rw [codeY, code]
      rfl
    have equal := Injective.apply_cancel with injective, hy, hp, sameCode
    rw equal
    exact halfLess
  . have one : (1:R) ∈ ℝ by typecheck
    have positive : (0:R) < 1 by linarith
    witness (1:R)
    refine ⟨one, positive, ?_⟩
    intros y hy code
    exfalso
    apply none
    exact ⟨y, hy, code⟩

-- Inside any interval around a point of a perfect set there is a
-- candidate of stage n: an interval around a point of the set, as small
-- as stage n asks, keeping out the point of code n.
theorem Perfect.shrink_candidate (P f I : Set, n : Nat) (C E : Real)
  requires perfect : Perfect(ℝ, realTopology, P)
  requires injective : InjectiveBetween(f, P, ℕ)
  requires hC : C ∈ P
  requires positive : 0 < E
  requires inside : centeredInterval(C, E) ⊆ I
  shows Nonempty(shrinkCandidates(P, f, I, n))
proof
  have subset : P ⊆ ℝ := perfect.left.left
  obtain ⟨D, hD, near, free⟩ :=
    Perfect.free_centre with perfect, injective, hC, positive
  have realD := subset with D, hD
  obtain ⟨R1, realR1, positive1, apart⟩ :=
    Injective.free_radius with injective, subset, free
  obtain ⟨realD2, close⟩ := openBall.membership.forward with near
  have distReal := dist.real at D, C
  have gapReal : E - dist(D, C) ∈ ℝ by typecheck
  have gapPositive : (0:R) < E - dist(D, C) by linarith
  have sequence := harmonicTerms.sequence
  have termReal := RealSequence.value at harmonicTerms, n with sequence
  have termPositive := harmonicTerms.positive at n
  obtain ⟨R2, realR2, positive2, leApart, leGap⟩ :=
    positiveRadius.common with positive1, gapPositive
  obtain ⟨R, realR, positiveR, leR2, leTerm⟩ :=
    positiveRadius.common with positive2, termPositive
  have nested : centeredInterval(D, R) ⊆ centeredInterval(C, E)
    apply centeredInterval.nested
    linarith
  have insideI := Subset.transitive with nested, inside
  have avoids : ∀ y ∈ P, y ∈ centeredInterval(D, R) → f(y) ≠ n
    intros y hy hIn code
    obtain ⟨realY, within⟩ :=
      centeredInterval.dist_membership.forward with hIn
    have far := apart with y, hy, code
    have distYD := dist.real at y, D
    linarith
  witness (D, R)
  exact shrinkCandidates.pair with hD, positiveR, leTerm, insideI, avoids

-- The step hypotheses of the shrinking hold for a nonempty perfect set.
theorem Perfect.shrink_steps (P f : Set)
  requires perfect : Perfect(ℝ, realTopology, P)
  requires injective : InjectiveBetween(f, P, ℕ)
  requires nonempty : Nonempty(P)
  shows ShrinkSteps(P, f)
proof
  have subset : P ⊆ ℝ := perfect.left.left
  constructor
  . obtain ⟨C, hC⟩ := nonempty
    have realC := subset with C, hC
    have one : (0:R) < 1 by linarith
    have inside := centeredInterval.subset_reals at C, (1:R)
    exact Perfect.shrink_candidate at P, f, ℝ, 0, C, (1:R) with
      perfect, injective, hC, one, inside
  . intros n hn C hC E hE positive
    have typedN := nat.omega.backward with hn
    have realC := subset with C, hC
    have reflexive := Subset.reflexive at centeredInterval(C, E)
    exact Perfect.shrink_candidate at
      P, f, centeredInterval(C, E), succ(n), C, E with
        perfect, injective, hC, positive, reflexive

-- Section: Uncountable
-- A nonempty perfect set of reals is uncountable: an injection into ℕ
-- would let the stages keep out every point of the set, yet their common
-- point lies in the closed set P, since the centres are points of P that
-- come arbitrarily close to it.
theorem perfect.uncountable (P : Set)
  requires perfect : Perfect(ℝ, realTopology, P)
  requires nonempty : Nonempty(P)
  shows ¬Countable(P)
proof
  intro countable
  obtain ⟨f, injective⟩ := countable
  obtain ⟨c, choice⟩ := SubsetChoice.exists at ℝ × ℝ
  have steps := Perfect.shrink_steps with perfect, injective, nonempty
  have function : f : P → ℕ := injective.left
  obtain ⟨L, realL, inside⟩ := shrink.common_point with choice, steps
  have outside := shrink.escapes with function, choice, steps, inside
  obtain ⟨closed, fixed⟩ := perfect
  have inComplement : L ∈ complement(ℝ, P) :=
    complement.membership.backward with ⟨realL, outside⟩
  have parts := realTopology.membership.forward with closed.right
  obtain ⟨E, realE, positive, ballOutside⟩ :=
    parts.right with L, inComplement
  obtain ⟨n, hn, small⟩ := harmonicTerms.below with positive
  have typedN := nat.omega.backward with hn
  have centreIn := shrinkCentre.member at P, f, c, n with choice, steps
  have realCentre := shrinkCentre.real at P, f, c, n with choice, steps
  have realRadius := shrinkRadius.real at P, f, c, n with choice, steps
  have bound := shrinkRadius.small at P, f, c, n with choice, steps
  have sequence := harmonicTerms.sequence
  have termReal := RealSequence.value at harmonicTerms, n with sequence
  have atStage := inside with n, hn
  have centered := shrinkInterval.centered at P, f, c, n
  rw centered at atStage
  obtain ⟨realL2, lower, upper⟩ :=
    centeredInterval.membership.forward with atStage
  have near : shrinkCentre(P, f, c, n) ∈ openBall(L, E)
    apply openBall.order_characterization.backward
    constructor
    . linarith
    . linarith
  have out := ballOutside with shrinkCentre(P, f, c, n), near
  have parts2 := complement.membership.forward with out
  exact parts2.right with centreIn

-- The perfect kernel of a closed set of reals is empty or uncountable.
theorem reals.kernel_uncountable (A : Set)
  requires closed : IsClosed(ℝ, realTopology, A)
  requires nonempty : Nonempty(perfectKernel(ℝ, realTopology, A))
  shows ¬Countable(perfectKernel(ℝ, realTopology, A))
proof
  have perfect := reals.kernel_perfect with closed
  exact perfect.uncountable with perfect, nonempty

-- Cantor's picture of the closed sets of reals: countable, or containing
-- a nonempty perfect set, which is uncountable.
theorem closed.countable_or_uncountable_perfect (A : Set)
  requires closed : IsClosed(ℝ, realTopology, A)
  shows Countable(A) ∨
    (∃ P, Nonempty(P) ∧ Perfect(ℝ, realTopology, P) ∧ P ⊆ A ∧
      ¬Countable(P))
proof
  have split := closed.countable_or_perfect_part with closed
  cases split with countable | perfectPart
  . left
    exact countable
  . right
    obtain ⟨P, nonempty, perfect, inside⟩ := perfectPart
    have uncountable := perfect.uncountable with perfect, nonempty
    exact ⟨P, nonempty, perfect, inside, uncountable⟩