Documentation

Mathlib.MeasureTheory.Function.LpSeminorm.Basic

ℒ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 MemLp 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 = ∞.
MemLp 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 MemLp 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 MemLp.

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

(∫ ‖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)

Instances For

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

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} {ε : Type u_2} [ENorm ε] {x✝ : MeasurableSpace α} (f : α → ε) (q : ℝ) (μ : Measure α) :

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 : α → ε) (μ : Measure α) :

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

Equations

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

Instances For

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

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} {ε : Type u_2} [ENorm ε] {x✝ : MeasurableSpace α} (f : α → ε) (μ : Measure α) :

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) (μ : Measure α := by volume_tac) :

ℒ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 μ

Instances For

theorem MeasureTheory.eLpNorm_eq_eLpNorm' {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [ENorm ε] (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) {f : α → ε} :

eLpNorm f p μ = eLpNorm' f p.toReal μ

theorem MeasureTheory.eLpNorm_nnreal_eq_eLpNorm' {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} [ENorm ε] {f : α → ε} {p : NNReal} (hp : p ≠ 0) :

eLpNorm f (↑p) μ = eLpNorm' f (↑p) μ

theorem MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [ENorm ε] (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) {f : α → ε} :

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} {ε : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [ENorm ε] (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) {f : α → ε} :

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} {ε : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} [ENorm ε] {f : α → ε} {p : NNReal} (hp : p ≠ 0) :

eLpNorm f (↑p) μ = (∫⁻ (x : α), ‖f x‖ₑ ^ ↑p ∂μ) ^ (1 / ↑p)

theorem MeasureTheory.eLpNorm_one_eq_lintegral_enorm {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} [ENorm ε] {f : α → ε} :

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} {ε : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} [ENorm ε] {f : α → ε} :

eLpNorm f 1 μ = ∫⁻ (x : α), ‖f x‖ₑ ∂μ

Alias of MeasureTheory.eLpNorm_one_eq_lintegral_enorm.

@[simp]

theorem MeasureTheory.eLpNorm_exponent_top {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} [ENorm ε] {f : α → ε} :

eLpNorm f ⊤ μ = eLpNormEssSup f μ

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

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

Equations

MeasureTheory.MemLp f p μ = (MeasureTheory.AEStronglyMeasurable f μ ∧ MeasureTheory.eLpNorm f p μ < ⊤)

Instances For

@[deprecated MeasureTheory.MemLp (since := "2025-02-21")]

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

Alias of MeasureTheory.MemLp.

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

Equations

@MeasureTheory.Memℒp = @MeasureTheory.MemLp

Instances For

theorem MeasureTheory.MemLp.aestronglyMeasurable {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} [ENorm ε] [TopologicalSpace ε] {f : α → ε} {p : ENNReal} (h : MemLp f p μ) :

AEStronglyMeasurable f μ

@[deprecated MeasureTheory.MemLp.aestronglyMeasurable (since := "2025-02-21")]

theorem MeasureTheory.Memℒp.aestronglyMeasurable {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} [ENorm ε] [TopologicalSpace ε] {f : α → ε} {p : ENNReal} (h : MemLp f p μ) :

AEStronglyMeasurable f μ

Alias of MeasureTheory.MemLp.aestronglyMeasurable.

theorem MeasureTheory.lintegral_rpow_enorm_eq_rpow_eLpNorm' {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {q : ℝ} {μ : Measure α} [ENorm ε] {f : α → ε} (hq0_lt : 0 < q) :

∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ = 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} {ε : Type u_2} {m0 : MeasurableSpace α} {q : ℝ} {μ : Measure α} [ENorm ε] {f : α → ε} (hq0_lt : 0 < q) :

∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ = eLpNorm' f q μ ^ q

Alias of MeasureTheory.lintegral_rpow_enorm_eq_rpow_eLpNorm'.

theorem MeasureTheory.eLpNorm_nnreal_pow_eq_lintegral {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} [ENorm ε] {f : α → ε} {p : NNReal} (hp : p ≠ 0) :

eLpNorm f (↑p) μ ^ ↑p = ∫⁻ (x : α), ‖f x‖ₑ ^ ↑p ∂μ

