L^p bounds for normalized convolution #
The proof uses Jensen for |·|^p, translation invariance, and Tonelli. The
result is the contraction estimate needed in the density argument for
mollification.
theorem
CKN.young_convolution_nonneg_integral_one
{d : ℕ}
{ρ g : Vec d → ℝ}
{p : ENNReal}
(hp : 1 ≤ p)
(hp_top : p ≠ ⊤)
(hρ_nonneg : ∀ (x : Vec d), 0 ≤ ρ x)
(hρ_int : MeasureTheory.Integrable ρ MeasureTheory.volume)
(hρ_one : ∫ (x : Vec d), ρ x = 1)
(hρ_meas : Measurable ρ)
(hg_meas : Measurable g)
:
theorem
CKN.young_convolution_nonneg_integral_one_of_aemeasurable
{d : ℕ}
{ρ g : Vec d → ℝ}
{p : ENNReal}
(hp : 1 ≤ p)
(hp_top : p ≠ ⊤)
(hρ_nonneg : ∀ (x : Vec d), 0 ≤ ρ x)
(hρ_int : MeasureTheory.Integrable ρ MeasureTheory.volume)
(hρ_one : ∫ (x : Vec d), ρ x = 1)
(hρ_meas : Measurable ρ)
(hg_meas : AEMeasurable g MeasureTheory.volume)
: