FiniteSmootherWeighted.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Weighted bounds for finite-order smoothing in the chart norms used by the correction iteration.

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.finiteSmooth_weighted_bounded line 18

Source documentation

Smoothing at one scale remains bounded in the original weighted norm at any other positive scale.

theorem finiteSmooth_weighted_bounded (n m : ℕ) {s t C : ℝ}
    (hs : 0 < s) (ht : 0 < t) {f : Base → E}
    (hf : ContDiff ℝ ∞ f) (hfc : HasCompactSupport f)
    (hb : WeightedBound Set.univ t m C f) :
    WeightedBound Set.univ t m ((1 + (1 + ∫ y, ‖kernel 0 y‖) ^ n) * C)
      (finiteSmooth n s f) := by
…

Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.kernel, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.finiteSmooth

def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.weightedGainConstant line 33
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.weightedGainConstant_nonneg line 36
theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.finiteSmooth_weighted_gain line 41
Source documentation
Every weighted output derivative is controlled by the zeroth input norm; higher input derivatives do not enter the constant.
```
theorem finiteSmooth_weighted_gain (n m : ℕ) {s C : ℝ} (hs : 0 < s)
    {f : Base → E} (hf : ContDiff ℝ ∞ f) (hb : ∀ x, ‖f x‖ ≤ C) :
    WeightedBound Set.univ s m (weightedGainConstant n m * C) (finiteSmooth n s f) := by
…
```
Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.weightedGainConstant, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.finiteSmooth