# mathlibdocumentation

measure_theory.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 #

• `snorm' f p μ` : `(∫ ∥f a∥^p ∂μ) ^ (1/p)` for `f : α → F` and `p : ℝ`, where `α` is a measurable space and `F` is a normed group.

• `snorm_ess_sup f μ` : seminorm in `ℒ∞`, equal to the essential supremum `ess_sup ∥f∥ μ`.

• `snorm f p μ` : for `p : ℝ≥0∞`, seminorm in `ℒp`, equal to `0` for `p=0`, to `snorm' f p μ` for `0 < p < ∞` and to `snorm_ess_sup f μ` for `p = ∞`.

• `mem_ℒp f p μ` : property that the function `f` is almost everywhere measurable and has finite p-seminorm for measure `μ` (`snorm f p μ < ∞`)

• `Lp E p μ` : elements of `α →ₘ[μ] E` (see ae_eq_fun) such that `snorm f p μ` is finite. Defined as an `add_subgroup` of `α →ₘ[μ] E`.

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

• `continuous_linear_map.comp_Lp` defines the action on `Lp` of a continuous linear map.
• `Lp.pos_part` is the positive part of an `Lp` function.
• `Lp.neg_part` is the negative part of an `Lp` function.

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 #

• `α →₁[μ] E` : the type `Lp E 1 μ`.
• `α →₂[μ] E` : the type `Lp E 2 μ`.

