# mathlibdocumentation

analysis.normed_space.inner_product

# Inner Product Space

This file defines inner product spaces 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. We define both the real and complex cases at the same time using the is_R_or_C typeclass.

## Main results

• We define the class inner_product_space π E extending normed_space π E with a number of basic properties, most notably the Cauchy-Schwarz inequality. Here π is understood to be either β or β, through the is_R_or_C typeclass.
• We show that if f i is an inner product space for each i, then so is Ξ  i, f i
• We define euclidean_space π n to be n β π for any fintype n, and show that this an inner product space.
• 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.

## Notation

We globally denote the real and complex inner products by βͺΒ·, Β·β«_β and βͺΒ·, Β·β«_β respectively. We also provide two notation namespaces: real_inner_product_space, complex_inner_product_space, which respectively introduce the plain notation βͺΒ·, Β·β« for the the real and complex inner product.

## Implementation notes

We choose the convention that inner products are conjugate linear in the first argument and linear in the second.

## TODO

• Fix the section on the existence of minimizers and orthogonal projections to make sure that it also applies in the complex case.

## Tags

inner product space, norm

## 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

@[class]
structure has_inner (π : Type u_4) (E : Type u_5) :
Type (max u_4 u_5)
• inner : E β E β π

Syntactic typeclass for types endowed with an inner product

Instances
@[class]
structure inner_product_space (π : Type u_4) (E : Type u_5) [is_R_or_C π] :
Type (max u_4 u_5)

An inner product space is a vector space with an additional operation called inner product. The norm could be derived from the inner product, instead we require the existence of a norm and the fact that β₯xβ₯^2 = re βͺ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.

Instances

### Constructing a normed space structure from an inner 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.

Warning: Do not use this core structure if the space you are interested in already has a norm instance defined on it, otherwise this will create a second non-defeq norm instance!

@[nolint, class]
structure inner_product_space.core (π : Type u_4) (F : Type u_5) [is_R_or_C π] [semimodule π F] :
Type (max u_4 u_5)

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.

def inner_product_space.of_core.to_has_inner {π : Type u_1} {F : Type u_3} [is_R_or_C π] [semimodule π F] [c : F] :
has_inner π F

Inner product defined by the inner_product_space.core structure.

Equations
def inner_product_space.of_core.norm_sq {π : Type u_1} {F : Type u_3} [is_R_or_C π] [semimodule π F] [c : F] (x : F) :

The norm squared function for inner_product_space.core structure.

Equations
theorem inner_product_space.of_core.inner_conj_sym {π : Type u_1} {F : Type u_3} [is_R_or_C π] [semimodule π F] [c : F] (x y : F) :

theorem inner_product_space.of_core.inner_self_nonneg {π : Type u_1} {F : Type u_3} [is_R_or_C π] [semimodule π F] [c : F] {x : F} :

theorem inner_product_space.of_core.inner_self_nonneg_im {π : Type u_1} {F : Type u_3} [is_R_or_C π] [semimodule π F] [c : F] {x : F} :

theorem inner_product_space.of_core.inner_self_im_zero {π : Type u_1} {F : Type u_3} [is_R_or_C π] [semimodule π F] [c : F] {x : F} :

theorem inner_product_space.of_core.inner_add_left {π : Type u_1} {F : Type u_3} [is_R_or_C π] [semimodule π F] [c : F] {x y z : F} :
inner (x + y) z = z + z

theorem inner_product_space.of_core.inner_add_right {π : Type u_1} {F : Type u_3} [is_R_or_C π] [semimodule π F] [c : F] {x y z : F} :
(y + z) = y + z

theorem inner_product_space.of_core.inner_norm_sq_eq_inner_self {π : Type u_1} {F : Type u_3} [is_R_or_C π] [semimodule π F] [c : F] (x : F) :

theorem inner_product_space.of_core.inner_re_symm {π : Type u_1} {F : Type u_3} [is_R_or_C π] [semimodule π F] [c : F] {x y : F} :

theorem inner_product_space.of_core.inner_im_symm {π : Type u_1} {F : Type u_3} [is_R_or_C π] [semimodule π F] [c : F] {x y : F} :

