MetricGoodSmoothingAtlas.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A smooth metric supplies the positive reference coefficients of an actual subordinate good-phase smoothing atlas.

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.exists_metric_good_smoothingAtlas line 38

Source documentation

The actual metric, local immersion and nonzero second fundamental form determine an atlas with positive coefficients and good pure and same-chart mixed directions on every compact weight support.

theorem exists_metric_good_smoothingAtlas (g : SmoothMetric M) {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) :
    ∃ (A : SmoothingAtlas M)
      (P : ∀ p, PhasePatch F (coordinateMetric g p) p),
      (∀ i : A.centers, tsupport (A.weight i) ⊆ (P (i : M)).V) ∧
      (∀ i x, x ∈ tsupport (A.weight i) → A.outer i =ᶠ[𝓝 x] (fun _ => 1)) ∧
      ∀ (i : A.centers) (x : SmallModes.Base),
        x ∈ (modeSupport (A.chartWeightCompact i) : Set SmallModes.Base) →
        Function.Injective (fderiv ℝ (spaceCoordinates ∘ A.vectorPlaneRead i F) x) ∧
…

Mentions: OAI.ClosedSurfaceR4.SmoothMetric, OAI.ClosedSurfaceR4.Space, OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.SmallModes.Base, OAI.ClosedSurfaceR4.coordinateMap, OAI.ClosedSurfaceR4.coordinateCenter, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas, OAI.ClosedSurfaceR4.PhasePatch, OAI.ClosedSurfaceR4.coordinateMetric, OAI.ClosedSurfaceR4.spaceCoordinates