AtlasPolynomialRemainderBounds.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The restored polynomial value has one fixed finite loss. Compact local jet ranges suffice: a fixed cutoff removes the irrelevant values away from the outer atlas supports before applying the restoration estimate.

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.atlas_polynomial_remainder_bound line 35

Source documentation

The cubic Taylor remainder of the actual global polynomial metric.

theorem atlas_polynomial_remainder_bound {n : A.centers → ℕ}
    (P : ∀ i : A.centers, Fin 3 → Fin (n i) → Expression)
    (hP : ∀ i k l, (P i k l).SmoothCoeffs univ)
    (U : A.centers → Set JetPolynomial.Base) (hU : ∀ i, IsOpen (U i))
    (houter : ∀ i : A.centers, (chart (i : M)) '' tsupport (A.outer i) ⊆ U i)
    (Q : A.centers → Set LowJet) (hQ : ∀ i, IsCompact (Q i))
    (m : ℕ) (B C : A.centers → ℝ) (hB : ∀ i, 1 ≤ B i) (hC : ∀ i, 0 < C i) :
    ∃ E : ℝ, 0 ≤ E ∧ ∀ (F X : M → Space),
      ContMDiff planeModel spaceModel ∞ F → ContMDiff planeModel spaceModel ∞ X →
      ∀ τ ε δ : ℝ, 0 < τ → τ ≤ 1 → 0 ≤ ε → ε ≤ 1 → 0 < δ →
      (∀ i, ε/τ^tensorLoss (P i) ≤ 1) →
      (∀ i t, t ∈ Icc (0 : ℝ) 1 → MapsTo
…

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