# mathlibdocumentation

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 #

• mem_ℓp f p : property that the function f satisfies, as appropriate, f finitely supported if p = 0, summable (λ a, ∥f a∥^p) if 0 < p < ∞, and bdd_above (norm '' (set.range f)) if p = ∞.
• lp E p : elements of Π i : α, E i such that mem_ℓp f p. Defined as an add_subgroup of a type synonym pre_lp for Π i : α, E i, and equipped with a normed_add_comm_group structure. Under appropriate conditions, this is also equipped with the instances lp.normed_space, lp.complete_space. For p=∞, there is also lp.infty_normed_ring, lp.infty_normed_algebra, lp.infty_star_ring and lp.infty_cstar_ring.

## Main results #

• mem_ℓp.of_exponent_ge: For q ≤ p, a function which is mem_ℓp for q is also mem_ℓp for p
• lp.mem_ℓp_of_tendsto, lp.norm_le_of_tendsto: A pointwise limit of functions in lp, all with lp norm ≤ C, is itself in lp and has lp 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 satisfying 1 / r = 1 / p + 1 / q)
• Equivalence with pi_Lp, for α finite
• Equivalence with measure_theory.Lp, for f : α → E (i.e., functions rather than pi-types) and the counting measure on α
• Equivalence with bounded_continuous_function, for f : α → E (i.e., functions rather than pi-types) and p = ∞, and the discrete topology on α

### mem_ℓp predicate #

