# Documentation

Mathlib.MeasureTheory.Function.LpSeminorm

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

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

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

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

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} :
=
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‖₊ ^ μ) ^ ()
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 = ∞.

Instances For
theorem MeasureTheory.memℒp_def {E : Type u_2} {α : Type u_5} :
∀ {x : } (f : αE) (p : ENNReal) (μ : ),
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‖₊ ^ μ <
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‖₊ ^ μ <
@[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
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) :
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 ^ ()
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 ^ ()
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) :
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 ^ ()⁻¹
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 ^ ()⁻¹ *
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.Memℒp.restrict {α : Type u_1} {E : Type u_2} {m0 : } {p : ENNReal} {μ : } (s : Set α) {f : αE} (hf : ) :
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) :
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) :
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 : ) :
theorem MeasureTheory.Memℒp.right_of_add_measure {α : Type u_1} {E : Type u_2} {m0 : } {p : ENNReal} {μ : } {ν : } {f : αE} (h : ) :
theorem MeasureTheory.Memℒp.norm {α : Type u_1} {E : Type u_2} {m0 : } {p : ENNReal} {μ : } {f : αE} (h : ) :
theorem MeasureTheory.memℒp_norm_iff {α : Type u_1} {E : Type u_2} {m0 : } {p : ENNReal} {μ : } {f : αE} (hf : ) :
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.snorm'_add_le {α : Type u_1} {E : Type u_2} {m0 : } {q : } {μ : } {f : αE} {g : αE} (hf : ) (hg : ) (hq1 : 1 q) :
theorem MeasureTheory.snorm'_add_le_of_le_one {α : Type u_1} {E : Type u_2} {m0 : } {q : } {μ : } {f : αE} {g : αE} (hf : ) (hq0 : 0 q) (hq1 : q 1) :
MeasureTheory.snorm' (f + g) q μ 2 ^ (1 / q - 1) * ( + )
theorem MeasureTheory.snormEssSup_add_le {α : Type u_1} {F : Type u_3} {m0 : } {μ : } {f : αF} {g : αF} :
theorem MeasureTheory.snorm_add_le {α : Type u_1} {E : Type u_2} {m0 : } {p : ENNReal} {μ : } {f : αE} {g : αE} (hf : ) (hg : ) (hp1 : 1 p) :

A constant for the inequality ‖f + g‖_{L^p} ≤ C * (‖f‖_{L^p} + ‖g‖_{L^p}). It is equal to 1 for p ≥ 1 or p = 0, and 2^(1/p-1) in the more tricky interval (0, 1).

Instances For
theorem MeasureTheory.snorm_add_le' {α : Type u_1} {E : Type u_2} {m0 : } {μ : } {f : αE} {g : αE} (hf : ) (hg : ) (p : ENNReal) :
MeasureTheory.snorm (f + g) p μ * ( + )
theorem MeasureTheory.exists_Lp_half {α : Type u_1} (E : Type u_2) {m0 : } (μ : ) (p : ENNReal) {δ : ENNReal} (hδ : δ 0) :
η, 0 < η ∀ (f g : αE), η ηMeasureTheory.snorm (f + g) p μ < δ

Technical lemma to control the addition of functions in L^p even for p < 1: Given δ > 0, there exists η such that two functions bounded by η in L^p have a sum bounded by δ. One could take η = δ / 2 for p ≥ 1, but the point of the lemma is that it works also for p < 1.

