SmoothingNormBounds.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Scale-independent zeroth-order bounds for the constructed smoothing operator, including the signed finite-moment kernels.

lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.norm_dilate line 14
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.norm_mass_dilate line 19
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.smooth_norm_le line 28
Source documentation
Signed moment cancellation does not cost a power of the smoothing scale: the operator bound is the fixed L1 norm of the chosen kernel.
```
lemma smooth_norm_le (r : ℕ) {s C : ℝ} (hs : 0 < s) {f : Base → E}
    (hf : ∀ x, ‖f x‖ ≤ C) (x : Base) :
    ‖smooth r s f x‖ ≤ (∫ y, ‖kernel r y‖) * C := by
…
```
Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.smooth, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.kernel