## 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,
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] (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] (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] (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} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group F] (hp_ne_zero : p 0) (hp_ne_top : p ) {f : α → F} :
μ =
@[simp]
theorem measure_theory.snorm_exponent_top {α : Type u_1} {F : Type u_3} {μ : measure_theory.measure α} [normed_group F] {f : α → F} :
def measure_theory.mem_ℒp {α : Type u_1} {E : Type u_2} [normed_group E] (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} [normed_group E] {f : α → E} {p : ℝ≥0∞} {μ : measure_theory.measure α} (h : μ) :
theorem measure_theory.lintegral_rpow_nnnorm_eq_rpow_snorm' {α : Type u_1} {F : Type u_3} {q : } {μ : measure_theory.measure α} [normed_group F] {f : α → F} (hq0_lt : 0 < q) :
∫⁻ (a : α), (nnnorm (f a)) ^ q μ = ^ q
theorem measure_theory.mem_ℒp.snorm_lt_top {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] {f : α → E} (hfp : μ) :
μ <
theorem measure_theory.mem_ℒp.snorm_ne_top {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] {f : α → E} (hfp : μ) :
μ
theorem measure_theory.lintegral_rpow_nnnorm_lt_top_of_snorm'_lt_top {α : Type u_1} {F : Type u_3} {q : } {μ : measure_theory.measure α} [normed_group F] {f : α → F} (hq0_lt : 0 < q) (hfq : < ) :
∫⁻ (a : α), (nnnorm (f a)) ^ q μ <
@[simp]
theorem measure_theory.snorm'_exponent_zero {α : Type u_1} {F : Type u_3} {μ : measure_theory.measure α} [normed_group F] {f : α → F} :
= 1
@[simp]
theorem measure_theory.snorm_exponent_zero {α : Type u_1} {F : Type u_3} {μ : measure_theory.measure α} [normed_group F] {f : α → F} :
μ = 0
theorem measure_theory.mem_ℒp_zero_iff_ae_measurable {α : Type u_1} {E : Type u_2} {μ : measure_theory.measure α} [normed_group E] {f : α → E} :
@[simp]
theorem measure_theory.snorm'_zero {α : Type u_1} {F : Type u_3} {q : } {μ : measure_theory.measure α} [normed_group F] (hp0_lt : 0 < q) :
= 0
@[simp]
theorem measure_theory.snorm'_zero' {α : Type u_1} {F : Type u_3} {q : } {μ : measure_theory.measure α} [normed_group F] (hq0_ne : q 0) (hμ : μ 0) :
= 0
@[simp]
theorem measure_theory.snorm_ess_sup_zero {α : Type u_1} {F : Type u_3} {μ : measure_theory.measure α} [normed_group F] :
@[simp]
theorem measure_theory.snorm_zero {α : Type u_1} {F : Type u_3} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group F] :
μ = 0
theorem measure_theory.zero_mem_ℒp {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] :
theorem measure_theory.snorm'_measure_zero_of_pos {α : Type u_1} {F : Type u_3} {q : } [normed_group F] {f : α → F} (hq_pos : 0 < q) :
= 0
theorem measure_theory.snorm'_measure_zero_of_exponent_zero {α : Type u_1} {F : Type u_3} [normed_group F] {f : α → F} :
= 1
theorem measure_theory.snorm'_measure_zero_of_neg {α : Type u_1} {F : Type u_3} {q : } [normed_group F] {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] {f : α → F} :
@[simp]
theorem measure_theory.snorm_measure_zero {α : Type u_1} {F : Type u_3} {p : ℝ≥0∞} [normed_group F] {f : α → F} :
0 = 0
theorem measure_theory.snorm'_const {α : Type u_1} {F : Type u_3} {q : } {μ : measure_theory.measure α} [normed_group F] (c : F) (hq_pos : 0 < q) :
measure_theory.snorm' (λ (x : α), c) q μ = ((nnnorm c)) * ^ (1 / q)
theorem measure_theory.snorm'_const' {α : Type u_1} {F : Type u_3} {q : } {μ : measure_theory.measure α} [normed_group F] (c : F) (hc_ne_zero : c 0) (hq_ne_zero : q 0) :
measure_theory.snorm' (λ (x : α), c) q μ = ((nnnorm c)) * ^ (1 / q)
theorem measure_theory.snorm_ess_sup_const {α : Type u_1} {F : Type u_3} {μ : measure_theory.measure α} [normed_group F] (c : F) (hμ : μ 0) :
measure_theory.snorm_ess_sup (λ (x : α), c) μ = (nnnorm c)
theorem measure_theory.snorm'_const_of_probability_measure {α : Type u_1} {F : Type u_3} {q : } {μ : measure_theory.measure α} [normed_group F] (c : F) (hq_pos : 0 < q)  :
measure_theory.snorm' (λ (x : α), c) q μ = (nnnorm c)
theorem measure_theory.snorm_const {α : Type u_1} {F : Type u_3} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group F] (c : F) (h0 : p 0) (hμ : μ 0) :
measure_theory.snorm (λ (x : α), c) p μ = ((nnnorm c)) * ^ (1 / p.to_real)
theorem measure_theory.snorm_const' {α : Type u_1} {F : Type u_3} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group F] (c : F) (h0 : p 0) (h_top : p ) :
measure_theory.snorm (λ (x : α), c) p μ = ((nnnorm c)) * ^ (1 / p.to_real)
theorem measure_theory.mem_ℒp_const {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] (c : E)  :
measure_theory.mem_ℒp (λ (a : α), c) p μ
theorem measure_theory.snorm'_mono_ae {α : Type u_1} {F : Type u_3} {G : Type u_4} {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} {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} {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} {μ : 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} {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_ess_sup_le_of_ae_bound {α : Type u_1} {F : Type u_3} {μ : 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} {μ : 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} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group F] {f : α → F} {C : } (hfC : ∀ᵐ (x : α) ∂μ, f x C) :
μ ^ (p.to_real)⁻¹) *
theorem measure_theory.snorm_congr_norm_ae {α : Type u_1} {F : Type u_3} {G : Type u_4} {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} {q : } {μ : measure_theory.measure α} [normed_group F] {f : α → F} :
measure_theory.snorm' (λ (a : α), f a) q μ =
@[simp]
theorem measure_theory.snorm_norm {α : Type u_1} {F : Type u_3} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group F] (f : α → F) :
measure_theory.snorm (λ (x : α), f x) p μ = μ
theorem measure_theory.snorm'_norm_rpow {α : Type u_1} {F : Type u_3} {μ : measure_theory.measure α} [normed_group F] (f : α → F) (p q : ) (hq_pos : 0 < q) :
measure_theory.snorm' (λ (x : α), f x ^ q) p μ = (p * q) μ ^ q
theorem measure_theory.snorm_norm_rpow {α : Type u_1} {F : Type u_3} {p : ℝ≥0∞} {q : } {μ : measure_theory.measure α} [normed_group F] (f : α → F) (hq_pos : 0 < q) :
measure_theory.snorm (λ (x : α), f x ^ q) p μ = (p * μ ^ q
theorem measure_theory.snorm_congr_ae {α : Type u_1} {F : Type u_3} {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} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] {f g : α → E} (hfg : f =ᵐ[μ] g) :
theorem measure_theory.mem_ℒp.ae_eq {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] {f g : α → E} (hfg : f =ᵐ[μ] g) (hf_Lp : μ) :
theorem measure_theory.mem_ℒp.of_le {α : Type u_1} {E : Type u_2} {F : Type u_3} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [normed_group F] {f : α → E} {g : α → F} (hg : μ) (hf : μ) (hfg : ∀ᵐ (x : α) ∂μ, f x g x) :
theorem measure_theory.mem_ℒp_top_of_bound {α : Type u_1} {E : Type u_2} {μ : measure_theory.measure α} [normed_group E] {f : α → E} (hf : μ) (C : ) (hfC : ∀ᵐ (x : α) ∂μ, f x C) :
theorem measure_theory.mem_ℒp.of_bound {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] {f : α → E} (hf : μ) (C : ) (hfC : ∀ᵐ (x : α) ∂μ, f x C) :
theorem measure_theory.snorm'_mono_measure {α : Type u_1} {F : Type u_3} {q : } [normed_group F] {μ ν : measure_theory.measure α} (f : α → F) (hμν : ν μ) (hq : 0 q) :
theorem measure_theory.snorm_ess_sup_mono_measure {α : Type u_1} {F : Type u_3} [normed_group F] {μ ν : measure_theory.measure α} (f : α → F) (hμν : ν μ) :
theorem measure_theory.snorm_mono_measure {α : Type u_1} {F : Type u_3} {p : ℝ≥0∞} [normed_group F] {μ ν : measure_theory.measure α} (f : α → F) (hμν : ν μ) :
ν μ
theorem measure_theory.mem_ℒp.mono_measure {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} [normed_group E] {μ ν : measure_theory.measure α} {f : α → E} (hμν : ν μ) (hf : μ) :
theorem measure_theory.mem_ℒp.restrict {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] (s : set α) {f : α → E} (hf : μ) :
(μ.restrict s)
theorem measure_theory.mem_ℒp.norm {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] {f : α → E} (h : μ) :
measure_theory.mem_ℒp (λ (x : α), f x) p μ
theorem measure_theory.snorm'_eq_zero_of_ae_zero {α : Type u_1} {F : Type u_3} {q : } {μ : measure_theory.measure α} [normed_group F] {f : α → F} (hq0_lt : 0 < q) (hf_zero : f =ᵐ[μ] 0) :
= 0
theorem measure_theory.snorm'_eq_zero_of_ae_zero' {α : Type u_1} {F : Type u_3} {q : } {μ : measure_theory.measure α} [normed_group F] (hq0_ne : q 0) (hμ : μ 0) {f : α → F} (hf_zero : f =ᵐ[μ] 0) :
= 0
theorem measure_theory.ae_eq_zero_of_snorm'_eq_zero {α : Type u_1} {E : Type u_2} {q : } {μ : measure_theory.measure α} [normed_group E] {f : α → E} (hq0 : 0 q) (hf : μ) (h : = 0) :
f =ᵐ[μ] 0
theorem measure_theory.snorm'_eq_zero_iff {α : Type u_1} {E : Type u_2} {q : } {μ : measure_theory.measure α} [normed_group E] (hq0_lt : 0 < q) {f : α → E} (hf : μ) :
= 0 f =ᵐ[μ] 0
theorem measure_theory.coe_nnnorm_ae_le_snorm_ess_sup {α : Type u_1} {F : Type u_3} [normed_group F] (f : α → F) (μ : measure_theory.measure α) :
∀ᵐ (x : α) ∂μ, (nnnorm (f x))
@[simp]
theorem measure_theory.snorm_ess_sup_eq_zero_iff {α : Type u_1} {F : Type u_3} {μ : measure_theory.measure α} [normed_group F] {f : α → F} :
f =ᵐ[μ] 0
theorem measure_theory.snorm_eq_zero_iff {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] {f : α → E} (hf : μ) (h0 : p 0) :
μ = 0 f =ᵐ[μ] 0
theorem measure_theory.snorm'_trim {E : Type u_2} {q : } [normed_group E] {α : Type u_1} {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) {f : α → E} (hf : measurable f) :
(μ.trim hm) =
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) :
(μ.trim hm) = μ
theorem measure_theory.snorm_ess_sup_trim {E : Type u_2} [normed_group E] {α : Type u_1} {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) {f : α → E} (hf : measurable f) :
theorem measure_theory.snorm_trim {E : Type u_2} {p : ℝ≥0∞} [normed_group E] {α : Type u_1} {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) {f : α → E} (hf : measurable f) :
(μ.trim hm) = μ
@[simp]
theorem measure_theory.snorm'_neg {α : Type u_1} {F : Type u_3} {q : } {μ : measure_theory.measure α} [normed_group F] {f : α → F} :
μ =
@[simp]
theorem measure_theory.snorm_neg {α : Type u_1} {F : Type u_3} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group F] {f : α → F} :
μ = μ
theorem measure_theory.mem_ℒp.neg {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E] {f : α → E} (hf : μ) :
μ
theorem measure_theory.snorm'_le_snorm'_mul_rpow_measure_univ {α : Type u_1} {E : Type u_2} {μ : measure_theory.measure α} [normed_group E] [borel_space E] {p q : } (hp0_lt : 0 < p) (hpq : p q) {f : α → E} (hf : μ) :
μ) * ^ (1 / p - 1 / q)
theorem measure_theory.snorm'_le_snorm_ess_sup_mul_rpow_measure_univ {α : Type u_1} {F : Type u_3} {q : } {μ : measure_theory.measure α} [normed_group F] (hq_pos : 0 < q) {f : α → F} :
* ^ (1 / q)
theorem measure_theory.snorm_le_snorm_mul_rpow_measure_univ {α : Type u_1} {E : Type u_2} {μ : measure_theory.measure α} [normed_group E] [borel_space E] {p q : ℝ≥0∞} (hpq : p q) {f : α → E} (hf : μ) :
μ μ) * ^ (1 / p.to_real - 1 / q.to_real)
theorem measure_theory.snorm'_le_snorm'_of_exponent_le {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {p q : } (hp0_lt : 0 < p) (hpq : p q) (μ : measure_theory.measure α) {f : α → E} (hf : μ) :
theorem measure_theory.snorm'_le_snorm_ess_sup {α : Type u_1} {F : Type u_3} {q : } {μ : measure_theory.measure α} [normed_group F] (hq_pos : 0 < q) {f : α → F}  :
theorem measure_theory.snorm_le_snorm_of_exponent_le {α : Type u_1} {E : Type u_2} {μ : measure_theory.measure α} [normed_group E] [borel_space E] {p q : ℝ≥0∞} (hpq : p q) {f : α → E} (hf : μ) :
μ μ
theorem measure_theory.snorm'_lt_top_of_snorm'_lt_top_of_exponent_le {α : Type u_1} {E : Type u_2} {μ : measure_theory.measure α} [normed_group E] [borel_space E] {p q : } {f : α → E} (hf : μ) (hfq_lt_top : < ) (hp_nonneg : 0 p) (hpq : p q) :
theorem measure_theory.mem_ℒp.mem_ℒp_of_exponent_le {α : Type u_1} {E : Type u_2} {μ : measure_theory.measure α} [normed_group E] [borel_space E] {p q : ℝ≥0∞} {f : α → E} (hfq : μ) (hpq : p q) :
theorem measure_theory.snorm'_add_le {α : Type u_1} {E : Type u_2} {q : } {μ : measure_theory.measure α} [normed_group E] [borel_space E] {f g : α → E} (hf : μ) (hg : μ) (hq1 : 1 q) :
theorem measure_theory.snorm_ess_sup_add_le {α : Type u_1} {F : Type u_3} {μ : measure_theory.measure α} [normed_group F] {f g : α → F} :
theorem measure_theory.snorm_add_le {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E] {f g : α → E} (hf : μ) (hg : μ) (hp1 : 1 p) :
measure_theory.snorm (f + g) p μ μ + μ
theorem measure_theory.snorm'_sum_le {α : Type u_1} {E : Type u_2} {q : } {μ : measure_theory.measure α} [normed_group E] [borel_space 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, q μ
theorem measure_theory.snorm_sum_le {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space 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.snorm_add_lt_top_of_one_le {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E] {f g : α → E} (hf : μ) (hg : μ) (hq1 : 1 p) :
theorem measure_theory.snorm'_add_lt_top_of_le_one {α : Type u_1} {E : Type u_2} {q : } {μ : measure_theory.measure α} [normed_group E] [borel_space E] {f g : α → E} (hf : μ) (hg : μ) (hf_snorm : < ) (hg_snorm : < ) (hq_pos : 0 < q) (hq1 : q 1) :
theorem measure_theory.snorm_add_lt_top {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E] {f g : α → E} (hf : μ) (hg : μ) :
theorem measure_theory.mem_ℒp.add {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E] {f g : α → E} (hf : μ) (hg : μ) :
theorem measure_theory.mem_ℒp.sub {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E] {f g : α → E} (hf : μ) (hg : μ) :
theorem measure_theory.snorm'_const_smul {α : Type u_1} {F : Type u_3} {q : } {μ : measure_theory.measure α} [normed_group F] {𝕜 : Type u_5} [normed_field 𝕜] [ F] {f : α → F} (c : 𝕜) (hq0_lt : 0 < q) :
theorem measure_theory.snorm_ess_sup_const_smul {α : Type u_1} {F : Type u_3} {μ : measure_theory.measure α} [normed_group F] {𝕜 : Type u_5} [normed_field 𝕜] [ F] {f : α → F} (c : 𝕜) :
μ = ((nnnorm c)) *
theorem measure_theory.snorm_const_smul {α : Type u_1} {F : Type u_3} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group F] {𝕜 : Type u_5} [normed_field 𝕜] [ F] {f : α → F} (c : 𝕜) :
measure_theory.snorm (c f) p μ = ((nnnorm c)) * μ
theorem measure_theory.mem_ℒp.const_smul {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] {𝕜 : Type u_5} [normed_field 𝕜] [ E] [borel_space E] {f : α → E} (hf : μ) (c : 𝕜) :
theorem measure_theory.mem_ℒp.const_mul {α : Type u_1} {p : ℝ≥0∞} {μ : measure_theory.measure α} {𝕜 : Type u_5} [normed_field 𝕜] [borel_space 𝕜] {f : α → 𝕜} (hf : μ) (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} {μ : measure_theory.measure α} [normed_group E] {𝕜 : Type u_5} [normed_field 𝕜] [ E] {p q r : } {f : α → E} (hf : μ) {φ : α → 𝕜} (hφ : μ) (hp0_lt : 0 < p) (hpq : p < q) (hpqr : 1 / p = 1 / q + 1 / r) :
measure_theory.snorm' f) p μ μ) *
theorem measure_theory.snorm_le_mul_snorm_aux_of_nonneg {α : Type u_1} {F : Type u_3} {G : Type u_4} {μ : 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} {μ : 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∞) :
μ = 0 μ = 0
theorem measure_theory.snorm_le_mul_snorm_of_ae_le_mul {α : Type u_1} {F : Type u_3} {G : Type u_4} {μ : 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} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [normed_group F] {f : α → E} {g : α → F} {c : } (hg : μ) (hf : μ) (hfg : ∀ᵐ (x : α) ∂μ, f x c * g x) :

### 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} {μ : measure_theory.measure α} [normed_group E] {p : ℝ≥0∞} {f : α → E} (hf : μ) :
= μ
theorem measure_theory.mem_ℒp.snorm_mk_lt_top {α : Type u_1} {E : Type u_2} {μ : measure_theory.measure α} [normed_group E] {p : ℝ≥0∞} {f : α → E} (hfp : μ) :
def measure_theory.Lp {α : Type u_1} (E : Type u_2) [normed_group E] [borel_space E] (p : ℝ≥0∞) (μ : measure_theory.measure α) :

Lp space

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

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

Equations
• h_mem_ℒp = , _⟩
theorem measure_theory.mem_ℒp.coe_fn_to_Lp {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E] {f : α → E} (hf : μ) :
@[simp]
theorem measure_theory.mem_ℒp.to_Lp_eq_to_Lp_iff {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E] {f g : α → E} (hf : μ) (hg : μ) :
f =ᵐ[μ] g
@[simp]
theorem measure_theory.mem_ℒp.to_Lp_zero {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E] (h : μ) :
theorem measure_theory.mem_ℒp.to_Lp_add {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E] {f g : α → E} (hf : μ) (hg : μ) :
_ =
theorem measure_theory.mem_ℒp.to_Lp_neg {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E] {f : α → E} (hf : μ) :
theorem measure_theory.mem_ℒp.to_Lp_sub {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E] {f g : α → E} (hf : μ) (hg : μ) :
_ =
@[instance]
def measure_theory.Lp.has_coe_to_fun {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E]  :
Equations
@[ext]
theorem measure_theory.Lp.ext {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E] {f g : μ)} (h : f =ᵐ[μ] g) :
f = g
theorem measure_theory.Lp.ext_iff {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E] {f g : μ)} :
f = g f =ᵐ[μ] g
theorem measure_theory.Lp.mem_Lp_iff_snorm_lt_top {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E] {f : α →ₘ[μ] E} :
f μ <
theorem measure_theory.Lp.mem_Lp_iff_mem_ℒp {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E] {f : α →ₘ[μ] E} :
f μ
theorem measure_theory.Lp.antimono {α : Type u_1} {E : Type u_2} {μ : measure_theory.measure α} [normed_group E] [borel_space E] {p q : ℝ≥0∞} (hpq : p q) :
μ μ
@[simp]
theorem measure_theory.Lp.coe_fn_mk {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E] {f : α →ₘ[μ] E} (hf : < ) :
f, hf⟩ = f
@[simp]
theorem measure_theory.Lp.coe_mk {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E] {f : α →ₘ[μ] E} (hf : < ) :
f, hf⟩ = f
@[simp]
theorem measure_theory.Lp.to_Lp_coe_fn {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E] (f : μ)) (hf : μ) :
theorem measure_theory.Lp.snorm_lt_top {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E] (f : μ)) :
theorem measure_theory.Lp.snorm_ne_top {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E] (f : μ)) :
theorem measure_theory.Lp.measurable {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E] (f : μ)) :
theorem measure_theory.Lp.ae_measurable {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E] (f : μ)) :
theorem measure_theory.Lp.mem_ℒp {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E] (f : μ)) :
theorem measure_theory.Lp.coe_fn_zero {α : Type u_1} (E : Type u_2) (p : ℝ≥0∞) (μ : measure_theory.measure α) [normed_group E] [borel_space E]  :
0 =ᵐ[μ] 0
theorem measure_theory.Lp.coe_fn_neg {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E] (f : μ)) :
theorem measure_theory.Lp.coe_fn_add {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E] (f g : μ)) :
(f + g) =ᵐ[μ] f + g
theorem measure_theory.Lp.coe_fn_sub {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E] (f g : μ)) :
(f - g) =ᵐ[μ] f - g
theorem measure_theory.Lp.mem_Lp_const {E : Type u_2} {p : ℝ≥0∞} [normed_group E] [borel_space E] (α : Type u_1) (μ : measure_theory.measure α) (c : E)  :
@[instance]
def measure_theory.Lp.has_norm {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E]  :
Equations
@[instance]
def measure_theory.Lp.has_dist {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E]  :
Equations
@[instance]
def measure_theory.Lp.has_edist {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E]  :
Equations
theorem measure_theory.Lp.norm_def {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E] (f : μ)) :
@[simp]
theorem measure_theory.Lp.norm_to_Lp {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E] (f : α → E) (hf : μ) :
theorem measure_theory.Lp.dist_def {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E] (f g : μ)) :
theorem measure_theory.Lp.edist_def {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E] (f g : μ)) :
@[simp]
theorem measure_theory.Lp.edist_to_Lp_to_Lp {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E] (f g : α → E) (hf : μ) (hg : μ) :
@[simp]
theorem measure_theory.Lp.edist_to_Lp_zero {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E] (f : α → E) (hf : μ) :
0 = μ
@[simp]
theorem measure_theory.Lp.norm_zero {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E]  :
theorem measure_theory.Lp.norm_eq_zero_iff {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E] {f : μ)} (hp : 0 < p) :
f = 0 f = 0
theorem measure_theory.Lp.eq_zero_iff_ae_eq_zero {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E] {f : μ)} :
f = 0 f =ᵐ[μ] 0
@[simp]
theorem measure_theory.Lp.norm_neg {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E] {f : μ)} :
theorem measure_theory.Lp.norm_le_mul_norm_of_ae_le_mul {α : Type u_1} {E : Type u_2} {F : Type u_3} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [normed_group F] [borel_space E] [borel_space F] {c : } {f : μ)} {g : μ)} (h : ∀ᵐ (x : α) ∂μ, f x c * g x) :
theorem measure_theory.Lp.norm_le_norm_of_ae_le {α : Type u_1} {E : Type u_2} {F : Type u_3} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [normed_group F] [borel_space E] [borel_space F] {f : μ)} {g : μ)} (h : ∀ᵐ (x : α) ∂μ, f x g x) :
theorem measure_theory.Lp.mem_Lp_of_ae_le_mul {α : Type u_1} {E : Type u_2} {F : Type u_3} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [normed_group F] [borel_space E] [borel_space F] {c : } {f : α →ₘ[μ] E} {g : μ)} (h : ∀ᵐ (x : α) ∂μ, f x c * g x) :
f μ
theorem measure_theory.Lp.mem_Lp_of_ae_le {α : Type u_1} {E : Type u_2} {F : Type u_3} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [normed_group F] [borel_space E] [borel_space F] {f : α →ₘ[μ] E} {g : μ)} (h : ∀ᵐ (x : α) ∂μ, f x g x) :
f μ
theorem measure_theory.Lp.mem_Lp_of_ae_bound {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E] {f : α →ₘ[μ] E} (C : ) (hfC : ∀ᵐ (x : α) ∂μ, f x C) :
f μ
theorem measure_theory.Lp.norm_le_of_ae_bound {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E] {f : μ)} {C : } (hC : 0 C) (hfC : ∀ᵐ (x : α) ∂μ, f x C) :
@[instance]
def measure_theory.Lp.normed_group {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E] [hp : fact (1 p)] :
Equations
@[instance]
def measure_theory.Lp.normed_group_L1 {α : Type u_1} {E : Type u_2} {μ : measure_theory.measure α} [normed_group E] [borel_space E]  :
Equations
@[instance]
def measure_theory.Lp.normed_group_L2 {α : Type u_1} {E : Type u_2} {μ : measure_theory.measure α} [normed_group E] [borel_space E]  :
Equations
@[instance]
def measure_theory.Lp.normed_group_Ltop {α : Type u_1} {E : Type u_2} {μ : measure_theory.measure α} [normed_group E] [borel_space E]  :
Equations
theorem measure_theory.Lp.mem_Lp_const_smul {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E] {𝕜 : Type u_5} [normed_field 𝕜] [ E] (c : 𝕜) (f : μ)) :
c f μ
def measure_theory.Lp.Lp_submodule {α : Type u_1} (E : Type u_2) (p : ℝ≥0∞) (μ : measure_theory.measure α) [normed_group E] [borel_space E] (𝕜 : Type u_5) [normed_field 𝕜] [ E]  :
→ₘ[μ] 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_Lp_submodule {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E] {𝕜 : Type u_5} [normed_field 𝕜] [ E]  :
= μ
@[instance]
def measure_theory.Lp.module {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E] {𝕜 : Type u_5} [normed_field 𝕜] [ E]  :
μ)
Equations
theorem measure_theory.Lp.coe_fn_smul {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E] {𝕜 : Type u_5} [normed_field 𝕜] [ E] (c : 𝕜) (f : μ)) :
(c f) =ᵐ[μ] c f
theorem measure_theory.Lp.norm_const_smul {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E] {𝕜 : Type u_5} [normed_field 𝕜] [ E] (c : 𝕜) (f : μ)) :
@[instance]
def measure_theory.Lp.normed_space {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E] {𝕜 : Type u_5} [normed_field 𝕜] [ E] [fact (1 p)] :
μ)
Equations
@[instance]
def measure_theory.Lp.normed_space_L1 {α : Type u_1} {E : Type u_2} {μ : measure_theory.measure α} [normed_group E] [borel_space E] {𝕜 : Type u_5} [normed_field 𝕜] [ E]  :
μ)
Equations
@[instance]
def measure_theory.Lp.normed_space_L2 {α : Type u_1} {E : Type u_2} {μ : measure_theory.measure α} [normed_group E] [borel_space E] {𝕜 : Type u_5} [normed_field 𝕜] [ E]  :
μ)
Equations
@[instance]
def measure_theory.Lp.normed_space_Ltop {α : Type u_1} {E : Type u_2} {μ : measure_theory.measure α} [normed_group E] [borel_space E] {𝕜 : Type u_5} [normed_field 𝕜] [ E]  :
μ)
Equations
theorem measure_theory.mem_ℒp.to_Lp_const_smul {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E] {𝕜 : Type u_5} [normed_field 𝕜] [ E] {f : α → E} (c : 𝕜) (hf : μ) :
_ =

