GlobalSmoothingBounds.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Global smoothing estimates in the fixed finite atlas.

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.smoothing_bounds line 23

Source documentation

Global boundedness and smoothing gain use fixed chart constants and no higher derivative of the true input.

theorem smoothing_bounds (r m : ℕ) :
    ∃ D : ℝ, 0 ≤ D ∧
      (∀ (f : M → V) (s t C : ℝ), 0 < s → 0 < t → t ≤ 1 → 0 ≤ C →
        ContMDiff planeModel 𝓘(ℝ, V) ∞ f → A.WeightedBound t m C f →
        A.WeightedBound t m (D * (1 + (1 + ∫ y, ‖kernel 0 y‖) ^ r) * C) (A.smooth r s f)) ∧
      (∀ (f : M → V) (s t C : ℝ), 0 < s → s ≤ 1 → 0 ≤ C →
        ContMDiff planeModel 𝓘(ℝ, V) ∞ f → A.WeightedBound t 0 C f →
        A.WeightedBound s m (D * weightedGainConstant r m * C) (A.smooth r s f)) := by
…

Mentions: OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.kernel, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.weightedGainConstant

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

Source documentation

The coordinate two-scale estimate survives finite atlas assembly. The large higher input norm still occurs only linearly.

theorem smoothing_tail_bound (r m : ℕ) :
    ∃ D : ℝ, 0 ≤ D ∧ ∀ (f : M → V) (s t τ B C : ℝ),
      0 < τ → τ ≤ s → s ≤ t → t ≤ 1 → 0 ≤ B → 0 ≤ C →
      ContMDiff planeModel 𝓘(ℝ, V) ∞ f →
      A.WeightedBound t r B f → A.WeightedBound t m C f →
      A.WeightedBound τ m
        (D * tailConstant r * (B * (s / t) ^ r + C * (τ / t) ^ r))
        (f - A.smooth r s f) := by
…

Mentions: OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.tailConstant