def mem_ℓp {α : Type u_1} {E : α → Type u_2} [Π (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 : α), ] {f : Π (i : α), E i} :
0 {i : α | f i 0}.finite
theorem mem_ℓp_zero {α : Type u_1} {E : α → Type u_2} [Π (i : α), ] {f : Π (i : α), E i} (hf : {i : α | f i 0}.finite) :
0
theorem mem_ℓp_infty_iff {α : Type u_1} {E : α → Type u_2} [Π (i : α), ] {f : Π (i : α), E i} :
bdd_above (set.range (λ (i : α), f i))
theorem mem_ℓp_infty {α : Type u_1} {E : α → Type u_2} [Π (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 : α), ] (hp : 0 < p.to_real) {f : Π (i : α), E i} :
p summable (λ (i : α), f i ^ p.to_real)
theorem mem_ℓp_gen {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), ] {f : Π (i : α), E i} (hf : summable (λ (i : α), f i ^ p.to_real)) :
p
theorem mem_ℓp_gen' {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), ] {C : } {f : Π (i : α), E i} (hf : ∀ (s : finset α), s.sum (λ (i : α), f i ^ p.to_real) C) :
p
theorem zero_mem_ℓp {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), ] :
p
theorem zero_mem_ℓp' {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), ] :
mem_ℓp (λ (i : α), 0) p
theorem mem_ℓp.finite_dsupport {α : Type u_1} {E : α → Type u_2} [Π (i : α), ] {f : Π (i : α), E i} (hf : 0) :
{i : α | f i 0}.finite
theorem mem_ℓp.bdd_above {α : Type u_1} {E : α → Type u_2} [Π (i : α), ] {f : Π (i : α), E i} (hf : ) :
bdd_above (set.range (λ (i : α), f i))
theorem mem_ℓp.summable {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), ] (hp : 0 < p.to_real) {f : Π (i : α), E i} (hf : p) :
summable (λ (i : α), f i ^ p.to_real)
theorem mem_ℓp.neg {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), ] {f : Π (i : α), E i} (hf : p) :
mem_ℓp (-f) p
@[simp]
theorem mem_ℓp.neg_iff {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), ] {f : Π (i : α), E i} :
mem_ℓp (-f) p p
theorem mem_ℓp.of_exponent_ge {α : Type u_1} {E : α → Type u_2} [Π (i : α), ] {p q : ennreal} {f : Π (i : α), E i} (hfq : q) (hpq : q p) :
p
theorem mem_ℓp.add {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), ] {f g : Π (i : α), E i} (hf : p) (hg : p) :
mem_ℓp (f + g) p
theorem mem_ℓp.sub {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), ] {f g : Π (i : α), E i} (hf : p) (hg : p) :
mem_ℓp (f - g) p
theorem mem_ℓp.finset_sum {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (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 : α), ] {𝕜 : Type u_3} [normed_field 𝕜] [Π (i : α), (E i)] {f : Π (i : α), E i} (hf : p) (c : 𝕜) :
mem_ℓp (c f) p
theorem mem_ℓp.const_mul {α : Type u_1} {p : ennreal} {𝕜 : Type u_3} [normed_field 𝕜] {f : α → 𝕜} (hf : 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 : α), ] :
@[nolint]
def pre_lp {α : Type u_1} (E : α → Type u_2) [Π (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
• = Π (i : α), E i
Instances for pre_lp
@[protected, instance]
def pre_lp.unique {α : Type u_1} {E : α → Type u_2} [Π (i : α), ] [is_empty α] :
Equations
def lp {α : Type u_1} (E : α → Type u_2) [Π (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 : α), ] :
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 : α), ] :
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 : α), ] {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 : α), ] {f g : (lp E p)} :
f = g f = g
theorem lp.eq_zero' {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), ] [is_empty α] (f : (lp E p)) :
f = 0
@[protected]
theorem lp.monotone {α : Type u_1} {E : α → Type u_2} [Π (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 : α), ] (f : (lp E p)) :
p
@[simp]
theorem lp.coe_fn_zero {α : Type u_1} (E : α → Type u_2) (p : ennreal) [Π (i : α), ] :
0 = 0
@[simp]
theorem lp.coe_fn_neg {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), ] (f : (lp E p)) :
@[simp]
theorem lp.coe_fn_add {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (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 : α), ] {ι : 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 : α), ] (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 : α), ] :
Equations
theorem lp.norm_eq_card_dsupport {α : Type u_1} {E : α → Type u_2} [Π (i : α), ] (f : (lp E 0)) :
theorem lp.norm_eq_csupr {α : Type u_1} {E : α → Type u_2} [Π (i : α), ] (f : (lp E )) :
f = ⨆ (i : α), f i
theorem lp.is_lub_norm {α : Type u_1} {E : α → Type u_2} [Π (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 : α), ] (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 : α), ] (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 : α), ] (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 : α), ] (f : (lp E p)) :
@[simp]
theorem lp.norm_zero {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), ] :
theorem lp.norm_eq_zero_iff {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (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 : α), ] {f : (lp E p)} :
f = 0 f = 0
@[simp]
theorem lp.norm_neg {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), ] ⦃f : (lp E p) :
@[protected, instance]
noncomputable def lp.normed_add_comm_group {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), ] [hp : fact (1 p)] :
Equations
@[protected]
theorem lp.tsum_mul_le_mul_norm {α : Type u_1} {E : α → Type u_2} [Π (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 : α), ] {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 : α), ] {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 : α), ] (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 : α), ] (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 : α), ] [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 : α), ] {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 : α), ] (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 : α), ] (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 : α), ] {𝕜 : Type u_3} [normed_field 𝕜] [Π (i : α), (E i)] :
(pre_lp E)
Equations
theorem lp.mem_lp_const_smul {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), ] {𝕜 : Type u_3} [normed_field 𝕜] [Π (i : α), (E i)] (c : 𝕜) (f : (lp E p)) :
c f lp E p
def lp_submodule {α : Type u_1} (E : α → Type u_2) (p : ennreal) [Π (i : α), ] (𝕜 : Type u_3) [normed_field 𝕜] [Π (i : α), (E i)] :
(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 : α), ] {𝕜 : Type u_3} [normed_field 𝕜] [Π (i : α), (E i)] :
p 𝕜).to_add_subgroup = lp E p
@[protected, instance]
def lp.module {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), ] {𝕜 : Type u_3} [normed_field 𝕜] [Π (i : α), (E i)] :
(lp E p)
Equations
@[simp]
theorem lp.coe_fn_smul {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), ] {𝕜 : Type u_3} [normed_field 𝕜] [Π (i : α), (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 : α), ] {𝕜 : Type u_3} [normed_field 𝕜] [Π (i : α), (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 : α), ] {𝕜 : Type u_3} [normed_field 𝕜] [Π (i : α), (E i)] [fact (1 p)] :
(lp E p)
Equations
@[protected, instance]
def lp.is_scalar_tower {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), ] {𝕜 : Type u_3} [normed_field 𝕜] [Π (i : α), (E i)] {𝕜' : Type u_4} [normed_field 𝕜'] [Π (i : α), (E i)] [has_smul 𝕜' 𝕜] [∀ (i : α), 𝕜 (E i)] :
𝕜 (lp E p)
theorem mem_ℓp.star_mem {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), ] [Π (i : α), star_add_monoid (E i)] [∀ (i : α), normed_star_group (E i)] {f : Π (i : α), E i} (hf : p) :
p
@[simp]
theorem mem_ℓp.star_iff {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), ] [Π (i : α), star_add_monoid (E i)] [∀ (i : α), normed_star_group (E i)] {f : Π (i : α), E i} :
p p
@[protected, instance]
def lp.has_star {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), ] [Π (i : α), star_add_monoid (E i)] [∀ (i : α), normed_star_group (E i)] :
Equations
@[simp]
theorem lp.coe_fn_star {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), ] [Π (i : α), star_add_monoid (E i)] [∀ (i : α), normed_star_group (E i)] (f : (lp E p)) :
@[protected, simp]
theorem lp.star_apply {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), ] [Π (i : α), star_add_monoid (E i)] [∀ (i : α), normed_star_group (E i)] (f : (lp E p)) (i : α) :
@[protected, instance]
def lp.has_involutive_star {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), ] [Π (i : α), star_add_monoid (E i)] [∀ (i : α), normed_star_group (E i)] :
Equations
@[protected, instance]
def lp.star_add_monoid {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), ] [Π (i : α), star_add_monoid (E i)] [∀ (i : α), normed_star_group (E i)] :
Equations
@[protected, instance]
def lp.normed_star_group {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), ] [Π (i : α), star_add_monoid (E i)] [∀ (i : α), normed_star_group (E i)] [hp : fact (1 p)] :
@[protected, instance]
def lp.star_module {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), ] [Π (i : α), star_add_monoid (E i)] [∀ (i : α), normed_star_group (E i)] {𝕜 : Type u_3} [has_star 𝕜] [normed_field 𝕜] [Π (i : α), (E i)] [∀ (i : α), (E i)] :
(lp E p)
theorem mem_ℓp.infty_mul {I : Type u_3} {B : I → Type u_4} [Π (i : I), ] {f g : Π (i : I), B i} (hf : ) (hg : ) :
mem_ℓp (f * g)
@[protected, instance]
noncomputable def lp.has_mul {I : Type u_3} {B : I → Type u_4} [Π (i : I), ] :
Equations
@[simp]
theorem lp.infty_coe_fn_mul {I : Type u_3} {B : I → Type u_4} [Π (i : I), ] (f g : (lp B )) :
(f * g) = f * g
@[protected, instance]
noncomputable def lp.non_unital_ring {I : Type u_3} {B : I → Type u_4} [Π (i : I), ] :
Equations
• lp.non_unital_ring = 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
@[protected, instance]
noncomputable def lp.non_unital_normed_ring {I : Type u_3} {B : I → Type u_4} [Π (i : I), ] :
Equations
@[protected, instance]
def lp.infty_is_scalar_tower {I : Type u_3} {B : I → Type u_4} [Π (i : I), ] {𝕜 : Type u_1} [normed_field 𝕜] [Π (i : I), (B i)] [∀ (i : I), (B i) (B i)] :
(lp B ) (lp B )
@[protected, instance]
def lp.infty_smul_comm_class {I : Type u_3} {B : I → Type u_4} [Π (i : I), ] {𝕜 : Type u_1} [normed_field 𝕜] [Π (i : I), (B i)] [∀ (i : I), (B i) (B i)] :
(lp B ) (lp B )
@[protected, instance]
noncomputable def lp.infty_star_ring {I : Type u_3} {B : I → Type u_4} [Π (i : I), ] [Π (i : I), star_ring (B i)] [∀ (i : I), normed_star_group (B i)] :
Equations
@[protected, instance]
def lp.infty_cstar_ring {I : Type u_3} {B : I → Type u_4} [Π (i : I), ] [Π (i : I), star_ring (B i)] [∀ (i : I), normed_star_group (B i)] [∀ (i : I), cstar_ring (B i)] :
@[protected, instance]
def pre_lp.ring {I : Type u_3} {B : I → Type u_4} [Π (i : I), normed_ring (B i)] :
Equations
theorem one_mem_ℓp_infty {I : Type u_3} {B : I → Type u_4} [Π (i : I), normed_ring (B i)] [∀ (i : I), norm_one_class (B i)] :
def lp_infty_subring {I : Type u_3} (B : I → Type u_4) [Π (i : I), normed_ring (B i)] [∀ (i : I), norm_one_class (B i)] :

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

