mathlib3 documentation

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 #

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

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

Notations #

Implementation #

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

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

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

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

Lp space #

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

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

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

Equations
@[protected, instance]
noncomputable def measure_theory.Lp.has_coe_to_fun {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] :
has_coe_to_fun (measure_theory.Lp E p μ) (λ (_x : (measure_theory.Lp E p μ)), α E)
Equations
@[ext]
theorem measure_theory.Lp.ext {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] {f g : (measure_theory.Lp E p μ)} (h : f =ᵐ[μ] g) :
f = g
theorem measure_theory.Lp.ext_iff {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] {f g : (measure_theory.Lp E p μ)} :
f = g f =ᵐ[μ] g
@[protected]
@[simp]
theorem measure_theory.Lp.coe_fn_mk {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] {f : α →ₘ[μ] E} (hf : measure_theory.snorm f p μ < ) :
f, hf⟩ = f
@[simp]
theorem measure_theory.Lp.coe_mk {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] {f : α →ₘ[μ] E} (hf : measure_theory.snorm f p μ < ) :
f, hf⟩ = f
@[protected, measurability]
@[protected, measurability]
@[protected]
theorem measure_theory.Lp.coe_fn_add {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] (f g : (measure_theory.Lp E p μ)) :
(f + g) =ᵐ[μ] f + g
theorem measure_theory.Lp.coe_fn_sub {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] (f g : (measure_theory.Lp E p μ)) :
(f - g) =ᵐ[μ] f - g
@[protected, instance]
noncomputable def measure_theory.Lp.has_norm {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] :
Equations
@[protected, instance]
noncomputable def measure_theory.Lp.has_nnnorm {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] :
Equations
@[protected, instance]
noncomputable def measure_theory.Lp.has_dist {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] :
Equations
@[protected, instance]
noncomputable def measure_theory.Lp.has_edist {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] :
Equations
@[protected, simp, norm_cast]
@[simp]
@[simp]
theorem measure_theory.Lp.norm_zero {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] :
theorem measure_theory.Lp.nnnorm_eq_zero_iff {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] {f : (measure_theory.Lp E p μ)} (hp : 0 < p) :
f‖₊ = 0 f = 0
theorem measure_theory.Lp.norm_eq_zero_iff {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] {f : (measure_theory.Lp E p μ)} (hp : 0 < p) :
f = 0 f = 0
@[simp]
@[simp]
theorem measure_theory.Lp.norm_neg {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] (f : (measure_theory.Lp E p μ)) :
theorem measure_theory.Lp.norm_le_mul_norm_of_ae_le_mul {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] [normed_add_comm_group F] {c : } {f : (measure_theory.Lp E p μ)} {g : (measure_theory.Lp F p μ)} (h : ∀ᵐ (x : α) μ, f x c * g x) :
theorem measure_theory.Lp.mem_Lp_of_nnnorm_ae_le_mul {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] [normed_add_comm_group F] {c : nnreal} {f : α →ₘ[μ] E} {g : (measure_theory.Lp F p μ)} (h : ∀ᵐ (x : α) μ, f x‖₊ c * g x‖₊) :
theorem measure_theory.Lp.mem_Lp_of_ae_le_mul {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] [normed_add_comm_group F] {c : } {f : α →ₘ[μ] E} {g : (measure_theory.Lp F p μ)} (h : ∀ᵐ (x : α) μ, f x c * g x) :
theorem measure_theory.Lp.mem_Lp_of_nnnorm_ae_le {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] [normed_add_comm_group F] {f : α →ₘ[μ] E} {g : (measure_theory.Lp F p μ)} (h : ∀ᵐ (x : α) μ, f x‖₊ g x‖₊) :
theorem measure_theory.Lp.mem_Lp_of_ae_le {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] [normed_add_comm_group F] {f : α →ₘ[μ] E} {g : (measure_theory.Lp F p μ)} (h : ∀ᵐ (x : α) μ, f x g x) :
theorem measure_theory.Lp.mem_Lp_of_ae_bound {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] [measure_theory.is_finite_measure μ] {f : α →ₘ[μ] E} (C : ) (hfC : ∀ᵐ (x : α) μ, f x C) :
theorem measure_theory.Lp.mem_Lp_const_smul {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] {𝕜 : Type u_5} [normed_ring 𝕜] [module 𝕜 E] [has_bounded_smul 𝕜 E] (c : 𝕜) (f : (measure_theory.Lp E p μ)) :
def measure_theory.Lp.Lp_submodule {α : Type u_1} (E : Type u_2) {m0 : measurable_space α} (p : ennreal) (μ : measure_theory.measure α) [normed_add_comm_group E] (𝕜 : Type u_5) [normed_ring 𝕜] [module 𝕜 E] [has_bounded_smul 𝕜 E] :
submodule 𝕜 →ₘ[μ] E)

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