### 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} {μ : measure_theory.measure α} [normed_group E] [normed_group F] [borel_space E] [borel_space F] {f : α → E} {g : E → F} (hg : g) (hg' : g) (g0 : g 0 = 0) :
def lipschitz_with.comp_Lp {α : Type u_1} {E : Type u_2} {F : Type u_3} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [normed_group F] [borel_space E] [borel_space F] {g : E → F} {c : ℝ≥0} (hg : g) (g0 : g 0 = 0) (f : μ)) :
μ)

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} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [normed_group F] [borel_space E] [borel_space F] {g : E → F} {c : ℝ≥0} (hg : g) (g0 : g 0 = 0) (f : μ)) :
(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} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [normed_group F] [borel_space E] [borel_space F] {g : E → F} {c : ℝ≥0} (hg : 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} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [normed_group F] [borel_space E] [borel_space F] {g : E → F} {c : ℝ≥0} (hg : g) (g0 : g 0 = 0) (f f' : μ)) :
hg.comp_Lp g0 f - hg.comp_Lp g0 f' (c) * f - f'
theorem lipschitz_with.norm_comp_Lp_le {α : Type u_1} {E : Type u_2} {F : Type u_3} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [normed_group F] [borel_space E] [borel_space F] {g : E → F} {c : ℝ≥0} (hg : g) (g0 : g 0 = 0) (f : μ)) :
theorem lipschitz_with.lipschitz_with_comp_Lp {α : Type u_1} {E : Type u_2} {F : Type u_3} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [normed_group F] [borel_space E] [borel_space F] {g : E → F} {c : ℝ≥0} [fact (1 p)] (hg : g) (g0 : g 0 = 0) :
(hg.comp_Lp g0)
theorem lipschitz_with.continuous_comp_Lp {α : Type u_1} {E : Type u_2} {F : Type u_3} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [normed_group F] [borel_space E] [borel_space F] {g : E → F} {c : ℝ≥0} [fact (1 p)] (hg : g) (g0 : g 0 = 0) :
def continuous_linear_map.comp_Lp {α : Type u_1} {E : Type u_2} {F : Type u_3} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [normed_group F] [borel_space E] [borel_space F] [ E] [ F] (L : E →L[] 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} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [normed_group F] [borel_space E] [borel_space F] [ E] [ F] (L : E →L[] F) (f : μ)) :
∀ᵐ (a : α) ∂μ, (L.comp_Lp f) a = L (f a)
def continuous_linear_map.comp_Lpₗ {α : Type u_1} {E : Type u_2} {F : Type u_3} (p : ℝ≥0∞) (μ : measure_theory.measure α) [normed_group E] [normed_group F] [borel_space E] [borel_space F] [ E] [ F] (L : E →L[] F) :

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

