mathlib3 documentation

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 #

ℒ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} [normed_add_comm_group F] {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} [normed_add_comm_group F] {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} [normed_add_comm_group F] {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 α} [normed_add_comm_group F] (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 α} [normed_add_comm_group F] (hp_ne_zero : p 0) (hp_ne_top : p ) {f : α F} :
measure_theory.snorm f p μ = (∫⁻ (x : α), f x‖₊ ^ p.to_real μ) ^ (1 / p.to_real)
def measure_theory.mem_ℒp {E : Type u_2} [normed_add_comm_group E] {α : Type u_1} {m : measurable_space α} (f : α E) (p : ennreal) (μ : measure_theory.measure α . "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.lintegral_rpow_nnnorm_eq_rpow_snorm' {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {q : } {μ : measure_theory.measure α} [normed_add_comm_group F] {f : α F} (hq0_lt : 0 < q) :
∫⁻ (a : α), f a‖₊ ^ q μ = measure_theory.snorm' f q μ ^ q
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 α} [normed_add_comm_group F] {f : α F} (hq0_lt : 0 < q) (hfq : measure_theory.snorm' f q μ < ) :
∫⁻ (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 α} [normed_add_comm_group F] {f : α F} (hp_ne_zero : p 0) (hp_ne_top : p ) (hfp : measure_theory.snorm f p μ < ) :
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 α} [normed_add_comm_group F] {f : α F} (hp_ne_zero : p 0) (hp_ne_top : p ) :
@[simp]
theorem measure_theory.snorm'_exponent_zero {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_add_comm_group F] {f : α F} :
@[simp]
theorem measure_theory.snorm_exponent_zero {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_add_comm_group F] {f : α F} :
@[simp]
theorem measure_theory.snorm'_zero {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {q : } {μ : measure_theory.measure α} [normed_add_comm_group F] (hp0_lt : 0 < q) :
@[simp]
theorem measure_theory.snorm'_zero' {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {q : } {μ : measure_theory.measure α} [normed_add_comm_group F] (hq0_ne : q 0) (hμ : μ 0) :
@[simp]
theorem measure_theory.snorm_zero {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group F] :
@[simp]
theorem measure_theory.snorm_zero' {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group F] :
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 α} [normed_add_comm_group E] :
measure_theory.mem_ℒp (λ (x : α), 0) p μ
theorem measure_theory.snorm'_measure_zero_of_pos {α : Type u_1} {F : Type u_3} {q : } [normed_add_comm_group F] [measurable_space α] {f : α F} (hq_pos : 0 < q) :
theorem measure_theory.snorm'_measure_zero_of_neg {α : Type u_1} {F : Type u_3} {q : } [normed_add_comm_group F] [measurable_space α] {f : α F} (hq_neg : q < 0) :
@[simp]
theorem measure_theory.snorm_measure_zero {α : Type u_1} {F : Type u_3} {p : ennreal} [normed_add_comm_group F] [measurable_space α] {f : α F} :
theorem measure_theory.snorm'_const {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {q : } {μ : measure_theory.measure α} [normed_add_comm_group F] (c : F) (hq_pos : 0 < q) :
measure_theory.snorm' (λ (x : α), c) q μ = c‖₊ * μ set.univ ^ (1 / q)
theorem measure_theory.snorm'_const' {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {q : } {μ : measure_theory.measure α} [normed_add_comm_group F] [measure_theory.is_finite_measure μ] (c : F) (hc_ne_zero : c 0) (hq_ne_zero : q 0) :
measure_theory.snorm' (λ (x : α), c) q μ = c‖₊ * μ set.univ ^ (1 / q)
theorem measure_theory.snorm_ess_sup_const {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_add_comm_group F] (c : F) (hμ : μ 0) :
theorem measure_theory.snorm_const {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group F] (c : F) (h0 : p 0) (hμ : μ 0) :
measure_theory.snorm (λ (x : α), c) p μ = c‖₊ * μ set.univ ^ (1 / p.to_real)
theorem measure_theory.snorm_const' {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group F] (c : F) (h0 : p 0) (h_top : p ) :
measure_theory.snorm (λ (x : α), c) p μ = c‖₊ * μ set.univ ^ (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 α} [normed_add_comm_group F] {p : ennreal} {c : F} (hp_ne_zero : p 0) (hp_ne_top : p ) :
measure_theory.snorm (λ (x : α), c) p μ < c = 0 μ set.univ <
theorem measure_theory.mem_ℒp_top_const {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_add_comm_group E] (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 α} [normed_add_comm_group E] {p : ennreal} {c : E} (hp_ne_zero : p 0) (hp_ne_top : p ) :
measure_theory.mem_ℒp (λ (x : α), c) p μ c = 0 μ set.univ <
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 α} [normed_add_comm_group F] [normed_add_comm_group G] {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 α} [normed_add_comm_group F] [normed_add_comm_group G] {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 α} [normed_add_comm_group F] {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 α} [normed_add_comm_group F] {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 α} [normed_add_comm_group F] {f g : α F} (hfg : f =ᵐ[μ] g) :
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 α} [normed_add_comm_group F] [normed_add_comm_group G] {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 α} [normed_add_comm_group F] [normed_add_comm_group G] {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 α} [normed_add_comm_group F] {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 α} [normed_add_comm_group F] [normed_add_comm_group G] {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 α} [normed_add_comm_group F] [normed_add_comm_group G] {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 α} [normed_add_comm_group F] {f : α F} {g : α } (h : (x : α), f x g x) :
theorem measure_theory.snorm_ess_sup_lt_top_of_ae_bound {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_add_comm_group F] {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 α} [normed_add_comm_group F] {f : α F} {C : nnreal} (hfC : ∀ᵐ (x : α) μ, f x‖₊ C) :
theorem measure_theory.snorm_le_of_ae_bound {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group F] {f : α F} {C : } (hfC : ∀ᵐ (x : α) μ, f x C) :
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 α} [normed_add_comm_group F] [normed_add_comm_group G] {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 α} [normed_add_comm_group F] [normed_add_comm_group G] {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 α} [normed_add_comm_group F] {f : α F} :
measure_theory.snorm' (λ (a : α), f a) q μ = measure_theory.snorm' f q μ
@[simp]
theorem measure_theory.snorm_norm {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group F] (f : α F) :
measure_theory.snorm (λ (x : α), f x) p μ = measure_theory.snorm f p μ
theorem measure_theory.snorm'_norm_rpow {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_add_comm_group F] (f : α F) (p q : ) (hq_pos : 0 < q) :
measure_theory.snorm' (λ (x : α), f x ^ q) p μ = measure_theory.snorm' f (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 α} [normed_add_comm_group F] (f : α F) (hq_pos : 0 < q) :
measure_theory.snorm (λ (x : α), f x ^ q) p μ = measure_theory.snorm f (p * ennreal.of_real q) μ ^ q
theorem measure_theory.snorm_congr_ae {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group F] {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 α} [normed_add_comm_group E] {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 α} [normed_add_comm_group E] {f g : α E} (hfg : f =ᵐ[μ] g) (hf_Lp : measure_theory.mem_ℒp f p μ) :
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 α} [normed_add_comm_group E] [normed_add_comm_group F] {f : α E} {g : α F} (hg : measure_theory.mem_ℒp g p μ) (hf : measure_theory.ae_strongly_measurable f μ) (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 α} [normed_add_comm_group E] [normed_add_comm_group F] {f : α E} {g : α F} (hg : measure_theory.mem_ℒp g p μ) (hf : measure_theory.ae_strongly_measurable f μ) (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 α} [normed_add_comm_group E] {f : α E} {g : α } (hg : measure_theory.mem_ℒp g p μ) (hf : measure_theory.ae_strongly_measurable f μ) (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 α} [normed_add_comm_group E] [normed_add_comm_group F] {f : α E} {g : α F} (hf : measure_theory.mem_ℒp f p μ) (hg : measure_theory.ae_strongly_measurable g μ) (h : ∀ᵐ (a : α) μ, f a = g a) :
theorem measure_theory.snorm'_mono_measure {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {q : } {μ ν : measure_theory.measure α} [normed_add_comm_group F] (f : α F) (hμν : ν μ) (hq : 0 q) :
theorem measure_theory.snorm_mono_measure {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ ν : measure_theory.measure α} [normed_add_comm_group F] (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 α} [normed_add_comm_group E] {f : α E} (hμν : ν μ) (hf : measure_theory.mem_ℒp f p μ) :
theorem measure_theory.mem_ℒp.restrict {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] (s : set α) {f : α E} (hf : measure_theory.mem_ℒp f p μ) :
theorem measure_theory.snorm'_smul_measure {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_add_comm_group F] {p : } (hp : 0 p) {f : α F} (c : ennreal) :
theorem measure_theory.snorm_smul_measure_of_ne_zero {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_add_comm_group F] {p : ennreal} {f : α F} {c : ennreal} (hc : c 0) :
theorem measure_theory.snorm_smul_measure_of_ne_top {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_add_comm_group F] {p : ennreal} (hp_ne_top : p ) {f : α F} (c : ennreal) :
theorem measure_theory.mem_ℒp.of_measure_le_smul {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] {μ' : measure_theory.measure α} (c : ennreal) (hc : c ) (hμ'_le : μ' c μ) {f : α E} (hf : measure_theory.mem_ℒp f p μ) :
theorem measure_theory.mem_ℒp.smul_measure {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] {f : α E} {c : ennreal} (hf : measure_theory.mem_ℒp f p μ) (hc : c ) :
theorem measure_theory.mem_ℒp.norm {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] {f : α E} (h : measure_theory.mem_ℒp f p μ) :
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 α} [normed_add_comm_group F] {f : α F} (hq0_lt : 0 < q) (hf_zero : f =ᵐ[μ] 0) :
theorem measure_theory.snorm'_eq_zero_of_ae_zero' {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {q : } {μ : measure_theory.measure α} [normed_add_comm_group F] (hq0_ne : q 0) (hμ : μ 0) {f : α F} (hf_zero : f =ᵐ[μ] 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 α} [normed_add_comm_group E] {f : α E} (hq0 : 0 q) (hf : measure_theory.ae_strongly_measurable f μ) (h : measure_theory.snorm' f q μ = 0) :
f =ᵐ[μ] 0
theorem measure_theory.snorm'_eq_zero_iff {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {q : } {μ : measure_theory.measure α} [normed_add_comm_group E] (hq0_lt : 0 < q) {f : α E} (hf : measure_theory.ae_strongly_measurable f μ) :
theorem measure_theory.snorm_eq_zero_iff {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] {f : α E} (hf : measure_theory.ae_strongly_measurable f μ) (h0 : p 0) :
theorem measure_theory.snorm'_add_le_of_le_one {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {q : } {μ : measure_theory.measure α} [normed_add_comm_group E] {f g : α E} (hf : measure_theory.ae_strongly_measurable f μ) (hq0 : 0 q) (hq1 : q 1) :
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

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_add_lt_top {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] {f g : α E} (hf : measure_theory.mem_ℒp f p μ) (hg : measure_theory.mem_ℒp g p μ) :
theorem measurable_embedding.snorm_map_measure {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group F] {β : Type u_5} {mβ : measurable_space β} {f : α β} {g : β F} (hf : measurable_embedding f) :
theorem measure_theory.snorm'_trim {α : Type u_1} {E : Type u_2} {m m0 : measurable_space α} {q : } {ν : measure_theory.measure α} [normed_add_comm_group E] (hm : m m0) {f : α E} (hf : measure_theory.strongly_measurable f) :
theorem measure_theory.limsup_trim {α : Type u_1} {m m0 : measurable_space α} {ν : measure_theory.measure α} (hm : m m0) {f : α ennreal} (hf : measurable f) :
theorem measure_theory.ess_sup_trim {α : Type u_1} {m m0 : measurable_space α} {ν : measure_theory.measure α} (hm : m m0) {f : α ennreal} (hf : measurable f) :
ess_sup f (ν.trim hm) = ess_sup f ν
theorem measure_theory.snorm_trim {α : Type u_1} {E : Type u_2} {m m0 : measurable_space α} {p : ennreal} {ν : measure_theory.measure α} [normed_add_comm_group E] (hm : m m0) {f : α E} (hf : measure_theory.strongly_measurable f) :
theorem measure_theory.snorm_trim_ae {α : Type u_1} {E : Type u_2} {m m0 : measurable_space α} {p : ennreal} {ν : measure_theory.measure α} [normed_add_comm_group E] (hm : m m0) {f : α E} (hf : measure_theory.ae_strongly_measurable f (ν.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 α} [normed_add_comm_group E] (hm : m m0) {f : α E} (hf : measure_theory.mem_ℒp f p (ν.trim hm)) :
@[simp]
theorem measure_theory.snorm'_neg {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {q : } {μ : measure_theory.measure α} [normed_add_comm_group F] {f : α F} :
@[simp]
theorem measure_theory.snorm_neg {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group F] {f : α F} :
theorem measure_theory.mem_ℒp.neg {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] {f : α E} (hf : measure_theory.mem_ℒp f p μ) :
theorem measure_theory.snorm'_le_snorm'_mul_rpow_measure_univ {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_add_comm_group E] {p q : } (hp0_lt : 0 < p) (hpq : p q) {f : α E} (hf : measure_theory.ae_strongly_measurable f μ) :
theorem measure_theory.pow_mul_meas_ge_le_snorm {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} (μ : measure_theory.measure α) [normed_add_comm_group E] {f : α E} (hp_ne_zero : p 0) (hp_ne_top : p ) (hf : measure_theory.ae_strongly_measurable f μ) (ε : ennreal) :
* μ {x : α | ε f x‖₊ ^ p.to_real}) ^ (1 / p.to_real) measure_theory.snorm f p μ
theorem measure_theory.mul_meas_ge_le_pow_snorm {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} (μ : measure_theory.measure α) [normed_add_comm_group E] {f : α E} (hp_ne_zero : p 0) (hp_ne_top : p ) (hf : measure_theory.ae_strongly_measurable f μ) (ε : ennreal) :
ε * μ {x : α | ε f x‖₊ ^ p.to_real} measure_theory.snorm f p μ ^ 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 α) [normed_add_comm_group E] {f : α E} (hp_ne_zero : p 0) (hp_ne_top : p ) (hf : measure_theory.ae_strongly_measurable f μ) (ε : ennreal) :
ε ^ p.to_real * μ {x : α | ε f x‖₊} measure_theory.snorm f p μ ^ 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 α) [normed_add_comm_group E] {f : α E} (hp_ne_zero : p 0) (hp_ne_top : p ) (hf : measure_theory.ae_strongly_measurable f μ) {ε : ennreal} (hε : ε 0) :
μ {x : α | ε f x‖₊} ε⁻¹ ^ p.to_real * measure_theory.snorm f p μ ^ p.to_real
theorem measure_theory.snorm'_sum_le {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {q : } {μ : measure_theory.measure α} [normed_add_comm_group E] {ι : Type u_3} {f : ι α E} {s : finset ι} (hfs : (i : ι), i s measure_theory.ae_strongly_measurable (f i) μ) (hq1 : 1 q) :
measure_theory.snorm' (s.sum (λ (i : ι), f i)) q μ s.sum (λ (i : ι), measure_theory.snorm' (f i) q μ)
theorem measure_theory.snorm_sum_le {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] {ι : Type u_3} {f : ι α E} {s : finset ι} (hfs : (i : ι), i s measure_theory.ae_strongly_measurable (f i) μ) (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 α} [normed_add_comm_group E] {f g : α E} (hf : measure_theory.mem_ℒp f p μ) (hg : measure_theory.mem_ℒp g p μ) :
theorem measure_theory.mem_ℒp.sub {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] {f g : α E} (hf : measure_theory.mem_ℒp f p μ) (hg : measure_theory.mem_ℒp g p μ) :
theorem measure_theory.mem_ℒp_finset_sum {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] {ι : Type u_3} (s : finset ι) {f : ι α E} (hf : (i : ι), i s measure_theory.mem_ℒp (f i) 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 α} [normed_add_comm_group E] {ι : Type u_3} (s : finset ι) {f : ι α E} (hf : (i : ι), i s measure_theory.mem_ℒp (f i) 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 α} [normed_add_comm_group F] [normed_add_comm_group G] {f : α F} {g : α G} {c : nnreal} (h : ∀ᵐ (x : α) μ, f x‖₊ c * g x‖₊) {p : } (hp : 0 < 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 α} [normed_add_comm_group F] [normed_add_comm_group G] {f : α F} {g : α G} {c : nnreal} (h : ∀ᵐ (x : α) μ, f x‖₊ c * g x‖₊) (p : ennreal) :
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 α} [normed_add_comm_group F] [normed_add_comm_group G] {f : α F} {g : α G} {c : } (h : ∀ᵐ (x : α) μ, f x c * g x) (hc : c < 0) (p : ennreal) :

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 α} [normed_add_comm_group F] [normed_add_comm_group G] {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 α} [normed_add_comm_group E] [normed_add_comm_group F] {f : α E} {g : α F} {c : nnreal} (hg : measure_theory.mem_ℒp g p μ) (hf : measure_theory.ae_strongly_measurable f μ) (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 α} [normed_add_comm_group E] [normed_add_comm_group F] {f : α E} {g : α F} {c : } (hg : measure_theory.mem_ℒp g p μ) (hf : measure_theory.ae_strongly_measurable f μ) (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 α} [normed_add_comm_group E] [normed_add_comm_group F] [normed_add_comm_group G] {p q r : } {f : α E} (hf : measure_theory.ae_strongly_measurable f μ) {g : α F} (hg : measure_theory.ae_strongly_measurable g μ) (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 μ measure_theory.snorm' f q μ * measure_theory.snorm' g r μ
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 α} [normed_add_comm_group E] [normed_add_comm_group F] [normed_add_comm_group G] (p : ennreal) (f : α E) {g : α F} (hg : measure_theory.ae_strongly_measurable g μ) (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 μ measure_theory.snorm f μ * measure_theory.snorm g 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 α} [normed_add_comm_group E] [normed_add_comm_group F] [normed_add_comm_group G] (p : ennreal) {f : α E} (hf : measure_theory.ae_strongly_measurable f μ) (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 μ measure_theory.snorm f p μ * measure_theory.snorm g μ
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 α} [normed_add_comm_group E] [normed_add_comm_group F] [normed_add_comm_group G] {p q r : ennreal} {f : α E} (hf : measure_theory.ae_strongly_measurable f μ) {g : α F} (hg : measure_theory.ae_strongly_measurable g μ) (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 μ measure_theory.snorm f q μ * measure_theory.snorm g r μ

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 α} [normed_add_comm_group E] [normed_add_comm_group F] [normed_add_comm_group G] {p q r : ennreal} {f : α E} (hf : measure_theory.ae_strongly_measurable f μ) {g : α F} (hg : measure_theory.ae_strongly_measurable g μ) (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 μ measure_theory.snorm f q μ * measure_theory.snorm g r μ

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 α} [normed_add_comm_group F] {𝕜 : Type u_5} [normed_ring 𝕜] [mul_action_with_zero 𝕜 F] [has_bounded_smul 𝕜 F] (c : 𝕜) (f : α F) (hq_pos : 0 < q) :
theorem measure_theory.snorm_const_smul_le {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group F] {𝕜 : Type u_5} [normed_ring 𝕜] [mul_action_with_zero 𝕜 F] [has_bounded_smul 𝕜 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 α} [normed_add_comm_group E] {𝕜 : Type u_5} [normed_ring 𝕜] [mul_action_with_zero 𝕜 E] [has_bounded_smul 𝕜 E] {f : α E} (hf : measure_theory.mem_ℒp f p μ) (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 : measure_theory.mem_ℒp f p μ) (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 α} [normed_add_comm_group E] {𝕜 : Type u_5} [normed_ring 𝕜] [mul_action_with_zero 𝕜 E] [has_bounded_smul 𝕜 E] {p q r : } {f : α E} (hf : measure_theory.ae_strongly_measurable f μ) {φ : α 𝕜} (hφ : measure_theory.ae_strongly_measurable φ μ) (hp0_lt : 0 < p) (hpq : p < q) (hpqr : 1 / p = 1 / q + 1 / r) :
theorem measure_theory.snorm_smul_le_mul_snorm {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_add_comm_group E] {𝕜 : Type u_5} [normed_ring 𝕜] [mul_action_with_zero 𝕜 E] [has_bounded_smul 𝕜 E] {p q r : ennreal} {f : α E} (hf : measure_theory.ae_strongly_measurable f μ) {φ : α 𝕜} (hφ : measure_theory.ae_strongly_measurable φ μ) (hpqr : 1 / p = 1 / q + 1 / r) :

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 α} [normed_add_comm_group E] {𝕜 : Type u_5} [normed_ring 𝕜] [mul_action_with_zero 𝕜 E] [has_bounded_smul 𝕜 E] {p q r : ennreal} {f : α E} {φ : α 𝕜} (hf : measure_theory.mem_ℒp f r μ) (hφ : measure_theory.mem_ℒp φ q μ) (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 α} [normed_add_comm_group E] {𝕜 : Type u_5} [normed_ring 𝕜] [mul_action_with_zero 𝕜 E] [has_bounded_smul 𝕜 E] {p : ennreal} {f : α E} {φ : α 𝕜} (hf : measure_theory.mem_ℒp f p μ) (hφ : measure_theory.mem_ℒp φ μ) :
theorem measure_theory.mem_ℒp.smul_of_top_left {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_add_comm_group E] {𝕜 : Type u_5} [normed_ring 𝕜] [mul_action_with_zero 𝕜 E] [has_bounded_smul 𝕜 E] {p : ennreal} {f : α E} {φ : α 𝕜} (hf : measure_theory.mem_ℒp f μ) (hφ : measure_theory.mem_ℒp φ p μ) :

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 α} [normed_add_comm_group F] {𝕜 : Type u_5} [normed_division_ring 𝕜] [module 𝕜 F] [has_bounded_smul 𝕜 F] {f : α F} (c : 𝕜) (hq_pos : 0 < q) :
theorem measure_theory.snorm_const_smul {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group F] {𝕜 : Type u_5} [normed_division_ring 𝕜] [module 𝕜 F] [has_bounded_smul 𝕜 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 α} [normed_add_comm_group F] (hp : p 0) (hp' : p ) {f : α F} (C : nnreal) {s : set α} (hs : measurable_set s) (hf : ∀ᵐ (x : α) μ, x s C s.indicator f x‖₊) :
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 f p μ) :
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 f p μ) :
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 α} [normed_add_comm_group E] [measurable_space E] [opens_measurable_space E] {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 α} [normed_add_comm_group E] [measurable_space E] [opens_measurable_space E] {R : nnreal} {p : ennreal} (hp : p 0) {f : α E} (hfmeas : (n : ), measurable (f n)) (hbdd : (n : ), measure_theory.snorm (f n) p μ R) :