theorem MeasureTheory.MemLp.eLpNorm_lt_top {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [ENorm ε] [TopologicalSpace ε] {f : α → ε} (hfp : MemLp f p μ) :

eLpNorm f p μ < ⊤

@[deprecated MeasureTheory.MemLp.eLpNorm_lt_top (since := "2025-02-21")]

theorem MeasureTheory.Memℒp.eLpNorm_lt_top {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [ENorm ε] [TopologicalSpace ε] {f : α → ε} (hfp : MemLp f p μ) :

eLpNorm f p μ < ⊤

Alias of MeasureTheory.MemLp.eLpNorm_lt_top.

theorem MeasureTheory.MemLp.eLpNorm_ne_top {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [ENorm ε] [TopologicalSpace ε] {f : α → ε} (hfp : MemLp f p μ) :

eLpNorm f p μ ≠ ⊤

@[deprecated MeasureTheory.MemLp.eLpNorm_ne_top (since := "2025-02-21")]

theorem MeasureTheory.Memℒp.eLpNorm_ne_top {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [ENorm ε] [TopologicalSpace ε] {f : α → ε} (hfp : MemLp f p μ) :

eLpNorm f p μ ≠ ⊤

Alias of MeasureTheory.MemLp.eLpNorm_ne_top.

theorem MeasureTheory.lintegral_rpow_enorm_lt_top_of_eLpNorm'_lt_top {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {q : ℝ} {μ : Measure α} [ENorm ε] {f : α → ε} (hq0_lt : 0 < q) (hfq : 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} {ε : Type u_2} {m0 : MeasurableSpace α} {q : ℝ} {μ : Measure α} [ENorm ε] {f : α → ε} (hq0_lt : 0 < q) (hfq : 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} {ε : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [ENorm ε] {f : α → ε} (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) (hfp : 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} {ε : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [ENorm ε] {f : α → ε} (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) (hfp : 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_enorm_lt_top {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [ENorm ε] {f : α → ε} (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) :

eLpNorm f p μ < ⊤ ↔ ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ < ⊤

@[deprecated MeasureTheory.eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top (since := "2025-02-04")]

theorem MeasureTheory.eLpNorm_lt_top_iff_lintegral_rpow_nnnorm_lt_top {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [ENorm ε] {f : α → ε} (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) :

eLpNorm f p μ < ⊤ ↔ ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ < ⊤

Alias of MeasureTheory.eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top.

@[simp]

theorem MeasureTheory.eLpNorm'_exponent_zero {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} [ENorm ε] {f : α → ε} :

eLpNorm' f 0 μ = 1

@[simp]

theorem MeasureTheory.eLpNorm_exponent_zero {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} [ENorm ε] {f : α → ε} :

eLpNorm f 0 μ = 0

@[simp]

theorem MeasureTheory.memLp_zero_iff_aestronglyMeasurable {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} [ENorm ε] [TopologicalSpace ε] {f : α → ε} :

MemLp f 0 μ ↔ AEStronglyMeasurable f μ

@[deprecated MeasureTheory.memLp_zero_iff_aestronglyMeasurable (since := "2025-02-21")]

theorem MeasureTheory.memℒp_zero_iff_aestronglyMeasurable {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} [ENorm ε] [TopologicalSpace ε] {f : α → ε} :

MemLp f 0 μ ↔ AEStronglyMeasurable f μ

Alias of MeasureTheory.memLp_zero_iff_aestronglyMeasurable.

@[simp]

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

eLpNorm' 0 q μ = 0

@[simp]

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

eLpNorm' 0 q μ = 0

@[simp]

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

eLpNormEssSup 0 μ = 0

@[simp]

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

eLpNorm 0 p μ = 0

@[simp]

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

eLpNorm (fun (x : α) => 0) p μ = 0

@[simp]

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

MemLp 0 p μ

@[deprecated MeasureTheory.MemLp.zero (since := "2025-02-21")]

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

MemLp 0 p μ

Alias of MeasureTheory.MemLp.zero.

@[simp]

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

MemLp (fun (x : α) => 0) p μ

@[deprecated MeasureTheory.MemLp.zero' (since := "2025-02-21")]

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

MemLp (fun (x : α) => 0) p μ

Alias of MeasureTheory.MemLp.zero'.

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

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

MemLp 0 p μ

Alias of MeasureTheory.MemLp.zero.

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

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

MemLp (fun (x : α) => 0) p μ

Alias of MeasureTheory.MemLp.zero'.

theorem MeasureTheory.eLpNorm'_measure_zero_of_pos {α : Type u_1} {ε : Type u_2} {q : ℝ} [ENorm ε] [MeasurableSpace α] {f : α → ε} (hq_pos : 0 < q) :

eLpNorm' f q 0 = 0

theorem MeasureTheory.eLpNorm'_measure_zero_of_exponent_zero {α : Type u_1} {ε : Type u_2} [ENorm ε] [MeasurableSpace α] {f : α → ε} :

eLpNorm' f 0 0 = 1

theorem MeasureTheory.eLpNorm'_measure_zero_of_neg {α : Type u_1} {ε : Type u_2} {q : ℝ} [ENorm ε] [MeasurableSpace α] {f : α → ε} (hq_neg : q < 0) :

eLpNorm' f q 0 = ⊤

@[simp]

theorem MeasureTheory.eLpNormEssSup_measure_zero {α : Type u_1} {ε : Type u_2} [ENorm ε] [MeasurableSpace α] {f : α → ε} :

eLpNormEssSup f 0 = 0

@[simp]

theorem MeasureTheory.eLpNorm_measure_zero {α : Type u_1} {ε : Type u_2} {p : ENNReal} [ENorm ε] [MeasurableSpace α] {f : α → ε} :

eLpNorm f p 0 = 0

@[simp]

theorem MeasureTheory.memLp_measure_zero {α : Type u_1} {ε : Type u_2} {p : ENNReal} [ENorm ε] [MeasurableSpace α] [TopologicalSpace ε] {f : α → ε} :

MemLp f p 0

@[deprecated MeasureTheory.memLp_measure_zero (since := "2025-02-21")]

theorem MeasureTheory.memℒp_measure_zero {α : Type u_1} {ε : Type u_2} {p : ENNReal} [ENorm ε] [MeasurableSpace α] [TopologicalSpace ε] {f : α → ε} :

MemLp f p 0

Alias of MeasureTheory.memLp_measure_zero.

@[simp]

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

eLpNorm' (-f) q μ = eLpNorm' f q μ

@[simp]

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

eLpNorm (-f) p μ = eLpNorm f p μ

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

eLpNorm (f - g) p μ = eLpNorm (g - f) p μ

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

MemLp (-f) p μ

@[deprecated MeasureTheory.MemLp.neg (since := "2025-02-21")]

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

MemLp (-f) p μ

Alias of MeasureTheory.MemLp.neg.

theorem MeasureTheory.memLp_neg_iff {α : Type u_1} {E : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {f : α → E} :

MemLp (-f) p μ ↔ MemLp f p μ

@[deprecated MeasureTheory.memLp_neg_iff (since := "2025-02-21")]

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

MemLp (-f) p μ ↔ MemLp f p μ

Alias of MeasureTheory.memLp_neg_iff.

theorem MeasureTheory.eLpNorm'_const {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {q : ℝ} {μ : Measure α} [ENorm ε] (c : ε) (hq_pos : 0 < q) :

eLpNorm' (fun (x : α) => c) q μ = ‖c‖ₑ * μ Set.univ ^ (1 / q)

theorem MeasureTheory.eLpNorm'_const' {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {q : ℝ} {μ : Measure α} [NormedAddCommGroup F] [IsFiniteMeasure μ] (c : F) (hc_ne_zero : c ≠ 0) (hq_ne_zero : q ≠ 0) :

eLpNorm' (fun (x : α) => c) q μ = ‖c‖ₑ * μ Set.univ ^ (1 / q)

theorem MeasureTheory.eLpNormEssSup_const {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} [ENorm ε] (c : ε) (hμ : μ ≠ 0) :

eLpNormEssSup (fun (x : α) => c) μ = ‖c‖ₑ

theorem MeasureTheory.eLpNorm'_const_of_isProbabilityMeasure {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {q : ℝ} {μ : Measure α} [ENorm ε] (c : ε) (hq_pos : 0 < q) [IsProbabilityMeasure μ] :

eLpNorm' (fun (x : α) => c) q μ = ‖c‖ₑ

theorem MeasureTheory.eLpNorm_const {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [ENorm ε] (c : ε) (h0 : p ≠ 0) (hμ : μ ≠ 0) :

eLpNorm (fun (x : α) => c) p μ = ‖c‖ₑ * μ Set.univ ^ (1 / p.toReal)

theorem MeasureTheory.eLpNorm_const' {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [ENorm ε] (c : ε) (h0 : p ≠ 0) (h_top : p ≠ ⊤) :

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 α} {μ : Measure α} [NormedAddCommGroup F] {p : ENNReal} {c : F} (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) :

eLpNorm (fun (x : α) => c) p μ < ⊤ ↔ c = 0 ∨ μ Set.univ < ⊤

theorem MeasureTheory.memLp_const {α : Type u_1} {E : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] (c : E) [IsFiniteMeasure μ] :

MemLp (fun (x : α) => c) p μ

@[deprecated MeasureTheory.memLp_const (since := "2025-02-21")]

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

MemLp (fun (x : α) => c) p μ

Alias of MeasureTheory.memLp_const.

theorem MeasureTheory.memLp_top_const {α : Type u_1} {E : Type u_3} {m0 : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup E] (c : E) :

MemLp (fun (x : α) => c) ⊤ μ

@[deprecated MeasureTheory.memLp_top_const (since := "2025-02-21")]

theorem MeasureTheory.memℒp_top_const {α : Type u_1} {E : Type u_3} {m0 : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup E] (c : E) :

MemLp (fun (x : α) => c) ⊤ μ

Alias of MeasureTheory.memLp_top_const.

theorem MeasureTheory.memLp_const_iff {α : Type u_1} {E : Type u_3} {m0 : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup E] {p : ENNReal} {c : E} (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) :

MemLp (fun (x : α) => c) p μ ↔ c = 0 ∨ μ Set.univ < ⊤

@[deprecated MeasureTheory.memLp_const_iff (since := "2025-02-21")]

theorem MeasureTheory.memℒp_const_iff {α : Type u_1} {E : Type u_3} {m0 : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup E] {p : ENNReal} {c : E} (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) :

MemLp (fun (x : α) => c) p μ ↔ c = 0 ∨ μ Set.univ < ⊤

Alias of MeasureTheory.memLp_const_iff.

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

eLpNorm' f q μ ≤ eLpNorm' g q μ

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

eLpNorm' f q μ ≤ eLpNorm' g q μ

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

eLpNorm' f q μ = eLpNorm' g q μ

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

eLpNorm' f q μ = eLpNorm' g q μ

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

eLpNorm' f q μ = eLpNorm' g q μ

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

eLpNormEssSup f μ = eLpNormEssSup g μ

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

eLpNormEssSup f μ ≤ eLpNormEssSup g μ

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

eLpNorm f p μ ≤ eLpNorm g p μ

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

eLpNorm f p μ ≤ eLpNorm g p μ

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

eLpNorm f p μ ≤ eLpNorm g p μ

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

eLpNorm f p μ ≤ eLpNorm g p μ

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

eLpNorm f p μ ≤ eLpNorm g p μ

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

eLpNorm f p μ ≤ eLpNorm g p μ

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

eLpNormEssSup f μ ≤ ↑C

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

eLpNormEssSup f μ ≤ ENNReal.ofReal C

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

eLpNormEssSup f μ < ⊤

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

eLpNormEssSup f μ < ⊤

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

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} {μ : Measure α} [NormedAddCommGroup F] {f : α → F} {C : ℝ} (hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C) :

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} {μ : Measure α} [NormedAddCommGroup F] [NormedAddCommGroup G] {f : α → F} {g : α → G} (hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ = ‖g x‖₊) :

eLpNorm f p μ = eLpNorm g p μ

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

eLpNorm f p μ = eLpNorm g p μ

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

eLpNorm (s.indicator f - t.indicator f) p μ = eLpNorm ((symmDiff s t).indicator f) p μ

@[simp]

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

eLpNorm' (fun (a : α) => ‖f a‖) q μ = eLpNorm' f q μ

@[simp]

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

eLpNorm (fun (x : α) => ‖f x‖) p μ = eLpNorm f p μ

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

eLpNorm' (fun (x : α) => ‖f x‖ ^ q) p μ = eLpNorm' f (p * q) μ ^ q

theorem MeasureTheory.eLpNorm_norm_rpow {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {q : ℝ} {μ : Measure α} [NormedAddCommGroup F] (f : α → F) (hq_pos : 0 < q) :

eLpNorm (fun (x : α) => ‖f x‖ ^ q) p μ = eLpNorm f (p * ENNReal.ofReal q) μ ^ q

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

eLpNorm f p μ = eLpNorm g p μ

theorem MeasureTheory.memLp_congr_ae {α : Type u_1} {E : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {f g : α → E} (hfg : f =ᶠ[ae μ] g) :

MemLp f p μ ↔ MemLp g p μ

@[deprecated MeasureTheory.memLp_congr_ae (since := "2025-02-21")]

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

MemLp f p μ ↔ MemLp g p μ

Alias of MeasureTheory.memLp_congr_ae.

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

MemLp g p μ

@[deprecated MeasureTheory.MemLp.ae_eq (since := "2025-02-21")]

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

MemLp g p μ

Alias of MeasureTheory.MemLp.ae_eq.

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

MemLp f p μ

@[deprecated MeasureTheory.MemLp.of_le (since := "2025-02-21")]

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

MemLp f p μ

Alias of MeasureTheory.MemLp.of_le.

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

MemLp f p μ

Alias of MeasureTheory.MemLp.of_le.

@[deprecated MeasureTheory.MemLp.mono (since := "2025-02-21")]

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

MemLp f p μ

Alias of MeasureTheory.MemLp.of_le.

Alias of MeasureTheory.MemLp.of_le.

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

MemLp f p μ

@[deprecated MeasureTheory.MemLp.mono' (since := "2025-02-21")]

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

MemLp f p μ

Alias of MeasureTheory.MemLp.mono'.

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

MemLp g p μ

@[deprecated MeasureTheory.MemLp.congr_norm (since := "2025-02-21")]

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

MemLp g p μ

Alias of MeasureTheory.MemLp.congr_norm.

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

MemLp f p μ ↔ MemLp g p μ

@[deprecated MeasureTheory.memLp_congr_norm (since := "2025-02-21")]

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

MemLp f p μ ↔ MemLp g p μ

Alias of MeasureTheory.memLp_congr_norm.

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

@[deprecated MeasureTheory.memLp_top_of_bound (since := "2025-02-21")]

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

Alias of MeasureTheory.memLp_top_of_bound.

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

MemLp f p μ

@[deprecated MeasureTheory.MemLp.of_bound (since := "2025-02-21")]

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

MemLp f p μ

Alias of MeasureTheory.MemLp.of_bound.

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

MemLp f p μ

@[deprecated MeasureTheory.memLp_of_bounded (since := "2025-02-21")]

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

MemLp f p μ

Alias of MeasureTheory.memLp_of_bounded.

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

eLpNorm' f q ν ≤ eLpNorm' f q μ

theorem MeasureTheory.eLpNormEssSup_mono_measure {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {μ ν : Measure α} [ENorm ε] (f : α → ε) (hμν : ν.AbsolutelyContinuous μ) :

eLpNormEssSup f ν ≤ eLpNormEssSup f μ

theorem MeasureTheory.eLpNorm_mono_measure {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ ν : Measure α} [ENorm ε] (f : α → ε) (hμν : ν ≤ μ) :

eLpNorm f p ν ≤ eLpNorm f p μ

theorem MeasureTheory.MemLp.mono_measure {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ ν : Measure α} [ENorm ε] [TopologicalSpace ε] {f : α → ε} (hμν : ν ≤ μ) (hf : MemLp f p μ) :

MemLp f p ν

@[deprecated MeasureTheory.MemLp.mono_measure (since := "2025-02-21")]

theorem MeasureTheory.Memℒp.mono_measure {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ ν : Measure α} [ENorm ε] [TopologicalSpace ε] {f : α → ε} (hμν : ν ≤ μ) (hf : MemLp f p μ) :

MemLp f p ν

Alias of MeasureTheory.MemLp.mono_measure.

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

eLpNorm (s.indicator f) p μ = 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} {μ : Measure α} [NormedAddCommGroup F] {f : α → F} {s : Set α} (hs : MeasurableSet s) :

eLpNorm (s.indicator f) p μ = 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 α} {μ : Measure α} [NormedAddCommGroup F] {f : α → F} {s : Set α} (hs : MeasurableSet s) :

eLpNormEssSup (s.indicator f) μ = eLpNormEssSup f (μ.restrict s)

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

eLpNorm f p (μ.restrict s) ≤ eLpNorm f p μ

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

eLpNorm (s.indicator f) p μ ≤ eLpNorm f p μ

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

eLpNormEssSup (s.indicator f) μ ≤ eLpNormEssSup f μ

theorem MeasureTheory.eLpNormEssSup_indicator_const_le {α : Type u_1} {G : Type u_5} {m0 : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup G] (s : Set α) (c : G) :

eLpNormEssSup (s.indicator fun (x : α) => c) μ ≤ ‖c‖ₑ

theorem MeasureTheory.eLpNormEssSup_indicator_const_eq {α : Type u_1} {G : Type u_5} {m0 : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup G] (s : Set α) (c : G) (hμs : μ s ≠ 0) :

eLpNormEssSup (s.indicator fun (x : α) => c) μ = ‖c‖ₑ

theorem MeasureTheory.eLpNorm_indicator_const₀ {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup F] {s : Set α} {c : F} (hs : NullMeasurableSet s μ) (hp : p ≠ 0) (hp_top : p ≠ ⊤) :

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} {μ : Measure α} [NormedAddCommGroup F] {s : Set α} {c : F} (hs : MeasurableSet s) (hp : p ≠ 0) (hp_top : p ≠ ⊤) :

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} {μ : Measure α} [NormedAddCommGroup F] {s : Set α} {c : F} (hs : MeasurableSet s) (hμs : μ s ≠ 0) (hp : p ≠ 0) :

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 α} {μ : Measure α} [NormedAddCommGroup G] {s : Set α} (c : G) (p : ENNReal) :

eLpNorm (s.indicator fun (x : α) => c) p μ ≤ ‖c‖ₑ * μ s ^ (1 / p.toReal)

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

MemLp (s.indicator f) p μ

@[deprecated MeasureTheory.MemLp.indicator (since := "2025-02-21")]

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

MemLp (s.indicator f) p μ

Alias of MeasureTheory.MemLp.indicator.

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

MemLp (s.indicator f) p μ ↔ MemLp f p (μ.restrict s)

@[deprecated MeasureTheory.memLp_indicator_iff_restrict (since := "2025-02-21")]

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

MemLp (s.indicator f) p μ ↔ MemLp f p (μ.restrict s)

Alias of MeasureTheory.memLp_indicator_iff_restrict.

theorem MeasureTheory.memLp_indicator_const {α : Type u_1} {E : Type u_3} {m0 : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup E] {s : Set α} (p : ENNReal) (hs : MeasurableSet s) (c : E) (hμsc : c = 0 ∨ μ s ≠ ⊤) :

MemLp (s.indicator fun (x : α) => c) p μ

@[deprecated MeasureTheory.memLp_indicator_const (since := "2025-02-21")]

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

MemLp (s.indicator fun (x : α) => c) p μ

Alias of MeasureTheory.memLp_indicator_const.

theorem MeasureTheory.eLpNormEssSup_piecewise {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} [ENorm ε] {s : Set α} (f g : α → ε) [DecidablePred fun (x : α) => x ∈ s] (hs : MeasurableSet s) :

eLpNormEssSup (s.piecewise f g) μ = eLpNormEssSup f (μ.restrict s) ⊔ eLpNormEssSup g (μ.restrict sᶜ)

theorem MeasureTheory.eLpNorm_top_piecewise {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} [ENorm ε] {s : Set α} (f g : α → ε) [DecidablePred fun (x : α) => x ∈ s] (hs : MeasurableSet s) :

eLpNorm (s.piecewise f g) ⊤ μ = eLpNorm f ⊤ (μ.restrict s) ⊔ eLpNorm g ⊤ (μ.restrict sᶜ)

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

MemLp (s.piecewise f g) p μ

@[deprecated MeasureTheory.MemLp.piecewise (since := "2025-02-21")]

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

MemLp (s.piecewise f g) p μ

Alias of MeasureTheory.MemLp.piecewise.

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

eLpNorm f p (μ.restrict s) = 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.MemLp.restrict {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [ENorm ε] [TopologicalSpace ε] (s : Set α) {f : α → ε} (hf : MemLp f p μ) :

MemLp f p (μ.restrict s)

@[deprecated MeasureTheory.MemLp.restrict (since := "2025-02-21")]

theorem MeasureTheory.Memℒp.restrict {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [ENorm ε] [TopologicalSpace ε] (s : Set α) {f : α → ε} (hf : MemLp f p μ) :

MemLp f p (μ.restrict s)

Alias of MeasureTheory.MemLp.restrict.

theorem MeasureTheory.eLpNorm'_smul_measure {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} [ENorm ε] {p : ℝ} (hp : 0 ≤ p) {f : α → ε} (c : ENNReal) :

eLpNorm' f p (c • μ) = c ^ (1 / p) * eLpNorm' f p μ

@[simp]

theorem MeasureTheory.eLpNormEssSup_smul_measure {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {μ : 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) :

eLpNormEssSup f (c • μ) = 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) (μ : Measure α) :

eLpNorm f p (c • μ) = c ^ (1 / p).toReal • 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) (μ : Measure α) :

eLpNorm f p (c • μ) = c ^ p.toReal⁻¹ • 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 α} {μ : Measure α} [NormedAddCommGroup F] {p : ENNReal} (hp_ne_top : p ≠ ⊤) (f : α → F) (c : ENNReal) :

eLpNorm f p (c • μ) = c ^ (1 / p).toReal • 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} {μ : Measure α} [NormedAddCommGroup F] (hp : p ≠ ⊤) (c : NNReal) (f : α → F) :

eLpNorm f p (c • μ) = c ^ p.toReal⁻¹ • 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 α} {μ : Measure α} [NormedAddCommGroup F] {f : α → F} (c : ENNReal) :

eLpNorm f 1 (c • μ) = c * eLpNorm f 1 μ

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

MemLp f p μ'

@[deprecated MeasureTheory.MemLp.of_measure_le_smul (since := "2025-02-21")]

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

MemLp f p μ'

Alias of MeasureTheory.MemLp.of_measure_le_smul.

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

MemLp f p (c • μ)

@[deprecated MeasureTheory.MemLp.smul_measure (since := "2025-02-21")]

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

MemLp f p (c • μ)

Alias of MeasureTheory.MemLp.smul_measure.

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

eLpNorm f 1 (μ + ν) = eLpNorm f 1 μ + eLpNorm f 1 ν

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

eLpNorm f p μ ≤ eLpNorm f p (μ + ν)

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

eLpNorm f p ν ≤ eLpNorm f p (μ + ν)

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

eLpNormEssSup f μ = ⨆ (a : α), ‖f a‖ₑ

@[simp]

theorem MeasureTheory.eLpNormEssSup_count {α : Type u_1} {E : Type u_3} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [MeasurableSingletonClass α] (f : α → E) :

eLpNormEssSup f Measure.count = ⨆ (a : α), ‖f a‖ₑ

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

MemLp f p μ

@[deprecated MeasureTheory.MemLp.left_of_add_measure (since := "2025-02-21")]

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

MemLp f p μ

Alias of MeasureTheory.MemLp.left_of_add_measure.

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

MemLp f p ν

@[deprecated MeasureTheory.MemLp.right_of_add_measure (since := "2025-02-21")]

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

MemLp f p ν

Alias of MeasureTheory.MemLp.right_of_add_measure.

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

MemLp (fun (x : α) => ‖f x‖) p μ

@[deprecated MeasureTheory.MemLp.norm (since := "2025-02-21")]

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

MemLp (fun (x : α) => ‖f x‖) p μ

Alias of MeasureTheory.MemLp.norm.

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

MemLp (fun (x : α) => ‖f x‖) p μ ↔ MemLp f p μ

@[deprecated MeasureTheory.memLp_norm_iff (since := "2025-02-21")]

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

MemLp (fun (x : α) => ‖f x‖) p μ ↔ MemLp f p μ

Alias of MeasureTheory.memLp_norm_iff.

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

eLpNorm' f q μ = 0

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

eLpNorm' f q μ = 0

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

f =ᶠ[ae μ] 0

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

eLpNorm' f q μ = 0 ↔ f =ᶠ[ae μ] 0

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

∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ eLpNormEssSup f μ

@[simp]

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

eLpNormEssSup f μ = 0 ↔ f =ᶠ[ae μ] 0

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

eLpNorm f p μ = 0 ↔ f =ᶠ[ae μ] 0

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

eLpNorm f p μ = 0

theorem MeasureTheory.ae_le_eLpNormEssSup {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} [ENorm ε] {f : α → ε} :

∀ᵐ (y : α) ∂μ, ‖f y‖ₑ ≤ eLpNormEssSup f μ

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

eLpNormEssSup f μ < ⊤ ↔ Filter.IsBoundedUnder (fun (x1 x2 : NNReal) => x1 ≤ x2) (ae μ) fun (x : α) => ‖f x‖₊

theorem MeasureTheory.meas_eLpNormEssSup_lt {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} [ENorm ε] {f : α → ε} :

μ {y : α | eLpNormEssSup f μ < ‖f y‖ₑ } = 0

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

eLpNorm f p μ < ⊤

@[simp]

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

MemLp f p μ

@[deprecated MeasureTheory.MemLp.of_discrete (since := "2025-02-21")]

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

MemLp f p μ

Alias of MeasureTheory.MemLp.of_discrete.

@[simp]

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

eLpNorm f p μ = 0

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

eLpNormEssSup g (Measure.map f μ) = eLpNormEssSup (g ∘ f) μ

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

eLpNorm g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ

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

MemLp g p (Measure.map f μ) ↔ MemLp (g ∘ f) p μ

@[deprecated MeasureTheory.memLp_map_measure_iff (since := "2025-02-21")]

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

MemLp g p (Measure.map f μ) ↔ MemLp (g ∘ f) p μ

Alias of MeasureTheory.memLp_map_measure_iff.

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

MemLp (g ∘ f) p μ

@[deprecated MeasureTheory.MemLp.comp_of_map (since := "2025-02-21")]

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

MemLp (g ∘ f) p μ

Alias of MeasureTheory.MemLp.comp_of_map.

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

eLpNorm (g ∘ f) p μ = eLpNorm g p ν

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

eLpNorm (↑(g.compMeasurePreserving f hf)) p μ = eLpNorm (↑g) p ν

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

MemLp (g ∘ f) p μ

@[deprecated MeasureTheory.MemLp.comp_measurePreserving (since := "2025-02-21")]

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

MemLp (g ∘ f) p μ

Alias of MeasureTheory.MemLp.comp_measurePreserving.

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.memLp_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.MemLp g p (MeasureTheory.Measure.map f μ) ↔ MeasureTheory.MemLp (g ∘ f) p μ

@[deprecated MeasurableEmbedding.memLp_map_measure_iff (since := "2025-02-21")]

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.MemLp g p (MeasureTheory.Measure.map f μ) ↔ MeasureTheory.MemLp (g ∘ f) p μ

Alias of MeasurableEmbedding.memLp_map_measure_iff.

theorem MeasurableEquiv.memLp_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.MemLp g p (MeasureTheory.Measure.map (⇑f) μ) ↔ MeasureTheory.MemLp (g ∘ ⇑f) p μ

@[deprecated MeasurableEquiv.memLp_map_measure_iff (since := "2025-02-21")]

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.MemLp g p (MeasureTheory.Measure.map (⇑f) μ) ↔ MeasureTheory.MemLp (g ∘ ⇑f) p μ

Alias of MeasurableEquiv.memLp_map_measure_iff.

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

eLpNorm' f p μ ≤ c • 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 α} {μ : Measure α} [NormedAddCommGroup F] [NormedAddCommGroup G] {f : α → F} {g : α → G} {c : NNReal} (h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊) :

eLpNormEssSup f μ ≤ c • 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 α} {μ : Measure α} [NormedAddCommGroup F] [NormedAddCommGroup G] {f : α → F} {g : α → G} {c : NNReal} (h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊) (p : ENNReal) :

eLpNorm f p μ ≤ c • 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 α} {μ : Measure α} [NormedAddCommGroup F] [NormedAddCommGroup G] {f : α → F} {g : α → G} {c : ℝ} (h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c * ‖g x‖) (hc : c < 0) (p : ENNReal) :

eLpNorm f p μ = 0 ∧ 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 α} {μ : Measure α} [NormedAddCommGroup F] [NormedAddCommGroup G] {f : α → F} {g : α → G} {c : ℝ} (h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c * ‖g x‖) (p : ENNReal) :