Equations
@[protected, instance]
def lp.infty_ring {I : Type u_3} {B : I → Type u_4} [Π (i : I), normed_ring (B i)] [∀ (i : I), norm_one_class (B i)] :
Equations
theorem mem_ℓp.infty_pow {I : Type u_3} {B : I → Type u_4} [Π (i : I), normed_ring (B i)] [∀ (i : I), norm_one_class (B i)] {f : Π (i : I), B i} (hf : ) (n : ) :
mem_ℓp (f ^ n)
theorem nat_cast_mem_ℓp_infty {I : Type u_3} {B : I → Type u_4} [Π (i : I), normed_ring (B i)] [∀ (i : I), norm_one_class (B i)] (n : ) :
theorem int_cast_mem_ℓp_infty {I : Type u_3} {B : I → Type u_4} [Π (i : I), normed_ring (B i)] [∀ (i : I), norm_one_class (B i)] (z : ) :
@[simp]
theorem lp.infty_coe_fn_one {I : Type u_3} {B : I → Type u_4} [Π (i : I), normed_ring (B i)] [∀ (i : I), norm_one_class (B i)] :
1 = 1
@[simp]
theorem lp.infty_coe_fn_pow {I : Type u_3} {B : I → Type u_4} [Π (i : I), normed_ring (B i)] [∀ (i : I), norm_one_class (B i)] (f : (lp B )) (n : ) :
(f ^ n) = f ^ n
@[simp]
theorem lp.infty_coe_fn_nat_cast {I : Type u_3} {B : I → Type u_4} [Π (i : I), normed_ring (B i)] [∀ (i : I), norm_one_class (B i)] (n : ) :
@[simp]
theorem lp.infty_coe_fn_int_cast {I : Type u_3} {B : I → Type u_4} [Π (i : I), normed_ring (B i)] [∀ (i : I), norm_one_class (B i)] (z : ) :
@[protected, instance]
def lp.norm_one_class {I : Type u_3} {B : I → Type u_4} [Π (i : I), normed_ring (B i)] [∀ (i : I), norm_one_class (B i)] [nonempty I] :
@[protected, instance]
noncomputable def lp.infty_normed_ring {I : Type u_3} {B : I → Type u_4} [Π (i : I), normed_ring (B i)] [∀ (i : I), norm_one_class (B i)] :
Equations
@[protected, instance]
def lp.infty_comm_ring {I : Type u_3} {B : I → Type u_4} [Π (i : I), normed_comm_ring (B i)] [∀ (i : I), norm_one_class (B i)] :
Equations
@[protected, instance]
noncomputable def lp.infty_normed_comm_ring {I : Type u_3} {B : I → Type u_4} [Π (i : I), normed_comm_ring (B i)] [∀ (i : I), norm_one_class (B i)] :
Equations
@[protected, instance]
def pi.algebra_of_normed_algebra {I : Type u_3} {𝕜 : Type u_4} {B : I → Type u_5} [normed_field 𝕜] [Π (i : I), normed_ring (B i)] [Π (i : I), (B i)] :
(Π (i : I), B i)

