Documentation

Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp

Compare Lp seminorms for different values of p #

In this file we compare MeasureTheory.eLpNorm' and MeasureTheory.eLpNorm for different exponents.

source
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 μ) :
eLpNorm' f p μ ≤ eLpNorm' f q μ * μ Set.univ ^ (1 / p - 1 / q)
source
@[deprecated MeasureTheory.eLpNorm'_le_eLpNorm'_mul_rpow_measure_univ (since := "2024-07-27")]
theorem MeasureTheory.snorm'_le_snorm'_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 μ) :
eLpNorm' f p μ ≤ eLpNorm' f q μ * μ Set.univ ^ (1 / p - 1 / q)

Alias of MeasureTheory.eLpNorm'_le_eLpNorm'_mul_rpow_measure_univ.

source
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) :
eLpNorm' f q μ ≤ eLpNormEssSup f μ * μ Set.univ ^ (1 / q)
source
@[deprecated MeasureTheory.eLpNorm'_le_eLpNormEssSup_mul_rpow_measure_univ (since := "2024-07-27")]
theorem MeasureTheory.snorm'_le_snormEssSup_mul_rpow_measure_univ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} [NormedAddCommGroup E] {μ : Measure α} {f : α → E} {q : ℝ} (hq_pos : 0 < q) :
eLpNorm' f q μ ≤ eLpNormEssSup f μ * μ Set.univ ^ (1 / q)

Alias of MeasureTheory.eLpNorm'_le_eLpNormEssSup_mul_rpow_measure_univ.

source
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 μ) :
eLpNorm f p μ ≤ eLpNorm f q μ * μ Set.univ ^ (1 / p.toReal - 1 / q.toReal)
source
@[deprecated MeasureTheory.eLpNorm_le_eLpNorm_mul_rpow_measure_univ (since := "2024-07-27")]
theorem MeasureTheory.snorm_le_snorm_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 μ) :
eLpNorm f p μ ≤ eLpNorm f q μ * μ Set.univ ^ (1 / p.toReal - 1 / q.toReal)

Alias of MeasureTheory.eLpNorm_le_eLpNorm_mul_rpow_measure_univ.

source
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 μ) :
eLpNorm' f p μ ≤ eLpNorm' f q μ
source
@[deprecated MeasureTheory.eLpNorm'_le_eLpNorm'_of_exponent_le (since := "2024-07-27")]
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) (μ : Measure α) [IsProbabilityMeasure μ] (hf : AEStronglyMeasurable f μ) :
eLpNorm' f p μ ≤ eLpNorm' f q μ

Alias of MeasureTheory.eLpNorm'_le_eLpNorm'_of_exponent_le.

source
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 μ] :
eLpNorm' f q μ ≤ eLpNormEssSup f μ
source
@[deprecated MeasureTheory.eLpNorm'_le_eLpNormEssSup (since := "2024-07-27")]
theorem MeasureTheory.snorm'_le_snormEssSup {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} [NormedAddCommGroup E] {μ : Measure α} {f : α → E} {q : ℝ} (hq_pos : 0 < q) [IsProbabilityMeasure μ] :
eLpNorm' f q μ ≤ eLpNormEssSup f μ

Alias of MeasureTheory.eLpNorm'_le_eLpNormEssSup.

source
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 μ) :
eLpNorm f p μ ≤ eLpNorm f q μ
source
@[deprecated MeasureTheory.eLpNorm_le_eLpNorm_of_exponent_le (since := "2024-07-27")]
theorem MeasureTheory.snorm_le_snorm_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 μ) :
eLpNorm f p μ ≤ eLpNorm f q μ

Alias of MeasureTheory.eLpNorm_le_eLpNorm_of_exponent_le.

source
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) :
eLpNorm' f p μ < ⊤
source
@[deprecated MeasureTheory.eLpNorm'_lt_top_of_eLpNorm'_lt_top_of_exponent_le (since := "2024-07-27")]
theorem MeasureTheory.snorm'_lt_top_of_snorm'_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) :
eLpNorm' f p μ < ⊤

Alias of MeasureTheory.eLpNorm'_lt_top_of_eLpNorm'_lt_top_of_exponent_le.

source
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 : Memℒp f q μ) (hpq : p ≤ q) :
Memℒp f p μ
source
@[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] {μ : Measure α} {p q : ENNReal} [IsFiniteMeasure μ] {f : α → E} (hfq : Memℒp f q μ) (hpq : p ≤ q) :
Memℒp f p μ

Alias of MeasureTheory.Memℒp.mono_exponent.

source
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 : Memℒp f q μ) {s : Set α} (hf : ∀ x ∉ s, f x = 0) (hs : μ s ≠ ⊤) (hpq : p ≤ q) :
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.

source
@[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] {μ : Measure α} {p q : ENNReal} {f : α → E} (hfq : Memℒp f q μ) {s : Set α} (hf : ∀ x ∉ s, f x = 0) (hs : μ s ≠ ⊤) (hpq : p ≤ q) :
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.

