ℒ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} {F : Type u_3} [NormedAddCommGroup F] {x✝ : MeasurableSpace α} (f : α → 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)

def MeasureTheory.eLpNormEssSup {α : Type u_1} {F : Type u_3} [NormedAddCommGroup F] {x✝ : MeasurableSpace α} (f : α → F) (μ : MeasureTheory.Measure α) : ENNReal

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

Equations

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

def MeasureTheory.eLpNorm {α : Type u_1} {F : Type u_3} [NormedAddCommGroup F] {x✝ : MeasurableSpace α} (f : α → 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 μ

@[deprecated MeasureTheory.eLpNorm]

def MeasureTheory.snorm {α : Type u_1} {F : Type u_3} [NormedAddCommGroup F] {x✝ : MeasurableSpace α} (f : α → F) (p : ENNReal) (μ : MeasureTheory.Measure α := by volume_tac) : ENNReal

Alias of MeasureTheory.eLpNorm.

---

ℒ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.snorm = @MeasureTheory.eLpNorm

theorem MeasureTheory.eLpNorm_eq_eLpNorm' {α : Type u_1} {F : Type u_3} {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 μ

@[deprecated MeasureTheory.eLpNorm_eq_eLpNorm']

theorem MeasureTheory.snorm_eq_snorm' {α : Type u_1} {F : Type u_3} {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 μ

Alias of MeasureTheory.eLpNorm_eq_eLpNorm'.

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

@[deprecated MeasureTheory.eLpNorm_nnreal_eq_eLpNorm']

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

Alias of MeasureTheory.eLpNorm_nnreal_eq_eLpNorm'.

theorem MeasureTheory.eLpNorm_eq_lintegral_rpow_nnnorm {α : Type u_1} {F : Type u_3} {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_nnnorm]

theorem MeasureTheory.snorm_eq_lintegral_rpow_nnnorm {α : Type u_1} {F : Type u_3} {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_nnnorm.

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

@[deprecated MeasureTheory.eLpNorm_nnreal_eq_lintegral]

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

Alias of MeasureTheory.eLpNorm_nnreal_eq_lintegral.

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

@[deprecated MeasureTheory.eLpNorm_one_eq_lintegral_nnnorm]

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

Alias of MeasureTheory.eLpNorm_one_eq_lintegral_nnnorm.

@[simp]

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

@[deprecated MeasureTheory.eLpNorm_exponent_top]

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

Alias of MeasureTheory.eLpNorm_exponent_top.

def MeasureTheory.Memℒp {E : Type u_2} [NormedAddCommGroup E] {α : Type u_5} {x✝ : MeasurableSpace α} (f : α → E) (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_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {f : α → E} {p : ENNReal} (h : MeasureTheory.Memℒp f p μ) : MeasureTheory.AEStronglyMeasurable f μ

theorem MeasureTheory.lintegral_rpow_nnnorm_eq_rpow_eLpNorm' {α : Type u_1} {F : Type u_3} {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_nnnorm_eq_rpow_eLpNorm']

theorem MeasureTheory.lintegral_rpow_nnnorm_eq_rpow_snorm' {α : Type u_1} {F : Type u_3} {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_nnnorm_eq_rpow_eLpNorm'.

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

@[deprecated MeasureTheory.eLpNorm_nnreal_pow_eq_lintegral]

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

Alias of MeasureTheory.eLpNorm_nnreal_pow_eq_lintegral.

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

@[deprecated MeasureTheory.Memℒp.eLpNorm_lt_top]

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

Alias of MeasureTheory.Memℒp.eLpNorm_lt_top.

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

@[deprecated MeasureTheory.Memℒp.eLpNorm_ne_top]

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

Alias of MeasureTheory.Memℒp.eLpNorm_ne_top.

theorem MeasureTheory.lintegral_rpow_nnnorm_lt_top_of_eLpNorm'_lt_top {α : Type u_1} {F : Type u_3} {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_nnnorm_lt_top_of_eLpNorm'_lt_top]

theorem MeasureTheory.lintegral_rpow_nnnorm_lt_top_of_snorm'_lt_top {α : Type u_1} {F : Type u_3} {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_nnnorm_lt_top_of_eLpNorm'_lt_top.

theorem MeasureTheory.lintegral_rpow_nnnorm_lt_top_of_eLpNorm_lt_top {α : Type u_1} {F : Type u_3} {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_nnnorm_lt_top_of_eLpNorm_lt_top]

theorem MeasureTheory.lintegral_rpow_nnnorm_lt_top_of_snorm_lt_top {α : Type u_1} {F : Type u_3} {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_nnnorm_lt_top_of_eLpNorm_lt_top.

theorem MeasureTheory.eLpNorm_lt_top_iff_lintegral_rpow_nnnorm_lt_top {α : Type u_1} {F : Type u_3} {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 ∂μ < ⊤

@[deprecated MeasureTheory.eLpNorm_lt_top_iff_lintegral_rpow_nnnorm_lt_top]

theorem MeasureTheory.snorm_lt_top_iff_lintegral_rpow_nnnorm_lt_top {α : Type u_1} {F : Type u_3} {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 ∂μ < ⊤

Alias of MeasureTheory.eLpNorm_lt_top_iff_lintegral_rpow_nnnorm_lt_top.

@[simp]

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

@[deprecated MeasureTheory.eLpNorm'_exponent_zero]

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

Alias of MeasureTheory.eLpNorm'_exponent_zero.

@[simp]

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

@[deprecated MeasureTheory.eLpNorm_exponent_zero]

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

Alias of MeasureTheory.eLpNorm_exponent_zero.

@[simp]

theorem MeasureTheory.memℒp_zero_iff_aestronglyMeasurable {α : Type u_1} {E : Type u_2} {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_3} {m0 : MeasurableSpace α} {q : ℝ} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] (hp0_lt : 0 < q) : MeasureTheory.eLpNorm' 0 q μ = 0

@[deprecated MeasureTheory.eLpNorm'_zero]

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

Alias of MeasureTheory.eLpNorm'_zero.

@[simp]

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

@[deprecated MeasureTheory.eLpNorm'_zero']

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

Alias of MeasureTheory.eLpNorm'_zero'.

@[simp]

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

@[deprecated MeasureTheory.eLpNormEssSup_zero]

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

Alias of MeasureTheory.eLpNormEssSup_zero.

@[simp]

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

@[deprecated MeasureTheory.eLpNorm_zero]

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

Alias of MeasureTheory.eLpNorm_zero.

@[simp]

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

@[deprecated MeasureTheory.eLpNorm_zero']

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

Alias of MeasureTheory.eLpNorm_zero'.

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

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

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

@[deprecated MeasureTheory.eLpNorm'_measure_zero_of_pos]

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

Alias of MeasureTheory.eLpNorm'_measure_zero_of_pos.

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

@[deprecated MeasureTheory.eLpNorm'_measure_zero_of_exponent_zero]

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

Alias of MeasureTheory.eLpNorm'_measure_zero_of_exponent_zero.

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

@[deprecated MeasureTheory.eLpNorm'_measure_zero_of_neg]

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

Alias of MeasureTheory.eLpNorm'_measure_zero_of_neg.

@[simp]

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

@[deprecated MeasureTheory.eLpNormEssSup_measure_zero]

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

Alias of MeasureTheory.eLpNormEssSup_measure_zero.

@[simp]

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

@[deprecated MeasureTheory.eLpNorm_measure_zero]

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

Alias of MeasureTheory.eLpNorm_measure_zero.

@[simp]

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

@[deprecated MeasureTheory.eLpNorm'_neg]

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

Alias of MeasureTheory.eLpNorm'_neg.

@[simp]

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

@[deprecated MeasureTheory.eLpNorm_neg]

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

Alias of MeasureTheory.eLpNorm_neg.

theorem MeasureTheory.Memℒp.neg {α : Type u_1} {E : Type u_2} {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_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {f : α → E} : MeasureTheory.Memℒp (-f) p μ ↔ MeasureTheory.Memℒp f p μ

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

@[deprecated MeasureTheory.eLpNorm_indicator_eq_restrict]

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

Alias of MeasureTheory.eLpNorm_indicator_eq_restrict.

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

@[deprecated MeasureTheory.eLpNorm'_const]

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

Alias of MeasureTheory.eLpNorm'_const.

theorem MeasureTheory.eLpNorm'_const' {α : Type u_1} {F : Type u_3} {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)

@[deprecated MeasureTheory.eLpNorm'_const']

theorem MeasureTheory.snorm'_const' {α : Type u_1} {F : Type u_3} {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)

Alias of MeasureTheory.eLpNorm'_const'.

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

@[deprecated MeasureTheory.eLpNormEssSup_const]

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

Alias of MeasureTheory.eLpNormEssSup_const.

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

@[deprecated MeasureTheory.eLpNorm'_const_of_isProbabilityMeasure]

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

Alias of MeasureTheory.eLpNorm'_const_of_isProbabilityMeasure.

theorem MeasureTheory.eLpNorm_const {α : Type u_1} {F : Type u_3} {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)

@[deprecated MeasureTheory.eLpNorm_const]

theorem MeasureTheory.snorm_const {α : Type u_1} {F : Type u_3} {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)

Alias of MeasureTheory.eLpNorm_const.

theorem MeasureTheory.eLpNorm_const' {α : Type u_1} {F : Type u_3} {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)

@[deprecated MeasureTheory.eLpNorm_const']

theorem MeasureTheory.snorm_const' {α : Type u_1} {F : Type u_3} {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)

Alias of MeasureTheory.eLpNorm_const'.

theorem MeasureTheory.eLpNorm_const_lt_top_iff {α : Type u_1} {F : Type u_3} {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 < ⊤

@[deprecated MeasureTheory.eLpNorm_const_lt_top_iff]

theorem MeasureTheory.snorm_const_lt_top_iff {α : Type u_1} {F : Type u_3} {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 < ⊤

Alias of MeasureTheory.eLpNorm_const_lt_top_iff.

theorem MeasureTheory.memℒp_const {α : Type u_1} {E : Type u_2} {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_2} {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_2} {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_3} {G : Type u_4} {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 μ

@[deprecated MeasureTheory.eLpNorm'_mono_nnnorm_ae]

theorem MeasureTheory.snorm'_mono_nnnorm_ae {α : Type u_1} {F : Type u_3} {G : Type u_4} {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 μ

Alias of MeasureTheory.eLpNorm'_mono_nnnorm_ae.

theorem MeasureTheory.eLpNorm'_mono_ae {α : Type u_1} {F : Type u_3} {G : Type u_4} {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 μ

@[deprecated MeasureTheory.eLpNorm'_mono_ae]

theorem MeasureTheory.snorm'_mono_ae {α : Type u_1} {F : Type u_3} {G : Type u_4} {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 μ

Alias of MeasureTheory.eLpNorm'_mono_ae.

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

@[deprecated MeasureTheory.eLpNorm'_congr_nnnorm_ae]

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

Alias of MeasureTheory.eLpNorm'_congr_nnnorm_ae.

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

@[deprecated MeasureTheory.eLpNorm'_congr_norm_ae]

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

Alias of MeasureTheory.eLpNorm'_congr_norm_ae.

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

@[deprecated MeasureTheory.eLpNorm'_congr_ae]

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

Alias of MeasureTheory.eLpNorm'_congr_ae.

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

@[deprecated MeasureTheory.eLpNormEssSup_congr_ae]

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

Alias of MeasureTheory.eLpNormEssSup_congr_ae.

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

@[deprecated MeasureTheory.eLpNormEssSup_mono_nnnorm_ae]

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

Alias of MeasureTheory.eLpNormEssSup_mono_nnnorm_ae.

theorem MeasureTheory.eLpNorm_mono_nnnorm_ae {α : Type u_1} {F : Type u_3} {G : Type u_4} {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 μ

@[deprecated MeasureTheory.eLpNorm_mono_nnnorm_ae]

theorem MeasureTheory.snorm_mono_nnnorm_ae {α : Type u_1} {F : Type u_3} {G : Type u_4} {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 μ

Alias of MeasureTheory.eLpNorm_mono_nnnorm_ae.

theorem MeasureTheory.eLpNorm_mono_ae {α : Type u_1} {F : Type u_3} {G : Type u_4} {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 μ

@[deprecated MeasureTheory.eLpNorm_mono_ae]

theorem MeasureTheory.snorm_mono_ae {α : Type u_1} {F : Type u_3} {G : Type u_4} {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 μ

Alias of MeasureTheory.eLpNorm_mono_ae.

theorem MeasureTheory.eLpNorm_mono_ae_real {α : Type u_1} {F : Type u_3} {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 μ

@[deprecated MeasureTheory.eLpNorm_mono_ae_real]

theorem MeasureTheory.snorm_mono_ae_real {α : Type u_1} {F : Type u_3} {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 μ

Alias of MeasureTheory.eLpNorm_mono_ae_real.

theorem MeasureTheory.eLpNorm_mono_nnnorm {α : Type u_1} {F : Type u_3} {G : Type u_4} {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 μ

@[deprecated MeasureTheory.eLpNorm_mono_nnnorm]

theorem MeasureTheory.snorm_mono_nnnorm {α : Type u_1} {F : Type u_3} {G : Type u_4} {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 μ

Alias of MeasureTheory.eLpNorm_mono_nnnorm.

theorem MeasureTheory.eLpNorm_mono {α : Type u_1} {F : Type u_3} {G : Type u_4} {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 μ

@[deprecated MeasureTheory.eLpNorm_mono]

theorem MeasureTheory.snorm_mono {α : Type u_1} {F : Type u_3} {G : Type u_4} {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 μ

Alias of MeasureTheory.eLpNorm_mono.

theorem MeasureTheory.eLpNorm_mono_real {α : Type u_1} {F : Type u_3} {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 μ

@[deprecated MeasureTheory.eLpNorm_mono_real]

theorem MeasureTheory.snorm_mono_real {α : Type u_1} {F : Type u_3} {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 μ

Alias of MeasureTheory.eLpNorm_mono_real.

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

@[deprecated MeasureTheory.eLpNormEssSup_le_of_ae_nnnorm_bound]

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

Alias of MeasureTheory.eLpNormEssSup_le_of_ae_nnnorm_bound.

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

@[deprecated MeasureTheory.eLpNormEssSup_le_of_ae_bound]

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

Alias of MeasureTheory.eLpNormEssSup_le_of_ae_bound.

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

@[deprecated MeasureTheory.eLpNormEssSup_lt_top_of_ae_nnnorm_bound]

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

Alias of MeasureTheory.eLpNormEssSup_lt_top_of_ae_nnnorm_bound.

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

@[deprecated MeasureTheory.eLpNormEssSup_lt_top_of_ae_bound]

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

Alias of MeasureTheory.eLpNormEssSup_lt_top_of_ae_bound.

theorem MeasureTheory.eLpNorm_le_of_ae_nnnorm_bound {α : Type u_1} {F : Type u_3} {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⁻¹

@[deprecated MeasureTheory.eLpNorm_le_of_ae_nnnorm_bound]

theorem MeasureTheory.snorm_le_of_ae_nnnorm_bound {α : Type u_1} {F : Type u_3} {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⁻¹

Alias of MeasureTheory.eLpNorm_le_of_ae_nnnorm_bound.

theorem MeasureTheory.eLpNorm_le_of_ae_bound {α : Type u_1} {F : Type u_3} {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

@[deprecated MeasureTheory.eLpNorm_le_of_ae_bound]

theorem MeasureTheory.snorm_le_of_ae_bound {α : Type u_1} {F : Type u_3} {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

Alias of MeasureTheory.eLpNorm_le_of_ae_bound.

theorem MeasureTheory.eLpNorm_congr_nnnorm_ae {α : Type u_1} {F : Type u_3} {G : Type u_4} {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 μ

@[deprecated MeasureTheory.eLpNorm_congr_nnnorm_ae]

theorem MeasureTheory.snorm_congr_nnnorm_ae {α : Type u_1} {F : Type u_3} {G : Type u_4} {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 μ

Alias of MeasureTheory.eLpNorm_congr_nnnorm_ae.

theorem MeasureTheory.eLpNorm_congr_norm_ae {α : Type u_1} {F : Type u_3} {G : Type u_4} {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 μ

@[deprecated MeasureTheory.eLpNorm_congr_norm_ae]

theorem MeasureTheory.snorm_congr_norm_ae {α : Type u_1} {F : Type u_3} {G : Type u_4} {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 μ

Alias of MeasureTheory.eLpNorm_congr_norm_ae.

theorem MeasureTheory.eLpNorm_indicator_sub_indicator {α : Type u_1} {E : Type u_2} {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 μ

@[deprecated MeasureTheory.eLpNorm_indicator_sub_indicator]

theorem MeasureTheory.snorm_indicator_sub_indicator {α : Type u_1} {E : Type u_2} {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 μ

Alias of MeasureTheory.eLpNorm_indicator_sub_indicator.

@[simp]

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

@[deprecated MeasureTheory.eLpNorm'_norm]

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

Alias of MeasureTheory.eLpNorm'_norm.

@[simp]

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

@[deprecated MeasureTheory.eLpNorm_norm]

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

Alias of MeasureTheory.eLpNorm_norm.

theorem MeasureTheory.eLpNorm'_norm_rpow {α : Type u_1} {F : Type u_3} {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

@[deprecated MeasureTheory.eLpNorm'_norm_rpow]

theorem MeasureTheory.snorm'_norm_rpow {α : Type u_1} {F : Type u_3} {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

Alias of MeasureTheory.eLpNorm'_norm_rpow.

theorem MeasureTheory.eLpNorm_norm_rpow {α : Type u_1} {F : Type u_3} {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

@[deprecated MeasureTheory.eLpNorm_norm_rpow]

theorem MeasureTheory.snorm_norm_rpow {α : Type u_1} {F : Type u_3} {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

Alias of MeasureTheory.eLpNorm_norm_rpow.

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

@[deprecated MeasureTheory.eLpNorm_congr_ae]

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

Alias of MeasureTheory.eLpNorm_congr_ae.

theorem MeasureTheory.memℒp_congr_ae {α : Type u_1} {E : Type u_2} {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_2} {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_2} {F : Type u_3} {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_2} {F : Type u_3} {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_2} {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_2} {F : Type u_3} {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_2} {F : Type u_3} {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_2} {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_2} {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_3} {m0 : MeasurableSpace α} {q : ℝ} {μ ν : MeasureTheory.Measure α} [NormedAddCommGroup F] (f : α → F) (hμν : ν ≤ μ) (hq : 0 ≤ q) : MeasureTheory.eLpNorm' f q ν ≤ MeasureTheory.eLpNorm' f q μ

@[deprecated MeasureTheory.eLpNorm'_mono_measure]

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

Alias of MeasureTheory.eLpNorm'_mono_measure.

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

@[deprecated MeasureTheory.eLpNormEssSup_mono_measure]

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

Alias of MeasureTheory.eLpNormEssSup_mono_measure.

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

@[deprecated MeasureTheory.eLpNorm_mono_measure]

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

Alias of MeasureTheory.eLpNorm_mono_measure.

theorem MeasureTheory.Memℒp.mono_measure {α : Type u_1} {E : Type u_2} {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_restrict_le {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} [NormedAddCommGroup F] (f : α → F) (p : ENNReal) (μ : MeasureTheory.Measure α) (s : Set α) : MeasureTheory.eLpNorm f p (μ.restrict s) ≤ MeasureTheory.eLpNorm f p μ

@[deprecated MeasureTheory.eLpNorm_restrict_le]

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

Alias of MeasureTheory.eLpNorm_restrict_le.

theorem MeasureTheory.eLpNorm_restrict_eq_of_support_subset {α : Type u_1} {F : Type u_3} {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.

@[deprecated MeasureTheory.eLpNorm_restrict_eq_of_support_subset]

theorem MeasureTheory.snorm_restrict_eq_of_support_subset {α : Type u_1} {F : Type u_3} {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 μ

Alias of MeasureTheory.eLpNorm_restrict_eq_of_support_subset.

---

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_2} {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_3} {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 μ

@[deprecated MeasureTheory.eLpNorm'_smul_measure]

theorem MeasureTheory.snorm'_smul_measure {α : Type u_1} {F : Type u_3} {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 μ

Alias of MeasureTheory.eLpNorm'_smul_measure.

@[simp]

theorem MeasureTheory.eLpNormEssSup_smul_measure {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {R : Type u_5} [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 μ

@[deprecated MeasureTheory.eLpNormEssSup_smul_measure]

theorem MeasureTheory.snormEssSup_smul_measure {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {R : Type u_5} [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 μ

Alias of MeasureTheory.eLpNormEssSup_smul_measure.

@[deprecated _private.Mathlib.MeasureTheory.Function.LpSeminorm.Basic.0.MeasureTheory.eLpNorm_smul_measure_of_ne_zero_of_ne_top]

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

Alias of _private.Mathlib.MeasureTheory.Function.LpSeminorm.Basic.0.MeasureTheory.eLpNorm_smul_measure_of_ne_zero_of_ne_top.

---

Use eLpNorm_smul_measure_of_ne_top instead.

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

@[deprecated MeasureTheory.eLpNorm_smul_measure_of_ne_zero]

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

Alias of MeasureTheory.eLpNorm_smul_measure_of_ne_zero.

theorem MeasureTheory.eLpNorm_smul_measure_of_ne_top {α : Type u_1} {F : Type u_3} {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 μ

@[deprecated MeasureTheory.eLpNorm_smul_measure_of_ne_top]

theorem MeasureTheory.snorm_smul_measure_of_ne_top {α : Type u_1} {F : Type u_3} {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 μ

Alias of MeasureTheory.eLpNorm_smul_measure_of_ne_top.

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

@[deprecated MeasureTheory.eLpNorm_one_smul_measure]

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

Alias of MeasureTheory.eLpNorm_one_smul_measure.

theorem MeasureTheory.Memℒp.of_measure_le_smul {α : Type u_1} {E : Type u_2} {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_2} {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_3} {m0 : MeasurableSpace α} [NormedAddCommGroup F] (f : α → F) (μ ν : MeasureTheory.Measure α) : MeasureTheory.eLpNorm f 1 (μ + ν) = MeasureTheory.eLpNorm f 1 μ + MeasureTheory.eLpNorm f 1 ν

@[deprecated MeasureTheory.eLpNorm_one_add_measure]

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

Alias of MeasureTheory.eLpNorm_one_add_measure.

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

@[deprecated MeasureTheory.eLpNorm_le_add_measure_right]

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

Alias of MeasureTheory.eLpNorm_le_add_measure_right.

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

@[deprecated MeasureTheory.eLpNorm_le_add_measure_left]

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

Alias of MeasureTheory.eLpNorm_le_add_measure_left.

theorem MeasureTheory.eLpNormEssSup_eq_iSup {α : Type u_1} {E : Type u_2} {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_2} {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_2} {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_2} {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_2} {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_2} {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_3} {m0 : MeasurableSpace α} {q : ℝ} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : α → F} (hq0_lt : 0 < q) (hf_zero : f =ᵐ[μ] 0) : MeasureTheory.eLpNorm' f q μ = 0

@[deprecated MeasureTheory.eLpNorm'_eq_zero_of_ae_zero]

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

Alias of MeasureTheory.eLpNorm'_eq_zero_of_ae_zero.

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

@[deprecated MeasureTheory.eLpNorm'_eq_zero_of_ae_zero']

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

Alias of MeasureTheory.eLpNorm'_eq_zero_of_ae_zero'.

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

@[deprecated MeasureTheory.ae_eq_zero_of_eLpNorm'_eq_zero]

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

Alias of MeasureTheory.ae_eq_zero_of_eLpNorm'_eq_zero.

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

@[deprecated MeasureTheory.eLpNorm'_eq_zero_iff]

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

Alias of MeasureTheory.eLpNorm'_eq_zero_iff.

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

@[deprecated MeasureTheory.coe_nnnorm_ae_le_eLpNormEssSup]

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

Alias of MeasureTheory.coe_nnnorm_ae_le_eLpNormEssSup.

@[simp]

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

@[deprecated MeasureTheory.eLpNormEssSup_eq_zero_iff]

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

Alias of MeasureTheory.eLpNormEssSup_eq_zero_iff.

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

@[deprecated MeasureTheory.eLpNorm_eq_zero_iff]

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

Alias of MeasureTheory.eLpNorm_eq_zero_iff.

theorem MeasureTheory.eLpNorm_eq_zero_of_ae_zero {α : Type u_1} {E : Type u_2} {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_3} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : α → F} : ∀ᵐ (y : α) ∂μ, ↑‖f y‖₊ ≤ MeasureTheory.eLpNormEssSup f μ

@[deprecated MeasureTheory.ae_le_eLpNormEssSup]

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

Alias of MeasureTheory.ae_le_eLpNormEssSup.

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

@[deprecated MeasureTheory.meas_eLpNormEssSup_lt]

theorem MeasureTheory.meas_snormEssSup_lt {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : α → F} : μ {y : α | MeasureTheory.eLpNormEssSup f μ < ↑‖f y‖₊} = 0

Alias of MeasureTheory.meas_eLpNormEssSup_lt.

theorem MeasureTheory.eLpNormEssSup_piecewise {α : Type u_1} {E : Type u_2} {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ᶜ)

@[deprecated MeasureTheory.eLpNormEssSup_piecewise]

theorem MeasureTheory.snormEssSup_piecewise {α : Type u_1} {E : Type u_2} {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ᶜ)

Alias of MeasureTheory.eLpNormEssSup_piecewise.

theorem MeasureTheory.eLpNorm_top_piecewise {α : Type u_1} {E : Type u_2} {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ᶜ)

@[deprecated MeasureTheory.eLpNorm_top_piecewise]

theorem MeasureTheory.snorm_top_piecewise {α : Type u_1} {E : Type u_2} {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ᶜ)

Alias of MeasureTheory.eLpNorm_top_piecewise.

theorem MeasureTheory.eLpNormEssSup_map_measure {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {β : Type u_5} {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) μ

@[deprecated MeasureTheory.eLpNormEssSup_map_measure]

theorem MeasureTheory.snormEssSup_map_measure {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {β : Type u_5} {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) μ

Alias of MeasureTheory.eLpNormEssSup_map_measure.

theorem MeasureTheory.eLpNorm_map_measure {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {β : Type u_5} {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 μ

@[deprecated MeasureTheory.eLpNorm_map_measure]

theorem MeasureTheory.snorm_map_measure {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {β : Type u_5} {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 μ

Alias of MeasureTheory.eLpNorm_map_measure.

theorem MeasureTheory.memℒp_map_measure_iff {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {β : Type u_5} {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_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {β : Type u_5} {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_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {β : Type u_5} {mβ : MeasurableSpace β} {f : α → β} {g : β → E} {ν : MeasureTheory.Measure β} (hg : MeasureTheory.AEStronglyMeasurable g ν) (hf : MeasureTheory.MeasurePreserving f μ ν) : MeasureTheory.eLpNorm (g ∘ f) p μ = MeasureTheory.eLpNorm g p ν

@[deprecated MeasureTheory.eLpNorm_comp_measurePreserving]

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

Alias of MeasureTheory.eLpNorm_comp_measurePreserving.

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

@[deprecated MeasureTheory.AEEqFun.eLpNorm_compMeasurePreserving]

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

Alias of MeasureTheory.AEEqFun.eLpNorm_compMeasurePreserving.

theorem MeasureTheory.Memℒp.comp_measurePreserving {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {β : Type u_5} {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_3} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {β : Type u_5} {mβ : MeasurableSpace β} {f : α → β} {g : β → F} (hf : MeasurableEmbedding f) : MeasureTheory.eLpNormEssSup g (MeasureTheory.Measure.map f μ) = MeasureTheory.eLpNormEssSup (g ∘ f) μ

@[deprecated MeasurableEmbedding.eLpNormEssSup_map_measure]

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

Alias of MeasurableEmbedding.eLpNormEssSup_map_measure.

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

@[deprecated MeasurableEmbedding.eLpNorm_map_measure]

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

Alias of MeasurableEmbedding.eLpNorm_map_measure.

theorem MeasurableEmbedding.memℒp_map_measure_iff {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {β : Type u_5} {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_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {β : Type u_5} {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_3} {G : Type u_4} {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 μ

@[deprecated MeasureTheory.eLpNorm'_le_nnreal_smul_eLpNorm'_of_ae_le_mul]

theorem MeasureTheory.snorm'_le_nnreal_smul_snorm'_of_ae_le_mul {α : Type u_1} {F : Type u_3} {G : Type u_4} {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 μ

Alias of MeasureTheory.eLpNorm'_le_nnreal_smul_eLpNorm'_of_ae_le_mul.

theorem MeasureTheory.eLpNormEssSup_le_nnreal_smul_eLpNormEssSup_of_ae_le_mul {α : Type u_1} {F : Type u_3} {G : Type u_4} {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 μ

@[deprecated MeasureTheory.eLpNormEssSup_le_nnreal_smul_eLpNormEssSup_of_ae_le_mul]

theorem MeasureTheory.snormEssSup_le_nnreal_smul_snormEssSup_of_ae_le_mul {α : Type u_1} {F : Type u_3} {G : Type u_4} {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 μ

Alias of MeasureTheory.eLpNormEssSup_le_nnreal_smul_eLpNormEssSup_of_ae_le_mul.

theorem MeasureTheory.eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul {α : Type u_1} {F : Type u_3} {G : Type u_4} {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 μ

@[deprecated MeasureTheory.eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul]

theorem MeasureTheory.snorm_le_nnreal_smul_snorm_of_ae_le_mul {α : Type u_1} {F : Type u_3} {G : Type u_4} {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 μ

Alias of MeasureTheory.eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul.

theorem MeasureTheory.eLpNorm_eq_zero_and_zero_of_ae_le_mul_neg {α : Type u_1} {F : Type u_3} {G : Type u_4} {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.

@[deprecated MeasureTheory.eLpNorm_eq_zero_and_zero_of_ae_le_mul_neg]

theorem MeasureTheory.snorm_eq_zero_and_zero_of_ae_le_mul_neg {α : Type u_1} {F : Type u_3} {G : Type u_4} {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

Alias of MeasureTheory.eLpNorm_eq_zero_and_zero_of_ae_le_mul_neg.

---

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_3} {G : Type u_4} {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 μ

@[deprecated MeasureTheory.eLpNorm_le_mul_eLpNorm_of_ae_le_mul]

theorem MeasureTheory.snorm_le_mul_snorm_of_ae_le_mul {α : Type u_1} {F : Type u_3} {G : Type u_4} {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 μ

Alias of MeasureTheory.eLpNorm_le_mul_eLpNorm_of_ae_le_mul.

theorem MeasureTheory.Memℒp.of_nnnorm_le_mul {α : Type u_1} {E : Type u_2} {F : Type u_3} {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_2} {F : Type u_3} {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_3} {m0 : MeasurableSpace α} {q : ℝ} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {𝕜 : Type u_5} [NormedRing 𝕜] [MulActionWithZero 𝕜 F] [BoundedSMul 𝕜 F] (c : 𝕜) (f : α → F) (hq_pos : 0 < q) : MeasureTheory.eLpNorm' (c • f) q μ ≤ ‖c‖₊ • MeasureTheory.eLpNorm' f q μ

@[deprecated MeasureTheory.eLpNorm'_const_smul_le]

theorem MeasureTheory.snorm'_const_smul_le {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {q : ℝ} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {𝕜 : Type u_5} [NormedRing 𝕜] [MulActionWithZero 𝕜 F] [BoundedSMul 𝕜 F] (c : 𝕜) (f : α → F) (hq_pos : 0 < q) : MeasureTheory.eLpNorm' (c • f) q μ ≤ ‖c‖₊ • MeasureTheory.eLpNorm' f q μ

Alias of MeasureTheory.eLpNorm'_const_smul_le.

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

@[deprecated MeasureTheory.eLpNormEssSup_const_smul_le]

theorem MeasureTheory.snormEssSup_const_smul_le {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {𝕜 : Type u_5} [NormedRing 𝕜] [MulActionWithZero 𝕜 F] [BoundedSMul 𝕜 F] (c : 𝕜) (f : α → F) : MeasureTheory.eLpNormEssSup (c • f) μ ≤ ‖c‖₊ • MeasureTheory.eLpNormEssSup f μ

Alias of MeasureTheory.eLpNormEssSup_const_smul_le.

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

@[deprecated MeasureTheory.eLpNorm_const_smul_le]

theorem MeasureTheory.snorm_const_smul_le {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {𝕜 : Type u_5} [NormedRing 𝕜] [MulActionWithZero 𝕜 F] [BoundedSMul 𝕜 F] (c : 𝕜) (f : α → F) : MeasureTheory.eLpNorm (c • f) p μ ≤ ‖c‖₊ • MeasureTheory.eLpNorm f p μ

Alias of MeasureTheory.eLpNorm_const_smul_le.

theorem MeasureTheory.Memℒp.const_smul {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {𝕜 : Type u_5} [NormedRing 𝕜] [MulActionWithZero 𝕜 E] [BoundedSMul 𝕜 E] {f : α → E} (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 α} {R : Type u_6} [NormedRing R] {f : α → R} (hf : MeasureTheory.Memℒp f p μ) (c : R) : 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_3} {m0 : MeasurableSpace α} {q : ℝ} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {𝕜 : Type u_5} [NormedDivisionRing 𝕜] [Module 𝕜 F] [BoundedSMul 𝕜 F] {f : α → F} (c : 𝕜) (hq_pos : 0 < q) : MeasureTheory.eLpNorm' (c • f) q μ = ‖c‖₊ • MeasureTheory.eLpNorm' f q μ

@[deprecated MeasureTheory.eLpNorm'_const_smul]

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

Alias of MeasureTheory.eLpNorm'_const_smul.

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

@[deprecated MeasureTheory.eLpNormEssSup_const_smul]

theorem MeasureTheory.snormEssSup_const_smul {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {𝕜 : Type u_5} [NormedDivisionRing 𝕜] [Module 𝕜 F] [BoundedSMul 𝕜 F] (c : 𝕜) (f : α → F) : MeasureTheory.eLpNormEssSup (c • f) μ = ↑‖c‖₊ * MeasureTheory.eLpNormEssSup f μ

Alias of MeasureTheory.eLpNormEssSup_const_smul.

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

@[deprecated MeasureTheory.eLpNorm_const_smul]

theorem MeasureTheory.snorm_const_smul {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {𝕜 : Type u_5} [NormedDivisionRing 𝕜] [Module 𝕜 F] [BoundedSMul 𝕜 F] (c : 𝕜) (f : α → F) : MeasureTheory.eLpNorm (c • f) p μ = ↑‖c‖₊ * MeasureTheory.eLpNorm f p μ

Alias of MeasureTheory.eLpNorm_const_smul.

theorem MeasureTheory.le_eLpNorm_of_bddBelow {α : Type u_1} {F : Type u_3} {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 μ

@[deprecated MeasureTheory.le_eLpNorm_of_bddBelow]

theorem MeasureTheory.le_snorm_of_bddBelow {α : Type u_1} {F : Type u_3} {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 μ

Alias of MeasureTheory.le_eLpNorm_of_bddBelow.

@[deprecated MeasureTheory.le_snorm_of_bddBelow]

theorem MeasureTheory.snorm_indicator_ge_of_bdd_below {α : Type u_1} {F : Type u_3} {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 μ

Alias of MeasureTheory.le_eLpNorm_of_bddBelow.

---

Alias of MeasureTheory.le_eLpNorm_of_bddBelow.

theorem MeasureTheory.Memℒp.re {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {𝕜 : Type u_5} [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_5} [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_2} {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 < ⊤

@[deprecated MeasureTheory.ae_bdd_liminf_atTop_rpow_of_eLpNorm_bdd]

theorem MeasureTheory.ae_bdd_liminf_atTop_rpow_of_snorm_bdd {α : Type u_1} {E : Type u_2} {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 < ⊤

Alias of MeasureTheory.ae_bdd_liminf_atTop_rpow_of_eLpNorm_bdd.

theorem MeasureTheory.ae_bdd_liminf_atTop_of_eLpNorm_bdd {α : Type u_1} {E : Type u_2} {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 < ⊤

@[deprecated MeasureTheory.ae_bdd_liminf_atTop_of_eLpNorm_bdd]

theorem MeasureTheory.ae_bdd_liminf_atTop_of_snorm_bdd {α : Type u_1} {E : Type u_2} {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 < ⊤

Alias of MeasureTheory.ae_bdd_liminf_atTop_of_eLpNorm_bdd.

theorem Continuous.memℒp_top_of_hasCompactSupport {E : Type u_2} [NormedAddCommGroup E] {X : Type u_5} [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_5} [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 μ.

@[deprecated MeasureTheory.Memℒp.exists_eLpNorm_indicator_compl_lt]

theorem MeasureTheory.Memℒp.exists_snorm_indicator_compl_lt {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {β : Type u_5} [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 μ < ε

Alias of MeasureTheory.Memℒp.exists_eLpNorm_indicator_compl_lt.

---

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