theorem MeasureTheory.snorm_sub_le' {α : Type u_1} {E : Type u_2} {m0 : } {μ : } {f : αE} {g : αE} (hf : ) (hg : ) (p : ENNReal) :
MeasureTheory.snorm (f - g) p μ * ( + )
theorem MeasureTheory.snorm_sub_le {α : Type u_1} {E : Type u_2} {m0 : } {p : ENNReal} {μ : } {f : αE} {g : αE} (hf : ) (hg : ) (hp : 1 p) :
theorem MeasureTheory.snorm_add_lt_top {α : Type u_1} {E : Type u_2} {m0 : } {p : ENNReal} {μ : } {f : αE} {g : αE} (hf : ) (hg : ) :
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_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'_trim {α : Type u_1} {E : Type u_2} {m : } {m0 : } {q : } {ν : } (hm : m m0) {f : αE} (hf : ) :
=
theorem MeasureTheory.limsup_trim {α : Type u_1} {m : } {m0 : } {ν : } (hm : m m0) {f : αENNReal} (hf : ) :
theorem MeasureTheory.essSup_trim {α : Type u_1} {m : } {m0 : } {ν : } (hm : m m0) {f : αENNReal} (hf : ) :
essSup f () = essSup f ν
theorem MeasureTheory.snormEssSup_trim {α : Type u_1} {E : Type u_2} {m : } {m0 : } {ν : } (hm : m m0) {f : αE} (hf : ) :
theorem MeasureTheory.snorm_trim {α : Type u_1} {E : Type u_2} {m : } {m0 : } {p : ENNReal} {ν : } (hm : m m0) {f : αE} (hf : ) :
=
theorem MeasureTheory.snorm_trim_ae {α : Type u_1} {E : Type u_2} {m : } {m0 : } {p : ENNReal} {ν : } (hm : m m0) {f : αE} (hf : ) :
=
theorem MeasureTheory.memℒp_of_memℒp_trim {α : Type u_1} {E : Type u_2} {m : } {m0 : } {p : ENNReal} {ν : } (hm : m m0) {f : αE} (hf : ) :
theorem MeasureTheory.snorm'_le_snorm'_mul_rpow_measure_univ {α : Type u_1} {E : Type u_2} {m0 : } {μ : } {p : } {q : } (hp0_lt : 0 < p) (hpq : p q) {f : αE} (hf : ) :
* μ Set.univ ^ (1 / p - 1 / q)
theorem MeasureTheory.snorm'_le_snormEssSup_mul_rpow_measure_univ {α : Type u_1} {F : Type u_3} {m0 : } {q : } {μ : } (hq_pos : 0 < q) {f : αF} :
* μ Set.univ ^ (1 / q)
theorem MeasureTheory.snorm_le_snorm_mul_rpow_measure_univ {α : Type u_1} {E : Type u_2} {m0 : } {μ : } {p : ENNReal} {q : ENNReal} (hpq : p q) {f : αE} (hf : ) :
* μ Set.univ ^ ( - )
theorem MeasureTheory.snorm'_le_snorm'_of_exponent_le {α : Type u_1} {E : Type u_2} {m : } {p : } {q : } (hp0_lt : 0 < p) (hpq : p q) (μ : ) {f : αE} (hf : ) :
theorem MeasureTheory.snorm'_le_snormEssSup {α : Type u_1} {F : Type u_3} {m0 : } {q : } {μ : } (hq_pos : 0 < q) {f : αF} :
theorem MeasureTheory.snorm_le_snorm_of_exponent_le {α : Type u_1} {E : Type u_2} {m0 : } {μ : } {p : ENNReal} {q : ENNReal} (hpq : p q) {f : αE} (hf : ) :
theorem MeasureTheory.snorm'_lt_top_of_snorm'_lt_top_of_exponent_le {α : Type u_1} {E : Type u_2} {m0 : } {μ : } {p : } {q : } {f : αE} (hf : ) (hfq_lt_top : < ) (hp_nonneg : 0 p) (hpq : p q) :
theorem MeasureTheory.pow_mul_meas_ge_le_snorm {α : Type u_1} {E : Type u_2} {m0 : } {p : ENNReal} (μ : ) {f : αE} (hp_ne_zero : p 0) (hp_ne_top : p ) (hf : ) (ε : ENNReal) :
(ε * μ {x | ε f x‖₊ ^ }) ^ ()
theorem MeasureTheory.mul_meas_ge_le_pow_snorm {α : Type u_1} {E : Type u_2} {m0 : } {p : ENNReal} (μ : ) {f : αE} (hp_ne_zero : p 0) (hp_ne_top : p ) (hf : ) (ε : ENNReal) :
ε * μ {x | ε f x‖₊ ^ }
theorem MeasureTheory.mul_meas_ge_le_pow_snorm' {α : Type u_1} {E : Type u_2} {m0 : } {p : ENNReal} (μ : ) {f : αE} (hp_ne_zero : p 0) (hp_ne_top : p ) (hf : ) (ε : ENNReal) :
* μ {x | ε f x‖₊}

