Compare Lp seminorms for different values of p #
In this file we compare MeasureTheory.snorm' and MeasureTheory.snorm for different exponents.
theorem
MeasureTheory.snorm'_le_snorm'_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.snorm' f p μ ≤ MeasureTheory.snorm' f q μ * ↑↑μ Set.univ ^ (1 / p - 1 / q)
theorem
MeasureTheory.snorm'_le_snormEssSup_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.snorm' f q μ ≤ MeasureTheory.snormEssSup f μ * ↑↑μ Set.univ ^ (1 / q)
theorem
MeasureTheory.snorm_le_snorm_mul_rpow_measure_univ
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure α}
{f : α → E}
{p : ENNReal}
{q : ENNReal}
(hpq : p ≤ q)
(hf : MeasureTheory.AEStronglyMeasurable f μ)
:
MeasureTheory.snorm f p μ ≤ MeasureTheory.snorm f q μ * ↑↑μ Set.univ ^ (1 / p.toReal - 1 / q.toReal)
theorem
MeasureTheory.snorm'_le_snorm'_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.snorm' f p μ ≤ MeasureTheory.snorm' f q μ
theorem
MeasureTheory.snorm'_le_snormEssSup
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure α}
{f : α → E}
{q : ℝ}
(hq_pos : 0 < q)
[MeasureTheory.IsProbabilityMeasure μ]
:
MeasureTheory.snorm' f q μ ≤ MeasureTheory.snormEssSup f μ
theorem
MeasureTheory.snorm_le_snorm_of_exponent_le
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure α}
{f : α → E}
{p : ENNReal}
{q : ENNReal}
(hpq : p ≤ q)
[MeasureTheory.IsProbabilityMeasure μ]
(hf : MeasureTheory.AEStronglyMeasurable f μ)
:
MeasureTheory.snorm f p μ ≤ MeasureTheory.snorm f q μ
theorem
MeasureTheory.snorm'_lt_top_of_snorm'_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.snorm' f q μ < ⊤)
(hp_nonneg : 0 ≤ p)
(hpq : p ≤ q)
:
MeasureTheory.snorm' f p μ < ⊤
theorem
MeasureTheory.Memℒp.memℒp_of_exponent_le
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure α}
{p : ENNReal}
{q : ENNReal}
[MeasureTheory.IsFiniteMeasure μ]
{f : α → E}
(hfq : MeasureTheory.Memℒp f q μ)
(hpq : p ≤ q)
:
MeasureTheory.Memℒp f p μ
theorem
MeasureTheory.snorm_le_snorm_top_mul_snorm
{α : 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.snorm (fun (x : α) => b (f x) (g x)) p μ ≤ MeasureTheory.snorm f ⊤ μ * MeasureTheory.snorm g p μ
theorem
MeasureTheory.snorm_le_snorm_mul_snorm_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.snorm (fun (x : α) => b (f x) (g x)) p μ ≤ MeasureTheory.snorm f p μ * MeasureTheory.snorm g ⊤ μ
theorem
MeasureTheory.snorm'_le_snorm'_mul_snorm'
{α : 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.snorm' (fun (x : α) => b (f x) (g x)) p μ ≤ MeasureTheory.snorm' f q μ * MeasureTheory.snorm' g r μ
theorem
MeasureTheory.snorm_le_snorm_mul_snorm_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 : ENNReal}
{q : ENNReal}
{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.snorm (fun (x : α) => b (f x) (g x)) p μ ≤ MeasureTheory.snorm f q μ * MeasureTheory.snorm 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.snorm_le_snorm_mul_snorm'_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 : ENNReal}
{q : ENNReal}
{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.snorm (fun (x : α) => b (f x) (g x)) p μ ≤ MeasureTheory.snorm f q μ * MeasureTheory.snorm 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.snorm_smul_le_snorm_top_mul_snorm
{𝕜 : 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.AEStronglyMeasurable f μ)
(φ : α → 𝕜)
:
MeasureTheory.snorm (φ • f) p μ ≤ MeasureTheory.snorm φ ⊤ μ * MeasureTheory.snorm f p μ
theorem
MeasureTheory.snorm_smul_le_snorm_mul_snorm_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.snorm (φ • f) p μ ≤ MeasureTheory.snorm φ p μ * MeasureTheory.snorm f ⊤ μ
theorem
MeasureTheory.snorm'_smul_le_mul_snorm'
{𝕜 : 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.snorm' (φ • f) p μ ≤ MeasureTheory.snorm' φ q μ * MeasureTheory.snorm' f r μ
theorem
MeasureTheory.snorm_smul_le_mul_snorm
{𝕜 : Type u_1}
{α : Type u_2}
{E : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedRing 𝕜]
[NormedAddCommGroup E]
[MulActionWithZero 𝕜 E]
[BoundedSMul 𝕜 E]
{p : ENNReal}
{q : ENNReal}
{r : ENNReal}
{f : α → E}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
{φ : α → 𝕜}
(hφ : MeasureTheory.AEStronglyMeasurable φ μ)
(hpqr : 1 / p = 1 / q + 1 / r)
:
MeasureTheory.snorm (φ • f) p μ ≤ MeasureTheory.snorm φ q μ * MeasureTheory.snorm 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 : ENNReal}
{q : ENNReal}
{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 μ