ℓp space #
This file describes properties of elements f
of a pi-type Π i, E i
with finite "norm",
defined for p:ℝ≥0∞
as the size of the support of f
if p=0
, (∑' a, ∥f a∥^p) ^ (1/p)
for
0 < p < ∞
and ⨆ a, ∥f a∥
for p=∞
.
The Prop-valued mem_ℓp f p
states that a function f : Π i, E i
has finite norm according
to the above definition; that is, f
has finite support if p = 0
, summable (λ a, ∥f a∥^p)
if
0 < p < ∞
, and bdd_above (norm '' (set.range f))
if p = ∞
.
The space lp E p
is the subtype of elements of Π i : α, E i
which satisfy mem_ℓp f p
. For
1 ≤ p
, the "norm" is genuinely a norm and lp
is a complete metric space.
Main definitions #
mem_ℓp f p
: property that the functionf
satisfies, as appropriate,f
finitely supported ifp = 0
,summable (λ a, ∥f a∥^p)
if0 < p < ∞
, andbdd_above (norm '' (set.range f))
ifp = ∞
.lp E p
: elements ofΠ i : α, E i
such thatmem_ℓp f p
. Defined as anadd_subgroup
of a type synonympre_lp
forΠ i : α, E i
, and equipped with anormed_add_comm_group
structure. Under appropriate conditions, this is also equipped with the instanceslp.normed_space
,lp.complete_space
. Forp=∞
, there is alsolp.infty_normed_ring
,lp.infty_normed_algebra
,lp.infty_star_ring
andlp.infty_cstar_ring
.
Main results #
mem_ℓp.of_exponent_ge
: Forq ≤ p
, a function which ismem_ℓp
forq
is alsomem_ℓp
forp
lp.mem_ℓp_of_tendsto
,lp.norm_le_of_tendsto
: A pointwise limit of functions inlp
, all withlp
norm≤ C
, is itself inlp
and haslp
norm≤ C
.lp.tsum_mul_le_mul_norm
: basic form of Hölder's inequality
Implementation #
Since lp
is defined as an add_subgroup
, dot notation does not work. Use lp.norm_neg f
to
say that ∥-f∥ = ∥f∥
, instead of the non-working f.norm_neg
.
TODO #
- More versions of Hölder's inequality (for example: the case
p = 1
,q = ∞
; a version for normed rings which has∥∑' i, f i * g i∥
rather than∑' i, ∥f i∥ * g i∥
on the RHS; a version for three exponents satisfying1 / r = 1 / p + 1 / q
) - Equivalence with
pi_Lp
, forα
finite - Equivalence with
measure_theory.Lp
, forf : α → E
(i.e., functions rather than pi-types) and the counting measure onα
- Equivalence with
bounded_continuous_function
, forf : α → E
(i.e., functions rather than pi-types) andp = ∞
, and the discrete topology onα
The property that f : Π i : α, E i
- is finitely supported, if
p = 0
, or - admits an upper bound for
set.range (λ i, ∥f i∥)
, ifp = ∞
, or - has the series
∑' i, ∥f i∥ ^ p
be summable, if0 < p < ∞
.
We define pre_lp E
to be a type synonym for Π i, E i
which, importantly, does not inherit
the pi
topology on Π i, E i
(otherwise this topology would descend to lp E p
and conflict
with the normed group topology we will later equip it with.)
We choose to deal with this issue by making a type synonym for Π i, E i
rather than for the lp
subgroup itself, because this allows all the spaces lp E p
(for varying p
) to be subgroups of
the same ambient group, which permits lemma statements like lp.monotone
(below).
Instances for pre_lp
Equations
lp space
Equations
Instances for ↥lp
- lp.pi.has_coe
- lp.has_coe_to_fun
- lp.has_norm
- lp.normed_add_comm_group
- lp.module
- lp.normed_space
- lp.is_scalar_tower
- lp.has_star
- lp.has_involutive_star
- lp.star_add_monoid
- lp.normed_star_group
- lp.star_module
- lp.has_mul
- lp.non_unital_ring
- lp.non_unital_normed_ring
- lp.infty_is_scalar_tower
- lp.infty_smul_comm_class
- lp.infty_star_ring
- lp.infty_cstar_ring
- lp.infty_ring
- lp.norm_one_class
- lp.infty_normed_ring
- lp.infty_comm_ring
- lp.infty_normed_comm_ring
- lp.infty_normed_algebra
- lp.complete_space
- lp.inner_product_space
Equations
Equations
- lp.normed_add_comm_group = normed_add_comm_group.of_core ↥(lp E p) lp.normed_add_comm_group._proof_1
Hölder inequality
Equations
- lp.pre_lp.module = pi.module α E 𝕜
The 𝕜
-submodule of elements of Π i : α, E i
whose lp
norm is finite. This is lp E p
,
with extra structure.
Equations
- lp.module = {to_distrib_mul_action := module.to_distrib_mul_action (lp_submodule E p 𝕜).module, add_smul := _, zero_smul := _}
Equations
- lp.normed_space = {to_module := lp.module (λ (i : α), _inst_3 i), norm_smul_le := _}
Equations
- lp.has_star = {star := λ (f : ↥(lp E p)), ⟨has_star.star ⇑f, _⟩}
Equations
- lp.has_involutive_star = {to_has_star := lp.has_star lp.has_involutive_star._proof_1, star_involutive := _}
Equations
- lp.star_add_monoid = {to_has_involutive_star := lp.has_involutive_star lp.star_add_monoid._proof_1, star_add := _}
Equations
- lp.non_unital_ring = function.injective.non_unital_ring has_coe_to_fun.coe lp.non_unital_ring._proof_1 lp.non_unital_ring._proof_2 lp.non_unital_ring._proof_3 lp.non_unital_ring._proof_4 lp.non_unital_ring._proof_5 lp.non_unital_ring._proof_6 lp.non_unital_ring._proof_7 lp.non_unital_ring._proof_8
Equations
- lp.non_unital_normed_ring = {to_has_norm := normed_add_comm_group.to_has_norm lp.normed_add_comm_group, to_non_unital_ring := lp.non_unital_ring (λ (i : I), _inst_2 i), to_metric_space := normed_add_comm_group.to_metric_space lp.normed_add_comm_group, dist_eq := _, norm_mul := _}
Equations
- lp.infty_star_ring = {to_star_semigroup := {to_has_involutive_star := star_add_monoid.to_has_involutive_star (show star_add_monoid ↥(lp B ⊤), from let _inst : Π (i : I), star_add_monoid (B i) := λ (i : I), infer_instance in lp.star_add_monoid), star_mul := _}, star_add := _}
Equations
The 𝕜
-subring of elements of Π i : α, B i
whose lp
norm is finite. This is lp E ∞
,
with extra structure.
Equations
Equations
- lp.infty_normed_ring = {to_has_norm := non_unital_normed_ring.to_has_norm lp.non_unital_normed_ring, to_ring := {add := ring.add lp.infty_ring, add_assoc := _, zero := ring.zero lp.infty_ring, zero_add := _, add_zero := _, nsmul := ring.nsmul lp.infty_ring, nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg lp.infty_ring, sub := ring.sub lp.infty_ring, sub_eq_add_neg := _, zsmul := ring.zsmul lp.infty_ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := ring.int_cast lp.infty_ring, nat_cast := ring.nat_cast lp.infty_ring, one := ring.one lp.infty_ring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := ring.mul lp.infty_ring, mul_assoc := _, one_mul := _, mul_one := _, npow := ring.npow lp.infty_ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _}, to_metric_space := non_unital_normed_ring.to_metric_space lp.non_unital_normed_ring, dist_eq := _, norm_mul := _}
Equations
- lp.infty_comm_ring = {add := ring.add lp.infty_ring, add_assoc := _, zero := ring.zero lp.infty_ring, zero_add := _, add_zero := _, nsmul := ring.nsmul lp.infty_ring, nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg lp.infty_ring, sub := ring.sub lp.infty_ring, sub_eq_add_neg := _, zsmul := ring.zsmul lp.infty_ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := ring.int_cast lp.infty_ring, nat_cast := ring.nat_cast lp.infty_ring, one := ring.one lp.infty_ring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := ring.mul lp.infty_ring, mul_assoc := _, one_mul := _, mul_one := _, npow := ring.npow lp.infty_ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _}
Equations
A variant of pi.algebra
that lean can't find otherwise.
Equations
Equations
The 𝕜
-subalgebra of elements of Π i : α, B i
whose lp
norm is finite. This is lp E ∞
,
with extra structure.
Equations
- lp.infty_normed_algebra = {to_algebra := {to_has_smul := algebra.to_has_smul (lp_infty_subalgebra 𝕜 B).algebra, to_ring_hom := algebra.to_ring_hom (lp_infty_subalgebra 𝕜 B).algebra, commutes' := _, smul_def' := _}, norm_smul_le := _}
The element of lp E p
which is a : E i
at the index i
, and zero elsewhere.
The canonical finitely-supported approximations to an element f
of lp
converge to it, in the
lp
topology.
The coercion from lp E p
to Π i, E i
is uniformly continuous.
"Semicontinuity of the lp
norm": If all sufficiently large elements of a sequence in lp E p
have lp
norm ≤ C
, then the pointwise limit, if it exists, also has lp
norm ≤ C
.
If f
is the pointwise limit of a bounded sequence in lp E p
, then f
is in lp E p
.
If a sequence is Cauchy in the lp E p
topology and pointwise convergent to a element f
of
lp E p
, then it converges to f
in the lp E p
topology.