A variant of pi.algebra that lean can't find otherwise.

Equations
@[protected, instance]
def pre_lp.algebra {I : Type u_3} {𝕜 : Type u_4} {B : I → Type u_5} [normed_field 𝕜] [Π (i : I), normed_ring (B i)] [Π (i : I), (B i)] :
(pre_lp B)
Equations
theorem algebra_map_mem_ℓp_infty {I : Type u_3} {𝕜 : Type u_4} {B : I → Type u_5} [normed_field 𝕜] [Π (i : I), normed_ring (B i)] [Π (i : I), (B i)] [∀ (i : I), norm_one_class (B i)] (k : 𝕜) :
mem_ℓp ( (Π (i : I), B i)) k)
def lp_infty_subalgebra {I : Type u_3} (𝕜 : Type u_4) (B : I → Type u_5) [normed_field 𝕜] [Π (i : I), normed_ring (B i)] [Π (i : I), (B i)] [∀ (i : I), norm_one_class (B i)] :
(pre_lp B)

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

Equations
@[protected, instance]
def lp.infty_normed_algebra {I : Type u_3} {𝕜 : Type u_4} {B : I → Type u_5} [normed_field 𝕜] [Π (i : I), normed_ring (B i)] [Π (i : I), (B i)] [∀ (i : I), norm_one_class (B i)] :
(lp B )
Equations
@[protected]
def lp.single {α : Type u_1} {E : α → Type u_2} [Π (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
• i a = λ (j : α), dite (j = i) (λ (h : j = i), eq.rec a _) (λ (h : ¬j = i), 0), _⟩
@[protected]
theorem lp.single_apply {α : Type u_1} {E : α → Type u_2} [Π (i : α), ] [decidable_eq α] (p : ennreal) (i : α) (a : E i) (j : α) :
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 : α), ] [decidable_eq α] (p : ennreal) (i : α) (a : E i) :
i a) i = a
@[protected]
theorem lp.single_apply_ne {α : Type u_1} {E : α → Type u_2} [Π (i : α), ] [decidable_eq α] (p : ennreal) (i : α) (a : E i) {j : α} (hij : j i) :
i a) j = 0
@[protected, simp]
theorem lp.single_neg {α : Type u_1} {E : α → Type u_2} [Π (i : α), ] [decidable_eq α] (p : ennreal) (i : α) (a : E i) :
i (-a) = - i a
@[protected, simp]
theorem lp.single_smul {α : Type u_1} {E : α → Type u_2} [Π (i : α), ] {𝕜 : Type u_3} [normed_field 𝕜] [Π (i : α), (E i)] [decidable_eq α] (p : ennreal) (i : α) (a : E i) (c : 𝕜) :
i (c a) = c i a
@[protected]
theorem lp.norm_sum_single {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), ] [decidable_eq α] (hp : 0 < p.to_real) (f : Π (i : α), E i) (s : finset α) :
s.sum (λ (i : α), 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 : α), ] [decidable_eq α] (hp : 0 < p.to_real) (f : Π (i : α), E i) (i : α) :
i (f i) = f i
@[protected]
theorem lp.norm_sub_norm_compl_sub_single {α : Type u_1} {E : α → Type u_2} {p : ennreal} [Π (i : α), ] [decidable_eq α] (hp : 0 < p.to_real) (f : (lp E p)) (s : finset α) :
f ^ p.to_real - f - s.sum (λ (i : α), 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 : α), ] [decidable_eq α] (hp : 0 < p.to_real) (f : (lp E p)) (s : finset α) :
f - s.sum (λ (i : α), 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 : α), ] [decidable_eq α] [fact (1 p)] (hp : p ) (f : (lp E p)) :
has_sum (λ (i : α), 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 : α), ] [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 : α), ] {ι : 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 : α), ] {ι : 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 : α), ] {ι : 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 : α), ] {ι : 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)) :
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 : ennreal} [Π (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 : α), ] [fact (1 p)] [∀ (a : α), complete_space (E a)] :