eLpNorm f p μ ≤ ENNReal.ofReal c * eLpNorm g p μ

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

MemLp f p μ

@[deprecated MeasureTheory.MemLp.of_nnnorm_le_mul (since := "2025-02-21")]

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

MemLp f p μ

Alias of MeasureTheory.MemLp.of_nnnorm_le_mul.

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

MemLp f p μ

@[deprecated MeasureTheory.MemLp.of_le_mul (since := "2025-02-21")]

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

MemLp f p μ

Alias of MeasureTheory.MemLp.of_le_mul.

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 : ℝ} {μ : Measure α} [NormedAddCommGroup F] {𝕜 : Type u_6} [NormedRing 𝕜] [MulActionWithZero 𝕜 F] [BoundedSMul 𝕜 F] {c : 𝕜} {f : α → F} (hq : 0 < q) :

eLpNorm' (c • f) q μ ≤ ‖c‖ₑ * eLpNorm' f q μ

theorem MeasureTheory.eLpNormEssSup_const_smul_le {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup F] {𝕜 : Type u_6} [NormedRing 𝕜] [MulActionWithZero 𝕜 F] [BoundedSMul 𝕜 F] {c : 𝕜} {f : α → F} :

eLpNormEssSup (c • f) μ ≤ ‖c‖ₑ * eLpNormEssSup f μ