theorem inner_product_space.of_core.inner_smul_left {π : Type u_1} {F : Type u_3} [is_R_or_C π] [semimodule π F] [c : F] {x y : F} {r : π} :
inner (r β’ x) y = * y

theorem inner_product_space.of_core.inner_smul_right {π : Type u_1} {F : Type u_3} [is_R_or_C π] [semimodule π F] [c : F] {x y : F} {r : π} :
(r β’ y) = r * y

theorem inner_product_space.of_core.inner_zero_left {π : Type u_1} {F : Type u_3} [is_R_or_C π] [semimodule π F] [c : F] {x : F} :
x = 0

theorem inner_product_space.of_core.inner_zero_right {π : Type u_1} {F : Type u_3} [is_R_or_C π] [semimodule π F] [c : F] {x : F} :
0 = 0

theorem inner_product_space.of_core.inner_self_eq_zero {π : Type u_1} {F : Type u_3} [is_R_or_C π] [semimodule π F] [c : F] {x : F} :
x = 0 β x = 0

theorem inner_product_space.of_core.inner_self_re_to_K {π : Type u_1} {F : Type u_3} [is_R_or_C π] [semimodule π F] [c : F] {x : F} :

theorem inner_product_space.of_core.inner_abs_conj_sym {π : Type u_1} {F : Type u_3} [is_R_or_C π] [semimodule π F] [c : F] {x y : F} :

theorem inner_product_space.of_core.inner_neg_left {π : Type u_1} {F : Type u_3} [is_R_or_C π] [semimodule π F] [c : F] {x y : F} :
inner (-x) y = - y

theorem inner_product_space.of_core.inner_neg_right {π : Type u_1} {F : Type u_3} [is_R_or_C π] [semimodule π F] [c : F] {x y : F} :
(-y) = - y

theorem inner_product_space.of_core.inner_sub_left {π : Type u_1} {F : Type u_3} [is_R_or_C π] [semimodule π F] [c : F] {x y z : F} :
inner (x - y) z = z - z

theorem inner_product_space.of_core.inner_sub_right {π : Type u_1} {F : Type u_3} [is_R_or_C π] [semimodule π F] [c : F] {x y z : F} :
(y - z) = y - z

theorem inner_product_space.of_core.inner_mul_conj_re_abs {π : Type u_1} {F : Type u_3} [is_R_or_C π] [semimodule π F] [c : F] {x y : F} :

theorem inner_product_space.of_core.inner_add_add_self {π : Type u_1} {F : Type u_3} [is_R_or_C π] [semimodule π F] [c : F] {x y : F} :
inner (x + y) (x + y) = x + y + x + y

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

theorem inner_product_space.of_core.inner_sub_sub_self {π : Type u_1} {F : Type u_3} [is_R_or_C π] [semimodule π F] [c : F] {x y : F} :
inner (x - y) (x - y) = x - y - x + y

theorem inner_product_space.of_core.inner_mul_inner_self_le {π : Type u_1} {F : Type u_3} [is_R_or_C π] [semimodule π F] [c : F] (x y : F) :

CauchyβSchwarz inequality. This proof follows "Proof 2" on Wikipedia. We need this for the core structure to prove the triangle inequality below when showing the core is a normed group.

def inner_product_space.of_core.to_has_norm {π : Type u_1} {F : Type u_3} [is_R_or_C π] [semimodule π F] [c : F] :

Norm constructed from a inner_product_space.core structure, defined to be the square root of the scalar product.

Equations
theorem inner_product_space.of_core.norm_eq_sqrt_inner {π : Type u_1} {F : Type u_3} [is_R_or_C π] [semimodule π F] [c : F] (x : F) :

theorem inner_product_space.of_core.inner_self_eq_norm_square {π : Type u_1} {F : Type u_3} [is_R_or_C π] [semimodule π F] [c : F] (x : F) :

theorem inner_product_space.of_core.sqrt_norm_sq_eq_norm {π : Type u_1} {F : Type u_3} [is_R_or_C π] [semimodule π F] [c : F] {x : F} :

