# mathlib3documentation

measure_theory.function.lp_space

# Lp space #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file provides the space `Lp E p μ` as 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 #

• `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,
with _ ha1 ha2 ha3 ha4,
simp only [ha1, ha2, ha3, ha4, add_assoc],
end
``````

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

### 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 α} {p : ennreal} {f : α E}  :
= μ
theorem measure_theory.mem_ℒp.snorm_mk_lt_top {α : Type u_1} {E : Type u_2} {μ : measure_theory.measure α} {p : ennreal} {f : α E} (hfp : μ) :
def measure_theory.Lp {α : Type u_1} (E : Type u_2) {m : measurable_space α} (p : ennreal) (μ : . "volume_tac") :

Lp space

Equations
Instances for `↥measure_theory.Lp`
def measure_theory.mem_ℒp.to_Lp {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} (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} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f : α E} (hf : μ) :
theorem measure_theory.mem_ℒp.to_Lp_congr {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f g : α E} (hf : μ) (hg : μ) (hfg : f =ᵐ[μ] g) :
@[simp]
theorem measure_theory.mem_ℒp.to_Lp_eq_to_Lp_iff {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f g : α E} (hf : μ) (hg : μ) :
f =ᵐ[μ] g
@[simp]
theorem measure_theory.mem_ℒp.to_Lp_zero {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} (h : μ) :
theorem measure_theory.mem_ℒp.to_Lp_add {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f g : α E} (hf : μ) (hg : μ) :
_ =
theorem measure_theory.mem_ℒp.to_Lp_neg {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f : α E} (hf : μ) :
theorem measure_theory.mem_ℒp.to_Lp_sub {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f g : α E} (hf : μ) (hg : μ) :
_ =
@[protected, instance]
noncomputable def measure_theory.Lp.has_coe_to_fun {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α}  :
has_coe_to_fun μ) (λ (_x : μ)), α E)
Equations
@[ext]
theorem measure_theory.Lp.ext {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f g : μ)} (h : f =ᵐ[μ] g) :
f = g
theorem measure_theory.Lp.ext_iff {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f g : μ)} :
f = g f =ᵐ[μ] g
theorem measure_theory.Lp.mem_Lp_iff_snorm_lt_top {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f : α →ₘ[μ] E} :
f μ <
theorem measure_theory.Lp.mem_Lp_iff_mem_ℒp {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f : α →ₘ[μ] E} :
f μ
@[protected]
theorem measure_theory.Lp.antitone {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} {p q : ennreal} (hpq : p q) :
μ μ
@[simp]
theorem measure_theory.Lp.coe_fn_mk {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f : α →ₘ[μ] E} (hf : < ) :
f, hf⟩ = f
@[simp]
theorem measure_theory.Lp.coe_mk {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f : α →ₘ[μ] E} (hf : < ) :
f, hf⟩ = f
@[simp]
theorem measure_theory.Lp.to_Lp_coe_fn {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} (f : μ)) (hf : μ) :
theorem measure_theory.Lp.snorm_lt_top {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} (f : μ)) :
theorem measure_theory.Lp.snorm_ne_top {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} (f : μ)) :
@[protected, measurability]
theorem measure_theory.Lp.strongly_measurable {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} (f : μ)) :
@[protected, measurability]
theorem measure_theory.Lp.ae_strongly_measurable {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} (f : μ)) :
@[protected]
theorem measure_theory.Lp.mem_ℒp {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} (f : μ)) :
theorem measure_theory.Lp.coe_fn_zero {α : Type u_1} (E : Type u_2) {m0 : measurable_space α} (p : ennreal) (μ : measure_theory.measure α)  :
0 =ᵐ[μ] 0
theorem measure_theory.Lp.coe_fn_neg {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} (f : μ)) :
theorem measure_theory.Lp.coe_fn_add {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} (f g : μ)) :
(f + g) =ᵐ[μ] f + g
theorem measure_theory.Lp.coe_fn_sub {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} (f g : μ)) :
(f - g) =ᵐ[μ] f - g
theorem measure_theory.Lp.mem_Lp_const {E : Type u_2} {p : ennreal} (α : Type u_1) {m : measurable_space α} (μ : measure_theory.measure α) (c : E)  :
@[protected, instance]
noncomputable def measure_theory.Lp.has_norm {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α}  :
Equations
@[protected, instance]
noncomputable def measure_theory.Lp.has_nnnorm {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α}  :
Equations
@[protected, instance]
noncomputable def measure_theory.Lp.has_dist {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α}  :
Equations
@[protected, instance]
noncomputable def measure_theory.Lp.has_edist {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α}  :
Equations
theorem measure_theory.Lp.norm_def {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} (f : μ)) :
theorem measure_theory.Lp.nnnorm_def {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} (f : μ)) :
@[protected, simp, norm_cast]
theorem measure_theory.Lp.coe_nnnorm {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} (f : μ)) :
@[simp]
theorem measure_theory.Lp.norm_to_Lp {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} (f : α E) (hf : μ) :
@[simp]
theorem measure_theory.Lp.nnnorm_to_Lp {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} (f : α E) (hf : μ) :
theorem measure_theory.Lp.dist_def {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} (f g : μ)) :
theorem measure_theory.Lp.edist_def {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} (f g : μ)) :
@[simp]
theorem measure_theory.Lp.edist_to_Lp_to_Lp {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} (f g : α E) (hf : μ) (hg : μ) :
@[simp]
theorem measure_theory.Lp.edist_to_Lp_zero {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} (f : α E) (hf : μ) :
= μ
@[simp]
theorem measure_theory.Lp.nnnorm_zero {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α}  :
@[simp]
theorem measure_theory.Lp.norm_zero {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α}  :
theorem measure_theory.Lp.nnnorm_eq_zero_iff {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f : μ)} (hp : 0 < p) :
f‖₊ = 0 f = 0
theorem measure_theory.Lp.norm_eq_zero_iff {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {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} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f : μ)} :
f = 0 f =ᵐ[μ] 0
@[simp]
theorem measure_theory.Lp.nnnorm_neg {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} (f : μ)) :
@[simp]
theorem measure_theory.Lp.norm_neg {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} (f : μ)) :
theorem measure_theory.Lp.nnnorm_le_mul_nnnorm_of_ae_le_mul {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {c : nnreal} {f : μ)} {g : μ)} (h : ∀ᵐ (x : α) μ, f x‖₊ c * g x‖₊) :
theorem measure_theory.Lp.norm_le_mul_norm_of_ae_le_mul {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {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} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f : μ)} {g : μ)} (h : ∀ᵐ (x : α) μ, f x g x) :
theorem measure_theory.Lp.mem_Lp_of_nnnorm_ae_le_mul {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {c : nnreal} {f : α →ₘ[μ] E} {g : μ)} (h : ∀ᵐ (x : α) μ, f x‖₊ c * g x‖₊) :
f μ
theorem measure_theory.Lp.mem_Lp_of_ae_le_mul {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {c : } {f : α →ₘ[μ] E} {g : μ)} (h : ∀ᵐ (x : α) μ, f x c * g x) :
f μ
theorem measure_theory.Lp.mem_Lp_of_nnnorm_ae_le {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f : α →ₘ[μ] E} {g : μ)} (h : ∀ᵐ (x : α) μ, f x‖₊ g x‖₊) :
f μ
theorem measure_theory.Lp.mem_Lp_of_ae_le {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f : α →ₘ[μ] E} {g : μ)} (h : ∀ᵐ (x : α) μ, f x g x) :
f μ
theorem measure_theory.Lp.mem_Lp_of_ae_nnnorm_bound {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f : α →ₘ[μ] E} (C : nnreal) (hfC : ∀ᵐ (x : α) μ, f x‖₊ C) :
f μ
theorem measure_theory.Lp.mem_Lp_of_ae_bound {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f : α →ₘ[μ] E} (C : ) (hfC : ∀ᵐ (x : α) μ, f x C) :
f μ
theorem measure_theory.Lp.nnnorm_le_of_ae_bound {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f : μ)} {C : nnreal} (hfC : ∀ᵐ (x : α) μ, f x‖₊ C) :
theorem measure_theory.Lp.norm_le_of_ae_bound {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f : μ)} {C : } (hC : 0 C) (hfC : ∀ᵐ (x : α) μ, f x C) :
@[protected, instance]
noncomputable def measure_theory.Lp.normed_add_comm_group {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [hp : fact (1 p)] :
Equations
theorem measure_theory.Lp.mem_Lp_const_smul {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {𝕜 : Type u_5} [normed_ring 𝕜] [ E] [ E] (c : 𝕜) (f : μ)) :
c f μ
def measure_theory.Lp.Lp_submodule {α : Type u_1} (E : Type u_2) {m0 : measurable_space α} (p : ennreal) (μ : measure_theory.measure α) (𝕜 : Type u_5) [normed_ring 𝕜] [ E] [ 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} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {𝕜 : Type u_5} [normed_ring 𝕜] [ E] [ E] :
= μ
@[protected, instance]
def measure_theory.Lp.module {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {𝕜 : Type u_5} [normed_ring 𝕜] [ E] [ E] :
μ)
Equations
theorem measure_theory.Lp.coe_fn_smul {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {𝕜 : Type u_5} [normed_ring 𝕜] [ E] [ E] (c : 𝕜) (f : μ)) :
(c f) =ᵐ[μ] c f
@[protected, instance]
def measure_theory.Lp.is_central_scalar {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {𝕜 : Type u_5} [normed_ring 𝕜] [ E] [ E] [ E] [ E] [ E] :
μ)
@[protected, instance]
def measure_theory.Lp.smul_comm_class {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {𝕜 : Type u_5} {𝕜' : Type u_6} [normed_ring 𝕜] [normed_ring 𝕜'] [ E] [module 𝕜' E] [ E] [ E] [ 𝕜' E] :
𝕜' μ)
@[protected, instance]
def measure_theory.Lp.is_scalar_tower {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {𝕜 : Type u_5} {𝕜' : Type u_6} [normed_ring 𝕜] [normed_ring 𝕜'] [ E] [module 𝕜' E] [ E] [ E] [ 𝕜'] [ 𝕜' E] :
𝕜' μ)
@[protected, instance]
def measure_theory.Lp.has_bounded_smul {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {𝕜 : Type u_5} [normed_ring 𝕜] [ E] [ E] [fact (1 p)] :
μ)
@[protected, instance]
def measure_theory.Lp.normed_space {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {𝕜 : Type u_5} [normed_field 𝕜] [ E] [fact (1 p)] :
μ)
Equations
theorem measure_theory.mem_ℒp.to_Lp_const_smul {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {𝕜 : Type u_5} [normed_ring 𝕜] [ E] [ E] {f : α E} (c : 𝕜) (hf : μ) :
_ =

### 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 α} (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 α} (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 α} (s : set α) (c : G) (hμs : μ s 0) :
theorem measure_theory.snorm_indicator_le {α : Type u_1} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {s : set α} {E : Type u_2} (f : α E) :
p μ μ
theorem measure_theory.snorm_indicator_const {α : Type u_1} {G : Type u_4} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {s : set α} {c : G} (hs : measurable_set s) (hp : p 0) (hp_top : p ) :
measure_theory.snorm (s.indicator (λ (x : α), c)) p μ = c‖₊ * μ s ^ (1 / p.to_real)
theorem measure_theory.snorm_indicator_const' {α : Type u_1} {G : Type u_4} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {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.snorm_indicator_const_le {α : Type u_1} {G : Type u_4} {m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} (c : G) (p : ennreal) :
measure_theory.snorm (s.indicator (λ (x : α), c)) p μ c‖₊ * μ s ^ (1 / p.to_real)
theorem measure_theory.mem_ℒp.indicator {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {s : set α} {f : α E} (hs : measurable_set s) (hf : μ) :
p μ
theorem measure_theory.snorm_ess_sup_indicator_eq_snorm_ess_sup_restrict {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} {f : α F} (hs : measurable_set s) :
theorem measure_theory.snorm_indicator_eq_snorm_restrict {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {s : set α} {f : α F} (hs : measurable_set s) :
p μ = (μ.restrict s)
theorem measure_theory.mem_ℒp_indicator_iff_restrict {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {s : set α} {f : α E} (hs : measurable_set s) :
p μ (μ.restrict s)
theorem measure_theory.mem_ℒp_indicator_const {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} (p : ennreal) (hs : measurable_set s) (c : E) (hμsc : c = 0 μ s ) :
measure_theory.mem_ℒp (s.indicator (λ (_x : α), c)) p μ
theorem measure_theory.exists_snorm_indicator_le {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} (hp : p ) (c : E) {ε : ennreal} (hε : ε 0) :
(η : nnreal), 0 < η (s : set α), μ s η measure_theory.snorm (s.indicator (λ (x : α), c)) p μ ε

The `ℒ^p` norm of the indicator of a set is uniformly small if the set itself has small measure, for any `p < ∞`. Given here as an existential `∀ ε > 0, ∃ η > 0, ...` to avoid later management of `ℝ≥0∞`-arithmetic.

noncomputable def measure_theory.indicator_const_Lp {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} (p : ennreal) (hs : measurable_set s) (hμs : μ s ) (c : E) :
μ)

Indicator of a set as an element of `Lp`.

Equations
theorem measure_theory.indicator_const_Lp_coe_fn {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {s : set α} {hs : measurable_set s} {hμs : μ s } {c : E} :
hμs c) =ᵐ[μ] s.indicator (λ (_x : α), c)
theorem measure_theory.indicator_const_Lp_coe_fn_mem {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {s : set α} {hs : measurable_set s} {hμs : μ s } {c : E} :
∀ᵐ (x : α) μ, x s hμs c) x = c
theorem measure_theory.indicator_const_Lp_coe_fn_nmem {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {s : set α} {hs : measurable_set s} {hμs : μ s } {c : E} :
∀ᵐ (x : α) μ, x s hμs c) x = 0
theorem measure_theory.norm_indicator_const_Lp {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {s : set α} {hs : measurable_set s} {hμs : μ s } {c : E} (hp_ne_zero : p 0) (hp_ne_top : p ) :
c = c * (μ s).to_real ^ (1 / p.to_real)
theorem measure_theory.norm_indicator_const_Lp_top {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} {hs : measurable_set s} {hμs : μ s } {c : E} (hμs_ne_zero : μ s 0) :
theorem measure_theory.norm_indicator_const_Lp' {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {s : set α} {hs : measurable_set s} {hμs : μ s } {c : E} (hp_pos : p 0) (hμs_pos : μ s 0) :
c = c * (μ s).to_real ^ (1 / p.to_real)
@[simp]
theorem measure_theory.indicator_const_empty {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {c : E} :
theorem measure_theory.mem_ℒp_add_of_disjoint {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f g : α E} (h : )  :
theorem measure_theory.indicator_const_Lp_disjoint_union {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {s t : set α} (hs : measurable_set s) (ht : measurable_set t) (hμs : μ s ) (hμt : μ t ) (hst : s t = ) (c : E) :
= c + c

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

theorem measure_theory.mem_ℒp.norm_rpow_div {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f : α E} (hf : μ) (q : ennreal) :
measure_theory.mem_ℒp (λ (x : α), f x ^ q.to_real) (p / q) μ
theorem measure_theory.mem_ℒp_norm_rpow_iff {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {q : ennreal} {f : α E} (q_zero : q 0) (q_top : q ) :
measure_theory.mem_ℒp (λ (x : α), f x ^ q.to_real) (p / q) μ
theorem measure_theory.mem_ℒp.norm_rpow {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f : α E} (hf : μ) (hp_ne_zero : p 0) (hp_ne_top : p ) :
measure_theory.mem_ℒp (λ (x : α), f x ^ p.to_real) 1 μ

### Composition on `L^p`#

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

theorem lipschitz_with.comp_mem_ℒp {p : ennreal} {α : Type u_1} {E : Type u_2} {F : Type u_3} {K : nnreal} {μ : measure_theory.measure α} {f : α E} {g : E F} (hg : g) (g0 : g 0 = 0) (hL : μ) :
theorem measure_theory.mem_ℒp.of_comp_antilipschitz_with {p : ennreal} {α : Type u_1} {E : Type u_2} {F : Type u_3} {K' : nnreal} {μ : measure_theory.measure α} {f : α E} {g : E F} (hL : measure_theory.mem_ℒp (g f) p μ) (hg : uniform_continuous g) (hg' : g) (g0 : g 0 = 0) :
theorem lipschitz_with.mem_ℒp_comp_iff_of_antilipschitz {p : ennreal} {α : Type u_1} {E : Type u_2} {F : Type u_3} {K K' : nnreal} {μ : measure_theory.measure α} {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} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {g : E F} {c : nnreal} (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} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {g : E F} {c : nnreal} (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} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {g : E F} {c : nnreal} (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} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {g : E F} {c : nnreal} (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} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {g : E F} {c : nnreal} (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} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {g : E F} {c : nnreal} [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} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {g : E F} {c : nnreal} [fact (1 p)] (hg : g) (g0 : g 0 = 0) :
noncomputable def continuous_linear_map.comp_Lp {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {𝕜 : Type u_5} [ 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} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {𝕜 : Type u_5} [ E] [ F] (L : E →L[𝕜] F) (f : μ)) :
∀ᵐ (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 : ennreal} {μ : measure_theory.measure α} {𝕜 : Type u_5} [ E] [ F] (L : E →L[𝕜] F) (f : μ)) :
(L.comp_Lp f) =ᵐ[μ] λ (a : α), L (f a)
theorem continuous_linear_map.comp_mem_ℒp {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {𝕜 : Type u_5} [ E] [ F] (L : E →L[𝕜] F) (f : μ)) :
theorem continuous_linear_map.comp_mem_ℒp' {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {𝕜 : Type u_5} [ E] [ F] (L : E →L[𝕜] F) {f : α E} (hf : μ) :
theorem measure_theory.mem_ℒp.of_real {α : Type u_1} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {K : Type u_6} [is_R_or_C K] {f : α } (hf : μ) :
measure_theory.mem_ℒp (λ (x : α), (f x)) p μ
theorem measure_theory.mem_ℒp_re_im_iff {α : Type u_1} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {K : Type u_6} [is_R_or_C K] {f : α K} :
measure_theory.mem_ℒp (λ (x : α), is_R_or_C.re (f x)) p μ measure_theory.mem_ℒp (λ (x : α), is_R_or_C.im (f x)) p μ
theorem continuous_linear_map.add_comp_Lp {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {𝕜 : Type u_5} [ E] [ F] (L L' : E →L[𝕜] F) (f : μ)) :
(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 : ennreal} {μ : measure_theory.measure α} {𝕜 : Type u_5} [ E] [ F] {𝕜' : Type u_4} [normed_ring 𝕜'] [module 𝕜' F] [ F] [ 𝕜' F] (c : 𝕜') (L : E →L[𝕜] F) (f : μ)) :
(c L).comp_Lp f = c L.comp_Lp f
theorem continuous_linear_map.norm_comp_Lp_le {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {𝕜 : Type u_5} [ E] [ F] (L : E →L[𝕜] F) (f : μ)) :
noncomputable def continuous_linear_map.comp_Lpₗ {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : measurable_space α} (p : ennreal) (μ : measure_theory.measure α) {𝕜 : Type u_5} [ 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
noncomputable def continuous_linear_map.comp_LpL {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : measurable_space α} (p : ennreal) (μ : measure_theory.measure α) {𝕜 : Type u_5} [ 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 μ`. See also the similar

