Theorems · Definition · functional analysis

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

Defined in

Mathlib.Analysis.Normed.Lp.lpSpace

Cited by

163 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 2 definitions · uses no axioms

Assumes

NormedAddCommGroup