Inner Product Space
This file defines real inner product space and proves its basic properties.
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.
Tags
inner product space, norm, orthogonal projection
References
- [Clément & Martin, The Lax-Milgram Theorem. A detailed proof to be formalized in Coq]
- [Clément & Martin, A Coq formal proof of the Lax–Milgram theorem]
The Coq code is available at the following address: http://www.lri.fr/~sboldo/elfic/index.html
- to_normed_group : normed_group α
- to_normed_space : normed_space ℝ α
- to_has_inner : has_inner α
- norm_eq_sqrt_inner : ∀ (x : α), ∥x∥ = real.sqrt (has_inner.inner x x)
- comm : ∀ (x y : α), has_inner.inner x y = has_inner.inner y x
- add_left : ∀ (x y z : α), has_inner.inner (x + y) z = has_inner.inner x z + has_inner.inner y z
- smul_left : ∀ (x y : α) (r : ℝ), has_inner.inner (r • x) y = r * has_inner.inner x y
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.
The norm could be derived from the inner product, instead we require the existence of a norm and
the fact that it is equal to sqrt (inner x x) to be able to put instances on ℝ or product
spaces.
To construct a norm from an inner product, see inner_product_space.of_core.
Constructing a normed space structure from a scalar product
In the definition of an inner product space, we require the existence of a norm, which is equal
(but maybe not defeq) to the square root of the scalar product. This makes it possible to put
an inner product space structure on spaces with a preexisting norm (for instance ℝ), with good
properties. However, sometimes, one would like to define the norm starting only from a well-behaved
scalar product. This is what we implement in this paragraph, starting from a structure
inner_product_space.core stating that we have a nice scalar product.
Our goal here is not to develop a whole theory with all the supporting API, as this will be done
below for inner_product_space. Instead, we implement the bare minimum to go as directly as
possible to the construction of the norm and the proof of the triangular inequality.
- inner : F → F → ℝ
- comm : ∀ (x y : F), c.inner x y = c.inner y x
- nonneg : ∀ (x : F), 0 ≤ c.inner x x
- definite : ∀ (x : F), c.inner x x = 0 → x = 0
- add_left : ∀ (x y z : F), c.inner (x + y) z = c.inner x z + c.inner y z
- smul_left : ∀ (x y : F) (r : ℝ), c.inner (r • x) y = r * c.inner x y
A structure requiring that a scalar product is positive definite and symmetric, from which one
can construct an inner_product_space instance in inner_product_space.of_core.
Inner product constructed from an inner_product_space.core structure
Equations
Norm constructed from an inner_product_space.core structure, defined to be the square root
of the scalar product.
Equations
- inner_product_space.of_core.to_has_norm = {norm := λ (x : F), real.sqrt (has_inner.inner x x)}
Expand inner (x + y) (x + y)
Cauchy–Schwarz inequality
Cauchy–Schwarz inequality with norm
Normed group structure constructed from an inner_product_space.core structure.
Equations
- inner_product_space.of_core.to_normed_group = normed_group.of_core F inner_product_space.of_core.to_normed_group._proof_1
Normed space structure constructed from an inner_product_space.core structure.
Equations
- inner_product_space.of_core.to_normed_space = {to_semimodule := _inst_2, norm_smul_le := _}
Given an inner_product_space.core structure on a space, one can use it to turn the space into
an inner product space, constructing the norm out of the inner product.
Equations
- inner_product_space.of_core c = let _inst : normed_group F := inner_product_space.of_core.to_normed_group, _inst_3 : normed_space ℝ F := inner_product_space.of_core.to_normed_space in {to_normed_group := _inst, to_normed_space := _inst_3, to_has_inner := {inner := c.inner}, norm_eq_sqrt_inner := _, comm := _, add_left := _, smul_left := _}
Properties of inner product spaces
The inner product as a bilinear form.
Equations
- bilin_form_of_inner α = {bilin := has_inner.inner inner_product_space.to_has_inner, bilin_add_left := _, bilin_smul_left := _, bilin_add_right := _, bilin_smul_right := _}
An inner product with a sum on the left.
An inner product with a sum on the right.
Expand inner (x + y) (x + y)
Expand inner (x - y) (x - y)
Parallelogram law
Cauchy–Schwarz inequality
Cauchy–Schwarz inequality with norm
The inner product of two vectors, divided by the product of their norms, has absolute value at most 1.
The inner product of a vector with a multiple of itself.
The inner product of a vector with a multiple of itself.
The inner product of a nonzero vector with a nonzero multiple of itself, divided by the product of their norms, has absolute value 1.
The inner product of a nonzero vector with a positive multiple of itself, divided by the product of their norms, has value 1.
The inner product of a nonzero vector with a negative multiple of itself, divided by the product of their norms, has value -1.
The inner product of two vectors, divided by the product of their norms, has absolute value 1 if and only if they are nonzero and one is a multiple of the other. One form of equality case for Cauchy-Schwarz.
The inner product of two vectors, divided by the product of their norms, has value 1 if and only if they are nonzero and one is a positive multiple of the other.
The inner product of two vectors, divided by the product of their norms, has value -1 if and only if they are nonzero and one is a negative multiple of the other.
The inner product of two weighted sums, where the weights in each sum add to 0, in terms of the norms of pairwise differences.
Inner product space structure on product spaces
If ι is a finite type and each space f i, i : ι, is an inner product space,
then Π i, f i is an inner product space as well. Since Π i, f i is endowed with the sup norm,
we use instead pi_Lp 2 one_le_two f for the product space, which is endowed with the L^2 norm.
Equations
- pi_Lp.inner_product_space ι f = {to_normed_group := pi_Lp.normed_group 2 one_le_two f (λ (i : ι), inner_product_space.to_normed_group), to_normed_space := pi_Lp.normed_space 2 one_le_two f ℝ (λ (i : ι), inner_product_space.to_normed_space), to_has_inner := {inner := λ (x y : pi_Lp 2 one_le_two f), finset.univ.sum (λ (i : ι), has_inner.inner (x i) (y i))}, norm_eq_sqrt_inner := _, comm := _, add_left := _, smul_left := _}
The type of real numbers is an inner product space.
Equations
- real.inner_product_space = {to_normed_group := normed_ring.to_normed_group normed_field.to_normed_ring, to_normed_space := normed_field.to_normed_space real.normed_field, to_has_inner := {inner := has_mul.mul real.has_mul}, norm_eq_sqrt_inner := real.inner_product_space._proof_1, comm := _, add_left := real.inner_product_space._proof_2, smul_left := real.inner_product_space._proof_3}
The standard Euclidean space, functions on a finite type. For an n-dimensional space
use euclidean_space (fin n).
Equations
- euclidean_space n = pi_Lp 2 one_le_two (λ (i : n), ℝ)
Orthogonal projection in inner product spaces
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.
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.
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)
The orthogonal projection onto a complete subspace, as an
unbundled function. This definition is only intended for use in
setting up the bundled version orthogonal_projection and should not
be used once that is defined.
Equations
- orthogonal_projection_fn h v = _.some
The unbundled orthogonal projection is in the given subspace. This lemma is only intended for use in setting up the bundled version and should not be used once that is defined.
The characterization of the unbundled orthogonal projection. This lemma is only intended for use in setting up the bundled version and should not be used once that is defined.
The unbundled orthogonal projection is the unique point in K
with the orthogonality property. This lemma is only intended for use
in setting up the bundled version and should not be used once that is
defined.
The orthogonal projection onto a complete subspace.
Equations
- orthogonal_projection h = {to_fun := orthogonal_projection_fn h, map_add' := _, map_smul' := _}
The orthogonal projection is in the given subspace.
The characterization of the orthogonal projection.
The orthogonal projection is the unique point in K with the
orthogonality property.
The subspace of vectors orthogonal to a given subspace.
Equations
- K.orthogonal = {carrier := {v : α | ∀ (u : α), u ∈ K → has_inner.inner u v = 0}, zero_mem' := _, add_mem' := _, smul_mem' := _}
When a vector is in K.orthogonal.
When a vector is in K.orthogonal, with the inner product the
other way round.
A vector in K is orthogonal to one in K.orthogonal.
A vector in K.orthogonal is orthogonal to one in K.
K and K.orthogonal have trivial intersection.
submodule.orthogonal gives a galois_connection between
submodule ℝ α and its order_dual.
K is contained in K.orthogonal.orthogonal.
The inf of two orthogonal subspaces equals the subspace orthogonal to the sup.
The inf of an indexed family of orthogonal subspaces equals the subspace orthogonal to the sup.
The inf of a set of orthogonal subspaces equals the subspace orthogonal to the sup.
If K is complete, K and K.orthogonal span the whole
space.
If K is complete, K and K.orthogonal are complements of each
other.