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 #

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)

`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

mem_ℓp f p = ite (p = 0) {i : α | f i ≠ 0}.finite (ite (p = ⊤) (bdd_above (set.range (λ (i : α), ‖f i‖))) (summable (λ (i : α), ‖f i‖ ^ p.to_real)))

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} :

mem_ℓp (-f) p ↔ mem_ℓp f p

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)] :

add_comm_group (pre_lp E)

@[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

pre_lp E = Π (i : α), E i

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 α] :

unique (pre_lp E)

Equations

pre_lp.unique = pi.unique_of_is_empty E

def lp {α : Type u_1} (E : α → Type u_2) [Π (i : α), normed_add_comm_group (E i)] (p : ennreal) :

add_subgroup (pre_lp E)

lp space

Equations

lp E p = {carrier := {f : pre_lp E | mem_ℓp f p}, add_mem' := _, zero_mem' := _, neg_mem' := _}

Instances for ↥lp

@[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

lp.pi.has_coe = coe_subtype

@[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

lp.has_coe_to_fun = {coe := λ (f : ↥(lp E p)), ↑f}

@[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)) :

mem_ℓp ⇑f 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)] :

has_norm ↥(lp E p)

Equations

lp.has_norm = {norm := λ (f : ↥(lp E p)), dite (p = 0) (λ (hp : p = 0), eq.rec (λ (f : ↥(lp E 0)), ↑(_.to_finset.card)) _ f) (λ (hp : ¬p = 0), ite (p = ⊤) (⨆ (i : α), ‖⇑f i‖) ((∑' (i : α), ‖⇑f i‖ ^ p.to_real) ^ (1 / p.to_real)))}

theorem lp.norm_eq_card_dsupport {α : Type u_1} {E : α → Type u_2} [Π (i : α), normed_add_comm_group (E i)] (f : ↥(lp E 0)) :

‖f‖ = ↑(_.to_finset.card)

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

‖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_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)⦄ :

‖-f‖ = ‖f‖

@[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)] :

normed_add_comm_group ↥(lp E p)

Equations

lp.normed_add_comm_group = {to_fun := has_norm.norm lp.has_norm, map_zero' := _, add_le' := _, neg' := _, eq_zero_of_map_eq_zero' := _}.to_normed_add_comm_group

@[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)) :

∑' (i : α), ‖⇑f i‖ * ‖⇑g i‖ ≤ ‖f‖ * ‖g‖

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 : α) :

‖⇑f i‖ ≤ ‖f‖

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

lp.pre_lp.module = pi.module α E 𝕜

@[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)] :

is_central_scalar 𝕜 (pre_lp E)

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

lp_submodule E p 𝕜 = {carrier := (lp E p).carrier, add_mem' := _, zero_mem' := _, smul_mem' := _}

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)] :

(lp_submodule E p 𝕜).to_add_subgroup = lp E p

@[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

lp.module = {to_distrib_mul_action := module.to_distrib_mul_action (lp_submodule E p 𝕜).module, add_smul := _, zero_smul := _}

@[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)] :

is_central_scalar 𝕜 ↥(lp E p)

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

‖c • f‖ ≤ ‖c‖ * ‖f‖

@[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)] :

has_bounded_smul 𝕜 ↥(lp E 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)) :

‖c • f‖ = ‖c‖ * ‖f‖

@[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

lp.normed_space = {to_module := lp.module lp.normed_space._proof_1, norm_smul_le := _}

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

mem_ℓp (has_star.star 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} :

mem_ℓp (has_star.star f) p ↔ mem_ℓp f p

@[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)] :

has_star ↥(lp E p)

Equations

lp.has_star = {star := λ (f : ↥(lp E p)), ⟨has_star.star ⇑f, _⟩}

@[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)) :

⇑(has_star.star f) = has_star.star ⇑f

@[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 : α) :

⇑(has_star.star f) i = has_star.star (⇑f 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)] :

has_involutive_star ↥(lp E p)

Equations

lp.has_involutive_star = {to_has_star := lp.has_star lp.has_involutive_star._proof_1, star_involutive := _}

@[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)] :

star_add_monoid ↥(lp E p)

Equations

lp.star_add_monoid = {to_has_involutive_star := lp.has_involutive_star lp.star_add_monoid._proof_1, star_add := _}

@[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)] :

normed_star_group ↥(lp E 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)] :

has_mul ↥(lp B ⊤)

Equations

lp.has_mul = {mul := λ (f g : ↥(lp B ⊤)), ⟨⇑f * ⇑g, _⟩}

@[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)] :

non_unital_ring ↥(lp B ⊤)

Equations

lp.non_unital_ring = function.injective.non_unital_ring has_coe_to_fun.coe 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), non_unital_normed_ring (B i)] :

non_unital_normed_ring ↥(lp B ⊤)

Equations

lp.non_unital_normed_ring = {to_has_norm := normed_add_comm_group.to_has_norm lp.normed_add_comm_group, to_non_unital_ring := lp.non_unital_ring (λ (i : I), _inst_2 i), to_metric_space := normed_add_comm_group.to_metric_space lp.normed_add_comm_group, dist_eq := _, norm_mul := _}

@[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)] :

is_scalar_tower 𝕜 ↥(lp B ⊤) ↥(lp B ⊤)

@[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)] :

smul_comm_class 𝕜 ↥(lp B ⊤) ↥(lp B ⊤)

@[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)] :

star_ring ↥(lp B ⊤)

Equations

lp.infty_star_ring = {to_star_semigroup := {to_has_involutive_star := star_add_monoid.to_has_involutive_star (show star_add_monoid ↥(lp B ⊤), from let _inst : Π (i : I), star_add_monoid (B i) := λ (i : I), infer_instance in lp.star_add_monoid), star_mul := _}, star_add := _}

@[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)] :

cstar_ring ↥(lp B ⊤)

@[protected, instance]

def pre_lp.ring {I : Type u_3} {B : I → Type u_4} [Π (i : I), normed_ring (B i)] :

ring (pre_lp B)

Equations

pre_lp.ring = pi.ring

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)] :

subring (pre_lp B)

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

Equations

lp_infty_subring B = {carrier := {f : pre_lp B | mem_ℓp f ⊤}, mul_mem' := _, one_mem' := _, add_mem' := _, zero_mem' := _, neg_mem' := _}

@[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)] :

ring ↥(lp B ⊤)

Equations

lp.infty_ring = (lp_infty_subring B).to_ring

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 : ℕ) :

mem_ℓp ↑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 : ℤ) :

mem_ℓp ↑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] :

norm_one_class ↥(lp B ⊤)

@[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)] :

normed_ring ↥(lp B ⊤)

Equations

lp.infty_normed_ring = {to_has_norm := non_unital_normed_ring.to_has_norm lp.non_unital_normed_ring, to_ring := {add := ring.add lp.infty_ring, add_assoc := _, zero := ring.zero lp.infty_ring, zero_add := _, add_zero := _, nsmul := ring.nsmul lp.infty_ring, nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg lp.infty_ring, sub := ring.sub lp.infty_ring, sub_eq_add_neg := _, zsmul := ring.zsmul lp.infty_ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := ring.int_cast lp.infty_ring, nat_cast := ring.nat_cast lp.infty_ring, one := ring.one lp.infty_ring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := ring.mul lp.infty_ring, mul_assoc := _, one_mul := _, mul_one := _, npow := ring.npow lp.infty_ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _}, to_metric_space := non_unital_normed_ring.to_metric_space lp.non_unital_normed_ring, dist_eq := _, norm_mul := _}

@[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)] :

comm_ring ↥(lp B ⊤)

Equations

lp.infty_comm_ring = {add := ring.add lp.infty_ring, add_assoc := _, zero := ring.zero lp.infty_ring, zero_add := _, add_zero := _, nsmul := ring.nsmul lp.infty_ring, nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg lp.infty_ring, sub := ring.sub lp.infty_ring, sub_eq_add_neg := _, zsmul := ring.zsmul lp.infty_ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := ring.int_cast lp.infty_ring, nat_cast := ring.nat_cast lp.infty_ring, one := ring.one lp.infty_ring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := ring.mul lp.infty_ring, mul_assoc := _, one_mul := _, mul_one := _, npow := ring.npow lp.infty_ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _}

@[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)] :

normed_comm_ring ↥(lp B ⊤)

Equations

lp.infty_normed_comm_ring = {to_normed_ring := {to_has_norm := normed_ring.to_has_norm lp.infty_normed_ring, to_ring := normed_ring.to_ring lp.infty_normed_ring, to_metric_space := normed_ring.to_metric_space lp.infty_normed_ring, dist_eq := _, norm_mul := _}, mul_comm := _}

@[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

pi.algebra_of_normed_algebra = pi.algebra I B

@[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

pre_lp.algebra = pi.algebra_of_normed_algebra

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)] :

subalgebra 𝕜 (pre_lp B)

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

Equations

lp_infty_subalgebra 𝕜 B = {carrier := {f : pre_lp B | mem_ℓp f ⊤}, mul_mem' := _, one_mem' := _, add_mem' := _, zero_mem' := _, algebra_map_mem' := _}

@[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)] :

normed_algebra 𝕜 ↥(lp B ⊤)

Equations

lp.infty_normed_algebra = {to_algebra := {to_has_smul := algebra.to_has_smul (lp_infty_subalgebra 𝕜 B).algebra, to_ring_hom := algebra.to_ring_hom (lp_infty_subalgebra 𝕜 B).algebra, commutes' := _, smul_def' := _}, norm_smul_le := _}

@[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

lp.single p 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 : α), 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)] :

uniform_continuous coe

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

filter.tendsto F 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)] :

complete_space ↥(lp E p)