RegularContours.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Smooth regular planar contours

The implicit function theorem supplies actual smooth local coordinates on a regular scalar level. Compactness then makes the number of components finite. For the subsequent circle-classification step, the needed classical result is Milnor, Topology from the Differentiable Viewpoint (1965), Appendix "Classifying 1-Manifolds", theorem on p. 55: a compact connected smooth one-manifold without boundary is diffeomorphic to the circle. Primary scan: https://www.ux1.eiu.edu/~cidelman/Classes/4855%20and%205220/Supplementary%20Texts/MilnorTopDiffVpt.pdf

theorem OAI.CircleDomainRigidity.finrank_ker_planar_functional line 27
Source documentation
The kernel of a nonzero real scalar differential on the plane is a line.
```
theorem finrank_ker_planar_functional {L : ℂ →L[ℝ] ℝ} (hL : L ≠ 0) :
    Module.finrank ℝ L.ker = 1 := by
…
```

theorem OAI.CircleDomainRigidity.exists_smooth_planar_level_chart line 41

Source documentation

A genuine smooth ambient normal form for a regular planar scalar map. The first chart coordinate is the original function, on its entire domain.

theorem exists_smooth_planar_level_chart {f : ℂ → ℝ}
    (hf : ContDiff ℝ ∞ f) {z : ℂ} (hz : fderiv ℝ f z ≠ 0) :
    ∃ e : OpenPartialHomeomorph ℂ (ℝ × ℝ), z ∈ e.source ∧
      (∀ w, (e w).1 = f w) ∧ ContDiff ℝ ∞ e ∧
      ContDiffOn ℝ ∞ e.symm e.target := by
…

def OAI.CircleDomainRigidity.levelChartInverse line 95
theorem OAI.CircleDomainRigidity.levelChartInverse_coe line 104

def OAI.CircleDomainRigidity.planarLevelChart line 113

Source documentation

Restrict ambient regular-level coordinates to an actual real chart of the level subtype.

noncomputable def planarLevelChart {f : ℂ → ℝ} {t : ℝ}
    (e : OpenPartialHomeomorph ℂ (ℝ × ℝ))
    (he : ∀ w, (e w).1 = f w) (z : {w // f w = t}) :
    OpenPartialHomeomorph {w // f w = t} ℝ where
…

theorem OAI.CircleDomainRigidity.contDiffOn_planarLevelChart_transition line 163
def OAI.CircleDomainRigidity.regularLevelAmbient line 181
theorem OAI.CircleDomainRigidity.regularLevelAmbient_spec line 186
def OAI.CircleDomainRigidity.regularLevelChartedSpace line 197
Source documentation
The actual real atlas induced by implicit-function charts on a regular level.
```
noncomputable def regularLevelChartedSpace {f : ℂ → ℝ} {t : ℝ}
    (hf : ContDiff ℝ ∞ f) (ht : IsPlanarRegularValue f t) :
    ChartedSpace ℝ {w // f w = t} where
…
```
Mentions: OAI.CircleDomainRigidity.IsPlanarRegularValue
theorem OAI.CircleDomainRigidity.regularLevel_isManifold line 209
Source documentation
A regular level of a smooth planar scalar map is a smooth one-dimensional manifold without boundary, with the topology inherited from the plane.
```
theorem regularLevel_isManifold {f : ℂ → ℝ} {t : ℝ}
    (hf : ContDiff ℝ ∞ f) (ht : IsPlanarRegularValue f t) :
    letI := regularLevelChartedSpace hf ht
…
```
Mentions: OAI.CircleDomainRigidity.IsPlanarRegularValue, OAI.CircleDomainRigidity.regularLevelChartedSpace
theorem OAI.CircleDomainRigidity.regularLevel_subtype_contMDiff line 225
Source documentation
The manifold charts describe the existing planar inclusion; their smooth structure is therefore compatible with the physical embedding.
```
theorem regularLevel_subtype_contMDiff {f : ℂ → ℝ} {t : ℝ}
    (hf : ContDiff ℝ ∞ f) (ht : IsPlanarRegularValue f t) :
    letI := regularLevelChartedSpace hf ht
…
```
Mentions: OAI.CircleDomainRigidity.IsPlanarRegularValue, OAI.CircleDomainRigidity.regularLevelChartedSpace
theorem OAI.CircleDomainRigidity.regularLevel_locallyConnectedSpace line 250

theorem OAI.CircleDomainRigidity.finite_connectedComponents_regularLevel line 257

Source documentation

Compact regular planar levels have only finitely many connected components.

theorem finite_connectedComponents_regularLevel {f : ℂ → ℝ} {t : ℝ}
    (hf : ContDiff ℝ ∞ f) (ht : IsPlanarRegularValue f t)
    (hc : IsCompact {w | f w = t}) :
    Finite (ConnectedComponents {w // f w = t}) := by
…

Mentions: OAI.CircleDomainRigidity.IsPlanarRegularValue

theorem OAI.CircleDomainRigidity.finite_connectedComponents_nonzero_regularLevel line 265