Real and complex inner-product spaces and their induced length

Let $\mathbb{F}$ be $\mathbb{R}$ or $\mathbb{C}$, with conjugation $z\mapsto \bar{z}$ the identity on $\mathbb{R}$ and complex conjugation on $\mathbb{C}$ (Real and imaginary parts, complex conjugation, and modulus). A real or complex inner-product space is an $\mathbb{F}$-vector space $V$ together with an inner product $⟨\cdot ,\cdot ⟩:V\times V\to \mathbb{F}$ in the sense of Real and complex inner product spaces, with the inner product linear in the first argument: for all $u,v,w\in V$ and $a,b\in \mathbb{F}$,

$⟨au+bv,w⟩=a⟨u,w⟩+b⟨v,w⟩,⟨u,v⟩=\overline{⟨v,u⟩},⟨v,v⟩\ge 0,⟨v,v⟩=0⟺v=0.$

Conjugate-linearity in the second argument. Conjugate symmetry together with linearity in the first argument gives, for all $w\in V$,

$⟨w,au+bv⟩=\overline{⟨au+bv,w⟩}=\overline{a⟨u,w⟩+b⟨v,w⟩}=\bar{a}⟨w,u⟩+\bar{b}⟨w,v⟩\mathrm{.}$

Induced length. The induced length, or inner-product norm, of $v$ is

$\mathrm{\parallel }v\mathrm{\parallel }:=\sqrt{⟨v,v⟩},$

which is exactly the published The norm $\parallel v\parallel =\sqrt{⟨v,v⟩}$ induced by a real or complex inner product: positive definiteness makes $⟨v,v⟩$ a nonnegative real with a unique nonnegative square root, so that $\mathrm{\parallel }v\mathrm{\parallel }\ge 0$, $\mathrm{\parallel }v\mathrm{\parallel }=0$ exactly for $v=0$, and $⟨v,v⟩=\mathrm{\parallel }v{\mathrm{\parallel }}^2$.

The convention on this page. Every inner-product space below is real or complex in this sense, the pairing is linear in the first argument and conjugate-linear in the second, and $\mathrm{\parallel }v\mathrm{\parallel }$ always denotes the induced length. In the real case conjugation is the identity and $\mathrm{\mid }z\mathrm{\mid }$ is the absolute value of $\mathbb{R}$; in the complex case they are complex conjugation and the complex modulus. All statements below are therefore written once and read in either scalar field.