Equations
theorem continuous_linear_map.norm_comp_Lp_le {α : Type u_1} {E : Type u_2} {F : Type u_3} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [normed_group F] [borel_space E] [borel_space F] [ E] [ F] (L : E →L[] F) (f : μ)) :
def continuous_linear_map.comp_LpL {α : Type u_1} {E : Type u_2} {F : Type u_3} (p : ℝ≥0∞) (μ : measure_theory.measure α) [normed_group E] [normed_group F] [borel_space E] [borel_space F] [ E] [ F] [fact (1 p)] (L : E →L[] F) :
μ) →L[] μ)

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

Equations
• = _
theorem continuous_linear_map.norm_compLpL_le {α : Type u_1} {E : Type u_2} {F : Type u_3} (p : ℝ≥0∞) (μ : measure_theory.measure α) [normed_group E] [normed_group F] [borel_space E] [borel_space F] [ E] [ F] [fact (1 p)] (L : E →L[] F) :
def measure_theory.Lp.pos_part {α : Type u_1} {p : ℝ≥0∞} {μ : measure_theory.measure α} (f : μ)) :
μ)

Positive part of a function in `L^p`.

Equations
def measure_theory.Lp.neg_part {α : Type u_1} {p : ℝ≥0∞} {μ : measure_theory.measure α} (f : μ)) :
μ)

