# mathlib3documentation

measure_theory.function.lp_seminorm

# ℒp space #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 `ess_sup ‖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.

• `snorm_ess_sup 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 `snorm_ess_sup 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 `snorm_ess_sup f μ`).

We also define a predicate `mem_ℒp f p μ`, requesting that a function is almost everywhere strongly 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 `snorm_ess_sup` when it makes sense, deduce it for `snorm`, and translate it in terms of `mem_ℒp`.

noncomputable def measure_theory.snorm' {α : Type u_1} {F : Type u_3} {m : measurable_space α} (f : α F) (q : ) (μ : measure_theory.measure α) :

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

Equations
noncomputable def measure_theory.snorm_ess_sup {α : Type u_1} {F : Type u_3} {m : measurable_space α} (f : α F) (μ : measure_theory.measure α) :

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

Equations
noncomputable def measure_theory.snorm {α : Type u_1} {F : Type u_3} {m : measurable_space α} (f : α F) (p : ennreal) (μ : measure_theory.measure α) :

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

Equations
theorem measure_theory.snorm_eq_snorm' {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} (hp_ne_zero : p 0) (hp_ne_top : p ) {f : α F} :
μ =
theorem measure_theory.snorm_eq_lintegral_rpow_nnnorm {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} (hp_ne_zero : p 0) (hp_ne_top : p ) {f : α F} :
μ = (∫⁻ (x : α), f x‖₊ ^ p.to_real μ) ^ (1 / p.to_real)
theorem measure_theory.snorm_one_eq_lintegral_nnnorm {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {μ : measure_theory.measure α} {f : α F} :
μ = ∫⁻ (x : α), f x‖₊ μ
@[simp]
theorem measure_theory.snorm_exponent_top {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {μ : measure_theory.measure α} {f : α F} :
def measure_theory.mem_ℒp {E : Type u_2} {α : Type u_1} {m : measurable_space α} (f : α E) (p : ennreal) (μ : . "volume_tac") :
Prop

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

Equations
theorem measure_theory.mem_ℒp.ae_strongly_measurable {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} {f : α E} {p : ennreal} (h : μ) :
theorem measure_theory.lintegral_rpow_nnnorm_eq_rpow_snorm' {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {q : } {μ : measure_theory.measure α} {f : α F} (hq0_lt : 0 < q) :
∫⁻ (a : α), f a‖₊ ^ q μ = ^ q
theorem measure_theory.mem_ℒp.snorm_lt_top {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f : α E} (hfp : μ) :
μ <
theorem measure_theory.mem_ℒp.snorm_ne_top {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f : α E} (hfp : μ) :
μ
theorem measure_theory.lintegral_rpow_nnnorm_lt_top_of_snorm'_lt_top {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {q : } {μ : measure_theory.measure α} {f : α F} (hq0_lt : 0 < q) (hfq : < ) :
∫⁻ (a : α), f a‖₊ ^ q μ <
theorem measure_theory.lintegral_rpow_nnnorm_lt_top_of_snorm_lt_top {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f : α F} (hp_ne_zero : p 0) (hp_ne_top : p ) (hfp : μ < ) :
theorem measure_theory.snorm_lt_top_iff_lintegral_rpow_nnnorm_lt_top {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f : α F} (hp_ne_zero : p 0) (hp_ne_top : p ) :
μ < ∫⁻ (a : α), f a‖₊ ^ p.to_real μ <
@[simp]
theorem measure_theory.snorm'_exponent_zero {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {μ : measure_theory.measure α} {f : α F} :
= 1
@[simp]
theorem measure_theory.snorm_exponent_zero {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {μ : measure_theory.measure α} {f : α F} :
μ = 0
@[simp]
theorem measure_theory.snorm'_zero {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {q : } {μ : measure_theory.measure α} (hp0_lt : 0 < q) :
= 0
@[simp]
theorem measure_theory.snorm'_zero' {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {q : } {μ : measure_theory.measure α} (hq0_ne : q 0) (hμ : μ 0) :
= 0
@[simp]
theorem measure_theory.snorm_ess_sup_zero {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {μ : measure_theory.measure α}  :
@[simp]
theorem measure_theory.snorm_zero {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α}  :
μ = 0
@[simp]
theorem measure_theory.snorm_zero' {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α}  :
measure_theory.snorm (λ (x : α), 0) p μ = 0
theorem measure_theory.zero_mem_ℒp {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α}  :
theorem measure_theory.zero_mem_ℒp' {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α}  :
measure_theory.mem_ℒp (λ (x : α), 0) p μ
theorem measure_theory.snorm'_measure_zero_of_pos {α : Type u_1} {F : Type u_3} {q : } {f : α F} (hq_pos : 0 < q) :
= 0
theorem measure_theory.snorm'_measure_zero_of_exponent_zero {α : Type u_1} {F : Type u_3} {f : α F} :
= 1
theorem measure_theory.snorm'_measure_zero_of_neg {α : Type u_1} {F : Type u_3} {q : } {f : α F} (hq_neg : q < 0) :
@[simp]
theorem measure_theory.snorm_ess_sup_measure_zero {α : Type u_1} {F : Type u_3} {f : α F} :
@[simp]
theorem measure_theory.snorm_measure_zero {α : Type u_1} {F : Type u_3} {p : ennreal} {f : α F} :
0 = 0
theorem measure_theory.snorm'_const {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {q : } {μ : measure_theory.measure α} (c : F) (hq_pos : 0 < q) :
measure_theory.snorm' (λ (x : α), c) q μ = c‖₊ * ^ (1 / q)
theorem measure_theory.snorm'_const' {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {q : } {μ : measure_theory.measure α} (c : F) (hc_ne_zero : c 0) (hq_ne_zero : q 0) :
measure_theory.snorm' (λ (x : α), c) q μ = c‖₊ * ^ (1 / q)
theorem measure_theory.snorm_ess_sup_const {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {μ : measure_theory.measure α} (c : F) (hμ : μ 0) :
theorem measure_theory.snorm'_const_of_is_probability_measure {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {q : } {μ : measure_theory.measure α} (c : F) (hq_pos : 0 < q)  :
measure_theory.snorm' (λ (x : α), c) q μ = c‖₊
theorem measure_theory.snorm_const {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} (c : F) (h0 : p 0) (hμ : μ 0) :
measure_theory.snorm (λ (x : α), c) p μ = c‖₊ * ^ (1 / p.to_real)
theorem measure_theory.snorm_const' {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} (c : F) (h0 : p 0) (h_top : p ) :
measure_theory.snorm (λ (x : α), c) p μ = c‖₊ * ^ (1 / p.to_real)
theorem measure_theory.snorm_const_lt_top_iff {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {μ : measure_theory.measure α} {p : ennreal} {c : F} (hp_ne_zero : p 0) (hp_ne_top : p ) :
measure_theory.snorm (λ (x : α), c) p μ < c = 0
theorem measure_theory.mem_ℒp_const {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} (c : E)  :
measure_theory.mem_ℒp (λ (a : α), c) p μ
theorem measure_theory.mem_ℒp_top_const {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} (c : E) :
measure_theory.mem_ℒp (λ (a : α), c) μ
theorem measure_theory.mem_ℒp_const_iff {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} {p : ennreal} {c : E} (hp_ne_zero : p 0) (hp_ne_top : p ) :
measure_theory.mem_ℒp (λ (x : α), c) p μ c = 0
theorem measure_theory.snorm'_mono_nnnorm_ae {α : Type u_1} {F : Type u_3} {G : Type u_4} {m0 : measurable_space α} {q : } {μ : measure_theory.measure α} {f : α F} {g : α G} (hq : 0 q) (h : ∀ᵐ (x : α) μ, f x‖₊ g x‖₊) :
theorem measure_theory.snorm'_mono_ae {α : Type u_1} {F : Type u_3} {G : Type u_4} {m0 : measurable_space α} {q : } {μ : measure_theory.measure α} {f : α F} {g : α G} (hq : 0 q) (h : ∀ᵐ (x : α) μ, f x g x) :
theorem measure_theory.snorm'_congr_nnnorm_ae {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {q : } {μ : measure_theory.measure α} {f g : α F} (hfg : ∀ᵐ (x : α) μ, f x‖₊ = g x‖₊) :
=
theorem measure_theory.snorm'_congr_norm_ae {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {q : } {μ : measure_theory.measure α} {f g : α F} (hfg : ∀ᵐ (x : α) μ, f x = g x) :
=
theorem measure_theory.snorm'_congr_ae {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {q : } {μ : measure_theory.measure α} {f g : α F} (hfg : f =ᵐ[μ] g) :
=
theorem measure_theory.snorm_ess_sup_congr_ae {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {μ : measure_theory.measure α} {f g : α F} (hfg : f =ᵐ[μ] g) :
theorem measure_theory.snorm_ess_sup_mono_nnnorm_ae {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {μ : measure_theory.measure α} {f g : α F} (hfg : ∀ᵐ (x : α) μ, f x‖₊ g x‖₊) :
theorem measure_theory.snorm_mono_nnnorm_ae {α : Type u_1} {F : Type u_3} {G : Type u_4} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f : α F} {g : α G} (h : ∀ᵐ (x : α) μ, f x‖₊ g x‖₊) :
μ μ
theorem measure_theory.snorm_mono_ae {α : Type u_1} {F : Type u_3} {G : Type u_4} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f : α F} {g : α G} (h : ∀ᵐ (x : α) μ, f x g x) :
μ μ
theorem measure_theory.snorm_mono_ae_real {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f : α F} {g : α } (h : ∀ᵐ (x : α) μ, f x g x) :
μ μ
theorem measure_theory.snorm_mono_nnnorm {α : Type u_1} {F : Type u_3} {G : Type u_4} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f : α F} {g : α G} (h : (x : α), f x‖₊ g x‖₊) :
μ μ
theorem measure_theory.snorm_mono {α : Type u_1} {F : Type u_3} {G : Type u_4} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f : α F} {g : α G} (h : (x : α), f x g x) :
μ μ
theorem measure_theory.snorm_mono_real {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f : α F} {g : α } (h : (x : α), f x g x) :
μ μ
theorem measure_theory.snorm_ess_sup_le_of_ae_nnnorm_bound {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {μ : measure_theory.measure α} {f : α F} {C : nnreal} (hfC : ∀ᵐ (x : α) μ, f x‖₊ C) :
theorem measure_theory.snorm_ess_sup_le_of_ae_bound {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {μ : measure_theory.measure α} {f : α F} {C : } (hfC : ∀ᵐ (x : α) μ, f x C) :
theorem measure_theory.snorm_ess_sup_lt_top_of_ae_nnnorm_bound {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {μ : measure_theory.measure α} {f : α F} {C : nnreal} (hfC : ∀ᵐ (x : α) μ, f x‖₊ C) :
theorem measure_theory.snorm_ess_sup_lt_top_of_ae_bound {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {μ : measure_theory.measure α} {f : α F} {C : } (hfC : ∀ᵐ (x : α) μ, f x C) :
theorem measure_theory.snorm_le_of_ae_nnnorm_bound {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f : α F} {C : nnreal} (hfC : ∀ᵐ (x : α) μ, f x‖₊ C) :
μ C ^ (p.to_real)⁻¹
theorem measure_theory.snorm_le_of_ae_bound {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f : α F} {C : } (hfC : ∀ᵐ (x : α) μ, f x C) :
μ ^ (p.to_real)⁻¹ *
theorem measure_theory.snorm_congr_nnnorm_ae {α : Type u_1} {F : Type u_3} {G : Type u_4} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f : α F} {g : α G} (hfg : ∀ᵐ (x : α) μ, f x‖₊ = g x‖₊) :
μ = μ
theorem measure_theory.snorm_congr_norm_ae {α : Type u_1} {F : Type u_3} {G : Type u_4} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f : α F} {g : α G} (hfg : ∀ᵐ (x : α) μ, f x = g x) :
μ = μ
@[simp]
theorem measure_theory.snorm'_norm {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {q : } {μ : measure_theory.measure α} {f : α F} :
measure_theory.snorm' (λ (a : α), f a) q μ =
@[simp]
theorem measure_theory.snorm_norm {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} (f : α F) :
measure_theory.snorm (λ (x : α), f x) p μ = μ
theorem measure_theory.snorm'_norm_rpow {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {μ : measure_theory.measure α} (f : α F) (p q : ) (hq_pos : 0 < q) :
measure_theory.snorm' (λ (x : α), f x ^ q) p μ = (p * q) μ ^ q
theorem measure_theory.snorm_norm_rpow {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {q : } {μ : measure_theory.measure α} (f : α F) (hq_pos : 0 < q) :
measure_theory.snorm (λ (x : α), f x ^ q) p μ = (p * μ ^ q
theorem measure_theory.snorm_congr_ae {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f g : α F} (hfg : f =ᵐ[μ] g) :
μ = μ
theorem measure_theory.mem_ℒp_congr_ae {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f g : α E} (hfg : f =ᵐ[μ] g) :
theorem measure_theory.mem_ℒp.ae_eq {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f g : α E} (hfg : f =ᵐ[μ] g) (hf_Lp : μ) :
theorem measure_theory.mem_ℒp.of_le {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f : α E} {g : α F} (hg : μ) (hfg : ∀ᵐ (x : α) μ, f x g x) :
theorem measure_theory.mem_ℒp.mono {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f : α E} {g : α F} (hg : μ) (hfg : ∀ᵐ (x : α) μ, f x g x) :

Alias of `measure_theory.mem_ℒp.of_le`.

theorem measure_theory.mem_ℒp.mono' {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f : α E} {g : α } (hg : μ) (h : ∀ᵐ (a : α) μ, f a g a) :
theorem measure_theory.mem_ℒp.congr_norm {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f : α E} {g : α F} (hf : μ) (h : ∀ᵐ (a : α) μ, f a = g a) :
theorem measure_theory.mem_ℒp_congr_norm {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f : α E} {g : α F} (h : ∀ᵐ (a : α) μ, f a = g a) :
theorem measure_theory.mem_ℒp_top_of_bound {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} {f : α E} (C : ) (hfC : ∀ᵐ (x : α) μ, f x C) :
theorem measure_theory.mem_ℒp.of_bound {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f : α E} (C : ) (hfC : ∀ᵐ (x : α) μ, f x C) :
theorem measure_theory.snorm'_mono_measure {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {q : } {μ ν : measure_theory.measure α} (f : α F) (hμν : ν μ) (hq : 0 q) :
theorem measure_theory.snorm_ess_sup_mono_measure {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {μ ν : measure_theory.measure α} (f : α F) (hμν : ν.absolutely_continuous μ) :
theorem measure_theory.snorm_mono_measure {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ ν : measure_theory.measure α} (f : α F) (hμν : ν μ) :
ν μ
theorem measure_theory.mem_ℒp.mono_measure {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ ν : measure_theory.measure α} {f : α E} (hμν : ν μ) (hf : μ) :
theorem measure_theory.mem_ℒp.restrict {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} (s : set α) {f : α E} (hf : μ) :
(μ.restrict s)
theorem measure_theory.snorm'_smul_measure {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {μ : measure_theory.measure α} {p : } (hp : 0 p) {f : α F} (c : ennreal) :
(c μ) = c ^ (1 / p) *
theorem measure_theory.snorm_ess_sup_smul_measure {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {μ : measure_theory.measure α} {f : α F} {c : ennreal} (hc : c 0) :
theorem measure_theory.snorm_smul_measure_of_ne_zero {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {μ : measure_theory.measure α} {p : ennreal} {f : α F} {c : ennreal} (hc : c 0) :
(c μ) = c ^ (1 / p).to_real μ
theorem measure_theory.snorm_smul_measure_of_ne_top {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {μ : measure_theory.measure α} {p : ennreal} (hp_ne_top : p ) {f : α F} (c : ennreal) :
(c μ) = c ^ (1 / p).to_real μ
theorem measure_theory.snorm_one_smul_measure {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {μ : measure_theory.measure α} {f : α F} (c : ennreal) :
(c μ) = c * μ
theorem measure_theory.mem_ℒp.of_measure_le_smul {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {μ' : measure_theory.measure α} (c : ennreal) (hc : c ) (hμ'_le : μ' c μ) {f : α E} (hf : μ) :
μ'
theorem measure_theory.mem_ℒp.smul_measure {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f : α E} {c : ennreal} (hf : μ) (hc : c ) :
(c μ)
theorem measure_theory.snorm_one_add_measure {α : Type u_1} {F : Type u_3} {m : measurable_space α} (f : α F) (μ ν : measure_theory.measure α) :
+ ν) = μ + ν
theorem measure_theory.snorm_le_add_measure_right {α : Type u_1} {F : Type u_3} {m : measurable_space α} (f : α F) (μ ν : measure_theory.measure α) {p : ennreal} :
μ + ν)
theorem measure_theory.snorm_le_add_measure_left {α : Type u_1} {F : Type u_3} {m : measurable_space α} (f : α F) (μ ν : measure_theory.measure α) {p : ennreal} :
ν + ν)
theorem measure_theory.mem_ℒp.left_of_add_measure {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ ν : measure_theory.measure α} {f : α E} (h : + ν)) :
theorem measure_theory.mem_ℒp.right_of_add_measure {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ ν : measure_theory.measure α} {f : α E} (h : + ν)) :
theorem measure_theory.mem_ℒp.norm {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f : α E} (h : μ) :
measure_theory.mem_ℒp (λ (x : α), f x) p μ
theorem measure_theory.mem_ℒp_norm_iff {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f : α E}  :
measure_theory.mem_ℒp (λ (x : α), f x) p μ
theorem measure_theory.snorm'_eq_zero_of_ae_zero {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {q : } {μ : measure_theory.measure α} {f : α F} (hq0_lt : 0 < q) (hf_zero : f =ᵐ[μ] 0) :
= 0
theorem measure_theory.snorm'_eq_zero_of_ae_zero' {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {q : } {μ : measure_theory.measure α} (hq0_ne : q 0) (hμ : μ 0) {f : α F} (hf_zero : f =ᵐ[μ] 0) :
= 0
theorem measure_theory.ae_eq_zero_of_snorm'_eq_zero {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {q : } {μ : measure_theory.measure α} {f : α E} (hq0 : 0 q) (h : = 0) :
f =ᵐ[μ] 0
theorem measure_theory.snorm'_eq_zero_iff {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {q : } {μ : measure_theory.measure α} (hq0_lt : 0 < q) {f : α E}  :
= 0 f =ᵐ[μ] 0
theorem measure_theory.coe_nnnorm_ae_le_snorm_ess_sup {α : Type u_1} {F : Type u_3} {m : measurable_space α} (f : α F) (μ : measure_theory.measure α) :
∀ᵐ (x : α) μ,
@[simp]
theorem measure_theory.snorm_ess_sup_eq_zero_iff {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {μ : measure_theory.measure α} {f : α F} :
f =ᵐ[μ] 0
theorem measure_theory.snorm_eq_zero_iff {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f : α E} (h0 : p 0) :
μ = 0 f =ᵐ[μ] 0
theorem measure_theory.snorm'_add_le {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {q : } {μ : measure_theory.measure α} {f g : α E} (hq1 : 1 q) :
theorem measure_theory.snorm'_add_le_of_le_one {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {q : } {μ : measure_theory.measure α} {f g : α E} (hq0 : 0 q) (hq1 : q 1) :
measure_theory.snorm' (f + g) q μ 2 ^ (1 / q - 1) * μ + μ)
theorem measure_theory.snorm_ess_sup_add_le {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {μ : measure_theory.measure α} {f g : α F} :
theorem measure_theory.snorm_add_le {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f g : α E} (hp1 : 1 p) :
measure_theory.snorm (f + g) p μ μ + μ
noncomputable def measure_theory.Lp_add_const (p : ennreal) :

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)`.

Equations
theorem measure_theory.snorm_add_le' {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} {f g : α E} (p : ennreal) :
measure_theory.snorm (f + g) p μ * μ + μ)
theorem measure_theory.exists_Lp_half {α : Type u_1} (E : Type u_2) {m0 : measurable_space α} (μ : measure_theory.measure α) (p : ennreal) {δ : ennreal} (hδ : δ 0) :
(η : ennreal), 0 < η (f g : α E), μ η μ η measure_theory.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 measure_theory.snorm_sub_le' {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} {f g : α E} (p : ennreal) :
measure_theory.snorm (f - g) p μ * μ + μ)
theorem measure_theory.snorm_sub_le {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f g : α E} (hp : 1 p) :
measure_theory.snorm (f - g) p μ μ + μ
theorem measure_theory.snorm_add_lt_top {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f g : α E} (hf : μ) (hg : μ) :
theorem measure_theory.ae_le_snorm_ess_sup {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {μ : measure_theory.measure α} {f : α F} :
∀ᵐ (y : α) μ,
theorem measure_theory.meas_snorm_ess_sup_lt {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {μ : measure_theory.measure α} {f : α F} :
μ {y : α | = 0
theorem measure_theory.snorm_ess_sup_map_measure {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} {β : Type u_5} {mβ : measurable_space β} {f : α β} {g : β E} (hf : μ) :
theorem measure_theory.snorm_map_measure {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {β : Type u_5} {mβ : measurable_space β} {f : α β} {g : β E} (hf : μ) :
theorem measure_theory.mem_ℒp_map_measure_iff {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {β : Type u_5} {mβ : measurable_space β} {f : α β} {g : β E} (hf : μ) :
theorem measurable_embedding.snorm_ess_sup_map_measure {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {μ : measure_theory.measure α} {β : Type u_5} {mβ : measurable_space β} {f : α β} {g : β F} (hf : measurable_embedding f) :
theorem measurable_embedding.snorm_map_measure {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {β : Type u_5} {mβ : measurable_space β} {f : α β} {g : β F} (hf : measurable_embedding f) :
theorem measurable_embedding.mem_ℒp_map_measure_iff {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {β : Type u_5} {mβ : measurable_space β} {f : α β} {g : β F} (hf : measurable_embedding f) :
theorem measurable_equiv.mem_ℒp_map_measure_iff {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {β : Type u_5} {mβ : measurable_space β} (f : α ≃ᵐ β) {g : β F} :
theorem measure_theory.snorm'_trim {α : Type u_1} {E : Type u_2} {m m0 : measurable_space α} {q : } {ν : measure_theory.measure α} (hm : m m0) {f : α E}  :
(ν.trim hm) =
theorem measure_theory.limsup_trim {α : Type u_1} {m m0 : measurable_space α} {ν : measure_theory.measure α} (hm : m m0) {f : α ennreal} (hf : measurable f) :
(ν.trim hm).ae = ν.ae
theorem measure_theory.ess_sup_trim {α : Type u_1} {m m0 : measurable_space α} {ν : measure_theory.measure α} (hm : m m0) {f : α ennreal} (hf : measurable f) :
(ν.trim hm) = ν
theorem measure_theory.snorm_ess_sup_trim {α : Type u_1} {E : Type u_2} {m m0 : measurable_space α} {ν : measure_theory.measure α} (hm : m m0) {f : α E}  :
theorem measure_theory.snorm_trim {α : Type u_1} {E : Type u_2} {m m0 : measurable_space α} {p : ennreal} {ν : measure_theory.measure α} (hm : m m0) {f : α E}  :
(ν.trim hm) = ν
theorem measure_theory.snorm_trim_ae {α : Type u_1} {E : Type u_2} {m m0 : measurable_space α} {p : ennreal} {ν : measure_theory.measure α} (hm : m m0) {f : α E} (hf : (ν.trim hm)) :
(ν.trim hm) = ν
theorem measure_theory.mem_ℒp_of_mem_ℒp_trim {α : Type u_1} {E : Type u_2} {m m0 : measurable_space α} {p : ennreal} {ν : measure_theory.measure α} (hm : m m0) {f : α E} (hf : (ν.trim hm)) :
@[simp]
theorem measure_theory.snorm'_neg {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {q : } {μ : measure_theory.measure α} {f : α F} :
μ =
@[simp]
theorem measure_theory.snorm_neg {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f : α F} :
μ = μ
theorem measure_theory.mem_ℒp.neg {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f : α E} (hf : μ) :
μ
theorem measure_theory.mem_ℒp_neg_iff {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f : α E} :
μ
theorem measure_theory.snorm'_le_snorm'_mul_rpow_measure_univ {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} {p q : } (hp0_lt : 0 < p) (hpq : p q) {f : α E}  :
* ^ (1 / p - 1 / q)
theorem measure_theory.snorm'_le_snorm_ess_sup_mul_rpow_measure_univ {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {q : } {μ : measure_theory.measure α} (hq_pos : 0 < q) {f : α F} :
* ^ (1 / q)
theorem measure_theory.snorm_le_snorm_mul_rpow_measure_univ {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} {p q : ennreal} (hpq : p q) {f : α E}  :
μ μ * ^ (1 / p.to_real - 1 / q.to_real)
theorem measure_theory.snorm'_le_snorm'_of_exponent_le {α : Type u_1} {E : Type u_2} {m : measurable_space α} {p q : } (hp0_lt : 0 < p) (hpq : p q) (μ : measure_theory.measure α) {f : α E}  :
theorem measure_theory.snorm'_le_snorm_ess_sup {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {q : } {μ : measure_theory.measure α} (hq_pos : 0 < q) {f : α F}  :
theorem measure_theory.snorm_le_snorm_of_exponent_le {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} {p q : ennreal} (hpq : p q) {f : α E}  :
μ μ
theorem measure_theory.snorm'_lt_top_of_snorm'_lt_top_of_exponent_le {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} {p q : } {f : α E} (hfq_lt_top : < ) (hp_nonneg : 0 p) (hpq : p q) :
theorem measure_theory.pow_mul_meas_ge_le_snorm {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} (μ : measure_theory.measure α) {f : α E} (hp_ne_zero : p 0) (hp_ne_top : p ) (ε : ennreal) :
* μ {x : α | ε f x‖₊ ^ p.to_real}) ^ (1 / p.to_real) μ
theorem measure_theory.mul_meas_ge_le_pow_snorm {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} (μ : measure_theory.measure α) {f : α E} (hp_ne_zero : p 0) (hp_ne_top : p ) (ε : ennreal) :
ε * μ {x : α | ε f x‖₊ ^ p.to_real} μ ^ p.to_real
theorem measure_theory.mul_meas_ge_le_pow_snorm' {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} (μ : measure_theory.measure α) {f : α E} (hp_ne_zero : p 0) (hp_ne_top : p ) (ε : ennreal) :
ε ^ p.to_real * μ {x : α | ε f x‖₊} μ ^ p.to_real

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

theorem measure_theory.meas_ge_le_mul_pow_snorm {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} (μ : measure_theory.measure α) {f : α E} (hp_ne_zero : p 0) (hp_ne_top : p ) {ε : ennreal} (hε : ε 0) :
μ {x : α | ε f x‖₊} ε⁻¹ ^ p.to_real * μ ^ p.to_real
theorem measure_theory.mem_ℒp.mem_ℒp_of_exponent_le {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} {p q : ennreal} {f : α E} (hfq : μ) (hpq : p q) :
theorem measure_theory.snorm'_sum_le {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {q : } {μ : measure_theory.measure α} {ι : Type u_3} {f : ι α E} {s : finset ι} (hfs : (i : ι), i s ) (hq1 : 1 q) :
measure_theory.snorm' (s.sum (λ (i : ι), f i)) q μ s.sum (λ (i : ι), q μ)
theorem measure_theory.snorm_sum_le {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {ι : Type u_3} {f : ι α E} {s : finset ι} (hfs : (i : ι), i s ) (hp1 : 1 p) :
measure_theory.snorm (s.sum (λ (i : ι), f i)) p μ s.sum (λ (i : ι), measure_theory.snorm (f i) p μ)
theorem measure_theory.mem_ℒp.add {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f g : α E} (hf : μ) (hg : μ) :
theorem measure_theory.mem_ℒp.sub {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f g : α E} (hf : μ) (hg : μ) :
theorem measure_theory.mem_ℒp_finset_sum {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {ι : Type u_3} (s : finset ι) {f : ι α E} (hf : (i : ι), i s p μ) :
measure_theory.mem_ℒp (λ (a : α), s.sum (λ (i : ι), f i a)) p μ
theorem measure_theory.mem_ℒp_finset_sum' {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {ι : Type u_3} (s : finset ι) {f : ι α E} (hf : (i : ι), i s p μ) :
measure_theory.mem_ℒp (s.sum (λ (i : ι), f i)) p μ
theorem measure_theory.snorm'_le_nnreal_smul_snorm'_of_ae_le_mul {α : Type u_1} {F : Type u_3} {G : Type u_4} {m0 : measurable_space α} {μ : measure_theory.measure α} {f : α F} {g : α G} {c : nnreal} (h : ∀ᵐ (x : α) μ, f x‖₊ c * g x‖₊) {p : } (hp : 0 < p) :
c
theorem measure_theory.snorm_ess_sup_le_nnreal_smul_snorm_ess_sup_of_ae_le_mul {α : Type u_1} {F : Type u_3} {G : Type u_4} {m0 : measurable_space α} {μ : measure_theory.measure α} {f : α F} {g : α G} {c : nnreal} (h : ∀ᵐ (x : α) μ, f x‖₊ c * g x‖₊) :
theorem measure_theory.snorm_le_nnreal_smul_snorm_of_ae_le_mul {α : Type u_1} {F : Type u_3} {G : Type u_4} {m0 : measurable_space α} {μ : measure_theory.measure α} {f : α F} {g : α G} {c : nnreal} (h : ∀ᵐ (x : α) μ, f x‖₊ c * g x‖₊) (p : ennreal) :
μ c μ
theorem measure_theory.snorm_eq_zero_and_zero_of_ae_le_mul_neg {α : Type u_1} {F : Type u_3} {G : Type u_4} {m0 : measurable_space α} {μ : measure_theory.measure α} {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 measure_theory.snorm_le_mul_snorm_of_ae_le_mul {α : Type u_1} {F : Type u_3} {G : Type u_4} {m0 : measurable_space α} {μ : measure_theory.measure α} {f : α F} {g : α G} {c : } (h : ∀ᵐ (x : α) μ, f x c * g x) (p : ennreal) :
μ
theorem measure_theory.mem_ℒp.of_nnnorm_le_mul {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f : α E} {g : α F} {c : nnreal} (hg : μ) (hfg : ∀ᵐ (x : α) μ, f x‖₊ c * g x‖₊) :
theorem measure_theory.mem_ℒp.of_le_mul {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f : α E} {g : α F} {c : } (hg : μ) (hfg : ∀ᵐ (x : α) μ, f x c * g x) :
theorem measure_theory.snorm'_le_snorm'_mul_snorm' {α : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {m0 : measurable_space α} {μ : measure_theory.measure α} {p q r : } {f : α E} {g : α F} (b : E F G) (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) :
measure_theory.snorm' (λ (x : α), b (f x) (g x)) p μ *
theorem measure_theory.snorm_le_snorm_top_mul_snorm {α : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {m0 : measurable_space α} {μ : measure_theory.measure α} (p : ennreal) (f : α E) {g : α F} (b : E F G) (h : ∀ᵐ (x : α) μ, b (f x) (g x)‖₊ f x‖₊ * g x‖₊) :
measure_theory.snorm (λ (x : α), b (f x) (g x)) p μ * μ
theorem measure_theory.snorm_le_snorm_mul_snorm_top {α : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {m0 : measurable_space α} {μ : measure_theory.measure α} (p : ennreal) {f : α E} (g : α F) (b : E F G) (h : ∀ᵐ (x : α) μ, b (f x) (g x)‖₊ f x‖₊ * g x‖₊) :
measure_theory.snorm (λ (x : α), b (f x) (g x)) p μ μ *
theorem measure_theory.snorm_le_snorm_mul_snorm_of_nnnorm {α : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {m0 : measurable_space α} {μ : measure_theory.measure α} {p q r : ennreal} {f : α E} {g : α F} (b : E F G) (h : ∀ᵐ (x : α) μ, b (f x) (g x)‖₊ f x‖₊ * g x‖₊) (hpqr : 1 / p = 1 / q + 1 / r) :
measure_theory.snorm (λ (x : α), b (f x) (g x)) p μ μ * μ

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

theorem measure_theory.snorm_le_snorm_mul_snorm'_of_norm {α : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {m0 : measurable_space α} {μ : measure_theory.measure α} {p q r : ennreal} {f : α E} {g : α F} (b : E F G) (h : ∀ᵐ (x : α) μ, b (f x) (g x) f x * g x) (hpqr : 1 / p = 1 / q + 1 / r) :
measure_theory.snorm (λ (x : α), b (f x) (g x)) p μ μ * μ

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

### Bounded actions by normed rings #

In this section we show inequalities on the norm.

theorem measure_theory.snorm'_const_smul_le {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {q : } {μ : measure_theory.measure α} {𝕜 : Type u_5} [normed_ring 𝕜] [ F] [ F] (c : 𝕜) (f : α F) (hq_pos : 0 < q) :
theorem measure_theory.snorm_ess_sup_const_smul_le {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {μ : measure_theory.measure α} {𝕜 : Type u_5} [normed_ring 𝕜] [ F] [ F] (c : 𝕜) (f : α F) :
μ
theorem measure_theory.snorm_const_smul_le {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {𝕜 : Type u_5} [normed_ring 𝕜] [ F] [ F] (c : 𝕜) (f : α F) :
theorem measure_theory.mem_ℒp.const_smul {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {𝕜 : Type u_5} [normed_ring 𝕜] [ E] [ E] {f : α E} (hf : μ) (c : 𝕜) :
theorem measure_theory.mem_ℒp.const_mul {α : Type u_1} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {R : Type u_2} [normed_ring R] {f : α R} (hf : μ) (c : R) :
measure_theory.mem_ℒp (λ (x : α), c * f x) p μ
theorem measure_theory.snorm'_smul_le_mul_snorm' {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} {𝕜 : Type u_5} [normed_ring 𝕜] [ E] [ E] {p q r : } {f : α E} {φ : α 𝕜} (hp0_lt : 0 < p) (hpq : p < q) (hpqr : 1 / p = 1 / q + 1 / r) :
theorem measure_theory.snorm_smul_le_snorm_top_mul_snorm {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} {𝕜 : Type u_5} [normed_ring 𝕜] [ E] [ E] (p : ennreal) {f : α E} (φ : α 𝕜) :
measure_theory.snorm f) p μ * μ
theorem measure_theory.snorm_smul_le_snorm_mul_snorm_top {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} {𝕜 : Type u_5} [normed_ring 𝕜] [ E] [ E] (p : ennreal) (f : α E) {φ : α 𝕜}  :
measure_theory.snorm f) p μ μ *
theorem measure_theory.snorm_smul_le_mul_snorm {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} {𝕜 : Type u_5} [normed_ring 𝕜] [ E] [ E] {p q r : ennreal} {f : α E} {φ : α 𝕜} (hpqr : 1 / p = 1 / q + 1 / r) :
measure_theory.snorm f) p μ μ * μ

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

theorem measure_theory.mem_ℒp.smul {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} {𝕜 : Type u_5} [normed_ring 𝕜] [ E] [ E] {p q r : ennreal} {f : α E} {φ : α 𝕜} (hf : μ) (hφ : μ) (hpqr : 1 / p = 1 / q + 1 / r) :
theorem measure_theory.mem_ℒp.smul_of_top_right {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} {𝕜 : Type u_5} [normed_ring 𝕜] [ E] [ E] {p : ennreal} {f : α E} {φ : α 𝕜} (hf : μ) (hφ : μ) :
theorem measure_theory.mem_ℒp.smul_of_top_left {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} {𝕜 : Type u_5} [normed_ring 𝕜] [ E] [ E] {p : ennreal} {f : α E} {φ : α 𝕜} (hf : μ) (hφ : μ) :

### Bounded actions by normed division rings #

The inequalities in the previous section are now tight.

theorem measure_theory.snorm'_const_smul {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {q : } {μ : measure_theory.measure α} {𝕜 : Type u_5} [ F] [ F] {f : α F} (c : 𝕜) (hq_pos : 0 < q) :
theorem measure_theory.snorm_ess_sup_const_smul {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {μ : measure_theory.measure α} {𝕜 : Type u_5} [ F] [ F] (c : 𝕜) (f : α F) :
μ =
theorem measure_theory.snorm_const_smul {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {𝕜 : Type u_5} [ F] [ F] (c : 𝕜) (f : α F) :
theorem measure_theory.snorm_indicator_ge_of_bdd_below {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} (hp : p 0) (hp' : p ) {f : α F} (C : nnreal) {s : set α} (hs : measurable_set s) (hf : ∀ᵐ (x : α) μ, x s C s.indicator f x‖₊) :
C μ s ^ (1 / p.to_real) p μ
theorem measure_theory.mem_ℒp.re {α : Type u_1} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {𝕜 : Type u_5} [is_R_or_C 𝕜] {f : α 𝕜} (hf : μ) :
measure_theory.mem_ℒp (λ (x : α), is_R_or_C.re (f x)) p μ
theorem measure_theory.mem_ℒp.im {α : Type u_1} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {𝕜 : Type u_5} [is_R_or_C 𝕜] {f : α 𝕜} (hf : μ) :
measure_theory.mem_ℒp (λ (x : α), is_R_or_C.im (f x)) p μ
theorem measure_theory.ae_bdd_liminf_at_top_rpow_of_snorm_bdd {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} {R : nnreal} {p : ennreal} {f : α E} (hfmeas : (n : ), measurable (f n)) (hbdd : (n : ), measure_theory.snorm (f n) p μ R) :
theorem measure_theory.ae_bdd_liminf_at_top_of_snorm_bdd {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} {R : nnreal} {p : ennreal} (hp : p 0) {f : α E} (hfmeas : (n : ), measurable (f n)) (hbdd : (n : ), measure_theory.snorm (f n) p μ R) :