Documentation

Mathlib.Analysis.NormedSpace.lpSpace

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

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 ↔ Set.Finite {i | f i ≠ 0}

theorem memℓp_zero {α : Type u_1} {E : α → Type u_2} [(i : α) → NormedAddCommGroup (E i)] {f : (i : α) → E i} (hf : Set.Finite {i | f i ≠ 0}) :

theorem memℓp_infty_iff {α : Type u_1} {E : α → Type u_2} [(i : α) → NormedAddCommGroup (E i)] {f : (i : α) → E i} :

Memℓp f ⊤ ↔ 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 < ENNReal.toReal p) {f : (i : α) → E i} :

Memℓp f p ↔ Summable fun i => ‖f i‖ ^ ENNReal.toReal p

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‖ ^ ENNReal.toReal p) :

theorem memℓp_gen' {α : Type u_1} {E : α → Type u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {C : ℝ} {f : (i : α) → E i} (hf : ∀ (s : Finset α), (Finset.sum s fun i => ‖f i‖ ^ ENNReal.toReal p) ≤ 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) :

Set.Finite {i | f i ≠ 0}

theorem Memℓp.bddAbove {α : Type u_1} {E : α → Type u_2} [(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_1} {E : α → Type u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] (hp : 0 < ENNReal.toReal p) {f : (i : α) → E i} (hf : Memℓp f p) :

Summable fun i => ‖f i‖ ^ ENNReal.toReal p

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

@[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 : Finset ι) {f : ι → (i : α) → E i} (hf : ∀ (i : ι), i ∈ s → Memℓp (f i) p) :

Memℓp (fun a => Finset.sum s fun i => 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} [NormedRing 𝕜] [(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} [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_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).

Instances For

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

AddCommGroup (PreLp E)

instance PreLp.unique {α : Type u_1} {E : α → Type u_2} [(i : α) → NormedAddCommGroup (E i)] [IsEmpty α] :

Unique (PreLp E)

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

AddSubgroup (PreLp E)

lp space

Instances For

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

Lean.ParserDescr

Instances For

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

Lean.ParserDescr

Instances For

instance lp.instCoeOutSubtypePreLpMemAddSubgroupToAddGroupInstAddCommGroupPreLpInstMembershipInstSetLikeAddSubgroupLpForAll {α : Type u_1} {E : α → Type u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] :

CoeOut { x // x ∈ lp E p } ((i : α) → E i)

instance lp.coeFun {α : Type u_1} {E : α → Type u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] :

CoeFun { x // x ∈ lp E p } fun x => (i : α) → E i

theorem lp.ext {α : Type u_1} {E : α → Type u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {f : { x // x ∈ lp E p }} {g : { x // x ∈ 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 : { x // x ∈ lp E p }} {g : { x // x ∈ lp E p }} :

f = g ↔ ↑f = ↑g

theorem lp.eq_zero' {α : Type u_1} {E : α → Type u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [IsEmpty α] (f : { x // x ∈ 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 : { x // x ∈ 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 : { x // x ∈ lp E p }) :

↑(-f) = -↑f

@[simp]

theorem lp.coeFn_add {α : Type u_1} {E : α → Type u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] (f : { x // x ∈ lp E p }) (g : { x // x ∈ 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 : ι → { x // x ∈ lp E p }) (s : Finset ι) :

↑(Finset.sum s fun i => f i) = Finset.sum s fun i => ↑(f i)

@[simp]

theorem lp.coeFn_sub {α : Type u_1} {E : α → Type u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] (f : { x // x ∈ lp E p }) (g : { x // x ∈ lp E p }) :

↑(f - g) = ↑f - ↑g

instance lp.instNormSubtypePreLpMemAddSubgroupToAddGroupInstAddCommGroupPreLpInstMembershipInstSetLikeAddSubgroupLp {α : Type u_1} {E : α → Type u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] :

Norm { x // x ∈ lp E p }

theorem lp.norm_eq_card_dsupport {α : Type u_1} {E : α → Type u_2} [(i : α) → NormedAddCommGroup (E i)] (f : { x // x ∈ lp E 0 }) :

‖f‖ = ↑(Finset.card (Set.Finite.toFinset (_ : Set.Finite {i | ↑f i ≠ 0})))

theorem lp.norm_eq_ciSup {α : Type u_1} {E : α → Type u_2} [(i : α) → NormedAddCommGroup (E i)] (f : { x // x ∈ lp E ⊤ }) :

‖f‖ = ⨆ (i : α), ‖↑f i‖

theorem lp.isLUB_norm {α : Type u_1} {E : α → Type u_2} [(i : α) → NormedAddCommGroup (E i)] [Nonempty α] (f : { x // x ∈ 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 < ENNReal.toReal p) (f : { x // x ∈ lp E p }) :

‖f‖ = (∑' (i : α), ‖↑f i‖ ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p)

theorem lp.norm_rpow_eq_tsum {α : Type u_1} {E : α → Type u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] (hp : 0 < ENNReal.toReal p) (f : { x // x ∈ lp E p }) :

‖f‖ ^ ENNReal.toReal p = ∑' (i : α), ‖↑f i‖ ^ ENNReal.toReal p

theorem lp.hasSum_norm {α : Type u_1} {E : α → Type u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] (hp : 0 < ENNReal.toReal p) (f : { x // x ∈ lp E p }) :

HasSum (fun i => ‖↑f i‖ ^ ENNReal.toReal p) (‖f‖ ^ ENNReal.toReal p)

theorem lp.norm_nonneg' {α : Type u_1} {E : α → Type u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] (f : { x // x ∈ 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 : { x // x ∈ 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 : { x // x ∈ 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 : { x // x ∈ lp E p }⦄ :

‖-f‖ = ‖f‖

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

NormedAddCommGroup { x // x ∈ lp E p }

theorem lp.tsum_mul_le_mul_norm {α : Type u_1} {E : α → Type u_2} [(i : α) → NormedAddCommGroup (E i)] {p : ENNReal} {q : ENNReal} (hpq : Real.IsConjugateExponent (ENNReal.toReal p) (ENNReal.toReal q)) (f : { x // x ∈ lp E p }) (g : { x // x ∈ 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 : Real.IsConjugateExponent (ENNReal.toReal p) (ENNReal.toReal q)) (f : { x // x ∈ lp E p }) (g : { x // x ∈ 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 : Real.IsConjugateExponent (ENNReal.toReal p) (ENNReal.toReal q)) (f : { x // x ∈ lp E p }) (g : { x // x ∈ 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 : { x // x ∈ lp E p }) (i : α) :

‖↑f i‖ ≤ ‖f‖

theorem lp.sum_rpow_le_norm_rpow {α : Type u_1} {E : α → Type u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] (hp : 0 < ENNReal.toReal p) (f : { x // x ∈ lp E p }) (s : Finset α) :

(Finset.sum s fun i => ‖↑f i‖ ^ ENNReal.toReal p) ≤ ‖f‖ ^ ENNReal.toReal p

theorem lp.norm_le_of_forall_le' {α : Type u_1} {E : α → Type u_2} [(i : α) → NormedAddCommGroup (E i)] [Nonempty α] {f : { x // x ∈ 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 : { x // x ∈ 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 < ENNReal.toReal p) {C : ℝ} (hC : 0 ≤ C) {f : { x // x ∈ lp E p }} (hf : ∑' (i : α), ‖↑f i‖ ^ ENNReal.toReal p ≤ C ^ ENNReal.toReal p) :

theorem lp.norm_le_of_forall_sum_le {α : Type u_1} {E : α → Type u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] (hp : 0 < ENNReal.toReal p) {C : ℝ} (hC : 0 ≤ C) {f : { x // x ∈ lp E p }} (hf : ∀ (s : Finset α), (Finset.sum s fun i => ‖↑f i‖ ^ ENNReal.toReal p) ≤ C ^ ENNReal.toReal p) :

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

Module 𝕜 (PreLp E)

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

SMulCommClass 𝕜' 𝕜 (PreLp E)

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

IsScalarTower 𝕜' 𝕜 (PreLp E)

instance lp.instIsCentralScalarPreLpToSMulToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidInstAddCommGroupPreLpToSMulZeroClassToZeroToMonoidWithZeroToSemiringToRingToSMulWithZeroToMulActionWithZeroToAddCommMonoidInstModulePreLpToSemiringToRingToAddCommMonoidInstAddCommGroupPreLpMulOppositeZeroMonoidWithZeroSemiringNormedRing {α : Type u_1} {E : α → Type u_2} [(i : α) → NormedAddCommGroup (E i)] {𝕜 : Type u_3} [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} {E : α → Type u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {𝕜 : Type u_3} [NormedRing 𝕜] [(i : α) → Module 𝕜 (E i)] [∀ (i : α), BoundedSMul 𝕜 (E i)] (c : 𝕜) (f : { x // x ∈ 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) [NormedRing 𝕜] [(i : α) → Module 𝕜 (E i)] [∀ (i : α), BoundedSMul 𝕜 (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.

Instances For

theorem lp.coe_lpSubmodule {α : Type u_1} {E : α → Type u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {𝕜 : Type u_3} [NormedRing 𝕜] [(i : α) → Module 𝕜 (E i)] [∀ (i : α), BoundedSMul 𝕜 (E i)] :

Submodule.toAddSubgroup (lpSubmodule E p 𝕜) = lp E p

instance lp.instModuleSubtypePreLpMemAddSubgroupToAddGroupInstAddCommGroupPreLpInstMembershipInstSetLikeAddSubgroupLpToSemiringToRingToAddCommMonoidToAddCommMonoidToAddSubmonoid {α : Type u_1} {E : α → Type u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {𝕜 : Type u_3} [NormedRing 𝕜] [(i : α) → Module 𝕜 (E i)] [∀ (i : α), BoundedSMul 𝕜 (E i)] :

Module 𝕜 { x // x ∈ lp E p }

@[simp]

theorem lp.coeFn_smul {α : Type u_1} {E : α → Type u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {𝕜 : Type u_3} [NormedRing 𝕜] [(i : α) → Module 𝕜 (E i)] [∀ (i : α), BoundedSMul 𝕜 (E i)] (c : 𝕜) (f : { x // x ∈ lp E p }) :

↑(c • f) = c • ↑f

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

SMulCommClass 𝕜' 𝕜 { x // x ∈ lp E p }

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

IsScalarTower 𝕜' 𝕜 { x // x ∈ lp E p }

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

IsCentralScalar 𝕜 { x // x ∈ lp E p }

theorem lp.norm_const_smul_le {α : Type u_1} {E : α → Type u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {𝕜 : Type u_3} [NormedRing 𝕜] [(i : α) → Module 𝕜 (E i)] [∀ (i : α), BoundedSMul 𝕜 (E i)] (hp : p ≠ 0) (c : 𝕜) (f : { x // x ∈ lp E p }) :

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

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

BoundedSMul 𝕜 { x // x ∈ lp E p }

theorem lp.norm_const_smul {α : Type u_1} {E : α → Type u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {𝕜 : Type u_3} [NormedDivisionRing 𝕜] [(i : α) → Module 𝕜 (E i)] [∀ (i : α), BoundedSMul 𝕜 (E i)] (hp : p ≠ 0) {c : 𝕜} (f : { x // x ∈ lp E p }) :

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

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

NormedSpace 𝕜 { x // x ∈ lp E p }

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

Memℓp (star 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} :

Memℓp (star f) p ↔ Memℓp f p

instance lp.instStarSubtypePreLpMemAddSubgroupToAddGroupInstAddCommGroupPreLpInstMembershipInstSetLikeAddSubgroupLp {α : Type u_1} {E : α → Type u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [(i : α) → StarAddMonoid (E i)] [∀ (i : α), NormedStarGroup (E i)] :

Star { x // x ∈ lp E p }

@[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 : { x // x ∈ 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 : { x // x ∈ 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)] :

InvolutiveStar { x // x ∈ lp E p }

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

StarAddMonoid { x // x ∈ lp E p }

instance lp.instNormedStarGroupSubtypePreLpMemAddSubgroupToAddGroupInstAddCommGroupPreLpInstMembershipInstSetLikeAddSubgroupLpToSeminormedAddCommGroupNormedAddCommGroupInstStarAddMonoid {α : 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)] :

NormedStarGroup { x // x ∈ lp E p }

instance lp.instStarModuleSubtypePreLpMemAddSubgroupToAddGroupInstAddCommGroupPreLpInstMembershipInstSetLikeAddSubgroupLpInstStarSubtypePreLpMemAddSubgroupToAddGroupInstAddCommGroupPreLpInstMembershipInstSetLikeAddSubgroupLpToSMulZeroToSMulZeroClassToZeroToMonoidWithZeroToSemiringToRingToSMulWithZeroToMulActionWithZeroToAddCommMonoidToAddCommMonoidToAddSubmonoidInstModuleSubtypePreLpMemAddSubgroupToAddGroupInstAddCommGroupPreLpInstMembershipInstSetLikeAddSubgroupLpToSemiringToRingToAddCommMonoidToAddCommMonoidToAddSubmonoid {α : 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 𝕜] [NormedRing 𝕜] [(i : α) → Module 𝕜 (E i)] [∀ (i : α), BoundedSMul 𝕜 (E i)] [∀ (i : α), StarModule 𝕜 (E i)] :

StarModule 𝕜 { x // x ∈ lp E p }

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

Memℓp (f * g) ⊤

instance lp.instMulSubtypePreLpToNormedAddCommGroupMemAddSubgroupToAddGroupInstAddCommGroupPreLpInstMembershipInstSetLikeAddSubgroupLpTopENNRealToTopToCompleteLatticeToCompletelyDistribLatticeInstCompleteLinearOrderENNReal {I : Type u_3} {B : I → Type u_4} [(i : I) → NonUnitalNormedRing (B i)] :

Mul { x // x ∈ lp B ⊤ }

@[simp]

theorem lp.infty_coeFn_mul {I : Type u_3} {B : I → Type u_4} [(i : I) → NonUnitalNormedRing (B i)] (f : { x // x ∈ lp B ⊤ }) (g : { x // x ∈ lp B ⊤ }) :

↑(f * g) = ↑f * ↑g

instance lp.nonUnitalRing {I : Type u_3} {B : I → Type u_4} [(i : I) → NonUnitalNormedRing (B i)] :

NonUnitalRing { x // x ∈ lp B ⊤ }

instance lp.nonUnitalNormedRing {I : Type u_3} {B : I → Type u_4} [(i : I) → NonUnitalNormedRing (B i)] :

NonUnitalNormedRing { x // x ∈ lp B ⊤ }

instance lp.infty_isScalarTower {I : Type u_3} {B : I → Type u_4} [(i : I) → NonUnitalNormedRing (B i)] {𝕜 : Type u_5} [NormedRing 𝕜] [(i : I) → Module 𝕜 (B i)] [∀ (i : I), BoundedSMul 𝕜 (B i)] [∀ (i : I), IsScalarTower 𝕜 (B i) (B i)] :

IsScalarTower 𝕜 { x // x ∈ lp B ⊤ } { x // x ∈ lp B ⊤ }

instance lp.infty_smulCommClass {I : Type u_3} {B : I → Type u_4} [(i : I) → NonUnitalNormedRing (B i)] {𝕜 : Type u_5} [NormedRing 𝕜] [(i : I) → Module 𝕜 (B i)] [∀ (i : I), BoundedSMul 𝕜 (B i)] [∀ (i : I), SMulCommClass 𝕜 (B i) (B i)] :

SMulCommClass 𝕜 { x // x ∈ lp B ⊤ } { x // x ∈ lp B ⊤ }

instance lp.inftyStarRing {I : Type u_3} {B : I → Type u_4} [(i : I) → NonUnitalNormedRing (B i)] [(i : I) → StarRing (B i)] [∀ (i : I), NormedStarGroup (B i)] :

StarRing { x // x ∈ lp B ⊤ }

instance lp.inftyCstarRing {I : Type u_3} {B : I → Type u_4} [(i : I) → NonUnitalNormedRing (B i)] [(i : I) → StarRing (B i)] [∀ (i : I), NormedStarGroup (B i)] [∀ (i : I), CstarRing (B i)] :

CstarRing { x // x ∈ lp B ⊤ }

instance PreLp.ring {I : Type u_3} {B : I → Type u_4} [(i : I) → NormedRing (B i)] :

theorem one_memℓp_infty {I : Type u_3} {B : I → Type u_4} [(i : I) → NormedRing (B i)] [∀ (i : I), NormOneClass (B i)] :

def lpInftySubring {I : Type u_3} (B : I → Type u_4) [(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.

Instances For

instance lp.inftyRing {I : Type u_3} {B : I → Type u_4} [(i : I) → NormedRing (B i)] [∀ (i : I), NormOneClass (B i)] :

Ring { x // x ∈ lp B ⊤ }

theorem Memℓp.infty_pow {I : Type u_3} {B : I → Type u_4} [(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 nat_cast_memℓp_infty {I : Type u_3} {B : I → Type u_4} [(i : I) → NormedRing (B i)] [∀ (i : I), NormOneClass (B i)] (n : ℕ) :

Memℓp ↑n ⊤

theorem int_cast_memℓp_infty {I : Type u_3} {B : I → Type u_4} [(i : I) → NormedRing (B i)] [∀ (i : I), NormOneClass (B i)] (z : ℤ) :

Memℓp ↑z ⊤

@[simp]

theorem lp.infty_coeFn_one {I : Type u_3} {B : I → Type 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 : I → Type u_4} [(i : I) → NormedRing (B i)] [∀ (i : I), NormOneClass (B i)] (f : { x // x ∈ lp B ⊤ }) (n : ℕ) :

↑(f ^ n) = ↑f ^ n

@[simp]

theorem lp.infty_coeFn_nat_cast {I : Type u_3} {B : I → Type u_4} [(i : I) → NormedRing (B i)] [∀ (i : I), NormOneClass (B i)] (n : ℕ) :

↑↑n = ↑n

@[simp]

theorem lp.infty_coeFn_int_cast {I : Type u_3} {B : I → Type u_4} [(i : I) → NormedRing (B i)] [∀ (i : I), NormOneClass (B i)] (z : ℤ) :

↑↑z = ↑z

instance lp.instNormOneClassSubtypePreLpToNormedAddCommGroupToNonUnitalNormedRingMemAddSubgroupToAddGroupInstAddCommGroupPreLpInstMembershipInstSetLikeAddSubgroupLpTopENNRealToTopToCompleteLatticeToCompletelyDistribLatticeInstCompleteLinearOrderENNRealInstNormSubtypePreLpMemAddSubgroupToAddGroupInstAddCommGroupPreLpInstMembershipInstSetLikeAddSubgroupLpToOneToSemiringInftyRing {I : Type u_3} {B : I → Type u_4} [(i : I) → NormedRing (B i)] [∀ (i : I), NormOneClass (B i)] [Nonempty I] :

NormOneClass { x // x ∈ lp B ⊤ }

instance lp.inftyNormedRing {I : Type u_3} {B : I → Type u_4} [(i : I) → NormedRing (B i)] [∀ (i : I), NormOneClass (B i)] :

NormedRing { x // x ∈ lp B ⊤ }

instance lp.inftyCommRing {I : Type u_3} {B : I → Type u_4} [(i : I) → NormedCommRing (B i)] [∀ (i : I), NormOneClass (B i)] :

CommRing { x // x ∈ lp B ⊤ }

instance lp.inftyNormedCommRing {I : Type u_3} {B : I → Type u_4} [(i : I) → NormedCommRing (B i)] [∀ (i : I), NormOneClass (B i)] :

NormedCommRing { x // x ∈ lp B ⊤ }

instance Pi.algebraOfNormedAlgebra {I : Type u_3} {𝕜 : Type u_4} {B : I → Type u_5} [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.

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

Algebra 𝕜 (PreLp B)

theorem algebraMap_memℓp_infty {I : Type u_3} {𝕜 : Type u_4} {B : I → Type u_5} [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 {I : Type u_3} (𝕜 : Type u_4) (B : I → Type u_5) [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.

Instances For

instance lp.inftyNormedAlgebra {I : Type u_3} {𝕜 : Type u_4} {B : I → Type u_5} [NormedField 𝕜] [(i : I) → NormedRing (B i)] [(i : I) → NormedAlgebra 𝕜 (B i)] [∀ (i : I), NormOneClass (B i)] :

NormedAlgebra 𝕜 { x // x ∈ lp B ⊤ }

def lp.single {α : Type u_1} {E : α → Type u_2} [(i : α) → NormedAddCommGroup (E i)] [DecidableEq α] (p : ENNReal) (i : α) (a : E i) :

{ x // x ∈ lp E p }

The element of lp E p which is a : E i at the index i, and zero elsewhere.

Instances For

theorem lp.single_apply {α : Type u_1} {E : α → Type u_2} [(i : α) → NormedAddCommGroup (E i)] [DecidableEq α] (p : ENNReal) (i : α) (a : E i) (j : α) :

↑(lp.single p i a) j = if h : j = i then (_ : i = j) ▸ a else 0

theorem lp.single_apply_self {α : Type u_1} {E : α → Type u_2} [(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_1} {E : α → Type u_2} [(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_neg {α : Type u_1} {E : α → Type u_2} [(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_smul {α : Type u_1} {E : α → Type u_2} [(i : α) → NormedAddCommGroup (E i)] {𝕜 : Type u_3} [NormedRing 𝕜] [(i : α) → Module 𝕜 (E i)] [∀ (i : α), BoundedSMul 𝕜 (E i)] [DecidableEq α] (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)] [DecidableEq α] (hp : 0 < ENNReal.toReal p) (f : (i : α) → E i) (s : Finset α) :

‖Finset.sum s fun i => lp.single p i (f i)‖ ^ ENNReal.toReal p = Finset.sum s fun i => ‖f i‖ ^ ENNReal.toReal p

theorem lp.norm_single {α : Type u_1} {E : α → Type u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [DecidableEq α] (hp : 0 < ENNReal.toReal p) (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)] [DecidableEq α] (hp : 0 < ENNReal.toReal p) (f : { x // x ∈ lp E p }) (s : Finset α) :

‖f‖ ^ ENNReal.toReal p - ‖f - Finset.sum s fun i => lp.single p i (↑f i)‖ ^ ENNReal.toReal p = Finset.sum s fun i => ‖↑f i‖ ^ ENNReal.toReal p

theorem lp.norm_compl_sum_single {α : Type u_1} {E : α → Type u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [DecidableEq α] (hp : 0 < ENNReal.toReal p) (f : { x // x ∈ lp E p }) (s : Finset α) :

‖f - Finset.sum s fun i => lp.single p i (↑f i)‖ ^ ENNReal.toReal p = ‖f‖ ^ ENNReal.toReal p - Finset.sum s fun i => ‖↑f i‖ ^ ENNReal.toReal p

theorem lp.hasSum_single {α : Type u_1} {E : α → Type u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [DecidableEq α] [Fact (1 ≤ p)] (hp : p ≠ ⊤) (f : { x // x ∈ 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 : Filter ι} [Filter.NeBot l] {C : ℝ} {F : ι → { x // x ∈ 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 : Filter ι} [Filter.NeBot l] [_i : Fact (1 ≤ p)] (hp : p ≠ ⊤) {C : ℝ} {F : ι → { x // x ∈ 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 α) :

(Finset.sum s fun i => ‖f i‖ ^ ENNReal.toReal p) ≤ C ^ ENNReal.toReal p

theorem lp.norm_le_of_tendsto {α : Type u_1} {E : α → Type u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {ι : Type u_3} {l : Filter ι} [Filter.NeBot l] [_i : Fact (1 ≤ p)] {C : ℝ} {F : ι → { x // x ∈ lp E p }} (hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C) {f : { x // x ∈ 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 : Filter ι} [Filter.NeBot l] [_i : Fact (1 ≤ p)] {F : ι → { x // x ∈ lp E p }} (hF : Bornology.IsBounded (Set.range F)) {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 : ℕ → { x // x ∈ lp E p }} (hF : CauchySeq F) {f : { x // x ∈ 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 { x // x ∈ lp E p }

theorem LipschitzWith.uniformly_bounded {α : Type u_1} {ι : Type u_3} [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_1} {ι : Type u_3} [PseudoMetricSpace α] (f : α → { x // x ∈ 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_1} {ι : Type u_3} [PseudoMetricSpace α] {f : α → { x // x ∈ lp (fun i => ℝ) ⊤ }} (K : NNReal) :

LipschitzWith K f ↔ ∀ (i : ι), LipschitzWith K fun a => ↑(f a) i