SmoothContours.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Compact smooth cutoffs and regular superlevel neighborhoods

This is the first half of the common contour construction in §1 of the Koebe manuscript's small-disks proof. The cutoff is constructed using Mathlib's smooth Urysohn theorem and a relatively compact open neighborhood; its existence is unconditional.

Only the regular-value choice is conditional on a published input: Arthur Sard, The measure of the critical values of differentiable maps, Bull. Amer. Math. Soc. 48 (1942), 883--890, Theorem 7.2, pp. 889--890, DOI: 10.1090/S0002-9904-1942-07811-6. We use only its specialization to compactly supported smooth maps from the plane to the real line. The assumption says that their actual critical-value image has Lebesgue outer measure zero. Original article: https://doi.org/10.1090/S0002-9904-1942-07811-6 Readable scan: https://webhomes.maths.ed.ac.uk/~v1ranick/papers/sard.pdf

No smooth Jordan disk or finite-component decomposition is assumed. The constructed neighborhood has compact closure in the prescribed open set and its boundary lies in a compact regular level set.

theorem OAI.CircleDomainRigidity.exists_smooth_planar_cutoff line 38

Source documentation

An actual smooth compactly supported planar cutoff, equal to one on a neighborhood of the given compact set.

theorem exists_smooth_planar_cutoff {A O : Set ℂ}
    (hA : IsCompact A) (hO : IsOpen O) (hAO : A ⊆ O) :
    ∃ f : ℂ → ℝ, ContDiff ℝ ∞ f ∧ HasCompactSupport f ∧
      tsupport f ⊆ O ∧ (∀ z, f z ∈ Icc 0 1) ∧
      ∀ᶠ z in 𝓝ˢ A, f z = 1 := by
…

def OAI.CircleDomainRigidity.IsPlanarRegularValue line 59
Source documentation
The actual differential is nonzero at every point of the level.
```
def IsPlanarRegularValue (f : ℂ → ℝ) (t : ℝ) : Prop :=
…
```
def OAI.CircleDomainRigidity.SmoothPlanarSard line 65
Source documentation
Published input: Sard (1942), Theorem 7.2, restricted to the smooth compactly supported scalar planar case needed for contour selection. This is a proposition parameter, not a global axiom.
```
def SmoothPlanarSard : Prop :=
…
```
theorem OAI.CircleDomainRigidity.exists_regular_value_in_interval line 69
theorem OAI.CircleDomainRigidity.closure_superlevel_subset_tsupport line 84
Source documentation
A positive superlevel of a compactly supported continuous function has compact closure inside its topological support.
```
theorem closure_superlevel_subset_tsupport {f : ℂ → ℝ} {t : ℝ} (ht : 0 < t) :
    closure {z | t < f z} ⊆ tsupport f := by
…
```
theorem OAI.CircleDomainRigidity.isCompact_nonzero_level line 90

theorem OAI.CircleDomainRigidity.exists_smooth_regular_superlevel_neighborhood line 102

Source documentation

The regular superlevel neighborhood used before taking outer contours. The cutoff, compact support and neighborhood control are constructed; only critical-value nullity is supplied by Sard.

theorem exists_smooth_regular_superlevel_neighborhood
    (hsard : SmoothPlanarSard) {A O : Set ℂ}
    (hA : IsCompact A) (hO : IsOpen O) (hAO : A ⊆ O) :
    ∃ (f : ℂ → ℝ) (t : ℝ), ContDiff ℝ ∞ f ∧ HasCompactSupport f ∧
      tsupport f ⊆ O ∧ (∀ z, f z ∈ Icc 0 1) ∧ 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} ⊆ O ∧
      IsCompact {z | f z = t} ∧ IsPlanarRegularValue f t ∧
      frontier {z | t < f z} ⊆ {z | f z = t} := by
…

Mentions: OAI.CircleDomainRigidity.SmoothPlanarSard, OAI.CircleDomainRigidity.IsPlanarRegularValue

theorem OAI.CircleDomainRigidity.exists_regular_superlevel_isolating_obstacle line 128

Source documentation

Isolate a compact relatively clopen piece of an obstacle by a regular superlevel neighborhood. IsClosed (F \ A) is precisely the closedness needed to exclude the other obstacle points. The positive level, hence also the boundary, misses the whole obstacle.

theorem exists_regular_superlevel_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 : ℝ), 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 ∧ IsCompact {z | f z = t} ∧
      IsPlanarRegularValue f t ∧ Disjoint {z | f z = t} F ∧
      Disjoint (frontier {z | t < f z}) F := by
…

Mentions: OAI.CircleDomainRigidity.SmoothPlanarSard, OAI.CircleDomainRigidity.IsPlanarRegularValue