# ℒp space #

This file describes properties of almost everywhere strongly measurable functions with finite p-seminorm, denoted by snorm 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 #

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

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

• snorm f p μ : for p : ℝ≥0∞, seminorm in ℒp, equal to 0 for p=0, to snorm' f p μ for 0 < p < ∞ and to snormEssSup 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 μ (snorm f p μ < ∞)

### ℒp seminorm #

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

We also define a predicate Memℒp f p μ, requesting that a function is almost everywhere measurable and has finite snorm 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 snorm' and snormEssSup when it makes sense, deduce it for snorm, and translate it in terms of Memℒp.

def MeasureTheory.snorm' {α : Type u_1} {F : Type u_3} :
{x : } → (αF)

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

Equations
Instances For
def MeasureTheory.snormEssSup {α : Type u_1} {F : Type u_3} :
{x : } → (αF)

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

Equations
Instances For
def MeasureTheory.snorm {α : Type u_1} {F : Type u_3} :
{x : } → (αF)

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

Equations
Instances For
theorem MeasureTheory.snorm_eq_snorm' {α : Type u_1} {F : Type u_3} {m0 : } {p : ENNReal} {μ : } (hp_ne_zero : p 0) (hp_ne_top : p ) {f : αF} :
= MeasureTheory.snorm' f p.toReal μ
theorem MeasureTheory.snorm_eq_lintegral_rpow_nnnorm {α : Type u_1} {F : Type u_3} {m0 : } {p : ENNReal} {μ : } (hp_ne_zero : p 0) (hp_ne_top : p ) {f : αF} :
= (∫⁻ (x : α), f x‖₊ ^ p.toRealμ) ^ (1 / p.toReal)
theorem MeasureTheory.snorm_one_eq_lintegral_nnnorm {α : Type u_1} {F : Type u_3} {m0 : } {μ : } {f : αF} :
= ∫⁻ (x : α), f x‖₊μ
@[simp]
theorem MeasureTheory.snorm_exponent_top {α : Type u_1} {F : Type u_3} {m0 : } {μ : } {f : αF} :
def MeasureTheory.Memℒp {E : Type u_2} {α : Type u_5} :
{x : } → (αE)

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
• = ()
Instances For
theorem MeasureTheory.Memℒp.aestronglyMeasurable {α : Type u_1} {E : Type u_2} {m0 : } {μ : } {f : αE} {p : ENNReal} (h : ) :
theorem MeasureTheory.lintegral_rpow_nnnorm_eq_rpow_snorm' {α : Type u_1} {F : Type u_3} {m0 : } {q : } {μ : } {f : αF} (hq0_lt : 0 < q) :
∫⁻ (a : α), f a‖₊ ^ qμ = ^ q
theorem MeasureTheory.Memℒp.snorm_lt_top {α : Type u_1} {E : Type u_2} {m0 : } {p : ENNReal} {μ : } {f : αE} (hfp : ) :
theorem MeasureTheory.Memℒp.snorm_ne_top {α : Type u_1} {E : Type u_2} {m0 : } {p : ENNReal} {μ : } {f : αE} (hfp : ) :
theorem MeasureTheory.lintegral_rpow_nnnorm_lt_top_of_snorm'_lt_top {α : Type u_1} {F : Type u_3} {m0 : } {q : } {μ : } {f : αF} (hq0_lt : 0 < q) (hfq : < ) :
∫⁻ (a : α), f a‖₊ ^ qμ <
theorem MeasureTheory.lintegral_rpow_nnnorm_lt_top_of_snorm_lt_top {α : Type u_1} {F : Type u_3} {m0 : } {p : ENNReal} {μ : } {f : αF} (hp_ne_zero : p 0) (hp_ne_top : p ) (hfp : < ) :
∫⁻ (a : α), f a‖₊ ^ p.toRealμ <
theorem MeasureTheory.snorm_lt_top_iff_lintegral_rpow_nnnorm_lt_top {α : Type u_1} {F : Type u_3} {m0 : } {p : ENNReal} {μ : } {f : αF} (hp_ne_zero : p 0) (hp_ne_top : p ) :
< ∫⁻ (a : α), f a‖₊ ^ p.toRealμ <
@[simp]
theorem MeasureTheory.snorm'_exponent_zero {α : Type u_1} {F : Type u_3} {m0 : } {μ : } {f : αF} :
= 1
@[simp]
theorem MeasureTheory.snorm_exponent_zero {α : Type u_1} {F : Type u_3} {m0 : } {μ : } {f : αF} :
= 0
@[simp]
theorem MeasureTheory.memℒp_zero_iff_aestronglyMeasurable {α : Type u_1} {E : Type u_2} {m0 : } {μ : } {f : αE} :
@[simp]
theorem MeasureTheory.snorm'_zero {α : Type u_1} {F : Type u_3} {m0 : } {q : } {μ : } (hp0_lt : 0 < q) :
= 0
@[simp]
theorem MeasureTheory.snorm'_zero' {α : Type u_1} {F : Type u_3} {m0 : } {q : } {μ : } (hq0_ne : q 0) (hμ : μ 0) :
= 0
@[simp]
theorem MeasureTheory.snormEssSup_zero {α : Type u_1} {F : Type u_3} {m0 : } {μ : } :
@[simp]
theorem MeasureTheory.snorm_zero {α : Type u_1} {F : Type u_3} {m0 : } {p : ENNReal} {μ : } :
= 0
@[simp]
theorem MeasureTheory.snorm_zero' {α : Type u_1} {F : Type u_3} {m0 : } {p : ENNReal} {μ : } :
MeasureTheory.snorm (fun (x : α) => 0) p μ = 0
theorem MeasureTheory.zero_memℒp {α : Type u_1} {E : Type u_2} {m0 : } {p : ENNReal} {μ : } :
theorem MeasureTheory.zero_mem_ℒp' {α : Type u_1} {E : Type u_2} {m0 : } {p : ENNReal} {μ : } :
MeasureTheory.Memℒp (fun (x : α) => 0) p μ
theorem MeasureTheory.snorm'_measure_zero_of_pos {α : Type u_1} {F : Type u_3} {q : } [] {f : αF} (hq_pos : 0 < q) :
= 0
theorem MeasureTheory.snorm'_measure_zero_of_exponent_zero {α : Type u_1} {F : Type u_3} [] {f : αF} :
= 1
theorem MeasureTheory.snorm'_measure_zero_of_neg {α : Type u_1} {F : Type u_3} {q : } [] {f : αF} (hq_neg : q < 0) :
@[simp]
theorem MeasureTheory.snormEssSup_measure_zero {α : Type u_1} {F : Type u_3} [] {f : αF} :
@[simp]
theorem MeasureTheory.snorm_measure_zero {α : Type u_1} {F : Type u_3} {p : ENNReal} [] {f : αF} :
= 0
@[simp]
theorem MeasureTheory.snorm'_neg {α : Type u_1} {F : Type u_3} {m0 : } {q : } {μ : } {f : αF} :
=
@[simp]
theorem MeasureTheory.snorm_neg {α : Type u_1} {F : Type u_3} {m0 : } {p : ENNReal} {μ : } {f : αF} :
theorem MeasureTheory.Memℒp.neg {α : Type u_1} {E : Type u_2} {m0 : } {p : ENNReal} {μ : } {f : αE} (hf : ) :
theorem MeasureTheory.memℒp_neg_iff {α : Type u_1} {E : Type u_2} {m0 : } {p : ENNReal} {μ : } {f : αE} :
theorem MeasureTheory.snorm'_const {α : Type u_1} {F : Type u_3} {m0 : } {q : } {μ : } (c : F) (hq_pos : 0 < q) :
MeasureTheory.snorm' (fun (x : α) => c) q μ = c‖₊ * μ Set.univ ^ (1 / q)
theorem MeasureTheory.snorm'_const' {α : Type u_1} {F : Type u_3} {m0 : } {q : } {μ : } (c : F) (hc_ne_zero : c 0) (hq_ne_zero : q 0) :
MeasureTheory.snorm' (fun (x : α) => c) q μ = c‖₊ * μ Set.univ ^ (1 / q)
theorem MeasureTheory.snormEssSup_const {α : Type u_1} {F : Type u_3} {m0 : } {μ : } (c : F) (hμ : μ 0) :
MeasureTheory.snormEssSup (fun (x : α) => c) μ = c‖₊
theorem MeasureTheory.snorm'_const_of_isProbabilityMeasure {α : Type u_1} {F : Type u_3} {m0 : } {q : } {μ : } (c : F) (hq_pos : 0 < q) :
MeasureTheory.snorm' (fun (x : α) => c) q μ = c‖₊
theorem MeasureTheory.snorm_const {α : Type u_1} {F : Type u_3} {m0 : } {p : ENNReal} {μ : } (c : F) (h0 : p 0) (hμ : μ 0) :
MeasureTheory.snorm (fun (x : α) => c) p μ = c‖₊ * μ Set.univ ^ (1 / p.toReal)
theorem MeasureTheory.snorm_const' {α : Type u_1} {F : Type u_3} {m0 : } {p : ENNReal} {μ : } (c : F) (h0 : p 0) (h_top : p ) :
MeasureTheory.snorm (fun (x : α) => c) p μ = c‖₊ * μ Set.univ ^ (1 / p.toReal)
theorem MeasureTheory.snorm_const_lt_top_iff {α : Type u_1} {F : Type u_3} {m0 : } {μ : } {p : ENNReal} {c : F} (hp_ne_zero : p 0) (hp_ne_top : p ) :
MeasureTheory.snorm (fun (x : α) => c) p μ < c = 0 μ Set.univ <
theorem MeasureTheory.memℒp_const {α : Type u_1} {E : Type u_2} {m0 : } {p : ENNReal} {μ : } (c : E) :
MeasureTheory.Memℒp (fun (x : α) => c) p μ
theorem MeasureTheory.memℒp_top_const {α : Type u_1} {E : Type u_2} {m0 : } {μ : } (c : E) :
MeasureTheory.Memℒp (fun (x : α) => c) μ
theorem MeasureTheory.memℒp_const_iff {α : Type u_1} {E : Type u_2} {m0 : } {μ : } {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.snorm'_mono_nnnorm_ae {α : Type u_1} {F : Type u_3} {G : Type u_4} {m0 : } {q : } {μ : } {f : αF} {g : αG} (hq : 0 q) (h : ∀ᵐ (x : α) ∂μ, f x‖₊ g x‖₊) :
theorem MeasureTheory.snorm'_mono_ae {α : Type u_1} {F : Type u_3} {G : Type u_4} {m0 : } {q : } {μ : } {f : αF} {g : αG} (hq : 0 q) (h : ∀ᵐ (x : α) ∂μ, f x g x) :
theorem MeasureTheory.snorm'_congr_nnnorm_ae {α : Type u_1} {F : Type u_3} {m0 : } {q : } {μ : } {f : αF} {g : αF} (hfg : ∀ᵐ (x : α) ∂μ, f x‖₊ = g x‖₊) :
=
theorem MeasureTheory.snorm'_congr_norm_ae {α : Type u_1} {F : Type u_3} {m0 : } {q : } {μ : } {f : αF} {g : αF} (hfg : ∀ᵐ (x : α) ∂μ, f x = g x) :
=
theorem MeasureTheory.snorm'_congr_ae {α : Type u_1} {F : Type u_3} {m0 : } {q : } {μ : } {f : αF} {g : αF} (hfg : ) :
=
theorem MeasureTheory.snormEssSup_congr_ae {α : Type u_1} {F : Type u_3} {m0 : } {μ : } {f : αF} {g : αF} (hfg : ) :
theorem MeasureTheory.snormEssSup_mono_nnnorm_ae {α : Type u_1} {F : Type u_3} {m0 : } {μ : } {f : αF} {g : αF} (hfg : ∀ᵐ (x : α) ∂μ, f x‖₊ g x‖₊) :
theorem MeasureTheory.snorm_mono_nnnorm_ae {α : Type u_1} {F : Type u_3} {G : Type u_4} {m0 : } {p : ENNReal} {μ : } {f : αF} {g : αG} (h : ∀ᵐ (x : α) ∂μ, f x‖₊ g x‖₊) :
theorem MeasureTheory.snorm_mono_ae {α : Type u_1} {F : Type u_3} {G : Type u_4} {m0 : } {p : ENNReal} {μ : } {f : αF} {g : αG} (h : ∀ᵐ (x : α) ∂μ, f x g x) :
theorem MeasureTheory.snorm_mono_ae_real {α : Type u_1} {F : Type u_3} {m0 : } {p : ENNReal} {μ : } {f : αF} {g : α} (h : ∀ᵐ (x : α) ∂μ, f x g x) :
theorem MeasureTheory.snorm_mono_nnnorm {α : Type u_1} {F : Type u_3} {G : Type u_4} {m0 : } {p : ENNReal} {μ : } {f : αF} {g : αG} (h : ∀ (x : α), f x‖₊ g x‖₊) :
theorem MeasureTheory.snorm_mono {α : Type u_1} {F : Type u_3} {G : Type u_4} {m0 : } {p : ENNReal} {μ : } {f : αF} {g : αG} (h : ∀ (x : α), f x g x) :
theorem MeasureTheory.snorm_mono_real {α : Type u_1} {F : Type u_3} {m0 : } {p : ENNReal} {μ : } {f : αF} {g : α} (h : ∀ (x : α), f x g x) :
theorem MeasureTheory.snormEssSup_le_of_ae_nnnorm_bound {α : Type u_1} {F : Type u_3} {m0 : } {μ : } {f : αF} {C : NNReal} (hfC : ∀ᵐ (x : α) ∂μ, f x‖₊ C) :
theorem MeasureTheory.snormEssSup_le_of_ae_bound {α : Type u_1} {F : Type u_3} {m0 : } {μ : } {f : αF} {C : } (hfC : ∀ᵐ (x : α) ∂μ, f x C) :
theorem MeasureTheory.snormEssSup_lt_top_of_ae_nnnorm_bound {α : Type u_1} {F : Type u_3} {m0 : } {μ : } {f : αF} {C : NNReal} (hfC : ∀ᵐ (x : α) ∂μ, f x‖₊ C) :
theorem MeasureTheory.snormEssSup_lt_top_of_ae_bound {α : Type u_1} {F : Type u_3} {m0 : } {μ : } {f : αF} {C : } (hfC : ∀ᵐ (x : α) ∂μ, f x C) :
theorem MeasureTheory.snorm_le_of_ae_nnnorm_bound {α : Type u_1} {F : Type u_3} {m0 : } {p : ENNReal} {μ : } {f : αF} {C : NNReal} (hfC : ∀ᵐ (x : α) ∂μ, f x‖₊ C) :
C μ Set.univ ^ p.toReal⁻¹
theorem MeasureTheory.snorm_le_of_ae_bound {α : Type u_1} {F : Type u_3} {m0 : } {p : ENNReal} {μ : } {f : αF} {C : } (hfC : ∀ᵐ (x : α) ∂μ, f x C) :
μ Set.univ ^ p.toReal⁻¹ *
theorem MeasureTheory.snorm_congr_nnnorm_ae {α : Type u_1} {F : Type u_3} {G : Type u_4} {m0 : } {p : ENNReal} {μ : } {f : αF} {g : αG} (hfg : ∀ᵐ (x : α) ∂μ, f x‖₊ = g x‖₊) :
=
theorem MeasureTheory.snorm_congr_norm_ae {α : Type u_1} {F : Type u_3} {G : Type u_4} {m0 : } {p : ENNReal} {μ : } {f : αF} {g : αG} (hfg : ∀ᵐ (x : α) ∂μ, f x = g x) :
=
theorem MeasureTheory.snorm_indicator_sub_indicator {α : Type u_1} {E : Type u_2} {m0 : } {p : ENNReal} {μ : } (s : Set α) (t : Set α) (f : αE) :
@[simp]
theorem MeasureTheory.snorm'_norm {α : Type u_1} {F : Type u_3} {m0 : } {q : } {μ : } {f : αF} :
MeasureTheory.snorm' (fun (a : α) => f a) q μ =
@[simp]
theorem MeasureTheory.snorm_norm {α : Type u_1} {F : Type u_3} {m0 : } {p : ENNReal} {μ : } (f : αF) :
MeasureTheory.snorm (fun (x : α) => f x) p μ =
theorem MeasureTheory.snorm'_norm_rpow {α : Type u_1} {F : Type u_3} {m0 : } {μ : } (f : αF) (p : ) (q : ) (hq_pos : 0 < q) :
MeasureTheory.snorm' (fun (x : α) => f x ^ q) p μ = MeasureTheory.snorm' f (p * q) μ ^ q
theorem MeasureTheory.snorm_norm_rpow {α : Type u_1} {F : Type u_3} {m0 : } {p : ENNReal} {q : } {μ : } (f : αF) (hq_pos : 0 < q) :
MeasureTheory.snorm (fun (x : α) => f x ^ q) p μ = MeasureTheory.snorm f () μ ^ q
theorem MeasureTheory.snorm_congr_ae {α : Type u_1} {F : Type u_3} {m0 : } {p : ENNReal} {μ : } {f : αF} {g : αF} (hfg : ) :
=
theorem MeasureTheory.memℒp_congr_ae {α : Type u_1} {E : Type u_2} {m0 : } {p : ENNReal} {μ : } {f : αE} {g : αE} (hfg : ) :
theorem MeasureTheory.Memℒp.ae_eq {α : Type u_1} {E : Type u_2} {m0 : } {p : ENNReal} {μ : } {f : αE} {g : αE} (hfg : ) (hf_Lp : ) :
theorem MeasureTheory.Memℒp.of_le {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : } {p : ENNReal} {μ : } {f : αE} {g : αF} (hg : ) (hf : ) (hfg : ∀ᵐ (x : α) ∂μ, f x g x) :
theorem MeasureTheory.Memℒp.mono {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : } {p : ENNReal} {μ : } {f : αE} {g : αF} (hg : ) (hf : ) (hfg : ∀ᵐ (x : α) ∂μ, f x g x) :

Alias of MeasureTheory.Memℒp.of_le.

theorem MeasureTheory.Memℒp.mono' {α : Type u_1} {E : Type u_2} {m0 : } {p : ENNReal} {μ : } {f : αE} {g : α} (hg : ) (hf : ) (h : ∀ᵐ (a : α) ∂μ, f a g a) :
theorem MeasureTheory.Memℒp.congr_norm {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : } {p : ENNReal} {μ : } {f : αE} {g : αF} (hf : ) (hg : ) (h : ∀ᵐ (a : α) ∂μ, f a = g a) :
theorem MeasureTheory.memℒp_congr_norm {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : } {p : ENNReal} {μ : } {f : αE} {g : αF} (hf : ) (hg : ) (h : ∀ᵐ (a : α) ∂μ, f a = g a) :
theorem MeasureTheory.memℒp_top_of_bound {α : Type u_1} {E : Type u_2} {m0 : } {μ : } {f : αE} (hf : ) (C : ) (hfC : ∀ᵐ (x : α) ∂μ, f x C) :
theorem MeasureTheory.Memℒp.of_bound {α : Type u_1} {E : Type u_2} {m0 : } {p : ENNReal} {μ : } {f : αE} (hf : ) (C : ) (hfC : ∀ᵐ (x : α) ∂μ, f x C) :
theorem MeasureTheory.snorm'_mono_measure {α : Type u_1} {F : Type u_3} {m0 : } {q : } {μ : } {ν : } (f : αF) (hμν : ν μ) (hq : 0 q) :
theorem MeasureTheory.snormEssSup_mono_measure {α : Type u_1} {F : Type u_3} {m0 : } {μ : } {ν : } (f : αF) (hμν : ) :
theorem MeasureTheory.snorm_mono_measure {α : Type u_1} {F : Type u_3} {m0 : } {p : ENNReal} {μ : } {ν : } (f : αF) (hμν : ν μ) :
theorem MeasureTheory.Memℒp.mono_measure {α : Type u_1} {E : Type u_2} {m0 : } {p : ENNReal} {μ : } {ν : } {f : αE} (hμν : ν μ) (hf : ) :
theorem MeasureTheory.snorm_restrict_le {α : Type u_1} {F : Type u_3} {m0 : } (f : αF) (p : ENNReal) (μ : ) (s : Set α) :
MeasureTheory.snorm f p (μ.restrict s)
theorem MeasureTheory.Memℒp.restrict {α : Type u_1} {E : Type u_2} {m0 : } {p : ENNReal} {μ : } (s : Set α) {f : αE} (hf : ) :
MeasureTheory.Memℒp f p (μ.restrict s)
theorem MeasureTheory.snorm'_smul_measure {α : Type u_1} {F : Type u_3} {m0 : } {μ : } {p : } (hp : 0 p) {f : αF} (c : ENNReal) :
MeasureTheory.snorm' f p (c μ) = c ^ (1 / p) *
theorem MeasureTheory.snormEssSup_smul_measure {α : Type u_1} {F : Type u_3} {m0 : } {μ : } {f : αF} {c : ENNReal} (hc : c 0) :
theorem MeasureTheory.snorm_smul_measure_of_ne_zero {α : Type u_1} {F : Type u_3} {m0 : } {μ : } {p : ENNReal} {f : αF} {c : ENNReal} (hc : c 0) :
MeasureTheory.snorm f p (c μ) = c ^ (1 / p).toReal
theorem MeasureTheory.snorm_smul_measure_of_ne_top {α : Type u_1} {F : Type u_3} {m0 : } {μ : } {p : ENNReal} (hp_ne_top : p ) {f : αF} (c : ENNReal) :
MeasureTheory.snorm f p (c μ) = c ^ (1 / p).toReal
theorem MeasureTheory.snorm_one_smul_measure {α : Type u_1} {F : Type u_3} {m0 : } {μ : } {f : αF} (c : ENNReal) :
MeasureTheory.snorm f 1 (c μ) = c *
theorem MeasureTheory.Memℒp.of_measure_le_smul {α : Type u_1} {E : Type u_2} {m0 : } {p : ENNReal} {μ : } {μ' : } (c : ENNReal) (hc : c ) (hμ'_le : μ' c μ) {f : αE} (hf : ) :
theorem MeasureTheory.Memℒp.smul_measure {α : Type u_1} {E : Type u_2} {m0 : } {p : ENNReal} {μ : } {f : αE} {c : ENNReal} (hf : ) (hc : c ) :
theorem MeasureTheory.snorm_one_add_measure {α : Type u_1} {F : Type u_3} {m0 : } (f : αF) (μ : ) (ν : ) :
MeasureTheory.snorm f 1 (μ + ν) = +
theorem MeasureTheory.snorm_le_add_measure_right {α : Type u_1} {F : Type u_3} {m0 : } (f : αF) (μ : ) (ν : ) {p : ENNReal} :
theorem MeasureTheory.snorm_le_add_measure_left {α : Type u_1} {F : Type u_3} {m0 : } (f : αF) (μ : ) (ν : ) {p : ENNReal} :
theorem MeasureTheory.Memℒp.left_of_add_measure {α : Type u_1} {E : Type u_2} {m0 : } {p : ENNReal} {μ : } {ν : } {f : αE} (h : MeasureTheory.Memℒp f p (μ + ν)) :
theorem MeasureTheory.Memℒp.right_of_add_measure {α : Type u_1} {E : Type u_2} {m0 : } {p : ENNReal} {μ : } {ν : } {f : αE} (h : MeasureTheory.Memℒp f p (μ + ν)) :
theorem MeasureTheory.Memℒp.norm {α : Type u_1} {E : Type u_2} {m0 : } {p : ENNReal} {μ : } {f : αE} (h : ) :
MeasureTheory.Memℒp (fun (x : α) => f x) p μ
theorem MeasureTheory.memℒp_norm_iff {α : Type u_1} {E : Type u_2} {m0 : } {p : ENNReal} {μ : } {f : αE} (hf : ) :
MeasureTheory.Memℒp (fun (x : α) => f x) p μ
theorem MeasureTheory.snorm'_eq_zero_of_ae_zero {α : Type u_1} {F : Type u_3} {m0 : } {q : } {μ : } {f : αF} (hq0_lt : 0 < q) (hf_zero : ) :
= 0
theorem MeasureTheory.snorm'_eq_zero_of_ae_zero' {α : Type u_1} {F : Type u_3} {m0 : } {q : } {μ : } (hq0_ne : q 0) (hμ : μ 0) {f : αF} (hf_zero : ) :
= 0
theorem MeasureTheory.ae_eq_zero_of_snorm'_eq_zero {α : Type u_1} {E : Type u_2} {m0 : } {q : } {μ : } {f : αE} (hq0 : 0 q) (hf : ) (h : = 0) :
theorem MeasureTheory.snorm'_eq_zero_iff {α : Type u_1} {E : Type u_2} {m0 : } {q : } {μ : } (hq0_lt : 0 < q) {f : αE} (hf : ) :
= 0
theorem MeasureTheory.coe_nnnorm_ae_le_snormEssSup {α : Type u_1} {F : Type u_3} :
∀ {x : } (f : αF) (μ : ), ∀ᵐ (x_1 : α) ∂μ, f x_1‖₊
@[simp]
theorem MeasureTheory.snormEssSup_eq_zero_iff {α : Type u_1} {F : Type u_3} {m0 : } {μ : } {f : αF} :
theorem MeasureTheory.snorm_eq_zero_iff {α : Type u_1} {E : Type u_2} {m0 : } {p : ENNReal} {μ : } {f : αE} (hf : ) (h0 : p 0) :
= 0
theorem MeasureTheory.ae_le_snormEssSup {α : Type u_1} {F : Type u_3} {m0 : } {μ : } {f : αF} :
∀ᵐ (y : α) ∂μ, f y‖₊
theorem MeasureTheory.meas_snormEssSup_lt {α : Type u_1} {F : Type u_3} {m0 : } {μ : } {f : αF} :
μ {y : α | < f y‖₊} = 0
theorem MeasureTheory.snormEssSup_piecewise {α : Type u_1} {E : Type u_2} {m0 : } {μ : } {s : Set α} (f : αE) (g : αE) [DecidablePred fun (x : α) => x s] (hs : ) :
= max (MeasureTheory.snormEssSup f (μ.restrict s)) (MeasureTheory.snormEssSup g (μ.restrict s))
theorem MeasureTheory.snorm_top_piecewise {α : Type u_1} {E : Type u_2} {m0 : } {μ : } {s : Set α} (f : αE) (g : αE) [DecidablePred fun (x : α) => x s] (hs : ) :
MeasureTheory.snorm () μ = max (MeasureTheory.snorm f (μ.restrict s)) (MeasureTheory.snorm g (μ.restrict s))
theorem MeasureTheory.snormEssSup_map_measure {α : Type u_1} {E : Type u_2} {m0 : } {μ : } {β : Type u_5} {mβ : } {f : αβ} {g : βE} (hg : ) (hf : ) :
theorem MeasureTheory.snorm_map_measure {α : Type u_1} {E : Type u_2} {m0 : } {p : ENNReal} {μ : } {β : Type u_5} {mβ : } {f : αβ} {g : βE} (hg : ) (hf : ) :
theorem MeasureTheory.memℒp_map_measure_iff {α : Type u_1} {E : Type u_2} {m0 : } {p : ENNReal} {μ : } {β : Type u_5} {mβ : } {f : αβ} {g : βE} (hg : ) (hf : ) :
theorem MeasureTheory.Memℒp.comp_of_map {α : Type u_1} {E : Type u_2} {m0 : } {p : ENNReal} {μ : } {β : Type u_5} {mβ : } {f : αβ} {g : βE} (hg : ) (hf : ) :
theorem MeasureTheory.snorm_comp_measurePreserving {α : Type u_1} {E : Type u_2} {m0 : } {p : ENNReal} {μ : } {β : Type u_5} {mβ : } {f : αβ} {g : βE} {ν : } (hg : ) (hf : ) :
theorem MeasureTheory.AEEqFun.snorm_compMeasurePreserving {α : Type u_1} {E : Type u_2} {m0 : } {p : ENNReal} {μ : } {β : Type u_5} {mβ : } {f : αβ} {ν : } (g : β →ₘ[ν] E) (hf : ) :
= MeasureTheory.snorm (g) p ν
theorem MeasureTheory.Memℒp.comp_measurePreserving {α : Type u_1} {E : Type u_2} {m0 : } {p : ENNReal} {μ : } {β : Type u_5} {mβ : } {f : αβ} {g : βE} {ν : } (hg : ) (hf : ) :
theorem MeasurableEmbedding.snormEssSup_map_measure {α : Type u_1} {F : Type u_3} {m0 : } {μ : } {β : Type u_5} {mβ : } {f : αβ} {g : βF} (hf : ) :
theorem MeasurableEmbedding.snorm_map_measure {α : Type u_1} {F : Type u_3} {m0 : } {p : ENNReal} {μ : } {β : Type u_5} {mβ : } {f : αβ} {g : βF} (hf : ) :
theorem MeasurableEmbedding.memℒp_map_measure_iff {α : Type u_1} {F : Type u_3} {m0 : } {p : ENNReal} {μ : } {β : Type u_5} {mβ : } {f : αβ} {g : βF} (hf : ) :
theorem MeasurableEquiv.memℒp_map_measure_iff {α : Type u_1} {F : Type u_3} {m0 : } {p : ENNReal} {μ : } {β : Type u_5} {mβ : } (f : α ≃ᵐ β) {g : βF} :
theorem MeasureTheory.snorm'_le_nnreal_smul_snorm'_of_ae_le_mul {α : Type u_1} {F : Type u_3} {G : Type u_4} {m0 : } {μ : } {f : αF} {g : αG} {c : NNReal} (h : ∀ᵐ (x : α) ∂μ, f x‖₊ c * g x‖₊) {p : } (hp : 0 < p) :
c
theorem MeasureTheory.snormEssSup_le_nnreal_smul_snormEssSup_of_ae_le_mul {α : Type u_1} {F : Type u_3} {G : Type u_4} {m0 : } {μ : } {f : αF} {g : αG} {c : NNReal} (h : ∀ᵐ (x : α) ∂μ, f x‖₊ c * g x‖₊) :
theorem MeasureTheory.snorm_le_nnreal_smul_snorm_of_ae_le_mul {α : Type u_1} {F : Type u_3} {G : Type u_4} {m0 : } {μ : } {f : αF} {g : αG} {c : NNReal} (h : ∀ᵐ (x : α) ∂μ, f x‖₊ c * g x‖₊) (p : ENNReal) :
c
theorem MeasureTheory.snorm_eq_zero_and_zero_of_ae_le_mul_neg {α : Type u_1} {F : Type u_3} {G : Type u_4} {m0 : } {μ : } {f : αF} {g : αG} {c : } (h : ∀ᵐ (x : α) ∂μ, f x c * g x) (hc : c < 0) (p : ENNReal) :
= 0 = 0

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

theorem MeasureTheory.snorm_le_mul_snorm_of_ae_le_mul {α : Type u_1} {F : Type u_3} {G : Type u_4} {m0 : } {μ : } {f : αF} {g : αG} {c : } (h : ∀ᵐ (x : α) ∂μ, f x c * g x) (p : ENNReal) :
theorem MeasureTheory.Memℒp.of_nnnorm_le_mul {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : } {p : ENNReal} {μ : } {f : αE} {g : αF} {c : NNReal} (hg : ) (hf : ) (hfg : ∀ᵐ (x : α) ∂μ, f x‖₊ c * g x‖₊) :
theorem MeasureTheory.Memℒp.of_le_mul {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : } {p : ENNReal} {μ : } {f : αE} {g : αF} {c : } (hg : ) (hf : ) (hfg : ∀ᵐ (x : α) ∂μ, f x c * g x) :

### Bounded actions by normed rings #

In this section we show inequalities on the norm.

theorem MeasureTheory.snorm'_const_smul_le {α : Type u_1} {F : Type u_3} {m0 : } {q : } {μ : } {𝕜 : Type u_5} [] [] [] (c : 𝕜) (f : αF) (hq_pos : 0 < q) :
theorem MeasureTheory.snormEssSup_const_smul_le {α : Type u_1} {F : Type u_3} {m0 : } {μ : } {𝕜 : Type u_5} [] [] [] (c : 𝕜) (f : αF) :
theorem MeasureTheory.snorm_const_smul_le {α : Type u_1} {F : Type u_3} {m0 : } {p : ENNReal} {μ : } {𝕜 : Type u_5} [] [] [] (c : 𝕜) (f : αF) :
theorem MeasureTheory.Memℒp.const_smul {α : Type u_1} {E : Type u_2} {m0 : } {p : ENNReal} {μ : } {𝕜 : Type u_5} [] [] [] {f : αE} (hf : ) (c : 𝕜) :
theorem MeasureTheory.Memℒp.const_mul {α : Type u_1} {m0 : } {p : ENNReal} {μ : } {R : Type u_6} [] {f : αR} (hf : ) (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.snorm'_const_smul {α : Type u_1} {F : Type u_3} {m0 : } {q : } {μ : } {𝕜 : Type u_5} [Module 𝕜 F] [] {f : αF} (c : 𝕜) (hq_pos : 0 < q) :
theorem MeasureTheory.snormEssSup_const_smul {α : Type u_1} {F : Type u_3} {m0 : } {μ : } {𝕜 : Type u_5} [Module 𝕜 F] [] (c : 𝕜) (f : αF) :
theorem MeasureTheory.snorm_const_smul {α : Type u_1} {F : Type u_3} {m0 : } {p : ENNReal} {μ : } {𝕜 : Type u_5} [Module 𝕜 F] [] (c : 𝕜) (f : αF) :
theorem MeasureTheory.snorm_indicator_ge_of_bdd_below {α : Type u_1} {F : Type u_3} {m0 : } {p : ENNReal} {μ : } (hp : p 0) (hp' : p ) {f : αF} (C : NNReal) {s : Set α} (hs : ) (hf : ∀ᵐ (x : α) ∂μ, x sC ‖₊) :
C μ s ^ (1 / p.toReal) MeasureTheory.snorm () p μ
theorem MeasureTheory.Memℒp.re {α : Type u_1} {m0 : } {p : ENNReal} {μ : } {𝕜 : Type u_5} [] {f : α𝕜} (hf : ) :
MeasureTheory.Memℒp (fun (x : α) => RCLike.re (f x)) p μ
theorem MeasureTheory.Memℒp.im {α : Type u_1} {m0 : } {p : ENNReal} {μ : } {𝕜 : Type u_5} [] {f : α𝕜} (hf : ) :
MeasureTheory.Memℒp (fun (x : α) => RCLike.im (f x)) p μ
theorem MeasureTheory.ae_bdd_liminf_atTop_rpow_of_snorm_bdd {α : Type u_1} {E : Type u_2} {m0 : } {μ : } [] {R : NNReal} {p : ENNReal} {f : αE} (hfmeas : ∀ (n : ), Measurable (f n)) (hbdd : ∀ (n : ), MeasureTheory.snorm (f n) p μ R) :
∀ᵐ (x : α) ∂μ, Filter.liminf (fun (n : ) => f n x‖₊ ^ p.toReal) Filter.atTop <
theorem MeasureTheory.ae_bdd_liminf_atTop_of_snorm_bdd {α : Type u_1} {E : Type u_2} {m0 : } {μ : } [] {R : NNReal} {p : ENNReal} (hp : p 0) {f : αE} (hfmeas : ∀ (n : ), Measurable (f n)) (hbdd : ∀ (n : ), MeasureTheory.snorm (f n) p μ R) :
∀ᵐ (x : α) ∂μ, Filter.liminf (fun (n : ) => f n x‖₊) Filter.atTop <
theorem Continuous.memℒp_top_of_hasCompactSupport {E : Type u_2} {X : Type u_5} [] [] {f : XE} (hf : ) (h'f : ) (μ : ) :

A continuous function with compact support belongs to L^∞.