A version of Markov's inequality using Lp-norms.

theorem MeasureTheory.meas_ge_le_mul_pow_snorm {α : Type u_1} {E : Type u_2} {m0 : } {p : ENNReal} (μ : ) {f : αE} (hp_ne_zero : p 0) (hp_ne_top : p ) (hf : ) {ε : ENNReal} (hε : ε 0) :
μ {x | ε f x‖₊} *
theorem MeasureTheory.Memℒp.memℒp_of_exponent_le {α : Type u_1} {E : Type u_2} {m0 : } {μ : } {p : ENNReal} {q : ENNReal} {f : αE} (hfq : ) (hpq : p q) :
theorem MeasureTheory.snorm'_sum_le {α : Type u_1} {E : Type u_2} {m0 : } {q : } {μ : } {ι : Type u_5} {f : ιαE} {s : } (hfs : ∀ (i : ι), i s) (hq1 : 1 q) :
MeasureTheory.snorm' (Finset.sum s fun i => f i) q μ Finset.sum s fun i => MeasureTheory.snorm' (f i) q μ
theorem MeasureTheory.snorm_sum_le {α : Type u_1} {E : Type u_2} {m0 : } {p : ENNReal} {μ : } {ι : Type u_5} {f : ιαE} {s : } (hfs : ∀ (i : ι), i s) (hp1 : 1 p) :
MeasureTheory.snorm (Finset.sum s fun i => f i) p μ Finset.sum s fun i => MeasureTheory.snorm (f i) p μ
theorem MeasureTheory.Memℒp.add {α : Type u_1} {E : Type u_2} {m0 : } {p : ENNReal} {μ : } {f : αE} {g : αE} (hf : ) (hg : ) :
theorem MeasureTheory.Memℒp.sub {α : Type u_1} {E : Type u_2} {m0 : } {p : ENNReal} {μ : } {f : αE} {g : αE} (hf : ) (hg : ) :
theorem MeasureTheory.memℒp_finset_sum {α : Type u_1} {E : Type u_2} {m0 : } {p : ENNReal} {μ : } {ι : Type u_5} (s : ) {f : ιαE} (hf : ∀ (i : ι), i sMeasureTheory.Memℒp (f i) p) :
MeasureTheory.Memℒp (fun a => Finset.sum s fun i => f i a) p
theorem MeasureTheory.memℒp_finset_sum' {α : Type u_1} {E : Type u_2} {m0 : } {p : ENNReal} {μ : } {ι : Type u_5} (s : ) {f : ιαE} (hf : ∀ (i : ι), i sMeasureTheory.Memℒp (f i) p) :
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) :
theorem MeasureTheory.snorm'_le_snorm'_mul_snorm' {α : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {m0 : } {μ : } {p : } {q : } {r : } {f : αE} (hf : ) {g : αF} (hg : ) (b : EFG) (h : ∀ᵐ (x : α) ∂μ, b (f x) (g x)‖₊ f x‖₊ * g x‖₊) (hp0_lt : 0 < p) (hpq : p < q) (hpqr : 1 / p = 1 / q + 1 / r) :
MeasureTheory.snorm' (fun x => b (f x) (g x)) p μ *
theorem MeasureTheory.snorm_le_snorm_top_mul_snorm {α : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {m0 : } {μ : } (p : ENNReal) (f : αE) {g : αF} (hg : ) (b : EFG) (h : ∀ᵐ (x : α) ∂μ, b (f x) (g x)‖₊ f x‖₊ * g x‖₊) :
MeasureTheory.snorm (fun x => b (f x) (g x)) p μ *
theorem MeasureTheory.snorm_le_snorm_mul_snorm_top {α : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {m0 : } {μ : } (p : ENNReal) {f : αE} (hf : ) (g : αF) (b : EFG) (h : ∀ᵐ (x : α) ∂μ, b (f x) (g x)‖₊ f x‖₊ * g x‖₊) :
MeasureTheory.snorm (fun x => b (f x) (g x)) p μ *
theorem MeasureTheory.snorm_le_snorm_mul_snorm_of_nnnorm {α : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {m0 : } {μ : } {p : ENNReal} {q : ENNReal} {r : ENNReal} {f : αE} (hf : ) {g : αF} (hg : ) (b : EFG) (h : ∀ᵐ (x : α) ∂μ, b (f x) (g x)‖₊ f x‖₊ * g x‖₊) (hpqr : 1 / p = 1 / q + 1 / r) :
MeasureTheory.snorm (fun x => b (f x) (g x)) p μ *

Hölder's inequality, as an inequality on the ℒp seminorm of an elementwise operation fun x => b (f x) (g x).

theorem MeasureTheory.snorm_le_snorm_mul_snorm'_of_norm {α : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {m0 : } {μ : } {p : ENNReal} {q : ENNReal} {r : ENNReal} {f : αE} (hf : ) {g : αF} (hg : ) (b : EFG) (h : ∀ᵐ (x : α) ∂μ, b (f x) (g x) f x * g x) (hpqr : 1 / p = 1 / q + 1 / r) :
MeasureTheory.snorm (fun x => b (f x) (g x)) p μ *

Hölder's inequality, as an inequality on the ℒp seminorm of an elementwise operation fun x => b (f x) (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
theorem MeasureTheory.snorm'_smul_le_mul_snorm' {α : Type u_1} {E : Type u_2} {m0 : } {μ : } {𝕜 : Type u_5} [] [] [] {p : } {q : } {r : } {f : αE} (hf : ) {φ : α𝕜} (hφ : ) (hp0_lt : 0 < p) (hpq : p < q) (hpqr : 1 / p = 1 / q + 1 / r) :
theorem MeasureTheory.snorm_smul_le_snorm_top_mul_snorm {α : Type u_1} {E : Type u_2} {m0 : } {μ : } {𝕜 : Type u_5} [] [] [] (p : ENNReal) {f : αE} (hf : ) (φ : α𝕜) :
theorem MeasureTheory.snorm_smul_le_snorm_mul_snorm_top {α : Type u_1} {E : Type u_2} {m0 : } {μ : } {𝕜 : Type u_5} [] [] [] (p : ENNReal) (f : αE) {φ : α𝕜} (hφ : ) :
theorem MeasureTheory.snorm_smul_le_mul_snorm {α : Type u_1} {E : Type u_2} {m0 : } {μ : } {𝕜 : Type u_5} [] [] [] {p : ENNReal} {q : ENNReal} {r : ENNReal} {f : αE} (hf : ) {φ : α𝕜} (hφ : ) (hpqr : 1 / p = 1 / q + 1 / r) :

Hölder's inequality, as an inequality on the ℒp seminorm of a scalar product φ • f.

theorem MeasureTheory.Memℒp.smul {α : Type u_1} {E : Type u_2} {m0 : } {μ : } {𝕜 : Type u_5} [] [] [] {p : ENNReal} {q : ENNReal} {r : ENNReal} {f : αE} {φ : α𝕜} (hf : ) (hφ : ) (hpqr : 1 / p = 1 / q + 1 / r) :
theorem MeasureTheory.Memℒp.smul_of_top_right {α : Type u_1} {E : Type u_2} {m0 : } {μ : } {𝕜 : Type u_5} [] [] [] {p : ENNReal} {f : αE} {φ : α𝕜} (hf : ) (hφ : ) :
theorem MeasureTheory.Memℒp.smul_of_top_left {α : Type u_1} {E : Type u_2} {m0 : } {μ : } {𝕜 : Type u_5} [] [] [] {p : ENNReal} {f : αE} {φ : α𝕜} (hf : ) (hφ : ) :

### 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 ^ () MeasureTheory.snorm () p μ
theorem MeasureTheory.Memℒp.re {α : Type u_1} {m0 : } {p : ENNReal} {μ : } {𝕜 : Type u_5} [] {f : α𝕜} (hf : ) :
MeasureTheory.Memℒp (fun x => IsROrC.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 => IsROrC.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‖₊ ^ ) 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^∞.