source
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) (h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊) :
eLpNorm (fun (x : α) => b (f x) (g x)) p μ ≤ eLpNorm f ⊤ μ * eLpNorm g p μ
source
@[deprecated MeasureTheory.eLpNorm_le_eLpNorm_top_mul_eLpNorm (since := "2024-07-27")]
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] {μ : Measure α} (p : ENNReal) (f : α → E) {g : α → F} (hg : AEStronglyMeasurable g μ) (b : E → F → G) (h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊) :
eLpNorm (fun (x : α) => b (f x) (g x)) p μ ≤ eLpNorm f ⊤ μ * eLpNorm g p μ

Alias of MeasureTheory.eLpNorm_le_eLpNorm_top_mul_eLpNorm.

source
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) (h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊) :
eLpNorm (fun (x : α) => b (f x) (g x)) p μ ≤ eLpNorm f p μ * eLpNorm g ⊤ μ
source
@[deprecated MeasureTheory.eLpNorm_le_eLpNorm_mul_eLpNorm_top (since := "2024-07-27")]
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] {μ : Measure α} (p : ENNReal) {f : α → E} (hf : AEStronglyMeasurable f μ) (g : α → F) (b : E → F → G) (h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊) :
eLpNorm (fun (x : α) => b (f x) (g x)) p μ ≤ eLpNorm f p μ * eLpNorm g ⊤ μ

Alias of MeasureTheory.eLpNorm_le_eLpNorm_mul_eLpNorm_top.

source
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) (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) :
eLpNorm' (fun (x : α) => b (f x) (g x)) p μ ≤ eLpNorm' f q μ * eLpNorm' g r μ
source
@[deprecated MeasureTheory.eLpNorm'_le_eLpNorm'_mul_eLpNorm' (since := "2024-07-27")]
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] {μ : Measure α} {f : α → E} {g : α → F} {p q r : ℝ} (hf : AEStronglyMeasurable f μ) (hg : 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) :
eLpNorm' (fun (x : α) => b (f x) (g x)) p μ ≤ eLpNorm' f q μ * eLpNorm' g r μ

Alias of MeasureTheory.eLpNorm'_le_eLpNorm'_mul_eLpNorm'.

source
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) (h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊) (hpqr : 1 / p = 1 / q + 1 / r) :
eLpNorm (fun (x : α) => b (f x) (g x)) p μ ≤ eLpNorm f q μ * 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).

source
@[deprecated MeasureTheory.eLpNorm_le_eLpNorm_mul_eLpNorm_of_nnnorm (since := "2024-07-27")]
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] {μ : Measure α} {f : α → E} {g : α → F} {p q r : ENNReal} (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) (b : E → F → G) (h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊) (hpqr : 1 / p = 1 / q + 1 / r) :
eLpNorm (fun (x : α) => b (f x) (g x)) p μ ≤ eLpNorm f q μ * eLpNorm g r μ

Alias of MeasureTheory.eLpNorm_le_eLpNorm_mul_eLpNorm_of_nnnorm.

Hölder's inequality, as an inequality on the ℒp seminorm of an elementwise operation fun x => b (f x) (g x).

source
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) (h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖ ≤ ‖f x‖ * ‖g x‖) (hpqr : 1 / p = 1 / q + 1 / r) :
eLpNorm (fun (x : α) => b (f x) (g x)) p μ ≤ eLpNorm f q μ * 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).

source
@[deprecated MeasureTheory.eLpNorm_le_eLpNorm_mul_eLpNorm'_of_norm (since := "2024-07-27")]
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] {μ : Measure α} {f : α → E} {g : α → F} {p q r : ENNReal} (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) (b : E → F → G) (h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖ ≤ ‖f x‖ * ‖g x‖) (hpqr : 1 / p = 1 / q + 1 / r) :
eLpNorm (fun (x : α) => b (f x) (g x)) p μ ≤ eLpNorm f q μ * eLpNorm g r μ

Alias of MeasureTheory.eLpNorm_le_eLpNorm_mul_eLpNorm'_of_norm.

Hölder's inequality, as an inequality on the ℒp seminorm of an elementwise operation fun x => b (f x) (g x).

source
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 μ) (φ : α → 𝕜) :
eLpNorm (φ • f) p μ ≤ eLpNorm φ ⊤ μ * eLpNorm f p μ
source
@[deprecated MeasureTheory.eLpNorm_smul_le_eLpNorm_top_mul_eLpNorm (since := "2024-07-27")]
theorem MeasureTheory.snorm_smul_le_snorm_top_mul_snorm {𝕜 : 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 μ) (φ : α → 𝕜) :
eLpNorm (φ • f) p μ ≤ eLpNorm φ ⊤ μ * eLpNorm f p μ

Alias of MeasureTheory.eLpNorm_smul_le_eLpNorm_top_mul_eLpNorm.

