ℓ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 (fun a ↦ ‖f a‖^p)
if
0 < p < ∞
, and BddAbove (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 (fun a ↦ ‖f a‖^p)
if0 < p < ∞
, andBddAbove (norm '' (Set.range f))
ifp = ∞
.lp E p
: elements of∀ i : α, E i
such thatMemℓp f p
. Defined as anAddSubgroup
of a type synonymPreLp
for∀ i : α, E i
, and equipped with aNormedAddCommGroup
structure. Under appropriate conditions, this is also equipped with the instanceslp.normedSpace
,lp.completeSpace
. Forp=∞
, there is alsolp.inftyNormedRing
,lp.inftyNormedAlgebra
,lp.inftyStarRing
andlp.inftyCStarRing
.
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 AddSubgroup
, 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
)
The property that f : ∀ i : α, E i
- is finitely supported, if
p = 0
, or - admits an upper bound for
Set.range (fun i ↦ ‖f i‖)
, ifp = ∞
, or - has the series
∑' i, ‖f i‖ ^ p
be summable, if0 < p < ∞
.
Equations
Instances For
We define PreLp 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
Equations
- PreLp.unique = Pi.uniqueOfIsEmpty E
lp space
Equations
- One or more equations did not get rendered due to their size.
Instances For
lp space
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- lp.instCoeOutSubtypePreLpMemAddSubgroupForall = { coe := Subtype.val }
Equations
- One or more equations did not get rendered due to their size.
Equations
- lp.normedAddCommGroup = { toFun := norm, map_zero' := ⋯, add_le' := ⋯, neg' := ⋯, eq_zero_of_map_eq_zero' := ⋯ }.toNormedAddCommGroup
Hölder inequality
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
The 𝕜
-submodule of elements of ∀ i : α, E i
whose lp
norm is finite. This is lp E p
,
with extra structure.
Equations
- lpSubmodule E p 𝕜 = { toAddSubmonoid := (lp E p).toAddSubmonoid, smul_mem' := ⋯ }
Instances For
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- lp.instNormedSpace = NormedSpace.mk ⋯
Equations
- lp.instInvolutiveStar = InvolutiveStar.mk ⋯
Equations
- lp.instStarAddMonoid = StarAddMonoid.mk ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- lp.nonUnitalRing = Function.Injective.nonUnitalRing CoeFun.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- lp.nonUnitalNormedRing = NonUnitalNormedRing.mk ⋯ ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- lp.inftyStarRing = StarRing.mk ⋯
Equations
- ⋯ = ⋯
Equations
- PreLp.ring = Pi.ring
The 𝕜
-subring of elements of ∀ i : α, B i
whose lp
norm is finite. This is lp E ∞
,
with extra structure.
Equations
- lpInftySubring B = { carrier := {f : PreLp B | Memℓp f ⊤}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
Instances For
Equations
- lp.inftyRing = (lpInftySubring B).toRing
Alias of natCast_memℓp_infty
.
Alias of intCast_memℓp_infty
.
Alias of lp.infty_coeFn_natCast
.
Alias of lp.infty_coeFn_intCast
.
Equations
- ⋯ = ⋯
Equations
- lp.inftyNormedRing = NormedRing.mk ⋯ ⋯
Equations
- lp.inftyCommRing = CommRing.mk ⋯
Equations
- lp.inftyNormedCommRing = NormedCommRing.mk ⋯
A variant of Pi.algebra
that lean can't find otherwise.
Equations
- Pi.algebraOfNormedAlgebra = Pi.algebra I B
Equations
- PreLp.algebra = Pi.algebraOfNormedAlgebra
The 𝕜
-subalgebra of elements of ∀ i : α, B i
whose lp
norm is finite. This is lp E ∞
,
with extra structure.
Equations
- lpInftySubalgebra 𝕜 B = { carrier := {f : PreLp B | Memℓp f ⊤}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := ⋯ }
Instances For
Equations
- lp.inftyNormedAlgebra = NormedAlgebra.mk ⋯
The element of lp E p
which is a : E i
at the index i
, and zero elsewhere.
Instances For
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 an element f
of
lp E p
, then it converges to f
in the lp E p
topology.
Equations
- ⋯ = ⋯