# ℓ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_1} {E : αType u_2} [(i : α) → NormedAddCommGroup (E i)] (f : (i : α) → E i) (p : ENNReal) :

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
Instances For
theorem memℓp_zero_iff {α : Type u_1} {E : αType u_2} [(i : α) → NormedAddCommGroup (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 : α) → NormedAddCommGroup (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 : α) → NormedAddCommGroup (E i)] {f : (i : α) → E i} :
BddAbove (Set.range fun (i : α) => f i)
theorem memℓp_infty {α : Type u_1} {E : αType u_2} [(i : α) → NormedAddCommGroup (E i)] {f : (i : α) → E i} (hf : BddAbove (Set.range fun (i : α) => f i)) :
theorem memℓp_gen_iff {α : Type u_1} {E : αType u_2} {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_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {f : (i : α) → E i} (hf : Summable fun (i : α) => f i ^ p.toReal) :
theorem memℓp_gen' {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {C : } {f : (i : α) → E i} (hf : ∀ (s : ), is, f i ^ p.toReal C) :
theorem zero_memℓp {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] :
theorem zero_mem_ℓp' {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] :
Memℓp (fun (i : α) => 0) p
theorem Memℓp.finite_dsupport {α : Type u_1} {E : αType u_2} [(i : α) → NormedAddCommGroup (E i)] {f : (i : α) → E i} (hf : Memℓp f 0) :
{i : α | f i 0}.Finite
theorem Memℓp.bddAbove {α : Type u_1} {E : αType u_2} [(i : α) → NormedAddCommGroup (E i)] {f : (i : α) → E i} (hf : ) :
BddAbove (Set.range fun (i : α) => f i)
theorem Memℓp.summable {α : Type u_1} {E : αType u_2} {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_1} {E : αType u_2} {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_1} {E : αType u_2} {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_1} {E : αType u_2} [(i : α) → NormedAddCommGroup (E i)] {p : ENNReal} {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 : α) → NormedAddCommGroup (E i)] {f : (i : α) → E i} {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 : α) → NormedAddCommGroup (E i)] {f : (i : α) → E i} {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 : α) → NormedAddCommGroup (E i)] {ι : Type u_3} (s : ) {f : ι(i : α) → E i} (hf : is, Memℓp (f i) p) :
Memℓp (fun (a : α) => is, f i a) p
theorem Memℓp.const_smul {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {𝕜 : Type u_3} [] [(i : α) → Module 𝕜 (E i)] [∀ (i : α), BoundedSMul 𝕜 (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} [] {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_1} (E : αType u_3) [(i : α) → NormedAddCommGroup (E i)] :
Type (max u_1 u_3)

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
• = ((i : α) → E i)
Instances For
instance instAddCommGroupPreLp {α : Type u_1} {E : αType u_2} [(i : α) → NormedAddCommGroup (E i)] :
Equations
instance PreLp.unique {α : Type u_1} {E : αType u_2} [(i : α) → NormedAddCommGroup (E i)] [] :
Equations
• PreLp.unique =
def lp {α : Type u_1} (E : αType u_3) [(i : α) → NormedAddCommGroup (E i)] (p : ENNReal) :

lp space

Equations
• lp E p = { carrier := {f : | Memℓp f p}, add_mem' := , zero_mem' := , neg_mem' := }
Instances For

lp space

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

lp space

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance lp.instCoeOutSubtypePreLpMemAddSubgroupForall {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] :
CoeOut ((lp E p)) ((i : α) → E i)
Equations
• lp.instCoeOutSubtypePreLpMemAddSubgroupForall = { coe := Subtype.val }
instance lp.coeFun {α : Type u_1} {E : αType u_2} {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_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {f : (lp E p)} {g : (lp E p)} (h : f = g) :
f = g
theorem lp.ext_iff {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {f : (lp E p)} {g : (lp E p)} :
f = g f = g
theorem lp.eq_zero' {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [] (f : (lp E p)) :
f = 0
theorem lp.monotone {α : Type u_1} {E : αType u_2} [(i : α) → NormedAddCommGroup (E i)] {p : ENNReal} {q : ENNReal} (hpq : q p) :
lp E q lp E p
theorem lp.memℓp {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] (f : (lp E p)) :
Memℓp (f) p
@[simp]
theorem lp.coeFn_zero {α : Type u_1} (E : αType u_2) (p : ENNReal) [(i : α) → NormedAddCommGroup (E i)] :
0 = 0
@[simp]
theorem lp.coeFn_neg {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] (f : (lp E p)) :
(-f) = -f
@[simp]
theorem lp.coeFn_add {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] (f : (lp E p)) (g : (lp E p)) :
(f + g) = f + g
theorem lp.coeFn_sum {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {ι : Type u_3} (f : ι(lp E p)) (s : ) :
(is, f i) = is, (f i)
@[simp]
theorem lp.coeFn_sub {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] (f : (lp E p)) (g : (lp E p)) :
(f - g) = f - g
instance lp.instNormSubtypePreLpMemAddSubgroup {α : Type u_1} {E : αType u_2} {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_1} {E : αType u_2} [(i : α) → NormedAddCommGroup (E i)] (f : (lp E 0)) :
f = .toFinset.card
theorem lp.norm_eq_ciSup {α : Type u_1} {E : αType u_2} [(i : α) → NormedAddCommGroup (E i)] (f : (lp E )) :
f = ⨆ (i : α), f i
theorem lp.isLUB_norm {α : Type u_1} {E : αType u_2} [(i : α) → NormedAddCommGroup (E i)] [] (f : (lp E )) :
IsLUB (Set.range fun (i : α) => f i) f
theorem lp.norm_eq_tsum_rpow {α : Type u_1} {E : αType u_2} {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_1} {E : αType u_2} {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_1} {E : αType u_2} {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_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] (f : (lp E p)) :
@[simp]
theorem lp.norm_zero {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] :
theorem lp.norm_eq_zero_iff {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {f : (lp E p)} :
f = 0 f = 0
theorem lp.eq_zero_iff_coeFn_eq_zero {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (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 : α) → NormedAddCommGroup (E i)] ⦃f : (lp E p) :
instance lp.normedAddCommGroup {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [hp : Fact (1 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_1} {E : αType u_2} [(i : α) → NormedAddCommGroup (E i)] {p : ENNReal} {q : ENNReal} (hpq : p.toReal.IsConjExponent 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_1} {E : αType u_2} [(i : α) → NormedAddCommGroup (E i)] {p : ENNReal} {q : ENNReal} (hpq : p.toReal.IsConjExponent 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_1} {E : αType u_2} [(i : α) → NormedAddCommGroup (E i)] {p : ENNReal} {q : ENNReal} (hpq : p.toReal.IsConjExponent 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_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] (hp : p 0) (f : (lp E p)) (i : α) :
theorem lp.sum_rpow_le_norm_rpow {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] (hp : 0 < p.toReal) (f : (lp E p)) (s : ) :
is, f i ^ p.toReal f ^ p.toReal
theorem lp.norm_le_of_forall_le' {α : Type u_1} {E : αType u_2} [(i : α) → NormedAddCommGroup (E i)] [] {f : (lp E )} (C : ) (hCf : ∀ (i : α), f i C) :
theorem lp.norm_le_of_forall_le {α : Type u_1} {E : αType u_2} [(i : α) → NormedAddCommGroup (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 : α) → NormedAddCommGroup (E i)] (hp : 0 < p.toReal) {C : } (hC : 0 C) {f : (lp E p)} (hf : ∑' (i : α), f i ^ p.toReal C ^ p.toReal) :
theorem lp.norm_le_of_forall_sum_le {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] (hp : 0 < p.toReal) {C : } (hC : 0 C) {f : (lp E p)} (hf : ∀ (s : ), is, f i ^ p.toReal C ^ p.toReal) :
instance lp.instModulePreLp {α : Type u_1} {E : αType u_2} [(i : α) → NormedAddCommGroup (E i)] {𝕜 : Type u_3} [] [(i : α) → Module 𝕜 (E i)] :
Module 𝕜 ()
Equations
instance lp.instSMulCommClassPreLp {α : Type u_1} {E : αType u_2} [(i : α) → NormedAddCommGroup (E i)] {𝕜 : Type u_3} {𝕜' : Type u_4} [] [] [(i : α) → Module 𝕜 (E i)] [(i : α) → Module 𝕜' (E i)] [∀ (i : α), SMulCommClass 𝕜' 𝕜 (E i)] :
SMulCommClass 𝕜' 𝕜 ()
Equations
• =
instance lp.instIsScalarTowerPreLp {α : Type u_1} {E : αType u_2} [(i : α) → NormedAddCommGroup (E i)] {𝕜 : Type u_3} {𝕜' : Type u_4} [] [] [(i : α) → Module 𝕜 (E i)] [(i : α) → Module 𝕜' (E i)] [SMul 𝕜' 𝕜] [∀ (i : α), IsScalarTower 𝕜' 𝕜 (E i)] :
IsScalarTower 𝕜' 𝕜 ()
Equations
• =
instance lp.instIsCentralScalarPreLp {α : Type u_1} {E : αType u_2} [(i : α) → NormedAddCommGroup (E i)] {𝕜 : Type u_3} [] [(i : α) → Module 𝕜 (E i)] [(i : α) → Module 𝕜ᵐᵒᵖ (E i)] [∀ (i : α), IsCentralScalar 𝕜 (E i)] :
Equations
• =
theorem lp.mem_lp_const_smul {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {𝕜 : Type u_3} [] [(i : α) → Module 𝕜 (E i)] [∀ (i : α), BoundedSMul 𝕜 (E i)] (c : 𝕜) (f : (lp E p)) :
c f lp E p
def lpSubmodule {α : Type u_1} (E : αType u_2) (p : ENNReal) [(i : α) → NormedAddCommGroup (E i)] (𝕜 : Type u_3) [] [(i : α) → Module 𝕜 (E i)] [∀ (i : α), BoundedSMul 𝕜 (E i)] :
Submodule 𝕜 ()

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 𝕜 = let __src := lp E p; { toAddSubmonoid := __src.toAddSubmonoid, smul_mem' := }
Instances For
theorem lp.coe_lpSubmodule {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {𝕜 : Type u_3} [] [(i : α) → Module 𝕜 (E i)] [∀ (i : α), BoundedSMul 𝕜 (E i)] :
(lpSubmodule E p 𝕜).toAddSubgroup = lp E p
instance lp.instModuleSubtypePreLpMemAddSubgroup {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {𝕜 : Type u_3} [] [(i : α) → Module 𝕜 (E i)] [∀ (i : α), BoundedSMul 𝕜 (E i)] :
Module 𝕜 (lp E p)
Equations
• lp.instModuleSubtypePreLpMemAddSubgroup = let __src := (lpSubmodule E p 𝕜).module;
@[simp]
theorem lp.coeFn_smul {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {𝕜 : Type u_3} [] [(i : α) → Module 𝕜 (E i)] [∀ (i : α), BoundedSMul 𝕜 (E i)] (c : 𝕜) (f : (lp E p)) :
(c f) = c f
instance lp.instSMulCommClassSubtypePreLpMemAddSubgroup {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {𝕜 : Type u_3} {𝕜' : Type u_4} [] [] [(i : α) → Module 𝕜 (E i)] [(i : α) → Module 𝕜' (E i)] [∀ (i : α), BoundedSMul 𝕜 (E i)] [∀ (i : α), BoundedSMul 𝕜' (E i)] [∀ (i : α), SMulCommClass 𝕜' 𝕜 (E i)] :
SMulCommClass 𝕜' 𝕜 (lp E p)
Equations
• =
instance lp.instIsScalarTowerSubtypePreLpMemAddSubgroup {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {𝕜 : Type u_3} {𝕜' : Type u_4} [] [] [(i : α) → Module 𝕜 (E i)] [(i : α) → Module 𝕜' (E i)] [∀ (i : α), BoundedSMul 𝕜 (E i)] [∀ (i : α), BoundedSMul 𝕜' (E i)] [SMul 𝕜' 𝕜] [∀ (i : α), IsScalarTower 𝕜' 𝕜 (E i)] :
IsScalarTower 𝕜' 𝕜 (lp E p)
Equations
• =
instance lp.instIsCentralScalarSubtypePreLpMemAddSubgroup {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {𝕜 : Type u_3} [] [(i : α) → Module 𝕜 (E i)] [∀ (i : α), BoundedSMul 𝕜 (E i)] [(i : α) → Module 𝕜ᵐᵒᵖ (E i)] [∀ (i : α), IsCentralScalar 𝕜 (E i)] :
IsCentralScalar 𝕜 (lp E p)
Equations
• =
theorem lp.norm_const_smul_le {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {𝕜 : Type u_3} [] [(i : α) → Module 𝕜 (E i)] [∀ (i : α), BoundedSMul 𝕜 (E i)] (hp : p 0) (c : 𝕜) (f : (lp E p)) :
instance lp.instBoundedSMulSubtypePreLpMemAddSubgroup {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {𝕜 : Type u_3} [] [(i : α) → Module 𝕜 (E i)] [∀ (i : α), BoundedSMul 𝕜 (E i)] [Fact (1 p)] :
BoundedSMul 𝕜 (lp E p)
Equations
• =
theorem lp.norm_const_smul {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {𝕜 : Type u_3} [(i : α) → Module 𝕜 (E i)] [∀ (i : α), BoundedSMul 𝕜 (E i)] (hp : p 0) {c : 𝕜} (f : (lp E p)) :
instance lp.instNormedSpace {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {𝕜 : Type u_3} [] [(i : α) → NormedSpace 𝕜 (E i)] [Fact (1 p)] :
NormedSpace 𝕜 (lp E p)
Equations
• lp.instNormedSpace =
theorem Memℓp.star_mem {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [(i : α) → StarAddMonoid (E i)] [∀ (i : α), NormedStarGroup (E i)] {f : (i : α) → E i} (hf : Memℓp f p) :
@[simp]
theorem Memℓp.star_iff {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [(i : α) → StarAddMonoid (E i)] [∀ (i : α), NormedStarGroup (E i)] {f : (i : α) → E i} :
instance lp.instStarSubtypePreLpMemAddSubgroup {α : Type u_1} {E : αType u_2} {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_1} {E : αType u_2} {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_1} {E : αType u_2} {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_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [(i : α) → StarAddMonoid (E i)] [∀ (i : α), NormedStarGroup (E i)] :
Equations
• lp.instInvolutiveStar =
instance lp.instStarAddMonoid {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [(i : α) → StarAddMonoid (E i)] [∀ (i : α), NormedStarGroup (E i)] :
Equations
instance lp.instNormedStarGroupSubtypePreLpMemAddSubgroup {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [(i : α) → StarAddMonoid (E i)] [∀ (i : α), NormedStarGroup (E i)] [hp : Fact (1 p)] :
Equations
• =
instance lp.instStarModuleSubtypePreLpMemAddSubgroup {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [(i : α) → StarAddMonoid (E i)] [∀ (i : α), NormedStarGroup (E i)] {𝕜 : Type u_3} [Star 𝕜] [] [(i : α) → Module 𝕜 (E i)] [∀ (i : α), BoundedSMul 𝕜 (E i)] [∀ (i : α), StarModule 𝕜 (E i)] :
StarModule 𝕜 (lp E p)
Equations
• =
theorem Memℓp.infty_mul {I : Type u_3} {B : IType u_4} [(i : I) → NonUnitalNormedRing (B i)] {f : (i : I) → B i} {g : (i : I) → B i} (hf : ) (hg : ) :
Memℓp (f * g)
instance lp.instMulSubtypePreLpMemAddSubgroupTopENNReal {I : Type u_3} {B : IType u_4} [(i : I) → NonUnitalNormedRing (B i)] :
Mul (lp B )
Equations
• lp.instMulSubtypePreLpMemAddSubgroupTopENNReal = { mul := fun (f g : (lp B )) => (fun (i : I) => f i) * fun (i : I) => g i, }
@[simp]
theorem lp.infty_coeFn_mul {I : Type u_3} {B : IType u_4} [(i : I) → NonUnitalNormedRing (B i)] (f : (lp B )) (g : (lp B )) :
(f * g) = f * g
instance lp.nonUnitalRing {I : Type u_3} {B : IType u_4} [(i : I) → NonUnitalNormedRing (B i)] :
Equations
instance lp.nonUnitalNormedRing {I : Type u_3} {B : IType u_4} [(i : I) → NonUnitalNormedRing (B i)] :
Equations
• lp.nonUnitalNormedRing = let __src := lp.normedAddCommGroup; let __src_1 := lp.nonUnitalRing;
instance lp.infty_isScalarTower {I : Type u_3} {B : IType u_4} [(i : I) → NonUnitalNormedRing (B i)] {𝕜 : Type u_5} [] [(i : I) → Module 𝕜 (B i)] [∀ (i : I), BoundedSMul 𝕜 (B i)] [∀ (i : I), IsScalarTower 𝕜 (B i) (B i)] :
IsScalarTower 𝕜 (lp B ) (lp B )
Equations
• =
instance lp.infty_smulCommClass {I : Type u_3} {B : IType u_4} [(i : I) → NonUnitalNormedRing (B i)] {𝕜 : Type u_5} [] [(i : I) → Module 𝕜 (B i)] [∀ (i : I), BoundedSMul 𝕜 (B i)] [∀ (i : I), SMulCommClass 𝕜 (B i) (B i)] :
SMulCommClass 𝕜 (lp B ) (lp B )
Equations
• =
instance lp.inftyStarRing {I : Type u_3} {B : IType u_4} [(i : I) → NonUnitalNormedRing (B i)] [(i : I) → StarRing (B i)] [∀ (i : I), NormedStarGroup (B i)] :
StarRing (lp B )
Equations
• lp.inftyStarRing = let __src := lp.instStarAddMonoid;
instance lp.inftyCstarRing {I : Type u_3} {B : IType u_4} [(i : I) → NonUnitalNormedRing (B i)] [(i : I) → StarRing (B i)] [∀ (i : I), NormedStarGroup (B i)] [∀ (i : I), CstarRing (B i)] :
Equations
• =
instance PreLp.ring {I : Type u_3} {B : IType u_4} [(i : I) → NormedRing (B i)] :
Ring ()
Equations
• PreLp.ring = Pi.ring
theorem one_memℓp_infty {I : Type u_3} {B : IType u_4} [(i : I) → NormedRing (B i)] [∀ (i : I), NormOneClass (B i)] :
def lpInftySubring {I : Type u_3} (B : IType u_4) [(i : I) → NormedRing (B i)] [∀ (i : I), NormOneClass (B i)] :

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

Equations
• = let __src := lp B ; { carrier := {f : | }, mul_mem' := , one_mem' := , add_mem' := , zero_mem' := , neg_mem' := }
Instances For
instance lp.inftyRing {I : Type u_3} {B : IType u_4} [(i : I) → NormedRing (B i)] [∀ (i : I), NormOneClass (B i)] :
Ring (lp B )
Equations
• lp.inftyRing = ().toRing
theorem Memℓp.infty_pow {I : Type u_3} {B : IType u_4} [(i : I) → NormedRing (B i)] [∀ (i : I), NormOneClass (B i)] {f : (i : I) → B i} (hf : ) (n : ) :
Memℓp (f ^ n)
theorem natCast_memℓp_infty {I : Type u_3} {B : IType u_4} [(i : I) → NormedRing (B i)] [∀ (i : I), NormOneClass (B i)] (n : ) :
theorem intCast_memℓp_infty {I : Type u_3} {B : IType u_4} [(i : I) → NormedRing (B i)] [∀ (i : I), NormOneClass (B i)] (z : ) :
@[simp]
theorem lp.infty_coeFn_one {I : Type u_3} {B : IType u_4} [(i : I) → NormedRing (B i)] [∀ (i : I), NormOneClass (B i)] :
1 = 1
@[simp]
theorem lp.infty_coeFn_pow {I : Type u_3} {B : IType u_4} [(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_3} {B : IType u_4} [(i : I) → NormedRing (B i)] [∀ (i : I), NormOneClass (B i)] (n : ) :
n = n
@[simp]
theorem lp.infty_coeFn_intCast {I : Type u_3} {B : IType u_4} [(i : I) → NormedRing (B i)] [∀ (i : I), NormOneClass (B i)] (z : ) :
z = z
instance lp.instNormOneClassSubtypePreLpMemAddSubgroupTopENNRealOfNonempty {I : Type u_3} {B : IType u_4} [(i : I) → NormedRing (B i)] [∀ (i : I), NormOneClass (B i)] [] :
Equations
• =
instance lp.inftyNormedRing {I : Type u_3} {B : IType u_4} [(i : I) → NormedRing (B i)] [∀ (i : I), NormOneClass (B i)] :
Equations
• lp.inftyNormedRing = let __src := lp.inftyRing; let __src_1 := lp.nonUnitalNormedRing;
instance lp.inftyCommRing {I : Type u_3} {B : IType u_4} [(i : I) → NormedCommRing (B i)] [∀ (i : I), NormOneClass (B i)] :
CommRing (lp B )
Equations
• lp.inftyCommRing = let __src := lp.inftyRing;
instance lp.inftyNormedCommRing {I : Type u_3} {B : IType u_4} [(i : I) → NormedCommRing (B i)] [∀ (i : I), NormOneClass (B i)] :
Equations
• lp.inftyNormedCommRing = let __src := lp.inftyCommRing; let __src_1 := lp.inftyNormedRing;
instance Pi.algebraOfNormedAlgebra {I : Type u_3} {𝕜 : Type u_4} {B : IType u_5} [] [(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 =
instance PreLp.algebra {I : Type u_3} {𝕜 : Type u_4} {B : IType u_5} [] [(i : I) → NormedRing (B i)] [(i : I) → NormedAlgebra 𝕜 (B i)] :
Algebra 𝕜 ()
Equations
• PreLp.algebra = Pi.algebraOfNormedAlgebra
theorem algebraMap_memℓp_infty {I : Type u_3} {𝕜 : Type u_4} {B : IType u_5} [] [(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 {I : Type u_3} (𝕜 : Type u_4) (B : IType u_5) [] [(i : I) → NormedRing (B i)] [(i : I) → NormedAlgebra 𝕜 (B i)] [∀ (i : I), NormOneClass (B i)] :
Subalgebra 𝕜 ()

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

Equations
• = let __src := ; { carrier := {f : | }, mul_mem' := , one_mem' := , add_mem' := , zero_mem' := , algebraMap_mem' := }
Instances For
instance lp.inftyNormedAlgebra {I : Type u_3} {𝕜 : Type u_4} {B : IType u_5} [] [(i : I) → NormedRing (B i)] [(i : I) → NormedAlgebra 𝕜 (B i)] [∀ (i : I), NormOneClass (B i)] :
NormedAlgebra 𝕜 (lp B )
Equations
• lp.inftyNormedAlgebra = let __src := ().algebra; let __src_1 := lp.instNormedSpace;
def lp.single {α : Type u_1} {E : αType u_2} [(i : α) → NormedAddCommGroup (E i)] [] (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 = fun (j : α) => if h : j = i then a else 0,
Instances For
theorem lp.single_apply {α : Type u_1} {E : αType u_2} [(i : α) → NormedAddCommGroup (E i)] [] (p : ENNReal) (i : α) (a : E i) (j : α) :
(lp.single p i a) j = if h : j = i then a else 0
theorem lp.single_apply_self {α : Type u_1} {E : αType u_2} [(i : α) → NormedAddCommGroup (E i)] [] (p : ENNReal) (i : α) (a : E i) :
(lp.single p i a) i = a
theorem lp.single_apply_ne {α : Type u_1} {E : αType u_2} [(i : α) → NormedAddCommGroup (E i)] [] (p : ENNReal) (i : α) (a : E i) {j : α} (hij : j i) :
(lp.single p i a) j = 0
@[simp]
theorem lp.single_neg {α : Type u_1} {E : αType u_2} [(i : α) → NormedAddCommGroup (E i)] [] (p : ENNReal) (i : α) (a : E i) :
lp.single p i (-a) = -lp.single p i a
@[simp]
theorem lp.single_smul {α : Type u_1} {E : αType u_2} [(i : α) → NormedAddCommGroup (E i)] {𝕜 : Type u_3} [] [(i : α) → Module 𝕜 (E i)] [∀ (i : α), BoundedSMul 𝕜 (E i)] [] (p : ENNReal) (i : α) (a : E i) (c : 𝕜) :
lp.single p i (c a) = c lp.single p i a
theorem lp.norm_sum_single {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [] (hp : 0 < p.toReal) (f : (i : α) → E i) (s : ) :
is, lp.single p i (f i) ^ p.toReal = is, f i ^ p.toReal
theorem lp.norm_single {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [] (hp : 0 < p.toReal) (f : (i : α) → E i) (i : α) :
lp.single p i (f i) = f i
theorem lp.norm_sub_norm_compl_sub_single {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [] (hp : 0 < p.toReal) (f : (lp E p)) (s : ) :
f ^ p.toReal - f - is, lp.single p i (f i) ^ p.toReal = is, f i ^ p.toReal
theorem lp.norm_compl_sum_single {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [] (hp : 0 < p.toReal) (f : (lp E p)) (s : ) :
f - is, lp.single p i (f i) ^ p.toReal = f ^ p.toReal - is, f i ^ p.toReal
theorem lp.hasSum_single {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [] [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.uniformContinuous_coe {α : Type u_1} {E : αType u_2} {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_1} {E : αType u_2} [(i : α) → NormedAddCommGroup (E i)] {ι : Type u_3} {l : } [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_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {ι : Type u_3} {l : } [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 : ) :
is, f i ^ p.toReal C ^ p.toReal
theorem lp.norm_le_of_tendsto {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {ι : Type u_3} {l : } [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)) :

"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 : α) → NormedAddCommGroup (E i)] {ι : Type u_3} {l : } [l.NeBot] [_i : Fact (1 p)] {F : ι(lp E p)} (hF : ) {f : (a : α) → E a} (hf : Filter.Tendsto (id fun (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 : α) → NormedAddCommGroup (E i)] [_i : Fact (1 p)] {F : (lp E p)} (hF : ) {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_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [_i : Fact (1 p)] [∀ (a : α), CompleteSpace (E a)] :
CompleteSpace (lp E p)
Equations
• =
theorem LipschitzWith.uniformly_bounded {α : Type u_1} {ι : Type u_3} (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_1} {ι : Type u_3} (f : α(lp (fun (i : ι) => ) )) (s : Set α) (K : NNReal) :
∀ (i : ι), LipschitzOnWith K (fun (a : α) => (f a) i) s
theorem LipschitzWith.coordinate {α : Type u_1} {ι : Type u_3} {f : α(lp (fun (i : ι) => ) )} (K : NNReal) :
∀ (i : ι), LipschitzWith K fun (a : α) => (f a) i