Source indexedtheorem · leanprover/lean4:v4.32.0

ENNReal.eLpNorm_convolution_le_of_norm_le_mul

Carleson.ToMathlib.MeasureTheory.Integral.MeanInequalities · Carleson/ToMathlib/MeasureTheory/Integral/MeanInequalities.lean:444 to 454

Source documentation

Young's convolution inequality: the L^r seminorm of a convolution (f ⋆[L, μ] g) is bounded by ‖L‖ₑ times the product of the L^p and L^q seminorms, where 1 / p + 1 / q = 1 / r + 1. Here ‖L‖ₑ is replaced with a bound for L restricted to the ranges of f and g; see eLpNorm_convolution_le_enorm_mul for a version using ‖L‖ₑ explicitly.

Exact Lean statement

theorem eLpNorm_convolution_le_of_norm_le_mul [MeasurableSpace E] [OpensMeasurableSpace E]
    [MeasurableSpace E'] [OpensMeasurableSpace E']
    [μ.IsAddRightInvariant] {p q r : ℝ≥0∞}
    (hp : 1 ≤ p) (hq : 1 ≤ q) (hr : 1 ≤ r) (hpqr : p⁻¹ + q⁻¹ = r⁻¹ + 1)
    {f : G → E} {g : G → E'} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ)
    (c : ℝ) (hL : ∀ (x y : G), ‖L (f x) (g y)‖ ≤ c * ‖f x‖ * ‖g y‖) :
    eLpNorm (f ⋆[L, μ] g) r μ ≤ .ofReal c * eLpNorm f p μ * eLpNorm g q μ

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem eLpNorm_convolution_le_of_norm_le_mul [MeasurableSpace E] [OpensMeasurableSpace E]    [MeasurableSpace E'] [OpensMeasurableSpace E']    [μ.IsAddRightInvariant] {p q r : ℝ≥0∞}    (hp : 1 ≤ p) (hq : 1 ≤ q) (hr : 1 ≤ r) (hpqr : p⁻¹ + q⁻¹ = r⁻¹ + 1)    {f : G → E} {g : G → E'} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ)    (c : ℝ) (hL : ∀ (x y : G), ‖L (f x) (g y)‖ ≤ c * ‖f x‖ * ‖g y‖) :    eLpNorm (f ⋆[L, μ] g) r μ ≤ .ofReal c * eLpNorm f p μ * eLpNorm g q μ := by  refine eLpNorm_convolution_le_of_norm_le_mul_aux hp hq hr hpqr hf.enorm ?_ ?_ ?_ c hL  · intro x; exact hg.enorm.comp_quasiMeasurePreserving (quasiMeasurePreserving_sub_left μ x)  · intro x; exact eLpNorm_comp_measurePreserving' hg (μ.measurePreserving_sub_left x)  · exact hg.comp_quasiMeasurePreserving (quasiMeasurePreserving_sub μ μ) |>.enorm.pow_const _