mathlib documentation

measure_theory.function.lp_space

ℒp space and Lp space #

This file describes properties of almost everywhere measurable functions with finite 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 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],
  assume a 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.

def measure_theory.snorm' {α : Type u_1} {F : Type u_3} [normed_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
def measure_theory.snorm_ess_sup {α : Type u_1} {F : Type u_3} [normed_group F] {m : measurable_space α} (f : α → F) (μ : measure_theory.measure α) :

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

Equations
def measure_theory.snorm {α : Type u_1} {F : Type u_3} [normed_group F] {m : measurable_space α} (f : α → F) (p : ℝ≥0∞) (μ : 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 : ℝ≥0∞} {μ : measure_theory.measure α} [normed_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 : ℝ≥0∞} {μ : measure_theory.measure α} [normed_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)
theorem measure_theory.snorm_one_eq_lintegral_nnnorm {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_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_group F] {f : α → F} :
def measure_theory.mem_ℒp {E : Type u_2} [measurable_space E] [normed_group E] {α : Type u_1} {m : measurable_space α} (f : α → E) (p : ℝ≥0∞) (μ : measure_theory.measure α) :
Prop

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

Equations
theorem measure_theory.mem_ℒp.ae_measurable {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] {f : α → E} {p : ℝ≥0∞} (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_group F] {f : α → F} (hq0_lt : 0 < q) :
∫⁻ (a : α), f a∥₊ ^ q μ = measure_theory.snorm' f q μ ^ q
theorem measure_theory.mem_ℒp.snorm_lt_top {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] {f : α → E} (hfp : measure_theory.mem_ℒp f p μ) :
theorem measure_theory.mem_ℒp.snorm_ne_top {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] {f : α → E} (hfp : measure_theory.mem_ℒp 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_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 : ℝ≥0∞} {μ : measure_theory.measure α} [normed_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 : ℝ≥0∞} {μ : measure_theory.measure α} [normed_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_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_group F] {f : α → F} :
theorem measure_theory.mem_ℒp_zero_iff_ae_measurable {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} [measurable_space E] [normed_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_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_group F] (hq0_ne : q 0) (hμ : μ 0) :
@[simp]
theorem measure_theory.snorm_ess_sup_zero {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_group F] :
@[simp]
theorem measure_theory.snorm_zero {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group F] :
@[simp]
theorem measure_theory.snorm_zero' {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_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 : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] :
theorem measure_theory.zero_mem_ℒp' {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_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_group F] [measurable_space α] {f : α → F} (hq_pos : 0 < q) :
theorem measure_theory.snorm'_measure_zero_of_exponent_zero {α : Type u_1} {F : Type u_3} [normed_group F] [measurable_space α] {f : α → F} :
theorem measure_theory.snorm'_measure_zero_of_neg {α : Type u_1} {F : Type u_3} {q : } [normed_group F] [measurable_space α] {f : α → F} (hq_neg : q < 0) :
@[simp]
theorem measure_theory.snorm_ess_sup_measure_zero {α : Type u_1} {F : Type u_3} [normed_group F] [measurable_space α] {f : α → F} :
@[simp]
theorem measure_theory.snorm_measure_zero {α : Type u_1} {F : Type u_3} {p : ℝ≥0∞} [normed_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_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_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_group F] (c : F) (hμ : μ 0) :
theorem measure_theory.snorm'_const_of_is_probability_measure {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {q : } {μ : measure_theory.measure α} [normed_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 : ℝ≥0∞} {μ : measure_theory.measure α} [normed_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 : ℝ≥0∞} {μ : measure_theory.measure α} [normed_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_group F] {p : ℝ≥0∞} {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_const {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] (c : E) [measure_theory.is_finite_measure μ] :
measure_theory.mem_ℒp (λ (a : α), c) p μ
theorem measure_theory.mem_ℒp_const_iff {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] {p : ℝ≥0∞} {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_group F] [normed_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_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_group F] {f g : α → F} (hfg : f =ᵐ[μ] g) :
theorem measure_theory.snorm_ess_sup_congr_ae {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_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 : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group F] [normed_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 : ℝ≥0∞} {μ : measure_theory.measure α} [normed_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 : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group F] [normed_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 : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group F] {f : α → F} {g : α → } (h : ∀ (x : α), f x g x) :
theorem measure_theory.snorm_ess_sup_le_of_ae_bound {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_group F] {f : α → F} {C : } (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_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 : ℝ≥0∞} {μ : measure_theory.measure α} [normed_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 : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group F] [normed_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_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 : ℝ≥0∞} {μ : measure_theory.measure α} [normed_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_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 : ℝ≥0∞} {q : } {μ : measure_theory.measure α} [normed_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 : ℝ≥0∞} {μ : measure_theory.measure α} [normed_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 : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_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 : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_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 : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [normed_group F] [measurable_space F] {f : α → E} {g : α → F} (hg : measure_theory.mem_ℒp g p μ) (hf : ae_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 : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [normed_group F] [measurable_space F] {f : α → E} {g : α → F} (hg : measure_theory.mem_ℒp g p μ) (hf : ae_measurable f μ) (hfg : ∀ᵐ (x : α) ∂μ, f x g x) :

Alias of mem_ℒp.of_le.

theorem measure_theory.mem_ℒp.mono' {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] {f : α → E} {g : α → } (hg : measure_theory.mem_ℒp g p μ) (hf : ae_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 : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [normed_group F] [measurable_space F] {f : α → E} {g : α → F} (hf : measure_theory.mem_ℒp f p μ) (hg : ae_measurable g μ) (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 : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [normed_group F] [measurable_space F] {f : α → E} {g : α → F} (hf : ae_measurable f μ) (hg : ae_measurable g μ) (h : ∀ᵐ (a : α) ∂μ, f a = g a) :
theorem measure_theory.mem_ℒp_top_of_bound {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] {f : α → E} (hf : ae_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 : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [measure_theory.is_finite_measure μ] {f : α → E} (hf : ae_measurable f μ) (C : ) (hfC : ∀ᵐ (x : α) ∂μ, f x C) :
theorem measure_theory.snorm'_mono_measure {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {q : } {μ ν : measure_theory.measure α} [normed_group F] (f : α → F) (hμν : ν μ) (hq : 0 q) :
theorem measure_theory.snorm_ess_sup_mono_measure {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {μ ν : measure_theory.measure α} [normed_group F] (f : α → F) (hμν : ν μ) :
theorem measure_theory.snorm_mono_measure {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {p : ℝ≥0∞} {μ ν : measure_theory.measure α} [normed_group F] (f : α → F) (hμν : ν μ) :
theorem measure_theory.mem_ℒp.mono_measure {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ℝ≥0∞} {μ ν : measure_theory.measure α} [measurable_space E] [normed_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 : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_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_group F] {p : } (hp : 0 p) {f : α → F} (c : ℝ≥0∞) :
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_group F] {f : α → F} {c : ℝ≥0∞} (hc : c 0) :
theorem measure_theory.snorm_smul_measure_of_ne_zero {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_group F] {p : ℝ≥0∞} {f : α → F} {c : ℝ≥0∞} (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_group F] {p : ℝ≥0∞} (hp_ne_top : p ) {f : α → F} (c : ℝ≥0∞) :
theorem measure_theory.snorm_one_smul_measure {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_group F] {f : α → F} (c : ℝ≥0∞) :
theorem measure_theory.mem_ℒp.norm {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [opens_measurable_space 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 : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [opens_measurable_space E] {f : α → E} (hf : ae_measurable f μ) :
theorem measure_theory.snorm'_eq_zero_of_ae_zero {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {q : } {μ : measure_theory.measure α} [normed_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_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 α} [measurable_space E] [normed_group E] [opens_measurable_space E] {f : α → E} (hq0 : 0 q) (hf : ae_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 α} [measurable_space E] [normed_group E] [opens_measurable_space E] (hq0_lt : 0 < q) {f : α → E} (hf : ae_measurable f μ) :
theorem measure_theory.coe_nnnorm_ae_le_snorm_ess_sup {α : Type u_1} {F : Type u_3} [normed_group F] {m : measurable_space α} (f : α → F) (μ : measure_theory.measure α) :
∀ᵐ (x : α) ∂μ, f x∥₊ measure_theory.snorm_ess_sup f μ
@[simp]
theorem measure_theory.snorm_ess_sup_eq_zero_iff {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_group F] {f : α → F} :
theorem measure_theory.snorm_eq_zero_iff {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [opens_measurable_space E] {f : α → E} (hf : ae_measurable f μ) (h0 : p 0) :
theorem measure_theory.snorm'_add_le {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {q : } {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [opens_measurable_space E] {f g : α → E} (hf : ae_measurable f μ) (hg : ae_measurable g μ) (hq1 : 1 q) :
theorem measure_theory.snorm_add_le {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [opens_measurable_space E] {f g : α → E} (hf : ae_measurable f μ) (hg : ae_measurable g μ) (hp1 : 1 p) :
theorem measure_theory.snorm_sub_le {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [opens_measurable_space E] {f g : α → E} (hf : ae_measurable f μ) (hg : ae_measurable g μ) (hp1 : 1 p) :
theorem measure_theory.snorm_add_lt_top_of_one_le {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [opens_measurable_space 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 α} [measurable_space E] [normed_group E] [opens_measurable_space E] {f g : α → E} (hf : ae_measurable f μ) (hg : ae_measurable g μ) (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 : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [opens_measurable_space E] {f g : α → E} (hf : measure_theory.mem_ℒp f p μ) (hg : measure_theory.mem_ℒp g p μ) :
theorem measure_theory.snorm'_trim {α : Type u_1} {E : Type u_2} {m m0 : measurable_space α} {q : } {ν : measure_theory.measure α} [measurable_space E] [normed_group E] [opens_measurable_space E] (hm : m m0) {f : α → E} (hf : measurable f) :
theorem measure_theory.limsup_trim {α : Type u_1} {m m0 : measurable_space α} {ν : measure_theory.measure α} (hm : m m0) {f : α → ℝ≥0∞} (hf : measurable f) :
(ν.trim hm).ae.limsup f = ν.ae.limsup f
theorem measure_theory.ess_sup_trim {α : Type u_1} {m m0 : measurable_space α} {ν : measure_theory.measure α} (hm : m m0) {f : α → ℝ≥0∞} (hf : measurable f) :
ess_sup f (ν.trim hm) = ess_sup f ν
theorem measure_theory.snorm_ess_sup_trim {α : Type u_1} {E : Type u_2} {m m0 : measurable_space α} {ν : measure_theory.measure α} [measurable_space E] [normed_group E] [opens_measurable_space E] (hm : m m0) {f : α → E} (hf : measurable f) :
theorem measure_theory.snorm_trim {α : Type u_1} {E : Type u_2} {m m0 : measurable_space α} {p : ℝ≥0∞} {ν : measure_theory.measure α} [measurable_space E] [normed_group E] [opens_measurable_space E] (hm : m m0) {f : α → E} (hf : measurable f) :
theorem measure_theory.snorm_trim_ae {α : Type u_1} {E : Type u_2} {m m0 : measurable_space α} {p : ℝ≥0∞} {ν : measure_theory.measure α} [measurable_space E] [normed_group E] [opens_measurable_space E] (hm : m m0) {f : α → E} (hf : ae_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 : ℝ≥0∞} {ν : measure_theory.measure α} [measurable_space E] [normed_group E] [opens_measurable_space 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_group F] {f : α → F} :
@[simp]
theorem measure_theory.snorm_neg {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group F] {f : α → F} :
theorem measure_theory.mem_ℒp.neg {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [borel_space E] {f : α → E} (hf : measure_theory.mem_ℒp f p μ) :
theorem measure_theory.mem_ℒp_neg_iff {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [borel_space E] {f : α → E} :
theorem measure_theory.snorm'_le_snorm'_mul_rpow_measure_univ {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [borel_space E] {p q : } (hp0_lt : 0 < p) (hpq : p q) {f : α → E} (hf : ae_measurable f μ) :
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_group F] (hq_pos : 0 < q) {f : α → F} :
theorem measure_theory.snorm_le_snorm_mul_rpow_measure_univ {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [borel_space E] {p q : ℝ≥0∞} (hpq : p q) {f : α → E} (hf : ae_measurable f μ) :
theorem measure_theory.snorm'_le_snorm'_of_exponent_le {α : Type u_1} {E : Type u_2} [measurable_space E] [normed_group E] [borel_space E] {m : measurable_space α} {p q : } (hp0_lt : 0 < p) (hpq : p q) (μ : measure_theory.measure α) [measure_theory.is_probability_measure μ] {f : α → E} (hf : ae_measurable f μ) :
theorem measure_theory.snorm'_le_snorm_ess_sup {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {q : } {μ : measure_theory.measure α} [normed_group F] (hq_pos : 0 < q) {f : α → F} [measure_theory.is_probability_measure μ] :
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 α} [measurable_space E] [normed_group E] [borel_space E] {p q : } [measure_theory.is_finite_measure μ] {f : α → E} (hf : ae_measurable f μ) (hfq_lt_top : measure_theory.snorm' f q μ < ) (hp_nonneg : 0 p) (hpq : p q) :
theorem measure_theory.mem_ℒp.mem_ℒp_of_exponent_le {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [borel_space E] {p q : ℝ≥0∞} [measure_theory.is_finite_measure μ] {f : α → E} (hfq : measure_theory.mem_ℒp f q μ) (hpq : p q) :
theorem measure_theory.snorm'_sum_le {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {q : } {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [borel_space E] [topological_space.second_countable_topology E] {ι : Type u_3} {f : ι → α → E} {s : finset ι} (hfs : ∀ (i : ι), i sae_measurable (f i) μ) (hq1 : 1 q) :
measure_theory.snorm' (∑ (i : ι) in s, f i) q μ ∑ (i : ι) in s, measure_theory.snorm' (f i) q μ
theorem measure_theory.snorm_sum_le {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [borel_space E] [topological_space.second_countable_topology E] {ι : Type u_3} {f : ι → α → E} {s : finset ι} (hfs : ∀ (i : ι), i sae_measurable (f i) μ) (hp1 : 1 p) :
measure_theory.snorm (∑ (i : ι) in s, f i) p μ ∑ (i : ι) in s, measure_theory.snorm (f i) p μ
theorem measure_theory.mem_ℒp_finset_sum {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [borel_space E] [topological_space.second_countable_topology E] {ι : Type u_3} (s : finset ι) {f : ι → α → E} (hf : ∀ (i : ι), i smeasure_theory.mem_ℒp (f i) p μ) :
measure_theory.mem_ℒp (λ (a : α), ∑ (i : ι) in s, f i a) p μ
theorem measure_theory.snorm'_const_smul {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {q : } {μ : measure_theory.measure α} [normed_group F] {𝕜 : Type u_5} [normed_field 𝕜] [normed_space 𝕜 F] {f : α → F} (c : 𝕜) (hq_pos : 0 < q) :
theorem measure_theory.snorm_ess_sup_const_smul {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_group F] {𝕜 : Type u_5} [normed_field 𝕜] [normed_space 𝕜 F] {f : α → F} (c : 𝕜) :
theorem measure_theory.snorm_const_smul {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_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 : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] {𝕜 : Type u_5} [normed_field 𝕜] [normed_space 𝕜 E] [measurable_space 𝕜] [opens_measurable_space 𝕜] [borel_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 : ℝ≥0∞} {μ : measure_theory.measure α} {𝕜 : Type u_5} [normed_field 𝕜] [measurable_space 𝕜] [borel_space 𝕜] {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 α} [measurable_space E] [normed_group E] {𝕜 : Type u_5} [normed_field 𝕜] [normed_space 𝕜 E] [opens_measurable_space E] [measurable_space 𝕜] [opens_measurable_space 𝕜] {p q r : } {f : α → E} (hf : ae_measurable f μ) {φ : α → 𝕜} (hφ : ae_measurable φ μ) (hp0_lt : 0 < p) (hpq : p < q) (hpqr : 1 / p = 1 / q + 1 / r) :
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_group F] [normed_group G] {f : α → F} {g : α → G} {c : } (h : ∀ᵐ (x : α) ∂μ, f x c * g x) (hc : 0 c) (p : ℝ≥0∞) :
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_group F] [normed_group G] {f : α → F} {g : α → G} {c : } (h : ∀ᵐ (x : α) ∂μ, f x c * g x) (hc : c < 0) (p : ℝ≥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_group F] [normed_group G] {f : α → F} {g : α → G} {c : } (h : ∀ᵐ (x : α) ∂μ, f x c * g x) (p : ℝ≥0∞) :
theorem measure_theory.mem_ℒp.of_le_mul {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : measurable_space α} {p : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [normed_group F] [measurable_space F] {f : α → E} {g : α → F} {c : } (hg : measure_theory.mem_ℒp g p μ) (hf : ae_measurable f μ) (hfg : ∀ᵐ (x : α) ∂μ, f x c * g x) :
theorem measure_theory.mem_ℒp.re {α : Type u_1} {m0 : measurable_space α} {p : ℝ≥0∞} {μ : measure_theory.measure α} {𝕜 : Type u_5} [is_R_or_C 𝕜] [measurable_space 𝕜] [opens_measurable_space 𝕜] {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 : ℝ≥0∞} {μ : measure_theory.measure α} {𝕜 : Type u_5} [is_R_or_C 𝕜] [measurable_space 𝕜] [opens_measurable_space 𝕜] {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 : ℝ≥0∞} {μ : measure_theory.measure α} {E' : Type u_5} {𝕜 : Type u_6} [is_R_or_C 𝕜] [measurable_space 𝕜] [borel_space 𝕜] [inner_product_space 𝕜 E'] [measurable_space E'] [opens_measurable_space E'] [topological_space.second_countable_topology E'] (c : E') {f : α → E'} (hf : measure_theory.mem_ℒp f p μ) :
measure_theory.mem_ℒp (λ (a : α), inner c (f a)) p μ
theorem measure_theory.mem_ℒp.inner_const {α : Type u_1} {m0 : measurable_space α} {p : ℝ≥0∞} {μ : measure_theory.measure α} {E' : Type u_5} {𝕜 : Type u_6} [is_R_or_C 𝕜] [measurable_space 𝕜] [borel_space 𝕜] [inner_product_space 𝕜 E'] [measurable_space E'] [opens_measurable_space E'] [topological_space.second_countable_topology E'] {f : α → E'} (hf : measure_theory.mem_ℒp f p μ) (c : E') :
measure_theory.mem_ℒp (λ (a : α), inner (f a) c) p μ

Lp space #

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

@[simp]
theorem measure_theory.snorm_ae_eq_fun {α : Type u_1} {E : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [measurable_space E] [normed_group E] {p : ℝ≥0∞} {f : α → E} (hf : ae_measurable f μ) :

Lp space

Equations
def measure_theory.mem_ℒp.to_Lp {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [borel_space E] [topological_space.second_countable_topology E] (f : α → E) (h_mem_ℒp : measure_theory.mem_ℒp f p μ) :

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

Equations
@[ext]
theorem measure_theory.Lp.ext {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [borel_space E] [topological_space.second_countable_topology E] {f g : (measure_theory.Lp E p μ)} (h : f =ᵐ[μ] g) :
f = g
@[simp]
theorem measure_theory.Lp.coe_fn_mk {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [borel_space E] [topological_space.second_countable_topology 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 : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [borel_space E] [topological_space.second_countable_topology E] {f : α →ₘ[μ] E} (hf : measure_theory.snorm f p μ < ) :
f, hf⟩ = f
theorem measure_theory.Lp.mem_Lp_of_ae_bound {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [borel_space E] [topological_space.second_countable_topology E] [measure_theory.is_finite_measure μ] {f : α →ₘ[μ] E} (C : ) (hfC : ∀ᵐ (x : α) ∂μ, f x C) :
@[instance]
Equations
theorem measure_theory.Lp.mem_Lp_const_smul {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [borel_space E] [topological_space.second_countable_topology E] {𝕜 : Type u_5} [normed_field 𝕜] [normed_space 𝕜 E] [measurable_space 𝕜] [opens_measurable_space 𝕜] (c : 𝕜) (f : (measure_theory.Lp E p μ)) :

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 : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [borel_space E] [topological_space.second_countable_topology E] {𝕜 : Type u_5} [normed_field 𝕜] [normed_space 𝕜 E] [measurable_space 𝕜] [opens_measurable_space 𝕜] (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 : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [borel_space E] [topological_space.second_countable_topology E] {𝕜 : Type u_5} [normed_field 𝕜] [normed_space 𝕜 E] [measurable_space 𝕜] [opens_measurable_space 𝕜] (c : 𝕜) (f : (measure_theory.Lp E 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_le {α : Type u_1} {G : Type u_4} {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_group G] (s : set α) (f : α → G) :
theorem measure_theory.snorm_ess_sup_indicator_const_le {α : Type u_1} {G : Type u_4} {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_group G] (s : set α) (c : G) :
theorem measure_theory.snorm_ess_sup_indicator_const_eq {α : Type u_1} {G : Type u_4} {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_group G] (s : set α) (c : G) (hμs : μ s 0) :
theorem measure_theory.snorm_indicator_le {α : Type u_1} {m0 : measurable_space α} {p : ℝ≥0∞} {μ : measure_theory.measure α} {s : set α} {E : Type u_2} [normed_group E] (f : α → E) :
theorem measure_theory.snorm_indicator_const {α : Type u_1} {G : Type u_4} {m0 : measurable_space α} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_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 : ℝ≥0∞} {μ : measure_theory.measure α} [normed_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 : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] {s : set α} {f : α → E} (hs : measurable_set s) (hf : measure_theory.mem_ℒp f p μ) :
theorem measure_theory.snorm_indicator_eq_snorm_restrict {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group F] {s : set α} {f : α → F} (hs : measurable_set s) :
theorem measure_theory.mem_ℒp_indicator_iff_restrict {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] {s : set α} {f : α → E} (hs : measurable_set s) :
theorem measure_theory.mem_ℒp_indicator_const {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] {s : set α} (p : ℝ≥0∞) (hs : measurable_set s) (c : E) (hμsc : c = 0 μ s ) :
measure_theory.mem_ℒp (s.indicator (λ (_x : α), c)) p μ
def measure_theory.indicator_const_Lp {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] {s : set α} [borel_space E] [topological_space.second_countable_topology E] (p : ℝ≥0∞) (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 : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] {s : set α} {hs : measurable_set s} {hμs : μ s } {c : E} [borel_space E] [topological_space.second_countable_topology 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 : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] {s : set α} {hs : measurable_set s} {hμs : μ s } {c : E} [borel_space E] [topological_space.second_countable_topology 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 : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] {s : set α} {hs : measurable_set s} {hμs : μ s } {c : E} [borel_space E] [topological_space.second_countable_topology 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 : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] {s : set α} {hs : measurable_set s} {hμs : μ s } {c : E} [borel_space E] [topological_space.second_countable_topology 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 α} [measurable_space E] [normed_group E] {s : set α} {hs : measurable_set s} {hμs : μ s } {c : E} [borel_space E] [topological_space.second_countable_topology 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 : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] {s : set α} {hs : measurable_set s} {hμs : μ s } {c : E} [borel_space E] [topological_space.second_countable_topology E] (hp_pos : p 0) (hμs_pos : μ s 0) :

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

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.mem_ℒp_comp_iff_of_antilipschitz {p : ℝ≥0∞} {α : Type u_1} {E : Type u_2} {F : Type u_3} {K K' : ℝ≥0} [measurable_space α] {μ : measure_theory.measure α} [measurable_space E] [measurable_space F] [normed_group E] [normed_group F] [borel_space E] [borel_space F] [complete_space E] {f : α → E} {g : E → F} (hg : lipschitz_with K g) (hg' : antilipschitz_with K' g) (g0 : g 0 = 0) :

When g is a Lipschitz function sending 0 to 0 and f is in Lp, then g ∘ f 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 : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [normed_group F] [topological_space.second_countable_topology E] [borel_space E] [topological_space.second_countable_topology F] [measurable_space F] [borel_space F] {g : E → F} {c : ℝ≥0} (hg : lipschitz_with c g) (g0 : g 0 = 0) (f : (measure_theory.Lp E p μ)) :
(hg.comp_Lp g0 f) =ᵐ[μ] g f
@[simp]
theorem lipschitz_with.comp_Lp_zero {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : measurable_space α} {p : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [normed_group F] [topological_space.second_countable_topology E] [borel_space E] [topological_space.second_countable_topology F] [measurable_space F] [borel_space F] {g : E → F} {c : ℝ≥0} (hg : lipschitz_with c g) (g0 : g 0 = 0) :
hg.comp_Lp g0 0 = 0
theorem lipschitz_with.norm_comp_Lp_sub_le {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : measurable_space α} {p : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [normed_group F] [topological_space.second_countable_topology E] [borel_space E] [topological_space.second_countable_topology F] [measurable_space F] [borel_space F] {g : E → F} {c : ℝ≥0} (hg : lipschitz_with c g) (g0 : g 0 = 0) (f f' : (measure_theory.Lp E p μ)) :
hg.comp_Lp g0 f - hg.comp_Lp g0 f' (c) * f - f'

Composing f : Lp with L : E →L[𝕜] F.

Equations
theorem continuous_linear_map.coe_fn_comp_Lp {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : measurable_space α} {p : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [normed_group F] [topological_space.second_countable_topology E] [borel_space E] [topological_space.second_countable_topology F] [measurable_space F] [borel_space F] {𝕜 : Type u_5} [nondiscrete_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] (L : E →L[𝕜] F) (f : (measure_theory.Lp E p μ)) :
∀ᵐ (a : α) ∂μ, (L.comp_Lp f) a = L (f a)
theorem continuous_linear_map.coe_fn_comp_Lp' {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : measurable_space α} {p : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [normed_group F] [topological_space.second_countable_topology E] [borel_space E] [topological_space.second_countable_topology F] [measurable_space F] [borel_space F] {𝕜 : Type u_5} [nondiscrete_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] (L : E →L[𝕜] F) (f : (measure_theory.Lp E p μ)) :
(L.comp_Lp f) =ᵐ[μ] λ (a : α), L (f a)
theorem continuous_linear_map.add_comp_Lp {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : measurable_space α} {p : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [normed_group F] [topological_space.second_countable_topology E] [borel_space E] [topological_space.second_countable_topology F] [measurable_space F] [borel_space F] {𝕜 : Type u_5} [nondiscrete_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] (L L' : E →L[𝕜] F) (f : (measure_theory.Lp E p μ)) :
(L + L').comp_Lp f = L.comp_Lp f + L'.comp_Lp f
theorem continuous_linear_map.smul_comp_Lp {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : measurable_space α} {p : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [normed_group F] [topological_space.second_countable_topology E] [borel_space E] [topological_space.second_countable_topology F] [measurable_space F] [borel_space F] {𝕜 : Type u_5} [nondiscrete_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] {𝕜' : Type u_4} [normed_field 𝕜'] [measurable_space 𝕜'] [opens_measurable_space 𝕜'] [normed_space 𝕜' F] [smul_comm_class 𝕜 𝕜' F] (c : 𝕜') (L : E →L[𝕜] F) (f : (measure_theory.Lp E p μ)) :
(c L).comp_Lp f = c L.comp_Lp f

Composing f : Lp E p μ with L : E →L[𝕜] F, seen as a 𝕜-linear map on Lp E p μ.

Equations

Composing f : Lp E p μ with L : E →L[𝕜] F, seen as a continuous 𝕜-linear map on Lp E p μ. See also the similar

Equations
theorem continuous_linear_map.smul_comp_LpL_apply {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : measurable_space α} {p : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [normed_group F] [topological_space.second_countable_topology E] [borel_space E] [topological_space.second_countable_topology F] [measurable_space F] [borel_space F] {𝕜 : Type u_5} [nondiscrete_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] [measurable_space 𝕜] [opens_measurable_space 𝕜] [fact (1 p)] {𝕜' : Type u_4} [normed_field 𝕜'] [measurable_space 𝕜'] [opens_measurable_space 𝕜'] [normed_space 𝕜' F] [smul_comm_class 𝕜 𝕜' F] (c : 𝕜') (L : E →L[𝕜] F) (f : (measure_theory.Lp E p μ)) :

TODO: written in an "apply" way because of a missing has_scalar instance.

Positive part of a function in L^p.

Equations

Negative part of a function in L^p.

Equations
theorem measure_theory.Lp.coe_fn_pos_part {α : Type u_1} {m0 : measurable_space α} {p : ℝ≥0∞} {μ : measure_theory.measure α} (f : (measure_theory.Lp p μ)) :
(measure_theory.Lp.pos_part f) =ᵐ[μ] λ (a : α), max (f a) 0
theorem measure_theory.Lp.coe_fn_neg_part_eq_max {α : Type u_1} {m0 : measurable_space α} {p : ℝ≥0∞} {μ : measure_theory.measure α} (f : (measure_theory.Lp p μ)) :
∀ᵐ (a : α) ∂μ, (measure_theory.Lp.neg_part f) a = max (-f a) 0
theorem measure_theory.Lp.coe_fn_neg_part {α : Type u_1} {m0 : measurable_space α} {p : ℝ≥0∞} {μ : measure_theory.measure α} (f : (measure_theory.Lp p μ)) :
∀ᵐ (a : α) ∂μ, (measure_theory.Lp.neg_part f) a = -min (f a) 0