mathlib documentation

analysis.normed_space.lp_space

ℓ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 #

Main results #

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 #

mem_ℓp predicate #

def mem_ℓp {α : Type u_1} {E : α → Type u_2} [Π (i : α), normed_group (E i)] (f : Π (i : α), E i) (p : ennreal) :
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∥), if p = ∞, or
  • has the series ∑' i, ∥f i∥ ^ p be summable, if 0 < p < ∞.
Equations
theorem mem_ℓp_zero_iff {α : Type u_1} {E : α → Type u_2} [Π (i : α), normed_group (E i)] {f : Π (i : α), E i} :
mem_ℓp f 0 {i : α | f i 0}.finite
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) :
theorem mem_ℓp_infty_iff {α : Type u_1} {E : α → Type u_2} [Π (i : α), normed_group (E i)] {f : Π (i : α), E i} :
mem_ℓp f bdd_above (set.range (λ (i : α), f 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_iff {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), normed_group (E i)] (hp : 0 < p.to_real) {f : Π (i : α), E i} :
mem_ℓp f p summable (λ (i : α), f i ^ p.to_real)
theorem mem_ℓp_gen {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), normed_group (E i)] {f : Π (i : α), E i} (hf : summable (λ (i : α), f i ^ p.to_real)) :
theorem mem_ℓp_gen' {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), normed_group (E i)] {C : } {f : Π (i : α), E i} (hf : ∀ (s : finset α), s.sum (λ (i : α), f i ^ p.to_real) C) :
theorem zero_mem_ℓp {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), normed_group (E i)] :
theorem zero_mem_ℓp' {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (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) :
{i : α | f i 0}.finite
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 ) :
bdd_above (set.range (λ (i : α), f i))
theorem mem_ℓp.summable {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), normed_group (E i)] (hp : 0 < p.to_real) {f : Π (i : α), E i} (hf : mem_ℓp f p) :
summable (λ (i : α), f i ^ p.to_real)
theorem mem_ℓp.neg {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), normed_group (E i)] {f : Π (i : α), E i} (hf : mem_ℓp f p) :
mem_ℓp (-f) p
@[simp]
theorem mem_ℓp.neg_iff {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (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 : ennreal} {f : Π (i : α), E i} (hfq : mem_ℓp f q) (hpq : q p) :
theorem mem_ℓp.add {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), normed_group (E i)] {f g : Π (i : α), E i} (hf : mem_ℓp f p) (hg : mem_ℓp g p) :
mem_ℓp (f + g) p
theorem mem_ℓp.sub {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), normed_group (E i)] {f g : Π (i : α), E i} (hf : mem_ℓp f p) (hg : mem_ℓp g p) :
mem_ℓp (f - g) p
theorem mem_ℓp.finset_sum {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), normed_group (E i)] {ι : Type u_3} (s : finset ι) {f : ι → Π (i : α), E i} (hf : ∀ (i : ι), i smem_ℓp (f i) p) :
mem_ℓp (λ (a : α), s.sum (λ (i : ι), f i a)) p
theorem mem_ℓp.const_smul {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (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 : 𝕜) :
mem_ℓp (c f) p
theorem mem_ℓp.const_mul {α : Type u_1} {p : ennreal} {𝕜 : Type u_3} [normed_field 𝕜] {f : α → 𝕜} (hf : mem_ℓp f p) (c : 𝕜) :
mem_ℓp (λ (x : α), c * f x) p

lp space #

The space of elements of Π i, E i satisfying the predicate mem_ℓp.

@[protected, instance]
def pre_lp.add_comm_group {α : Type u_1} (E : α → Type u_2) [Π (i : α), normed_group (E i)] :
@[nolint]
def pre_lp {α : Type u_1} (E : α → Type u_2) [Π (i : α), normed_group (E i)] :
Type (max u_1 u_2)

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).

