Compare Lp seminorms for different values of p #
In this file we compare MeasureTheory.eLpNorm' and MeasureTheory.eLpNorm for different
exponents.
theorem
MeasureTheory.eLpNorm'_le_eLpNorm'_mul_rpow_measure_univ
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure α}
{f : α → E}
{p q : ℝ}
(hp0_lt : 0 < p)
(hpq : p ≤ q)
(hf : MeasureTheory.AEStronglyMeasurable f μ)
:
MeasureTheory.eLpNorm' f p μ ≤ MeasureTheory.eLpNorm' f q μ * μ Set.univ ^ (1 / p - 1 / q)
theorem
MeasureTheory.eLpNorm'_le_eLpNormEssSup_mul_rpow_measure_univ
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure α}
{f : α → E}
{q : ℝ}
(hq_pos : 0 < q)
:
MeasureTheory.eLpNorm' f q μ ≤ MeasureTheory.eLpNormEssSup f μ * μ Set.univ ^ (1 / q)
theorem
MeasureTheory.eLpNorm_le_eLpNorm_mul_rpow_measure_univ
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure α}
{f : α → E}
{p q : ENNReal}
(hpq : p ≤ q)
(hf : MeasureTheory.AEStronglyMeasurable f μ)
:
MeasureTheory.eLpNorm f p μ ≤ MeasureTheory.eLpNorm f q μ * μ Set.univ ^ (1 / p.toReal - 1 / q.toReal)
theorem
MeasureTheory.eLpNorm'_le_eLpNorm'_of_exponent_le
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
{f : α → E}
{p q : ℝ}
(hp0_lt : 0 < p)
(hpq : p ≤ q)
(μ : MeasureTheory.Measure α)
[MeasureTheory.IsProbabilityMeasure μ]
(hf : MeasureTheory.AEStronglyMeasurable f μ)
:
MeasureTheory.eLpNorm' f p μ ≤ MeasureTheory.eLpNorm' f q μ
theorem
MeasureTheory.eLpNorm'_le_eLpNormEssSup
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure α}
{f : α → E}
{q : ℝ}
(hq_pos : 0 < q)
[MeasureTheory.IsProbabilityMeasure μ]
:
theorem
MeasureTheory.eLpNorm_le_eLpNorm_of_exponent_le
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure α}
{f : α → E}
{p q : ENNReal}
(hpq : p ≤ q)
[MeasureTheory.IsProbabilityMeasure μ]
(hf : MeasureTheory.AEStronglyMeasurable f μ)
:
MeasureTheory.eLpNorm f p μ ≤ MeasureTheory.eLpNorm f q μ
theorem
MeasureTheory.eLpNorm'_lt_top_of_eLpNorm'_lt_top_of_exponent_le
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure α}
{f : α → E}
{p q : ℝ}
[MeasureTheory.IsFiniteMeasure μ]
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(hfq_lt_top : MeasureTheory.eLpNorm' f q μ < ⊤)
(hp_nonneg : 0 ≤ p)
(hpq : p ≤ q)
:
MeasureTheory.eLpNorm' f p μ < ⊤
theorem
MeasureTheory.Memℒp.mono_exponent
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure α}
{p q : ENNReal}
[MeasureTheory.IsFiniteMeasure μ]
{f : α → E}
(hfq : MeasureTheory.Memℒp f q μ)
(hpq : p ≤ q)
:
MeasureTheory.Memℒp f p μ
@[deprecated MeasureTheory.Memℒp.mono_exponent (since := "2025-01-07")]
theorem
MeasureTheory.Memℒp.memℒp_of_exponent_le
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure α}
{p q : ENNReal}
[MeasureTheory.IsFiniteMeasure μ]
{f : α → E}
(hfq : MeasureTheory.Memℒp f q μ)
(hpq : p ≤ q)
:
MeasureTheory.Memℒp f p μ
Alias of MeasureTheory.Memℒp.mono_exponent.
theorem
MeasureTheory.Memℒp.mono_exponent_of_measure_support_ne_top
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure α}
{p q : ENNReal}
{f : α → E}
(hfq : MeasureTheory.Memℒp f q μ)
{s : Set α}
(hf : ∀ x ∉ s, f x = 0)
(hs : μ s ≠ ⊤)
(hpq : p ≤ q)
:
MeasureTheory.Memℒp f p μ
If a function is supported on a finite-measure set and belongs to ℒ^p, then it belongs to
ℒ^q for any q ≤ p.
@[deprecated MeasureTheory.Memℒp.mono_exponent_of_measure_support_ne_top (since := "2025-01-07")]
theorem
MeasureTheory.Memℒp.memℒp_of_exponent_le_of_measure_support_ne_top
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure α}
{p q : ENNReal}
{f : α → E}
(hfq : MeasureTheory.Memℒp f q μ)
{s : Set α}
(hf : ∀ x ∉ s, f x = 0)
(hs : μ s ≠ ⊤)
(hpq : p ≤ q)
:
MeasureTheory.Memℒp f p μ
Alias of MeasureTheory.Memℒp.mono_exponent_of_measure_support_ne_top.
If a function is supported on a finite-measure set and belongs to ℒ^p, then it belongs to
ℒ^q for any q ≤ p.
theorem
MeasureTheory.eLpNorm_le_eLpNorm_top_mul_eLpNorm
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{μ : MeasureTheory.Measure α}
(p : ENNReal)
(f : α → E)
{g : α → F}
(hg : MeasureTheory.AEStronglyMeasurable g μ)
(b : E → F → G)
(h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊)
:
MeasureTheory.eLpNorm (fun (x : α) => b (f x) (g x)) p μ ≤ MeasureTheory.eLpNorm f ⊤ μ * MeasureTheory.eLpNorm g p μ
theorem
MeasureTheory.eLpNorm_le_eLpNorm_mul_eLpNorm_top
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{μ : MeasureTheory.Measure α}
(p : ENNReal)
{f : α → E}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(g : α → F)
(b : E → F → G)
(h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊)
:
MeasureTheory.eLpNorm (fun (x : α) => b (f x) (g x)) p μ ≤ MeasureTheory.eLpNorm f p μ * MeasureTheory.eLpNorm g ⊤ μ
theorem
MeasureTheory.eLpNorm'_le_eLpNorm'_mul_eLpNorm'
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{μ : MeasureTheory.Measure α}
{f : α → E}
{g : α → F}
{p q r : ℝ}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(hg : MeasureTheory.AEStronglyMeasurable g μ)
(b : E → F → G)
(h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊)
(hp0_lt : 0 < p)
(hpq : p < q)
(hpqr : 1 / p = 1 / q + 1 / r)
:
MeasureTheory.eLpNorm' (fun (x : α) => b (f x) (g x)) p μ ≤ MeasureTheory.eLpNorm' f q μ * MeasureTheory.eLpNorm' g r μ
theorem
MeasureTheory.eLpNorm_le_eLpNorm_mul_eLpNorm_of_nnnorm
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{μ : MeasureTheory.Measure α}
{f : α → E}
{g : α → F}
{p q r : ENNReal}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(hg : MeasureTheory.AEStronglyMeasurable g μ)
(b : E → F → G)
(h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊)
(hpqr : 1 / p = 1 / q + 1 / r)
:
MeasureTheory.eLpNorm (fun (x : α) => b (f x) (g x)) p μ ≤ MeasureTheory.eLpNorm f q μ * MeasureTheory.eLpNorm g r μ
Hölder's inequality, as an inequality on the ℒp seminorm of an elementwise operation
fun x => b (f x) (g x).
theorem
MeasureTheory.eLpNorm_le_eLpNorm_mul_eLpNorm'_of_norm
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{μ : MeasureTheory.Measure α}
{f : α → E}
{g : α → F}
{p q r : ENNReal}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(hg : MeasureTheory.AEStronglyMeasurable g μ)
(b : E → F → G)
(h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖ ≤ ‖f x‖ * ‖g x‖)
(hpqr : 1 / p = 1 / q + 1 / r)
:
MeasureTheory.eLpNorm (fun (x : α) => b (f x) (g x)) p μ ≤ MeasureTheory.eLpNorm f q μ * MeasureTheory.eLpNorm g r μ
Hölder's inequality, as an inequality on the ℒp seminorm of an elementwise operation
fun x => b (f x) (g x).
theorem
MeasureTheory.eLpNorm_smul_le_eLpNorm_top_mul_eLpNorm
{𝕜 : Type u_1}
{α : Type u_2}
{E : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedRing 𝕜]
[NormedAddCommGroup E]
[MulActionWithZero 𝕜 E]
[BoundedSMul 𝕜 E]
{f : α → E}
(p : ENNReal)
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(φ : α → 𝕜)
:
MeasureTheory.eLpNorm (φ • f) p μ ≤ MeasureTheory.eLpNorm φ ⊤ μ * MeasureTheory.eLpNorm f p μ
theorem
MeasureTheory.eLpNorm_smul_le_eLpNorm_mul_eLpNorm_top
{𝕜 : Type u_1}
{α : Type u_2}
{E : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedRing 𝕜]
[NormedAddCommGroup E]
[MulActionWithZero 𝕜 E]
[BoundedSMul 𝕜 E]
(p : ENNReal)
(f : α → E)
{φ : α → 𝕜}
(hφ : MeasureTheory.AEStronglyMeasurable φ μ)
:
MeasureTheory.eLpNorm (φ • f) p μ ≤ MeasureTheory.eLpNorm φ p μ * MeasureTheory.eLpNorm f ⊤ μ
theorem
MeasureTheory.eLpNorm'_smul_le_mul_eLpNorm'
{𝕜 : Type u_1}
{α : Type u_2}
{E : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedRing 𝕜]
[NormedAddCommGroup E]
[MulActionWithZero 𝕜 E]
[BoundedSMul 𝕜 E]
{p q r : ℝ}
{f : α → E}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
{φ : α → 𝕜}
(hφ : MeasureTheory.AEStronglyMeasurable φ μ)
(hp0_lt : 0 < p)
(hpq : p < q)
(hpqr : 1 / p = 1 / q + 1 / r)
:
MeasureTheory.eLpNorm' (φ • f) p μ ≤ MeasureTheory.eLpNorm' φ q μ * MeasureTheory.eLpNorm' f r μ
theorem
MeasureTheory.eLpNorm_smul_le_mul_eLpNorm
{𝕜 : Type u_1}
{α : Type u_2}
{E : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedRing 𝕜]
[NormedAddCommGroup E]
[MulActionWithZero 𝕜 E]
[BoundedSMul 𝕜 E]
{p q r : ENNReal}
{f : α → E}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
{φ : α → 𝕜}
(hφ : MeasureTheory.AEStronglyMeasurable φ μ)
(hpqr : 1 / p = 1 / q + 1 / r)
:
MeasureTheory.eLpNorm (φ • f) p μ ≤ MeasureTheory.eLpNorm φ q μ * MeasureTheory.eLpNorm f r μ
Hölder's inequality, as an inequality on the ℒp seminorm of a scalar product φ • f.
theorem
MeasureTheory.Memℒp.smul
{𝕜 : Type u_1}
{α : Type u_2}
{E : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedRing 𝕜]
[NormedAddCommGroup E]
[MulActionWithZero 𝕜 E]
[BoundedSMul 𝕜 E]
{p q r : ENNReal}
{f : α → E}
{φ : α → 𝕜}
(hf : MeasureTheory.Memℒp f r μ)
(hφ : MeasureTheory.Memℒp φ q μ)
(hpqr : 1 / p = 1 / q + 1 / r)
:
MeasureTheory.Memℒp (φ • f) p μ
theorem
MeasureTheory.Memℒp.smul_of_top_right
{𝕜 : Type u_1}
{α : Type u_2}
{E : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedRing 𝕜]
[NormedAddCommGroup E]
[MulActionWithZero 𝕜 E]
[BoundedSMul 𝕜 E]
{p : ENNReal}
{f : α → E}
{φ : α → 𝕜}
(hf : MeasureTheory.Memℒp f p μ)
(hφ : MeasureTheory.Memℒp φ ⊤ μ)
:
MeasureTheory.Memℒp (φ • f) p μ
theorem
MeasureTheory.Memℒp.smul_of_top_left
{𝕜 : Type u_1}
{α : Type u_2}
{E : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedRing 𝕜]
[NormedAddCommGroup E]
[MulActionWithZero 𝕜 E]
[BoundedSMul 𝕜 E]
{p : ENNReal}
{f : α → E}
{φ : α → 𝕜}
(hf : MeasureTheory.Memℒp f ⊤ μ)
(hφ : MeasureTheory.Memℒp φ p μ)
:
MeasureTheory.Memℒp (φ • f) p μ
theorem
MeasureTheory.Memℒp.mul
{α : Type u_1}
{x✝ : MeasurableSpace α}
{𝕜 : Type u_2}
[NormedRing 𝕜]
{μ : MeasureTheory.Measure α}
{p q r : ENNReal}
{f φ : α → 𝕜}
(hf : MeasureTheory.Memℒp f r μ)
(hφ : MeasureTheory.Memℒp φ q μ)
(hpqr : 1 / p = 1 / q + 1 / r)
:
MeasureTheory.Memℒp (φ * f) p μ
theorem
MeasureTheory.Memℒp.mul'
{α : Type u_1}
{x✝ : MeasurableSpace α}
{𝕜 : Type u_2}
[NormedRing 𝕜]
{μ : MeasureTheory.Measure α}
{p q r : ENNReal}
{f φ : α → 𝕜}
(hf : MeasureTheory.Memℒp f r μ)
(hφ : MeasureTheory.Memℒp φ q μ)
(hpqr : 1 / p = 1 / q + 1 / r)
:
MeasureTheory.Memℒp (fun (x : α) => φ x * f x) p μ
Variant of Memℒp.mul where the function is written as fun x ↦ φ x * f x
instead of φ * f.
theorem
MeasureTheory.Memℒp.mul_of_top_right
{α : Type u_1}
{x✝ : MeasurableSpace α}
{𝕜 : Type u_2}
[NormedRing 𝕜]
{μ : MeasureTheory.Measure α}
{p : ENNReal}
{f φ : α → 𝕜}
(hf : MeasureTheory.Memℒp f p μ)
(hφ : MeasureTheory.Memℒp φ ⊤ μ)
:
MeasureTheory.Memℒp (φ * f) p μ
theorem
MeasureTheory.Memℒp.mul_of_top_right'
{α : Type u_1}
{x✝ : MeasurableSpace α}
{𝕜 : Type u_2}
[NormedRing 𝕜]
{μ : MeasureTheory.Measure α}
{p : ENNReal}
{f φ : α → 𝕜}
(hf : MeasureTheory.Memℒp f p μ)
(hφ : MeasureTheory.Memℒp φ ⊤ μ)
:
MeasureTheory.Memℒp (fun (x : α) => φ x * f x) p μ
Variant of Memℒp.mul_of_top_right where the function is written as fun x ↦ φ x * f x
instead of φ * f.
theorem
MeasureTheory.Memℒp.mul_of_top_left
{α : Type u_1}
{x✝ : MeasurableSpace α}
{𝕜 : Type u_2}
[NormedRing 𝕜]
{μ : MeasureTheory.Measure α}
{p : ENNReal}
{f φ : α → 𝕜}
(hf : MeasureTheory.Memℒp f ⊤ μ)
(hφ : MeasureTheory.Memℒp φ p μ)
:
MeasureTheory.Memℒp (φ * f) p μ
theorem
MeasureTheory.Memℒp.mul_of_top_left'
{α : Type u_1}
{x✝ : MeasurableSpace α}
{𝕜 : Type u_2}
[NormedRing 𝕜]
{μ : MeasureTheory.Measure α}
{p : ENNReal}
{f φ : α → 𝕜}
(hf : MeasureTheory.Memℒp f ⊤ μ)
(hφ : MeasureTheory.Memℒp φ p μ)
:
MeasureTheory.Memℒp (fun (x : α) => φ x * f x) p μ
Variant of Memℒp.mul_of_top_left where the function is written as fun x ↦ φ x * f x
instead of φ * f.
theorem
MeasureTheory.Memℒp.prod
{ι : Type u_1}
{α : Type u_2}
{𝕜 : Type u_3}
{x✝ : MeasurableSpace α}
[NormedCommRing 𝕜]
{μ : MeasureTheory.Measure α}
{f : ι → α → 𝕜}
{p : ι → ENNReal}
{s : Finset ι}
(hf : ∀ i ∈ s, MeasureTheory.Memℒp (f i) (p i) μ)
:
MeasureTheory.Memℒp (∏ i ∈ s, f i) (∑ i ∈ s, (p i)⁻¹)⁻¹ μ
See Memℒp.prod' for the applied version.
theorem
MeasureTheory.Memℒp.prod'
{ι : Type u_1}
{α : Type u_2}
{𝕜 : Type u_3}
{x✝ : MeasurableSpace α}
[NormedCommRing 𝕜]
{μ : MeasureTheory.Measure α}
{f : ι → α → 𝕜}
{p : ι → ENNReal}
{s : Finset ι}
(hf : ∀ i ∈ s, MeasureTheory.Memℒp (f i) (p i) μ)
:
MeasureTheory.Memℒp (fun (ω : α) => ∏ i ∈ s, f i ω) (∑ i ∈ s, (p i)⁻¹)⁻¹ μ
See Memℒp.prod for the unapplied version.