GoodSmoothingAtlas.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

A smoothing atlas subordinate to actual good-phase neighborhoods.

def OAI.ClosedSurfaceR4.PhasePatch.phaseBasis line 18
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.planeCoordinateIsometry_chart line 29
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.coordinateMap_chart_symm line 33
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.vectorPlaneRead_eventually_coordinateMap line 44
Source documentation
Locally constant outer cutoffs identify the entire coordinate germ on the original weight support, and hence every derivative used by the phases.
```
lemma vectorPlaneRead_eventually_coordinateMap
    (F : M → Space) (i : A.centers)
    (houter : ∀ x ∈ tsupport (A.weight i), A.outer i =ᶠ[𝓝 x] (fun _ => 1))
    {p : M} (hp : p ∈ tsupport (A.weight i)) :
    (spaceCoordinates ∘ A.vectorPlaneRead i F) =ᶠ[
      𝓝 (planeCoordinateIsometry (chart (i : M) p))] coordinateMap F (i : M) := by
…
```
Mentions: OAI.ClosedSurfaceR4.Space, OAI.ClosedSurfaceR4.spaceCoordinates, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.chart, OAI.ClosedSurfaceR4.coordinateMap

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.exists_good_smoothingAtlas line 80

Source documentation

Good phase patches and a smoothing atlas share the same actual centers. All local immersion, positivity and pure/mixed phase conditions are inherited by the globally smooth coordinate readings on their compact supports.

theorem exists_good_smoothingAtlas {F : M → Space}
    (hF : ContMDiff planeModel spaceModel ∞ F)
    (hImm : ∀ p, Function.Injective (mfderiv planeModel spaceModel F p))
    (hB : ∀ p, ∃ v w : SmallModes.Base,
      realSecondForm (coordinateMap F p) v w (coordinateCenter p) ≠ 0)
    (H : M → SmallModes.Base → PhaseMean.Tensor)
    (hH : ∀ p, ContinuousAt (H p) (coordinateCenter p))
    (hH0 : ∀ p, 0 < H p (coordinateCenter p) 0)
    (hHdet : ∀ p, 0 < H p (coordinateCenter p) 0 * H p (coordinateCenter p) 2 -
      (H p (coordinateCenter p) 1)^2) :
    ∃ (A : SmoothingAtlas M) (P : ∀ p, PhasePatch F (H p) p),
      (∀ i : A.centers, tsupport (A.weight i) ⊆ (P (i : M)).V) ∧
…

Mentions: OAI.ClosedSurfaceR4.Space, OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.SmallModes.Base, OAI.ClosedSurfaceR4.coordinateMap, OAI.ClosedSurfaceR4.coordinateCenter, OAI.ClosedSurfaceR4.PhaseMean.Tensor, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas, OAI.ClosedSurfaceR4.PhasePatch