Equations
Instances for pre_lp
@[protected, instance]
def pre_lp.unique {α : Type u_1} {E : α → Type u_2} [Π (i : α), normed_group (E i)] [is_empty α] :
Equations
def lp {α : Type u_1} (E : α → Type u_2) [Π (i : α), normed_group (E i)] (p : ennreal) :

lp space

Equations
Instances for lp
@[protected, instance]
def lp.pi.has_coe {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), normed_group (E i)] :
has_coe (lp E p) (Π (i : α), E i)
Equations
@[protected, instance]
def lp.has_coe_to_fun {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), normed_group (E i)] :
has_coe_to_fun (lp E p) (λ (_x : (lp E p)), Π (i : α), E i)
Equations
@[ext]
theorem lp.ext {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), normed_group (E i)] {f g : (lp E p)} (h : f = g) :
f = g
@[protected]
theorem lp.ext_iff {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), normed_group (E i)] {f g : (lp E p)} :
f = g f = g
theorem lp.eq_zero' {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (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 : ennreal} (hpq : q p) :
lp E q lp E p
@[protected]
theorem lp.mem_ℓp {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), normed_group (E i)] (f : (lp E p)) :
@[simp]
theorem lp.coe_fn_zero {α : Type u_1} (E : α → Type u_2) (p : ennreal) [Π (i : α), normed_group (E i)] :
0 = 0
@[simp]
theorem lp.coe_fn_neg {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), normed_group (E i)] (f : (lp E p)) :
@[simp]
theorem lp.coe_fn_add {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), normed_group (E i)] (f g : (lp E p)) :
(f + g) = f + g
@[simp]
theorem lp.coe_fn_sum {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), normed_group (E i)] {ι : Type u_3} (f : ι → (lp E p)) (s : finset ι) :
(s.sum (λ (i : ι), f i)) = s.sum (λ (i : ι), (f i))
@[simp]
theorem lp.coe_fn_sub {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), normed_group (E i)] (f g : (lp E p)) :
(f - g) = f - g
@[protected, instance]
noncomputable def lp.has_norm {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), normed_group (E i)] :
Equations
theorem lp.norm_eq_card_dsupport {α : Type u_1} {E : α → Type u_2} [Π (i : α), normed_group (E i)] (f : (lp E 0)) :
theorem lp.norm_eq_csupr {α : Type u_1} {E : α → Type u_2} [Π (i : α), normed_group (E i)] (f : (lp E )) :
f = ⨆ (i : α), f i
theorem lp.is_lub_norm {α : Type u_1} {E : α → Type u_2} [Π (i : α), normed_group (E i)] [nonempty α] (f : (lp E )) :
is_lub (set.range (λ (i : α), f i)) f
theorem lp.norm_eq_tsum_rpow {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), normed_group (E i)] (hp : 0 < p.to_real) (f : (lp E p)) :
f = (∑' (i : α), f i ^ p.to_real) ^ (1 / p.to_real)
theorem lp.norm_rpow_eq_tsum {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), normed_group (E i)] (hp : 0 < p.to_real) (f : (lp E p)) :
f ^ p.to_real = ∑' (i : α), f i ^ p.to_real
theorem lp.has_sum_norm {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), normed_group (E i)] (hp : 0 < p.to_real) (f : (lp E p)) :
has_sum (λ (i : α), f i ^ p.to_real) (f ^ p.to_real)
theorem lp.norm_nonneg' {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), normed_group (E i)] (f : (lp E p)) :
@[simp]
theorem lp.norm_zero {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), normed_group (E i)] :
theorem lp.norm_eq_zero_iff {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), normed_group (E i)] ⦃f : (lp E p) :
f = 0 f = 0
theorem lp.eq_zero_iff_coe_fn_eq_zero {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), normed_group (E i)] {f : (lp E p)} :
f = 0 f = 0
@[simp]
theorem lp.norm_neg {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), normed_group (E i)] ⦃f : (lp E p) :
@[protected, instance]
noncomputable def lp.normed_group {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), normed_group (E i)] [hp : fact (1 p)] :
Equations
@[protected]
theorem lp.tsum_mul_le_mul_norm {α : Type u_1} {E : α → Type u_2} [Π (i : α), normed_group (E i)] {p q : ennreal} (hpq : p.to_real.is_conjugate_exponent q.to_real) (f : (lp E p)) (g : (lp E q)) :
summable (λ (i : α), f i * g i) ∑' (i : α), f i * g i f * g