Negative part of a function in `L^p`.

Equations
theorem measure_theory.Lp.coe_pos_part {α : Type u_1} {p : ℝ≥0∞} {μ : measure_theory.measure α} (f : μ)) :
theorem measure_theory.Lp.coe_fn_pos_part {α : Type u_1} {p : ℝ≥0∞} {μ : measure_theory.measure α} (f : μ)) :
=ᵐ[μ] λ (a : α), max (f a) 0
theorem measure_theory.Lp.coe_fn_neg_part_eq_max {α : Type u_1} {p : ℝ≥0∞} {μ : measure_theory.measure α} (f : μ)) :
∀ᵐ (a : α) ∂μ, = max (-f a) 0
theorem measure_theory.Lp.coe_fn_neg_part {α : Type u_1} {p : ℝ≥0∞} {μ : measure_theory.measure α} (f : μ)) :
∀ᵐ (a : α) ∂μ, = -min (f a) 0
theorem measure_theory.Lp.continuous_pos_part {α : Type u_1} {p : ℝ≥0∞} {μ : measure_theory.measure α} [fact (1 p)] :
continuous (λ (f : μ)),
theorem measure_theory.Lp.continuous_neg_part {α : Type u_1} {p : ℝ≥0∞} {μ : measure_theory.measure α} [fact (1 p)] :
continuous (λ (f : μ)),

