theorem
ENNReal.lintegral_prod_norm_pow_le'
{α : Type u_2}
{ι : Type u_3}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{s : Finset ι}
{f : ι → α → ENNReal}
(hf : ∀ i ∈ s, AEMeasurable (f i) μ)
{p : ι → ENNReal}
(hp : ∑ i ∈ s, (p i)⁻¹ = 1)
:
A version of Hölder with multiple arguments, allowing ∞ as an exponent.
theorem
ENNReal.lintegral_mul_le_eLpNorm_mul_eLqNorm
{α : Type u_1}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{p q : ENNReal}
(hpq : p.HolderConjugate q)
{f g : α → ENNReal}
(hf : AEMeasurable f μ)
(hg : AEMeasurable g μ)
:
Hölder's inequality for functions α → ℝ≥0∞, using exponents in ℝ≥0∞
theorem
ENNReal.sq_lintegral_mul_le_mul_lintegral_sq
{α : Type u_1}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{f g : α → ENNReal}
(hf : AEMeasurable f μ)
(hg : AEMeasurable g μ)
:
Cauchy–Schwarz inequality for functions α → ℝ≥0∞ (Hölder's inequality squared).
theorem
ENNReal.eLpNorm_top_convolution_le
{𝕜 : Type u𝕜}
{G : Type uG}
[MeasurableSpace G]
{μ : MeasureTheory.Measure G}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[NormedAddCommGroup E]
[NormedAddCommGroup E']
[NormedAddCommGroup F]
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 E']
[NormedSpace 𝕜 F]
[NormedSpace ℝ F]
{L : E →L[𝕜] E' →L[𝕜] F}
[AddGroup G]
[TopologicalSpace G]
[IsTopologicalAddGroup G]
[BorelSpace G]
[μ.IsAddHaarMeasure]
[LocallyCompactSpace G]
[SecondCountableTopology G]
[MeasurableSpace E]
[OpensMeasurableSpace E]
[MeasurableSpace E']
[OpensMeasurableSpace E']
[μ.IsNegInvariant]
{p q : ENNReal}
(hpq : p.HolderConjugate q)
{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‖)
:
MeasureTheory.eLpNorm (MeasureTheory.convolution f g L μ) ⊤ μ ≤ ENNReal.ofReal c * MeasureTheory.eLpNorm f p μ * MeasureTheory.eLpNorm g q μ
Special case of Young's convolution inequality when r = ∞.
theorem
ENNReal.eLpNorm_top_convolution_le'
{𝕜 : Type u𝕜}
{G : Type uG}
[MeasurableSpace G]
{μ : MeasureTheory.Measure G}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[NormedAddCommGroup E]
[NormedAddCommGroup E']
[NormedAddCommGroup F]
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 E']
[NormedSpace 𝕜 F]
[NormedSpace ℝ F]
{L : E →L[𝕜] E' →L[𝕜] F}
[AddGroup G]
[TopologicalSpace G]
[IsTopologicalAddGroup G]
[BorelSpace G]
[μ.IsAddHaarMeasure]
[LocallyCompactSpace G]
[SecondCountableTopology G]
[μ.IsNegInvariant]
{p q : ENNReal}
(hpq : p.HolderConjugate q)
{f : G → E}
{g : G → E'}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(hg : MeasureTheory.AEStronglyMeasurable g μ)
(c : ℝ)
(hL : ∀ (x y : G), ‖(L (f x)) (g y)‖ ≤ c * ‖f x‖ * ‖g y‖)
:
MeasureTheory.eLpNorm (MeasureTheory.convolution f g L μ) ⊤ μ ≤ ENNReal.ofReal c * MeasureTheory.eLpNorm f p μ * MeasureTheory.eLpNorm g q μ
Special case of Young's convolution inequality when r = ∞.
theorem
ENNReal.enorm_convolution_le_eLpNorm_mul_eLpNorm_mul_eLpNorm
{𝕜 : Type u𝕜}
{G : Type uG}
[MeasurableSpace G]
{μ : MeasureTheory.Measure G}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[NormedAddCommGroup E]
[NormedAddCommGroup E']
[NormedAddCommGroup F]
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 E']
[NormedSpace 𝕜 F]
[NormedSpace ℝ F]
{L : E →L[𝕜] E' →L[𝕜] F}
[AddGroup G]
[TopologicalSpace G]
[IsTopologicalAddGroup G]
[BorelSpace G]
[μ.IsAddHaarMeasure]
[LocallyCompactSpace G]
[SecondCountableTopology G]
[MeasurableSpace E]
[OpensMeasurableSpace E]
[MeasurableSpace E']
[OpensMeasurableSpace E']
[μ.IsNegInvariant]
{p q r : ℝ}
(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‖)
(x : G)
:
‖MeasureTheory.convolution f g L μ x‖ₑ ≤ ENNReal.ofReal c * MeasureTheory.eLpNorm (fun (y : G) => (‖f y‖ₑ ^ p * ‖g (x - y)‖ₑ ^ q) ^ (1 / r)) (ENNReal.ofReal r) μ * (MeasureTheory.eLpNorm f (ENNReal.ofReal p) μ ^ ((r - p) / r) * MeasureTheory.eLpNorm g (ENNReal.ofReal q) μ ^ ((r - q) / r))
This inequality is used in the proof of Young's convolution inequality
eLpNorm_convolution_le_ofReal. See enorm_convolution_le_eLpNorm_mul_eLpNorm_mul_eLpNorm' for
a version assuming a.e. strong measurability instead.
theorem
ENNReal.enorm_convolution_le_eLpNorm_mul_eLpNorm_mul_eLpNorm'
{𝕜 : Type u𝕜}
{G : Type uG}
[MeasurableSpace G]
{μ : MeasureTheory.Measure G}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[NormedAddCommGroup E]
[NormedAddCommGroup E']
[NormedAddCommGroup F]
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 E']
[NormedSpace 𝕜 F]
[NormedSpace ℝ F]
{L : E →L[𝕜] E' →L[𝕜] F}
[AddGroup G]
[TopologicalSpace G]
[IsTopologicalAddGroup G]
[BorelSpace G]
[μ.IsAddHaarMeasure]
[LocallyCompactSpace G]
[SecondCountableTopology G]
[μ.IsNegInvariant]
{p q r : ℝ}
(hp : 1 ≤ p)
(hq : 1 ≤ q)
(hr : 1 ≤ r)
(hpqr : p⁻¹ + q⁻¹ = r⁻¹ + 1)
{f : G → E}
{g : G → E'}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(hg : MeasureTheory.AEStronglyMeasurable g μ)
(c : ℝ)
(hL : ∀ (x y : G), ‖(L (f x)) (g y)‖ ≤ c * ‖f x‖ * ‖g y‖)
(x : G)
:
‖MeasureTheory.convolution f g L μ x‖ₑ ≤ ENNReal.ofReal c * MeasureTheory.eLpNorm (fun (y : G) => (‖f y‖ₑ ^ p * ‖g (x - y)‖ₑ ^ q) ^ (1 / r)) (ENNReal.ofReal r) μ * (MeasureTheory.eLpNorm f (ENNReal.ofReal p) μ ^ ((r - p) / r) * MeasureTheory.eLpNorm g (ENNReal.ofReal q) μ ^ ((r - q) / r))
This inequality is used in the proof of Young's convolution inequality
eLpNorm_convolution_le_ofReal'.
theorem
ENNReal.eLpNorm_convolution_le_ofReal
{𝕜 : Type u𝕜}
{G : Type uG}
[MeasurableSpace G]
{μ : MeasureTheory.Measure G}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[NormedAddCommGroup E]
[NormedAddCommGroup E']
[NormedAddCommGroup F]
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 E']
[NormedSpace 𝕜 F]
[NormedSpace ℝ F]
{L : E →L[𝕜] E' →L[𝕜] F}
[AddGroup G]
[TopologicalSpace G]
[IsTopologicalAddGroup G]
[BorelSpace G]
[μ.IsAddHaarMeasure]
[LocallyCompactSpace G]
[SecondCountableTopology G]
[MeasurableSpace E]
[OpensMeasurableSpace E]
[MeasurableSpace E']
[OpensMeasurableSpace E']
[μ.IsAddRightInvariant]
{p q r : ℝ}
(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‖)
:
MeasureTheory.eLpNorm (MeasureTheory.convolution f g L μ) (ENNReal.ofReal r) μ ≤ ENNReal.ofReal c * MeasureTheory.eLpNorm f (ENNReal.ofReal p) μ * MeasureTheory.eLpNorm g (ENNReal.ofReal q) μ
theorem
ENNReal.eLpNorm_convolution_le_ofReal'
{𝕜 : Type u𝕜}
{G : Type uG}
[MeasurableSpace G]
{μ : MeasureTheory.Measure G}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[NormedAddCommGroup E]
[NormedAddCommGroup E']
[NormedAddCommGroup F]
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 E']
[NormedSpace 𝕜 F]
[NormedSpace ℝ F]
{L : E →L[𝕜] E' →L[𝕜] F}
[AddGroup G]
[TopologicalSpace G]
[IsTopologicalAddGroup G]
[BorelSpace G]
[μ.IsAddHaarMeasure]
[LocallyCompactSpace G]
[SecondCountableTopology G]
[μ.IsAddRightInvariant]
{p q r : ℝ}
(hp : 1 ≤ p)
(hq : 1 ≤ q)
(hr : 1 ≤ r)
(hpqr : p⁻¹ + q⁻¹ = r⁻¹ + 1)
{f : G → E}
{g : G → E'}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(hg : MeasureTheory.AEStronglyMeasurable g μ)
(c : ℝ)
(hL : ∀ (x y : G), ‖(L (f x)) (g y)‖ ≤ c * ‖f x‖ * ‖g y‖)
:
MeasureTheory.eLpNorm (MeasureTheory.convolution f g L μ) (ENNReal.ofReal r) μ ≤ ENNReal.ofReal c * MeasureTheory.eLpNorm f (ENNReal.ofReal p) μ * MeasureTheory.eLpNorm g (ENNReal.ofReal q) μ
theorem
ENNReal.eLpNorm_convolution_le_of_norm_le_mul
{𝕜 : Type u𝕜}
{G : Type uG}
[MeasurableSpace G]
{μ : MeasureTheory.Measure G}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[NormedAddCommGroup E]
[NormedAddCommGroup E']
[NormedAddCommGroup F]
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 E']
[NormedSpace 𝕜 F]
[NormedSpace ℝ F]
(L : E →L[𝕜] E' →L[𝕜] F)
[AddGroup G]
[TopologicalSpace G]
[IsTopologicalAddGroup G]
[BorelSpace G]
[μ.IsAddHaarMeasure]
[LocallyCompactSpace G]
[SecondCountableTopology G]
[MeasurableSpace E]
[OpensMeasurableSpace E]
[MeasurableSpace E']
[OpensMeasurableSpace E']
[μ.IsAddRightInvariant]
{p q r : ENNReal}
(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‖)
:
MeasureTheory.eLpNorm (MeasureTheory.convolution f g L μ) r μ ≤ ENNReal.ofReal c * MeasureTheory.eLpNorm f p μ * MeasureTheory.eLpNorm g q μ
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.
theorem
ENNReal.eLpNorm_convolution_le_of_norm_le_mul'
{𝕜 : Type u𝕜}
{G : Type uG}
[MeasurableSpace G]
{μ : MeasureTheory.Measure G}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[NormedAddCommGroup E]
[NormedAddCommGroup E']
[NormedAddCommGroup F]
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 E']
[NormedSpace 𝕜 F]
[NormedSpace ℝ F]
(L : E →L[𝕜] E' →L[𝕜] F)
[AddGroup G]
[TopologicalSpace G]
[IsTopologicalAddGroup G]
[BorelSpace G]
[μ.IsAddHaarMeasure]
[LocallyCompactSpace G]
[SecondCountableTopology G]
[μ.IsAddRightInvariant]
{p q r : ENNReal}
(hp : 1 ≤ p)
(hq : 1 ≤ q)
(hr : 1 ≤ r)
(hpqr : p⁻¹ + q⁻¹ = r⁻¹ + 1)
{f : G → E}
{g : G → E'}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(hg : MeasureTheory.AEStronglyMeasurable g μ)
(c : ℝ)
(hL : ∀ (x y : G), ‖(L (f x)) (g y)‖ ≤ c * ‖f x‖ * ‖g y‖)
:
MeasureTheory.eLpNorm (MeasureTheory.convolution f g L μ) r μ ≤ ENNReal.ofReal c * MeasureTheory.eLpNorm f p μ * MeasureTheory.eLpNorm g q μ
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.
theorem
ENNReal.eLpNorm_convolution_le_enorm_mul
{𝕜 : Type u𝕜}
{G : Type uG}
[MeasurableSpace G]
{μ : MeasureTheory.Measure G}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[NormedAddCommGroup E]
[NormedAddCommGroup E']
[NormedAddCommGroup F]
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 E']
[NormedSpace 𝕜 F]
[NormedSpace ℝ F]
(L : E →L[𝕜] E' →L[𝕜] F)
[AddGroup G]
[TopologicalSpace G]
[IsTopologicalAddGroup G]
[BorelSpace G]
[μ.IsAddHaarMeasure]
[LocallyCompactSpace G]
[SecondCountableTopology G]
[MeasurableSpace E]
[OpensMeasurableSpace E]
[MeasurableSpace E']
[OpensMeasurableSpace E']
[μ.IsAddRightInvariant]
{p q r : ENNReal}
(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 μ)
:
MeasureTheory.eLpNorm (MeasureTheory.convolution f g L μ) r μ ≤ ‖L‖ₑ * MeasureTheory.eLpNorm f p μ * MeasureTheory.eLpNorm g q μ
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.
theorem
ENNReal.eLpNorm_convolution_le_enorm_mul'
{𝕜 : Type u𝕜}
{G : Type uG}
[MeasurableSpace G]
{μ : MeasureTheory.Measure G}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[NormedAddCommGroup E]
[NormedAddCommGroup E']
[NormedAddCommGroup F]
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 E']
[NormedSpace 𝕜 F]
[NormedSpace ℝ F]
(L : E →L[𝕜] E' →L[𝕜] F)
[AddGroup G]
[TopologicalSpace G]
[IsTopologicalAddGroup G]
[BorelSpace G]
[μ.IsAddHaarMeasure]
[LocallyCompactSpace G]
[SecondCountableTopology G]
[μ.IsAddRightInvariant]
{p q r : ENNReal}
(hp : 1 ≤ p)
(hq : 1 ≤ q)
(hr : 1 ≤ r)
(hpqr : p⁻¹ + q⁻¹ = r⁻¹ + 1)
{f : G → E}
{g : G → E'}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(hg : MeasureTheory.AEStronglyMeasurable g μ)
:
MeasureTheory.eLpNorm (MeasureTheory.convolution f g L μ) r μ ≤ ‖L‖ₑ * MeasureTheory.eLpNorm f p μ * MeasureTheory.eLpNorm g q μ
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.
theorem
ENNReal.eLpNorm_Ioc_convolution_le_of_norm_le_mul_aux
{𝕜 : Type u𝕜}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[NormedAddCommGroup E]
[NormedAddCommGroup E']
[NormedAddCommGroup F]
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 E']
[NormedSpace 𝕜 F]
[NormedSpace ℝ F]
(L : E →L[𝕜] E' →L[𝕜] F)
(a : ℝ)
{T : ℝ}
[hT : Fact (0 < T)]
{p q r : ENNReal}
(hp : 1 ≤ p)
(hq : 1 ≤ q)
(hr : 1 ≤ r)
(hpqr : p⁻¹ + q⁻¹ = r⁻¹ + 1)
{f : ℝ → E}
{g : ℝ → E'}
(hfT : Function.Periodic f T)
(hgT : Function.Periodic g T)
(hf : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume)
(hg : MeasureTheory.AEStronglyMeasurable g MeasureTheory.volume)
(c : ℝ)
(hL : ∀ (x y : ℝ), ‖(L (f x)) (g y)‖ ≤ c * ‖f x‖ * ‖g y‖)
:
MeasureTheory.eLpNorm (fun (x : ℝ) => ∫ (y : ℝ) in a..a + T, (L (f y)) (g (x - y))) r
(MeasureTheory.volume.restrict (Set.Ioc a (a + T))) ≤ ENNReal.ofReal c * MeasureTheory.eLpNorm f p (MeasureTheory.volume.restrict (Set.Ioc a (a + T))) * MeasureTheory.eLpNorm g q (MeasureTheory.volume.restrict (Set.Ioc a (a + T)))
theorem
ENNReal.eLpNorm_Ioc_convolution_le_of_norm_le_mul
{𝕜 : Type u𝕜}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[NormedAddCommGroup E]
[NormedAddCommGroup E']
[NormedAddCommGroup F]
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 E']
[NormedSpace 𝕜 F]
[NormedSpace ℝ F]
(L : E →L[𝕜] E' →L[𝕜] F)
(a : ℝ)
{T : ℝ}
[hT : Fact (0 < T)]
{p q r : ENNReal}
(hp : 1 ≤ p)
(hq : 1 ≤ q)
(hr : 1 ≤ r)
(hpqr : p⁻¹ + q⁻¹ = r⁻¹ + 1)
{f : ℝ → E}
{g : ℝ → E'}
(hgT : Function.Periodic g T)
(hf : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume)
(hg : MeasureTheory.AEStronglyMeasurable g MeasureTheory.volume)
(c : ℝ)
(hL : ∀ (x y : ℝ), ‖(L (f x)) (g y)‖ ≤ c * ‖f x‖ * ‖g y‖)
:
MeasureTheory.eLpNorm (fun (x : ℝ) => ∫ (y : ℝ) in a..a + T, (L (f y)) (g (x - y))) r
(MeasureTheory.volume.restrict (Set.Ioc a (a + T))) ≤ ENNReal.ofReal c * MeasureTheory.eLpNorm f p (MeasureTheory.volume.restrict (Set.Ioc a (a + T))) * MeasureTheory.eLpNorm g q (MeasureTheory.volume.restrict (Set.Ioc a (a + T)))
Young's convolution inequality on (a, a + T]: the L^r seminorm of the convolution
of T-periodic functions over (a, a + T] is bounded by ‖L‖ₑ times the product of
the L^p and L^q seminorms on that interval, 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_Ioc_convolution_le_enorm_mul for a version using ‖L‖ₑ explicitly.
theorem
ENNReal.eLpNorm_Ioc_convolution_le_enorm_mul
{𝕜 : Type u𝕜}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[NormedAddCommGroup E]
[NormedAddCommGroup E']
[NormedAddCommGroup F]
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 E']
[NormedSpace 𝕜 F]
[NormedSpace ℝ F]
(L : E →L[𝕜] E' →L[𝕜] F)
(a : ℝ)
{T : ℝ}
[hT : Fact (0 < T)]
{p q r : ENNReal}
(hp : 1 ≤ p)
(hq : 1 ≤ q)
(hr : 1 ≤ r)
(hpqr : p⁻¹ + q⁻¹ = r⁻¹ + 1)
{f : ℝ → E}
{g : ℝ → E'}
(hgT : Function.Periodic g T)
(hf : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume)
(hg : MeasureTheory.AEStronglyMeasurable g MeasureTheory.volume)
:
MeasureTheory.eLpNorm (fun (x : ℝ) => ∫ (y : ℝ) in a..a + T, (L (f y)) (g (x - y))) r
(MeasureTheory.volume.restrict (Set.Ioc a (a + T))) ≤ ‖L‖ₑ * MeasureTheory.eLpNorm f p (MeasureTheory.volume.restrict (Set.Ioc a (a + T))) * MeasureTheory.eLpNorm g q (MeasureTheory.volume.restrict (Set.Ioc a (a + T)))
Young's convolution inequality on (a, a + T]: the L^r seminorm of the convolution
of T-periodic functions over (a, a + T] is bounded by ‖L‖ₑ times the product of
the L^p and L^q seminorms on that interval, where 1 / p + 1 / q = 1 / r + 1.