mathlib documentation

measure_theory.function.lp_space

ℒp space and Lp space #

This file describes properties of almost everywhere strongly measurable functions with finite seminorm, denoted by snorm f p μ and defined for p:ℝ≥0∞ asmm_group (Lp E p μ) := 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 seminorm. The space Lp E p μ is the subtype of elements of α →ₘ[μ] E (see ae_eq_fun) such that snorm f p μ is finite. For 1 ≤ p, snorm defines a norm and Lp is a complete metric space.

Main definitions #

Lipschitz functions vanishing at zero act by composition on Lp. We define this action, and prove that it is continuous. In particular,

When α is a topological space equipped with a finite Borel measure, there is a bounded linear map from the normed space of bounded continuous functions (α →ᵇ E) to Lp E p μ. We construct this as bounded_continuous_function.to_Lp.

Notations #

Implementation #

Since Lp is defined as an add_subgroup, dot notation does not work. Use Lp.measurable f to say that the coercion of f to a genuine function is measurable, instead of the non-working f.measurable.

To prove that two Lp elements are equal, it suffices to show that their coercions to functions coincide almost everywhere (this is registered as an ext rule). This can often be done using filter_upwards. For instance, a proof from first principles that f + (g + h) = (f + g) + h could read (in the Lp namespace)

example (f g h : Lp E p μ) : (f + g) + h = f + (g + h) :=
begin
  ext1,
  filter_upwards [coe_fn_add (f + g) h, coe_fn_add f g, coe_fn_add f (g + h), coe_fn_add g h]
    with _ ha1 ha2 ha3 ha4,
  simp only [ha1, ha2, ha3, ha4, add_assoc],
end

The lemma coe_fn_add states that the coercion of f + g coincides almost everywhere with the sum of the coercions of f and g. All such lemmas use coe_fn in their name, to distinguish the function coercion from the coercion to almost everywhere defined functions.

ℒ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 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_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_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_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 {α : 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_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_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_lt_top_of_one_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.mem_ℒp f p μ) (hg : measure_theory.mem_ℒp g p μ) (hq1 : 1 p) :
theorem measure_theory.snorm'_add_lt_top_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 μ) (hf_snorm : measure_theory.snorm' f q μ < ) (hg_snorm : measure_theory.snorm' g q μ < ) (hq_pos : 0 < q) (hq1 : q 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'_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_field 𝕜] [normed_space 𝕜 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_field 𝕜] [normed_space 𝕜 F] {f : α F} (c : 𝕜) :
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_field 𝕜] [normed_space 𝕜 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 α} {𝕜 : Type u_5} [normed_field 𝕜] {f : α 𝕜} (hf : measure_theory.mem_ℒp f p μ) (c : 𝕜) :
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_field 𝕜] [normed_space 𝕜 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_field 𝕜] [normed_space 𝕜 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_field 𝕜] [normed_space 𝕜 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_field 𝕜] [normed_space 𝕜 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_field 𝕜] [normed_space 𝕜 E] {p : ennreal} {f : α E} {φ : α 𝕜} (hf : measure_theory.mem_ℒp f μ) (hφ : measure_theory.mem_ℒp φ p μ) :
theorem measure_theory.snorm_le_mul_snorm_aux_of_nonneg {α : 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 : 0 c) (p : ennreal) :
theorem measure_theory.snorm_le_mul_snorm_aux_of_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) :
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_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_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.mem_ℒp.const_inner {α : Type u_1} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {E' : Type u_5} {𝕜 : Type u_6} [is_R_or_C 𝕜] [normed_add_comm_group E'] [inner_product_space 𝕜 E'] (c : E') {f : α E'} (hf : measure_theory.mem_ℒp f p μ) :
measure_theory.mem_ℒp (λ (a : α), has_inner.inner c (f a)) p μ
theorem measure_theory.mem_ℒp.inner_const {α : Type u_1} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {E' : Type u_5} {𝕜 : Type u_6} [is_R_or_C 𝕜] [normed_add_comm_group E'] [inner_product_space 𝕜 E'] {f : α E'} (hf : measure_theory.mem_ℒp f p μ) (c : E') :
measure_theory.mem_ℒp (λ (a : α), has_inner.inner (f a) c) 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) :

Lp space #

The space of equivalence classes of measurable functions for which snorm f p μ < ∞.

def measure_theory.mem_ℒp.to_Lp {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] (f : α E) (h_mem_ℒp : measure_theory.mem_ℒp f p μ) :

make an element of Lp from a function verifying mem_ℒp

Equations
@[protected, instance]
noncomputable def measure_theory.Lp.has_coe_to_fun {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] :
has_coe_to_fun (measure_theory.Lp E p μ) (λ (_x : (measure_theory.Lp E p μ)), α E)
Equations
@[ext]
theorem measure_theory.Lp.ext {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] {f g : (measure_theory.Lp E p μ)} (h : f =ᵐ[μ] g) :
f = g
theorem measure_theory.Lp.ext_iff {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] {f g : (measure_theory.Lp E p μ)} :
f = g f =ᵐ[μ] g
@[protected]
@[simp]
theorem measure_theory.Lp.coe_fn_mk {α : 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.snorm f p μ < ) :
f, hf⟩ = f
@[simp]
theorem measure_theory.Lp.coe_mk {α : 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.snorm f p μ < ) :
f, hf⟩ = f
@[protected, measurability]
@[protected, measurability]
@[protected]
theorem measure_theory.Lp.coe_fn_add {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] (f g : (measure_theory.Lp E p μ)) :
(f + g) =ᵐ[μ] f + g
theorem measure_theory.Lp.coe_fn_sub {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] (f g : (measure_theory.Lp E p μ)) :
(f - g) =ᵐ[μ] f - g
@[protected, instance]
noncomputable def measure_theory.Lp.has_norm {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] :
Equations
@[protected, instance]
noncomputable def measure_theory.Lp.has_dist {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] :
Equations
@[protected, instance]
noncomputable def measure_theory.Lp.has_edist {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] :
Equations
@[simp]
theorem measure_theory.Lp.norm_zero {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] :
theorem measure_theory.Lp.norm_eq_zero_iff {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] {f : (measure_theory.Lp E p μ)} (hp : 0 < p) :
f = 0 f = 0
@[simp]
theorem measure_theory.Lp.norm_neg {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] {f : (measure_theory.Lp E p μ)} :
theorem measure_theory.Lp.norm_le_mul_norm_of_ae_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] {c : } {f : (measure_theory.Lp E p μ)} {g : (measure_theory.Lp F p μ)} (h : ∀ᵐ (x : α) μ, f x c * g x) :
theorem measure_theory.Lp.mem_Lp_of_ae_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] {c : } {f : α →ₘ[μ] E} {g : (measure_theory.Lp F p μ)} (h : ∀ᵐ (x : α) μ, f x c * g x) :
theorem measure_theory.Lp.mem_Lp_of_ae_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 : (measure_theory.Lp F p μ)} (h : ∀ᵐ (x : α) μ, f x g x) :
theorem measure_theory.Lp.mem_Lp_of_ae_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} (C : ) (hfC : ∀ᵐ (x : α) μ, f x C) :
theorem measure_theory.Lp.mem_Lp_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_field 𝕜] [normed_space 𝕜 E] (c : 𝕜) (f : (measure_theory.Lp E p μ)) :
def measure_theory.Lp.Lp_submodule {α : Type u_1} (E : Type u_2) {m0 : measurable_space α} (p : ennreal) (μ : measure_theory.measure α) [normed_add_comm_group E] (𝕜 : Type u_5) [normed_field 𝕜] [normed_space 𝕜 E] :
submodule 𝕜 →ₘ[μ] E)