source
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 φ μ) :
eLpNorm (φ • f) p μ ≤ eLpNorm φ p μ * eLpNorm f ⊤ μ
source
@[deprecated MeasureTheory.eLpNorm_smul_le_eLpNorm_mul_eLpNorm_top (since := "2024-07-27")]
theorem MeasureTheory.snorm_smul_le_snorm_mul_snorm_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 φ μ) :
eLpNorm (φ • f) p μ ≤ eLpNorm φ p μ * eLpNorm f ⊤ μ

Alias of MeasureTheory.eLpNorm_smul_le_eLpNorm_mul_eLpNorm_top.

source
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) :
eLpNorm' (φ • f) p μ ≤ eLpNorm' φ q μ * eLpNorm' f r μ
source
@[deprecated MeasureTheory.eLpNorm'_smul_le_mul_eLpNorm' (since := "2024-07-27")]
theorem MeasureTheory.snorm'_smul_le_mul_snorm' {𝕜 : 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) :
eLpNorm' (φ • f) p μ ≤ eLpNorm' φ q μ * eLpNorm' f r μ

Alias of MeasureTheory.eLpNorm'_smul_le_mul_eLpNorm'.

source
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 : 1 / p = 1 / q + 1 / r) :
eLpNorm (φ • f) p μ ≤ eLpNorm φ q μ * eLpNorm f r μ

Hölder's inequality, as an inequality on the ℒp seminorm of a scalar product φ • f.

source
@[deprecated MeasureTheory.eLpNorm_smul_le_mul_eLpNorm (since := "2024-07-27")]
theorem MeasureTheory.snorm_smul_le_mul_snorm {𝕜 : 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 : 1 / p = 1 / q + 1 / r) :
eLpNorm (φ • f) p μ ≤ eLpNorm φ q μ * eLpNorm f r μ

Alias of MeasureTheory.eLpNorm_smul_le_mul_eLpNorm.

Hölder's inequality, as an inequality on the ℒp seminorm of a scalar product φ • f.

source
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 : Memℒp f r μ) (hφ : Memℒp φ q μ) (hpqr : 1 / p = 1 / q + 1 / r) :
Memℒp (φ • f) p μ
source
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 : ENNReal} {f : α → E} {φ : α → 𝕜} (hf : Memℒp f p μ) (hφ : Memℒp φ ⊤ μ) :
Memℒp (φ • f) p μ
source
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 : ENNReal} {f : α → E} {φ : α → 𝕜} (hf : Memℒp f ⊤ μ) (hφ : Memℒp φ p μ) :
Memℒp (φ • f) p μ
source
theorem MeasureTheory.Memℒp.mul {α : Type u_1} [MeasurableSpace α] {𝕜 : Type u_2} [NormedRing 𝕜] {μ : Measure α} {p q r : ENNReal} {f φ : α → 𝕜} (hf : Memℒp f r μ) (hφ : Memℒp φ q μ) (hpqr : 1 / p = 1 / q + 1 / r) :
Memℒp (φ * f) p μ
source
theorem MeasureTheory.Memℒp.mul' {α : Type u_1} [MeasurableSpace α] {𝕜 : Type u_2} [NormedRing 𝕜] {μ : Measure α} {p q r : ENNReal} {f φ : α → 𝕜} (hf : Memℒp f r μ) (hφ : Memℒp φ q μ) (hpqr : 1 / p = 1 / q + 1 / r) :
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.

source
theorem MeasureTheory.Memℒp.mul_of_top_right {α : Type u_1} [MeasurableSpace α] {𝕜 : Type u_2} [NormedRing 𝕜] {μ : Measure α} {p : ENNReal} {f φ : α → 𝕜} (hf : Memℒp f p μ) (hφ : Memℒp φ ⊤ μ) :
Memℒp (φ * f) p μ
source
theorem MeasureTheory.Memℒp.mul_of_top_right' {α : Type u_1} [MeasurableSpace α] {𝕜 : Type u_2} [NormedRing 𝕜] {μ : Measure α} {p : ENNReal} {f φ : α → 𝕜} (hf : Memℒp f p μ) (hφ : Memℒp φ ⊤ μ) :
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.

source
theorem MeasureTheory.Memℒp.mul_of_top_left {α : Type u_1} [MeasurableSpace α] {𝕜 : Type u_2} [NormedRing 𝕜] {μ : Measure α} {p : ENNReal} {f φ : α → 𝕜} (hf : Memℒp f ⊤ μ) (hφ : Memℒp φ p μ) :
Memℒp (φ * f) p μ
source
theorem MeasureTheory.Memℒp.mul_of_top_left' {α : Type u_1} [MeasurableSpace α] {𝕜 : Type u_2} [NormedRing 𝕜] {μ : Measure α} {p : ENNReal} {f φ : α → 𝕜} (hf : Memℒp f ⊤ μ) (hφ : Memℒp φ p μ) :
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.