AtlasPolynomialInteractionBounds.lean`

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

lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.atlasPolynomialQuadratic_difference line 35

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

Source documentation

The mixed polynomial error is cubic in the correction amplitude after using the fixed loss condition.

theorem atlas_polynomial_interaction_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 D : A.centers → ℝ) (hB : ∀ i, 1 ≤ B i)
    (hC : ∀ i, 0 < C i) (hD : ∀ i, 0 < D i) :
    ∃ E : ℝ, 0 ≤ E ∧ ∀ (F X Y : M → Space),
      ContMDiff planeModel spaceModel ∞ F → ContMDiff planeModel spaceModel ∞ X →
      ContMDiff planeModel spaceModel ∞ Y →
      ∀ τ ε δ : ℝ, 0 < τ → τ ≤ 1 → 0 ≤ ε → ε ≤ 1 → 0 < δ → δ ≤ τ →
…

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