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]
{μ : Measure α}
{f : α → E}
{p q : ℝ}
(hp0_lt : 0 < p)
(hpq : p ≤ q)
(hf : AEStronglyMeasurable f μ)
:
theorem
MeasureTheory.eLpNorm'_le_eLpNormEssSup_mul_rpow_measure_univ
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
{μ : Measure α}
{f : α → E}
{q : ℝ}
(hq_pos : 0 < q)
:
theorem
MeasureTheory.eLpNorm_le_eLpNorm_mul_rpow_measure_univ
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
{μ : Measure α}
{f : α → E}
{p q : ENNReal}
(hpq : p ≤ q)
(hf : AEStronglyMeasurable f μ)
:
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)
(μ : Measure α)
[IsProbabilityMeasure μ]
(hf : AEStronglyMeasurable f μ)
:
theorem
MeasureTheory.eLpNorm'_le_eLpNormEssSup
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
{μ : Measure α}
{f : α → E}
{q : ℝ}
(hq_pos : 0 < q)
[IsProbabilityMeasure μ]
:
theorem
MeasureTheory.eLpNorm_le_eLpNorm_of_exponent_le
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
{μ : Measure α}
{f : α → E}
{p q : ENNReal}
(hpq : p ≤ q)
[IsProbabilityMeasure μ]
(hf : AEStronglyMeasurable f μ)
:
theorem
MeasureTheory.eLpNorm'_lt_top_of_eLpNorm'_lt_top_of_exponent_le
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
{μ : Measure α}
{f : α → E}
{p q : ℝ}
[IsFiniteMeasure μ]
(hf : AEStronglyMeasurable f μ)
(hfq_lt_top : eLpNorm' f q μ < ⊤)
(hp_nonneg : 0 ≤ p)
(hpq : p ≤ q)
:
theorem
MeasureTheory.MemLp.mono_exponent
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
{μ : Measure α}
{p q : ENNReal}
[IsFiniteMeasure μ]
{f : α → E}
(hfq : MemLp f q μ)
(hpq : p ≤ q)
:
MemLp f p μ
@[deprecated MeasureTheory.MemLp.mono_exponent (since := "2025-02-21")]
theorem
MeasureTheory.Memℒp.mono_exponent
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
{μ : Measure α}
{p q : ENNReal}
[IsFiniteMeasure μ]
{f : α → E}
(hfq : MemLp f q μ)
(hpq : p ≤ q)
:
MemLp f p μ
Alias of MeasureTheory.MemLp.mono_exponent.
@[deprecated MeasureTheory.MemLp.mono_exponent (since := "2025-01-07")]
theorem
MeasureTheory.MemLp.memℒp_of_exponent_le
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
{μ : Measure α}
{p q : ENNReal}
[IsFiniteMeasure μ]
{f : α → E}
(hfq : MemLp f q μ)
(hpq : p ≤ q)
:
MemLp f p μ
Alias of MeasureTheory.MemLp.mono_exponent.
theorem
MeasureTheory.MemLp.mono_exponent_of_measure_support_ne_top
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
{μ : Measure α}
{p q : ENNReal}
{f : α → E}
(hfq : MemLp f q μ)
{s : Set α}
(hf : ∀ x ∉ s, f x = 0)
(hs : μ s ≠ ⊤)
(hpq : p ≤ q)
:
MemLp 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.MemLp.mono_exponent_of_measure_support_ne_top (since := "2025-02-21")]
theorem
MeasureTheory.Memℒp.mono_exponent_of_measure_support_ne_top
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
{μ : Measure α}
{p q : ENNReal}
{f : α → E}
(hfq : MemLp f q μ)
{s : Set α}
(hf : ∀ x ∉ s, f x = 0)
(hs : μ s ≠ ⊤)
(hpq : p ≤ q)
:
MemLp f p μ
Alias of MeasureTheory.MemLp.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.
@[deprecated MeasureTheory.MemLp.mono_exponent_of_measure_support_ne_top (since := "2025-01-07")]
theorem
MeasureTheory.MemLp.memℒp_of_exponent_le_of_measure_support_ne_top
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
{μ : Measure α}
{p q : ENNReal}
{f : α → E}
(hfq : MemLp f q μ)
{s : Set α}
(hf : ∀ x ∉ s, f x = 0)
(hs : μ s ≠ ⊤)
(hpq : p ≤ q)
:
MemLp f p μ
Alias of MeasureTheory.MemLp.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]
{μ : Measure α}
(p : ENNReal)
(f : α → E)
{g : α → F}
(hg : AEStronglyMeasurable g μ)
(b : E → F → G)
(c : NNReal)
(h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊)
:
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]
{μ : Measure α}
(p : ENNReal)
{f : α → E}
(hf : AEStronglyMeasurable f μ)
(g : α → F)
(b : E → F → G)
(c : NNReal)
(h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊)
:
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]
{μ : Measure α}
{f : α → E}
{g : α → F}
{p q r : ℝ}
(hf : AEStronglyMeasurable f μ)
(hg : AEStronglyMeasurable g μ)
(b : E → F → G)
(c : NNReal)
(h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊)
(hro_lt : 0 < r)
(hrp : r < p)
(hpqr : 1 / r = 1 / p + 1 / q)
:
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]
{μ : Measure α}
{f : α → E}
{g : α → F}
{p q r : ENNReal}
(hf : AEStronglyMeasurable f μ)
(hg : AEStronglyMeasurable g μ)
(b : E → F → G)
(c : NNReal)
(h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊)
[hpqr : p.HolderTriple q 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]
{μ : Measure α}
{f : α → E}
{g : α → F}
{p q r : ENNReal}
(hf : AEStronglyMeasurable f μ)
(hg : AEStronglyMeasurable g μ)
(b : E → F → G)
(c : NNReal)
(h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖ ≤ ↑c * ‖f x‖ * ‖g x‖)
[hpqr : p.HolderTriple q 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.MemLp.of_bilin
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{μ : Measure α}
{p q r : ENNReal}
{f : α → E}
{g : α → F}
(b : E → F → G)
(c : NNReal)
(hf : MemLp f p μ)
(hg : MemLp g q μ)
(h : AEStronglyMeasurable (fun (x : α) => b (f x) (g x)) μ)
(hb : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊)
[hpqr : p.HolderTriple q r]
:
MemLp (fun (x : α) => b (f x) (g x)) r μ
@[deprecated MeasureTheory.MemLp.of_bilin (since := "2025-02-21")]
theorem
MeasureTheory.Memℒp.of_bilin
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{μ : Measure α}
{p q r : ENNReal}
{f : α → E}
{g : α → F}
(b : E → F → G)
(c : NNReal)
(hf : MemLp f p μ)
(hg : MemLp g q μ)
(h : AEStronglyMeasurable (fun (x : α) => b (f x) (g x)) μ)
(hb : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊)
[hpqr : p.HolderTriple q r]
:
MemLp (fun (x : α) => b (f x) (g x)) r μ
Alias of MeasureTheory.MemLp.of_bilin.
theorem
MeasureTheory.eLpNorm_smul_le_eLpNorm_top_mul_eLpNorm
{𝕜 : Type u_1}
{α : Type u_2}
{E : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedRing 𝕜]
[NormedAddCommGroup E]
[MulActionWithZero 𝕜 E]
[BoundedSMul 𝕜 E]
{f : α → E}
(p : ENNReal)
(hf : AEStronglyMeasurable f μ)
(φ : α → 𝕜)
:
theorem
MeasureTheory.eLpNorm_smul_le_eLpNorm_mul_eLpNorm_top
{𝕜 : Type u_1}
{α : Type u_2}
{E : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedRing 𝕜]
[NormedAddCommGroup E]
[MulActionWithZero 𝕜 E]
[BoundedSMul 𝕜 E]
(p : ENNReal)
(f : α → E)
{φ : α → 𝕜}
(hφ : AEStronglyMeasurable φ μ)
:
theorem
MeasureTheory.eLpNorm'_smul_le_mul_eLpNorm'
{𝕜 : Type u_1}
{α : Type u_2}
{E : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedRing 𝕜]
[NormedAddCommGroup E]
[MulActionWithZero 𝕜 E]
[BoundedSMul 𝕜 E]
{p q r : ℝ}
{f : α → E}
(hf : AEStronglyMeasurable f μ)
{φ : α → 𝕜}
(hφ : AEStronglyMeasurable φ μ)
(hp0_lt : 0 < p)
(hpq : p < q)
(hpqr : 1 / p = 1 / q + 1 / r)
:
theorem
MeasureTheory.eLpNorm_smul_le_mul_eLpNorm
{𝕜 : Type u_1}
{α : Type u_2}
{E : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedRing 𝕜]
[NormedAddCommGroup E]
[MulActionWithZero 𝕜 E]
[BoundedSMul 𝕜 E]
{p q r : ENNReal}
{f : α → E}
(hf : AEStronglyMeasurable f μ)
{φ : α → 𝕜}
(hφ : AEStronglyMeasurable φ μ)
[hpqr : p.HolderTriple q r]
:
Hölder's inequality, as an inequality on the ℒp seminorm of a scalar product φ • f.
theorem
MeasureTheory.MemLp.smul
{𝕜 : Type u_1}
{α : Type u_2}
{E : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedRing 𝕜]
[NormedAddCommGroup E]
[MulActionWithZero 𝕜 E]
[BoundedSMul 𝕜 E]
{p q r : ENNReal}
{f : α → E}
{φ : α → 𝕜}
(hf : MemLp f q μ)
(hφ : MemLp φ p μ)
[hpqr : p.HolderTriple q r]
:
@[deprecated MeasureTheory.MemLp.smul (since := "2025-02-21")]
theorem
MeasureTheory.Memℒp.smul
{𝕜 : Type u_1}
{α : Type u_2}
{E : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedRing 𝕜]
[NormedAddCommGroup E]
[MulActionWithZero 𝕜 E]
[BoundedSMul 𝕜 E]
{p q r : ENNReal}
{f : α → E}
{φ : α → 𝕜}
(hf : MemLp f q μ)
(hφ : MemLp φ p μ)
[hpqr : p.HolderTriple q r]
:
Alias of MeasureTheory.MemLp.smul.
@[deprecated MeasureTheory.MemLp.smul (since := "2025-02-13")]
theorem
MeasureTheory.Memℒp.smul_of_top_right
{𝕜 : Type u_1}
{α : Type u_2}
{E : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedRing 𝕜]
[NormedAddCommGroup E]
[MulActionWithZero 𝕜 E]
[BoundedSMul 𝕜 E]
{p q r : ENNReal}
{f : α → E}
{φ : α → 𝕜}
(hf : MemLp f q μ)
(hφ : MemLp φ p μ)
[hpqr : p.HolderTriple q r]
:
Alias of MeasureTheory.MemLp.smul.
@[deprecated MeasureTheory.MemLp.smul (since := "2025-02-13")]
theorem
MeasureTheory.Memℒp.smul_of_top_left
{𝕜 : Type u_1}
{α : Type u_2}
{E : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedRing 𝕜]
[NormedAddCommGroup E]
[MulActionWithZero 𝕜 E]
[BoundedSMul 𝕜 E]
{p q r : ENNReal}
{f : α → E}
{φ : α → 𝕜}
(hf : MemLp f q μ)
(hφ : MemLp φ p μ)
[hpqr : p.HolderTriple q r]
:
Alias of MeasureTheory.MemLp.smul.
theorem
MeasureTheory.MemLp.mul
{α : Type u_1}
{x✝ : MeasurableSpace α}
{𝕜 : Type u_2}
[NormedRing 𝕜]
{μ : Measure α}
{p q r : ENNReal}
{f φ : α → 𝕜}
(hf : MemLp f q μ)
(hφ : MemLp φ p μ)
[hpqr : p.HolderTriple q r]
:
@[deprecated MeasureTheory.MemLp.mul (since := "2025-02-21")]
theorem
MeasureTheory.Memℒp.mul
{α : Type u_1}
{x✝ : MeasurableSpace α}
{𝕜 : Type u_2}
[NormedRing 𝕜]
{μ : Measure α}
{p q r : ENNReal}
{f φ : α → 𝕜}
(hf : MemLp f q μ)
(hφ : MemLp φ p μ)
[hpqr : p.HolderTriple q r]
:
Alias of MeasureTheory.MemLp.mul.
theorem
MeasureTheory.MemLp.mul'
{α : Type u_1}
{x✝ : MeasurableSpace α}
{𝕜 : Type u_2}
[NormedRing 𝕜]
{μ : Measure α}
{p q r : ENNReal}
{f φ : α → 𝕜}
(hf : MemLp f q μ)
(hφ : MemLp φ p μ)
[hpqr : p.HolderTriple q r]
:
Variant of MemLp.mul where the function is written as fun x ↦ φ x * f x
instead of φ * f.
@[deprecated MeasureTheory.MemLp.mul' (since := "2025-02-21")]
theorem
MeasureTheory.Memℒp.mul'
{α : Type u_1}
{x✝ : MeasurableSpace α}
{𝕜 : Type u_2}
[NormedRing 𝕜]
{μ : Measure α}
{p q r : ENNReal}
{f φ : α → 𝕜}
(hf : MemLp f q μ)
(hφ : MemLp φ p μ)
[hpqr : p.HolderTriple q r]
:
Alias of MeasureTheory.MemLp.mul'.
Variant of MemLp.mul where the function is written as fun x ↦ φ x * f x
instead of φ * f.
@[deprecated MeasureTheory.MemLp.mul (since := "2025-02-13")]
theorem
MeasureTheory.Memℒp.mul_of_top_right
{α : Type u_1}
{x✝ : MeasurableSpace α}
{𝕜 : Type u_2}
[NormedRing 𝕜]
{μ : Measure α}
{p q r : ENNReal}
{f φ : α → 𝕜}
(hf : MemLp f q μ)
(hφ : MemLp φ p μ)
[hpqr : p.HolderTriple q r]
:
Alias of MeasureTheory.MemLp.mul.
@[deprecated MeasureTheory.MemLp.mul' (since := "2025-02-13")]
theorem
MeasureTheory.Memℒp.mul_of_top_right'
{α : Type u_1}
{x✝ : MeasurableSpace α}
{𝕜 : Type u_2}
[NormedRing 𝕜]
{μ : Measure α}
{p q r : ENNReal}
{f φ : α → 𝕜}
(hf : MemLp f q μ)
(hφ : MemLp φ p μ)
[hpqr : p.HolderTriple q r]
:
Alias of MeasureTheory.MemLp.mul'.
Variant of MemLp.mul where the function is written as fun x ↦ φ x * f x
instead of φ * f.
@[deprecated MeasureTheory.MemLp.mul (since := "2025-02-13")]
theorem
MeasureTheory.Memℒp.mul_of_top_left
{α : Type u_1}
{x✝ : MeasurableSpace α}
{𝕜 : Type u_2}
[NormedRing 𝕜]
{μ : Measure α}
{p q r : ENNReal}
{f φ : α → 𝕜}
(hf : MemLp f q μ)
(hφ : MemLp φ p μ)
[hpqr : p.HolderTriple q r]
:
Alias of MeasureTheory.MemLp.mul.
@[deprecated MeasureTheory.MemLp.mul' (since := "2025-02-13")]
theorem
MeasureTheory.Memℒp.mul_of_top_left'
{α : Type u_1}
{x✝ : MeasurableSpace α}
{𝕜 : Type u_2}
[NormedRing 𝕜]
{μ : Measure α}
{p q r : ENNReal}
{f φ : α → 𝕜}
(hf : MemLp f q μ)
(hφ : MemLp φ p μ)
[hpqr : p.HolderTriple q r]
:
Alias of MeasureTheory.MemLp.mul'.
Variant of MemLp.mul where the function is written as fun x ↦ φ x * f x
instead of φ * f.
theorem
MeasureTheory.MemLp.prod
{ι : Type u_1}
{α : Type u_2}
{𝕜 : Type u_3}
{x✝ : MeasurableSpace α}
[NormedCommRing 𝕜]
{μ : Measure α}
{f : ι → α → 𝕜}
{p : ι → ENNReal}
{s : Finset ι}
(hf : ∀ i ∈ s, MemLp (f i) (p i) μ)
:
See MemLp.prod' for the applied version.
@[deprecated MeasureTheory.MemLp.prod (since := "2025-02-21")]
theorem
MeasureTheory.Memℒp.prod
{ι : Type u_1}
{α : Type u_2}
{𝕜 : Type u_3}
{x✝ : MeasurableSpace α}
[NormedCommRing 𝕜]
{μ : Measure α}
{f : ι → α → 𝕜}
{p : ι → ENNReal}
{s : Finset ι}
(hf : ∀ i ∈ s, MemLp (f i) (p i) μ)
:
Alias of MeasureTheory.MemLp.prod.
See MemLp.prod' for the applied version.
theorem
MeasureTheory.MemLp.prod'
{ι : Type u_1}
{α : Type u_2}
{𝕜 : Type u_3}
{x✝ : MeasurableSpace α}
[NormedCommRing 𝕜]
{μ : Measure α}
{f : ι → α → 𝕜}
{p : ι → ENNReal}
{s : Finset ι}
(hf : ∀ i ∈ s, MemLp (f i) (p i) μ)
:
See MemLp.prod for the unapplied version.
@[deprecated MeasureTheory.MemLp.prod' (since := "2025-02-21")]
theorem
MeasureTheory.Memℒp.prod'
{ι : Type u_1}
{α : Type u_2}
{𝕜 : Type u_3}
{x✝ : MeasurableSpace α}
[NormedCommRing 𝕜]
{μ : Measure α}
{f : ι → α → 𝕜}
{p : ι → ENNReal}
{s : Finset ι}
(hf : ∀ i ∈ s, MemLp (f i) (p i) μ)
:
Alias of MeasureTheory.MemLp.prod'.
See MemLp.prod for the unapplied version.