AtlasPrimitiveExpansion.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Construct the actual globally supported primitive from the finite recursion and its extended polynomial mean operator.

lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.euclidean_jetChartMap line 30
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.periodicAtlasRemainder_mean line 37

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.supported_primitive_metric line 53

Source documentation

The extended mean is chosen once. Its actual periodic realization is then available uniformly for all admissible nearby maps and small scales.

theorem supported_primitive_metric (i : A.centers)
    {O : TopologicalSpace.Opens LowJet} (l : SurfaceVelocityFamily.Loop O)
    {a : JetPolynomial.Base → ℝ} (ha : ContDiff ℝ ∞ a) (hamp : l.HasSpatialAmplitude a)
    (S : TopologicalSpace.Opens JetPolynomial.Base)
    (houter : (chart (i : M)) '' tsupport (A.outer i) ⊆ S)
    {Q : Set LowJet} (hQ : IsCompact Q) (hQO : Q ⊆ O)
    (n : ℕ) (ℓ : JetPolynomial.Base →L[ℝ] ℝ)
    (hℓx : ℓ (coordinateVector 0) = 1) (hℓy : ℓ (coordinateVector 1) = 0) :
    ∃ P : Fin 3 → Fin n → Expression, (∀ k r, (P k r).SmoothCoeffs univ) ∧
    ∃ loss : ℕ, ∀ (m : ℕ) (B : ℝ), 1 ≤ B → ∃ Dv D : ℝ, 0 ≤ Dv ∧ 0 ≤ D ∧
      ∀ (G : M → Space) (hG : ContMDiff planeModel spaceModel ∞ G)
        (hGQ : MapsTo (lowJet (A.jetChartMap i G)) S Q),
…

Mentions: OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop, OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.chart, OAI.ClosedSurfaceR4.Space, OAI.ClosedSurfaceR4.planeModel