The recursive quantitative stage construction

This module iterates the two-sided quantitative successor. Window centres are read from a recurrent sequence and all three quantitative parameters use a dyadic scale.

structure Schoenflies.QuantitativeSchedule (C : Set Plane) : Type

The external choices needed by the quantitative recursion. centreBase will be wrapped by recur, so every one of its values occurs at arbitrarily late stages.

• centreBase : ℕ → Plane

  Interior centres to revisit arbitrarily late in the recursion.

• centreBase_mem (n : ℕ) : self.centreBase n ∈ inside C
• anchors : ℕ → List Plane

  Boundary anchors prescribed at each stage.

def Schoenflies.QuantitativeSchedule.centre {C : Set Plane} (q : QuantitativeSchedule C) (n : ℕ) : Plane

The recurrent centre used at stage n.

Equations

• q.centre n = Schoenflies.recur q.centreBase n

theorem Schoenflies.QuantitativeSchedule.centre_mem {C : Set Plane} (q : QuantitativeSchedule C) (n : ℕ) : q.centre n ∈ inside C

noncomputable def Schoenflies.dyadicScale (n : ℕ) : ℝ

The dyadic window and source-mesh scale at successor n.

Equations

• Schoenflies.dyadicScale n = (2 ^ n)⁻¹ / 2

theorem Schoenflies.dyadicScale_pos (n : ℕ) : 0 < dyadicScale n

theorem Schoenflies.tendsto_dyadicScale : Filter.Tendsto dyadicScale Filter.atTop (nhds 0)

noncomputable def Schoenflies.dyadicTargetBound (n : ℕ) : ℝ

The target bound leaves an inessential factor four for the initial-stage estimate.

Equations

• Schoenflies.dyadicTargetBound n = 4 * Schoenflies.dyadicScale n

theorem Schoenflies.dyadicTargetBound_pos (n : ℕ) : 0 < dyadicTargetBound n

theorem Schoenflies.tendsto_dyadicTargetBound : Filter.Tendsto dyadicTargetBound Filter.atTop (nhds 0)

noncomputable def Schoenflies.quantitativeTargetEps : ℕ → ℝ

A target-star bound indexed by the actual stages. The initial pair receives one coarse bound; every successor uses the estimate established when it was constructed.

Equations

• Schoenflies.quantitativeTargetEps 0 = 4
• Schoenflies.quantitativeTargetEps n.succ = Schoenflies.dyadicTargetBound n

theorem Schoenflies.tendsto_quantitativeTargetEps : Filter.Tendsto quantitativeTargetEps Filter.atTop (nhds 0)

noncomputable def Schoenflies.scheduledQuantitativeSuccessor {γ : Type u_1} {S₀ : CellStructure γ} {C : Set Plane} [Infinite γ] (hC : IsSeparating C) (hcycle : S₀.OuterEdgesFormCycle) (q : QuantitativeSchedule C) (n : ℕ) (P : GeneratedPair S₀ C (C ∪ inside C) modelCurve (Plane.closedSquare 0 1)) : QuantitativeSuccessor P (q.anchors n) (q.centre n) (dyadicScale n) (dyadicScale n) (dyadicTargetBound n)

Choose a quantitative successor at stage n.

Equations

• Schoenflies.scheduledQuantitativeSuccessor hC hcycle q n P = Classical.choice ⋯

noncomputable def Schoenflies.quantitativeStage {γ : Type u_1} {S₀ : CellStructure γ} {C : Set Plane} [Infinite γ] (P₀ : GeneratedPair S₀ C (C ∪ inside C) modelCurve (Plane.closedSquare 0 1)) (hC : IsSeparating C) (hcycle : S₀.OuterEdgesFormCycle) (q : QuantitativeSchedule C) : ℕ → GeneratedPair S₀ C (C ∪ inside C) modelCurve (Plane.closedSquare 0 1)

The recursively chosen generated pairs.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Schoenflies.quantitativeStage_zero {γ : Type u_1} {S₀ : CellStructure γ} {C : Set Plane} [Infinite γ] (P₀ : GeneratedPair S₀ C (C ∪ inside C) modelCurve (Plane.closedSquare 0 1)) (hC : IsSeparating C) (hcycle : S₀.OuterEdgesFormCycle) (q : QuantitativeSchedule C) : quantitativeStage P₀ hC hcycle q 0 = P₀

