AtlasPrimitiveLocalErrorBound.lean`

1 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.

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.periodicAtlasAnsatz_error_bound_on_outer line 30

Source documentation

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

theorem periodicAtlasAnsatz_error_bound_on_outer (i : A.centers)
    {V : Set JetPolynomial.Base} (hV : IsOpen V)
    (houter : (chart (i : M)) '' tsupport (A.outer i) ⊆ V) (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)) ∞
…

Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.chart, OAI.ClosedSurfaceR4.Space, OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.CovariantTwoTensor, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.TensorFiber