Extended norm #
In this file we define a structure
ENorm 𝕜 V representing an extended norm (i.e., a norm that can
take the value
∞) on a vector space
V over a normed field
𝕜. We do not use
ENorm because the same space can have more than one extended norm. For example, the space of
f : α → ℝ has a family of
L_p extended norms.
We prove some basic inequalities, then define
e : ENorm 𝕜 V;
- the subspace of vectors with finite norm, called
NormedSpacestructure on this space.
The last definition is an instance because the type involves
Implementation notes #
We do not define extended normed groups. They can be added to the chain once someone will need them.
normed space, extended norm
- toFun : V → ENNReal
Extended norm on a vector space. As in the case of normed spaces, we require only
‖c • x‖ ≤ ‖c‖ * ‖x‖ in the definition, then prove an equality in