theorem MeasureTheory.eLpNorm_const_smul_le {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup F] {𝕜 : Type u_6} [NormedRing 𝕜] [MulActionWithZero 𝕜 F] [BoundedSMul 𝕜 F] {c : 𝕜} {f : α → F} :

eLpNorm (c • f) p μ ≤ ‖c‖ₑ * eLpNorm f p μ

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

MemLp (c • f) p μ

@[deprecated MeasureTheory.MemLp.const_smul (since := "2025-02-21")]

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

MemLp (c • f) p μ

Alias of MeasureTheory.MemLp.const_smul.

theorem MeasureTheory.MemLp.const_mul {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : Measure α} {𝕜 : Type u_6} [NormedRing 𝕜] {f : α → 𝕜} (hf : MemLp f p μ) (c : 𝕜) :

MemLp (fun (x : α) => c * f x) p μ

@[deprecated MeasureTheory.MemLp.const_mul (since := "2025-02-21")]

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

MemLp (fun (x : α) => c * f x) p μ

Alias of MeasureTheory.MemLp.const_mul.

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 : ℝ} {μ : Measure α} [NormedAddCommGroup F] {𝕜 : Type u_6} [NormedDivisionRing 𝕜] [Module 𝕜 F] [BoundedSMul 𝕜 F] {f : α → F} (c : 𝕜) (hq_pos : 0 < q) :

