AtlasPolynomialIncrementBound.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_increment_bound line 38

Source documentation

Combine the actual free, forced and mean residuals, with the derived mixed-polynomial and Taylor bounds, into a bound for the changed metric.

theorem atlas_polynomial_increment_bound (m : ℕ) (A₀ B₀ : ℝ)
    (hA : 0 ≤ A₀) (hB : 0 ≤ B₀) :
    ∃ D : ℝ, 0 ≤ D ∧ ∀ {n : A.centers → ℕ}
      (P : ∀ i : A.centers, Fin 3 → Fin (n i) → Expression)
      (_hP : ∀ i k l, (P i k l).SmoothCoeffs univ)
      (F U V : M → Space), ContMDiff planeModel spaceModel ∞ F →
      ContMDiff planeModel spaceModel ∞ U → ContMDiff planeModel spaceModel ∞ V →
      ∀ (T H : ∀ p : M, CovariantTwoTensor p),
      ContMDiff planeModel (planeModel.prod 𝓘(ℝ,TensorFiber)) ∞
        (fun p => TotalSpace.mk' TensorFiber p (T p)) →
      ContMDiff planeModel (planeModel.prod 𝓘(ℝ,TensorFiber)) ∞
        (fun p => TotalSpace.mk' TensorFiber p (H p)) →
…

Mentions: OAI.ClosedSurfaceR4.Space, OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.CovariantTwoTensor, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.TensorFiber