ℓ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 < ∞.

Equations

• Memℓp f p = if p = 0 then {i : α | f i ≠ 0}.Finite else if p = ⊤ then BddAbove (Set.range fun (i : α) => ‖f i‖) else Summable fun (i : α) => ‖f i‖ ^ p.toReal

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

Equations

• PreLp E = ((i : α) → E i)

instance instAddCommGroupPreLp {α : Type u_3} {E : α → Type u_4} [(i : α) → NormedAddCommGroup (E i)] : AddCommGroup (PreLp E)

Equations

• instAddCommGroupPreLp = id inferInstance

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

Equations

• PreLp.unique = Pi.uniqueOfIsEmpty E

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

lp space The p=∞ case has notation ℓ^∞(ι, E) resp. ℓ^∞(ι) (for E = ℝ) in the lp namespace.

Equations

• lp E p = { carrier := {f : PreLp E | Memℓp f p}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

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

lp space The p=∞ case has notation ℓ^∞(ι, E) resp. ℓ^∞(ι) (for E = ℝ) in the lp namespace.

Equations

• One or more equations did not get rendered due to their size.

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

lp space The p=∞ case has notation ℓ^∞(ι, E) resp. ℓ^∞(ι) (for E = ℝ) in the lp namespace.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• lp.instCoeOutSubtypePreLpMemAddSubgroupForall = { coe := Subtype.val }

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

Equations

• lp.coeFun = { coe := fun (f : ↥(lp E p)) => ↑f }

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.

Equations

• lp.coeFnAddMonoidHom E p = { toFun := Subtype.val, map_zero' := ⋯, map_add' := ⋯ }

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

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

Equations

• One or more equations did not get rendered due to their size.

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)

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‖

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

Equations

• lp.normedAddCommGroup = { toFun := norm, map_zero' := ⋯, add_le' := ⋯, neg' := ⋯, eq_zero_of_map_eq_zero' := ⋯ }.toNormedAddCommGroup

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

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)

Equations

• lp.instModulePreLp = Pi.module α 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.

Equations

• lpSubmodule 𝕜 E p = { toAddSubmonoid := (lp E p).toAddSubmonoid, smul_mem' := ⋯ }

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

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)

Equations

• lp.instModuleSubtypePreLpMemAddSubgroup = (lpSubmodule 𝕜 E p).module

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

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)

Equations

• lp.instNormedSpace = { toModule := lp.instModuleSubtypePreLpMemAddSubgroup, norm_smul_le := ⋯ }

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

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)

Equations

• lp.instStarSubtypePreLpMemAddSubgroup = { star := fun (f : ↥(lp E p)) => ⟨star ↑f, ⋯⟩ }

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

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)

Equations

• lp.instInvolutiveStar = { toStar := lp.instStarSubtypePreLpMemAddSubgroup, star_involutive := ⋯ }

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)

Equations

• lp.instStarAddMonoid = { toInvolutiveStar := lp.instInvolutiveStar, star_add := ⋯ }

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

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

Equations

• lp.instMulSubtypePreLpMemAddSubgroupTopENNReal = { mul := fun (f g : ↥(lp B ⊤)) => ⟨↑f * ↑g, ⋯⟩ }

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

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

Equations

• lp.nonUnitalRing = Function.Injective.nonUnitalRing CoeFun.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• lp.nonUnitalNormedCommRing = { toNonUnitalNormedRing := lp.nonUnitalNormedRing, mul_comm := ⋯ }

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

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

Equations

• lp.inftyStarRing = { toInvolutiveStar := lp.instStarAddMonoid.toInvolutiveStar, star_mul := ⋯, star_add := ⋯ }

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

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

Equations

• PreLp.ring = Pi.ring

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.

Equations

• lpInftySubring B = { carrier := {f : PreLp B | Memℓp f ⊤}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

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

Equations

• lp.inftyRing = (lpInftySubring B).toRing

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

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

Equations

• lp.inftyNormedRing = { toNorm := lp.nonUnitalNormedRing.toNorm, toRing := lp.inftyRing, toMetricSpace := lp.nonUnitalNormedRing.toMetricSpace, dist_eq := ⋯, norm_mul_le := ⋯ }

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

Equations

• lp.inftyNormedCommRing = { toNormedRing := lp.inftyNormedRing, mul_comm := ⋯ }

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

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

Equations

• Pi.algebraOfNormedAlgebra = Pi.algebra I B

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)

Equations

• PreLp.algebra = Pi.algebraOfNormedAlgebra

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.

Equations

• lpInftySubalgebra 𝕜 B = { carrier := {f : PreLp B | Memℓp f ⊤}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := ⋯ }

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

Equations

• lp.inftyNormedAlgebra = { toAlgebra := (lpInftySubalgebra 𝕜 B).algebra, norm_smul_le := ⋯ }

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.

Equations

• lp.single p i a = ⟨Pi.single i a, ⋯⟩

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.

Equations

• lp.singleAddMonoidHom p i = { toFun := lp.single p i, map_zero' := ⋯, map_add' := ⋯ }

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

Equations

• lp.lsingle p i = { toFun := lp.single p i, map_add' := ⋯, map_smul' := ⋯ }

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

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.

Equations

• lp.singleContinuousAddMonoidHom E p i = { toAddMonoidHom := lp.singleAddMonoidHom p i, continuous_toFun := ⋯ }

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

Equations

• lp.singleContinuousLinearMap 𝕜 E p i = { toLinearMap := lp.lsingle p i, cont := ⋯ }

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

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 (i : ι) => ℝ) ⊤)) (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 (i : ι) => ℝ) ⊤)} (K : NNReal) : LipschitzWith K f ↔ ∀ (i : ι), LipschitzWith K fun (a : α) => ↑(f a) i