AtlasPrimitiveErrorBound.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A local finite periodic remainder and a global solved mean error control the metric of the actual globally restored primitive.

def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.periodicAtlasRemainder line 28
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.periodicAtlasRemainder_smooth line 38

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.periodicAtlasAnsatz_error_bound line 58

Source documentation

No error is lost in globalization; the only new constant is the fixed single-patch tensor restoration norm.

theorem periodicAtlasAnsatz_error_bound (i : A.centers) (m : ℕ) :
    ∃ D : ℝ, 0 ≤ D ∧ ∀ (F : M → Space), ContMDiff planeModel spaceModel ∞ F →
    ∀ (O : TopologicalSpace.Opens JetPolynomial.Base) (U : ℕ → Family O Space)
      (K : Set JetPolynomial.Base), IsClosed K → K ⊆ O →
      K ⊆ (A.chartWeightCompact i : Set JetPolynomial.Base) →
      (∀ j x, x ∉ K → (U j).val x = 0) →
    ∀ (ℓ : JetPolynomial.Base →L[ℝ] ℝ) (L : ℕ) (z : ℝ) (n : ℕ)
      (P : Fin 3 → Fin n → Expression), (∀ k r, (P k r).SmoothCoeffs univ) →
    ∀ (γ : ∀ x : M, CovariantTwoTensor x),
      ContMDiff planeModel (planeModel.prod 𝓘(ℝ,TensorFiber)) ∞
        (fun x => TotalSpace.mk' TensorFiber x (γ x)) →
    ∀ (H : SmallModes.Base → PhaseMean.Tensor), ContDiff ℝ ∞ H →
…

Mentions: OAI.ClosedSurfaceR4.Space, OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.CovariantTwoTensor, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.TensorFiber, OAI.ClosedSurfaceR4.SmallModes.Base, OAI.ClosedSurfaceR4.PhaseMean.Tensor