Hölder inequality

@[protected]
theorem lp.summable_mul {α : Type u_1} {E : α → Type u_2} [Π (i : α), normed_group (E i)] {p q : ennreal} (hpq : p.to_real.is_conjugate_exponent q.to_real) (f : (lp E p)) (g : (lp E q)) :
summable (λ (i : α), f i * g i)
@[protected]
theorem lp.tsum_mul_le_mul_norm' {α : Type u_1} {E : α → Type u_2} [Π (i : α), normed_group (E i)] {p q : ennreal} (hpq : p.to_real.is_conjugate_exponent q.to_real) (f : (lp E p)) (g : (lp E q)) :
∑' (i : α), f i * g i f * g
theorem lp.norm_apply_le_norm {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), normed_group (E i)] (hp : p 0) (f : (lp E p)) (i : α) :
theorem lp.sum_rpow_le_norm_rpow {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), normed_group (E i)] (hp : 0 < p.to_real) (f : (lp E p)) (s : finset α) :
s.sum (λ (i : α), f i ^ p.to_real) f ^ p.to_real
theorem lp.norm_le_of_forall_le' {α : Type u_1} {E : α → Type u_2} [Π (i : α), normed_group (E i)] [nonempty α] {f : (lp E )} (C : ) (hCf : ∀ (i : α), f i C) :
theorem lp.norm_le_of_forall_le {α : Type u_1} {E : α → Type u_2} [Π (i : α), normed_group (E i)] {f : (lp E )} {C : } (hC : 0 C) (hCf : ∀ (i : α), f i C) :
theorem lp.norm_le_of_tsum_le {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), normed_group (E i)] (hp : 0 < p.to_real) {C : } (hC : 0 C) {f : (lp E p)} (hf : ∑' (i : α), f i ^ p.to_real C ^ p.to_real) :
theorem lp.norm_le_of_forall_sum_le {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), normed_group (E i)] (hp : 0 < p.to_real) {C : } (hC : 0 C) {f : (lp E p)} (hf : ∀ (s : finset α), s.sum (λ (i : α), f i ^ p.to_real) C ^ p.to_real) :
@[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)] :
module 𝕜 (pre_lp E)
Equations
theorem lp.mem_lp_const_smul {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), normed_group (E i)] {𝕜 : Type u_3} [normed_field 𝕜] [Π (i : α), normed_space 𝕜 (E i)] (c : 𝕜) (f : (lp E p)) :
c f lp E p
def lp.lp_submodule {α : Type u_1} (E : α → Type u_2) (p : ennreal) [Π (i : α), normed_group (E i)] (𝕜 : Type u_3) [normed_field 𝕜] [Π (i : α), normed_space 𝕜 (E i)] :
submodule 𝕜 (pre_lp E)

The 𝕜-submodule of elements of Π i : α, E i whose lp norm is finite. This is lp E p, with extra structure.

