EuclideanRadialKernelDerivative.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Second derivative bounds for radial averaging

theorem OAI.RegularPointCoordinates.euclideanRadialKernel_second_bound line 15
Source documentation
Only one fixed compact kernel contributes to the dimensional constant; every change of radius contributes exactly its inverse square.
```
theorem euclideanRadialKernel_second_bound (n : ℕ) :
    ∃ J : ℝ, 0 < J ∧ ∀ r : ℝ, 0 < r → ∀ x : Euclidean n,
      ‖iteratedFDeriv ℝ 2 (euclideanRadialKernel n r) x‖ ≤ J/r^2 := by
…
```
Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.euclideanRadialKernel

theorem OAI.RegularPointCoordinates.euclideanRadialConvolution_hessian_bound line 44

Source documentation

The Hessian of an actual convolution is bounded using the L¹ mass of its first factor and the inverse-square kernel estimate.

theorem euclideanRadialConvolution_hessian_bound (n : ℕ) :
    ∃ C : ℝ, 0 < C ∧ ∀ r : ℝ, 0 < r →
      ∀ f : Euclidean n → ℝ, Integrable f volume → ∀ x : Euclidean n,
      ‖fderiv ℝ (fderiv ℝ (f ⋆[ContinuousLinearMap.mul ℝ ℝ,volume] euclideanRadialKernel n r)) x‖ ≤
        (C/r^2)*(∫ y, |f y|) := by
…

Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.euclideanRadialKernel