## `L^p` is a complete space #

We show that `L^p` is a complete space for `1 ≤ p`.

theorem measure_theory.Lp.snorm'_lim_eq_lintegral_liminf {α : Type u_1} {G : Type u_4} {μ : measure_theory.measure α} [normed_group G] {ι : Type u_2} [nonempty ι] [linear_order ι] {f : ι → α → G} {p : } (hp_nonneg : 0 p) {f_lim : α → G} (h_lim : ∀ᵐ (x : α) ∂μ, filter.tendsto (λ (n : ι), f n x) filter.at_top (𝓝 (f_lim x))) :
p μ = (∫⁻ (a : α), filter.at_top.liminf (λ (m : ι), (nnnorm (f m a)) ^ p) μ) ^ (1 / p)
theorem measure_theory.Lp.snorm'_lim_le_liminf_snorm' {α : Type u_1} {μ : measure_theory.measure α} {E : Type u_2} [normed_group E] [borel_space E] {f : α → E} {p : } (hp_pos : 0 < p) (hf : ∀ (n : ), ae_measurable (f n) μ) {f_lim : α → E} (h_lim : ∀ᵐ (x : α) ∂μ, filter.tendsto (λ (n : ), f n x) filter.at_top (𝓝 (f_lim x))) :
p μ filter.at_top.liminf (λ (n : ), p μ)
theorem measure_theory.Lp.snorm_exponent_top_lim_eq_ess_sup_liminf {α : Type u_1} {G : Type u_4} {μ : measure_theory.measure α} [normed_group G] {ι : Type u_2} [nonempty ι] [linear_order ι] {f : ι → α → G} {f_lim : α → G} (h_lim : ∀ᵐ (x : α) ∂μ, filter.tendsto (λ (n : ι), f n x) filter.at_top (𝓝 (f_lim x))) :
measure_theory.snorm f_lim μ = ess_sup (λ (x : α), filter.at_top.liminf (λ (m : ι), (nnnorm (f m x)))) μ
theorem measure_theory.Lp.snorm_exponent_top_lim_le_liminf_snorm_exponent_top {α : Type u_1} {F : Type u_3} {μ : measure_theory.measure α} [normed_group F] {ι : Type u_2} [nonempty ι] [encodable ι] [linear_order ι] {f : ι → α → F} {f_lim : α → F} (h_lim : ∀ᵐ (x : α) ∂μ, filter.tendsto (λ (n : ι), f n x) filter.at_top (𝓝 (f_lim x))) :
theorem measure_theory.Lp.snorm_lim_le_liminf_snorm {α : Type u_1} {p : ℝ≥0∞} {μ : measure_theory.measure α} {E : Type u_2} [normed_group E] [borel_space E] {f : α → E} (hf : ∀ (n : ), ae_measurable (f n) μ) (f_lim : α → E) (h_lim : ∀ᵐ (x : α) ∂μ, filter.tendsto (λ (n : ), f n x) filter.at_top (𝓝 (f_lim x))) :

