NonlinearAtlasErrorBound.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Exact decomposition of a global primitive's metric defect into the solved polynomial mean error and the finite periodic remainder.

lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.phaseAtlasRemainder_smooth line 33

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.phaseAtlasAnsatz_error_bound line 61

Source documentation

A local phase remainder and the actual solved mean control the global metric error.

theorem phaseAtlasAnsatz_error_bound (i : A.centers)
    (e : OpenPartialHomeomorph JetPolynomial.Base JetPolynomial.Base)
    (he : ContDiff ℝ ∞ e) (hi : ContDiff ℝ ∞ e.symm)
    {χ : JetPolynomial.Base → ℝ} (hχ : ContDiff ℝ ∞ χ)
    (hχc : HasCompactSupport χ) (hχs : tsupport χ ⊆ e.source)
    {W : Set JetPolynomial.Base} (hW : IsOpen W) (hTW : MapsTo e e.source W) (m : ℕ) :
    ∃ D : ℝ, 0 ≤ D ∧ ∀ (F : M → Space), ContMDiff planeModel spaceModel ∞ F →
    ∀ (O : TopologicalSpace.Opens JetPolynomial.Base) (U : ℕ → Family O Space)
      (K : Set JetPolynomial.Base), IsCompact K → K ⊆ O →
      e.symm '' K ⊆ (A.chartWeightCompact i : Set JetPolynomial.Base) →
      (∀ j x, x ∉ K → (U j).val x = 0) →
      (∀ x ∈ e.symm '' K, χ x = 1) →
…

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