eLpNorm' (c • f) q μ = ‖c‖ₑ * eLpNorm' f q μ

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

eLpNormEssSup (c • f) μ = ‖c‖ₑ * 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) (μ : Measure α) :

eLpNorm (c • f) p μ = ‖c‖ₑ * eLpNorm f p μ

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

eLpNorm (n • f) p μ = ↑n * eLpNorm f p μ

theorem MeasureTheory.le_eLpNorm_of_bddBelow {α : Type u_1} {F : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : 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) ≤ eLpNorm f p μ

@[simp]

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

eLpNorm ((starRingEnd (α → 𝕜)) f) p μ = eLpNorm f p μ

theorem MeasureTheory.MemLp.re {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : Measure α} {𝕜 : Type u_6} [RCLike 𝕜] {f : α → 𝕜} (hf : MemLp f p μ) :

MemLp (fun (x : α) => RCLike.re (f x)) p μ

@[deprecated MeasureTheory.MemLp.re (since := "2025-02-21")]

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

MemLp (fun (x : α) => RCLike.re (f x)) p μ

Alias of MeasureTheory.MemLp.re.

theorem MeasureTheory.MemLp.im {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : Measure α} {𝕜 : Type u_6} [RCLike 𝕜] {f : α → 𝕜} (hf : MemLp f p μ) :

