An inner product space is a vector space endowed with an inner product. It generalizes the notion of dot product in ℝ^n and provides the means of defining the length of a vector and the angle between two vectors. In particular vectors x and y are orthogonal if their inner product equals zero.

Main statements

Existence of orthogonal projection onto nonempty complete subspace: Let u be a point in an inner product space, and let K be a nonempty complete subspace. Then there exists a unique v in K that minimizes the distance ∥u - v∥ to u. The point v is usually called the orthogonal projection of u onto K.

Implementation notes

We decide to develop the theory of real inner product spaces and that of complex inner product spaces separately.

inner_product_space

An inner product space is a real vector space with an additional operation called inner product. Inner product spaces over complex vector space will be defined in another file.

inner_add_add_self

Expand inner (x + y) (x + y)

inner_sub_sub_self

Expand inner (x - y) (x - y)

parallelogram_law

Parallelogram law

inner_mul_inner_self_le

Cauchy–Schwarz inequality

inner_product_space_has_norm

An inner product naturally induces a norm.

norm_add_pow_two

Expand the square

norm_add_mul_self

Same lemma as above but in a different form

norm_sub_pow_two

Expand the square

norm_sub_mul_self

Same lemma as above but in a different form

abs_inner_le_norm

Cauchy–Schwarz inequality with norm

inner_product_space_is_normed_group

An inner product space forms a normed group w.r.t. its associated norm.

inner_product_space_is_normed_space

An inner product space forms a normed space over reals w.r.t. its associated norm.

exists_norm_eq_infi_of_complete_convex

Existence of minimizers Let u be a point in an inner product space, and let K be a nonempty complete convex subset. Then there exists a unique v in K that minimizes the distance ∥u - v∥ to u.

norm_eq_infi_iff_inner_le_zero

Characterization of minimizers in the above theorem

exists_norm_eq_infi_of_complete_subspace

Existence of minimizers. Let u be a point in an inner product space, and let K be a nonempty complete subspace. Then there exists a unique v in K that minimizes the distance ∥u - v∥ to u. This point v is usually called the orthogonal projection of u onto K.

norm_eq_infi_iff_inner_eq_zero

Characterization of minimizers in the above theorem. Let u be a point in an inner product space, and let K be a nonempty subspace. Then point v minimizes the distance ∥u - v∥ if and only if for all w ∈ K, inner (u - v) w = 0 (i.e., u - v is orthogonal to the subspace K)

Inner Product Space