The 𝕜-submodule of elements of α →ₘ[μ] E whose Lp norm is finite. This is Lp E p μ, with extra structure.

Equations
theorem measure_theory.Lp.coe_fn_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_field 𝕜] [normed_space 𝕜 E] (c : 𝕜) (f : (measure_theory.Lp E p μ)) :
(c f) =ᵐ[μ] c f
theorem measure_theory.Lp.norm_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_field 𝕜] [normed_space 𝕜 E] (c : 𝕜) (f : (measure_theory.Lp E p μ)) :
@[protected, instance]
def measure_theory.Lp.normed_space {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] {𝕜 : Type u_5} [normed_field 𝕜] [normed_space 𝕜 E] [fact (1 p)] :
Equations
theorem measure_theory.mem_ℒp.to_Lp_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_field 𝕜] [normed_space 𝕜 E] {f : α E} (c : 𝕜) (hf : measure_theory.mem_ℒp f p μ) :

Indicator of a set as an element of Lᵖ #

For a set s with (hs : measurable_set s) and (hμs : μ s < ∞), we build indicator_const_Lp p hs hμs c, the element of Lp corresponding to s.indicator (λ x, c).

theorem measure_theory.snorm_ess_sup_indicator_const_eq {α : Type u_1} {G : Type u_4} {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_add_comm_group G] (s : set α) (c : G) (hμs : μ s 0) :
theorem measure_theory.snorm_indicator_le {α : Type u_1} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {s : set α} {E : Type u_2} [normed_add_comm_group E] (f : α E) :
theorem measure_theory.snorm_indicator_const {α : Type u_1} {G : Type u_4} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group G] {s : set α} {c : G} (hs : measurable_set s) (hp : p 0) (hp_top : p ) :
measure_theory.snorm (s.indicator (λ (x : α), c)) p μ = c‖₊ * μ s ^ (1 / p.to_real)
theorem measure_theory.snorm_indicator_const' {α : Type u_1} {G : Type u_4} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group G] {s : set α} {c : G} (hs : measurable_set s) (hμs : μ s 0) (hp : p 0) :
measure_theory.snorm (s.indicator (λ (_x : α), c)) p μ = c‖₊ * μ s ^ (1 / p.to_real)
theorem measure_theory.mem_ℒp.indicator {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] {s : set α} {f : α E} (hs : measurable_set s) (hf : measure_theory.mem_ℒp f p μ) :
theorem measure_theory.mem_ℒp_indicator_const {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_add_comm_group E] {s : set α} (p : ennreal) (hs : measurable_set s) (c : E) (hμsc : c = 0 μ s ) :
measure_theory.mem_ℒp (s.indicator (λ (_x : α), c)) p μ
noncomputable def measure_theory.indicator_const_Lp {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_add_comm_group E] {s : set α} (p : ennreal) (hs : measurable_set s) (hμs : μ s ) (c : E) :

