OAI/Geometry/SurfaceImmersion/Primitive/AtlasPeriodicAnsatz.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The supported finite periodic ansatz is a genuine global smooth map, with exactly the intended coordinate jets on its chosen chart.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.periodicAtlasAnsatz line 18
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.jetChartMap_restored_supported line 24
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.periodicAtlasAnsatz_smooth line 43
  4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.periodicAtlasAnsatz_coordinate line 57

    Source documentation

    This equality is global in the chart coordinates and therefore also identifies every derivative used by the periodic metric expansion.

    lemma periodicAtlasAnsatz_coordinate (i : A.centers) (F : M → Space)
    {O : TopologicalSpace.Opens JetPolynomial.Base} (U : ℕ → Family O Space)
    {K : Set JetPolynomial.Base} (hK : IsClosed K)
    (hKA : K ⊆ (A.chartWeightCompact i : Set JetPolynomial.Base))
    (hzero : ∀ j x, x ∉ K → (U j).val x = 0)
    (ℓ : JetPolynomial.Base →L[ℝ] ℝ) (L : ℕ) (z : ℝ) :
    A.jetChartMap i (A.periodicAtlasAnsatz i F U ℓ L z) =
      spaceCoordinates ∘ finiteAnsatz (A.vectorChartRead i F) U ℓ L z := by
…

    Mentions: OAI.ClosedSurfaceR4.Space, OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.spaceCoordinates

  5. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.periodicAtlasAnsatz_eventuallyEq line 79

    Source documentation

    Outside the original chart support the global ansatz retains the exact baseline germ, including all boundary jets on the exterior.

    lemma periodicAtlasAnsatz_eventuallyEq (i : A.centers) (F : M → Space)
    {O : TopologicalSpace.Opens JetPolynomial.Base} (U : ℕ → Family O Space)
    {K : Set JetPolynomial.Base} (hK : IsClosed K)
    (hKA : K ⊆ (A.chartWeightCompact i : Set JetPolynomial.Base))
    (hzero : ∀ j x, x ∉ K → (U j).val x = 0)
    (ℓ : JetPolynomial.Base →L[ℝ] ℝ) (L : ℕ) (z : ℝ)
    {p : M} (hp : p ∉ tsupport (A.weight i)) :
    A.periodicAtlasAnsatz i F U ℓ L z =ᶠ[𝓝 p] F := by
…

    Mentions: OAI.ClosedSurfaceR4.Space, OAI.ClosedSurfaceR4.JetPolynomial.Base