ℒ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)forf : α → Fandp : ℝ, whereαis a measurable space andFis a normed group. -
snorm_ess_sup f μ: seminorm inℒ∞, equal to the essential supremumess_sup ‖f‖ μ. -
snorm f p μ: forp : ℝ≥0∞, seminorm inℒp, equal to0forp=0, tosnorm' f p μfor0 < p < ∞and tosnorm_ess_sup f μforp = ∞. -
mem_ℒp f p μ: property that the functionfis almost everywhere strongly measurable and has finitep-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}
[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
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‖.
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
- measure_theory.snorm f p μ = ite (p = 0) 0 (ite (p = ⊤) (measure_theory.snorm_ess_sup f μ) (measure_theory.snorm' f p.to_real μ))
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} :
measure_theory.snorm f p μ = measure_theory.snorm' f p.to_real μ
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} :
theorem
measure_theory.snorm_one_eq_lintegral_nnnorm
{α : 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_top
{α : Type u_1}
{F : Type u_3}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group F]
{f : α → F} :
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
- measure_theory.mem_ℒp f p μ = (measure_theory.ae_strongly_measurable f μ ∧ measure_theory.snorm f p μ < ⊤)
theorem
measure_theory.mem_ℒp.ae_strongly_measurable
{α : Type u_1}
{E : Type u_2}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group E]
{f : α → E}
{p : ennreal}
(h : measure_theory.mem_ℒp f p μ) :
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) :
theorem
measure_theory.mem_ℒp.snorm_lt_top
{α : Type u_1}
{E : Type u_2}
{m0 : measurable_space α}
{p : ennreal}
{μ : measure_theory.measure α}
[normed_add_comm_group E]
{f : α → E}
(hfp : measure_theory.mem_ℒp f p μ) :
measure_theory.snorm f p μ < ⊤
theorem
measure_theory.mem_ℒp.snorm_ne_top
{α : Type u_1}
{E : Type u_2}
{m0 : measurable_space α}
{p : ennreal}
{μ : measure_theory.measure α}
[normed_add_comm_group E]
{f : α → E}
(hfp : measure_theory.mem_ℒp f p μ) :
measure_theory.snorm f p μ ≠ ⊤
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 μ < ⊤) :
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} :
measure_theory.snorm' f 0 μ = 1
@[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} :
measure_theory.snorm f 0 μ = 0
theorem
measure_theory.mem_ℒp_zero_iff_ae_strongly_measurable
{α : Type u_1}
{E : Type u_2}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group E]
{f : α → E} :
@[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) :
measure_theory.snorm' 0 q μ = 0
@[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) :
measure_theory.snorm' 0 q μ = 0
@[simp]
theorem
measure_theory.snorm_ess_sup_zero
{α : Type u_1}
{F : Type u_3}
{m0 : measurable_space α}
{μ : 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 0 p μ = 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] :
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 0 p μ
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) :
measure_theory.snorm' f q 0 = 0
theorem
measure_theory.snorm'_measure_zero_of_exponent_zero
{α : Type u_1}
{F : Type u_3}
[normed_add_comm_group F]
[measurable_space α]
{f : α → F} :
measure_theory.snorm' f 0 0 = 1
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) :
measure_theory.snorm' f q 0 = ⊤
@[simp]
theorem
measure_theory.snorm_ess_sup_measure_zero
{α : Type u_1}
{F : Type u_3}
[normed_add_comm_group F]
[measurable_space α]
{f : α → F} :
@[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} :
measure_theory.snorm f p 0 = 0
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) :
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) :
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) :
measure_theory.snorm_ess_sup (λ (x : α), c) μ = ↑‖c‖₊
theorem
measure_theory.snorm'_const_of_is_probability_measure
{α : 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.is_probability_measure μ] :
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 α}
[normed_add_comm_group F]
(c : F)
(h0 : p ≠ 0)
(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_top : p ≠ ⊤) :
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 ≠ ⊤) :
theorem
measure_theory.mem_ℒp_const
{α : Type u_1}
{E : Type u_2}
{m0 : measurable_space α}
{p : ennreal}
{μ : measure_theory.measure α}
[normed_add_comm_group E]
(c : E)
[measure_theory.is_finite_measure μ] :
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 α}
[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 ≠ ⊤) :
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‖₊) :
measure_theory.snorm' f q μ ≤ measure_theory.snorm' g q μ
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‖) :
measure_theory.snorm' f q μ ≤ measure_theory.snorm' g q μ
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‖₊) :
measure_theory.snorm' f q μ = measure_theory.snorm' g q μ
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‖) :
measure_theory.snorm' f q μ = measure_theory.snorm' g q μ
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) :
measure_theory.snorm' f q μ = measure_theory.snorm' g q μ
theorem
measure_theory.snorm_ess_sup_congr_ae
{α : Type u_1}
{F : Type u_3}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group F]
{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 α}
[normed_add_comm_group F]
{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 α}
[normed_add_comm_group F]
[normed_add_comm_group G]
{f : α → F}
{g : α → G}
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ ‖g x‖₊) :
measure_theory.snorm f p μ ≤ measure_theory.snorm g p μ
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‖) :
measure_theory.snorm f p μ ≤ measure_theory.snorm g p μ
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) :
measure_theory.snorm f p μ ≤ measure_theory.snorm g p μ
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‖₊) :
measure_theory.snorm f p μ ≤ measure_theory.snorm g p μ
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‖) :
measure_theory.snorm f p μ ≤ measure_theory.snorm g p μ
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) :
measure_theory.snorm f p μ ≤ measure_theory.snorm g p μ
theorem
measure_theory.snorm_ess_sup_le_of_ae_nnnorm_bound
{α : Type u_1}
{F : Type u_3}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group F]
{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 α}
[normed_add_comm_group F]
{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 α}
[normed_add_comm_group F]
{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 α}
[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) :
measure_theory.snorm f p μ ≤ ⇑μ set.univ ^ (p.to_real)⁻¹ * ennreal.of_real 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‖₊) :
measure_theory.snorm f p μ = measure_theory.snorm g p μ
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‖) :
measure_theory.snorm f p μ = measure_theory.snorm g p μ
@[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) :
measure_theory.snorm f p μ = measure_theory.snorm g p μ
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) :
measure_theory.mem_ℒp f p μ ↔ measure_theory.mem_ℒp g p μ
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 μ) :
measure_theory.mem_ℒp g 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‖) :
measure_theory.mem_ℒp f p μ
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‖) :
measure_theory.mem_ℒp f p μ
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) :
measure_theory.mem_ℒp f p μ
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‖) :
measure_theory.mem_ℒp g p μ
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.ae_strongly_measurable f μ)
(hg : measure_theory.ae_strongly_measurable g μ)
(h : ∀ᵐ (a : α) ∂μ, ‖f a‖ = ‖g a‖) :
measure_theory.mem_ℒp f p μ ↔ measure_theory.mem_ℒp g p μ
theorem
measure_theory.mem_ℒp_top_of_bound
{α : Type u_1}
{E : Type u_2}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group E]
{f : α → E}
(hf : measure_theory.ae_strongly_measurable f μ)
(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 α}
[normed_add_comm_group E]
[measure_theory.is_finite_measure μ]
{f : α → E}
(hf : measure_theory.ae_strongly_measurable f μ)
(C : ℝ)
(hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C) :
measure_theory.mem_ℒp f p μ
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) :
measure_theory.snorm' f q ν ≤ measure_theory.snorm' f q μ
theorem
measure_theory.snorm_ess_sup_mono_measure
{α : Type u_1}
{F : Type u_3}
{m0 : measurable_space α}
{μ ν : measure_theory.measure α}
[normed_add_comm_group F]
(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 α}
[normed_add_comm_group F]
(f : α → F)
(hμν : ν ≤ μ) :
measure_theory.snorm f p ν ≤ measure_theory.snorm f p μ
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 μ) :
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 μ) :
measure_theory.mem_ℒp f p (μ.restrict s)
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) :
measure_theory.snorm' f p (c • μ) = c ^ (1 / p) * measure_theory.snorm' f p μ
theorem
measure_theory.snorm_ess_sup_smul_measure
{α : Type u_1}
{F : Type u_3}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group F]
{f : α → F}
{c : ennreal}
(hc : c ≠ 0) :
measure_theory.snorm_ess_sup f (c • μ) = measure_theory.snorm_ess_sup f μ
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) :
measure_theory.snorm f p (c • μ) = c ^ (1 / p).to_real • measure_theory.snorm f p μ
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) :
measure_theory.snorm f p (c • μ) = c ^ (1 / p).to_real • measure_theory.snorm f p μ
theorem
measure_theory.snorm_one_smul_measure
{α : Type u_1}
{F : Type u_3}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group F]
{f : α → F}
(c : ennreal) :
measure_theory.snorm f 1 (c • μ) = c * measure_theory.snorm f 1 μ
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 μ) :
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 ≠ ⊤) :
measure_theory.mem_ℒp f p (c • μ)
theorem
measure_theory.snorm_one_add_measure
{α : Type u_1}
{F : Type u_3}
{m : measurable_space α}
[normed_add_comm_group F]
(f : α → F)
(μ ν : measure_theory.measure α) :
measure_theory.snorm f 1 (μ + ν) = measure_theory.snorm f 1 μ + measure_theory.snorm f 1 ν
theorem
measure_theory.snorm_le_add_measure_right
{α : Type u_1}
{F : Type u_3}
{m : measurable_space α}
[normed_add_comm_group F]
(f : α → F)
(μ ν : measure_theory.measure α)
{p : ennreal} :
measure_theory.snorm f p μ ≤ measure_theory.snorm f p (μ + ν)
theorem
measure_theory.snorm_le_add_measure_left
{α : Type u_1}
{F : Type u_3}
{m : measurable_space α}
[normed_add_comm_group F]
(f : α → F)
(μ ν : measure_theory.measure α)
{p : ennreal} :
measure_theory.snorm f p ν ≤ measure_theory.snorm f p (μ + ν)
theorem
measure_theory.mem_ℒp.left_of_add_measure
{α : 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 f p μ
theorem
measure_theory.mem_ℒp.right_of_add_measure
{α : 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 f p ν
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.mem_ℒp_norm_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 μ) :
measure_theory.mem_ℒp (λ (x : α), ‖f x‖) p μ ↔ measure_theory.mem_ℒp f 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) :
measure_theory.snorm' f q μ = 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) :
measure_theory.snorm' f q μ = 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) :
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 μ) :
measure_theory.snorm' f q μ = 0 ↔ f =ᵐ[μ] 0
theorem
measure_theory.coe_nnnorm_ae_le_snorm_ess_sup
{α : Type u_1}
{F : Type u_3}
[normed_add_comm_group F]
{m : measurable_space α}
(f : α → F)
(μ : measure_theory.measure α) :
@[simp]
theorem
measure_theory.snorm_ess_sup_eq_zero_iff
{α : Type u_1}
{F : Type u_3}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group F]
{f : α → F} :
measure_theory.snorm_ess_sup f μ = 0 ↔ f =ᵐ[μ] 0
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) :
measure_theory.snorm f p μ = 0 ↔ f =ᵐ[μ] 0
theorem
measure_theory.snorm'_add_le
{α : 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 μ)
(hg : measure_theory.ae_strongly_measurable g μ)
(hq1 : 1 ≤ q) :
measure_theory.snorm' (f + g) q μ ≤ measure_theory.snorm' f q μ + measure_theory.snorm' g q μ
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) :
measure_theory.snorm' (f + g) q μ ≤ 2 ^ (1 / q - 1) * (measure_theory.snorm' f q μ + measure_theory.snorm' g q μ)
theorem
measure_theory.snorm_ess_sup_add_le
{α : Type u_1}
{F : Type u_3}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group F]
{f g : α → F} :
theorem
measure_theory.snorm_add_le
{α : 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.ae_strongly_measurable f μ)
(hg : measure_theory.ae_strongly_measurable g μ)
(hp1 : 1 ≤ p) :
measure_theory.snorm (f + g) p μ ≤ measure_theory.snorm f p μ + measure_theory.snorm g 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).
theorem
measure_theory.snorm_add_le'
{α : Type u_1}
{E : Type u_2}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group E]
{f g : α → E}
(hf : measure_theory.ae_strongly_measurable f μ)
(hg : measure_theory.ae_strongly_measurable g μ)
(p : ennreal) :
measure_theory.snorm (f + g) p μ ≤ measure_theory.Lp_add_const p * (measure_theory.snorm f p μ + measure_theory.snorm g p μ)
theorem
measure_theory.exists_Lp_half
{α : Type u_1}
(E : Type u_2)
{m0 : measurable_space α}
(μ : measure_theory.measure α)
[normed_add_comm_group E]
(p : ennreal)
{δ : ennreal}
(hδ : δ ≠ 0) :
∃ (η : ennreal), 0 < η ∧ ∀ (f g : α → E), measure_theory.ae_strongly_measurable f μ → measure_theory.ae_strongly_measurable g μ → measure_theory.snorm f p μ ≤ η → measure_theory.snorm g p μ ≤ η → 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 α}
[normed_add_comm_group E]
{f g : α → E}
(hf : measure_theory.ae_strongly_measurable f μ)
(hg : measure_theory.ae_strongly_measurable g μ)
(p : ennreal) :
measure_theory.snorm (f - g) p μ ≤ measure_theory.Lp_add_const p * (measure_theory.snorm f p μ + measure_theory.snorm g p μ)
theorem
measure_theory.snorm_sub_le
{α : 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.ae_strongly_measurable f μ)
(hg : measure_theory.ae_strongly_measurable g μ)
(hp : 1 ≤ p) :
measure_theory.snorm (f - g) p μ ≤ measure_theory.snorm f p μ + measure_theory.snorm g p μ
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 μ) :
measure_theory.snorm (f + g) p μ < ⊤
theorem
measure_theory.ae_le_snorm_ess_sup
{α : Type u_1}
{F : Type u_3}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group F]
{f : α → F} :
theorem
measure_theory.meas_snorm_ess_sup_lt
{α : Type u_1}
{F : Type u_3}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group F]
{f : α → F} :
theorem
measure_theory.snorm_ess_sup_map_measure
{α : Type u_1}
{E : Type u_2}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group E]
{β : Type u_5}
{mβ : measurable_space β}
{f : α → β}
{g : β → E}
(hg : measure_theory.ae_strongly_measurable g (measure_theory.measure.map f μ))
(hf : ae_measurable f μ) :
theorem
measure_theory.snorm_map_measure
{α : Type u_1}
{E : Type u_2}
{m0 : measurable_space α}
{p : ennreal}
{μ : measure_theory.measure α}
[normed_add_comm_group E]
{β : Type u_5}
{mβ : measurable_space β}
{f : α → β}
{g : β → E}
(hg : measure_theory.ae_strongly_measurable g (measure_theory.measure.map f μ))
(hf : ae_measurable f μ) :
measure_theory.snorm g p (measure_theory.measure.map f μ) = measure_theory.snorm (g ∘ f) p μ
theorem
measure_theory.mem_ℒp_map_measure_iff
{α : Type u_1}
{E : Type u_2}
{m0 : measurable_space α}
{p : ennreal}
{μ : measure_theory.measure α}
[normed_add_comm_group E]
{β : Type u_5}
{mβ : measurable_space β}
{f : α → β}
{g : β → E}
(hg : measure_theory.ae_strongly_measurable g (measure_theory.measure.map f μ))
(hf : ae_measurable f μ) :
measure_theory.mem_ℒp g p (measure_theory.measure.map f μ) ↔ measure_theory.mem_ℒp (g ∘ f) p μ
theorem
measurable_embedding.snorm_ess_sup_map_measure
{α : Type u_1}
{F : Type u_3}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group F]
{β : 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 α}
[normed_add_comm_group F]
{β : Type u_5}
{mβ : measurable_space β}
{f : α → β}
{g : β → F}
(hf : measurable_embedding f) :
measure_theory.snorm g p (measure_theory.measure.map f μ) = measure_theory.snorm (g ∘ f) p μ
theorem
measurable_embedding.mem_ℒp_map_measure_iff
{α : 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) :
measure_theory.mem_ℒp g p (measure_theory.measure.map f μ) ↔ measure_theory.mem_ℒp (g ∘ f) p μ
theorem
measurable_equiv.mem_ℒp_map_measure_iff
{α : 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} :
measure_theory.mem_ℒp g p (measure_theory.measure.map ⇑f μ) ↔ measure_theory.mem_ℒp (g ∘ ⇑f) p μ
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) :
measure_theory.snorm' f q (ν.trim hm) = measure_theory.snorm' f q ν
theorem
measure_theory.limsup_trim
{α : Type u_1}
{m m0 : measurable_space α}
{ν : measure_theory.measure α}
(hm : m ≤ m0)
{f : α → ennreal}
(hf : measurable f) :
filter.limsup f (ν.trim hm).ae = filter.limsup f ν.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) :
theorem
measure_theory.snorm_ess_sup_trim
{α : Type u_1}
{E : Type u_2}
{m m0 : measurable_space α}
{ν : measure_theory.measure α}
[normed_add_comm_group E]
(hm : m ≤ m0)
{f : α → E}
(hf : measure_theory.strongly_measurable f) :
measure_theory.snorm_ess_sup f (ν.trim hm) = measure_theory.snorm_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) :
measure_theory.snorm f p (ν.trim hm) = measure_theory.snorm f p ν
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)) :
measure_theory.snorm f p (ν.trim hm) = measure_theory.snorm f p ν
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)) :
measure_theory.mem_ℒp f p ν
@[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} :
measure_theory.snorm' (-f) q μ = measure_theory.snorm' f q μ
@[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} :
measure_theory.snorm (-f) p μ = measure_theory.snorm f p μ
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 μ) :
measure_theory.mem_ℒp (-f) p μ
theorem
measure_theory.mem_ℒp_neg_iff
{α : Type u_1}
{E : Type u_2}
{m0 : measurable_space α}
{p : ennreal}
{μ : measure_theory.measure α}
[normed_add_comm_group E]
{f : α → E} :
measure_theory.mem_ℒp (-f) p μ ↔ 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 μ) :
measure_theory.snorm' f p μ ≤ measure_theory.snorm' f q μ * ⇑μ set.univ ^ (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 α}
[normed_add_comm_group F]
(hq_pos : 0 < q)
{f : α → F} :
measure_theory.snorm' f q μ ≤ measure_theory.snorm_ess_sup f μ * ⇑μ set.univ ^ (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 α}
[normed_add_comm_group E]
{p q : ennreal}
(hpq : p ≤ q)
{f : α → E}
(hf : measure_theory.ae_strongly_measurable f μ) :
theorem
measure_theory.snorm'_le_snorm'_of_exponent_le
{α : Type u_1}
{E : Type u_2}
[normed_add_comm_group E]
{m : measurable_space α}
{p q : ℝ}
(hp0_lt : 0 < p)
(hpq : p ≤ q)
(μ : measure_theory.measure α)
[measure_theory.is_probability_measure μ]
{f : α → E}
(hf : measure_theory.ae_strongly_measurable f μ) :
measure_theory.snorm' f p μ ≤ measure_theory.snorm' f q μ
theorem
measure_theory.snorm'_le_snorm_ess_sup
{α : Type u_1}
{F : Type u_3}
{m0 : measurable_space α}
{q : ℝ}
{μ : measure_theory.measure α}
[normed_add_comm_group F]
(hq_pos : 0 < q)
{f : α → F}
[measure_theory.is_probability_measure μ] :
theorem
measure_theory.snorm_le_snorm_of_exponent_le
{α : Type u_1}
{E : Type u_2}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group E]
{p q : ennreal}
(hpq : p ≤ q)
[measure_theory.is_probability_measure μ]
{f : α → E}
(hf : measure_theory.ae_strongly_measurable f μ) :
measure_theory.snorm f p μ ≤ measure_theory.snorm f q μ
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 α}
[normed_add_comm_group E]
{p q : ℝ}
[measure_theory.is_finite_measure μ]
{f : α → E}
(hf : measure_theory.ae_strongly_measurable f μ)
(hfq_lt_top : measure_theory.snorm' f q μ < ⊤)
(hp_nonneg : 0 ≤ p)
(hpq : p ≤ q) :
measure_theory.snorm' f p μ < ⊤
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) :
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) :
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) :
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) :
theorem
measure_theory.mem_ℒp.mem_ℒp_of_exponent_le
{α : Type u_1}
{E : Type u_2}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group E]
{p q : ennreal}
[measure_theory.is_finite_measure μ]
{f : α → E}
(hfq : measure_theory.mem_ℒp f q μ)
(hpq : p ≤ q) :
measure_theory.mem_ℒp f p μ
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 μ) :
measure_theory.mem_ℒp (f + 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 μ) :
measure_theory.mem_ℒp (f - 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) :
measure_theory.snorm' f p μ ≤ c • measure_theory.snorm' g p μ
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 α}
[normed_add_comm_group F]
[normed_add_comm_group G]
{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 α}
[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) :
measure_theory.snorm f p μ ≤ c • measure_theory.snorm g p μ
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) :
measure_theory.snorm f p μ = 0 ∧ measure_theory.snorm g p μ = 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 α}
[normed_add_comm_group F]
[normed_add_comm_group G]
{f : α → F}
{g : α → G}
{c : ℝ}
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c * ‖g x‖)
(p : ennreal) :
measure_theory.snorm f p μ ≤ ennreal.of_real c * measure_theory.snorm g p μ
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‖₊) :
measure_theory.mem_ℒp f p μ
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‖) :
measure_theory.mem_ℒp f p μ
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) :
measure_theory.snorm' (c • f) q μ ≤ ‖c‖₊ • measure_theory.snorm' f q μ
theorem
measure_theory.snorm_ess_sup_const_smul_le
{α : Type u_1}
{F : Type u_3}
{m0 : measurable_space α}
{μ : 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) :
measure_theory.snorm_ess_sup (c • f) μ ≤ ‖c‖₊ • measure_theory.snorm_ess_sup f μ
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) :
measure_theory.snorm (c • f) p μ ≤ ‖c‖₊ • measure_theory.snorm f p μ
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 : 𝕜) :
measure_theory.mem_ℒp (c • f) p μ
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) :
measure_theory.snorm' (φ • f) p μ ≤ measure_theory.snorm' φ q μ * measure_theory.snorm' f r μ
theorem
measure_theory.snorm_smul_le_snorm_top_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 : ennreal)
{f : α → E}
(hf : measure_theory.ae_strongly_measurable f μ)
(φ : α → 𝕜) :
measure_theory.snorm (φ • f) p μ ≤ measure_theory.snorm φ ⊤ μ * 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 α}
[normed_add_comm_group E]
{𝕜 : Type u_5}
[normed_ring 𝕜]
[mul_action_with_zero 𝕜 E]
[has_bounded_smul 𝕜 E]
(p : ennreal)
(f : α → E)
{φ : α → 𝕜}
(hφ : measure_theory.ae_strongly_measurable φ μ) :
measure_theory.snorm (φ • f) p μ ≤ measure_theory.snorm φ p μ * measure_theory.snorm f ⊤ μ
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) :
measure_theory.snorm (φ • f) p μ ≤ measure_theory.snorm φ q μ * measure_theory.snorm f 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) :
measure_theory.mem_ℒp (φ • f) p μ
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 φ ⊤ μ) :
measure_theory.mem_ℒp (φ • f) 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 μ) :
measure_theory.mem_ℒp (φ • f) 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) :
measure_theory.snorm' (c • f) q μ = ‖c‖₊ • measure_theory.snorm' f q μ
theorem
measure_theory.snorm_ess_sup_const_smul
{α : Type u_1}
{F : Type u_3}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group F]
{𝕜 : Type u_5}
[normed_division_ring 𝕜]
[module 𝕜 F]
[has_bounded_smul 𝕜 F]
(c : 𝕜)
(f : α → F) :
measure_theory.snorm_ess_sup (c • f) μ = ↑‖c‖₊ * measure_theory.snorm_ess_sup f μ
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) :
measure_theory.snorm (c • f) p μ = ↑‖c‖₊ * measure_theory.snorm f p μ
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) :