AtlasTensorLocalBounds.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.tensorPlaneRestore_bound_on_outer line 33

Source documentation

Compact coordinate bounds on the outer supports suffice for global restoration.

theorem tensorPlaneRestore_bound_on_outer
    (U : A.centers → Set JetPolynomial.Base) (hU : ∀ i, IsOpen (U i))
    (houter : ∀ i : A.centers, (chart (i : M)) '' tsupport (A.outer i) ⊆ U i)
    (m : ℕ) :
    ∃ D : ℝ, 0 ≤ D ∧ ∀ (f : A.centers → SmallModes.Base → Tensor),
      (∀ i, ContDiff ℝ ∞ (f i)) → ∀ (s C : ℝ), 0 < s → s ≤ 1 → 0 ≤ C →
      (∀ i, WeightedEstimates.WeightedBound (planeCoordinateIsometry.symm ⁻¹' U i) s m C (f i)) →
      A.TensorWeightedBound s m (D*C) (A.tensorPlaneRestore f) := by
…

Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.chart, OAI.ClosedSurfaceR4.SmallModes.Base, OAI.ClosedSurfaceR4.WeightedEstimates.WeightedBound