Structures · Analysis

InnerProductSpace

A (pre) inner product space is a vector space with an additional operation called inner product. The (semi)norm could be derived from the inner product, instead we require the existence of a seminorm and the fact that ‖x‖^2 = re ⟪x, x⟫ to be able to put instances on 𝕂 or product spaces. Note that NormedSpace does not assume that ‖x‖=0 implies x=0 (it is rather a seminorm). To construct a seminorm from an inner product, see PreInnerProductSpace.ofCore.

Defined in

Mathlib.Analysis.InnerProductSpace.Defs

Shape

2 explicit arguments · adds norm_sq_eq_re_inner, conj_inner_symm, add_left, smul_left