• `linear_map.comp_left` for functions,
• `continuous_linear_map.comp_left_continuous` for continuous functions,
• `continuous_linear_map.comp_left_continuous_bounded` for bounded continuous functions,
• `continuous_linear_map.comp_left_continuous_compact` for continuous functions on compact spaces.
Equations
• = _
theorem continuous_linear_map.coe_fn_comp_LpL {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {𝕜 : Type u_5} [ E] [ F] [fact (1 p)] (L : E →L[𝕜] F) (f : μ)) :
( f) =ᵐ[μ] λ (a : α), L (f a)
theorem continuous_linear_map.add_comp_LpL {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {𝕜 : Type u_5} [ E] [ F] [fact (1 p)] (L L' : E →L[𝕜] F) :
(L + L') =
theorem continuous_linear_map.smul_comp_LpL {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {𝕜 : Type u_5} [ E] [ F] [fact (1 p)] {𝕜' : Type u_4} [normed_ring 𝕜'] [module 𝕜' F] [ F] [ 𝕜' F] (c : 𝕜') (L : E →L[𝕜] F) :
(c L) =
theorem continuous_linear_map.norm_compLpL_le {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {𝕜 : Type u_5} [ E] [ F] [fact (1 p)] (L : E →L[𝕜] F) :
theorem measure_theory.indicator_const_Lp_eq_to_span_singleton_comp_Lp {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} [ F] (hs : measurable_set s) (hμs : μ s ) (x : F) :
x =
theorem measure_theory.mem_ℒp.pos_part {α : Type u_1} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f : α } (hf : μ) :
measure_theory.mem_ℒp (λ (x : α), linear_order.max (f x) 0) p μ
theorem measure_theory.mem_ℒp.neg_part {α : Type u_1} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f : α } (hf : μ) :
measure_theory.mem_ℒp (λ (x : α), linear_order.max (-f x) 0) p μ
noncomputable def measure_theory.Lp.pos_part {α : Type u_1} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} (f : μ)) :
μ)

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

Equations
noncomputable def measure_theory.Lp.neg_part {α : Type u_1} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} (f : μ)) :
μ)

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