@[simp]

theorem Schoenflies.quantitativeStage_succ {γ : Type u_1} {S₀ : CellStructure γ} {C : Set Plane} [Infinite γ] (P₀ : GeneratedPair S₀ C (C ∪ inside C) modelCurve (Plane.closedSquare 0 1)) (hC : IsSeparating C) (hcycle : S₀.OuterEdgesFormCycle) (q : QuantitativeSchedule C) (n : ℕ) : quantitativeStage P₀ hC hcycle q (n + 1) = (scheduledQuantitativeSuccessor hC hcycle q n (quantitativeStage P₀ hC hcycle q n)).pair

noncomputable def Schoenflies.quantitativeParent {γ : Type u_1} {S₀ : CellStructure γ} {C : Set Plane} [Infinite γ] (P₀ : GeneratedPair S₀ C (C ∪ inside C) modelCurve (Plane.closedSquare 0 1)) (hC : IsSeparating C) (hcycle : S₀.OuterEdgesFormCycle) (q : QuantitativeSchedule C) (n : ℕ) : γ → γ

The composite parent map selected at successor n.

Equations

• Schoenflies.quantitativeParent P₀ hC hcycle q n = (Schoenflies.scheduledQuantitativeSuccessor hC hcycle q n (Schoenflies.quantitativeStage P₀ hC hcycle q n)).parent

theorem Schoenflies.quantitativeTransition {γ : Type u_1} {S₀ : CellStructure γ} {C : Set Plane} [Infinite γ] (P₀ : GeneratedPair S₀ C (C ∪ inside C) modelCurve (Plane.closedSquare 0 1)) (hC : IsSeparating C) (hcycle : S₀.OuterEdgesFormCycle) (q : QuantitativeSchedule C) (n : ℕ) : StageTransition (quantitativeStage P₀ hC hcycle q (n + 1)) (quantitativeStage P₀ hC hcycle q n) (quantitativeParent P₀ hC hcycle q n)

Consecutive recursively chosen stages satisfy the common transition interface.

theorem Schoenflies.quantitativeStage_diam_targetStar_lt {γ : Type u_1} {S₀ : CellStructure γ} {C : Set Plane} [Infinite γ] (P₀ : GeneratedPair S₀ C (C ∪ inside C) modelCurve (Plane.closedSquare 0 1)) (hC : IsSeparating C) (hcycle : S₀.OuterEdgesFormCycle) (q : QuantitativeSchedule C) (n : ℕ) {σ : γ} (hσ : σ ∈ (quantitativeStage P₀ hC hcycle q (n + 1)).str.cells) : Metric.diam ((quantitativeStage P₀ hC hcycle q (n + 1)).tgt.star σ) < dyadicTargetBound n

Every noninitial target star satisfies the scheduled dyadic bound.

theorem Schoenflies.quantitativeStage_diam_targetStar_le {γ : Type u_1} {S₀ : CellStructure γ} {C : Set Plane} [Infinite γ] (P₀ : GeneratedPair S₀ C (C ∪ inside C) modelCurve (Plane.closedSquare 0 1)) (hC : IsSeparating C) (hcycle : S₀.OuterEdgesFormCycle) (q : QuantitativeSchedule C) (n : ℕ) {σ : γ} (hσ : σ ∈ (quantitativeStage P₀ hC hcycle q n).str.cells) : Metric.diam ((quantitativeStage P₀ hC hcycle q n).tgt.star σ) ≤ quantitativeTargetEps n

Every target star satisfies the stage-indexed uniform bound, including stage zero.

theorem Schoenflies.quantitativeStage_diam_sourceStar_le {γ : Type u_1} {S₀ : CellStructure γ} {C : Set Plane} [Infinite γ] (P₀ : GeneratedPair S₀ C (C ∪ inside C) modelCurve (Plane.closedSquare 0 1)) (hC : IsSeparating C) (hcycle : S₀.OuterEdgesFormCycle) (q : QuantitativeSchedule C) (n : ℕ) {x : Plane} (hx : x ∈ openWindow C (dyadicScale n) (q.centre n)) : Metric.diam ((quantitativeStage P₀ hC hcycle q (n + 1)).src.star ((quantitativeStage P₀ hC hcycle q (n + 1)).src.carrier x)) ≤ 2 * dyadicScale n