### `Lp` is complete iff Cauchy sequences of `ℒp` have limits in `ℒp`#

theorem measure_theory.Lp.tendsto_Lp_iff_tendsto_ℒp' {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E] {ι : Type u_3} {fi : filter ι} [hp : fact (1 p)] (f : ι → μ)) (f_lim : μ)) :
fi (𝓝 f_lim) filter.tendsto (λ (n : ι), measure_theory.snorm ((f n) - f_lim) p μ) fi (𝓝 0)
theorem measure_theory.Lp.tendsto_Lp_iff_tendsto_ℒp {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E] {ι : Type u_3} {fi : filter ι} [hp : fact (1 p)] (f : ι → μ)) (f_lim : α → E) (f_lim_ℒp : p μ) :
fi (𝓝 f_lim_ℒp)) filter.tendsto (λ (n : ι), measure_theory.snorm ((f n) - f_lim) p μ) fi (𝓝 0)
theorem measure_theory.Lp.tendsto_Lp_of_tendsto_ℒp {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E] {ι : Type u_3} {fi : filter ι} [hp : fact (1 p)] {f : ι → μ)} (f_lim : α → E) (f_lim_ℒp : p μ) (h_tendsto : filter.tendsto (λ (n : ι), measure_theory.snorm ((f n) - f_lim) p μ) fi (𝓝 0)) :
fi (𝓝 f_lim_ℒp))
theorem measure_theory.Lp.cauchy_seq_Lp_iff_cauchy_seq_ℒp {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E] {ι : Type u_3} [nonempty ι] [hp : fact (1 p)] (f : ι → μ)) :
filter.tendsto (λ (n : ι × ι), measure_theory.snorm ((f n.fst) - (f n.snd)) p μ) filter.at_top (𝓝 0)
theorem measure_theory.Lp.complete_space_Lp_of_cauchy_complete_ℒp {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E] [hp : fact (1 p)] (H : ∀ (f : α → E), (∀ (n : ), p μ)∀ (B : ℝ≥0∞), ∑' (i : ), B i < (∀ (N n m : ), N nN mmeasure_theory.snorm (f n - f m) p μ < B N)(∃ (f_lim : α → E) (hf_lim_meas : p μ), filter.tendsto (λ (n : ), measure_theory.snorm (f n - f_lim) p μ) filter.at_top (𝓝 0))) :

### Prove that controlled Cauchy sequences of `ℒp` have limits in `ℒp`#

theorem measure_theory.Lp.ae_tendsto_of_cauchy_snorm' {α : Type u_1} {E : Type u_2} {μ : measure_theory.measure α} [normed_group E] [borel_space E] {f : α → E} {p : } (hf : ∀ (n : ), ae_measurable (f n) μ) (hp1 : 1 p) {B : ℝ≥0∞} (hB : ∑' (i : ), B i < ) (h_cau : ∀ (N n m : ), N nN mmeasure_theory.snorm' (f n - f m) p μ < B N) :
∀ᵐ (x : α) ∂μ, ∃ (l : E), filter.tendsto (λ (n : ), f n x) filter.at_top (𝓝 l)
theorem measure_theory.Lp.ae_tendsto_of_cauchy_snorm {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E] {f : α → E} (hf : ∀ (n : ), ae_measurable (f n) μ) (hp : 1 p) {B : ℝ≥0∞} (hB : ∑' (i : ), B i < ) (h_cau : ∀ (N n m : ), N nN mmeasure_theory.snorm (f n - f m) p μ < B N) :
∀ᵐ (x : α) ∂μ, ∃ (l : E), filter.tendsto (λ (n : ), f n x) filter.at_top (𝓝 l)
theorem measure_theory.Lp.cauchy_tendsto_of_tendsto {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E] {f : α → E} (hf : ∀ (n : ), ae_measurable (f n) μ) (f_lim : α → E) {B : ℝ≥0∞} (hB : ∑' (i : ), B i < ) (h_cau : ∀ (N n m : ), N nN mmeasure_theory.snorm (f n - f m) p μ < B N) (h_lim : ∀ᵐ (x : α) ∂μ, filter.tendsto (λ (n : ), f n x) filter.at_top (𝓝 (f_lim x))) :
filter.tendsto (λ (n : ), measure_theory.snorm (f n - f_lim) p μ) filter.at_top (𝓝 0)
theorem measure_theory.Lp.mem_ℒp_of_cauchy_tendsto {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E] (hp : 1 p) {f : α → E} (hf : ∀ (n : ), p μ) (f_lim : α → E) (h_lim_meas : ae_measurable f_lim μ) (h_tendsto : filter.tendsto (λ (n : ), measure_theory.snorm (f n - f_lim) p μ) filter.at_top (𝓝 0)) :
p μ
theorem measure_theory.Lp.cauchy_complete_ℒp {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E] (hp : 1 p) {f : α → E} (hf : ∀ (n : ), p μ) {B : ℝ≥0∞} (hB : ∑' (i : ), B i < ) (h_cau : ∀ (N n m : ), N nN mmeasure_theory.snorm (f n - f m) p μ < B N) :
∃ (f_lim : α → E) (hf_lim_meas : p μ), filter.tendsto (λ (n : ), measure_theory.snorm (f n - f_lim) p μ) filter.at_top (𝓝 0)

### `Lp` is complete for `1 ≤ p`#

@[instance]
def measure_theory.Lp.complete_space {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E] [hp : fact (1 p)] :
theorem bounded_continuous_function.mem_Lp {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E] [borel_space α] (f : α →ᵇ E) :

A bounded continuous function is in `Lp`.

theorem bounded_continuous_function.Lp_norm_le {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group E] [borel_space E] [borel_space α] (f : α →ᵇ E) :

The `Lp`-norm of a bounded continuous function is at most a constant (depending on the measure of the whole space) times its sup-norm.

def bounded_continuous_function.to_Lp_hom {α : Type u_1} {E : Type u_2} (p : ℝ≥0∞) (μ : measure_theory.measure α) [normed_group E] [borel_space E] [borel_space α] [fact (1 p)] :

The normed group homomorphism of considering a bounded continuous function on a finite-measure space as an element of `Lp`.

Equations
def bounded_continuous_function.to_Lp {α : Type u_1} {E : Type u_2} (p : ℝ≥0∞) (μ : measure_theory.measure α) [normed_group E] [borel_space E] [borel_space α] (𝕜 : Type u_5) [normed_field 𝕜] [ E] [fact (1 p)] :
→ᵇ E) →L[𝕜] μ)

The bounded linear map of considering a bounded continuous function on a finite-measure space as an element of `Lp`.

Equations
theorem bounded_continuous_function.coe_fn_to_Lp {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} (μ : measure_theory.measure α) [normed_group E] [borel_space E] [borel_space α] {𝕜 : Type u_5} [normed_field 𝕜] [ E] [fact (1 p)] (f : α →ᵇ E) :
theorem bounded_continuous_function.to_Lp_norm_le {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} (μ : measure_theory.measure α) [normed_group E] [borel_space E] [borel_space α] {𝕜 : Type u_5} [ E] [fact (1 p)] :
def continuous_map.to_Lp {α : Type u_1} {E : Type u_2} (p : ℝ≥0∞) (μ : measure_theory.measure α) [normed_group E] [borel_space E] [borel_space α] (𝕜 : Type u_5) [fact (1 p)] [normed_field 𝕜] [ E] :
C(α, E) →L[𝕜] μ)

The bounded linear map of considering a continuous function on a compact finite-measure space `α` as an element of `Lp`. By definition, the norm on `C(α, E)` is the sup-norm, transferred from the space `α →ᵇ E` of bounded continuous functions, so this construction is just a matter of transferring the structure from `bounded_continuous_function.to_Lp` along the isometry.

Equations
theorem continuous_map.coe_fn_to_Lp {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} (μ : measure_theory.measure α) [normed_group E] [borel_space E] [borel_space α] {𝕜 : Type u_5} [fact (1 p)] [normed_field 𝕜] [ E] (f : C(α, E)) :
( 𝕜) f) =ᵐ[μ] f
theorem continuous_map.to_Lp_def {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} (μ : measure_theory.measure α) [normed_group E] [borel_space E] [borel_space α] {𝕜 : Type u_5} [fact (1 p)] [normed_field 𝕜] [ E] (f : C(α, E)) :
𝕜) f =
@[simp]
theorem continuous_map.to_Lp_comp_forget_boundedness {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} (μ : measure_theory.measure α) [normed_group E] [borel_space E] [borel_space α] {𝕜 : Type u_5} [fact (1 p)] [normed_field 𝕜] [ E] (f : α →ᵇ E) :
= f
@[simp]
theorem continuous_map.coe_to_Lp {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} (μ : measure_theory.measure α) [normed_group E] [borel_space E] [borel_space α] {𝕜 : Type u_5} [fact (1 p)] [normed_field 𝕜] [ E] (f : C(α, E)) :
( 𝕜) f) =
theorem continuous_map.to_Lp_norm_eq_to_Lp_norm_coe {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} (μ : measure_theory.measure α) [normed_group E] [borel_space E] [borel_space α] {𝕜 : Type u_5} [fact (1 p)] [ E] :
theorem continuous_map.to_Lp_norm_le {α : Type u_1} {E : Type u_2} {p : ℝ≥0∞} (μ : measure_theory.measure α) [normed_group E] [borel_space E] [borel_space α] {𝕜 : Type u_5} [fact (1 p)] [ E] :

Bound for the operator norm of `continuous_map.to_Lp`.