Indicator of a set as an element of Lp.

Equations
theorem measure_theory.indicator_const_Lp_coe_fn {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] {s : set α} {hs : measurable_set s} {hμs : μ s } {c : E} :
(measure_theory.indicator_const_Lp p hs hμs c) =ᵐ[μ] s.indicator (λ (_x : α), c)
theorem measure_theory.indicator_const_Lp_coe_fn_mem {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] {s : set α} {hs : measurable_set s} {hμs : μ s } {c : E} :
∀ᵐ (x : α) μ, x s (measure_theory.indicator_const_Lp p hs hμs c) x = c
theorem measure_theory.indicator_const_Lp_coe_fn_nmem {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] {s : set α} {hs : measurable_set s} {hμs : μ s } {c : E} :
∀ᵐ (x : α) μ, x s (measure_theory.indicator_const_Lp p hs hμs c) x = 0
theorem measure_theory.norm_indicator_const_Lp {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] {s : set α} {hs : measurable_set s} {hμs : μ s } {c : E} (hp_ne_zero : p 0) (hp_ne_top : p ) :
theorem measure_theory.norm_indicator_const_Lp_top {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_add_comm_group E] {s : set α} {hs : measurable_set s} {hμs : μ s } {c : E} (hμs_ne_zero : μ s 0) :
theorem measure_theory.norm_indicator_const_Lp' {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] {s : set α} {hs : measurable_set s} {hμs : μ s } {c : E} (hp_pos : p 0) (hμs_pos : μ s 0) :
theorem measure_theory.indicator_const_Lp_disjoint_union {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] {s t : set α} (hs : measurable_set s) (ht : measurable_set t) (hμs : μ s ) (hμt : μ t ) (hst : s t = ) (c : E) :

The indicator of a disjoint union of two sets is the sum of the indicators of the sets.

theorem measure_theory.mem_ℒp.norm_rpow_div {α : 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 μ) (q : ennreal) :
measure_theory.mem_ℒp (λ (x : α), f x ^ q.to_real) (p / q) μ
theorem measure_theory.mem_ℒp_norm_rpow_iff {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] {q : ennreal} {f : α E} (hf : measure_theory.ae_strongly_measurable f μ) (q_zero : q 0) (q_top : q ) :
theorem measure_theory.mem_ℒp.norm_rpow {α : 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 μ) (hp_ne_zero : p 0) (hp_ne_top : p ) :
measure_theory.mem_ℒp (λ (x : α), f x ^ p.to_real) 1 μ

Composition on L^p #

We show that Lipschitz functions vanishing at zero act by composition on L^p, and specialize this to the composition with continuous linear maps, and to the definition of the positive part of an L^p function.

theorem lipschitz_with.comp_mem_ℒp {p : ennreal} {α : Type u_1} {E : Type u_2} {F : Type u_3} {K : nnreal} [measurable_space α] {μ : measure_theory.measure α} [normed_add_comm_group E] [normed_add_comm_group F] {f : α E} {g : E F} (hg : lipschitz_with K g) (g0 : g 0 = 0) (hL : measure_theory.mem_ℒp f p μ) :
theorem measure_theory.mem_ℒp.of_comp_antilipschitz_with {p : ennreal} {α : Type u_1} {E : Type u_2} {F : Type u_3} {K' : nnreal} [measurable_space α] {μ : measure_theory.measure α} [normed_add_comm_group E] [normed_add_comm_group F] {f : α E} {g : E F} (hL : measure_theory.mem_ℒp (g f) p μ) (hg : uniform_continuous g) (hg' : antilipschitz_with K' g) (g0 : g 0 = 0) :
theorem lipschitz_with.mem_ℒp_comp_iff_of_antilipschitz {p : ennreal} {α : Type u_1} {E : Type u_2} {F : Type u_3} {K K' : nnreal} [measurable_space α] {μ : measure_theory.measure α} [normed_add_comm_group E] [normed_add_comm_group F] {f : α E} {g : E F} (hg : lipschitz_with K g) (hg' : antilipschitz_with K' g) (g0 : g 0 = 0) :
def lipschitz_with.comp_Lp {α : 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] {g : E F} {c : nnreal} (hg : lipschitz_with c g) (g0 : g 0 = 0) (f : (measure_theory.Lp E p μ)) :

When g is a Lipschitz function sending 0 to 0 and f is in Lp, then gf is well defined as an element of Lp.

Equations
theorem lipschitz_with.coe_fn_comp_Lp {α : 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] {g : E F} {c : nnreal} (hg : lipschitz_with c g) (g0 : g 0 = 0) (f : (measure_theory.Lp E p μ)) :
(hg.comp_Lp g0 f) =ᵐ[μ] g f