Equations
theorem lp.coe_lp_submodule {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), normed_group (E i)] {𝕜 : Type u_3} [normed_field 𝕜] [Π (i : α), normed_space 𝕜 (E i)] :
@[protected, instance]
def lp.module {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), normed_group (E i)] {𝕜 : Type u_3} [normed_field 𝕜] [Π (i : α), normed_space 𝕜 (E i)] :
module 𝕜 (lp E p)
Equations
@[simp]
theorem lp.coe_fn_smul {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), normed_group (E i)] {𝕜 : Type u_3} [normed_field 𝕜] [Π (i : α), normed_space 𝕜 (E i)] (c : 𝕜) (f : (lp E p)) :
(c f) = c f
theorem lp.norm_const_smul {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (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]
def lp.normed_space {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), normed_group (E i)] {𝕜 : Type u_3} [normed_field 𝕜] [Π (i : α), normed_space 𝕜 (E i)] [fact (1 p)] :
normed_space 𝕜 (lp E p)
Equations
@[protected, instance]
def lp.is_scalar_tower {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (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 : ennreal) (i : α) (a : E i) :
(lp E p)

The element of lp E p which is a : E i at the index i, and zero elsewhere.

Equations
@[protected]
theorem lp.single_apply {α : Type u_1} {E : α → Type u_2} [Π (i : α), normed_group (E i)] [decidable_eq α] (p : ennreal) (i : α) (a : E i) (j : α) :
(lp.single p i a) j = dite (j = i) (λ (h : j = i), eq.rec a _) (λ (h : ¬j = i), 0)
@[protected]
theorem lp.single_apply_self {α : Type u_1} {E : α → Type u_2} [Π (i : α), normed_group (E i)] [decidable_eq α] (p : ennreal) (i : α) (a : E i) :
(lp.single p i a) i = a
@[protected]
theorem lp.single_apply_ne {α : Type u_1} {E : α → Type u_2} [Π (i : α), normed_group (E i)] [decidable_eq α] (p : ennreal) (i : α) (a : E i) {j : α} (hij : j i) :
(lp.single p i a) j = 0
@[protected, simp]
theorem lp.single_neg {α : Type u_1} {E : α → Type u_2} [Π (i : α), normed_group (E i)] [decidable_eq α] (p : ennreal) (i : α) (a : E i) :
lp.single p i (-a) = -lp.single p i a
@[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 : ennreal) (i : α) (a : E i) (c : 𝕜) :
lp.single p i (c a) = c lp.single p i a
@[protected]
theorem lp.norm_sum_single {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), normed_group (E i)] [decidable_eq α] (hp : 0 < p.to_real) (f : Π (i : α), E i) (s : finset α) :
s.sum (λ (i : α), lp.single p i (f i)) ^ p.to_real = s.sum (λ (i : α), f i ^ p.to_real)
@[protected]
theorem lp.norm_single {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), normed_group (E i)] [decidable_eq α] (hp : 0 < p.to_real) (f : Π (i : α), E i) (i : α) :
lp.single p i (f i) = f i
@[protected]
theorem lp.norm_sub_norm_compl_sub_single {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), normed_group (E i)] [decidable_eq α] (hp : 0 < p.to_real) (f : (lp E p)) (s : finset α) :
f ^ p.to_real - f - s.sum (λ (i : α), lp.single p i (f i)) ^ p.to_real = s.sum (λ (i : α), f i ^ p.to_real)
@[protected]
theorem lp.norm_compl_sum_single {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), normed_group (E i)] [decidable_eq α] (hp : 0 < p.to_real) (f : (lp E p)) (s : finset α) :
f - s.sum (λ (i : α), lp.single p i (f i)) ^ p.to_real = f ^ p.to_real - s.sum (λ (i : α), f i ^ p.to_real)
@[protected]
theorem lp.has_sum_single {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), normed_group (E i)] [decidable_eq α] [fact (1 p)] (hp : p ) (f : (lp E p)) :
has_sum (λ (i : α), lp.single p i (f i)) f

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 : ennreal} [Π (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 (nhds f)) (a : α) :
f a C
theorem lp.sum_rpow_le_of_tendsto {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (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 (nhds f)) (s : finset α) :
s.sum (λ (i : α), f i ^ p.to_real) C ^ p.to_real
theorem lp.norm_le_of_tendsto {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (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 (nhds 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 : ennreal} [Π (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 (nhds f)) :

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 : ennreal} [Π (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 (nhds 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 : ennreal} [Π (i : α), normed_group (E i)] [fact (1 p)] [∀ (a : α), complete_space (E a)] :