Lp norms

noncomputable def MeasureTheory.dLpNorm {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] (p : ENNReal) (f : α → E) : ℝ

The Lp norm of a function with the compact normalisation.

Equations

• ‖f‖_[p] = MeasureTheory.lpNorm f p MeasureTheory.Measure.count

def MeasureTheory.«term‖_‖_[_]» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MeasureTheory.dLpNorm_nonneg {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {f : α → E} : 0 ≤ ‖f‖_[p]

@[simp]

theorem MeasureTheory.dLpNorm_exponent_zero {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] (f : α → E) : ‖f‖_[0] = 0

@[simp]

theorem MeasureTheory.dLpNorm_zero {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] (p : ENNReal) : ‖0‖_[p] = 0

@[simp]

theorem MeasureTheory.dLpNorm_zero' {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] (p : ENNReal) : ‖fun (x : α) => 0‖_[p] = 0

@[simp]

theorem MeasureTheory.dLpNorm_of_isEmpty {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] [IsEmpty α] (f : α → E) (p : ENNReal) : ‖f‖_[p] = 0

@[simp]

theorem MeasureTheory.dLpNorm_neg {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] (f : α → E) (p : ENNReal) : ‖-f‖_[p] = ‖f‖_[p]

@[simp]

theorem MeasureTheory.dLpNorm_neg' {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] (f : α → E) (p : ENNReal) : ‖fun (x : α) => -f x‖_[p] = ‖f‖_[p]

theorem MeasureTheory.dLpNorm_sub_comm {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] (f g : α → E) (p : ENNReal) : ‖f - g‖_[p] = ‖g - f‖_[p]

@[simp]

theorem MeasureTheory.dLpNorm_norm {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {f : α → E} (hf : StronglyMeasurable f) (p : ENNReal) : ‖fun (i : α) => ‖f i‖‖_[p] = ‖f‖_[p]

@[simp]

theorem MeasureTheory.dLpNorm_abs {α : Type u_1} [MeasurableSpace α] {f : α → ℝ} (hf : StronglyMeasurable f) (p : ENNReal) : ‖|f|‖_[p] = ‖f‖_[p]

@[simp]

theorem MeasureTheory.dLpNorm_fun_abs {α : Type u_1} [MeasurableSpace α] {f : α → ℝ} (hf : StronglyMeasurable f) (p : ENNReal) : ‖fun (i : α) => |f i|‖_[p] = ‖f‖_[p]

theorem MeasureTheory.dLpNorm_const_smul {α : Type u_1} {𝕜 : Type u_2} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] [NormedField 𝕜] {p : ENNReal} [Module 𝕜 E] [NormSMulClass 𝕜 E] (c : 𝕜) (f : α → E) : ‖c • f‖_[p] = ‖c‖ * ‖f‖_[p]

theorem MeasureTheory.dLpNorm_nsmul {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] [NormedSpace ℝ E] (n : ℕ) (f : α → E) (p : ENNReal) : ‖n • f‖_[p] = n • ‖f‖_[p]

theorem MeasureTheory.dLpNorm_natCast_mul {α : Type u_1} {𝕜 : Type u_2} [MeasurableSpace α] [NormedField 𝕜] [NormedSpace ℝ 𝕜] (n : ℕ) (f : α → 𝕜) (p : ENNReal) : ‖↑n * f‖_[p] = ↑n * ‖f‖_[p]

theorem MeasureTheory.dLpNorm_fun_natCast_mul {α : Type u_1} {𝕜 : Type u_2} [MeasurableSpace α] [NormedField 𝕜] [NormedSpace ℝ 𝕜] (n : ℕ) (f : α → 𝕜) (p : ENNReal) : ‖fun (x : α) => ↑n * f x‖_[p] = ↑n * ‖f‖_[p]

theorem MeasureTheory.dLpNorm_mul_natCast {α : Type u_1} {𝕜 : Type u_2} [MeasurableSpace α] [NormedField 𝕜] [NormedSpace ℝ 𝕜] (f : α → 𝕜) (n : ℕ) (p : ENNReal) : ‖f * ↑n‖_[p] = ‖f‖_[p] * ↑n

theorem MeasureTheory.dLpNorm_fun_mul_natCast {α : Type u_1} {𝕜 : Type u_2} [MeasurableSpace α] [NormedField 𝕜] [NormedSpace ℝ 𝕜] (f : α → 𝕜) (n : ℕ) (p : ENNReal) : ‖fun (x : α) => f x * ↑n‖_[p] = ‖f‖_[p] * ↑n

theorem MeasureTheory.dLpNorm_div_natCast {α : Type u_1} {𝕜 : Type u_2} [MeasurableSpace α] [NormedField 𝕜] [NormedSpace ℝ 𝕜] [CharZero 𝕜] {n : ℕ} (hn : n ≠ 0) (f : α → 𝕜) (p : ENNReal) : ‖f / ↑n‖_[p] = ‖f‖_[p] / ↑n

theorem MeasureTheory.dLpNorm_fun_div_natCast {α : Type u_1} {𝕜 : Type u_2} [MeasurableSpace α] [NormedField 𝕜] [NormedSpace ℝ 𝕜] [CharZero 𝕜] {n : ℕ} (hn : n ≠ 0) (f : α → 𝕜) (p : ENNReal) : ‖fun (x : α) => f x / ↑n‖_[p] = ‖f‖_[p] / ↑n

theorem MeasureTheory.dLpNorm_nnqsmul {α : Type u_1} [MeasurableSpace α] {p : ENNReal} (q : ℚ≥0) (f : α → ℂ) : ‖q • f‖_[p] = ↑q * ‖f‖_[p]

@[simp]

theorem MeasureTheory.dLpNorm_conj {α : Type u_1} {R : Type u_3} [MeasurableSpace α] {p : ENNReal} [RCLike R] (f : α → R) : ‖(starRingEnd (α → R)) f‖_[p] = ‖f‖_[p]

theorem MeasureTheory.dLpNorm_add_le {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {f g : α → E} [DiscreteMeasurableSpace α] [Finite α] (hp : 1 ≤ p) : ‖f + g‖_[p] ≤ ‖f‖_[p] + ‖g‖_[p]

theorem MeasureTheory.dLpNorm_sub_le {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {f g : α → E} [DiscreteMeasurableSpace α] [Finite α] (hp : 1 ≤ p) : ‖f - g‖_[p] ≤ ‖f‖_[p] + ‖g‖_[p]

theorem MeasureTheory.dLpNorm_sum_le {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} [DiscreteMeasurableSpace α] [Finite α] {ι : Type u_5} {s : Finset ι} {f : ι → α → E} (hp : 1 ≤ p) : ‖∑ i ∈ s, f i‖_[p] ≤ ∑ i ∈ s, ‖f i‖_[p]

theorem MeasureTheory.dLpNorm_expect_le {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} [DiscreteMeasurableSpace α] [Finite α] [Module ℚ≥0 E] [NormedSpace ℝ E] {ι : Type u_5} {s : Finset ι} {f : ι → α → E} (hp : 1 ≤ p) : ‖s.expect fun (i : ι) => f i‖_[p] ≤ s.expect fun (i : ι) => ‖f i‖_[p]

theorem MeasureTheory.dLpNorm_le_dLpNorm_add_dLpNorm_sub' {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {f g : α → E} [DiscreteMeasurableSpace α] [Finite α] (hp : 1 ≤ p) : ‖f‖_[p] ≤ ‖g‖_[p] + ‖f - g‖_[p]

theorem MeasureTheory.dLpNorm_le_dLpNorm_add_dLpNorm_sub {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {f g : α → E} [DiscreteMeasurableSpace α] [Finite α] (hp : 1 ≤ p) : ‖f‖_[p] ≤ ‖g‖_[p] + ‖g - f‖_[p]

theorem MeasureTheory.dLpNorm_le_add_dLpNorm_add {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {f g : α → E} [DiscreteMeasurableSpace α] [Finite α] (hp : 1 ≤ p) : ‖f‖_[p] ≤ ‖f + g‖_[p] + ‖g‖_[p]

theorem MeasureTheory.dLpNorm_sub_le_dLpNorm_sub_add_dLpNorm_sub {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {f g h : α → E} [DiscreteMeasurableSpace α] [Finite α] (hp : 1 ≤ p) : ‖f - h‖_[p] ≤ ‖f - g‖_[p] + ‖g - h‖_[p]

@[simp]

theorem MeasureTheory.dLpNorm_const {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] [Fintype α] [Nonempty α] {p : ENNReal} (hp : p ≠ 0) (a : E) : ‖fun (_i : α) => a‖_[p] = ↑‖a‖₊ * ↑(Fintype.card α) ^ p.toReal⁻¹

@[simp]

theorem MeasureTheory.dLpNorm_const' {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] [Fintype α] {p : ENNReal} (hp₀ : p ≠ 0) (hp : p ≠ ⊤) (a : E) : ‖fun (_i : α) => a‖_[p] = ↑‖a‖₊ * ↑(Fintype.card α) ^ p.toReal⁻¹

@[simp]

theorem MeasureTheory.dLpNorm_one {α : Type u_1} {𝕜 : Type u_2} [MeasurableSpace α] [Fintype α] [NormedField 𝕜] {p : ENNReal} [Nonempty α] (hp : p ≠ 0) : ‖1‖_[p] = ↑(Fintype.card α) ^ p.toReal⁻¹

@[simp]

theorem MeasureTheory.dLpNorm_one' {α : Type u_1} {𝕜 : Type u_2} [MeasurableSpace α] [Fintype α] [NormedField 𝕜] {p : ENNReal} (hp₀ : p ≠ 0) (hp : p ≠ ⊤) : ‖1‖_[p] = ↑(Fintype.card α) ^ p.toReal⁻¹

theorem MeasureTheory.dLpNorm_eq_sum_norm' {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} [Fintype α] [DiscreteMeasurableSpace α] (hp₀ : p ≠ 0) (hp : p ≠ ⊤) (f : α → E) : ‖f‖_[p] = (∑ i : α, ‖f i‖ ^ p.toReal) ^ p.toReal⁻¹

theorem MeasureTheory.dLpNorm_toNNReal_eq_sum_norm {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] [Fintype α] [DiscreteMeasurableSpace α] {p : ℝ} (hp : 0 < p) (f : α → E) : ‖f‖_[↑p.toNNReal] = (∑ i : α, ‖f i‖ ^ p) ^ p⁻¹

theorem MeasureTheory.dLpNorm_eq_sum_norm {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] [Fintype α] [DiscreteMeasurableSpace α] {p : NNReal} (hp : p ≠ 0) (f : α → E) : ‖f‖_[↑p] = (∑ i : α, ‖f i‖ ^ ↑p) ^ (↑p)⁻¹

theorem MeasureTheory.dLpNorm_rpow_eq_sum_norm {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] [Fintype α] [DiscreteMeasurableSpace α] {p : NNReal} (hp : p ≠ 0) (f : α → E) : ‖f‖_[↑p] ^ ↑p = ∑ i : α, ‖f i‖ ^ ↑p

theorem MeasureTheory.dLpNorm_pow_eq_sum_norm {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] [Fintype α] [DiscreteMeasurableSpace α] {p : ℕ} (hp : p ≠ 0) (f : α → E) : ‖f‖_[↑p] ^ p = ∑ i : α, ‖f i‖ ^ p

theorem MeasureTheory.dL2Norm_sq_eq_sum_norm {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] [Fintype α] [DiscreteMeasurableSpace α] (f : α → E) : ‖f‖_[2] ^ 2 = ∑ i : α, ‖f i‖ ^ 2

theorem MeasureTheory.dL2Norm_eq_sum_norm {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] [Fintype α] [DiscreteMeasurableSpace α] (f : α → E) : ‖f‖_[2] = (∑ i : α, ‖f i‖ ^ 2) ^ 2⁻¹

theorem MeasureTheory.dL1Norm_eq_sum_norm {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] [Fintype α] [DiscreteMeasurableSpace α] (f : α → E) : ‖f‖_[1] = ∑ i : α, ‖f i‖

theorem MeasureTheory.dLinftyNorm_eq_iSup_norm {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] [DiscreteMeasurableSpace α] [Finite α] (f : α → E) : ‖f‖_[⊤] = ⨆ (i : α), ‖f i‖

theorem MeasureTheory.norm_le_dLinftyNorm {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {f : α → E} [DiscreteMeasurableSpace α] [Finite α] {i : α} : ‖f i‖ ≤ ‖f‖_[⊤]

@[simp]

theorem MeasureTheory.dLpNorm_eq_zero {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {f : α → E} [DiscreteMeasurableSpace α] [Finite α] (hp : p ≠ 0) : ‖f‖_[p] = 0 ↔ f = 0

@[simp]

theorem MeasureTheory.dLpNorm_pos {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {f : α → E} [DiscreteMeasurableSpace α] [Finite α] (hp : p ≠ 0) : 0 < ‖f‖_[p] ↔ f ≠ 0

theorem MeasureTheory.dLpNorm_mono_real {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {f : α → E} [DiscreteMeasurableSpace α] [Finite α] {g : α → ℝ} (h : ∀ (x : α), ‖f x‖ ≤ g x) : ‖f‖_[p] ≤ ‖g‖_[p]

theorem MeasureTheory.dLpNorm_two_mul_sum_pow {α : Type u_1} [MeasurableSpace α] [DiscreteMeasurableSpace α] [Fintype α] {ι : Type u_5} {n : ℕ} (hn : n ≠ 0) (s : Finset ι) (f : ι → α → ℂ) : ↑‖∑ i ∈ s, f i‖_[2 * ↑n] ^ (2 * n) = ∑ x ∈ Fintype.piFinset fun (x : Fin n) => s, ∑ y ∈ Fintype.piFinset fun (x : Fin n) => s, ∑ a : α, (∏ i : Fin n, (starRingEnd ℂ) (f (x i) a)) * ∏ i : Fin n, f (y i) a

theorem Mathlib.Meta.Positivity.dLpNorm_pos_of_ne_zero {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {f : α → E} [DiscreteMeasurableSpace α] [Finite α] (hp : p ≠ 0) : f ≠ 0 → 0 < ‖f‖_[p]

Alias of the reverse direction of MeasureTheory.dLpNorm_pos.

def Mathlib.Meta.Positivity.evalDLpNorm : PositivityExt

The positivity extension which identifies expressions of the form ‖f‖_[p].

Equations

• One or more equations did not get rendered due to their size.

Hölder inequality

theorem MeasureTheory.dLpNorm_rpow {α : Type u_5} {mα : MeasurableSpace α} [DiscreteMeasurableSpace α] [Finite α] {p q : NNReal} {f : α → ℝ} (hp : p ≠ 0) (hq : q ≠ 0) (hf : 0 ≤ f) : ‖f ^ ↑q‖_[↑p] = ‖f‖_[↑p * ↑q] ^ ↑q

theorem MeasureTheory.dLpNorm_pow {α : Type u_5} {mα : MeasurableSpace α} [DiscreteMeasurableSpace α] [Finite α] {p : NNReal} (hp : p ≠ 0) {q : ℕ} (hq : q ≠ 0) (f : α → ℂ) : ‖f ^ q‖_[↑p] = ‖f‖_[↑p * ↑q] ^ q

theorem MeasureTheory.dL1Norm_rpow {α : Type u_5} {mα : MeasurableSpace α} [DiscreteMeasurableSpace α] [Finite α] {q : NNReal} {f : α → ℝ} (hq : q ≠ 0) (hf : 0 ≤ f) : ‖f ^ ↑q‖_[1] = ‖f‖_[↑q] ^ ↑q

theorem MeasureTheory.dL1Norm_pow {α : Type u_5} {mα : MeasurableSpace α} [DiscreteMeasurableSpace α] [Finite α] {q : ℕ} (hq : q ≠ 0) (f : α → ℂ) : ‖f ^ q‖_[1] = ‖f‖_[↑q] ^ q

theorem MeasureTheory.dLpNorm_eq_dL1Norm_rpow {𝕜 : Type u_2} {α : Type u_5} {mα : MeasurableSpace α} [DiscreteMeasurableSpace α] [Finite α] [RCLike 𝕜] {p : NNReal} (hp : p ≠ 0) (f : α → 𝕜) : ‖f‖_[↑p] = ‖fun (a : α) => ‖f a‖ ^ ↑p‖_[1] ^ (↑p)⁻¹

theorem MeasureTheory.dLpNorm_rpow' {𝕜 : Type u_2} {α : Type u_5} {mα : MeasurableSpace α} [DiscreteMeasurableSpace α] [Finite α] [RCLike 𝕜] {q : NNReal} {p : ENNReal} (hp₀ : p ≠ 0) (hp : p ≠ ⊤) (hq : q ≠ 0) (f : α → 𝕜) : ‖f‖_[p] ^ ↑q = ‖(fun (a : α) => ‖f a‖) ^ ↑q‖_[p / ↑q]

@[simp]

theorem MeasureTheory.RCLike.dLpNorm_coe_comp {𝕜 : Type u_2} {α : Type u_5} {mα : MeasurableSpace α} [RCLike 𝕜] (p : ENNReal) (f : α → ℝ) : ‖RCLike.ofReal ∘ f‖_[p] = ‖f‖_[p]

@[simp]

theorem MeasureTheory.Complex.dLpNorm_coe_comp {α : Type u_5} {mα : MeasurableSpace α} (p : ENNReal) (f : α → ℝ) : ‖Complex.ofReal ∘ f‖_[p] = ‖f‖_[p]