AtlasPhaseMeanDomains.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Fixed mean domains and common margins obtained from compact atlas geometry.

structure OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.PhaseMeanDomains line 19

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.exists_phaseMeanDomains line 51

Source documentation

Strict positivity and good geometry on the actual compact supports supply all domain and margin data for the mean constructor.

theorem exists_phaseMeanDomains (F : M → Space)
    (hF : ContMDiff planeModel spaceModel ∞ F) (Q : A.centers → PhaseBasis)
    (hImm : ∀ i x, x ∈ (modeSupport (A.chartWeightCompact i) : Set SmallModes.Base) →
      Function.Injective (fderiv ℝ (spaceCoordinates ∘ A.vectorPlaneRead i F) x))
    (hgood : ∀ i j x, x ∈ (modeSupport (A.chartWeightCompact i) : Set SmallModes.Base) →
      Good (realSecondTensor (spaceCoordinates ∘ A.vectorPlaneRead i F) x) ((Q i).ξ j))
    (reference : A.centers → SmallModes.Base → Tensor)
    (href : ∀ i, Continuous (reference i))
    (hpos : ∀ i j x, x ∈ (modeSupport (A.chartWeightCompact i) : Set SmallModes.Base) →
      0 < (Q i).Q j (reference i x)) : Nonempty (A.PhaseMeanDomains F Q reference) := by
…

Mentions: OAI.ClosedSurfaceR4.Space, OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.SmallModes.Base, OAI.ClosedSurfaceR4.spaceCoordinates