JordanContours.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Circle contours of compact regular levels

Two classical inputs are separated from the contour construction.

CompactOneManifoldClassification is the compact boundaryless case of Milnor, Topology from the Differentiable Viewpoint (1965), Appendix "Classifying 1-Manifolds", theorem p. 55 (proof pp. 55--57). https://www.ux1.eiu.edu/~cidelman/Classes/4855%20and%205220/Supplementary%20Texts/MilnorTopDiffVpt.pdf
PlanarSchoenflies is Moise, Geometric Topology in Dimensions 2 and 3, Graduate Texts in Mathematics 47 (1977), Theorem 10.4: a continuous injection of the unit circle into the plane extends to a homeomorphism of the plane. DOI: https://doi.org/10.1007/978-1-4612-9906-6

Both are explicit proposition parameters, not axioms. Neither input asserts the manuscript's obstacle-isolating disk selection. Smooth local charts, finite components, their planar embeddings and the contour cover are proved.

def OAI.CircleDomainRigidity.CompactOneManifoldClassification line 36
Source documentation
Published input: the compact connected boundaryless case of Milnor's classification of smooth one-manifolds.
```
def CompactOneManifoldClassification : Prop :=
…
```
def OAI.CircleDomainRigidity.PlanarSchoenflies line 44
Source documentation
Published input: the planar Schoenflies extension theorem in exactly its circle-to-plane form.
```
def PlanarSchoenflies : Prop :=
…
```
def OAI.CircleDomainRigidity.componentOpen line 48
theorem OAI.CircleDomainRigidity.componentOpen_connectedSpace line 55
theorem OAI.CircleDomainRigidity.componentOpen_compactSpace line 64

theorem OAI.CircleDomainRigidity.finite_smooth_circle_contours_of_regularLevel line 78

Source documentation

A compact regular scalar level is covered by finitely many pairwise disjoint actual embedded smooth circle parametrizations. Only the circle classification theorem is assumed; its local manifold hypotheses were proved in RegularContours.

theorem finite_smooth_circle_contours_of_regularLevel
    (legacyClassification : CompactOneManifoldClassification) {f : ℂ → ℝ} {t : ℝ}
    (hf : ContDiff ℝ ∞ f) (ht : IsPlanarRegularValue f t)
    (hc : IsCompact {z | f z = t}) :
    Finite (ConnectedComponents {z // f z = t}) ∧
      ∃ γ : ConnectedComponents {z // f z = t} → Circle → ℂ,
        (∀ c, ContMDiff (𝓡 1) (𝓘(ℝ, ℂ)) ∞ (γ c) ∧ Topology.IsEmbedding (γ c)) ∧
        Pairwise (fun c d => Disjoint (range (γ c)) (range (γ d))) ∧
        (⋃ c, range (γ c)) = {z | f z = t} := by
…

Mentions: OAI.CircleDomainRigidity.CompactOneManifoldClassification, OAI.CircleDomainRigidity.IsPlanarRegularValue

theorem OAI.CircleDomainRigidity.exists_filled_disk_of_circle line 130

Source documentation

The bounded filled side of one embedded circle is an actual topological disk. Compact closure, connectedness and the exact boundary are derived from the ambient Schoenflies extension.

theorem exists_filled_disk_of_circle (hschoenflies : PlanarSchoenflies)
    (γ : Circle → ℂ) (hγ : Continuous γ) (hinj : Injective γ) :
    ∃ U : Set ℂ, IsOpen U ∧ IsConnected U ∧ IsCompact (closure U) ∧
      frontier U = range γ ∧
      Nonempty ((Metric.closedBall (0 : ℂ) 1) ≃ₜ closure U) := by
…

Mentions: OAI.CircleDomainRigidity.PlanarSchoenflies

theorem OAI.CircleDomainRigidity.exists_finite_contours_isolating_obstacle line 158

Source documentation

Apply the constructed regular cutoff and classify all its level components. The finite smooth contours avoid the entire obstacle, while the unfilled superlevel neighborhood isolates exactly the chosen compact piece.

theorem exists_finite_contours_isolating_obstacle
    (hsard : SmoothPlanarSard) {A F V : Set ℂ} (hA : IsCompact A) (hAF : A ⊆ F)
    (hFA : IsClosed (F \ A)) (hV : IsOpen V) (hAV : A ⊆ V) :
    ∃ (f : ℂ → ℝ) (t : ℝ)
      (γ : ConnectedComponents {z // f z = t} → Circle → ℂ),
      Finite (ConnectedComponents {z // f z = t}) ∧
      ContDiff ℝ ∞ f ∧ t ∈ Ioo 0 1 ∧
      IsOpen {z | t < f z} ∧ A ⊆ {z | t < f z} ∧
      IsCompact (closure {z | t < f z}) ∧ closure {z | t < f z} ⊆ V ∧
      closure {z | t < f z} ∩ F = A ∧
      (∀ c, ContMDiff (𝓡 1) (𝓘(ℝ, ℂ)) ∞ (γ c) ∧
        Topology.IsEmbedding (γ c) ∧ Disjoint (range (γ c)) F) ∧
…

Mentions: OAI.CircleDomainRigidity.SmoothPlanarSard