ℓ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 functionfsatisfies, as appropriate,ffinitely supported ifp = 0,summable (λ a, ∥f a∥^p)if0 < p < ∞, andbdd_above (norm '' (set.range f))ifp = ∞lp E p: elements ofΠ i : α, E isuch thatmem_ℓp f p. Defined as anadd_subgroupof a type synonympre_lpforΠ i : α, E i, and equipped with anormed_groupstructure; also equipped withnormed_space 𝕜andcomplete_spaceinstances under appropriate conditions
Main results #
mem_ℓp.of_exponent_ge: Forq ≤ p, a function which ismem_ℓpforqis alsomem_ℓpforplp.mem_ℓp_of_tendsto,lp.norm_le_of_tendsto: A pointwise limit of functions inlp, all withlpnorm≤ C, is itself inlpand haslpnorm≤ 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α
def
mem_ℓp
{α : Type u_1}
{E : α → Type u_2}
[Π (i : α), normed_group (E i)]
(f : Π (i : α), E i)
(p : ℝ≥0∞) :
Prop
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∥ ^ pbe summable, if0 < p < ∞.
theorem
mem_ℓp_zero_iff
{α : Type u_1}
{E : α → Type u_2}
[Π (i : α), normed_group (E i)]
{f : Π (i : α), E i} :
theorem
mem_ℓp_zero
{α : Type u_1}
{E : α → Type u_2}
[Π (i : α), normed_group (E i)]
{f : Π (i : α), E i}
(hf : {i : α | f i ≠ 0}.finite) :
mem_ℓp f 0
theorem
mem_ℓp_infty_iff
{α : Type u_1}
{E : α → Type u_2}
[Π (i : α), normed_group (E i)]
{f : Π (i : α), E i} :
theorem
mem_ℓp_infty
{α : Type u_1}
{E : α → Type u_2}
[Π (i : α), normed_group (E i)]
{f : Π (i : α), E i}
(hf : bdd_above (set.range (λ (i : α), ∥f i∥))) :
theorem
mem_ℓp_gen
{α : Type u_1}
{E : α → Type u_2}
{p : ℝ≥0∞}
[Π (i : α), normed_group (E i)]
{f : Π (i : α), E i}
(hf : summable (λ (i : α), ∥f i∥ ^ p.to_real)) :
mem_ℓp f p
theorem
zero_mem_ℓp
{α : Type u_1}
{E : α → Type u_2}
{p : ℝ≥0∞}
[Π (i : α), normed_group (E i)] :
mem_ℓp 0 p
theorem
zero_mem_ℓp'
{α : Type u_1}
{E : α → Type u_2}
{p : ℝ≥0∞}
[Π (i : α), normed_group (E i)] :
mem_ℓp (λ (i : α), 0) p
theorem
mem_ℓp.finite_dsupport
{α : Type u_1}
{E : α → Type u_2}
[Π (i : α), normed_group (E i)]
{f : Π (i : α), E i}
(hf : mem_ℓp f 0) :
theorem
mem_ℓp.bdd_above
{α : Type u_1}
{E : α → Type u_2}
[Π (i : α), normed_group (E i)]
{f : Π (i : α), E i}
(hf : mem_ℓp f ⊤) :
theorem
mem_ℓp.neg
{α : Type u_1}
{E : α → Type u_2}
{p : ℝ≥0∞}
[Π (i : α), normed_group (E i)]
{f : Π (i : α), E i}
(hf : mem_ℓp f p) :
@[simp]
theorem
mem_ℓp.neg_iff
{α : Type u_1}
{E : α → Type u_2}
{p : ℝ≥0∞}
[Π (i : α), normed_group (E i)]
{f : Π (i : α), E i} :
theorem
mem_ℓp.of_exponent_ge
{α : Type u_1}
{E : α → Type u_2}
[Π (i : α), normed_group (E i)]
{p q : ℝ≥0∞}
{f : Π (i : α), E i}
(hfq : mem_ℓp f q)
(hpq : q ≤ p) :
mem_ℓp f p
theorem
mem_ℓp.add
{α : Type u_1}
{E : α → Type u_2}
{p : ℝ≥0∞}
[Π (i : α), normed_group (E i)]
{f g : Π (i : α), E i}
(hf : mem_ℓp f p)
(hg : mem_ℓp g p) :
theorem
mem_ℓp.sub
{α : Type u_1}
{E : α → Type u_2}
{p : ℝ≥0∞}
[Π (i : α), normed_group (E i)]
{f g : Π (i : α), E i}
(hf : mem_ℓp f p)
(hg : mem_ℓp g p) :
theorem
mem_ℓp.finset_sum
{α : Type u_1}
{E : α → Type u_2}
{p : ℝ≥0∞}
[Π (i : α), normed_group (E i)]
{ι : Type u_3}
(s : finset ι)
{f : ι → Π (i : α), E i}
(hf : ∀ (i : ι), i ∈ s → mem_ℓp (f i) p) :
mem_ℓp (λ (a : α), ∑ (i : ι) in s, f i a) p
theorem
mem_ℓp.const_smul
{α : Type u_1}
{E : α → Type u_2}
{p : ℝ≥0∞}
[Π (i : α), normed_group (E i)]
{𝕜 : Type u_3}
[normed_field 𝕜]
[Π (i : α), normed_space 𝕜 (E i)]
{f : Π (i : α), E i}
(hf : mem_ℓp f p)
(c : 𝕜) :
theorem
mem_ℓp.const_mul
{α : Type u_1}
{p : ℝ≥0∞}
{𝕜 : Type u_3}
[normed_field 𝕜]
{f : α → 𝕜}
(hf : mem_ℓp f p)
(c : 𝕜) :
@[protected, instance]
def
pre_lp.add_comm_group
{α : Type u_1}
(E : α → Type u_2)
[Π (i : α), normed_group (E i)] :
add_comm_group (pre_lp E)
@[nolint]
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).
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def
lp.has_coe_to_fun
{α : Type u_1}
{E : α → Type u_2}
{p : ℝ≥0∞}
[Π (i : α), normed_group (E i)] :
has_coe_to_fun ↥(lp E p) (λ (_x : ↥(lp E p)), Π (i : α), E i)
theorem
lp.eq_zero'
{α : Type u_1}
{E : α → Type u_2}
{p : ℝ≥0∞}
[Π (i : α), normed_group (E i)]
[is_empty α]
(f : ↥(lp E p)) :
f = 0
@[protected]
theorem
lp.monotone
{α : Type u_1}
{E : α → Type u_2}
[Π (i : α), normed_group (E i)]
{p q : ℝ≥0∞}
(hpq : q ≤ p) :
@[simp]
theorem
lp.coe_fn_zero
{α : Type u_1}
(E : α → Type u_2)
(p : ℝ≥0∞)
[Π (i : α), normed_group (E i)] :
@[simp]
theorem
lp.coe_fn_sum
{α : Type u_1}
{E : α → Type u_2}
{p : ℝ≥0∞}
[Π (i : α), normed_group (E i)]
{ι : Type u_3}
(f : ι → ↥(lp E p))
(s : finset ι) :
@[protected, instance]
noncomputable
def
lp.has_norm
{α : Type u_1}
{E : α → Type u_2}
{p : ℝ≥0∞}
[Π (i : α), normed_group (E i)] :
theorem
lp.norm_nonneg'
{α : Type u_1}
{E : α → Type u_2}
{p : ℝ≥0∞}
[Π (i : α), normed_group (E i)]
(f : ↥(lp E p)) :
@[simp]
theorem
lp.eq_zero_iff_coe_fn_eq_zero
{α : Type u_1}
{E : α → Type u_2}
{p : ℝ≥0∞}
[Π (i : α), normed_group (E i)]
{f : ↥(lp E p)} :
@[protected, instance]
noncomputable
def
lp.normed_group
{α : Type u_1}
{E : α → Type u_2}
{p : ℝ≥0∞}
[Π (i : α), normed_group (E i)]
[hp : fact (1 ≤ p)] :
normed_group ↥(lp E p)
Equations
- lp.normed_group = normed_group.of_core ↥(lp E p) lp.normed_group._proof_1
@[protected]
theorem
lp.tsum_mul_le_mul_norm
{α : Type u_1}
{E : α → Type u_2}
[Π (i : α), normed_group (E i)]
{p q : ℝ≥0∞}
(hpq : p.to_real.is_conjugate_exponent q.to_real)
(f : ↥(lp E p))
(g : ↥(lp E q)) :
Hölder inequality
@[protected, instance]
def
lp.pre_lp.module
{α : Type u_1}
{E : α → Type u_2}
[Π (i : α), normed_group (E i)]
{𝕜 : Type u_3}
[normed_field 𝕜]
[Π (i : α), normed_space 𝕜 (E i)] :
Equations
- lp.pre_lp.module = pi.module α E 𝕜
theorem
lp.mem_lp_const_smul
{α : Type u_1}
{E : α → Type u_2}
{p : ℝ≥0∞}
[Π (i : α), normed_group (E i)]
{𝕜 : Type u_3}
[normed_field 𝕜]
[Π (i : α), normed_space 𝕜 (E i)]
(c : 𝕜)
(f : ↥(lp E p)) :
def
lp.lp_submodule
{α : Type u_1}
(E : α → Type u_2)
(p : ℝ≥0∞)
[Π (i : α), normed_group (E i)]
(𝕜 : Type u_3)
[normed_field 𝕜]
[Π (i : α), normed_space 𝕜 (E i)] :
The 𝕜-submodule of elements of Π i : α, E i whose lp norm is finite. This is lp E p,
with extra structure.
theorem
lp.coe_lp_submodule
{α : Type u_1}
{E : α → Type u_2}
{p : ℝ≥0∞}
[Π (i : α), normed_group (E i)]
{𝕜 : Type u_3}
[normed_field 𝕜]
[Π (i : α), normed_space 𝕜 (E i)] :
(lp.lp_submodule E p 𝕜).to_add_subgroup = lp E p
@[protected, instance]
def
lp.module
{α : Type u_1}
{E : α → Type u_2}
{p : ℝ≥0∞}
[Π (i : α), normed_group (E i)]
{𝕜 : Type u_3}
[normed_field 𝕜]
[Π (i : α), normed_space 𝕜 (E i)] :
Equations
- lp.module = {to_distrib_mul_action := module.to_distrib_mul_action (lp.lp_submodule E p 𝕜).module, add_smul := _, zero_smul := _}
@[simp]
theorem
lp.coe_fn_smul
{α : Type u_1}
{E : α → Type u_2}
{p : ℝ≥0∞}
[Π (i : α), normed_group (E i)]
{𝕜 : Type u_3}
[normed_field 𝕜]
[Π (i : α), normed_space 𝕜 (E i)]
(c : 𝕜)
(f : ↥(lp E p)) :
theorem
lp.norm_const_smul
{α : Type u_1}
{E : α → Type u_2}
{p : ℝ≥0∞}
[Π (i : α), normed_group (E i)]
{𝕜 : Type u_3}
[normed_field 𝕜]
[Π (i : α), normed_space 𝕜 (E i)]
(hp : p ≠ 0)
{c : 𝕜}
(f : ↥(lp E p)) :
@[protected, instance]
noncomputable
def
lp.normed_space
{α : Type u_1}
{E : α → Type u_2}
{p : ℝ≥0∞}
[Π (i : α), normed_group (E i)]
{𝕜 : Type u_3}
[normed_field 𝕜]
[Π (i : α), normed_space 𝕜 (E i)]
[fact (1 ≤ p)] :
normed_space 𝕜 ↥(lp E p)
Equations
- lp.normed_space = {to_module := lp.module (λ (i : α), _inst_3 i), norm_smul_le := _}
@[protected, instance]
def
lp.is_scalar_tower
{α : Type u_1}
{E : α → Type u_2}
{p : ℝ≥0∞}
[Π (i : α), normed_group (E i)]
{𝕜 : Type u_3}
[normed_field 𝕜]
[Π (i : α), normed_space 𝕜 (E i)]
{𝕜' : Type u_4}
[normed_field 𝕜']
[Π (i : α), normed_space 𝕜' (E i)]
[has_scalar 𝕜' 𝕜]
[∀ (i : α), is_scalar_tower 𝕜' 𝕜 (E i)] :
is_scalar_tower 𝕜' 𝕜 ↥(lp E p)
@[protected]
def
lp.single
{α : Type u_1}
{E : α → Type u_2}
[Π (i : α), normed_group (E i)]
[decidable_eq α]
(p : ℝ≥0∞)
(i : α)
(a : E i) :
The element of lp E p which is a : E i at the index i, and zero elsewhere.
@[protected]
theorem
lp.single_apply
{α : Type u_1}
{E : α → Type u_2}
[Π (i : α), normed_group (E i)]
[decidable_eq α]
(p : ℝ≥0∞)
(i : α)
(a : E i)
(j : α) :
@[protected]
theorem
lp.single_apply_self
{α : Type u_1}
{E : α → Type u_2}
[Π (i : α), normed_group (E i)]
[decidable_eq α]
(p : ℝ≥0∞)
(i : α)
(a : E i) :
@[protected]
theorem
lp.single_apply_ne
{α : Type u_1}
{E : α → Type u_2}
[Π (i : α), normed_group (E i)]
[decidable_eq α]
(p : ℝ≥0∞)
(i : α)
(a : E i)
{j : α}
(hij : j ≠ i) :
@[protected, simp]
theorem
lp.single_neg
{α : Type u_1}
{E : α → Type u_2}
[Π (i : α), normed_group (E i)]
[decidable_eq α]
(p : ℝ≥0∞)
(i : α)
(a : E i) :
@[protected, simp]
theorem
lp.single_smul
{α : Type u_1}
{E : α → Type u_2}
[Π (i : α), normed_group (E i)]
{𝕜 : Type u_3}
[normed_field 𝕜]
[Π (i : α), normed_space 𝕜 (E i)]
[decidable_eq α]
(p : ℝ≥0∞)
(i : α)
(a : E i)
(c : 𝕜) :
@[protected]
theorem
lp.norm_single
{α : Type u_1}
{E : α → Type u_2}
{p : ℝ≥0∞}
[Π (i : α), normed_group (E i)]
[decidable_eq α]
(hp : 0 < p.to_real)
(f : Π (i : α), E i)
(i : α) :
@[protected]
@[protected]
@[protected]
theorem
lp.has_sum_single
{α : Type u_1}
{E : α → Type u_2}
{p : ℝ≥0∞}
[Π (i : α), normed_group (E i)]
[decidable_eq α]
[fact (1 ≤ p)]
(hp : p ≠ ⊤)
(f : ↥(lp E p)) :
The canonical finitely-supported approximations to an element f of lp converge to it, in the
lp topology.
theorem
lp.uniform_continuous_coe
{α : Type u_1}
{E : α → Type u_2}
{p : ℝ≥0∞}
[Π (i : α), normed_group (E i)]
[fact (1 ≤ p)] :
The coercion from lp E p to Π i, E i is uniformly continuous.
theorem
lp.norm_apply_le_of_tendsto
{α : Type u_1}
{E : α → Type u_2}
[Π (i : α), normed_group (E i)]
{ι : Type u_3}
{l : filter ι}
[l.ne_bot]
{C : ℝ}
{F : ι → ↥(lp E ⊤)}
(hCF : ∀ᶠ (k : ι) in l, ∥F k∥ ≤ C)
{f : Π (a : α), E a}
(hf : filter.tendsto (id (λ (i : ι), ⇑(F i))) l (𝓝 f))
(a : α) :
theorem
lp.sum_rpow_le_of_tendsto
{α : Type u_1}
{E : α → Type u_2}
{p : ℝ≥0∞}
[Π (i : α), normed_group (E i)]
{ι : Type u_3}
{l : filter ι}
[l.ne_bot]
[fact (1 ≤ p)]
(hp : p ≠ ⊤)
{C : ℝ}
{F : ι → ↥(lp E p)}
(hCF : ∀ᶠ (k : ι) in l, ∥F k∥ ≤ C)
{f : Π (a : α), E a}
(hf : filter.tendsto (id (λ (i : ι), ⇑(F i))) l (𝓝 f))
(s : finset α) :
theorem
lp.norm_le_of_tendsto
{α : Type u_1}
{E : α → Type u_2}
{p : ℝ≥0∞}
[Π (i : α), normed_group (E i)]
{ι : Type u_3}
{l : filter ι}
[l.ne_bot]
[fact (1 ≤ p)]
{C : ℝ}
{F : ι → ↥(lp E p)}
(hCF : ∀ᶠ (k : ι) in l, ∥F k∥ ≤ C)
{f : ↥(lp E p)}
(hf : filter.tendsto (id (λ (i : ι), ⇑(F i))) l (𝓝 ⇑f)) :
"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.
theorem
lp.mem_ℓp_of_tendsto
{α : Type u_1}
{E : α → Type u_2}
{p : ℝ≥0∞}
[Π (i : α), normed_group (E i)]
{ι : Type u_3}
{l : filter ι}
[l.ne_bot]
[fact (1 ≤ p)]
{F : ι → ↥(lp E p)}
(hF : metric.bounded (set.range F))
{f : Π (a : α), E a}
(hf : filter.tendsto (id (λ (i : ι), ⇑(F i))) l (𝓝 f)) :
mem_ℓp f p
If f is the pointwise limit of a bounded sequence in lp E p, then f is in lp E p.
theorem
lp.tendsto_lp_of_tendsto_pi
{α : Type u_1}
{E : α → Type u_2}
{p : ℝ≥0∞}
[Π (i : α), normed_group (E i)]
[fact (1 ≤ p)]
{F : ℕ → ↥(lp E p)}
(hF : cauchy_seq F)
{f : ↥(lp E p)}
(hf : filter.tendsto (id (λ (i : ℕ), ⇑(F i))) filter.at_top (𝓝 ⇑f)) :
filter.tendsto F filter.at_top (𝓝 f)
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.
@[protected, instance]
def
lp.complete_space
{α : Type u_1}
{E : α → Type u_2}
{p : ℝ≥0∞}
[Π (i : α), normed_group (E i)]
[fact (1 ≤ p)]
[∀ (a : α), complete_space (E a)] :
complete_space ↥(lp E p)