Equations
@[norm_cast]
theorem measure_theory.Lp.coe_pos_part {α : Type u_1} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} (f : μ)) :
theorem measure_theory.Lp.coe_fn_pos_part {α : Type u_1} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} (f : μ)) :
=ᵐ[μ] λ (a : α), linear_order.max (f a) 0
theorem measure_theory.Lp.coe_fn_neg_part_eq_max {α : Type u_1} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} (f : μ)) :
∀ᵐ (a : α) μ, = linear_order.max (-f a) 0
theorem measure_theory.Lp.coe_fn_neg_part {α : Type u_1} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} (f : μ)) :
∀ᵐ (a : α) μ, = -linear_order.min (f a) 0
theorem measure_theory.Lp.continuous_pos_part {α : Type u_1} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [fact (1 p)] :
continuous (λ (f : μ)),
theorem measure_theory.Lp.continuous_neg_part {α : Type u_1} {m0 : measurable_space α} {p : ennreal} {μ : 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} {m0 : measurable_space α} {μ : measure_theory.measure α} {ι : 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 (nhds (f_lim x))) :
p μ = (∫⁻ (a : α), filter.liminf (λ (m : ι), f m a‖₊ ^ p) filter.at_top μ) ^ (1 / p)
theorem measure_theory.Lp.snorm'_lim_le_liminf_snorm' {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {E : Type u_2} {f : α E} {p : } (hp_pos : 0 < p) (hf : (n : ), ) {f_lim : α E} (h_lim : ∀ᵐ (x : α) μ, filter.tendsto (λ (n : ), f n x) filter.at_top (nhds (f_lim x))) :
p μ filter.liminf (λ (n : ), p μ) filter.at_top
theorem measure_theory.Lp.snorm_exponent_top_lim_eq_ess_sup_liminf {α : Type u_1} {G : Type u_4} {m0 : measurable_space α} {μ : measure_theory.measure α} {ι : Type u_2} [nonempty ι] [linear_order ι] {f : ι α G} {f_lim : α G} (h_lim : ∀ᵐ (x : α) μ, filter.tendsto (λ (n : ι), f n x) filter.at_top (nhds (f_lim x))) :
measure_theory.snorm f_lim μ = ess_sup (λ (x : α), filter.liminf (λ (m : ι), f m x‖₊) filter.at_top) μ
theorem measure_theory.Lp.snorm_exponent_top_lim_le_liminf_snorm_exponent_top {α : Type u_1} {F : Type u_3} {m0 : measurable_space α} {μ : measure_theory.measure α} {ι : Type u_2} [nonempty ι] [countable ι] [linear_order ι] {f : ι α F} {f_lim : α F} (h_lim : ∀ᵐ (x : α) μ, filter.tendsto (λ (n : ι), f n x) filter.at_top (nhds (f_lim x))) :
theorem measure_theory.Lp.snorm_lim_le_liminf_snorm {α : Type u_1} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {E : Type u_2} {f : α E} (hf : (n : ), ) (f_lim : α E) (h_lim : ∀ᵐ (x : α) μ, filter.tendsto (λ (n : ), f n x) filter.at_top (nhds (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} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {ι : Type u_3} {fi : filter ι} [fact (1 p)] (f : ι μ)) (f_lim : μ)) :
fi (nhds f_lim) filter.tendsto (λ (n : ι), measure_theory.snorm ((f n) - f_lim) p μ) fi (nhds 0)
theorem measure_theory.Lp.tendsto_Lp_iff_tendsto_ℒp {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {ι : Type u_3} {fi : filter ι} [fact (1 p)] (f : ι μ)) (f_lim : α E) (f_lim_ℒp : p μ) :
fi (nhds f_lim_ℒp)) filter.tendsto (λ (n : ι), measure_theory.snorm ((f n) - f_lim) p μ) fi (nhds 0)
theorem measure_theory.Lp.tendsto_Lp_iff_tendsto_ℒp'' {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {ι : Type u_3} {fi : filter ι} [fact (1 p)] (f : ι α E) (f_ℒp : (n : ι), p μ) (f_lim : α E) (f_lim_ℒp : p μ) :
filter.tendsto (λ (n : ι), _) fi (nhds f_lim_ℒp)) filter.tendsto (λ (n : ι), measure_theory.snorm (f n - f_lim) p μ) fi (nhds 0)
theorem measure_theory.Lp.tendsto_Lp_of_tendsto_ℒp {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {ι : 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 (nhds 0)) :
fi (nhds f_lim_ℒp))
theorem measure_theory.Lp.cauchy_seq_Lp_iff_cauchy_seq_ℒp {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {ι : 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 (nhds 0)
theorem measure_theory.Lp.complete_space_Lp_of_cauchy_complete_ℒp {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [hp : fact (1 p)] (H : (f : α E), ( (n : ), p μ) (B : , ∑' (i : ), B i < ( (N n m : ), N n N m measure_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 (nhds 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} {m0 : measurable_space α} {μ : measure_theory.measure α} {f : α E} {p : } (hf : (n : ), ) (hp1 : 1 p) {B : ennreal} (hB : ∑' (i : ), B i ) (h_cau : (N n m : ), N n N m measure_theory.snorm' (f n - f m) p μ < B N) :
∀ᵐ (x : α) μ, (l : E), filter.tendsto (λ (n : ), f n x) filter.at_top (nhds l)
theorem measure_theory.Lp.ae_tendsto_of_cauchy_snorm {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f : α E} (hf : (n : ), ) (hp : 1 p) {B : ennreal} (hB : ∑' (i : ), B i ) (h_cau : (N n m : ), N n N m measure_theory.snorm (f n - f m) p μ < B N) :
∀ᵐ (x : α) μ, (l : E), filter.tendsto (λ (n : ), f n x) filter.at_top (nhds l)
theorem measure_theory.Lp.cauchy_tendsto_of_tendsto {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f : α E} (hf : (n : ), ) (f_lim : α E) {B : ennreal} (hB : ∑' (i : ), B i ) (h_cau : (N n m : ), N n N m measure_theory.snorm (f n - f m) p μ < B N) (h_lim : ∀ᵐ (x : α) μ, filter.tendsto (λ (n : ), f n x) filter.at_top (nhds (f_lim x))) :
filter.tendsto (λ (n : ), measure_theory.snorm (f n - f_lim) p μ) filter.at_top (nhds 0)
theorem measure_theory.Lp.mem_ℒp_of_cauchy_tendsto {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} (hp : 1 p) {f : α E} (hf : (n : ), p μ) (f_lim : α E) (h_lim_meas : μ) (h_tendsto : filter.tendsto (λ (n : ), measure_theory.snorm (f n - f_lim) p μ) filter.at_top (nhds 0)) :
p μ
theorem measure_theory.Lp.cauchy_complete_ℒp {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} (hp : 1 p) {f : α E} (hf : (n : ), p μ) {B : ennreal} (hB : ∑' (i : ), B i ) (h_cau : (N n m : ), N n N m measure_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 (nhds 0)

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

@[protected, instance]
def measure_theory.Lp.complete_space {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [hp : fact (1 p)] :

### Continuous functions in `Lp`#

noncomputable def measure_theory.Lp.bounded_continuous_function {α : Type u_1} (E : Type u_2) {m0 : measurable_space α} (p : ennreal) (μ : measure_theory.measure α) [borel_space α]  :

An additive subgroup of `Lp E p μ`, consisting of the equivalence classes which contain a bounded continuous representative.

Equations
theorem measure_theory.Lp.mem_bounded_continuous_function_iff {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [borel_space α] {f : μ)} :
(f₀ : ,

By definition, the elements of `Lp.bounded_continuous_function E p μ` are the elements of `Lp E p μ` which contain a bounded continuous representative.

theorem bounded_continuous_function.mem_Lp {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [borel_space α] (f : E) :

A bounded continuous function on a finite-measure space is in `Lp`.

theorem bounded_continuous_function.Lp_nnnorm_le {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [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.

theorem bounded_continuous_function.Lp_norm_le {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [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.

noncomputable def bounded_continuous_function.to_Lp_hom {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} (p : ennreal) (μ : measure_theory.measure α) [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
theorem bounded_continuous_function.range_to_Lp_hom {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} (p : ennreal) (μ : measure_theory.measure α) [borel_space α] [fact (1 p)] :
noncomputable def bounded_continuous_function.to_Lp {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} (p : ennreal) (μ : measure_theory.measure α) [borel_space α] (𝕜 : Type u_5) [fact (1 p)] [normed_field 𝕜] [ 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} {m0 : measurable_space α} (p : ennreal) (μ : measure_theory.measure α) [borel_space α] (𝕜 : Type u_5) [fact (1 p)] [normed_field 𝕜] [ E] (f : E) :
theorem bounded_continuous_function.range_to_Lp {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} (p : ennreal) (μ : measure_theory.measure α) [borel_space α] {𝕜 : Type u_5} [fact (1 p)] [normed_field 𝕜] [ E] :
theorem bounded_continuous_function.to_Lp_norm_le {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} (μ : measure_theory.measure α) [borel_space α] {𝕜 : Type u_5} [fact (1 p)] [ E] :
theorem bounded_continuous_function.to_Lp_inj {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} (μ : measure_theory.measure α) [borel_space α] {𝕜 : Type u_5} [fact (1 p)] {f g : E} [normed_field 𝕜] [ E] :
f = g f = g
theorem bounded_continuous_function.to_Lp_injective {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} (μ : measure_theory.measure α) [borel_space α] {𝕜 : Type u_5} [fact (1 p)] [normed_field 𝕜] [ E] :
noncomputable def continuous_map.to_Lp {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} (p : ennreal) (μ : measure_theory.measure α) [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.range_to_Lp {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} (p : ennreal) (μ : measure_theory.measure α) [borel_space α] {𝕜 : Type u_5} [fact (1 p)] [normed_field 𝕜] [ E] :
theorem continuous_map.coe_fn_to_Lp {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} (μ : measure_theory.measure α) [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} {m0 : measurable_space α} {p : ennreal} (μ : measure_theory.measure α) [borel_space α] {𝕜 : Type u_5} [fact (1 p)] [normed_field 𝕜] [ E] (f : C(α, E)) :
𝕜) f =
@[simp]
theorem continuous_map.to_Lp_comp_to_continuous_map {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} (μ : measure_theory.measure α) [borel_space α] {𝕜 : Type u_5} [fact (1 p)] [normed_field 𝕜] [ E] (f : E) :
@[simp]
theorem continuous_map.coe_to_Lp {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} (μ : measure_theory.measure α) [borel_space α] {𝕜 : Type u_5} [fact (1 p)] [normed_field 𝕜] [ E] (f : C(α, E)) :
( 𝕜) f) =
theorem continuous_map.to_Lp_injective {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} (μ : measure_theory.measure α) [borel_space α] {𝕜 : Type u_5} [fact (1 p)] [normed_field 𝕜] [ E] :
theorem continuous_map.to_Lp_inj {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} (μ : measure_theory.measure α) [borel_space α] {𝕜 : Type u_5} [fact (1 p)] {f g : C(α, E)} [normed_field 𝕜] [ E] :
𝕜) f = 𝕜) g f = g
theorem continuous_map.has_sum_of_has_sum_Lp {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [borel_space α] {𝕜 : Type u_5} [fact (1 p)] {β : Type u_3} [normed_field 𝕜] [ E] {g : β C(α, E)} {f : C(α, E)} (hg : summable g) (hg2 : has_sum ( 𝕜) g) ( 𝕜) f)) :
f

If a sum of continuous functions `g n` is convergent, and the same sum converges in `Lᵖ` to `h`, then in fact `g n` converges uniformly to `h`.

theorem continuous_map.to_Lp_norm_eq_to_Lp_norm_coe {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} (μ : measure_theory.measure α) [borel_space α] {𝕜 : Type u_5} [fact (1 p)] [ E] :
theorem continuous_map.to_Lp_norm_le {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} (μ : measure_theory.measure α) [borel_space α] {𝕜 : Type u_5} [fact (1 p)] [ E] :

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

theorem measure_theory.Lp.pow_mul_meas_ge_le_norm {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} (f : μ)) (hp_ne_zero : p 0) (hp_ne_top : p ) (ε : ennreal) :
* μ {x : α | ε f x‖₊ ^ p.to_real}) ^ (1 / p.to_real)
theorem measure_theory.Lp.mul_meas_ge_le_pow_norm {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} (f : μ)) (hp_ne_zero : p 0) (hp_ne_top : p ) (ε : ennreal) :
ε * μ {x : α | ε f x‖₊ ^ p.to_real}
theorem measure_theory.Lp.mul_meas_ge_le_pow_norm' {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} (f : μ)) (hp_ne_zero : p 0) (hp_ne_top : p ) (ε : ennreal) :
ε ^ p.to_real * μ {x : α | ε f x‖₊}

A version of Markov's inequality with elements of Lp.

theorem measure_theory.Lp.meas_ge_le_mul_pow_norm {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} (f : μ)) (hp_ne_zero : p 0) (hp_ne_top : p ) {ε : ennreal} (hε : ε 0) :
μ {x : α | ε f x‖₊} ε⁻¹ ^ p.to_real *