AtlasGoodPhaseCancellation.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Assemble compact good-phase corrections in the fixed atlas. All local solvers and constants are constructed from immersion and good-phase geometry before any target or scale is chosen.

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.atlas_good_phase_cancellation line 44

Source documentation

Good phase geometry on the compact supports supplies an actual global linear correction, with constants uniform over targets and both scales.

theorem atlas_good_phase_cancellation
    {ι : A.centers → Type*} [∀ i, Fintype (ι i)]
    (F : M → Space) (hF : ContMDiff planeModel spaceModel ∞ F)
    (φ : (i : A.centers) → ι i → JetPolynomial.Base → ℝ)
    (hφ : ∀ i j, ContDiff ℝ ∞ (φ i j))
    (K : (i : A.centers) → ι i → TopologicalSpace.Compacts JetPolynomial.Base)
    (hK : ∀ i j, (modeSupport (K i j) : Set SmallModes.Base) ⊆
      (modeSupport (A.chartWeightCompact i) : Set SmallModes.Base))
    (hImm : ∀ i j p, p ∈ (modeSupport (K i j) : Set SmallModes.Base) →
      Function.Injective (fderiv ℝ (spaceCoordinates ∘ A.vectorPlaneRead i F) p))
    (hgood : ∀ i j p, p ∈ (modeSupport (K i j) : Set SmallModes.Base) →
      PhaseGeometry.Good (RealModes.realSecondTensor (spaceCoordinates ∘ A.vectorPlaneRead i F) p)
…

Mentions: OAI.ClosedSurfaceR4.Space, OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.SmallModes.Base, OAI.ClosedSurfaceR4.spaceCoordinates, OAI.ClosedSurfaceR4.PhaseGeometry.Good, OAI.ClosedSurfaceR4.RealModes.realSecondTensor