At every point caught by the stage-n window, the successor source star satisfies the scheduled dyadic bound.

theorem Schoenflies.quantitativeStage_sourceStar_subset_of_le {γ : Type u_1} {S₀ : CellStructure γ} {C : Set Plane} [Infinite γ] (P₀ : GeneratedPair S₀ C (C ∪ inside C) modelCurve (Plane.closedSquare 0 1)) (hC : IsSeparating C) (hcycle : S₀.OuterEdgesFormCycle) (q : QuantitativeSchedule C) {n m : ℕ} (hnm : n ≤ m) {x : Plane} (hx : x ∈ C ∪ inside C) : (quantitativeStage P₀ hC hcycle q m).src.star ((quantitativeStage P₀ hC hcycle q m).src.carrier x) ⊆ (quantitativeStage P₀ hC hcycle q n).src.star ((quantitativeStage P₀ hC hcycle q n).src.carrier x)

Source stars at a fixed point shrink monotonically through all later recursive stages.

def Schoenflies.QuantitativeSchedule.CentresDense {C : Set Plane} (q : QuantitativeSchedule C) : Prop

Metric density of the base centre sequence inside the Jordan domain.

Equations

• q.CentresDense = ∀ x ∈ Schoenflies.inside C, ∀ (δ : ℝ), 0 < δ → ∃ (k : ℕ), (q.centreBase k).supDist x < δ

noncomputable def Schoenflies.denseQuantitativeSchedule {C : Set Plane} (hC : IsSeparating C) : QuantitativeSchedule C

A canonical schedule obtained by taking a dense sequence in the open Jordan domain. The auxiliary anchor list may be empty: each target-mesh constructor adds whatever fresh boundary anchors it needs.

Equations

• Schoenflies.denseQuantitativeSchedule hC = { centreBase := fun (n : ℕ) => ↑(TopologicalSpace.denseSeq (↑(Schoenflies.inside C)) n), centreBase_mem := ⋯, anchors := fun (x : ℕ) => [] }

theorem Schoenflies.denseQuantitativeSchedule_centresDense {C : Set Plane} (hC : IsSeparating C) : (denseQuantitativeSchedule hC).CentresDense

theorem Schoenflies.tendsto_quantitativeStage_diam_sourceStar {γ : Type u_1} {S₀ : CellStructure γ} {C : Set Plane} [Infinite γ] (P₀ : GeneratedPair S₀ C (C ∪ inside C) modelCurve (Plane.closedSquare 0 1)) (hC : IsSeparating C) (hcycle : S₀.OuterEdgesFormCycle) (q : QuantitativeSchedule C) (hdense : q.CentresDense) {x : Plane} (hx : x ∈ inside C) : Filter.Tendsto (fun (n : ℕ) => Metric.diam ((quantitativeStage P₀ hC hcycle q n).src.star ((quantitativeStage P₀ hC hcycle q n).src.carrier x))) Filter.atTop (nhds 0)

The recurrent dense windows and dyadic mesh bounds force pointwise convergence of the source-star diameters.

noncomputable def Schoenflies.quantitativeStageSequence {γ : Type u_1} {S₀ : CellStructure γ} {C : Set Plane} [Infinite γ] (P₀ : GeneratedPair S₀ C (C ∪ inside C) modelCurve (Plane.closedSquare 0 1)) (hC : IsSeparating C) (hcycle : S₀.OuterEdgesFormCycle) (q : QuantitativeSchedule C) (hbase : S₀.CombInvariants) (hdense : q.CentresDense) : StageSequence γ S₀ C

The complete quantitative recursion, in the exact interface consumed by the limit-map construction.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Schoenflies.denseQuantitativeStageSequence {γ : Type u_1} {S₀ : CellStructure γ} {C : Set Plane} [Infinite γ] (P₀ : GeneratedPair S₀ C (C ∪ inside C) modelCurve (Plane.closedSquare 0 1)) (hC : IsSeparating C) (hcycle : S₀.OuterEdgesFormCycle) (hbase : S₀.CombInvariants) : StageSequence γ S₀ C

The recursion with its canonical dense schedule. No convergence hypothesis remains in this interface.

Equations

• Schoenflies.denseQuantitativeStageSequence P₀ hC hcycle hbase = Schoenflies.quantitativeStageSequence P₀ hC hcycle (Schoenflies.denseQuantitativeSchedule hC) hbase ⋯