ℒp space

This file describes properties of almost everywhere strongly measurable functions with finite p-seminorm, denoted by eLpNorm f p μ and defined for p:ℝ≥0∞ as 0 if p=0, (∫ ‖f a‖^p ∂μ) ^ (1/p) for 0 < p < ∞ and essSup ‖f‖ μ for p=∞.

The Prop-valued Memℒp f p μ states that a function f : α → E has finite p-seminorm and is almost everywhere strongly measurable.

Main definitions

• eLpNorm' f p μ : (∫ ‖f a‖^p ∂μ) ^ (1/p) for f : α → F and p : ℝ, where α is a measurable space and F is a normed group.

• eLpNormEssSup f μ : seminorm in ℒ∞, equal to the essential supremum essSup ‖f‖ μ.

• eLpNorm f p μ : for p : ℝ≥0∞, seminorm in ℒp, equal to 0 for p=0, to eLpNorm' f p μ for 0 < p < ∞ and to eLpNormEssSup f μ for p = ∞.

• Memℒp f p μ : property that the function f is almost everywhere strongly measurable and has finite p-seminorm for the measure μ (eLpNorm f p μ < ∞)

ℒp seminorm

We define the ℒp seminorm, denoted by eLpNorm f p μ. For real p, it is given by an integral formula (for which we use the notation eLpNorm' f p μ), and for p = ∞ it is the essential supremum (for which we use the notation eLpNormEssSup f μ).

We also define a predicate Memℒp f p μ, requesting that a function is almost everywhere measurable and has finite eLpNorm f p μ.

This paragraph is devoted to the basic properties of these definitions. It is constructed as follows: for a given property, we prove it for eLpNorm' and eLpNormEssSup when it makes sense, deduce it for eLpNorm, and translate it in terms of Memℒp.

def MeasureTheory.eLpNorm' {α : Type u_1} {ε : Type u_2} [ENorm ε] {x✝ : MeasurableSpace α} (f : α → ε) (q : ℝ) (μ : MeasureTheory.Measure α) : ENNReal

(∫ ‖f a‖^q ∂μ) ^ (1/q), which is a seminorm on the space of measurable functions for which this quantity is finite

Equations

• MeasureTheory.eLpNorm' f q μ = (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ (1 / q)

theorem MeasureTheory.eLpNorm'_eq_lintegral_enorm {α : Type u_1} {F : Type u_4} [NormedAddCommGroup F] {x✝ : MeasurableSpace α} (f : α → F) (q : ℝ) (μ : MeasureTheory.Measure α) : MeasureTheory.eLpNorm' f q μ = (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ (1 / q)

@[deprecated MeasureTheory.eLpNorm'_eq_lintegral_enorm (since := "2025-01-17")]

theorem MeasureTheory.eLpNorm'_eq_lintegral_nnnorm {α : Type u_1} {F : Type u_4} [NormedAddCommGroup F] {x✝ : MeasurableSpace α} (f : α → F) (q : ℝ) (μ : MeasureTheory.Measure α) : MeasureTheory.eLpNorm' f q μ = (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ (1 / q)

Alias of MeasureTheory.eLpNorm'_eq_lintegral_enorm.

def MeasureTheory.eLpNormEssSup {α : Type u_1} {ε : Type u_2} [ENorm ε] {x✝ : MeasurableSpace α} (f : α → ε) (μ : MeasureTheory.Measure α) : ENNReal

seminorm for ℒ∞, equal to the essential supremum of ‖f‖.

Equations

• MeasureTheory.eLpNormEssSup f μ = essSup (fun (x : α) => ‖f x‖ₑ) μ

theorem MeasureTheory.eLpNormEssSup_eq_essSup_enorm {α : Type u_1} {F : Type u_4} [NormedAddCommGroup F] {x✝ : MeasurableSpace α} (f : α → F) (μ : MeasureTheory.Measure α) : MeasureTheory.eLpNormEssSup f μ = essSup (fun (x : α) => ‖f x‖ₑ) μ

@[deprecated MeasureTheory.eLpNormEssSup_eq_essSup_enorm (since := "2025-01-17")]

theorem MeasureTheory.eLpNormEssSup_eq_essSup_nnnorm {α : Type u_1} {F : Type u_4} [NormedAddCommGroup F] {x✝ : MeasurableSpace α} (f : α → F) (μ : MeasureTheory.Measure α) : MeasureTheory.eLpNormEssSup f μ = essSup (fun (x : α) => ‖f x‖ₑ) μ

Alias of MeasureTheory.eLpNormEssSup_eq_essSup_enorm.

def MeasureTheory.eLpNorm {α : Type u_1} {ε : Type u_2} [ENorm ε] {x✝ : MeasurableSpace α} (f : α → ε) (p : ENNReal) (μ : MeasureTheory.Measure α := by volume_tac) : ENNReal

ℒp seminorm, equal to 0 for p=0, to (∫ ‖f a‖^p ∂μ) ^ (1/p) for 0 < p < ∞ and to essSup ‖f‖ μ for p = ∞.

Equations

• MeasureTheory.eLpNorm f p μ = if p = 0 then 0 else if p = ⊤ then MeasureTheory.eLpNormEssSup f μ else MeasureTheory.eLpNorm' f p.toReal μ

theorem MeasureTheory.eLpNorm_eq_eLpNorm' {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) {f : α → F} : MeasureTheory.eLpNorm f p μ = MeasureTheory.eLpNorm' f p.toReal μ

theorem MeasureTheory.eLpNorm_nnreal_eq_eLpNorm' {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : α → F} {p : NNReal} (hp : p ≠ 0) : MeasureTheory.eLpNorm f (↑p) μ = MeasureTheory.eLpNorm' f (↑p) μ

theorem MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) {f : α → F} : MeasureTheory.eLpNorm f p μ = (∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)

@[deprecated MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm (since := "2025-01-17")]

theorem MeasureTheory.eLpNorm_eq_lintegral_rpow_nnnorm {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) {f : α → F} : MeasureTheory.eLpNorm f p μ = (∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)

Alias of MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm.

theorem MeasureTheory.eLpNorm_nnreal_eq_lintegral {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : α → F} {p : NNReal} (hp : p ≠ 0) : MeasureTheory.eLpNorm f (↑p) μ = (∫⁻ (x : α), ‖f x‖ₑ ^ ↑p ∂μ) ^ (1 / ↑p)

theorem MeasureTheory.eLpNorm_one_eq_lintegral_enorm {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : α → F} : MeasureTheory.eLpNorm f 1 μ = ∫⁻ (x : α), ‖f x‖ₑ ∂μ

@[deprecated MeasureTheory.eLpNorm_one_eq_lintegral_enorm (since := "2025-01-17")]

theorem MeasureTheory.eLpNorm_one_eq_lintegral_nnnorm {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : α → F} : MeasureTheory.eLpNorm f 1 μ = ∫⁻ (x : α), ‖f x‖ₑ ∂μ

Alias of MeasureTheory.eLpNorm_one_eq_lintegral_enorm.

@[simp]

theorem MeasureTheory.eLpNorm_exponent_top {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : α → F} : MeasureTheory.eLpNorm f ⊤ μ = MeasureTheory.eLpNormEssSup f μ

def MeasureTheory.Memℒp {ε : Type u_2} [ENorm ε] {α : Type u_6} {x✝ : MeasurableSpace α} [TopologicalSpace ε] (f : α → ε) (p : ENNReal) (μ : MeasureTheory.Measure α := by volume_tac) : Prop

The property that f:α→E is ae strongly measurable and (∫ ‖f a‖^p ∂μ)^(1/p) is finite if p < ∞, or essSup f < ∞ if p = ∞.

Equations

• MeasureTheory.Memℒp f p μ = (MeasureTheory.AEStronglyMeasurable f μ ∧ MeasureTheory.eLpNorm f p μ < ⊤)

theorem MeasureTheory.Memℒp.aestronglyMeasurable {α : Type u_1} {E : Type u_3} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {f : α → E} {p : ENNReal} (h : MeasureTheory.Memℒp f p μ) : MeasureTheory.AEStronglyMeasurable f μ

theorem MeasureTheory.lintegral_rpow_enorm_eq_rpow_eLpNorm' {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {q : ℝ} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : α → F} (hq0_lt : 0 < q) : ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ = MeasureTheory.eLpNorm' f q μ ^ q

@[deprecated MeasureTheory.lintegral_rpow_enorm_eq_rpow_eLpNorm' (since := "2025-01-17")]

theorem MeasureTheory.lintegral_rpow_nnnorm_eq_rpow_eLpNorm' {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {q : ℝ} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : α → F} (hq0_lt : 0 < q) : ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ = MeasureTheory.eLpNorm' f q μ ^ q

Alias of MeasureTheory.lintegral_rpow_enorm_eq_rpow_eLpNorm'.

theorem MeasureTheory.eLpNorm_nnreal_pow_eq_lintegral {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : α → F} {p : NNReal} (hp : p ≠ 0) : MeasureTheory.eLpNorm f (↑p) μ ^ ↑p = ∫⁻ (x : α), ‖f x‖ₑ ^ ↑p ∂μ

theorem MeasureTheory.Memℒp.eLpNorm_lt_top {α : Type u_1} {E : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {f : α → E} (hfp : MeasureTheory.Memℒp f p μ) : MeasureTheory.eLpNorm f p μ < ⊤

theorem MeasureTheory.Memℒp.eLpNorm_ne_top {α : Type u_1} {E : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {f : α → E} (hfp : MeasureTheory.Memℒp f p μ) : MeasureTheory.eLpNorm f p μ ≠ ⊤

theorem MeasureTheory.lintegral_rpow_enorm_lt_top_of_eLpNorm'_lt_top {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {q : ℝ} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : α → F} (hq0_lt : 0 < q) (hfq : MeasureTheory.eLpNorm' f q μ < ⊤) : ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ < ⊤

@[deprecated MeasureTheory.lintegral_rpow_enorm_lt_top_of_eLpNorm'_lt_top (since := "2025-01-17")]

theorem MeasureTheory.lintegral_rpow_nnnorm_lt_top_of_eLpNorm'_lt_top' {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {q : ℝ} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : α → F} (hq0_lt : 0 < q) (hfq : MeasureTheory.eLpNorm' f q μ < ⊤) : ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ < ⊤

Alias of MeasureTheory.lintegral_rpow_enorm_lt_top_of_eLpNorm'_lt_top.

theorem MeasureTheory.lintegral_rpow_enorm_lt_top_of_eLpNorm_lt_top {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : α → F} (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) (hfp : MeasureTheory.eLpNorm f p μ < ⊤) : ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ < ⊤

@[deprecated MeasureTheory.lintegral_rpow_enorm_lt_top_of_eLpNorm_lt_top (since := "2025-01-17")]

theorem MeasureTheory.lintegral_rpow_nnnorm_lt_top_of_eLpNorm_lt_top {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : α → F} (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) (hfp : MeasureTheory.eLpNorm f p μ < ⊤) : ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ < ⊤

Alias of MeasureTheory.lintegral_rpow_enorm_lt_top_of_eLpNorm_lt_top.

theorem MeasureTheory.eLpNorm_lt_top_iff_lintegral_rpow_nnnorm_lt_top {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : α → F} (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) : MeasureTheory.eLpNorm f p μ < ⊤ ↔ ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ < ⊤

@[simp]

theorem MeasureTheory.eLpNorm'_exponent_zero {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : α → F} : MeasureTheory.eLpNorm' f 0 μ = 1

@[simp]

theorem MeasureTheory.eLpNorm_exponent_zero {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : α → F} : MeasureTheory.eLpNorm f 0 μ = 0

@[simp]

theorem MeasureTheory.memℒp_zero_iff_aestronglyMeasurable {α : Type u_1} {E : Type u_3} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {f : α → E} : MeasureTheory.Memℒp f 0 μ ↔ MeasureTheory.AEStronglyMeasurable f μ

@[simp]

theorem MeasureTheory.eLpNorm'_zero {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {q : ℝ} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] (hp0_lt : 0 < q) : MeasureTheory.eLpNorm' 0 q μ = 0

@[simp]

theorem MeasureTheory.eLpNorm'_zero' {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {q : ℝ} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] (hq0_ne : q ≠ 0) (hμ : μ ≠ 0) : MeasureTheory.eLpNorm' 0 q μ = 0

@[simp]

theorem MeasureTheory.eLpNormEssSup_zero {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] : MeasureTheory.eLpNormEssSup 0 μ = 0

@[simp]

theorem MeasureTheory.eLpNorm_zero {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] : MeasureTheory.eLpNorm 0 p μ = 0

@[simp]

theorem MeasureTheory.eLpNorm_zero' {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] : MeasureTheory.eLpNorm (fun (x : α) => 0) p μ = 0

@[simp]

theorem MeasureTheory.Memℒp.zero {α : Type u_1} {E : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] : MeasureTheory.Memℒp 0 p μ

@[simp]

theorem MeasureTheory.Memℒp.zero' {α : Type u_1} {E : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] : MeasureTheory.Memℒp (fun (x : α) => 0) p μ

@[deprecated MeasureTheory.Memℒp.zero (since := "2025-01-21")]

theorem MeasureTheory.zero_memℒp {α : Type u_1} {E : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] : MeasureTheory.Memℒp 0 p μ

Alias of MeasureTheory.Memℒp.zero.

@[deprecated MeasureTheory.Memℒp.zero' (since := "2025-01-21")]

theorem MeasureTheory.zero_mem_ℒp {α : Type u_1} {E : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] : MeasureTheory.Memℒp (fun (x : α) => 0) p μ

Alias of MeasureTheory.Memℒp.zero'.

theorem MeasureTheory.eLpNorm'_measure_zero_of_pos {α : Type u_1} {F : Type u_4} {q : ℝ} [NormedAddCommGroup F] [MeasurableSpace α] {f : α → F} (hq_pos : 0 < q) : MeasureTheory.eLpNorm' f q 0 = 0

theorem MeasureTheory.eLpNorm'_measure_zero_of_exponent_zero {α : Type u_1} {F : Type u_4} [NormedAddCommGroup F] [MeasurableSpace α] {f : α → F} : MeasureTheory.eLpNorm' f 0 0 = 1

theorem MeasureTheory.eLpNorm'_measure_zero_of_neg {α : Type u_1} {F : Type u_4} {q : ℝ} [NormedAddCommGroup F] [MeasurableSpace α] {f : α → F} (hq_neg : q < 0) : MeasureTheory.eLpNorm' f q 0 = ⊤

@[simp]

theorem MeasureTheory.eLpNormEssSup_measure_zero {α : Type u_1} {F : Type u_4} [NormedAddCommGroup F] [MeasurableSpace α] {f : α → F} : MeasureTheory.eLpNormEssSup f 0 = 0

@[simp]

theorem MeasureTheory.eLpNorm_measure_zero {α : Type u_1} {F : Type u_4} {p : ENNReal} [NormedAddCommGroup F] [MeasurableSpace α] {f : α → F} : MeasureTheory.eLpNorm f p 0 = 0

@[simp]

theorem MeasureTheory.memℒp_measure_zero {α : Type u_1} {F : Type u_4} {p : ENNReal} [NormedAddCommGroup F] [MeasurableSpace α] {f : α → F} : MeasureTheory.Memℒp f p 0

@[simp]

theorem MeasureTheory.eLpNorm'_neg {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} [NormedAddCommGroup F] (f : α → F) (q : ℝ) (μ : MeasureTheory.Measure α) : MeasureTheory.eLpNorm' (-f) q μ = MeasureTheory.eLpNorm' f q μ

@[simp]

theorem MeasureTheory.eLpNorm_neg {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} [NormedAddCommGroup F] (f : α → F) (p : ENNReal) (μ : MeasureTheory.Measure α) : MeasureTheory.eLpNorm (-f) p μ = MeasureTheory.eLpNorm f p μ

theorem MeasureTheory.eLpNorm_sub_comm {α : Type u_1} {E : Type u_3} {m0 : MeasurableSpace α} [NormedAddCommGroup E] (f g : α → E) (p : ENNReal) (μ : MeasureTheory.Measure α) : MeasureTheory.eLpNorm (f - g) p μ = MeasureTheory.eLpNorm (g - f) p μ

theorem MeasureTheory.Memℒp.neg {α : Type u_1} {E : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {f : α → E} (hf : MeasureTheory.Memℒp f p μ) : MeasureTheory.Memℒp (-f) p μ

theorem MeasureTheory.memℒp_neg_iff {α : Type u_1} {E : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {f : α → E} : MeasureTheory.Memℒp (-f) p μ ↔ MeasureTheory.Memℒp f p μ

theorem MeasureTheory.eLpNorm'_const {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {q : ℝ} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] (c : F) (hq_pos : 0 < q) : MeasureTheory.eLpNorm' (fun (x : α) => c) q μ = ‖c‖ₑ * μ Set.univ ^ (1 / q)

theorem MeasureTheory.eLpNorm'_const' {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {q : ℝ} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] [MeasureTheory.IsFiniteMeasure μ] (c : F) (hc_ne_zero : c ≠ 0) (hq_ne_zero : q ≠ 0) : MeasureTheory.eLpNorm' (fun (x : α) => c) q μ = ‖c‖ₑ * μ Set.univ ^ (1 / q)

theorem MeasureTheory.eLpNormEssSup_const {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] (c : F) (hμ : μ ≠ 0) : MeasureTheory.eLpNormEssSup (fun (x : α) => c) μ = ‖c‖ₑ

theorem MeasureTheory.eLpNorm'_const_of_isProbabilityMeasure {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {q : ℝ} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] (c : F) (hq_pos : 0 < q) [MeasureTheory.IsProbabilityMeasure μ] : MeasureTheory.eLpNorm' (fun (x : α) => c) q μ = ‖c‖ₑ

theorem MeasureTheory.eLpNorm_const {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] (c : F) (h0 : p ≠ 0) (hμ : μ ≠ 0) : MeasureTheory.eLpNorm (fun (x : α) => c) p μ = ‖c‖ₑ * μ Set.univ ^ (1 / p.toReal)

theorem MeasureTheory.eLpNorm_const' {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] (c : F) (h0 : p ≠ 0) (h_top : p ≠ ⊤) : MeasureTheory.eLpNorm (fun (x : α) => c) p μ = ‖c‖ₑ * μ Set.univ ^ (1 / p.toReal)

theorem MeasureTheory.eLpNorm_const_lt_top_iff {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {p : ENNReal} {c : F} (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) : MeasureTheory.eLpNorm (fun (x : α) => c) p μ < ⊤ ↔ c = 0 ∨ μ Set.univ < ⊤

theorem MeasureTheory.memℒp_const {α : Type u_1} {E : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] (c : E) [MeasureTheory.IsFiniteMeasure μ] : MeasureTheory.Memℒp (fun (x : α) => c) p μ

theorem MeasureTheory.memℒp_top_const {α : Type u_1} {E : Type u_3} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] (c : E) : MeasureTheory.Memℒp (fun (x : α) => c) ⊤ μ

theorem MeasureTheory.memℒp_const_iff {α : Type u_1} {E : Type u_3} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {p : ENNReal} {c : E} (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) : MeasureTheory.Memℒp (fun (x : α) => c) p μ ↔ c = 0 ∨ μ Set.univ < ⊤

theorem MeasureTheory.eLpNorm'_mono_nnnorm_ae {α : Type u_1} {F : Type u_4} {G : Type u_5} {m0 : MeasurableSpace α} {q : ℝ} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] [NormedAddCommGroup G] {f : α → F} {g : α → G} (hq : 0 ≤ q) (h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ ‖g x‖₊) : MeasureTheory.eLpNorm' f q μ ≤ MeasureTheory.eLpNorm' g q μ

theorem MeasureTheory.eLpNorm'_mono_ae {α : Type u_1} {F : Type u_4} {G : Type u_5} {m0 : MeasurableSpace α} {q : ℝ} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] [NormedAddCommGroup G] {f : α → F} {g : α → G} (hq : 0 ≤ q) (h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖g x‖) : MeasureTheory.eLpNorm' f q μ ≤ MeasureTheory.eLpNorm' g q μ

theorem MeasureTheory.eLpNorm'_congr_nnnorm_ae {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {q : ℝ} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f g : α → F} (hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ = ‖g x‖₊) : MeasureTheory.eLpNorm' f q μ = MeasureTheory.eLpNorm' g q μ

theorem MeasureTheory.eLpNorm'_congr_norm_ae {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {q : ℝ} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f g : α → F} (hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖ = ‖g x‖) : MeasureTheory.eLpNorm' f q μ = MeasureTheory.eLpNorm' g q μ

theorem MeasureTheory.eLpNorm'_congr_ae {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {q : ℝ} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f g : α → F} (hfg : f =ᵐ[μ] g) : MeasureTheory.eLpNorm' f q μ = MeasureTheory.eLpNorm' g q μ

theorem MeasureTheory.eLpNormEssSup_congr_ae {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f g : α → F} (hfg : f =ᵐ[μ] g) : MeasureTheory.eLpNormEssSup f μ = MeasureTheory.eLpNormEssSup g μ

theorem MeasureTheory.eLpNormEssSup_mono_nnnorm_ae {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f g : α → F} (hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ ‖g x‖₊) : MeasureTheory.eLpNormEssSup f μ ≤ MeasureTheory.eLpNormEssSup g μ

theorem MeasureTheory.eLpNorm_mono_nnnorm_ae {α : Type u_1} {F : Type u_4} {G : Type u_5} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] [NormedAddCommGroup G] {f : α → F} {g : α → G} (h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ ‖g x‖₊) : MeasureTheory.eLpNorm f p μ ≤ MeasureTheory.eLpNorm g p μ

theorem MeasureTheory.eLpNorm_mono_ae {α : Type u_1} {F : Type u_4} {G : Type u_5} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] [NormedAddCommGroup G] {f : α → F} {g : α → G} (h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖g x‖) : MeasureTheory.eLpNorm f p μ ≤ MeasureTheory.eLpNorm g p μ

theorem MeasureTheory.eLpNorm_mono_ae_real {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : α → F} {g : α → ℝ} (h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ g x) : MeasureTheory.eLpNorm f p μ ≤ MeasureTheory.eLpNorm g p μ

theorem MeasureTheory.eLpNorm_mono_nnnorm {α : Type u_1} {F : Type u_4} {G : Type u_5} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] [NormedAddCommGroup G] {f : α → F} {g : α → G} (h : ∀ (x : α), ‖f x‖₊ ≤ ‖g x‖₊) : MeasureTheory.eLpNorm f p μ ≤ MeasureTheory.eLpNorm g p μ

theorem MeasureTheory.eLpNorm_mono {α : Type u_1} {F : Type u_4} {G : Type u_5} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] [NormedAddCommGroup G] {f : α → F} {g : α → G} (h : ∀ (x : α), ‖f x‖ ≤ ‖g x‖) : MeasureTheory.eLpNorm f p μ ≤ MeasureTheory.eLpNorm g p μ

theorem MeasureTheory.eLpNorm_mono_real {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : α → F} {g : α → ℝ} (h : ∀ (x : α), ‖f x‖ ≤ g x) : MeasureTheory.eLpNorm f p μ ≤ MeasureTheory.eLpNorm g p μ

theorem MeasureTheory.eLpNormEssSup_le_of_ae_nnnorm_bound {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : α → F} {C : NNReal} (hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ C) : MeasureTheory.eLpNormEssSup f μ ≤ ↑C

theorem MeasureTheory.eLpNormEssSup_le_of_ae_bound {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : α → F} {C : ℝ} (hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C) : MeasureTheory.eLpNormEssSup f μ ≤ ENNReal.ofReal C

theorem MeasureTheory.eLpNormEssSup_lt_top_of_ae_nnnorm_bound {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : α → F} {C : NNReal} (hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ C) : MeasureTheory.eLpNormEssSup f μ < ⊤

theorem MeasureTheory.eLpNormEssSup_lt_top_of_ae_bound {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : α → F} {C : ℝ} (hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C) : MeasureTheory.eLpNormEssSup f μ < ⊤

theorem MeasureTheory.eLpNorm_le_of_ae_nnnorm_bound {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : α → F} {C : NNReal} (hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ C) : MeasureTheory.eLpNorm f p μ ≤ C • μ Set.univ ^ p.toReal⁻¹

theorem MeasureTheory.eLpNorm_le_of_ae_bound {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : α → F} {C : ℝ} (hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C) : MeasureTheory.eLpNorm f p μ ≤ μ Set.univ ^ p.toReal⁻¹ * ENNReal.ofReal C

theorem MeasureTheory.eLpNorm_congr_nnnorm_ae {α : Type u_1} {F : Type u_4} {G : Type u_5} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] [NormedAddCommGroup G] {f : α → F} {g : α → G} (hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ = ‖g x‖₊) : MeasureTheory.eLpNorm f p μ = MeasureTheory.eLpNorm g p μ

theorem MeasureTheory.eLpNorm_congr_norm_ae {α : Type u_1} {F : Type u_4} {G : Type u_5} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] [NormedAddCommGroup G] {f : α → F} {g : α → G} (hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖ = ‖g x‖) : MeasureTheory.eLpNorm f p μ = MeasureTheory.eLpNorm g p μ

theorem MeasureTheory.eLpNorm_indicator_sub_indicator {α : Type u_1} {E : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] (s t : Set α) (f : α → E) : MeasureTheory.eLpNorm (s.indicator f - t.indicator f) p μ = MeasureTheory.eLpNorm ((symmDiff s t).indicator f) p μ

@[simp]

theorem MeasureTheory.eLpNorm'_norm {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {q : ℝ} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : α → F} : MeasureTheory.eLpNorm' (fun (a : α) => ‖f a‖) q μ = MeasureTheory.eLpNorm' f q μ

@[simp]

theorem MeasureTheory.eLpNorm_norm {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] (f : α → F) : MeasureTheory.eLpNorm (fun (x : α) => ‖f x‖) p μ = MeasureTheory.eLpNorm f p μ

theorem MeasureTheory.eLpNorm'_norm_rpow {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] (f : α → F) (p q : ℝ) (hq_pos : 0 < q) : MeasureTheory.eLpNorm' (fun (x : α) => ‖f x‖ ^ q) p μ = MeasureTheory.eLpNorm' f (p * q) μ ^ q

theorem MeasureTheory.eLpNorm_norm_rpow {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {q : ℝ} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] (f : α → F) (hq_pos : 0 < q) : MeasureTheory.eLpNorm (fun (x : α) => ‖f x‖ ^ q) p μ = MeasureTheory.eLpNorm f (p * ENNReal.ofReal q) μ ^ q

theorem MeasureTheory.eLpNorm_congr_ae {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f g : α → F} (hfg : f =ᵐ[μ] g) : MeasureTheory.eLpNorm f p μ = MeasureTheory.eLpNorm g p μ

theorem MeasureTheory.memℒp_congr_ae {α : Type u_1} {E : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {f g : α → E} (hfg : f =ᵐ[μ] g) : MeasureTheory.Memℒp f p μ ↔ MeasureTheory.Memℒp g p μ

theorem MeasureTheory.Memℒp.ae_eq {α : Type u_1} {E : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {f g : α → E} (hfg : f =ᵐ[μ] g) (hf_Lp : MeasureTheory.Memℒp f p μ) : MeasureTheory.Memℒp g p μ

theorem MeasureTheory.Memℒp.of_le {α : Type u_1} {E : Type u_3} {F : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] {f : α → E} {g : α → F} (hg : MeasureTheory.Memℒp g p μ) (hf : MeasureTheory.AEStronglyMeasurable f μ) (hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖g x‖) : MeasureTheory.Memℒp f p μ

theorem MeasureTheory.Memℒp.mono {α : Type u_1} {E : Type u_3} {F : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] {f : α → E} {g : α → F} (hg : MeasureTheory.Memℒp g p μ) (hf : MeasureTheory.AEStronglyMeasurable f μ) (hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖g x‖) : MeasureTheory.Memℒp f p μ

Alias of MeasureTheory.Memℒp.of_le.

theorem MeasureTheory.Memℒp.mono' {α : Type u_1} {E : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {f : α → E} {g : α → ℝ} (hg : MeasureTheory.Memℒp g p μ) (hf : MeasureTheory.AEStronglyMeasurable f μ) (h : ∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ g a) : MeasureTheory.Memℒp f p μ

theorem MeasureTheory.Memℒp.congr_norm {α : Type u_1} {E : Type u_3} {F : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] {f : α → E} {g : α → F} (hf : MeasureTheory.Memℒp f p μ) (hg : MeasureTheory.AEStronglyMeasurable g μ) (h : ∀ᵐ (a : α) ∂μ, ‖f a‖ = ‖g a‖) : MeasureTheory.Memℒp g p μ

theorem MeasureTheory.memℒp_congr_norm {α : Type u_1} {E : Type u_3} {F : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] {f : α → E} {g : α → F} (hf : MeasureTheory.AEStronglyMeasurable f μ) (hg : MeasureTheory.AEStronglyMeasurable g μ) (h : ∀ᵐ (a : α) ∂μ, ‖f a‖ = ‖g a‖) : MeasureTheory.Memℒp f p μ ↔ MeasureTheory.Memℒp g p μ

theorem MeasureTheory.memℒp_top_of_bound {α : Type u_1} {E : Type u_3} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {f : α → E} (hf : MeasureTheory.AEStronglyMeasurable f μ) (C : ℝ) (hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C) : MeasureTheory.Memℒp f ⊤ μ

theorem MeasureTheory.Memℒp.of_bound {α : Type u_1} {E : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [MeasureTheory.IsFiniteMeasure μ] {f : α → E} (hf : MeasureTheory.AEStronglyMeasurable f μ) (C : ℝ) (hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C) : MeasureTheory.Memℒp f p μ

theorem MeasureTheory.memℒp_of_bounded {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {a b : ℝ} {f : α → ℝ} (h : ∀ᵐ (x : α) ∂μ, f x ∈ Set.Icc a b) (hX : MeasureTheory.AEStronglyMeasurable f μ) (p : ENNReal) : MeasureTheory.Memℒp f p μ

theorem MeasureTheory.eLpNorm'_mono_measure {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {q : ℝ} {μ ν : MeasureTheory.Measure α} [NormedAddCommGroup F] (f : α → F) (hμν : ν ≤ μ) (hq : 0 ≤ q) : MeasureTheory.eLpNorm' f q ν ≤ MeasureTheory.eLpNorm' f q μ

theorem MeasureTheory.eLpNormEssSup_mono_measure {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [NormedAddCommGroup F] (f : α → F) (hμν : ν.AbsolutelyContinuous μ) : MeasureTheory.eLpNormEssSup f ν ≤ MeasureTheory.eLpNormEssSup f μ

theorem MeasureTheory.eLpNorm_mono_measure {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ ν : MeasureTheory.Measure α} [NormedAddCommGroup F] (f : α → F) (hμν : ν ≤ μ) : MeasureTheory.eLpNorm f p ν ≤ MeasureTheory.eLpNorm f p μ

theorem MeasureTheory.Memℒp.mono_measure {α : Type u_1} {E : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ ν : MeasureTheory.Measure α} [NormedAddCommGroup E] {f : α → E} (hμν : ν ≤ μ) (hf : MeasureTheory.Memℒp f p μ) : MeasureTheory.Memℒp f p ν

theorem MeasureTheory.eLpNorm_indicator_eq_eLpNorm_restrict {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : α → F} {s : Set α} (hs : MeasurableSet s) : MeasureTheory.eLpNorm (s.indicator f) p μ = MeasureTheory.eLpNorm f p (μ.restrict s)

@[deprecated MeasureTheory.eLpNorm_indicator_eq_eLpNorm_restrict (since := "2025-01-07")]

theorem MeasureTheory.eLpNorm_indicator_eq_restrict {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : α → F} {s : Set α} (hs : MeasurableSet s) : MeasureTheory.eLpNorm (s.indicator f) p μ = MeasureTheory.eLpNorm f p (μ.restrict s)

Alias of MeasureTheory.eLpNorm_indicator_eq_eLpNorm_restrict.

theorem MeasureTheory.eLpNormEssSup_indicator_eq_eLpNormEssSup_restrict {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : α → F} {s : Set α} (hs : MeasurableSet s) : MeasureTheory.eLpNormEssSup (s.indicator f) μ = MeasureTheory.eLpNormEssSup f (μ.restrict s)

theorem MeasureTheory.eLpNorm_restrict_le {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} [NormedAddCommGroup F] (f : α → F) (p : ENNReal) (μ : MeasureTheory.Measure α) (s : Set α) : MeasureTheory.eLpNorm f p (μ.restrict s) ≤ MeasureTheory.eLpNorm f p μ

theorem MeasureTheory.eLpNorm_indicator_le {α : Type u_1} {E : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {s : Set α} (f : α → E) : MeasureTheory.eLpNorm (s.indicator f) p μ ≤ MeasureTheory.eLpNorm f p μ

theorem MeasureTheory.eLpNormEssSup_indicator_le {α : Type u_1} {G : Type u_5} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup G] (s : Set α) (f : α → G) : MeasureTheory.eLpNormEssSup (s.indicator f) μ ≤ MeasureTheory.eLpNormEssSup f μ

theorem MeasureTheory.eLpNormEssSup_indicator_const_le {α : Type u_1} {G : Type u_5} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup G] (s : Set α) (c : G) : MeasureTheory.eLpNormEssSup (s.indicator fun (x : α) => c) μ ≤ ‖c‖ₑ

theorem MeasureTheory.eLpNormEssSup_indicator_const_eq {α : Type u_1} {G : Type u_5} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup G] (s : Set α) (c : G) (hμs : μ s ≠ 0) : MeasureTheory.eLpNormEssSup (s.indicator fun (x : α) => c) μ = ‖c‖ₑ

theorem MeasureTheory.eLpNorm_indicator_const₀ {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {c : F} {s : Set α} (hs : MeasureTheory.NullMeasurableSet s μ) (hp : p ≠ 0) (hp_top : p ≠ ⊤) : MeasureTheory.eLpNorm (s.indicator fun (x : α) => c) p μ = ‖c‖ₑ * μ s ^ (1 / p.toReal)

theorem MeasureTheory.eLpNorm_indicator_const {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {c : F} {s : Set α} (hs : MeasurableSet s) (hp : p ≠ 0) (hp_top : p ≠ ⊤) : MeasureTheory.eLpNorm (s.indicator fun (x : α) => c) p μ = ‖c‖ₑ * μ s ^ (1 / p.toReal)

theorem MeasureTheory.eLpNorm_indicator_const' {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {c : F} {s : Set α} (hs : MeasurableSet s) (hμs : μ s ≠ 0) (hp : p ≠ 0) : MeasureTheory.eLpNorm (s.indicator fun (x : α) => c) p μ = ‖c‖ₑ * μ s ^ (1 / p.toReal)

theorem MeasureTheory.eLpNorm_indicator_const_le {α : Type u_1} {G : Type u_5} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup G] {s : Set α} (c : G) (p : ENNReal) : MeasureTheory.eLpNorm (s.indicator fun (x : α) => c) p μ ≤ ‖c‖ₑ * μ s ^ (1 / p.toReal)

theorem MeasureTheory.Memℒp.indicator {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : α → F} {s : Set α} (hs : MeasurableSet s) (hf : MeasureTheory.Memℒp f p μ) : MeasureTheory.Memℒp (s.indicator f) p μ

theorem MeasureTheory.memℒp_indicator_iff_restrict {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : α → F} {s : Set α} (hs : MeasurableSet s) : MeasureTheory.Memℒp (s.indicator f) p μ ↔ MeasureTheory.Memℒp f p (μ.restrict s)

theorem MeasureTheory.memℒp_indicator_const {α : Type u_1} {E : Type u_3} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {s : Set α} (p : ENNReal) (hs : MeasurableSet s) (c : E) (hμsc : c = 0 ∨ μ s ≠ ⊤) : MeasureTheory.Memℒp (s.indicator fun (x : α) => c) p μ

theorem MeasureTheory.eLpNormEssSup_piecewise {α : Type u_1} {E : Type u_3} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {s : Set α} (f g : α → E) [DecidablePred fun (x : α) => x ∈ s] (hs : MeasurableSet s) : MeasureTheory.eLpNormEssSup (s.piecewise f g) μ = MeasureTheory.eLpNormEssSup f (μ.restrict s) ⊔ MeasureTheory.eLpNormEssSup g (μ.restrict sᶜ)

theorem MeasureTheory.eLpNorm_top_piecewise {α : Type u_1} {E : Type u_3} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {s : Set α} (f g : α → E) [DecidablePred fun (x : α) => x ∈ s] (hs : MeasurableSet s) : MeasureTheory.eLpNorm (s.piecewise f g) ⊤ μ = MeasureTheory.eLpNorm f ⊤ (μ.restrict s) ⊔ MeasureTheory.eLpNorm g ⊤ (μ.restrict sᶜ)

theorem MeasureTheory.Memℒp.piecewise {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : α → F} {s : Set α} [DecidablePred fun (x : α) => x ∈ s] {g : α → F} (hs : MeasurableSet s) (hf : MeasureTheory.Memℒp f p (μ.restrict s)) (hg : MeasureTheory.Memℒp g p (μ.restrict sᶜ)) : MeasureTheory.Memℒp (s.piecewise f g) p μ

theorem MeasureTheory.eLpNorm_restrict_eq_of_support_subset {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {s : Set α} {f : α → F} (hsf : Function.support f ⊆ s) : MeasureTheory.eLpNorm f p (μ.restrict s) = MeasureTheory.eLpNorm f p μ

For a function f with support in s, the Lᵖ norms of f with respect to μ and μ.restrict s are the same.

theorem MeasureTheory.Memℒp.restrict {α : Type u_1} {E : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] (s : Set α) {f : α → E} (hf : MeasureTheory.Memℒp f p μ) : MeasureTheory.Memℒp f p (μ.restrict s)

theorem MeasureTheory.eLpNorm'_smul_measure {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {p : ℝ} (hp : 0 ≤ p) {f : α → F} (c : ENNReal) : MeasureTheory.eLpNorm' f p (c • μ) = c ^ (1 / p) * MeasureTheory.eLpNorm' f p μ

@[simp]

theorem MeasureTheory.eLpNormEssSup_smul_measure {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {R : Type u_6} [Zero R] [SMulWithZero R ENNReal] [IsScalarTower R ENNReal ENNReal] [NoZeroSMulDivisors R ENNReal] {c : R} (hc : c ≠ 0) (f : α → F) : MeasureTheory.eLpNormEssSup f (c • μ) = MeasureTheory.eLpNormEssSup f μ

theorem MeasureTheory.eLpNorm_smul_measure_of_ne_zero {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} [NormedAddCommGroup F] {c : ENNReal} (hc : c ≠ 0) (f : α → F) (p : ENNReal) (μ : MeasureTheory.Measure α) : MeasureTheory.eLpNorm f p (c • μ) = c ^ (1 / p).toReal • MeasureTheory.eLpNorm f p μ

See eLpNorm_smul_measure_of_ne_zero' for a version with scalar multiplication by ℝ≥0.

theorem MeasureTheory.eLpNorm_smul_measure_of_ne_zero' {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} [NormedAddCommGroup F] {c : NNReal} (hc : c ≠ 0) (f : α → F) (p : ENNReal) (μ : MeasureTheory.Measure α) : MeasureTheory.eLpNorm f p (c • μ) = c ^ p.toReal⁻¹ • MeasureTheory.eLpNorm f p μ

See eLpNorm_smul_measure_of_ne_zero for a version with scalar multiplication by ℝ≥0∞.

theorem MeasureTheory.eLpNorm_smul_measure_of_ne_top {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {p : ENNReal} (hp_ne_top : p ≠ ⊤) (f : α → F) (c : ENNReal) : MeasureTheory.eLpNorm f p (c • μ) = c ^ (1 / p).toReal • MeasureTheory.eLpNorm f p μ

See eLpNorm_smul_measure_of_ne_top' for a version with scalar multiplication by ℝ≥0.

theorem MeasureTheory.eLpNorm_smul_measure_of_ne_top' {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] (hp : p ≠ ⊤) (c : NNReal) (f : α → F) : MeasureTheory.eLpNorm f p (c • μ) = c ^ p.toReal⁻¹ • MeasureTheory.eLpNorm f p μ

See eLpNorm_smul_measure_of_ne_top' for a version with scalar multiplication by ℝ≥0∞.

theorem MeasureTheory.eLpNorm_one_smul_measure {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : α → F} (c : ENNReal) : MeasureTheory.eLpNorm f 1 (c • μ) = c * MeasureTheory.eLpNorm f 1 μ

theorem MeasureTheory.Memℒp.of_measure_le_smul {α : Type u_1} {E : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {μ' : MeasureTheory.Measure α} (c : ENNReal) (hc : c ≠ ⊤) (hμ'_le : μ' ≤ c • μ) {f : α → E} (hf : MeasureTheory.Memℒp f p μ) : MeasureTheory.Memℒp f p μ'

theorem MeasureTheory.Memℒp.smul_measure {α : Type u_1} {E : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {f : α → E} {c : ENNReal} (hf : MeasureTheory.Memℒp f p μ) (hc : c ≠ ⊤) : MeasureTheory.Memℒp f p (c • μ)

theorem MeasureTheory.eLpNorm_one_add_measure {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} [NormedAddCommGroup F] (f : α → F) (μ ν : MeasureTheory.Measure α) : MeasureTheory.eLpNorm f 1 (μ + ν) = MeasureTheory.eLpNorm f 1 μ + MeasureTheory.eLpNorm f 1 ν

theorem MeasureTheory.eLpNorm_le_add_measure_right {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} [NormedAddCommGroup F] (f : α → F) (μ ν : MeasureTheory.Measure α) {p : ENNReal} : MeasureTheory.eLpNorm f p μ ≤ MeasureTheory.eLpNorm f p (μ + ν)

theorem MeasureTheory.eLpNorm_le_add_measure_left {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} [NormedAddCommGroup F] (f : α → F) (μ ν : MeasureTheory.Measure α) {p : ENNReal} : MeasureTheory.eLpNorm f p ν ≤ MeasureTheory.eLpNorm f p (μ + ν)

theorem MeasureTheory.eLpNormEssSup_eq_iSup {α : Type u_1} {E : Type u_3} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] (hμ : ∀ (a : α), μ {a} ≠ 0) (f : α → E) : MeasureTheory.eLpNormEssSup f μ = ⨆ (a : α), ‖f a‖ₑ

@[simp]

theorem MeasureTheory.eLpNormEssSup_count {α : Type u_1} {E : Type u_3} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [MeasurableSingletonClass α] (f : α → E) : MeasureTheory.eLpNormEssSup f MeasureTheory.Measure.count = ⨆ (a : α), ‖f a‖ₑ

theorem MeasureTheory.Memℒp.left_of_add_measure {α : Type u_1} {E : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ ν : MeasureTheory.Measure α} [NormedAddCommGroup E] {f : α → E} (h : MeasureTheory.Memℒp f p (μ + ν)) : MeasureTheory.Memℒp f p μ

theorem MeasureTheory.Memℒp.right_of_add_measure {α : Type u_1} {E : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ ν : MeasureTheory.Measure α} [NormedAddCommGroup E] {f : α → E} (h : MeasureTheory.Memℒp f p (μ + ν)) : MeasureTheory.Memℒp f p ν

theorem MeasureTheory.Memℒp.norm {α : Type u_1} {E : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {f : α → E} (h : MeasureTheory.Memℒp f p μ) : MeasureTheory.Memℒp (fun (x : α) => ‖f x‖) p μ

theorem MeasureTheory.memℒp_norm_iff {α : Type u_1} {E : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {f : α → E} (hf : MeasureTheory.AEStronglyMeasurable f μ) : MeasureTheory.Memℒp (fun (x : α) => ‖f x‖) p μ ↔ MeasureTheory.Memℒp f p μ

theorem MeasureTheory.eLpNorm'_eq_zero_of_ae_zero {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {q : ℝ} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : α → F} (hq0_lt : 0 < q) (hf_zero : f =ᵐ[μ] 0) : MeasureTheory.eLpNorm' f q μ = 0

theorem MeasureTheory.eLpNorm'_eq_zero_of_ae_zero' {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {q : ℝ} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] (hq0_ne : q ≠ 0) (hμ : μ ≠ 0) {f : α → F} (hf_zero : f =ᵐ[μ] 0) : MeasureTheory.eLpNorm' f q μ = 0

theorem MeasureTheory.ae_eq_zero_of_eLpNorm'_eq_zero {α : Type u_1} {E : Type u_3} {m0 : MeasurableSpace α} {q : ℝ} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {f : α → E} (hq0 : 0 ≤ q) (hf : MeasureTheory.AEStronglyMeasurable f μ) (h : MeasureTheory.eLpNorm' f q μ = 0) : f =ᵐ[μ] 0

theorem MeasureTheory.eLpNorm'_eq_zero_iff {α : Type u_1} {E : Type u_3} {m0 : MeasurableSpace α} {q : ℝ} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] (hq0_lt : 0 < q) {f : α → E} (hf : MeasureTheory.AEStronglyMeasurable f μ) : MeasureTheory.eLpNorm' f q μ = 0 ↔ f =ᵐ[μ] 0

theorem MeasureTheory.coe_nnnorm_ae_le_eLpNormEssSup {α : Type u_1} {F : Type u_4} [NormedAddCommGroup F] {x✝ : MeasurableSpace α} (f : α → F) (μ : MeasureTheory.Measure α) : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ MeasureTheory.eLpNormEssSup f μ

@[simp]

theorem MeasureTheory.eLpNormEssSup_eq_zero_iff {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : α → F} : MeasureTheory.eLpNormEssSup f μ = 0 ↔ f =ᵐ[μ] 0

theorem MeasureTheory.eLpNorm_eq_zero_iff {α : Type u_1} {E : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {f : α → E} (hf : MeasureTheory.AEStronglyMeasurable f μ) (h0 : p ≠ 0) : MeasureTheory.eLpNorm f p μ = 0 ↔ f =ᵐ[μ] 0

theorem MeasureTheory.eLpNorm_eq_zero_of_ae_zero {α : Type u_1} {E : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {f : α → E} (hf : f =ᵐ[μ] 0) : MeasureTheory.eLpNorm f p μ = 0

theorem MeasureTheory.ae_le_eLpNormEssSup {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : α → F} : ∀ᵐ (y : α) ∂μ, ‖f y‖ₑ ≤ MeasureTheory.eLpNormEssSup f μ

theorem MeasureTheory.eLpNormEssSup_lt_top_iff_isBoundedUnder {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : α → F} : MeasureTheory.eLpNormEssSup f μ < ⊤ ↔ Filter.IsBoundedUnder (fun (x1 x2 : NNReal) => x1 ≤ x2) (MeasureTheory.ae μ) fun (x : α) => ‖f x‖₊

theorem MeasureTheory.meas_eLpNormEssSup_lt {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : α → F} : μ {y : α | MeasureTheory.eLpNormEssSup f μ < ‖f y‖ₑ} = 0

theorem MeasureTheory.eLpNorm_lt_top_of_finite {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : α → F} [Finite α] [MeasureTheory.IsFiniteMeasure μ] : MeasureTheory.eLpNorm f p μ < ⊤

@[simp]

theorem MeasureTheory.Memℒp.of_discrete {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : α → F} [DiscreteMeasurableSpace α] [Finite α] [MeasureTheory.IsFiniteMeasure μ] : MeasureTheory.Memℒp f p μ

@[simp]

theorem MeasureTheory.eLpNorm_of_isEmpty {α : Type u_1} {E : Type u_3} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [IsEmpty α] (f : α → E) (p : ENNReal) : MeasureTheory.eLpNorm f p μ = 0

theorem MeasureTheory.eLpNormEssSup_map_measure {α : Type u_1} {E : Type u_3} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {β : Type u_6} {mβ : MeasurableSpace β} {f : α → β} {g : β → E} (hg : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map f μ)) (hf : AEMeasurable f μ) : MeasureTheory.eLpNormEssSup g (MeasureTheory.Measure.map f μ) = MeasureTheory.eLpNormEssSup (g ∘ f) μ

theorem MeasureTheory.eLpNorm_map_measure {α : Type u_1} {E : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {β : Type u_6} {mβ : MeasurableSpace β} {f : α → β} {g : β → E} (hg : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map f μ)) (hf : AEMeasurable f μ) : MeasureTheory.eLpNorm g p (MeasureTheory.Measure.map f μ) = MeasureTheory.eLpNorm (g ∘ f) p μ

theorem MeasureTheory.memℒp_map_measure_iff {α : Type u_1} {E : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {β : Type u_6} {mβ : MeasurableSpace β} {f : α → β} {g : β → E} (hg : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map f μ)) (hf : AEMeasurable f μ) : MeasureTheory.Memℒp g p (MeasureTheory.Measure.map f μ) ↔ MeasureTheory.Memℒp (g ∘ f) p μ

theorem MeasureTheory.Memℒp.comp_of_map {α : Type u_1} {E : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {β : Type u_6} {mβ : MeasurableSpace β} {f : α → β} {g : β → E} (hg : MeasureTheory.Memℒp g p (MeasureTheory.Measure.map f μ)) (hf : AEMeasurable f μ) : MeasureTheory.Memℒp (g ∘ f) p μ

theorem MeasureTheory.eLpNorm_comp_measurePreserving {α : Type u_1} {E : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {β : Type u_6} {mβ : MeasurableSpace β} {f : α → β} {g : β → E} {ν : MeasureTheory.Measure β} (hg : MeasureTheory.AEStronglyMeasurable g ν) (hf : MeasureTheory.MeasurePreserving f μ ν) : MeasureTheory.eLpNorm (g ∘ f) p μ = MeasureTheory.eLpNorm g p ν

theorem MeasureTheory.AEEqFun.eLpNorm_compMeasurePreserving {α : Type u_1} {E : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {β : Type u_6} {mβ : MeasurableSpace β} {f : α → β} {ν : MeasureTheory.Measure β} (g : β →ₘ[ν] E) (hf : MeasureTheory.MeasurePreserving f μ ν) : MeasureTheory.eLpNorm (↑(g.compMeasurePreserving f hf)) p μ = MeasureTheory.eLpNorm (↑g) p ν

theorem MeasureTheory.Memℒp.comp_measurePreserving {α : Type u_1} {E : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {β : Type u_6} {mβ : MeasurableSpace β} {f : α → β} {g : β → E} {ν : MeasureTheory.Measure β} (hg : MeasureTheory.Memℒp g p ν) (hf : MeasureTheory.MeasurePreserving f μ ν) : MeasureTheory.Memℒp (g ∘ f) p μ

theorem MeasurableEmbedding.eLpNormEssSup_map_measure {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {β : Type u_6} {mβ : MeasurableSpace β} {f : α → β} {g : β → F} (hf : MeasurableEmbedding f) : MeasureTheory.eLpNormEssSup g (MeasureTheory.Measure.map f μ) = MeasureTheory.eLpNormEssSup (g ∘ f) μ

theorem MeasurableEmbedding.eLpNorm_map_measure {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {β : Type u_6} {mβ : MeasurableSpace β} {f : α → β} {g : β → F} (hf : MeasurableEmbedding f) : MeasureTheory.eLpNorm g p (MeasureTheory.Measure.map f μ) = MeasureTheory.eLpNorm (g ∘ f) p μ

theorem MeasurableEmbedding.memℒp_map_measure_iff {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {β : Type u_6} {mβ : MeasurableSpace β} {f : α → β} {g : β → F} (hf : MeasurableEmbedding f) : MeasureTheory.Memℒp g p (MeasureTheory.Measure.map f μ) ↔ MeasureTheory.Memℒp (g ∘ f) p μ

theorem MeasurableEquiv.memℒp_map_measure_iff {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {β : Type u_6} {mβ : MeasurableSpace β} (f : α ≃ᵐ β) {g : β → F} : MeasureTheory.Memℒp g p (MeasureTheory.Measure.map (⇑f) μ) ↔ MeasureTheory.Memℒp (g ∘ ⇑f) p μ

theorem MeasureTheory.eLpNorm'_le_nnreal_smul_eLpNorm'_of_ae_le_mul {α : Type u_1} {F : Type u_4} {G : Type u_5} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] [NormedAddCommGroup G] {f : α → F} {g : α → G} {c : NNReal} (h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊) {p : ℝ} (hp : 0 < p) : MeasureTheory.eLpNorm' f p μ ≤ c • MeasureTheory.eLpNorm' g p μ

theorem MeasureTheory.eLpNormEssSup_le_nnreal_smul_eLpNormEssSup_of_ae_le_mul {α : Type u_1} {F : Type u_4} {G : Type u_5} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] [NormedAddCommGroup G] {f : α → F} {g : α → G} {c : NNReal} (h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊) : MeasureTheory.eLpNormEssSup f μ ≤ c • MeasureTheory.eLpNormEssSup g μ

theorem MeasureTheory.eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul {α : Type u_1} {F : Type u_4} {G : Type u_5} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] [NormedAddCommGroup G] {f : α → F} {g : α → G} {c : NNReal} (h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊) (p : ENNReal) : MeasureTheory.eLpNorm f p μ ≤ c • MeasureTheory.eLpNorm g p μ

theorem MeasureTheory.eLpNorm_eq_zero_and_zero_of_ae_le_mul_neg {α : Type u_1} {F : Type u_4} {G : Type u_5} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] [NormedAddCommGroup G] {f : α → F} {g : α → G} {c : ℝ} (h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c * ‖g x‖) (hc : c < 0) (p : ENNReal) : MeasureTheory.eLpNorm f p μ = 0 ∧ MeasureTheory.eLpNorm g p μ = 0

When c is negative, ‖f x‖ ≤ c * ‖g x‖ is nonsense and forces both f and g to have an eLpNorm of 0.

theorem MeasureTheory.eLpNorm_le_mul_eLpNorm_of_ae_le_mul {α : Type u_1} {F : Type u_4} {G : Type u_5} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] [NormedAddCommGroup G] {f : α → F} {g : α → G} {c : ℝ} (h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c * ‖g x‖) (p : ENNReal) : MeasureTheory.eLpNorm f p μ ≤ ENNReal.ofReal c * MeasureTheory.eLpNorm g p μ

theorem MeasureTheory.Memℒp.of_nnnorm_le_mul {α : Type u_1} {E : Type u_3} {F : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] {f : α → E} {g : α → F} {c : NNReal} (hg : MeasureTheory.Memℒp g p μ) (hf : MeasureTheory.AEStronglyMeasurable f μ) (hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊) : MeasureTheory.Memℒp f p μ

theorem MeasureTheory.Memℒp.of_le_mul {α : Type u_1} {E : Type u_3} {F : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] {f : α → E} {g : α → F} {c : ℝ} (hg : MeasureTheory.Memℒp g p μ) (hf : MeasureTheory.AEStronglyMeasurable f μ) (hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c * ‖g x‖) : MeasureTheory.Memℒp f p μ

Bounded actions by normed rings

In this section we show inequalities on the norm.

theorem MeasureTheory.eLpNorm'_const_smul_le {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {q : ℝ} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {𝕜 : Type u_6} [NormedRing 𝕜] [MulActionWithZero 𝕜 F] [BoundedSMul 𝕜 F] {c : 𝕜} {f : α → F} (hq : 0 < q) : MeasureTheory.eLpNorm' (c • f) q μ ≤ ‖c‖ₑ * MeasureTheory.eLpNorm' f q μ

theorem MeasureTheory.eLpNormEssSup_const_smul_le {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {𝕜 : Type u_6} [NormedRing 𝕜] [MulActionWithZero 𝕜 F] [BoundedSMul 𝕜 F] {c : 𝕜} {f : α → F} : MeasureTheory.eLpNormEssSup (c • f) μ ≤ ‖c‖ₑ * MeasureTheory.eLpNormEssSup f μ

theorem MeasureTheory.eLpNorm_const_smul_le {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {𝕜 : Type u_6} [NormedRing 𝕜] [MulActionWithZero 𝕜 F] [BoundedSMul 𝕜 F] {c : 𝕜} {f : α → F} : MeasureTheory.eLpNorm (c • f) p μ ≤ ‖c‖ₑ * MeasureTheory.eLpNorm f p μ

theorem MeasureTheory.Memℒp.const_smul {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {𝕜 : Type u_6} [NormedRing 𝕜] [MulActionWithZero 𝕜 F] [BoundedSMul 𝕜 F] {f : α → F} (hf : MeasureTheory.Memℒp f p μ) (c : 𝕜) : MeasureTheory.Memℒp (c • f) p μ

theorem MeasureTheory.Memℒp.const_mul {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {𝕜 : Type u_6} [NormedRing 𝕜] {f : α → 𝕜} (hf : MeasureTheory.Memℒp f p μ) (c : 𝕜) : MeasureTheory.Memℒp (fun (x : α) => c * f x) p μ

Bounded actions by normed division rings

The inequalities in the previous section are now tight.

theorem MeasureTheory.eLpNorm'_const_smul {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {q : ℝ} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {𝕜 : Type u_6} [NormedDivisionRing 𝕜] [Module 𝕜 F] [BoundedSMul 𝕜 F] {f : α → F} (c : 𝕜) (hq_pos : 0 < q) : MeasureTheory.eLpNorm' (c • f) q μ = ‖c‖ₑ * MeasureTheory.eLpNorm' f q μ

theorem MeasureTheory.eLpNormEssSup_const_smul {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {𝕜 : Type u_6} [NormedDivisionRing 𝕜] [Module 𝕜 F] [BoundedSMul 𝕜 F] (c : 𝕜) (f : α → F) : MeasureTheory.eLpNormEssSup (c • f) μ = ‖c‖ₑ * MeasureTheory.eLpNormEssSup f μ

theorem MeasureTheory.eLpNorm_const_smul {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} [NormedAddCommGroup F] {𝕜 : Type u_6} [NormedDivisionRing 𝕜] [Module 𝕜 F] [BoundedSMul 𝕜 F] (c : 𝕜) (f : α → F) (p : ENNReal) (μ : MeasureTheory.Measure α) : MeasureTheory.eLpNorm (c • f) p μ = ‖c‖ₑ * MeasureTheory.eLpNorm f p μ

theorem MeasureTheory.eLpNorm_nsmul {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] [NormedSpace ℝ F] (n : ℕ) (f : α → F) : MeasureTheory.eLpNorm (n • f) p μ = ↑n * MeasureTheory.eLpNorm f p μ

theorem MeasureTheory.le_eLpNorm_of_bddBelow {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] (hp : p ≠ 0) (hp' : p ≠ ⊤) {f : α → F} (C : NNReal) {s : Set α} (hs : MeasurableSet s) (hf : ∀ᵐ (x : α) ∂μ, x ∈ s → C ≤ ‖f x‖₊) : C • μ s ^ (1 / p.toReal) ≤ MeasureTheory.eLpNorm f p μ

@[simp]

theorem MeasureTheory.eLpNorm_conj {α : Type u_1} {m0 : MeasurableSpace α} {𝕜 : Type u_6} [RCLike 𝕜] (f : α → 𝕜) (p : ENNReal) (μ : MeasureTheory.Measure α) : MeasureTheory.eLpNorm ((starRingEnd (α → 𝕜)) f) p μ = MeasureTheory.eLpNorm f p μ

theorem MeasureTheory.Memℒp.re {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {𝕜 : Type u_6} [RCLike 𝕜] {f : α → 𝕜} (hf : MeasureTheory.Memℒp f p μ) : MeasureTheory.Memℒp (fun (x : α) => RCLike.re (f x)) p μ

theorem MeasureTheory.Memℒp.im {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {𝕜 : Type u_6} [RCLike 𝕜] {f : α → 𝕜} (hf : MeasureTheory.Memℒp f p μ) : MeasureTheory.Memℒp (fun (x : α) => RCLike.im (f x)) p μ

theorem MeasureTheory.ae_bdd_liminf_atTop_rpow_of_eLpNorm_bdd {α : Type u_1} {E : Type u_3} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [MeasurableSpace E] [OpensMeasurableSpace E] {R : NNReal} {p : ENNReal} {f : ℕ → α → E} (hfmeas : ∀ (n : ℕ), Measurable (f n)) (hbdd : ∀ (n : ℕ), MeasureTheory.eLpNorm (f n) p μ ≤ ↑R) : ∀ᵐ (x : α) ∂μ, Filter.liminf (fun (n : ℕ) => ‖f n x‖ₑ ^ p.toReal) Filter.atTop < ⊤

theorem MeasureTheory.ae_bdd_liminf_atTop_of_eLpNorm_bdd {α : Type u_1} {E : Type u_3} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [MeasurableSpace E] [OpensMeasurableSpace E] {R : NNReal} {p : ENNReal} (hp : p ≠ 0) {f : ℕ → α → E} (hfmeas : ∀ (n : ℕ), Measurable (f n)) (hbdd : ∀ (n : ℕ), MeasureTheory.eLpNorm (f n) p μ ≤ ↑R) : ∀ᵐ (x : α) ∂μ, Filter.liminf (fun (n : ℕ) => ‖f n x‖ₑ) Filter.atTop < ⊤

theorem Continuous.memℒp_top_of_hasCompactSupport {E : Type u_3} [NormedAddCommGroup E] {X : Type u_6} [TopologicalSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] {f : X → E} (hf : Continuous f) (h'f : HasCompactSupport f) (μ : MeasureTheory.Measure X) : MeasureTheory.Memℒp f ⊤ μ

A continuous function with compact support belongs to L^∞. See Continuous.memℒp_of_hasCompactSupport for a version for L^p.

theorem MeasureTheory.Memℒp.exists_eLpNorm_indicator_compl_lt {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {β : Type u_6} [NormedAddCommGroup β] (hp_top : p ≠ ⊤) {f : α → β} (hf : MeasureTheory.Memℒp f p μ) {ε : ENNReal} (hε : ε ≠ 0) : ∃ (s : Set α), MeasurableSet s ∧ μ s < ⊤ ∧ MeasureTheory.eLpNorm (sᶜ.indicator f) p μ < ε

A single function that is Memℒp f p μ is tight with respect to μ.