OAI/Geometry/SurfaceImmersion/Correction/AtlasGlobalFreeModes.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The finite free correction is an actual sum of globally smooth phase modes.

  1. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.coordinateAmplitude_support line 17
  2. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.freeGlobalPhase line 28

    Source documentation

    The outer cutoff makes the original local phase a globally smooth scalar.

    def freeGlobalPhase
    (d : ∀ i, ChartedMeanFamilyData (P i) ε τ s (r i) ρ R (reference i))
    (i : A.centers) (j : Fin 3) : M → ℝ :=
…
  3. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.freeGlobalAmplitude line 34

    Source documentation

    The global complex amplitude retains the original compact support.

    def freeGlobalAmplitude
    (d : ∀ i, ChartedMeanFamilyData (P i) ε τ s (r i) ρ R (reference i))
    (hρ : 0 < ρ) (δ : ℝ) (q : ℕ) (u : ∀ x : M, CovariantTwoTensor x)
    (i : A.centers) (j : Fin 3) : M → Fin 4 → ℂ :=
…

    Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.CovariantTwoTensor

  4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.freeGlobalPhase_smooth line 41
  5. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.freeGlobalAmplitude_smooth line 47
  6. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.atlas_free_global_modes line 55