ℒ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)
forf : α → F
andp : ℝ
, whereα
is a measurable space andF
is a normed group. -
snorm_ess_sup f μ
: seminorm inℒ∞
, equal to the essential supremumess_sup ∥f∥ μ
. -
snorm f p μ
: forp : ℝ≥0∞
, seminorm inℒp
, equal to0
forp=0
, tosnorm' f p μ
for0 < p < ∞
and tosnorm_ess_sup f μ
forp = ∞
. -
mem_ℒp f p μ
: property that the functionf
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 thatsnorm f p μ
is finite. Defined as anadd_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 onLp
of a continuous linear map.Lp.pos_part
is the positive part of anLp
function.Lp.neg_part
is the negative part of anLp
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 typeLp E 1 μ
.α →₂[μ] E
: the typeLp 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,
filter_upwards [coe_fn_add (f + g) h, coe_fn_add f g, coe_fn_add f (g + h), coe_fn_add g h],
assume a ha1 ha2 ha3 ha4,
simp only [ha1, ha2, ha3, ha4, add_assoc],
end
The lemma coe_fn_add
states that the coercion of f + g
coincides almost everywhere with the sum
of the coercions of f
and g
. All such lemmas use coe_fn
in their name, to distinguish the
function coercion from the coercion to almost everywhere defined functions.
ℒp seminorm #
We define the ℒp seminorm, denoted by snorm f p μ
. For real p
, it is given by an integral
formula (for which we use the notation snorm' f p μ
), and for p = ∞
it is the essential
supremum (for which we use the notation snorm_ess_sup f μ
).
We also define a predicate mem_ℒp f p μ
, requesting that a function is almost everywhere
measurable and has finite snorm f p μ
.
This paragraph is devoted to the basic properties of these definitions. It is constructed as
follows: for a given property, we prove it for snorm'
and snorm_ess_sup
when it makes sense,
deduce it for snorm
, and translate it in terms of mem_ℒp
.
(∫ ∥f a∥^q ∂μ) ^ (1/q)
, which is a seminorm on the space of measurable functions for which
this quantity is finite
seminorm for ℒ∞
, equal to the essential supremum of ∥f∥
.
Equations
- measure_theory.snorm_ess_sup f μ = ess_sup (λ (x : α), ↑(nnnorm (f x))) μ
ℒ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
- measure_theory.snorm f p μ = ite (p = 0) 0 (ite (p = ⊤) (measure_theory.snorm_ess_sup f μ) (measure_theory.snorm' f p.to_real μ))
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
- measure_theory.mem_ℒp f p μ = (ae_measurable f μ ∧ measure_theory.snorm f p μ < ⊤)
Lp space #
The space of equivalence classes of measurable functions for which snorm f p μ < ∞
.
Lp space
make an element of Lp from a function verifying mem_ℒp
Equations
- measure_theory.mem_ℒp.to_Lp f h_mem_ℒp = ⟨measure_theory.ae_eq_fun.mk f _, _⟩
Equations
- measure_theory.Lp.has_coe_to_fun = {F := λ (_x : ↥(measure_theory.Lp E p μ)), α → E, coe := λ (f : ↥(measure_theory.Lp E p μ)), ⇑↑f}
Equations
- measure_theory.Lp.has_norm = {norm := λ (f : ↥(measure_theory.Lp E p μ)), (measure_theory.snorm ⇑f p μ).to_real}
Equations
- measure_theory.Lp.has_dist = {dist := λ (f g : ↥(measure_theory.Lp E p μ)), ∥f - g∥}
Equations
- measure_theory.Lp.has_edist = {edist := λ (f g : ↥(measure_theory.Lp E p μ)), ennreal.of_real (dist f g)}
Equations
- measure_theory.Lp.normed_group = normed_group.of_core ↥(measure_theory.Lp E p μ) measure_theory.Lp.normed_group._proof_2
The 𝕜
-submodule of elements of α →ₘ[μ] E
whose Lp
norm is finite. This is Lp E p μ
,
with extra structure.
Equations
- measure_theory.Lp.Lp_submodule E p μ 𝕜 = {carrier := (measure_theory.Lp E p μ).carrier, zero_mem' := _, add_mem' := _, smul_mem' := _}
Equations
- measure_theory.Lp.module = {to_distrib_mul_action := module.to_distrib_mul_action (measure_theory.Lp.Lp_submodule E p μ 𝕜).module, add_smul := _, zero_smul := _}
Equations
- measure_theory.Lp.normed_space = {to_module := measure_theory.Lp.module _inst_11, norm_smul_le := _}
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.
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
- hg.comp_Lp g0 f = ⟨measure_theory.ae_eq_fun.comp g _ ↑f, _⟩
Composing f : Lp
with L : E →L[ℝ] F
.
Composing f : Lp E p μ
with L : E →L[ℝ] F
, seen as a ℝ
-linear map on Lp E p μ
.
Equations
- continuous_linear_map.comp_Lpₗ p μ L = {to_fun := λ (f : ↥(measure_theory.Lp E p μ)), L.comp_Lp f, map_add' := _, map_smul' := _}
Composing f : Lp E p μ
with L : E →L[ℝ] F
, seen as a continuous ℝ
-linear map on
Lp E p μ
.
Equations
- continuous_linear_map.comp_LpL p μ L = (continuous_linear_map.comp_Lpₗ p μ L).mk_continuous ∥L∥ _
Positive part of a function in L^p
.
Equations
- measure_theory.Lp.pos_part f = measure_theory.Lp.lipschitz_with_pos_part.comp_Lp measure_theory.Lp.pos_part._proof_1 f
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
.
Lp
is complete iff Cauchy sequences of ℒp
have limits in ℒp
#
Prove that controlled Cauchy sequences of ℒp
have limits in ℒp
#
Lp
is complete for 1 ≤ p
#
A bounded continuous function is in Lp
.
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 normed group homomorphism of considering a bounded continuous function on a finite-measure
space as an element of Lp
.
Equations
The bounded linear map of considering a bounded continuous function on a finite-measure space
as an element of Lp
.
Equations
- bounded_continuous_function.to_Lp E p μ 𝕜 = (linear_map.cod_restrict (measure_theory.Lp.Lp_submodule E p μ 𝕜) ((continuous_map.to_ae_eq_fun_linear_map μ).comp (bounded_continuous_function.forget_boundedness_linear_map α E)) bounded_continuous_function.mem_Lp).mk_continuous (↑(measure_theory.measure_univ_nnreal μ) ^ (p.to_real)⁻¹) bounded_continuous_function.Lp_norm_le
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
Bound for the operator norm of continuous_map.to_Lp
.