Equations
theorem measure_theory.Lp.coe_fn_smul {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] {𝕜 : Type u_5} [normed_ring 𝕜] [module 𝕜 E] [has_bounded_smul 𝕜 E] (c : 𝕜) (f : (measure_theory.Lp E p μ)) :
(c f) =ᵐ[μ] c f
@[protected, instance]
@[protected, instance]
def measure_theory.Lp.smul_comm_class {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] {𝕜 : Type u_5} {𝕜' : Type u_6} [normed_ring 𝕜] [normed_ring 𝕜'] [module 𝕜 E] [module 𝕜' E] [has_bounded_smul 𝕜 E] [has_bounded_smul 𝕜' E] [smul_comm_class 𝕜 𝕜' 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 α} [normed_add_comm_group E] {𝕜 : Type u_5} {𝕜' : Type u_6} [normed_ring 𝕜] [normed_ring 𝕜'] [module 𝕜 E] [module 𝕜' E] [has_bounded_smul 𝕜 E] [has_bounded_smul 𝕜' E] [has_smul 𝕜 𝕜'] [is_scalar_tower 𝕜 𝕜' 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 α} [normed_add_comm_group E] {𝕜 : Type u_5} [normed_ring 𝕜] [module 𝕜 E] [has_bounded_smul 𝕜 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 α} [normed_add_comm_group E] {𝕜 : Type u_5} [normed_field 𝕜] [normed_space 𝕜 E] [fact (1 p)] :
Equations
theorem measure_theory.mem_ℒp.to_Lp_const_smul {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] {𝕜 : Type u_5} [normed_ring 𝕜] [module 𝕜 E] [has_bounded_smul 𝕜 E] {f : α E} (c : 𝕜) (hf : measure_theory.mem_ℒp f p μ) :

Indicator of a set as an element of Lᵖ #

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

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

Indicator of a set as an element of Lp.

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

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

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

Composition on L^p #

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

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

When g is a Lipschitz function sending 0 to 0 and f is in Lp, then 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 α} [normed_add_comm_group E] [normed_add_comm_group F] {g : E F} {c : nnreal} (hg : lipschitz_with c g) (g0 : g 0 = 0) (f : (measure_theory.Lp E p μ)) :
(hg.comp_Lp g0 f) =ᵐ[μ] g f
@[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 α} [normed_add_comm_group E] [normed_add_comm_group F] {g : E F} {c : nnreal} (hg : lipschitz_with c g) (g0 : g 0 = 0) :
hg.comp_Lp g0 0 = 0
theorem lipschitz_with.norm_comp_Lp_sub_le {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] [normed_add_comm_group F] {g : E F} {c : nnreal} (hg : lipschitz_with c g) (g0 : g 0 = 0) (f f' : (measure_theory.Lp E p μ)) :
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 α} [normed_add_comm_group E] [normed_add_comm_group F] {g : E F} {c : nnreal} (hg : lipschitz_with c g) (g0 : g 0 = 0) (f : (measure_theory.Lp E p μ)) :
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 α} [normed_add_comm_group E] [normed_add_comm_group F] {g : E F} {c : nnreal} [fact (1 p)] (hg : lipschitz_with c g) (g0 : g 0 = 0) :
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 α} [normed_add_comm_group E] [normed_add_comm_group F] {g : E F} {c : nnreal} [fact (1 p)] (hg : lipschitz_with c 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 α} [normed_add_comm_group E] [normed_add_comm_group F] {𝕜 : Type u_5} [nontrivially_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] (L : E →L[𝕜] F) (f : (measure_theory.Lp E p μ)) :

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 α} [normed_add_comm_group E] [normed_add_comm_group F] {𝕜 : Type u_5} [nontrivially_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] (L : E →L[𝕜] F) (f : (measure_theory.Lp E p μ)) :
∀ᵐ (a : α) μ, (L.comp_Lp f) a = L (f a)
theorem continuous_linear_map.coe_fn_comp_Lp' {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] [normed_add_comm_group F] {𝕜 : Type u_5} [nontrivially_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] (L : E →L[𝕜] F) (f : (measure_theory.Lp E p μ)) :
(L.comp_Lp f) =ᵐ[μ] λ (a : α), L (f a)
theorem continuous_linear_map.comp_mem_ℒp {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] [normed_add_comm_group F] {𝕜 : Type u_5} [nontrivially_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] (L : E →L[𝕜] F) (f : (measure_theory.Lp E p μ)) :
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 α} [normed_add_comm_group E] [normed_add_comm_group F] {𝕜 : Type u_5} [nontrivially_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] (L : E →L[𝕜] F) {f : α E} (hf : measure_theory.mem_ℒp f p μ) :
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 f p μ) :
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} :
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 α} [normed_add_comm_group E] [normed_add_comm_group F] {𝕜 : Type u_5} [nontrivially_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] (L L' : E →L[𝕜] F) (f : (measure_theory.Lp E p μ)) :
(L + L').comp_Lp f = L.comp_Lp f + L'.comp_Lp f
theorem continuous_linear_map.smul_comp_Lp {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] [normed_add_comm_group F] {𝕜 : Type u_5} [nontrivially_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] {𝕜' : Type u_4} [normed_ring 𝕜'] [module 𝕜' F] [has_bounded_smul 𝕜' F] [smul_comm_class 𝕜 𝕜' F] (c : 𝕜') (L : E →L[𝕜] F) (f : (measure_theory.Lp E p μ)) :
(c L).comp_Lp f = c L.comp_Lp f
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 α} [normed_add_comm_group E] [normed_add_comm_group F] {𝕜 : Type u_5} [nontrivially_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] (L : E →L[𝕜] F) (f : (measure_theory.Lp E p μ)) :
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 α) [normed_add_comm_group E] [normed_add_comm_group F] {𝕜 : Type u_5} [nontrivially_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 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 α) [normed_add_comm_group E] [normed_add_comm_group F] {𝕜 : Type u_5} [nontrivially_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] [fact (1 p)] (L : E →L[𝕜] F) :

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

