mathlib3 documentation

analysis.normed_space.lp_space

ℓp space #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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_add_comm_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_add_comm_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_add_comm_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_add_comm_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_add_comm_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_add_comm_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_add_comm_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_add_comm_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_add_comm_group (E i)] :
theorem zero_mem_ℓp' {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), normed_add_comm_group (E i)] :
mem_ℓp (λ (i : α), 0) p
theorem mem_ℓp.finite_dsupport {α : Type u_1} {E : α Type u_2} [Π (i : α), normed_add_comm_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_add_comm_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_add_comm_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_add_comm_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_add_comm_group (E i)] {f : Π (i : α), E i} :
theorem mem_ℓp.of_exponent_ge {α : Type u_1} {E : α Type u_2} [Π (i : α), normed_add_comm_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_add_comm_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_add_comm_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_add_comm_group (E i)] {ι : Type u_3} (s : finset ι) {f : ι Π (i : α), E i} (hf : (i : ι), i s mem_ℓ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_add_comm_group (E i)] {𝕜 : Type u_3} [normed_ring 𝕜] [Π (i : α), module 𝕜 (E i)] [ (i : α), has_bounded_smul 𝕜 (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_ring 𝕜] {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_add_comm_group (E i)] :
@[nolint]
def pre_lp {α : Type u_1} (E : α Type u_2) [Π (i : α), normed_add_comm_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_add_comm_group (E i)] [is_empty α] :
Equations
@[protected, instance]
def lp.pi.has_coe {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), normed_add_comm_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_add_comm_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_add_comm_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_add_comm_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_add_comm_group (E i)] [is_empty α] (f : (lp E p)) :
f = 0
@[protected]
theorem lp.monotone {α : Type u_1} {E : α Type u_2} [Π (i : α), normed_add_comm_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_add_comm_group (E i)] (f : (lp E p)) :
@[simp]
theorem lp.coe_fn_zero {α : Type u_1} (E : α Type u_2) (p : ennreal) [Π (i : α), normed_add_comm_group (E i)] :
0 = 0
@[simp]
theorem lp.coe_fn_neg {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), normed_add_comm_group (E i)] (f : (lp E p)) :
@[simp]
theorem lp.coe_fn_add {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), normed_add_comm_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_add_comm_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_add_comm_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_add_comm_group (E i)] :
Equations
theorem lp.norm_eq_card_dsupport {α : Type u_1} {E : α Type u_2} [Π (i : α), normed_add_comm_group (E i)] (f : (lp E 0)) :
theorem lp.norm_eq_csupr {α : Type u_1} {E : α Type u_2} [Π (i : α), normed_add_comm_group (E i)] (f : (lp E )) :
f = (i : α), f i
theorem lp.is_lub_norm {α : Type u_1} {E : α Type u_2} [Π (i : α), normed_add_comm_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_add_comm_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_add_comm_group (E i)] (hp : 0 < p.to_real) (f : (lp E p)) :
theorem lp.has_sum_norm {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), normed_add_comm_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_add_comm_group (E i)] (f : (lp E p)) :
@[simp]
theorem lp.norm_zero {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), normed_add_comm_group (E i)] :
theorem lp.norm_eq_zero_iff {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), normed_add_comm_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_add_comm_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_add_comm_group (E i)] ⦃f : (lp E p) :
@[protected, instance]
noncomputable def lp.normed_add_comm_group {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), normed_add_comm_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_add_comm_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_add_comm_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_add_comm_group (E i)] {p q : ennreal} (hpq : p.to_real.is_conjugate_exponent q.to_real) (f : (lp E p)) (g : (lp E q)) :
theorem lp.norm_apply_le_norm {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), normed_add_comm_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_add_comm_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_add_comm_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_add_comm_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_add_comm_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_add_comm_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_add_comm_group (E i)] {𝕜 : Type u_3} [normed_ring 𝕜] [Π (i : α), module 𝕜 (E i)] :
module 𝕜 (pre_lp E)
Equations
@[protected, instance]
def lp.pre_lp.smul_comm_class {α : Type u_1} {E : α Type u_2} [Π (i : α), normed_add_comm_group (E i)] {𝕜 : Type u_3} {𝕜' : Type u_4} [normed_ring 𝕜] [normed_ring 𝕜'] [Π (i : α), module 𝕜 (E i)] [Π (i : α), module 𝕜' (E i)] [ (i : α), smul_comm_class 𝕜' 𝕜 (E i)] :
smul_comm_class 𝕜' 𝕜 (pre_lp E)
@[protected, instance]
def lp.pre_lp.is_scalar_tower {α : Type u_1} {E : α Type u_2} [Π (i : α), normed_add_comm_group (E i)] {𝕜 : Type u_3} {𝕜' : Type u_4} [normed_ring 𝕜] [normed_ring 𝕜'] [Π (i : α), module 𝕜 (E i)] [Π (i : α), module 𝕜' (E i)] [has_smul 𝕜' 𝕜] [ (i : α), is_scalar_tower 𝕜' 𝕜 (E i)] :
is_scalar_tower 𝕜' 𝕜 (pre_lp E)
@[protected, instance]
def lp.pre_lp.is_central_scalar {α : Type u_1} {E : α Type u_2} [Π (i : α), normed_add_comm_group (E i)] {𝕜 : Type u_3} [normed_ring 𝕜] [Π (i : α), module 𝕜 (E i)] [Π (i : α), module 𝕜ᵐᵒᵖ (E i)] [ (i : α), is_central_scalar 𝕜 (E i)] :
theorem lp.mem_lp_const_smul {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), normed_add_comm_group (E i)] {𝕜 : Type u_3} [normed_ring 𝕜] [Π (i : α), module 𝕜 (E i)] [ (i : α), has_bounded_smul 𝕜 (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 : α), normed_add_comm_group (E i)] (𝕜 : Type u_3) [normed_ring 𝕜] [Π (i : α), module 𝕜 (E i)] [ (i : α), has_bounded_smul 𝕜 (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_add_comm_group (E i)] {𝕜 : Type u_3} [normed_ring 𝕜] [Π (i : α), module 𝕜 (E i)] [ (i : α), has_bounded_smul 𝕜 (E i)] :
@[protected, instance]
def lp.module {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), normed_add_comm_group (E i)] {𝕜 : Type u_3} [normed_ring 𝕜] [Π (i : α), module 𝕜 (E i)] [ (i : α), has_bounded_smul 𝕜 (E i)] :
module 𝕜 (lp E p)
Equations
@[simp]
theorem lp.coe_fn_smul {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), normed_add_comm_group (E i)] {𝕜 : Type u_3} [normed_ring 𝕜] [Π (i : α), module 𝕜 (E i)] [ (i : α), has_bounded_smul 𝕜 (E i)] (c : 𝕜) (f : (lp E p)) :
(c f) = c f
@[protected, instance]
def lp.smul_comm_class {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), normed_add_comm_group (E i)] {𝕜 : Type u_3} {𝕜' : Type u_4} [normed_ring 𝕜] [normed_ring 𝕜'] [Π (i : α), module 𝕜 (E i)] [Π (i : α), module 𝕜' (E i)] [ (i : α), has_bounded_smul 𝕜 (E i)] [ (i : α), has_bounded_smul 𝕜' (E i)] [ (i : α), smul_comm_class 𝕜' 𝕜 (E i)] :
smul_comm_class 𝕜' 𝕜 (lp E p)
@[protected, instance]
def lp.is_scalar_tower {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), normed_add_comm_group (E i)] {𝕜 : Type u_3} {𝕜' : Type u_4} [normed_ring 𝕜] [normed_ring 𝕜'] [Π (i : α), module 𝕜 (E i)] [Π (i : α), module 𝕜' (E i)] [ (i : α), has_bounded_smul 𝕜 (E i)] [ (i : α), has_bounded_smul 𝕜' (E i)] [has_smul 𝕜' 𝕜] [ (i : α), is_scalar_tower 𝕜' 𝕜 (E i)] :
is_scalar_tower 𝕜' 𝕜 (lp E p)
@[protected, instance]
def lp.is_central_scalar {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), normed_add_comm_group (E i)] {𝕜 : Type u_3} [normed_ring 𝕜] [Π (i : α), module 𝕜 (E i)] [ (i : α), has_bounded_smul 𝕜 (E i)] [Π (i : α), module 𝕜ᵐᵒᵖ (E i)] [ (i : α), is_central_scalar 𝕜 (E i)] :
theorem lp.norm_const_smul_le {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), normed_add_comm_group (E i)] {𝕜 : Type u_3} [normed_ring 𝕜] [Π (i : α), module 𝕜 (E i)] [ (i : α), has_bounded_smul 𝕜 (E i)] (hp : p 0) (c : 𝕜) (f : (lp E p)) :
@[protected, instance]
def lp.has_bounded_smul {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), normed_add_comm_group (E i)] {𝕜 : Type u_3} [normed_ring 𝕜] [Π (i : α), module 𝕜 (E i)] [ (i : α), has_bounded_smul 𝕜 (E i)] [fact (1 p)] :
theorem lp.norm_const_smul {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), normed_add_comm_group (E i)] {𝕜 : Type u_3} [normed_division_ring 𝕜] [Π (i : α), module 𝕜 (E i)] [ (i : α), has_bounded_smul 𝕜 (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_add_comm_group (E i)] {𝕜 : Type u_3} [normed_field 𝕜] [Π (i : α), normed_space 𝕜 (E i)] [fact (1 p)] :
normed_space 𝕜 (lp E p)
Equations
theorem mem_ℓp.star_mem {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), normed_add_comm_group (E i)] [Π (i : α), star_add_monoid (E i)] [ (i : α), normed_star_group (E i)] {f : Π (i : α), E i} (hf : mem_ℓp f p) :
@[simp]
theorem mem_ℓp.star_iff {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), normed_add_comm_group (E i)] [Π (i : α), star_add_monoid (E i)] [ (i : α), normed_star_group (E i)] {f : Π (i : α), E i} :
@[protected, instance]
def lp.has_star {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), normed_add_comm_group (E 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 : α), normed_add_comm_group (E 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 : α), normed_add_comm_group (E 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 : α), normed_add_comm_group (E 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 : α), normed_add_comm_group (E 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 : α), normed_add_comm_group (E 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 : α), normed_add_comm_group (E i)] [Π (i : α), star_add_monoid (E i)] [ (i : α), normed_star_group (E i)] {𝕜 : Type u_3} [has_star 𝕜] [normed_ring 𝕜] [Π (i : α), module 𝕜 (E i)] [ (i : α), has_bounded_smul 𝕜 (E i)] [ (i : α), star_module 𝕜 (E i)] :
star_module 𝕜 (lp E p)
theorem mem_ℓp.infty_mul {I : Type u_3} {B : I Type u_4} [Π (i : I), non_unital_normed_ring (B i)] {f g : Π (i : I), B i} (hf : mem_ℓp f ) (hg : mem_ℓp g ) :
mem_ℓp (f * g)
@[protected, instance]
noncomputable def lp.has_mul {I : Type u_3} {B : I Type u_4} [Π (i : I), non_unital_normed_ring (B i)] :
Equations
@[simp]
theorem lp.infty_coe_fn_mul {I : Type u_3} {B : I Type u_4} [Π (i : I), non_unital_normed_ring (B 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), non_unital_normed_ring (B i)] :
Equations
@[protected, instance]
def lp.infty_is_scalar_tower {I : Type u_3} {B : I Type u_4} [Π (i : I), non_unital_normed_ring (B i)] {𝕜 : Type u_1} [normed_ring 𝕜] [Π (i : I), module 𝕜 (B i)] [ (i : I), has_bounded_smul 𝕜 (B i)] [ (i : I), is_scalar_tower 𝕜 (B i) (B i)] :
@[protected, instance]
def lp.infty_smul_comm_class {I : Type u_3} {B : I Type u_4} [Π (i : I), non_unital_normed_ring (B i)] {𝕜 : Type u_1} [normed_ring 𝕜] [Π (i : I), module 𝕜 (B i)] [ (i : I), has_bounded_smul 𝕜 (B i)] [ (i : I), smul_comm_class 𝕜 (B i) (B i)] :
@[protected, instance]
noncomputable def lp.infty_star_ring {I : Type u_3} {B : I Type u_4} [Π (i : I), non_unital_normed_ring (B 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), non_unital_normed_ring (B 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 : mem_ℓp f ) (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]
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), normed_algebra 𝕜 (B i)] :
algebra 𝕜 (Π (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), normed_algebra 𝕜 (B i)] :
algebra 𝕜 (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), normed_algebra 𝕜 (B i)] [ (i : I), norm_one_class (B i)] (k : 𝕜) :
mem_ℓp ((algebra_map 𝕜 (Π (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), normed_algebra 𝕜 (B i)] [ (i : I), norm_one_class (B i)] :

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), normed_algebra 𝕜 (B i)] [ (i : I), norm_one_class (B i)] :
Equations
@[protected]
def lp.single {α : Type u_1} {E : α Type u_2} [Π (i : α), normed_add_comm_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_add_comm_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_add_comm_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_add_comm_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_add_comm_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_add_comm_group (E i)] {𝕜 : Type u_3} [normed_ring 𝕜] [Π (i : α), module 𝕜 (E i)] [ (i : α), has_bounded_smul 𝕜 (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_add_comm_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_add_comm_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_add_comm_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_add_comm_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_add_comm_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_add_comm_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_add_comm_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_add_comm_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_add_comm_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_add_comm_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_add_comm_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_add_comm_group (E i)] [fact (1 p)] [ (a : α), complete_space (E a)] :