GoodQuadraticAtlasPhases.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The actual restored global phases have good quadratic interactions.

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.exists_good_quadratic_atlas_phases line 21

Source documentation

A single choice of positive frequencies makes every actual quadratic phase good on the compact support where its amplitude can be nonzero.

theorem exists_good_quadratic_atlas_phases {F : M → Space}
    (hF : ContMDiff planeModel spaceModel ∞ F) (Q : A.centers → PhaseBasis)
    (houter : ∀ i x, x ∈ tsupport (A.weight i) → A.outer i =ᶠ[𝓝 x] (fun _ => 1))
    (hImm : ∀ i x, x ∈ (modeSupport (A.chartWeightCompact i) : Set SmallModes.Base) →
      Function.Injective (fderiv ℝ (spaceCoordinates ∘ A.vectorPlaneRead i F) x))
    (hpure : ∀ i j x, x ∈ (modeSupport (A.chartWeightCompact i) : Set SmallModes.Base) →
      Good (realSecondTensor (spaceCoordinates ∘ A.vectorPlaneRead i F) x) ((Q i).ξ j)) :
    ∃ w : A.centers → Fin 3 → ℝ, (∀ i j, 0 < w i j) ∧
      ∀ k l x, x ∈ (modeSupport
        (A.quadraticOverlapCompact (fun a : A.centers × Fin 3 => tsupport (A.weight a.1))
          (fun a => isClosed_tsupport (A.weight a.1)) k l) : Set SmallModes.Base) →
        Good (realSecondTensor (spaceCoordinates ∘ A.vectorPlaneRead k F) x)
…

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