Equations
theorem continuous_linear_map.coe_fn_comp_LpL {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] [normed_add_comm_group F] {𝕜 : Type u_5} [nontrivially_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] [fact (1 p)] (L : E →L[𝕜] F) (f : (measure_theory.Lp E p μ)) :
((continuous_linear_map.comp_LpL p μ L) f) =ᵐ[μ] λ (a : α), L (f a)
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 α} [normed_add_comm_group E] [normed_add_comm_group F] {𝕜 : Type u_5} [nontrivially_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] [fact (1 p)] {𝕜' : Type u_4} [normed_ring 𝕜'] [module 𝕜' F] [has_bounded_smul 𝕜' F] [smul_comm_class 𝕜 𝕜' F] (c : 𝕜') (L : E →L[𝕜] F) :
theorem measure_theory.mem_ℒp.pos_part {α : Type u_1} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {f : α } (hf : measure_theory.mem_ℒp f p μ) :
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 f p μ) :
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 : (measure_theory.Lp p μ)) :

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 : (measure_theory.Lp p μ)) :

Negative part of a function in L^p.

Equations

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 α} [normed_add_comm_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 (nhds (f_lim x))) :
measure_theory.snorm' f_lim 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} [normed_add_comm_group E] {f : α E} {p : } (hp_pos : 0 < p) (hf : (n : ), measure_theory.ae_strongly_measurable (f n) μ) {f_lim : α E} (h_lim : ∀ᵐ (x : α) μ, filter.tendsto (λ (n : ), f n x) filter.at_top (nhds (f_lim x))) :
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 α} [normed_add_comm_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 (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 α} [normed_add_comm_group F] {ι : 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} [normed_add_comm_group E] {f : α E} (hf : (n : ), measure_theory.ae_strongly_measurable (f 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 α} [normed_add_comm_group E] {ι : Type u_3} {fi : filter ι} [fact (1 p)] (f : ι (measure_theory.Lp E p μ)) (f_lim : (measure_theory.Lp E p μ)) :
filter.tendsto f 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 α} [normed_add_comm_group E] {ι : Type u_3} {fi : filter ι} [fact (1 p)] (f : ι (measure_theory.Lp E p μ)) (f_lim : α E) (f_lim_ℒp : measure_theory.mem_ℒp f_lim p μ) :
filter.tendsto f fi (nhds (measure_theory.mem_ℒp.to_Lp f_lim 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 α} [normed_add_comm_group E] {ι : Type u_3} {fi : filter ι} [fact (1 p)] (f : ι α E) (f_ℒp : (n : ι), measure_theory.mem_ℒp (f n) p μ) (f_lim : α E) (f_lim_ℒp : measure_theory.mem_ℒp f_lim p μ) :
filter.tendsto (λ (n : ι), measure_theory.mem_ℒp.to_Lp (f n) _) fi (nhds (measure_theory.mem_ℒp.to_Lp f_lim 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 α} [normed_add_comm_group E] {ι : Type u_3} {fi : filter ι} [hp : fact (1 p)] {f : ι (measure_theory.Lp E p μ)} (f_lim : α E) (f_lim_ℒp : measure_theory.mem_ℒp f_lim p μ) (h_tendsto : filter.tendsto (λ (n : ι), measure_theory.snorm ((f n) - f_lim) p μ) fi (nhds 0)) :
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 α} [normed_add_comm_group E] {ι : Type u_3} [nonempty ι] [semilattice_sup ι] [hp : fact (1 p)] (f : ι (measure_theory.Lp E p μ)) :
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 α} [normed_add_comm_group E] [hp : fact (1 p)] (H : (f : α E), ( (n : ), measure_theory.mem_ℒp (f n) p μ) (B : ennreal), ∑' (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 : measure_theory.mem_ℒp f_lim 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 α} [normed_add_comm_group E] [complete_space E] {f : α E} {p : } (hf : (n : ), measure_theory.ae_strongly_measurable (f 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 α} [normed_add_comm_group E] [complete_space E] {f : α E} (hf : (n : ), measure_theory.ae_strongly_measurable (f 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 α} [normed_add_comm_group E] {f : α E} (hf : (n : ), measure_theory.ae_strongly_measurable (f 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 α} [normed_add_comm_group E] (hp : 1 p) {f : α E} (hf : (n : ), measure_theory.mem_ℒp (f n) p μ) (f_lim : α E) (h_lim_meas : measure_theory.ae_strongly_measurable f_lim μ) (h_tendsto : filter.tendsto (λ (n : ), measure_theory.snorm (f n - f_lim) p μ) filter.at_top (nhds 0)) :
theorem measure_theory.Lp.cauchy_complete_ℒp {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] [complete_space E] (hp : 1 p) {f : α E} (hf : (n : ), measure_theory.mem_ℒp (f 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 : measure_theory.mem_ℒp f_lim 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]

Continuous functions in Lp #

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

Equations

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

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.

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.

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.has_sum_of_has_sum_Lp {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] [topological_space α] [borel_space α] [second_countable_topology_either α E] [compact_space α] [measure_theory.is_finite_measure μ] {𝕜 : Type u_5} [fact (1 p)] {β : Type u_3} [μ.is_open_pos_measure] [normed_field 𝕜] [normed_space 𝕜 E] {g : β C(α, E)} {f : C(α, E)} (hg : summable g) (hg2 : has_sum ((continuous_map.to_Lp p μ 𝕜) g) ((continuous_map.to_Lp p μ 𝕜) 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 measure_theory.Lp.pow_mul_meas_ge_le_norm {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} [normed_add_comm_group E] (f : (measure_theory.Lp E p μ)) (hp_ne_zero : p 0) (hp_ne_top : p ) (ε : ennreal) :
* μ {x : α | ε f x‖₊ ^ p.to_real}) ^ (1 / p.to_real) ennreal.of_real f
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 α} [normed_add_comm_group E] (f : (measure_theory.Lp E p μ)) (hp_ne_zero : p 0) (hp_ne_top : p ) (ε : ennreal) :
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 α} [normed_add_comm_group E] (f : (measure_theory.Lp E p μ)) (hp_ne_zero : p 0) (hp_ne_top : p ) (ε : ennreal) :

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 α} [normed_add_comm_group E] (f : (measure_theory.Lp E p μ)) (hp_ne_zero : p 0) (hp_ne_top : p ) {ε : ennreal} (hε : ε 0) :