ℓ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 (fun a ↦ ‖f a‖^p) if 0 < p < ∞, and BddAbove (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 (fun a ↦ ‖f a‖^p) if 0 < p < ∞, and BddAbove (norm '' (Set.range f)) if p = ∞.
• lp E p : elements of ∀ i : α, E i such that Memℓp f p. Defined as an AddSubgroup of a type synonym PreLp for ∀ i : α, E i, and equipped with a NormedAddCommGroup structure. Under appropriate conditions, this is also equipped with the instances lp.normedSpace, lp.completeSpace. For p=∞, there is also lp.inftyNormedRing, lp.inftyNormedAlgebra, lp.inftyStarRing and lp.inftyCStarRing.

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 AddSubgroup, 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_3} {E : α → Type u_4} [(i : α) → NormedAddCommGroup (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 (fun i ↦ ‖f i‖), if p = ∞, or
• has the series ∑' i, ‖f i‖ ^ p be summable, if 0 < p < ∞.

theorem memℓp_zero_iff {α : Type u_3} {E : α → Type u_4} [(i : α) → NormedAddCommGroup (E i)] {f : (i : α) → E i} : Memℓp f 0 ↔ {i : α | f i ≠ 0}.Finite

theorem memℓp_zero {α : Type u_3} {E : α → Type u_4} [(i : α) → NormedAddCommGroup (E i)] {f : (i : α) → E i} (hf : {i : α | f i ≠ 0}.Finite) : Memℓp f 0

theorem memℓp_infty_iff {α : Type u_3} {E : α → Type u_4} [(i : α) → NormedAddCommGroup (E i)] {f : (i : α) → E i} : Memℓp f ⊤ ↔ BddAbove (Set.range fun (i : α) => ‖f i‖)

theorem memℓp_infty {α : Type u_3} {E : α → Type u_4} [(i : α) → NormedAddCommGroup (E i)] {f : (i : α) → E i} (hf : BddAbove (Set.range fun (i : α) => ‖f i‖)) : Memℓp f ⊤

theorem memℓp_gen_iff {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] (hp : 0 < p.toReal) {f : (i : α) → E i} : Memℓp f p ↔ Summable fun (i : α) => ‖f i‖ ^ p.toReal

theorem memℓp_gen {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {f : (i : α) → E i} (hf : Summable fun (i : α) => ‖f i‖ ^ p.toReal) : Memℓp f p

theorem memℓp_gen' {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {C : ℝ} {f : (i : α) → E i} (hf : ∀ (s : Finset α), ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C) : Memℓp f p

theorem memℓp_gen_iff' {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {f : (i : α) → E i} (hp : 0 < p.toReal) : Memℓp f p ↔ ∀ (s : Finset α), ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ ∑' (i : α), ‖f i‖ ^ p.toReal

theorem memℓp_gen_iff'' {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {f : (i : α) → E i} (hp : 0 < p.toReal) : Memℓp f p ↔ ∃ (C : ℝ), 0 ≤ C ∧ ∀ (s : Finset α), ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C

theorem zero_memℓp {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] : Memℓp 0 p

theorem zero_mem_ℓp' {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] : Memℓp (fun (i : α) => 0) p

theorem memℓp_norm_iff {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {f : (i : α) → E i} : Memℓp (fun (x : α) => ‖f x‖) p ↔ Memℓp f p

theorem Memℓp.norm {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {f : (i : α) → E i} : Memℓp f p → Memℓp (fun (x : α) => ‖f x‖) p

Alias of the reverse direction of memℓp_norm_iff.

theorem Memℓp.of_norm {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {f : (i : α) → E i} : Memℓp (fun (x : α) => ‖f x‖) p → Memℓp f p

Alias of the forward direction of memℓp_norm_iff.

theorem Memℓp.mono {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {f : (i : α) → E i} {g : α → ℝ} (hg : Memℓp g p) (hfg : ∀ (i : α), ‖f i‖ ≤ g i) : Memℓp f p

theorem Memℓp.mono' {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {F : α → Type u_5} [(i : α) → NormedAddCommGroup (F i)] {f : (i : α) → E i} {g : (i : α) → F i} (hg : Memℓp g p) (hfg : ∀ (i : α), ‖f i‖ ≤ ‖g i‖) : Memℓp f p

Often it is more convenient to use Memℓp.mono, where the bounding function is real-valued. This version is provable from that one using Memℓp.toNorm applied to the argument with type Memℓp g p.

theorem Memℓp.finite_dsupport {α : Type u_3} {E : α → Type u_4} [(i : α) → NormedAddCommGroup (E i)] {f : (i : α) → E i} (hf : Memℓp f 0) : {i : α | f i ≠ 0}.Finite

theorem Memℓp.bddAbove {α : Type u_3} {E : α → Type u_4} [(i : α) → NormedAddCommGroup (E i)] {f : (i : α) → E i} (hf : Memℓp f ⊤) : BddAbove (Set.range fun (i : α) => ‖f i‖)

theorem Memℓp.summable {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] (hp : 0 < p.toReal) {f : (i : α) → E i} (hf : Memℓp f p) : Summable fun (i : α) => ‖f i‖ ^ p.toReal

theorem Memℓp.summable_of_one {α : Type u_3} {E : Type u_5} [NormedAddCommGroup E] [CompleteSpace E] {x : α → E} (hx : Memℓp x 1) : Summable x

theorem Memℓp.neg {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {f : (i : α) → E i} (hf : Memℓp f p) : Memℓp (-f) p

@[simp]

theorem Memℓp.neg_iff {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {f : (i : α) → E i} : Memℓp (-f) p ↔ Memℓp f p

theorem Memℓp.of_exponent_ge {α : Type u_3} {E : α → Type u_4} [(i : α) → NormedAddCommGroup (E i)] {p q : ENNReal} {f : (i : α) → E i} (hfq : Memℓp f q) (hpq : q ≤ p) : Memℓp f p

theorem Memℓp.add {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (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_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (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_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {ι : Type u_5} (s : Finset ι) {f : ι → (i : α) → E i} (hf : ∀ i ∈ s, Memℓp (f i) p) : Memℓp (fun (a : α) => ∑ i ∈ s, f i a) p

theorem Memℓp.const_smul {𝕜 : Type u_1} {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [NormedRing 𝕜] [(i : α) → Module 𝕜 (E i)] [∀ (i : α), IsBoundedSMul 𝕜 (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} {α : Type u_3} {p : ENNReal} [NormedRing 𝕜] {f : α → 𝕜} (hf : Memℓp f p) (c : 𝕜) : Memℓp (fun (x : α) => c * f x) p

lp space

The space of elements of ∀ i, E i satisfying the predicate Memℓp.

def PreLp {α : Type u_3} (E : α → Type u_5) [(i : α) → NormedAddCommGroup (E i)] : Type (max u_3 u_5)

We define PreLp 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).

@[implicit_reducible]

noncomputable instance instAddCommGroupPreLp {α : Type u_1} (E : α → Type u_2) [(i : α) → NormedAddCommGroup (E i)] : AddCommGroup (PreLp E)

@[implicit_reducible]

instance PreLp.unique {α : Type u_3} {E : α → Type u_4} [(i : α) → NormedAddCommGroup (E i)] [IsEmpty α] : Unique (PreLp E)

def lp {α : Type u_3} (E : α → Type u_5) [(i : α) → NormedAddCommGroup (E i)] (p : ENNReal) : AddSubgroup (PreLp E)

The (little) ℓᵖ space: The additive subgroup of a type synonym of Π i, E i, which consists of those functions f such that Memℓp f p (i.e., f has finite p-norm).

The non-dependent version comes equipped with the notation ℓ^p(ι, E) in the lp namespace. When p takes the values 0, 1 or 2, the notation ℓ⁰(ι, E), ℓ¹(ι, E), ℓ²(ι, E) is also available.

def lp.«termℓ^_(_,_)» : Lean.ParserDescr

The (little) ℓᵖ space: The additive subgroup of a type synonym of Π i, E i, which consists of those functions f such that Memℓp f p (i.e., f has finite p-norm).

The non-dependent version comes equipped with the notation ℓ^p(ι, E) in the lp namespace. When p takes the values 0, 1 or 2, the notation ℓ⁰(ι, E), ℓ¹(ι, E), ℓ²(ι, E) is also available.

def lp.«termℓ⁰(_,_)» : Lean.ParserDescr

ℓ⁰(ι, E) is the space of finitely supported functions ι → E. In general, this should not be used outside of the context of ℓ^p(ι, E) spaces, and one should instead prefer Finsupp in other situations.

def lp.«termℓ¹(_,_)» : Lean.ParserDescr

ℓ¹(ι, E) is the space of summable functions ι → E. To be more precise, it is the space of functions whose norms are summable, but when E is complete these coincide.

def lp.«termℓ²(_,_)» : Lean.ParserDescr

ℓ²(ι, E) is the space of square-summable functions ι → E. When E := 𝕜, with RCLike 𝕜, this is a Hilbert space.

@[implicit_reducible]

instance lp.coeFun {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] : CoeFun ↥(lp E p) fun (x : ↥(lp E p)) => (i : α) → E i

theorem lp.ext {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {f g : ↥(lp E p)} (h : ↑f = ↑g) : f = g

theorem lp.ext_iff {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {f g : ↥(lp E p)} : f = g ↔ ↑f = ↑g

theorem lp.eq_zero' {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [IsEmpty α] (f : ↥(lp E p)) : f = 0

theorem lp.monotone {α : Type u_3} {E : α → Type u_4} [(i : α) → NormedAddCommGroup (E i)] {p q : ENNReal} (hpq : q ≤ p) : lp E q ≤ lp E p

theorem lp.memℓp {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] (f : ↥(lp E p)) : Memℓp (↑f) p

@[simp]

theorem lp.coeFn_zero {α : Type u_3} (E : α → Type u_4) (p : ENNReal) [(i : α) → NormedAddCommGroup (E i)] : ↑0 = 0

@[simp]

theorem lp.coeFn_neg {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] (f : ↥(lp E p)) : ↑(-f) = -↑f

@[simp]

theorem lp.coeFn_add {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] (f g : ↥(lp E p)) : ↑(f + g) = ↑f + ↑g

def lp.coeFnAddMonoidHom {α : Type u_3} (E : α → Type u_4) (p : ENNReal) [(i : α) → NormedAddCommGroup (E i)] : ↥(lp E p) →+ (i : α) → E i

Coercion to function as an AddMonoidHom.

@[simp]

theorem lp.coeFnAddMonoidHom_apply {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] (x : ↥(lp E p)) : (coeFnAddMonoidHom E p) x = ↑x

theorem lp.coeFn_sum {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {ι : Type u_5} (f : ι → ↥(lp E p)) (s : Finset ι) : ↑(∑ i ∈ s, f i) = ∑ i ∈ s, ↑(f i)

@[simp]

theorem lp.coeFn_sub {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] (f g : ↥(lp E p)) : ↑(f - g) = ↑f - ↑g

@[implicit_reducible]

noncomputable instance lp.instNormSubtypePreLpMemAddSubgroup {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] : Norm ↥(lp E p)

theorem lp.norm_eq_card_dsupport {α : Type u_3} {E : α → Type u_4} [(i : α) → NormedAddCommGroup (E i)] (f : ↥(lp E 0)) : ‖f‖ = ↑⋯.toFinset.card

theorem lp.norm_eq_ciSup {α : Type u_3} {E : α → Type u_4} [(i : α) → NormedAddCommGroup (E i)] (f : ↥(lp E ⊤)) : ‖f‖ = ⨆ (i : α), ‖↑f i‖

theorem lp.isLUB_norm {α : Type u_3} {E : α → Type u_4} [(i : α) → NormedAddCommGroup (E i)] [Nonempty α] (f : ↥(lp E ⊤)) : IsLUB (Set.range fun (i : α) => ‖↑f i‖) ‖f‖

theorem lp.norm_eq_tsum_rpow {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] (hp : 0 < p.toReal) (f : ↥(lp E p)) : ‖f‖ = (∑' (i : α), ‖↑f i‖ ^ p.toReal) ^ (1 / p.toReal)

theorem lp.norm_rpow_eq_tsum {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] (hp : 0 < p.toReal) (f : ↥(lp E p)) : ‖f‖ ^ p.toReal = ∑' (i : α), ‖↑f i‖ ^ p.toReal

theorem lp.hasSum_norm {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] (hp : 0 < p.toReal) (f : ↥(lp E p)) : HasSum (fun (i : α) => ‖↑f i‖ ^ p.toReal) (‖f‖ ^ p.toReal)

def lp.toNorm {α : Type u_3} {E : α → Type u_4} [(i : α) → NormedAddCommGroup (E i)] {p : ENNReal} (x : ↥(lp E p)) : ↥(lp (fun (x : α) => ℝ) p)

The sequence of norms of x : lp E p as a term of ℓ^p(α, ℝ). Here E : α → Type* is a dependent type and ℓ^p(α, ℝ) is the non-dependent ℝ-valued lp space.

@[simp]

theorem lp.toNorm_coe {α : Type u_3} {E : α → Type u_4} [(i : α) → NormedAddCommGroup (E i)] {p : ENNReal} (x : ↥(lp E p)) (i : α) : ↑(toNorm x) i = ‖↑x i‖

theorem lp.norm_toNorm {α : Type u_3} {E : α → Type u_4} [(i : α) → NormedAddCommGroup (E i)] {p : ENNReal} {x : ↥(lp E p)} : ‖toNorm x‖ = ‖x‖

theorem lp.norm_nonneg' {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] (f : ↥(lp E p)) : 0 ≤ ‖f‖

@[simp]

theorem lp.norm_zero {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] : ‖0‖ = 0

theorem lp.norm_eq_zero_iff {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {f : ↥(lp E p)} : ‖f‖ = 0 ↔ f = 0

theorem lp.eq_zero_iff_coeFn_eq_zero {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {f : ↥(lp E p)} : f = 0 ↔ ↑f = 0

@[simp]

theorem lp.norm_neg {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] ⦃f : ↥(lp E p)⦄ : ‖-f‖ = ‖f‖

@[implicit_reducible]

noncomputable instance lp.normedAddCommGroup {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [hp : Fact (1 ≤ p)] : NormedAddCommGroup ↥(lp E p)

theorem lp.tsum_mul_le_mul_norm {α : Type u_3} {E : α → Type u_4} [(i : α) → NormedAddCommGroup (E i)] {p q : ENNReal} (hpq : p.toReal.HolderConjugate q.toReal) (f : ↥(lp E p)) (g : ↥(lp E q)) : (Summable fun (i : α) => ‖↑f i‖ * ‖↑g i‖) ∧ ∑' (i : α), ‖↑f i‖ * ‖↑g i‖ ≤ ‖f‖ * ‖g‖

Hölder inequality

theorem lp.summable_mul {α : Type u_3} {E : α → Type u_4} [(i : α) → NormedAddCommGroup (E i)] {p q : ENNReal} (hpq : p.toReal.HolderConjugate q.toReal) (f : ↥(lp E p)) (g : ↥(lp E q)) : Summable fun (i : α) => ‖↑f i‖ * ‖↑g i‖

theorem lp.tsum_mul_le_mul_norm' {α : Type u_3} {E : α → Type u_4} [(i : α) → NormedAddCommGroup (E i)] {p q : ENNReal} (hpq : p.toReal.HolderConjugate q.toReal) (f : ↥(lp E p)) (g : ↥(lp E q)) : ∑' (i : α), ‖↑f i‖ * ‖↑g i‖ ≤ ‖f‖ * ‖g‖

theorem lp.norm_apply_le_norm {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] (hp : p ≠ 0) (f : ↥(lp E p)) (i : α) : ‖↑f i‖ ≤ ‖f‖

theorem lp.lipschitzWith_one_eval {α : Type u_3} {E : α → Type u_4} [(i : α) → NormedAddCommGroup (E i)] (p : ENNReal) [Fact (1 ≤ p)] (i : α) : LipschitzWith 1 fun (x : ↥(lp E p)) => ↑x i

theorem lp.sum_rpow_le_norm_rpow {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] (hp : 0 < p.toReal) (f : ↥(lp E p)) (s : Finset α) : ∑ i ∈ s, ‖↑f i‖ ^ p.toReal ≤ ‖f‖ ^ p.toReal

theorem lp.norm_le_of_forall_le' {α : Type u_3} {E : α → Type u_4} [(i : α) → NormedAddCommGroup (E i)] [Nonempty α] {f : ↥(lp E ⊤)} (C : ℝ) (hCf : ∀ (i : α), ‖↑f i‖ ≤ C) : ‖f‖ ≤ C

theorem lp.norm_le_of_forall_le {α : Type u_3} {E : α → Type u_4} [(i : α) → NormedAddCommGroup (E i)] {f : ↥(lp E ⊤)} {C : ℝ} (hC : 0 ≤ C) (hCf : ∀ (i : α), ‖↑f i‖ ≤ C) : ‖f‖ ≤ C

theorem lp.norm_le_of_tsum_le {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] (hp : 0 < p.toReal) {C : ℝ} (hC : 0 ≤ C) {f : ↥(lp E p)} (hf : ∑' (i : α), ‖↑f i‖ ^ p.toReal ≤ C ^ p.toReal) : ‖f‖ ≤ C

theorem lp.norm_le_of_forall_sum_le {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] (hp : 0 < p.toReal) {C : ℝ} (hC : 0 ≤ C) {f : ↥(lp E p)} (hf : ∀ (s : Finset α), ∑ i ∈ s, ‖↑f i‖ ^ p.toReal ≤ C ^ p.toReal) : ‖f‖ ≤ C

theorem lp.norm_mono {α : Type u_3} {E : α → Type u_4} [(i : α) → NormedAddCommGroup (E i)] {F : α → Type u_5} [(i : α) → NormedAddCommGroup (F i)] {p : ENNReal} (hp : p ≠ 0) {x : ↥(lp E p)} {y : ↥(lp F p)} (h : ∀ (i : α), ‖↑x i‖ ≤ ‖↑y i‖) : ‖x‖ ≤ ‖y‖

@[implicit_reducible]

instance lp.instModulePreLp {𝕜 : Type u_1} {α : Type u_3} {E : α → Type u_4} [(i : α) → NormedAddCommGroup (E i)] [NormedRing 𝕜] [(i : α) → Module 𝕜 (E i)] : Module 𝕜 (PreLp E)

instance lp.instSMulCommClassPreLp {𝕜 : Type u_1} {𝕜' : Type u_2} {α : Type u_3} {E : α → Type u_4} [(i : α) → NormedAddCommGroup (E i)] [NormedRing 𝕜] [NormedRing 𝕜'] [(i : α) → Module 𝕜 (E i)] [(i : α) → Module 𝕜' (E i)] [∀ (i : α), SMulCommClass 𝕜' 𝕜 (E i)] : SMulCommClass 𝕜' 𝕜 (PreLp E)

instance lp.instIsScalarTowerPreLp {𝕜 : Type u_1} {𝕜' : Type u_2} {α : Type u_3} {E : α → Type u_4} [(i : α) → NormedAddCommGroup (E i)] [NormedRing 𝕜] [NormedRing 𝕜'] [(i : α) → Module 𝕜 (E i)] [(i : α) → Module 𝕜' (E i)] [SMul 𝕜' 𝕜] [∀ (i : α), IsScalarTower 𝕜' 𝕜 (E i)] : IsScalarTower 𝕜' 𝕜 (PreLp E)

instance lp.instIsCentralScalarPreLp {𝕜 : Type u_1} {α : Type u_3} {E : α → Type u_4} [(i : α) → NormedAddCommGroup (E i)] [NormedRing 𝕜] [(i : α) → Module 𝕜 (E i)] [(i : α) → Module 𝕜ᵐᵒᵖ (E i)] [∀ (i : α), IsCentralScalar 𝕜 (E i)] : IsCentralScalar 𝕜 (PreLp E)

theorem lp.mem_lp_const_smul {𝕜 : Type u_1} {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [NormedRing 𝕜] [(i : α) → Module 𝕜 (E i)] [∀ (i : α), IsBoundedSMul 𝕜 (E i)] (c : 𝕜) (f : ↥(lp E p)) : c • ↑f ∈ lp E p

def lpSubmodule (𝕜 : Type u_1) {α : Type u_3} (E : α → Type u_4) (p : ENNReal) [(i : α) → NormedAddCommGroup (E i)] [NormedRing 𝕜] [(i : α) → Module 𝕜 (E i)] [∀ (i : α), IsBoundedSMul 𝕜 (E i)] : Submodule 𝕜 (PreLp E)

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

theorem lp.coe_lpSubmodule {𝕜 : Type u_1} {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [NormedRing 𝕜] [(i : α) → Module 𝕜 (E i)] [∀ (i : α), IsBoundedSMul 𝕜 (E i)] : (lpSubmodule 𝕜 E p).toAddSubgroup = lp E p

@[implicit_reducible]

noncomputable instance lp.instModuleSubtypePreLpMemAddSubgroup {𝕜 : Type u_1} {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [NormedRing 𝕜] [(i : α) → Module 𝕜 (E i)] [∀ (i : α), IsBoundedSMul 𝕜 (E i)] : Module 𝕜 ↥(lp E p)

@[simp]

theorem lp.coeFn_smul {𝕜 : Type u_1} {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [NormedRing 𝕜] [(i : α) → Module 𝕜 (E i)] [∀ (i : α), IsBoundedSMul 𝕜 (E i)] (c : 𝕜) (f : ↥(lp E p)) : ↑(c • f) = c • ↑f

instance lp.instSMulCommClassSubtypePreLpMemAddSubgroup {𝕜 : Type u_1} {𝕜' : Type u_2} {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [NormedRing 𝕜] [NormedRing 𝕜'] [(i : α) → Module 𝕜 (E i)] [(i : α) → Module 𝕜' (E i)] [∀ (i : α), IsBoundedSMul 𝕜 (E i)] [∀ (i : α), IsBoundedSMul 𝕜' (E i)] [∀ (i : α), SMulCommClass 𝕜' 𝕜 (E i)] : SMulCommClass 𝕜' 𝕜 ↥(lp E p)

instance lp.instIsScalarTowerSubtypePreLpMemAddSubgroup {𝕜 : Type u_1} {𝕜' : Type u_2} {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [NormedRing 𝕜] [NormedRing 𝕜'] [(i : α) → Module 𝕜 (E i)] [(i : α) → Module 𝕜' (E i)] [∀ (i : α), IsBoundedSMul 𝕜 (E i)] [∀ (i : α), IsBoundedSMul 𝕜' (E i)] [SMul 𝕜' 𝕜] [∀ (i : α), IsScalarTower 𝕜' 𝕜 (E i)] : IsScalarTower 𝕜' 𝕜 ↥(lp E p)

instance lp.instIsCentralScalarSubtypePreLpMemAddSubgroup {𝕜 : Type u_1} {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [NormedRing 𝕜] [(i : α) → Module 𝕜 (E i)] [∀ (i : α), IsBoundedSMul 𝕜 (E i)] [(i : α) → Module 𝕜ᵐᵒᵖ (E i)] [∀ (i : α), IsCentralScalar 𝕜 (E i)] : IsCentralScalar 𝕜 ↥(lp E p)

theorem lp.norm_const_smul_le {𝕜 : Type u_1} {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [NormedRing 𝕜] [(i : α) → Module 𝕜 (E i)] [∀ (i : α), IsBoundedSMul 𝕜 (E i)] (hp : p ≠ 0) (c : 𝕜) (f : ↥(lp E p)) : ‖c • f‖ ≤ ‖c‖ * ‖f‖

instance lp.instIsBoundedSMulSubtypePreLpMemAddSubgroup {𝕜 : Type u_1} {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [NormedRing 𝕜] [(i : α) → Module 𝕜 (E i)] [∀ (i : α), IsBoundedSMul 𝕜 (E i)] [Fact (1 ≤ p)] : IsBoundedSMul 𝕜 ↥(lp E p)

theorem lp.norm_tsum_le {α : Type u_3} {E : Type u_5} [NormedAddCommGroup E] (f : ↥(lp (fun (x : α) => E) 1)) : ‖∑' (i : α), ↑f i‖ ≤ ‖f‖

noncomputable def lp.tsumCLM (𝕜 : Type u_1) (α : Type u_3) (E : Type u_5) [NormedAddCommGroup E] [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] [CompleteSpace E] : ↥(lp (fun (x : α) => E) 1) →L[𝕜] E

Summation (i.e., tsum) in ℓ¹(α, E) as a continuous linear map.

@[simp]

theorem lp.tsumCLM_apply (𝕜 : Type u_1) (α : Type u_3) (E : Type u_5) [NormedAddCommGroup E] [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] [CompleteSpace E] (f : ↥(lp (fun (x : α) => E) 1)) : (tsumCLM 𝕜 α E) f = ∑' (i : α), ↑f i

theorem lp.norm_const_smul {𝕜 : Type u_1} {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [NormedDivisionRing 𝕜] [(i : α) → Module 𝕜 (E i)] [∀ (i : α), IsBoundedSMul 𝕜 (E i)] (hp : p ≠ 0) {c : 𝕜} (f : ↥(lp E p)) : ‖c • f‖ = ‖c‖ * ‖f‖

@[implicit_reducible]

noncomputable instance lp.instNormedSpace {𝕜 : Type u_1} {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [NormedField 𝕜] [(i : α) → NormedSpace 𝕜 (E i)] [Fact (1 ≤ p)] : NormedSpace 𝕜 ↥(lp E p)

theorem Memℓp.star_mem {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [(i : α) → StarAddMonoid (E i)] [∀ (i : α), NormedStarGroup (E i)] {f : (i : α) → E i} (hf : Memℓp f p) : Memℓp (star f) p

@[simp]

theorem Memℓp.star_iff {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [(i : α) → StarAddMonoid (E i)] [∀ (i : α), NormedStarGroup (E i)] {f : (i : α) → E i} : Memℓp (star f) p ↔ Memℓp f p

@[implicit_reducible]

instance lp.instStarSubtypePreLpMemAddSubgroup {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [(i : α) → StarAddMonoid (E i)] [∀ (i : α), NormedStarGroup (E i)] : Star ↥(lp E p)

@[simp]

theorem lp.coeFn_star {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [(i : α) → StarAddMonoid (E i)] [∀ (i : α), NormedStarGroup (E i)] (f : ↥(lp E p)) : ↑(star f) = star ↑f

@[simp]

theorem lp.star_apply {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [(i : α) → StarAddMonoid (E i)] [∀ (i : α), NormedStarGroup (E i)] (f : ↥(lp E p)) (i : α) : ↑(star f) i = star (↑f i)

@[implicit_reducible]

instance lp.instInvolutiveStar {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [(i : α) → StarAddMonoid (E i)] [∀ (i : α), NormedStarGroup (E i)] : InvolutiveStar ↥(lp E p)

@[implicit_reducible]

instance lp.instStarAddMonoid {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [(i : α) → StarAddMonoid (E i)] [∀ (i : α), NormedStarGroup (E i)] : StarAddMonoid ↥(lp E p)

instance lp.instNormedStarGroupSubtypePreLpMemAddSubgroup {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [(i : α) → StarAddMonoid (E i)] [∀ (i : α), NormedStarGroup (E i)] [hp : Fact (1 ≤ p)] : NormedStarGroup ↥(lp E p)

instance lp.instStarModuleSubtypePreLpMemAddSubgroup {𝕜 : Type u_1} {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [(i : α) → StarAddMonoid (E i)] [∀ (i : α), NormedStarGroup (E i)] [Star 𝕜] [NormedRing 𝕜] [(i : α) → Module 𝕜 (E i)] [∀ (i : α), IsBoundedSMul 𝕜 (E i)] [∀ (i : α), StarModule 𝕜 (E i)] : StarModule 𝕜 ↥(lp E p)

theorem Memℓp.infty_mul {I : Type u_5} {B : I → Type u_6} [(i : I) → NonUnitalNormedRing (B i)] {f g : (i : I) → B i} (hf : Memℓp f ⊤) (hg : Memℓp g ⊤) : Memℓp (f * g) ⊤

@[implicit_reducible]

instance lp.instMulSubtypePreLpMemAddSubgroupTopENNReal {I : Type u_5} {B : I → Type u_6} [(i : I) → NonUnitalNormedRing (B i)] : Mul ↥(lp B ⊤)

@[simp]

theorem lp.infty_coeFn_mul {I : Type u_5} {B : I → Type u_6} [(i : I) → NonUnitalNormedRing (B i)] (f g : ↥(lp B ⊤)) : ↑(f * g) = ↑f * ↑g

@[implicit_reducible]

noncomputable instance lp.nonUnitalRing {I : Type u_5} {B : I → Type u_6} [(i : I) → NonUnitalNormedRing (B i)] : NonUnitalRing ↥(lp B ⊤)

@[implicit_reducible]

noncomputable instance lp.nonUnitalNormedRing {I : Type u_5} {B : I → Type u_6} [(i : I) → NonUnitalNormedRing (B i)] : NonUnitalNormedRing ↥(lp B ⊤)

@[implicit_reducible]

noncomputable instance lp.nonUnitalNormedCommRing {I : Type u_5} {B : I → Type u_7} [(i : I) → NonUnitalNormedCommRing (B i)] : NonUnitalNormedCommRing ↥(lp B ⊤)

instance lp.infty_isScalarTower {I : Type u_5} {B : I → Type u_6} [(i : I) → NonUnitalNormedRing (B i)] {𝕜 : Type u_7} [NormedRing 𝕜] [(i : I) → Module 𝕜 (B i)] [∀ (i : I), IsBoundedSMul 𝕜 (B i)] [∀ (i : I), IsScalarTower 𝕜 (B i) (B i)] : IsScalarTower 𝕜 ↥(lp B ⊤) ↥(lp B ⊤)

instance lp.infty_smulCommClass {I : Type u_5} {B : I → Type u_6} [(i : I) → NonUnitalNormedRing (B i)] {𝕜 : Type u_7} [NormedRing 𝕜] [(i : I) → Module 𝕜 (B i)] [∀ (i : I), IsBoundedSMul 𝕜 (B i)] [∀ (i : I), SMulCommClass 𝕜 (B i) (B i)] : SMulCommClass 𝕜 ↥(lp B ⊤) ↥(lp B ⊤)

@[implicit_reducible]

instance lp.inftyStarRing {I : Type u_5} {B : I → Type u_6} [(i : I) → NonUnitalNormedRing (B i)] [(i : I) → StarRing (B i)] [∀ (i : I), NormedStarGroup (B i)] : StarRing ↥(lp B ⊤)

instance lp.inftyCStarRing {I : Type u_5} {B : I → Type u_6} [(i : I) → NonUnitalNormedRing (B i)] [(i : I) → StarRing (B i)] [∀ (i : I), NormedStarGroup (B i)] [∀ (i : I), CStarRing (B i)] : CStarRing ↥(lp B ⊤)

@[implicit_reducible]

noncomputable instance PreLp.ring {I : Type u_5} {B : I → Type u_6} [(i : I) → NormedRing (B i)] : Ring (PreLp B)

theorem one_memℓp_infty {I : Type u_5} {B : I → Type u_6} [(i : I) → NormedRing (B i)] [∀ (i : I), NormOneClass (B i)] : Memℓp 1 ⊤

def lpInftySubring {I : Type u_5} (B : I → Type u_6) [(i : I) → NormedRing (B i)] [∀ (i : I), NormOneClass (B i)] : Subring (PreLp B)

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

@[implicit_reducible]

noncomputable instance lp.inftyRing {I : Type u_5} {B : I → Type u_6} [(i : I) → NormedRing (B i)] [∀ (i : I), NormOneClass (B i)] : Ring ↥(lp B ⊤)

theorem Memℓp.infty_pow {I : Type u_5} {B : I → Type u_6} [(i : I) → NormedRing (B i)] [∀ (i : I), NormOneClass (B i)] {f : (i : I) → B i} (hf : Memℓp f ⊤) (n : ℕ) : Memℓp (f ^ n) ⊤

theorem natCast_memℓp_infty {I : Type u_5} {B : I → Type u_6} [(i : I) → NormedRing (B i)] [∀ (i : I), NormOneClass (B i)] (n : ℕ) : Memℓp ↑n ⊤

theorem intCast_memℓp_infty {I : Type u_5} {B : I → Type u_6} [(i : I) → NormedRing (B i)] [∀ (i : I), NormOneClass (B i)] (z : ℤ) : Memℓp ↑z ⊤

@[simp]

theorem lp.infty_coeFn_one {I : Type u_5} {B : I → Type u_6} [(i : I) → NormedRing (B i)] [∀ (i : I), NormOneClass (B i)] : ↑1 = 1

@[simp]

theorem lp.infty_coeFn_pow {I : Type u_5} {B : I → Type u_6} [(i : I) → NormedRing (B i)] [∀ (i : I), NormOneClass (B i)] (f : ↥(lp B ⊤)) (n : ℕ) : ↑(f ^ n) = ↑f ^ n

@[simp]

theorem lp.infty_coeFn_natCast {I : Type u_5} {B : I → Type u_6} [(i : I) → NormedRing (B i)] [∀ (i : I), NormOneClass (B i)] (n : ℕ) : ↑↑n = ↑n

@[simp]

theorem lp.infty_coeFn_intCast {I : Type u_5} {B : I → Type u_6} [(i : I) → NormedRing (B i)] [∀ (i : I), NormOneClass (B i)] (z : ℤ) : ↑↑z = ↑z

instance lp.instNormOneClassSubtypePreLpMemAddSubgroupTopENNRealOfNonempty {I : Type u_5} {B : I → Type u_6} [(i : I) → NormedRing (B i)] [∀ (i : I), NormOneClass (B i)] [Nonempty I] : NormOneClass ↥(lp B ⊤)

@[implicit_reducible]

noncomputable instance lp.inftyNormedRing {I : Type u_5} {B : I → Type u_6} [(i : I) → NormedRing (B i)] [∀ (i : I), NormOneClass (B i)] : NormedRing ↥(lp B ⊤)

@[implicit_reducible]

noncomputable instance lp.inftyNormedCommRing {I : Type u_5} {B : I → Type u_6} [(i : I) → NormedCommRing (B i)] [∀ (i : I), NormOneClass (B i)] : NormedCommRing ↥(lp B ⊤)

@[implicit_reducible]

instance PreLp.algebra {𝕜 : Type u_1} {I : Type u_5} {B : I → Type u_6} [NormedField 𝕜] [(i : I) → NormedRing (B i)] [(i : I) → NormedAlgebra 𝕜 (B i)] : Algebra 𝕜 (PreLp B)

theorem algebraMap_memℓp_infty {𝕜 : Type u_1} {I : Type u_5} {B : I → Type u_6} [NormedField 𝕜] [(i : I) → NormedRing (B i)] [(i : I) → NormedAlgebra 𝕜 (B i)] [∀ (i : I), NormOneClass (B i)] (k : 𝕜) : Memℓp ((algebraMap 𝕜 ((i : I) → B i)) k) ⊤

def lpInftySubalgebra (𝕜 : Type u_1) {I : Type u_5} (B : I → Type u_6) [NormedField 𝕜] [(i : I) → NormedRing (B i)] [(i : I) → NormedAlgebra 𝕜 (B i)] [∀ (i : I), NormOneClass (B i)] : Subalgebra 𝕜 (PreLp B)

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

@[implicit_reducible]

noncomputable instance lp.instAlgebraSubtypePreLpMemAddSubgroupTopENNReal {𝕜 : Type u_1} {I : Type u_5} {B : I → Type u_6} [NormedField 𝕜] [(i : I) → NormedRing (B i)] [(i : I) → NormedAlgebra 𝕜 (B i)] [∀ (i : I), NormOneClass (B i)] : Algebra 𝕜 ↥(lp B ⊤)

@[implicit_reducible]

noncomputable instance lp.inftyNormedAlgebra {𝕜 : Type u_1} {I : Type u_5} {B : I → Type u_6} [NormedField 𝕜] [(i : I) → NormedRing (B i)] [(i : I) → NormedAlgebra 𝕜 (B i)] [∀ (i : I), NormOneClass (B i)] : NormedAlgebra 𝕜 ↥(lp B ⊤)

def lp.single {α : Type u_3} {E : α → Type u_4} [(i : α) → NormedAddCommGroup (E i)] [DecidableEq α] (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.

theorem lp.coeFn_single {α : Type u_3} {E : α → Type u_4} [(i : α) → NormedAddCommGroup (E i)] [DecidableEq α] (p : ENNReal) (i : α) (a : E i) : ↑(lp.single p i a) = Pi.single i a

@[simp]

theorem lp.single_apply {α : Type u_3} {E : α → Type u_4} [(i : α) → NormedAddCommGroup (E i)] [DecidableEq α] (p : ENNReal) (i : α) (a : E i) (j : α) : ↑(lp.single p i a) j = Pi.single i a j

theorem lp.single_apply_self {α : Type u_3} {E : α → Type u_4} [(i : α) → NormedAddCommGroup (E i)] [DecidableEq α] (p : ENNReal) (i : α) (a : E i) : ↑(lp.single p i a) i = a

theorem lp.single_apply_ne {α : Type u_3} {E : α → Type u_4} [(i : α) → NormedAddCommGroup (E i)] [DecidableEq α] (p : ENNReal) (i : α) (a : E i) {j : α} (hij : j ≠ i) : ↑(lp.single p i a) j = 0

@[simp]

theorem lp.single_zero {α : Type u_3} {E : α → Type u_4} [(i : α) → NormedAddCommGroup (E i)] [DecidableEq α] (p : ENNReal) (i : α) : lp.single p i 0 = 0

@[simp]

theorem lp.single_add {α : Type u_3} {E : α → Type u_4} [(i : α) → NormedAddCommGroup (E i)] [DecidableEq α] (p : ENNReal) (i : α) (a b : E i) : lp.single p i (a + b) = lp.single p i a + lp.single p i b

def lp.singleAddMonoidHom {α : Type u_3} {E : α → Type u_4} [(i : α) → NormedAddCommGroup (E i)] [DecidableEq α] (p : ENNReal) (i : α) : E i →+ ↥(lp E p)

single as an AddMonoidHom.

@[simp]

theorem lp.singleAddMonoidHom_apply {α : Type u_3} {E : α → Type u_4} [(i : α) → NormedAddCommGroup (E i)] [DecidableEq α] (p : ENNReal) (i : α) (a : E i) : (singleAddMonoidHom p i) a = lp.single p i a

@[simp]

theorem lp.single_neg {α : Type u_3} {E : α → Type u_4} [(i : α) → NormedAddCommGroup (E i)] [DecidableEq α] (p : ENNReal) (i : α) (a : E i) : lp.single p i (-a) = -lp.single p i a

@[simp]

theorem lp.single_sub {α : Type u_3} {E : α → Type u_4} [(i : α) → NormedAddCommGroup (E i)] [DecidableEq α] (p : ENNReal) (i : α) (a b : E i) : lp.single p i (a - b) = lp.single p i a - lp.single p i b

@[simp]

theorem lp.single_smul {𝕜 : Type u_1} {α : Type u_3} {E : α → Type u_4} [(i : α) → NormedAddCommGroup (E i)] [NormedRing 𝕜] [(i : α) → Module 𝕜 (E i)] [∀ (i : α), IsBoundedSMul 𝕜 (E i)] [DecidableEq α] (p : ENNReal) (i : α) (c : 𝕜) (a : E i) : lp.single p i (c • a) = c • lp.single p i a

def lp.lsingle {𝕜 : Type u_1} {α : Type u_3} {E : α → Type u_4} [(i : α) → NormedAddCommGroup (E i)] [NormedRing 𝕜] [(i : α) → Module 𝕜 (E i)] [∀ (i : α), IsBoundedSMul 𝕜 (E i)] [DecidableEq α] (p : ENNReal) (i : α) : E i →ₗ[𝕜] ↥(lp E p)

single as a LinearMap.

@[simp]

theorem lp.lsingle_apply {𝕜 : Type u_1} {α : Type u_3} {E : α → Type u_4} [(i : α) → NormedAddCommGroup (E i)] [NormedRing 𝕜] [(i : α) → Module 𝕜 (E i)] [∀ (i : α), IsBoundedSMul 𝕜 (E i)] [DecidableEq α] (p : ENNReal) (i : α) (a : E i) : (lsingle p i) a = lp.single p i a

noncomputable def lp.zeroBasis {𝕜 : Type u_1} {α : Type u_3} [NormedRing 𝕜] : Module.Basis α 𝕜 ↥(lp (fun (x : α) => 𝕜) 0)

The basis for ℓ⁰(α, 𝕜) given by lp.single.

@[simp]

theorem lp.zeroBasis_repr_apply {𝕜 : Type u_1} {α : Type u_3} [NormedRing 𝕜] (x : ↥(lp (fun (x : α) => 𝕜) 0)) : zeroBasis.repr x = Finsupp.ofSupportFinite ↑x ⋯

@[simp]

theorem lp.zeroBasis_repr_symm_apply_coe {𝕜 : Type u_1} {α : Type u_3} [NormedRing 𝕜] (x : α →₀ 𝕜) (a : α) : ↑(zeroBasis.repr.symm x) a = x a

theorem lp.zeroBasis_apply {𝕜 : Type u_1} {α : Type u_3} [NormedRing 𝕜] [DecidableEq α] (i : α) : zeroBasis i = lp.single 0 i 1

theorem lp.norm_sum_single {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [DecidableEq α] (hp : 0 < p.toReal) (f : (i : α) → E i) (s : Finset α) : ‖∑ i ∈ s, lp.single p i (f i)‖ ^ p.toReal = ∑ i ∈ s, ‖f i‖ ^ p.toReal

@[simp]

theorem lp.norm_single {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [DecidableEq α] (hp : 0 < p) (i : α) (x : E i) : ‖lp.single p i x‖ = ‖x‖

theorem lp.isometry_single {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [DecidableEq α] [Fact (1 ≤ p)] (i : α) : Isometry (lp.single p i)

def lp.singleContinuousAddMonoidHom {α : Type u_3} (E : α → Type u_4) (p : ENNReal) [(i : α) → NormedAddCommGroup (E i)] [DecidableEq α] [Fact (1 ≤ p)] (i : α) : E i →ₜ+ ↥(lp E p)

lp.single as a continuous morphism of additive monoids.

@[simp]

theorem lp.singleContinuousAddMonoidHom_apply {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [DecidableEq α] [Fact (1 ≤ p)] (i : α) (x : E i) : (singleContinuousAddMonoidHom E p i) x = lp.single p i x

def lp.singleContinuousLinearMap (𝕜 : Type u_1) {α : Type u_3} (E : α → Type u_4) (p : ENNReal) [(i : α) → NormedAddCommGroup (E i)] [NormedRing 𝕜] [(i : α) → Module 𝕜 (E i)] [∀ (i : α), IsBoundedSMul 𝕜 (E i)] [DecidableEq α] [Fact (1 ≤ p)] (i : α) : E i →L[𝕜] ↥(lp E p)

lp.single as a continuous linear map.

@[simp]

theorem lp.singleContinuousLinearMap_apply {𝕜 : Type u_1} {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [NormedRing 𝕜] [(i : α) → Module 𝕜 (E i)] [∀ (i : α), IsBoundedSMul 𝕜 (E i)] [DecidableEq α] [Fact (1 ≤ p)] (i : α) (x : E i) : (singleContinuousLinearMap 𝕜 E p i) x = lp.single p i x

theorem lp.norm_sub_norm_compl_sub_single {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [DecidableEq α] (hp : 0 < p.toReal) (f : ↥(lp E p)) (s : Finset α) : ‖f‖ ^ p.toReal - ‖f - ∑ i ∈ s, lp.single p i (↑f i)‖ ^ p.toReal = ∑ i ∈ s, ‖↑f i‖ ^ p.toReal

theorem lp.norm_compl_sum_single {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [DecidableEq α] (hp : 0 < p.toReal) (f : ↥(lp E p)) (s : Finset α) : ‖f - ∑ i ∈ s, lp.single p i (↑f i)‖ ^ p.toReal = ‖f‖ ^ p.toReal - ∑ i ∈ s, ‖↑f i‖ ^ p.toReal

theorem lp.hasSum_single {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [DecidableEq α] [Fact (1 ≤ p)] (hp : p ≠ ⊤) (f : ↥(lp E p)) : HasSum (fun (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.ext_continuousAddMonoidHom {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [DecidableEq α] {F : Type u_5} [AddCommMonoid F] [TopologicalSpace F] [T2Space F] [Fact (1 ≤ p)] (hp : p ≠ ⊤) ⦃f g : ↥(lp E p) →ₜ+ F⦄ (h : ∀ (i : α), f.comp (singleContinuousAddMonoidHom E p i) = g.comp (singleContinuousAddMonoidHom E p i)) : f = g

Two continuous additive maps from lp E p agree if they agree on lp.single.

See note [partially-applied ext lemmas].

theorem lp.ext_continuousAddMonoidHom_iff {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [DecidableEq α] {F : Type u_5} [AddCommMonoid F] [TopologicalSpace F] [T2Space F] [Fact (1 ≤ p)] {hp : p ≠ ⊤} {f g : ↥(lp E p) →ₜ+ F} : f = g ↔ ∀ (i : α), f.comp (singleContinuousAddMonoidHom E p i) = g.comp (singleContinuousAddMonoidHom E p i)

theorem lp.ext_continuousLinearMap {𝕜 : Type u_1} {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [NormedRing 𝕜] [(i : α) → Module 𝕜 (E i)] [∀ (i : α), IsBoundedSMul 𝕜 (E i)] [DecidableEq α] {F : Type u_5} [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F] [T2Space F] [Fact (1 ≤ p)] (hp : p ≠ ⊤) ⦃f g : ↥(lp E p) →L[𝕜] F⦄ (h : ∀ (i : α), f.comp (singleContinuousLinearMap 𝕜 E p i) = g.comp (singleContinuousLinearMap 𝕜 E p i)) : f = g

Two continuous linear maps from lp E p agree if they agree on lp.single.

See note [partially-applied ext lemmas].

theorem lp.ext_continuousLinearMap_iff {𝕜 : Type u_1} {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [NormedRing 𝕜] [(i : α) → Module 𝕜 (E i)] [∀ (i : α), IsBoundedSMul 𝕜 (E i)] [DecidableEq α] {F : Type u_5} [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F] [T2Space F] [Fact (1 ≤ p)] {hp : p ≠ ⊤} {f g : ↥(lp E p) →L[𝕜] F} : f = g ↔ ∀ (i : α), f.comp (singleContinuousLinearMap 𝕜 E p i) = g.comp (singleContinuousLinearMap 𝕜 E p i)

def lp.linearMapOfLE (𝕜 : Type u_1) {α : Type u_3} (E : α → Type u_4) [(i : α) → NormedAddCommGroup (E i)] [NormedRing 𝕜] [(i : α) → Module 𝕜 (E i)] [∀ (i : α), IsBoundedSMul 𝕜 (E i)] {p q : ENNReal} (h : p ≤ q) : ↥(lp E p) →ₗ[𝕜] ↥(lp E q)

The AddSubgroup.inclusion between lp spaces, as a linear map.

@[simp]

theorem lp.coe_linearMapOfLE_apply {𝕜 : Type u_1} {α : Type u_3} {E : α → Type u_4} [(i : α) → NormedAddCommGroup (E i)] [NormedRing 𝕜] [(i : α) → Module 𝕜 (E i)] [∀ (i : α), IsBoundedSMul 𝕜 (E i)] {p q : ENNReal} (h : p ≤ q) (f : ↥(lp E p)) : ↑((linearMapOfLE 𝕜 E h) f) = ↑f

@[simp]

theorem lp.toAddMonoidHom_linearMapOfLE {𝕜 : Type u_1} {α : Type u_3} {E : α → Type u_4} [(i : α) → NormedAddCommGroup (E i)] [NormedRing 𝕜] [(i : α) → Module 𝕜 (E i)] [∀ (i : α), IsBoundedSMul 𝕜 (E i)] {p q : ENNReal} (h : p ≤ q) : (linearMapOfLE 𝕜 E h).toAddMonoidHom = AddSubgroup.inclusion ⋯

theorem lp.linearMapOfLE_comp {𝕜 : Type u_1} {α : Type u_3} {E : α → Type u_4} [(i : α) → NormedAddCommGroup (E i)] [NormedRing 𝕜] [(i : α) → Module 𝕜 (E i)] [∀ (i : α), IsBoundedSMul 𝕜 (E i)] {p q r : ENNReal} (hpq : p ≤ q) (hqr : q ≤ r) : linearMapOfLE 𝕜 E hqr ∘ₗ linearMapOfLE 𝕜 E hpq = linearMapOfLE 𝕜 E ⋯

def lp.evalₗ {𝕜 : Type u_1} {α : Type u_3} (E : α → Type u_4) [(i : α) → NormedAddCommGroup (E i)] [NormedRing 𝕜] [(i : α) → Module 𝕜 (E i)] [∀ (i : α), IsBoundedSMul 𝕜 (E i)] (p : ENNReal) (i : α) : ↥(lp E p) →ₗ[𝕜] E i

Evaluation at a single coordinate, as a linear map on lp E p.

@[simp]

theorem lp.evalₗ_apply {𝕜 : Type u_1} {α : Type u_3} (E : α → Type u_4) [(i : α) → NormedAddCommGroup (E i)] [NormedRing 𝕜] [(i : α) → Module 𝕜 (E i)] [∀ (i : α), IsBoundedSMul 𝕜 (E i)] (p : ENNReal) (i : α) (f : ↥(lp E p)) : (evalₗ E p i) f = ↑f i

noncomputable def lp.evalCLM (𝕜 : Type u_1) {α : Type u_3} (E : α → Type u_4) [(i : α) → NormedAddCommGroup (E i)] [NormedRing 𝕜] [(i : α) → Module 𝕜 (E i)] [∀ (i : α), IsBoundedSMul 𝕜 (E i)] (p : ENNReal) [Fact (1 ≤ p)] (i : α) : ↥(lp E p) →L[𝕜] E i

Evaluation at a single coordinate, as a continuous linear map on lp E p.

theorem lp.uniformContinuous_coe {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [_i : Fact (1 ≤ p)] : UniformContinuous Subtype.val

The coercion from lp E p to ∀ i, E i is uniformly continuous.

theorem lp.norm_apply_le_of_tendsto {α : Type u_3} {E : α → Type u_4} [(i : α) → NormedAddCommGroup (E i)] {ι : Type u_5} {l : Filter ι} [l.NeBot] {C : ℝ} {F : ι → ↥(lp E ⊤)} (hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C) {f : (a : α) → E a} (hf : Filter.Tendsto (id fun (i : ι) => ↑(F i)) l (nhds f)) (a : α) : ‖f a‖ ≤ C

theorem lp.sum_rpow_le_of_tendsto {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {ι : Type u_5} {l : Filter ι} [l.NeBot] [_i : 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 fun (i : ι) => ↑(F i)) l (nhds f)) (s : Finset α) : ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C ^ p.toReal

theorem lp.norm_le_of_tendsto {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {ι : Type u_5} {l : Filter ι} [l.NeBot] [_i : Fact (1 ≤ p)] {C : ℝ} {F : ι → ↥(lp E p)} (hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C) {f : ↥(lp E p)} (hf : Filter.Tendsto (id fun (i : ι) => ↑(F i)) l (nhds ↑f)) : ‖f‖ ≤ C

"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_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {ι : Type u_5} {l : Filter ι} [l.NeBot] [_i : Fact (1 ≤ p)] {F : ι → ↥(lp E p)} (hF : Bornology.IsBounded (Set.range F)) {f : (a : α) → E a} (hf : Filter.Tendsto (id fun (i : ι) => ↑(F i)) l (nhds f)) : Memℓp f p

If f is the pointwise limit of a bounded sequence in lp E p, then f is in lp E p.

theorem lp.tendsto_lp_of_tendsto_pi {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [_i : Fact (1 ≤ p)] {F : ℕ → ↥(lp E p)} (hF : CauchySeq F) {f : ↥(lp E p)} (hf : Filter.Tendsto (id fun (i : ℕ) => ↑(F i)) Filter.atTop (nhds ↑f)) : Filter.Tendsto F Filter.atTop (nhds f)

If a sequence is Cauchy in the lp E p topology and pointwise convergent to an element f of lp E p, then it converges to f in the lp E p topology.

instance lp.completeSpace {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [_i : Fact (1 ≤ p)] [∀ (a : α), CompleteSpace (E a)] : CompleteSpace ↥(lp E p)

theorem LipschitzWith.uniformly_bounded {α : Type u_3} {ι : Type u_5} [PseudoMetricSpace α] (g : α → ι → ℝ) {K : NNReal} (hg : ∀ (i : ι), LipschitzWith K fun (x : α) => g x i) (a₀ : α) (hga₀b : Memℓp (g a₀) ⊤) (a : α) : Memℓp (g a) ⊤

theorem LipschitzOnWith.coordinate {α : Type u_3} {ι : Type u_5} [PseudoMetricSpace α] (f : α → ↥(lp (fun (x : ι) => ℝ) ⊤)) (s : Set α) (K : NNReal) : LipschitzOnWith K f s ↔ ∀ (i : ι), LipschitzOnWith K (fun (a : α) => ↑(f a) i) s

theorem LipschitzWith.coordinate {α : Type u_3} {ι : Type u_5} [PseudoMetricSpace α] {f : α → ↥(lp (fun (x : ι) => ℝ) ⊤)} (K : NNReal) : LipschitzWith K f ↔ ∀ (i : ι), LipschitzWith K fun (a : α) => ↑(f a) i