ℒp space and Lp space #
This file describes properties of almost everywhere strongly measurable functions with finite
seminorm, denoted by snorm f p μ
and defined for p:ℝ≥0∞
asmm_group (Lp E p μ) := 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 strongly measurable and has finitep
-seminorm for the 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]
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.
ℒ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‖
.
ℒ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 strongly measurable and (∫ ‖f a‖^p ∂μ)^(1/p)
is finite
if p < ∞
, or ess_sup f < ∞
if p = ∞
.
Equations
- measure_theory.mem_ℒp f p μ = (measure_theory.ae_strongly_measurable f μ ∧ measure_theory.snorm f p μ < ⊤)
Alias of measure_theory.mem_ℒp.of_le
.
A version of Markov's inequality using Lp-norms.
Hölder's inequality, as an inequality on the ℒp
seminorm of a scalar product φ • f
.
Lp space
Equations
Instances for ↥measure_theory.Lp
- measure_theory.Lp.has_coe_to_fun
- measure_theory.Lp.has_norm
- measure_theory.Lp.has_dist
- measure_theory.Lp.has_edist
- measure_theory.Lp.normed_add_comm_group
- measure_theory.Lp.module
- measure_theory.Lp.normed_space
- measure_theory.Lp.complete_space
- measure_theory.Lp.has_le.le.covariant_class
- measure_theory.Lp.ordered_add_comm_group
- measure_theory.Lp.lattice
- measure_theory.Lp.normed_lattice_add_comm_group
- measure_theory.L2.measure_theory.Lp.has_inner
- measure_theory.L2.inner_product_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 = {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 μ)), measure_theory.snorm (⇑f - ⇑g) p μ}
Equations
- measure_theory.Lp.normed_add_comm_group = {to_has_norm := normed_add_comm_group.to_has_norm {to_fun := has_norm.norm measure_theory.Lp.has_norm, map_zero' := _, add_le' := _, neg' := _, eq_zero_of_map_eq_zero' := _}.to_normed_add_comm_group, to_add_comm_group := normed_add_comm_group.to_add_comm_group {to_fun := has_norm.norm measure_theory.Lp.has_norm, map_zero' := _, add_le' := _, neg' := _, eq_zero_of_map_eq_zero' := _}.to_normed_add_comm_group, to_metric_space := {to_pseudo_metric_space := {to_has_dist := pseudo_metric_space.to_has_dist metric_space.to_pseudo_metric_space, dist_self := _, dist_comm := _, dist_triangle := _, edist := has_edist.edist measure_theory.Lp.has_edist, edist_dist := _, to_uniform_space := pseudo_metric_space.to_uniform_space metric_space.to_pseudo_metric_space, uniformity_dist := _, to_bornology := pseudo_metric_space.to_bornology metric_space.to_pseudo_metric_space, cobounded_sets := _}, eq_of_dist_eq_zero := _}, dist_eq := _}
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, add_mem' := _, zero_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_5, norm_smul_le := _}
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)
.
Indicator of a set as an element of Lp
.
Equations
- measure_theory.indicator_const_Lp p hs hμs c = measure_theory.mem_ℒp.to_Lp (s.indicator (λ (_x : α), c)) _
The indicator of a disjoint union of two sets is the sum of the indicators of the sets.
Composition on L^p
#
We show that Lipschitz functions vanishing at zero act by composition on L^p
, and specialize
this to the composition with continuous linear maps, and to the definition of the positive
part of an L^p
function.
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, _⟩