OAI/Geometry/SurfaceImmersion/Atlas/GlobalPhaseGerms.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

On intersecting weight supports, restored global linear phases have the same germs and covectors as the actual manifold coordinate phases.

  1. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.linearAtlasPhase_eventually line 21
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.vectorPlaneRead_eventually_comp_coordinateInverse line 32
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.linearAtlasPhase_read_eventually line 67

    Source documentation

    Both the original phase and its reading in another chart agree as germs where the two actual compact supports meet.

    lemma linearAtlasPhase_read_eventually (Q : A.centers → PhaseBasis)
    (w : A.centers → Fin 3 → ℝ) (a : A.centers × Fin 3) (k : A.centers)
    (houter : ∀ i x, x ∈ tsupport (A.weight i) → A.outer i =ᶠ[𝓝 x] (fun _ => 1))
    {p : M} (hpa : p ∈ tsupport (A.weight a.1)) (hpk : p ∈ tsupport (A.weight k)) :
    A.vectorPlaneRead k (A.linearAtlasPhase Q w a) =ᶠ[𝓝 (coordinateChart (k : M) p)]
      atlasPhase (a.1 : M) (w a.1 a.2 • (Q a.1).ξ a.2) ∘ (coordinateChart (k : M)).symm := by
…

    Mentions: OAI.ClosedSurfaceR4.coordinateChart, OAI.ClosedSurfaceR4.atlasPhase

  4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.linearAtlasPhase_read_phaseDerivative line 84