theorem inner_product_space.of_core.abs_inner_le_norm {π : Type u_1} {F : Type u_3} [is_R_or_C π] [semimodule π F] [c : F] (x y : F) :

CauchyβSchwarz inequality with norm

def inner_product_space.of_core.to_normed_group {π : Type u_1} {F : Type u_3} [is_R_or_C π] [semimodule π F] [c : F] :

Normed group structure constructed from an inner_product_space.core structure

Equations
def inner_product_space.of_core.to_normed_space {π : Type u_1} {F : Type u_3} [is_R_or_C π] [semimodule π F] [c : F] :
normed_space π F

Normed space structure constructed from a inner_product_space.core structure

Equations
def inner_product_space.of_core {π : Type u_1} {F : Type u_3} [is_R_or_C π] [semimodule π F] (c : F) :
F

Given a 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

### Properties of inner product spaces

theorem inner_conj_sym {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] (x y : E) :

theorem real_inner_comm {F : Type u_3} (x y : F) :
x = y

theorem inner_eq_zero_sym {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {x y : E} :
y = 0 β x = 0

theorem inner_self_nonneg_im {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {x : E} :

theorem inner_self_im_zero {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {x : E} :

theorem inner_add_left {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {x y z : E} :
inner (x + y) z = z + z

theorem inner_add_right {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {x y z : E} :
(y + z) = y + z

theorem inner_re_symm {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {x y : E} :

theorem inner_im_symm {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {x y : E} :

theorem inner_smul_left {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {x y : E} {r : π} :
inner (r β’ x) y = * y

theorem real_inner_smul_left {F : Type u_3} {x y : F} {r : β} :
inner (r β’ x) y = r * y

theorem inner_smul_real_left {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {x y : E} {r : β} :

theorem inner_smul_right {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {x y : E} {r : π} :
(r β’ y) = r * y

theorem real_inner_smul_right {F : Type u_3} {x y : F} {r : β} :
(r β’ y) = r * y

theorem inner_smul_real_right {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {x y : E} {r : β} :

def sesq_form_of_inner {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] :
sesq_form π E

The inner product as a sesquilinear form.

Equations
def bilin_form_of_real_inner {F : Type u_3}  :

The real inner product as a bilinear form.

Equations
theorem sum_inner {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {ΞΉ : Type u_3} (s : finset ΞΉ) (f : ΞΉ β E) (x : E) :
inner (β (i : ΞΉ) in s, f i) x = β (i : ΞΉ) in s, inner (f i) x

An inner product with a sum on the left.

theorem inner_sum {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {ΞΉ : Type u_3} (s : finset ΞΉ) (f : ΞΉ β E) (x : E) :
(β (i : ΞΉ) in s, f i) = β (i : ΞΉ) in s, (f i)

An inner product with a sum on the right.

@[simp]
theorem inner_zero_left {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {x : E} :
x = 0

theorem inner_re_zero_left {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {x : E} :

@[simp]
theorem inner_zero_right {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {x : E} :
0 = 0

theorem inner_re_zero_right {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {x : E} :

theorem inner_self_nonneg {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {x : E} :

theorem real_inner_self_nonneg {F : Type u_3} {x : F} :

@[simp]
theorem inner_self_eq_zero {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {x : E} :
x = 0 β x = 0

@[simp]
theorem inner_self_nonpos {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {x : E} :

theorem real_inner_self_nonpos {F : Type u_3} {x : F} :
x β€ 0 β x = 0

@[simp]
theorem inner_self_re_to_K {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {x : E} :

theorem inner_self_re_abs {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {x : E} :

theorem inner_self_abs_to_K {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {x : E} :

theorem real_inner_self_abs {F : Type u_3} {x : F} :
abs (inner x x) = x

theorem inner_abs_conj_sym {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {x y : E} :

@[simp]
theorem inner_neg_left {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {x y : E} :
inner (-x) y = - y

@[simp]
theorem inner_neg_right {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {x y : E} :
(-y) = - y

theorem inner_neg_neg {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {x y : E} :
inner (-x) (-y) = y

@[simp]
theorem inner_self_conj {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {x : E} :

theorem inner_sub_left {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {x y z : E} :
inner (x - y) z = z - z

theorem inner_sub_right {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {x y z : E} :
(y - z) = y - z

theorem inner_mul_conj_re_abs {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {x y : E} :

theorem inner_add_add_self {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {x y : E} :
inner (x + y) (x + y) = x + y + x + y

Expand βͺx + y, x + yβ«

inner (x + y) (x + y) = x + 2 * y + y

Expand βͺx + y, x + yβ«_β

theorem inner_sub_sub_self {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {x y : E} :
inner (x - y) (x - y) = x - y - x + y

theorem real_inner_sub_sub_self {F : Type u_3} {x y : F} :
inner (x - y) (x - y) = x - 2 * y + y

Expand βͺx - y, x - yβ«_β

theorem parallelogram_law {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {x y : E} :
inner (x + y) (x + y) + inner (x - y) (x - y) = 2 * (inner x x + y)

Parallelogram law

theorem inner_mul_inner_self_le {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] (x y : E) :

CauchyβSchwarz inequality. This proof follows "Proof 2" on Wikipedia.

theorem real_inner_mul_inner_self_le {F : Type u_3} (x y : F) :
(inner x y) * y β€ (inner x x) * y

CauchyβSchwarz inequality for real inner products.

theorem linear_independent_of_ne_zero_of_inner_eq_zero {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {ΞΉ : Type u_3} {v : ΞΉ β E} (hz : β (i : ΞΉ), v i β  0) (ho : β (i j : ΞΉ), i β  j β inner (v i) (v j) = 0) :
v

A family of vectors is linearly independent if they are nonzero and orthogonal.

theorem norm_eq_sqrt_inner {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] (x : E) :

theorem norm_eq_sqrt_real_inner {F : Type u_3} (x : F) :

theorem inner_self_eq_norm_square {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] (x : E) :

theorem real_inner_self_eq_norm_square {F : Type u_3} (x : F) :
x =

theorem norm_add_pow_two {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {x y : E} :

Expand the square

theorem norm_add_pow_two_real {F : Type u_3} {x y : F} :

Expand the square

theorem norm_add_mul_self {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {x y : E} :

Expand the square

theorem norm_add_mul_self_real {F : Type u_3} {x y : F} :

Expand the square

theorem norm_sub_pow_two {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {x y : E} :

Expand the square

theorem norm_sub_pow_two_real {F : Type u_3} {x y : F} :

Expand the square

theorem norm_sub_mul_self {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {x y : E} :

Expand the square

theorem norm_sub_mul_self_real {F : Type u_3} {x y : F} :

Expand the square

theorem abs_inner_le_norm {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] (x y : E) :

CauchyβSchwarz inequality with norm

theorem abs_real_inner_le_norm {F : Type u_3} (x y : F) :

CauchyβSchwarz inequality with norm

theorem parallelogram_law_with_norm {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {x y : E} :

Polarization identity: The real inner product, in terms of the norm.

Polarization identity: The real inner product, in terms of the norm.

Pythagorean theorem, if-and-only-if vector inner product form.

theorem norm_add_square_eq_norm_square_add_norm_square_of_inner_eq_zero {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] (x y : E) (h : y = 0) :

Pythagorean theorem, vector inner product form.

theorem norm_add_square_eq_norm_square_add_norm_square_real {F : Type u_3} {x y : F} (h : y = 0) :

Pythagorean theorem, vector inner product form.

Pythagorean theorem, subtracting vectors, if-and-only-if vector inner product form.

theorem norm_sub_square_eq_norm_square_add_norm_square_real {F : Type u_3} {x y : F} (h : y = 0) :

Pythagorean theorem, subtracting vectors, vector inner product form.

theorem real_inner_add_sub_eq_zero_iff {F : Type u_3} (x y : F) :
inner (x + y) (x - y) = 0 β

The sum and difference of two vectors are orthogonal if and only if they have the same norm.

theorem abs_real_inner_div_norm_mul_norm_le_one {F : Type u_3} (x y : F) :

The real inner product of two vectors, divided by the product of their norms, has absolute value at most 1.

theorem real_inner_smul_self_left {F : Type u_3} (x : F) (r : β) :
inner (r β’ x) x = r *

The inner product of a vector with a multiple of itself.

theorem real_inner_smul_self_right {F : Type u_3} (x : F) (r : β) :
(r β’ x) = r *

The inner product of a vector with a multiple of itself.

theorem abs_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {x : E} {r : π} (hx : x β  0) (hr : r β  0) :

The inner product of a nonzero vector with a nonzero multiple of itself, divided by the product of their norms, has absolute value 1.

theorem abs_real_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul {F : Type u_3} {x : F} {r : β} (hx : x β  0) (hr : r β  0) :

The inner product of a nonzero vector with a nonzero multiple of itself, divided by the product of their norms, has absolute value 1.

theorem real_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_pos_mul {F : Type u_3} {x : F} {r : β} (hx : x β  0) (hr : 0 < r) :

The inner product of a nonzero vector with a positive multiple of itself, divided by the product of their norms, has value 1.

theorem real_inner_div_norm_mul_norm_eq_neg_one_of_ne_zero_of_neg_mul {F : Type u_3} {x : F} {r : β} (hx : x β  0) (hr : r < 0) :

The inner product of a nonzero vector with a negative multiple of itself, divided by the product of their norms, has value -1.

theorem abs_inner_div_norm_mul_norm_eq_one_iff {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] (x y : E) :

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.

theorem abs_real_inner_div_norm_mul_norm_eq_one_iff {F : Type u_3} (x y : F) :
abs (inner x y / = 1 β x β  0 β§ β (r : β), r β  0 β§ y = r β’ x

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.

theorem abs_inner_eq_norm_iff {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] (x y : E) (hx0 : x β  0) (hy0 : y β  0) :
is_R_or_C.abs (inner x y) = β β (r : π), r β  0 β§ y = r β’ x

If the inner product of two vectors is equal to the product of their norms, then the two vectors are multiples of each other. One form of the equality case for Cauchy-Schwarz.

theorem real_inner_div_norm_mul_norm_eq_one_iff {F : Type u_3} (x y : F) :
y / = 1 β x β  0 β§ β (r : β), 0 < r β§ y = r β’ x

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.

theorem real_inner_div_norm_mul_norm_eq_neg_one_iff {F : Type u_3} (x y : F) :
y / = -1 β x β  0 β§ β (r : β), r < 0 β§ y = r β’ x

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.

theorem inner_sum_smul_sum_smul_of_sum_eq_zero {F : Type u_3} {ΞΉβ : Type u_1} {sβ : finset ΞΉβ} {wβ : ΞΉβ β β} (vβ : ΞΉβ β F) (hβ : β (i : ΞΉβ) in sβ, wβ i = 0) {ΞΉβ : Type u_2} {sβ : finset ΞΉβ} {wβ : ΞΉβ β β} (vβ : ΞΉβ β F) (hβ : β (i : ΞΉβ) in sβ, wβ i = 0) :
inner (β (iβ : ΞΉβ) in sβ, wβ iβ β’ vβ iβ) (β (iβ : ΞΉβ) in sβ, wβ iβ β’ vβ iβ) = (-β (iβ : ΞΉβ) in sβ, β (iβ : ΞΉβ) in sβ, ((wβ iβ) * wβ iβ) * β₯vβ iβ - vβ iββ₯ * β₯vβ iβ - vβ iββ₯) / 2

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

@[instance]
def pi_Lp.inner_product_space {π : Type u_1} [is_R_or_C π] {ΞΉ : Type u_2} [fintype ΞΉ] (f : ΞΉ β Type u_3) [Ξ  (i : ΞΉ), (f i)] :
f)

Equations
@[instance]
def is_R_or_C.inner_product_space {π : Type u_1} [is_R_or_C π] :
π

A field π satisfying is_R_or_C is itself a π-inner product space.

Equations
@[nolint]
def euclidean_space (π : Type u_1) [is_R_or_C π] (n : Type u_2) [fintype n] :
Type (max u_2 u_1)

The standard real/complex Euclidean space, functions on a finite type. For an n-dimensional space use euclidean_space π (fin n).

Equations
def has_inner.is_R_or_C_to_real (π : Type u_1) (E : Type u_2) [is_R_or_C π] [ E] :

A general inner product implies a real inner product. This is not registered as an instance since it creates problems with the case π = β.

Equations
def inner_product_space.is_R_or_C_to_real (π : Type u_1) (E : Type u_2) [is_R_or_C π] [ E] :

A general inner product space structure implies a real inner product structure. This is not registered as an instance since it creates problems with the case π = β, but in can be used in a proof to obtain a real inner product space structure from a given π-inner product space structure.

Equations
theorem real_inner_eq_re_inner (π : Type u_1) {E : Type u_2} [is_R_or_C π] [ E] (x y : E) :

@[instance]
def inner_product_space.complex_to_real {G : Type u_4}  :

A complex inner product implies a real inner product

Equations
theorem is_bounded_bilinear_map_inner {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] [ E] [ π E] :
(Ξ» (p : E Γ E), inner p.fst p.snd)

theorem times_cont_diff_inner {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] [ E] [ π E] {n : with_top β} :
(Ξ» (p : E Γ E), inner p.fst p.snd)

theorem times_cont_diff_at_inner {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] [ E] [ π E] {p : E Γ E} {n : with_top β} :
(Ξ» (p : E Γ E), inner p.fst p.snd) p

theorem differentiable_inner {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] [ E] [ π E] :
(Ξ» (p : E Γ E), inner p.fst p.snd)

theorem continuous_inner {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] [ E] [ π E] :
continuous (Ξ» (p : E Γ E), inner p.fst p.snd)

theorem times_cont_diff_within_at.inner {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] [ E] [ π E] {G : Type u_4} [normed_group G] [ G] {f g : G β E} {s : set G} {x : G} {n : with_top β} (hf : x) (hg : x) :
(Ξ» (x : G), inner (f x) (g x)) s x

theorem times_cont_diff_at.inner {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] [ E] [ π E] {G : Type u_4} [normed_group G] [ G] {f g : G β E} {x : G} {n : with_top β} (hf : x) (hg : x) :
(Ξ» (x : G), inner (f x) (g x)) x

theorem times_cont_diff_on.inner {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] [ E] [ π E] {G : Type u_4} [normed_group G] [ G] {f g : G β E} {s : set G} {n : with_top β} (hf : s) (hg : s) :
(Ξ» (x : G), inner (f x) (g x)) s

theorem times_cont_diff.inner {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] [ E] [ π E] {G : Type u_4} [normed_group G] [ G] {f g : G β E} {n : with_top β} (hf : f) (hg : g) :
(Ξ» (x : G), inner (f x) (g x))

theorem differentiable_within_at.inner {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] [ E] [ π E] {G : Type u_4} [normed_group G] [ G] {f g : G β E} {s : set G} {x : G} (hf : x) (hg : x) :
(Ξ» (x : G), inner (f x) (g x)) s x

theorem differentiable_at.inner {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] [ E] [ π E] {G : Type u_4} [normed_group G] [ G] {f g : G β E} {x : G} (hf : x) (hg : x) :
(Ξ» (x : G), inner (f x) (g x)) x

theorem differentiable_on.inner {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] [ E] [ π E] {G : Type u_4} [normed_group G] [ G] {f g : G β E} {s : set G} (hf : s) (hg : s) :
(Ξ» (x : G), inner (f x) (g x)) s

theorem differentiable.inner {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] [ E] [ π E] {G : Type u_4} [normed_group G] [ G] {f g : G β E} (hf : f) (hg : g) :
(Ξ» (x : G), inner (f x) (g x))

@[instance]
def euclidean_space.finite_dimensional {π : Type u_1} [is_R_or_C π] {ΞΉ : Type u_4} [fintype ΞΉ] :
(euclidean_space π ΞΉ)

@[simp]
theorem findim_euclidean_space {π : Type u_1} [is_R_or_C π] {ΞΉ : Type u_4} [fintype ΞΉ] :
(euclidean_space π ΞΉ) =

theorem findim_euclidean_space_fin {π : Type u_1} [is_R_or_C π] {n : β} :
(euclidean_space π (fin n)) = n

### Orthogonal projection in inner product spaces

theorem exists_norm_eq_infi_of_complete_convex {F : Type u_3} {K : set F} (ne : K.nonempty) (hβ : is_complete K) (hβ : convex K) (u : F) :
β (v : F) (H : v β K), β₯u - vβ₯ = β¨ (w : β₯K), β₯u - βwβ₯

Existence of minimizers Let u be a point in a real 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.

theorem norm_eq_infi_iff_real_inner_le_zero {F : Type u_3} {K : set F} (h : convex K) {u v : F} (hv : v β K) :
(β₯u - vβ₯ = β¨ (w : β₯K), β₯u - βwβ₯) β β (w : F), w β K β inner (u - v) (w - v) β€ 0

Characterization of minimizers for the projection on a convex set in a real inner product space.

theorem exists_norm_eq_infi_of_complete_subspace {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] (K : subspace π E) (h : is_complete βK) (u : E) :
β (v : E) (H : v β K), β₯u - vβ₯ = β¨ (w : β₯βK), β₯u - βwβ₯

Existence of projections on complete subspaces. 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.

theorem norm_eq_infi_iff_real_inner_eq_zero {F : Type u_3} (K : F) {u v : F} (hv : v β K) :
(β₯u - vβ₯ = β¨ (w : β₯βK), β₯u - βwβ₯) β β (w : F), w β K β inner (u - v) w = 0

Characterization of minimizers in the projection on a subspace, in the real case. Let u be a point in a real inner product space, and let K be a nonempty subspace. Then point v minimizes the distance β₯u - vβ₯ over points in K if and only if for all w β K, βͺu - v, wβ« = 0 (i.e., u - v is orthogonal to the subspace K). This is superceded by norm_eq_infi_iff_inner_eq_zero that gives the same conclusion over any is_R_or_C field.

theorem norm_eq_infi_iff_inner_eq_zero {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] (K : subspace π E) {u v : E} (hv : v β K) :
(β₯u - vβ₯ = β¨ (w : β₯βK), β₯u - βwβ₯) β β (w : E), w β K β inner (u - v) w = 0

Characterization of minimizers in the projection on a subspace. 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β₯ over points in K if and only if for all w β K, βͺu - v, wβ« = 0 (i.e., u - v is orthogonal to the subspace K)

def orthogonal_projection_fn {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {K : subspace π E} (h : is_complete βK) (v : E) :
E

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
theorem orthogonal_projection_fn_mem {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {K : submodule π E} (h : is_complete βK) (v : E) :

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.

theorem orthogonal_projection_fn_inner_eq_zero {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {K : submodule π E} (h : is_complete βK) (v w : E) (H : w β K) :
inner (v - w = 0

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.

theorem eq_orthogonal_projection_fn_of_mem_of_inner_eq_zero {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {K : submodule π E} (h : is_complete βK) {u v : E} (hvm : v β K) (hvo : β (w : E), w β K β inner (u - v) w = 0) :

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.

def orthogonal_projection_of_complete {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {K : submodule π E} (h : is_complete βK) :
E ββ[π] E

The orthogonal projection onto a complete subspace. For most purposes, orthogonal_projection, which removes the is_complete hypothesis and is the identity map when the subspace is not complete, should be used instead.

Equations
def orthogonal_projection {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] (K : submodule π E) :
E ββ[π] E

The orthogonal projection onto a subspace, which is expected to be complete. If the subspace is not complete, this uses the identity map instead.

Equations
theorem orthogonal_projection_def {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] (K : submodule π E) :
= (Ξ» (h : , (Ξ» (h : , linear_map.id)

The definition of orthogonal_projection using if.

@[simp]
theorem orthogonal_projection_fn_eq {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {K : submodule π E} (h : is_complete βK) (v : E) :

theorem orthogonal_projection_mem {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {K : submodule π E} (h : is_complete βK) (v : E) :

The orthogonal projection is in the given subspace.

@[simp]
theorem orthogonal_projection_inner_eq_zero {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] (K : submodule π E) (v w : E) (H : w β K) :
inner (v - v) w = 0

The characterization of the orthogonal projection.

theorem eq_orthogonal_projection_of_mem_of_inner_eq_zero {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {K : submodule π E} (h : is_complete βK) {u v : E} (hvm : v β K) (hvo : β (w : E), w β K β inner (u - v) w = 0) :
v =

The orthogonal projection is the unique point in K with the orthogonality property.

def submodule.orthogonal {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] (K : submodule π E) :
submodule π E

The subspace of vectors orthogonal to a given subspace.

Equations
theorem submodule.mem_orthogonal {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] (K : submodule π E) (v : E) :
β β (u : E), u β K β v = 0

When a vector is in K.orthogonal.

theorem submodule.mem_orthogonal' {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] (K : submodule π E) (v : E) :
β β (u : E), u β K β u = 0

When a vector is in K.orthogonal, with the inner product the other way round.

theorem submodule.inner_right_of_mem_orthogonal {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {u v : E} {K : submodule π E} (hu : u β K) (hv : v β K.orthogonal) :
v = 0

A vector in K is orthogonal to one in K.orthogonal.

theorem submodule.inner_left_of_mem_orthogonal {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {u v : E} {K : submodule π E} (hu : u β K) (hv : v β K.orthogonal) :
u = 0

A vector in K.orthogonal is orthogonal to one in K.

theorem submodule.orthogonal_disjoint {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] (K : submodule π E) :

K and K.orthogonal have trivial intersection.

theorem submodule.orthogonal_gc (π : Type u_1) (E : Type u_2) [is_R_or_C π] [ E] :

submodule.orthogonal gives a galois_connection between submodule π E and its order_dual.

theorem submodule.orthogonal_le {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {Kβ Kβ : submodule π E} (h : Kβ β€ Kβ) :
Kβ.orthogonal β€ Kβ.orthogonal

submodule.orthogonal reverses the β€ ordering of two subspaces.

theorem submodule.le_orthogonal_orthogonal {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] (K : submodule π E) :

K is contained in K.orthogonal.orthogonal.

theorem submodule.inf_orthogonal {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] (Kβ Kβ : submodule π E) :
Kβ.orthogonal β Kβ.orthogonal = (Kβ β Kβ).orthogonal

The inf of two orthogonal subspaces equals the subspace orthogonal to the sup.

theorem submodule.infi_orthogonal {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {ΞΉ : Type u_3} (K : ΞΉ β submodule π E) :
(β¨ (i : ΞΉ), (K i).orthogonal) = (supr K).orthogonal

The inf of an indexed family of orthogonal subspaces equals the subspace orthogonal to the sup.

theorem submodule.Inf_orthogonal {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] (s : set (submodule π E)) :
(β¨ (K : submodule π E) (H : K β s), K.orthogonal) = (Sup s).orthogonal

The inf of a set of orthogonal subspaces equals the subspace orthogonal to the sup.

theorem submodule.sup_orthogonal_inf_of_is_complete {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {Kβ Kβ : submodule π E} (h : Kβ β€ Kβ) (hc : is_complete βKβ) :
Kβ β Kβ.orthogonal β Kβ = Kβ

If Kβ is complete and contained in Kβ, Kβ and Kβ.orthogonal β Kβ span Kβ.

theorem submodule.sup_orthogonal_of_is_complete {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {K : submodule π E} (h : is_complete βK) :

If K is complete, K and K.orthogonal span the whole space.

theorem submodule.is_compl_orthogonal_of_is_complete {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {K : submodule π E} (h : is_complete βK) :

If K is complete, K and K.orthogonal are complements of each other.

@[simp]
theorem submodule.top_orthogonal_eq_bot {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] :

@[simp]
theorem submodule.bot_orthogonal_eq_top {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] :

theorem submodule.eq_top_iff_orthogonal_eq_bot {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {K : submodule π E} (hK : is_complete βK) :

theorem submodule.findim_add_inf_findim_orthogonal {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {Kβ Kβ : submodule π E} [ β₯Kβ] (h : Kβ β€ Kβ) :
β₯Kβ + β₯(Kβ.orthogonal β Kβ) = β₯Kβ

Given a finite-dimensional subspace Kβ, and a subspace Kβ containined in it, the dimensions of Kβ and the intersection of its orthogonal subspace with Kβ add to that of Kβ.