MemLp (fun (x : α) => RCLike.im (f x)) p μ

@[deprecated MeasureTheory.MemLp.im (since := "2025-02-21")]

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

MemLp (fun (x : α) => RCLike.im (f x)) p μ

Alias of MeasureTheory.MemLp.im.

theorem MeasureTheory.ae_bdd_liminf_atTop_rpow_of_eLpNorm_bdd {α : Type u_1} {E : Type u_3} {m0 : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup E] [MeasurableSpace E] [OpensMeasurableSpace E] {R : NNReal} {p : ENNReal} {f : ℕ → α → E} (hfmeas : ∀ (n : ℕ), Measurable (f n)) (hbdd : ∀ (n : ℕ), 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 α} {μ : Measure α} [NormedAddCommGroup E] [MeasurableSpace E] [OpensMeasurableSpace E] {R : NNReal} {p : ENNReal} (hp : p ≠ 0) {f : ℕ → α → E} (hfmeas : ∀ (n : ℕ), Measurable (f n)) (hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R) :

∀ᵐ (x : α) ∂μ, Filter.liminf (fun (n : ℕ) => ‖f n x‖ₑ) Filter.atTop < ⊤

theorem Continuous.memLp_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.MemLp f ⊤ μ

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

@[deprecated Continuous.memLp_top_of_hasCompactSupport (since := "2025-02-21")]

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.MemLp f ⊤ μ

Alias of Continuous.memLp_top_of_hasCompactSupport.

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

theorem MeasureTheory.MemLp.exists_eLpNorm_indicator_compl_lt {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : Measure α} {β : Type u_6} [NormedAddCommGroup β] (hp_top : p ≠ ⊤) {f : α → β} (hf : MemLp f p μ) {ε : ENNReal} (hε : ε ≠ 0) :

∃ (s : Set α), MeasurableSet s ∧ μ s < ⊤ ∧ eLpNorm (sᶜ.indicator f) p μ < ε

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

@[deprecated MeasureTheory.MemLp.exists_eLpNorm_indicator_compl_lt (since := "2025-02-21")]

theorem MeasureTheory.Memℒp.exists_eLpNorm_indicator_compl_lt {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : Measure α} {β : Type u_6} [NormedAddCommGroup β] (hp_top : p ≠ ⊤) {f : α → β} (hf : MemLp f p μ) {ε : ENNReal} (hε : ε ≠ 0) :

∃ (s : Set α), MeasurableSet s ∧ μ s < ⊤ ∧ eLpNorm (sᶜ.indicator f) p μ < ε

Alias of MeasureTheory.MemLp.exists_eLpNorm_indicator_compl_lt.

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