mathlib documentation

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 #

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.

The orthogonal complement of a submodule K is denoted by Kᗮ.

Implementation notes #

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

TODO #

Tags #

inner product space, norm

References #

The Coq code is available at the following address: http://www.lri.fr/~sboldo/elfic/index.html

source
@[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
source
@[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!

source
@[nolint, class]
structure inner_product_space.core (𝕜 : Type u_4) (F : Type u_5) [is_R_or_C 𝕜] [add_comm_group F] [module 𝕜 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.

source
def inner_product_space.of_core.to_has_inner {𝕜 : Type u_1} {F : Type u_3} [is_R_or_C 𝕜] [add_comm_group F] [module 𝕜 F] [c : inner_product_space.core 𝕜 F] :
has_inner 𝕜 F

Inner product defined by the inner_product_space.core structure.

Equations
source
def inner_product_space.of_core.norm_sq {𝕜 : Type u_1} {F : Type u_3} [is_R_or_C 𝕜] [add_comm_group F] [module 𝕜 F] [c : inner_product_space.core 𝕜 F] (x : F) :
ℝ

The norm squared function for inner_product_space.core structure.

Equations
source
theorem inner_product_space.of_core.inner_conj_sym {𝕜 : Type u_1} {F : Type u_3} [is_R_or_C 𝕜] [add_comm_group F] [module 𝕜 F] [c : inner_product_space.core 𝕜 F] (x y : F) :
⇑is_R_or_C.conj (inner y x) = inner x y
source
theorem inner_product_space.of_core.inner_self_nonneg {𝕜 : Type u_1} {F : Type u_3} [is_R_or_C 𝕜] [add_comm_group F] [module 𝕜 F] [c : inner_product_space.core 𝕜 F] {x : F} :
0 ≤ ⇑is_R_or_C.re (inner x x)
source
theorem inner_product_space.of_core.inner_self_nonneg_im {𝕜 : Type u_1} {F : Type u_3} [is_R_or_C 𝕜] [add_comm_group F] [module 𝕜 F] [c : inner_product_space.core 𝕜 F] {x : F} :
⇑is_R_or_C.im (inner x x) = 0
source
theorem inner_product_space.of_core.inner_self_im_zero {𝕜 : Type u_1} {F : Type u_3} [is_R_or_C 𝕜] [add_comm_group F] [module 𝕜 F] [c : inner_product_space.core 𝕜 F] {x : F} :
⇑is_R_or_C.im (inner x x) = 0
source
theorem inner_product_space.of_core.inner_add_left {𝕜 : Type u_1} {F : Type u_3} [is_R_or_C 𝕜] [add_comm_group F] [module 𝕜 F] [c : inner_product_space.core 𝕜 F] {x y z : F} :
inner (x + y) z = inner x z + inner y z
source
theorem inner_product_space.of_core.inner_add_right {𝕜 : Type u_1} {F : Type u_3} [is_R_or_C 𝕜] [add_comm_group F] [module 𝕜 F] [c : inner_product_space.core 𝕜 F] {x y z : F} :
inner x (y + z) = inner x y + inner x z
source
theorem inner_product_space.of_core.inner_norm_sq_eq_inner_self {𝕜 : Type u_1} {F : Type u_3} [is_R_or_C 𝕜] [add_comm_group F] [module 𝕜 F] [c : inner_product_space.core 𝕜 F] (x : F) :
↑(inner_product_space.of_core.norm_sq x) = inner x x
source
theorem inner_product_space.of_core.inner_re_symm {𝕜 : Type u_1} {F : Type u_3} [is_R_or_C 𝕜] [add_comm_group F] [module 𝕜 F] [c : inner_product_space.core 𝕜 F] {x y : F} :
⇑is_R_or_C.re (inner x y) = ⇑is_R_or_C.re (inner y x)
source
theorem inner_product_space.of_core.inner_im_symm {𝕜 : Type u_1} {F : Type u_3} [is_R_or_C 𝕜] [add_comm_group F] [module 𝕜 F] [c : inner_product_space.core 𝕜 F] {x y : F} :
⇑is_R_or_C.im (inner x y) = -⇑is_R_or_C.im (inner y x)
source
theorem inner_product_space.of_core.inner_smul_left {𝕜 : Type u_1} {F : Type u_3} [is_R_or_C 𝕜] [add_comm_group F] [module 𝕜 F] [c : inner_product_space.core 𝕜 F] {x y : F} {r : 𝕜} :
inner (r • x) y = (⇑is_R_or_C.conj r) * inner x y
source
theorem inner_product_space.of_core.inner_smul_right {𝕜 : Type u_1} {F : Type u_3} [is_R_or_C 𝕜] [add_comm_group F] [module 𝕜 F] [c : inner_product_space.core 𝕜 F] {x y : F} {r : 𝕜} :
inner x (r • y) = r * inner x y
source
theorem inner_product_space.of_core.inner_zero_left {𝕜 : Type u_1} {F : Type u_3} [is_R_or_C 𝕜] [add_comm_group F] [module 𝕜 F] [c : inner_product_space.core 𝕜 F] {x : F} :
inner 0 x = 0
source
theorem inner_product_space.of_core.inner_zero_right {𝕜 : Type u_1} {F : Type u_3} [is_R_or_C 𝕜] [add_comm_group F] [module 𝕜 F] [c : inner_product_space.core 𝕜 F] {x : F} :
inner x 0 = 0
source
theorem inner_product_space.of_core.inner_self_eq_zero {𝕜 : Type u_1} {F : Type u_3} [is_R_or_C 𝕜] [add_comm_group F] [module 𝕜 F] [c : inner_product_space.core 𝕜 F] {x : F} :
inner x x = 0 ↔ x = 0
source
theorem inner_product_space.of_core.inner_self_re_to_K {𝕜 : Type u_1} {F : Type u_3} [is_R_or_C 𝕜] [add_comm_group F] [module 𝕜 F] [c : inner_product_space.core 𝕜 F] {x : F} :
↑(⇑is_R_or_C.re (inner x x)) = inner x x
source
theorem inner_product_space.of_core.inner_abs_conj_sym {𝕜 : Type u_1} {F : Type u_3} [is_R_or_C 𝕜] [add_comm_group F] [module 𝕜 F] [c : inner_product_space.core 𝕜 F] {x y : F} :
is_R_or_C.abs (inner x y) = is_R_or_C.abs (inner y x)
source
theorem inner_product_space.of_core.inner_neg_left {𝕜 : Type u_1} {F : Type u_3} [is_R_or_C 𝕜] [add_comm_group F] [module 𝕜 F] [c : inner_product_space.core 𝕜 F] {x y : F} :
inner (-x) y = -inner x y
source
theorem inner_product_space.of_core.inner_neg_right {𝕜 : Type u_1} {F : Type u_3} [is_R_or_C 𝕜] [add_comm_group F] [module 𝕜 F] [c : inner_product_space.core 𝕜 F] {x y : F} :
inner x (-y) = -inner x y
source
theorem inner_product_space.of_core.inner_sub_left {𝕜 : Type u_1} {F : Type u_3} [is_R_or_C 𝕜] [add_comm_group F] [module 𝕜 F] [c : inner_product_space.core 𝕜 F] {x y z : F} :
inner (x - y) z = inner x z - inner y z
source
theorem inner_product_space.of_core.inner_sub_right {𝕜 : Type u_1} {F : Type u_3} [is_R_or_C 𝕜] [add_comm_group F] [module 𝕜 F] [c : inner_product_space.core 𝕜 F] {x y z : F} :
inner x (y - z) = inner x y - inner x z
source
theorem inner_product_space.of_core.inner_mul_conj_re_abs {𝕜 : Type u_1} {F : Type u_3} [is_R_or_C 𝕜] [add_comm_group F] [module 𝕜 F] [c : inner_product_space.core 𝕜 F] {x y : F} :
⇑is_R_or_C.re ((inner x y) * inner y x) = is_R_or_C.abs ((inner x y) * inner y x)
source
theorem inner_product_space.of_core.inner_add_add_self {𝕜 : Type u_1} {F : Type u_3} [is_R_or_C 𝕜] [add_comm_group F] [module 𝕜 F] [c : inner_product_space.core 𝕜 F] {x y : F} :
inner (x + y) (x + y) = inner x x + inner x y + inner y x + inner y y

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

source
theorem inner_product_space.of_core.inner_sub_sub_self {𝕜 : Type u_1} {F : Type u_3} [is_R_or_C 𝕜] [add_comm_group F] [module 𝕜 F] [c : inner_product_space.core 𝕜 F] {x y : F} :
inner (x - y) (x - y) = inner x x - inner x y - inner y x + inner y y
source
theorem inner_product_space.of_core.inner_mul_inner_self_le {𝕜 : Type u_1} {F : Type u_3} [is_R_or_C 𝕜] [add_comm_group F] [module 𝕜 F] [c : inner_product_space.core 𝕜 F] (x y : F) :
(is_R_or_C.abs (inner x y)) * is_R_or_C.abs (inner y x) ≤ (⇑is_R_or_C.re (inner x x)) * ⇑is_R_or_C.re (inner y y)

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.

source
def inner_product_space.of_core.to_has_norm {𝕜 : Type u_1} {F : Type u_3} [is_R_or_C 𝕜] [add_comm_group F] [module 𝕜 F] [c : inner_product_space.core 𝕜 F] :
has_norm F

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

Equations
source
theorem inner_product_space.of_core.norm_eq_sqrt_inner {𝕜 : Type u_1} {F : Type u_3} [is_R_or_C 𝕜] [add_comm_group F] [module 𝕜 F] [c : inner_product_space.core 𝕜 F] (x : F) :
∥x∥ = real.sqrt (⇑is_R_or_C.re (inner x x))
source
theorem inner_product_space.of_core.inner_self_eq_norm_sq {𝕜 : Type u_1} {F : Type u_3} [is_R_or_C 𝕜] [add_comm_group F] [module 𝕜 F] [c : inner_product_space.core 𝕜 F] (x : F) :
⇑is_R_or_C.re (inner x x) = ∥x∥ * ∥x∥
source
theorem inner_product_space.of_core.sqrt_norm_sq_eq_norm {𝕜 : Type u_1} {F : Type u_3} [is_R_or_C 𝕜] [add_comm_group F] [module 𝕜 F] [c : inner_product_space.core 𝕜 F] {x : F} :
real.sqrt (inner_product_space.of_core.norm_sq x) = ∥x∥
source
theorem inner_product_space.of_core.abs_inner_le_norm {𝕜 : Type u_1} {F : Type u_3} [is_R_or_C 𝕜] [add_comm_group F] [module 𝕜 F] [c : inner_product_space.core 𝕜 F] (x y : F) :
is_R_or_C.abs (inner x y) ≤ ∥x∥ * ∥y∥

Cauchy–Schwarz inequality with norm

source
def inner_product_space.of_core.to_normed_group {𝕜 : Type u_1} {F : Type u_3} [is_R_or_C 𝕜] [add_comm_group F] [module 𝕜 F] [c : inner_product_space.core 𝕜 F] :
normed_group F

Normed group structure constructed from an inner_product_space.core structure

Equations
source
def inner_product_space.of_core.to_normed_space {𝕜 : Type u_1} {F : Type u_3} [is_R_or_C 𝕜] [add_comm_group F] [module 𝕜 F] [c : inner_product_space.core 𝕜 F] :
normed_space 𝕜 F

Normed space structure constructed from a inner_product_space.core structure

Equations
source
def inner_product_space.of_core {𝕜 : Type u_1} {F : Type u_3} [is_R_or_C 𝕜] [add_comm_group F] [module 𝕜 F] (c : inner_product_space.core 𝕜 F) :
inner_product_space 𝕜 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 #

source
@[simp]
theorem inner_conj_sym {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (x y : E) :
⇑is_R_or_C.conj (inner y x) = inner x y
source
theorem real_inner_comm {F : Type u_3} [inner_product_space ℝ F] (x y : F) :
inner y x = inner x y
source
theorem inner_eq_zero_sym {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {x y : E} :
inner x y = 0 ↔ inner y x = 0
source
@[simp]
theorem inner_self_nonneg_im {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {x : E} :
⇑is_R_or_C.im (inner x x) = 0
source
theorem inner_self_im_zero {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {x : E} :
⇑is_R_or_C.im (inner x x) = 0
source
theorem inner_add_left {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {x y z : E} :
inner (x + y) z = inner x z + inner y z
source
theorem inner_add_right {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {x y z : E} :
inner x (y + z) = inner x y + inner x z
source
theorem inner_re_symm {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {x y : E} :
⇑is_R_or_C.re (inner x y) = ⇑is_R_or_C.re (inner y x)
source
theorem inner_im_symm {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {x y : E} :
⇑is_R_or_C.im (inner x y) = -⇑is_R_or_C.im (inner y x)
source
theorem inner_smul_left {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {x y : E} {r : 𝕜} :
inner (r • x) y = (⇑is_R_or_C.conj r) * inner x y
source
theorem real_inner_smul_left {F : Type u_3} [inner_product_space ℝ F] {x y : F} {r : ℝ} :
inner (r • x) y = r * inner x y
source
theorem inner_smul_real_left {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {x y : E} {r : ℝ} :
inner (↑r • x) y = r • inner x y
source
theorem inner_smul_right {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {x y : E} {r : 𝕜} :
inner x (r • y) = r * inner x y
source
theorem real_inner_smul_right {F : Type u_3} [inner_product_space ℝ F] {x y : F} {r : ℝ} :
inner x (r • y) = r * inner x y
source
theorem inner_smul_real_right {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {x y : E} {r : ℝ} :
inner x (↑r • y) = r • inner x y
source
def sesq_form_of_inner {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] :
sesq_form 𝕜 E (is_R_or_C.conj_to_ring_equiv 𝕜)

The inner product as a sesquilinear form.

Equations
source
@[simp]
theorem sesq_form_of_inner_sesq {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (x y : E) :
⇑sesq_form_of_inner x y = inner y x
source
def bilin_form_of_real_inner {F : Type u_3} [inner_product_space ℝ F] :
bilin_form ℝ F

The real inner product as a bilinear form.

Equations
source
@[simp]
theorem bilin_form_of_real_inner_apply {F : Type u_3} [inner_product_space ℝ F] (ᾰ ᾰ_1 : F) :
⇑bilin_form_of_real_inner ᾰ ᾰ_1 = inner ᾰ ᾰ_1
source
theorem sum_inner {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 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.

source
theorem inner_sum {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {ι : Type u_3} (s : finset ι) (f : ι → E) (x : E) :
inner x (∑ (i : ι) in s, f i) = ∑ (i : ι) in s, inner x (f i)

An inner product with a sum on the right.

source
theorem finsupp.sum_inner {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {ι : Type u_3} (l : ι →₀ 𝕜) (v : ι → E) (x : E) :
inner (l.sum (λ (i : ι) (a : 𝕜), a • v i)) x = l.sum (λ (i : ι) (a : 𝕜), ⇑is_R_or_C.conj a • inner (v i) x)

An inner product with a sum on the left, finsupp version.

source
theorem finsupp.inner_sum {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {ι : Type u_3} (l : ι →₀ 𝕜) (v : ι → E) (x : E) :
inner x (l.sum (λ (i : ι) (a : 𝕜), a • v i)) = l.sum (λ (i : ι) (a : 𝕜), a • inner x (v i))

An inner product with a sum on the right, finsupp version.

source
@[simp]
theorem inner_zero_left {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {x : E} :
inner 0 x = 0
source
theorem inner_re_zero_left {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {x : E} :
⇑is_R_or_C.re (inner 0 x) = 0
source
@[simp]
theorem inner_zero_right {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {x : E} :
inner x 0 = 0
source
theorem inner_re_zero_right {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {x : E} :
⇑is_R_or_C.re (inner x 0) = 0
source
theorem inner_self_nonneg {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {x : E} :
0 ≤ ⇑is_R_or_C.re (inner x x)
source
theorem real_inner_self_nonneg {F : Type u_3} [inner_product_space ℝ F] {x : F} :
0 ≤ inner x x
source
@[simp]
theorem inner_self_eq_zero {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {x : E} :
inner x x = 0 ↔ x = 0
source
@[simp]
theorem inner_self_nonpos {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {x : E} :
⇑is_R_or_C.re (inner x x) ≤ 0 ↔ x = 0
source
theorem real_inner_self_nonpos {F : Type u_3} [inner_product_space ℝ F] {x : F} :
inner x x ≤ 0 ↔ x = 0
source
@[simp]
theorem inner_self_re_to_K {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {x : E} :
↑(⇑is_R_or_C.re (inner x x)) = inner x x
source
theorem inner_self_eq_norm_sq_to_K {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (x : E) :
inner x x = ↑∥x∥ ^ 2
source
theorem inner_self_re_abs {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {x : E} :
⇑is_R_or_C.re (inner x x) = is_R_or_C.abs (inner x x)
source
theorem inner_self_abs_to_K {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {x : E} :
↑(is_R_or_C.abs (inner x x)) = inner x x
source
theorem real_inner_self_abs {F : Type u_3} [inner_product_space ℝ F] {x : F} :
abs (inner x x) = inner x x
source
theorem inner_abs_conj_sym {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {x y : E} :
is_R_or_C.abs (inner x y) = is_R_or_C.abs (inner y x)
source
@[simp]
theorem inner_neg_left {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {x y : E} :
inner (-x) y = -inner x y
source
@[simp]
theorem inner_neg_right {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {x y : E} :
inner x (-y) = -inner x y
source
theorem inner_neg_neg {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {x y : E} :
inner (-x) (-y) = inner x y
source
@[simp]
theorem inner_self_conj {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {x : E} :
⇑is_R_or_C.conj (inner x x) = inner x x
source
theorem inner_sub_left {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {x y z : E} :
inner (x - y) z = inner x z - inner y z
source
theorem inner_sub_right {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {x y z : E} :
inner x (y - z) = inner x y - inner x z
source
theorem inner_mul_conj_re_abs {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {x y : E} :
⇑is_R_or_C.re ((inner x y) * inner y x) = is_R_or_C.abs ((inner x y) * inner y x)
source
theorem inner_add_add_self {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {x y : E} :
inner (x + y) (x + y) = inner x x + inner x y + inner y x + inner y y

Expand ⟪x + y, x + y⟫

source
theorem real_inner_add_add_self {F : Type u_3} [inner_product_space ℝ F] {x y : F} :
inner (x + y) (x + y) = inner x x + 2 * inner x y + inner y y

Expand ⟪x + y, x + y⟫_ℝ

source
theorem inner_sub_sub_self {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {x y : E} :
inner (x - y) (x - y) = inner x x - inner x y - inner y x + inner y y
source
theorem real_inner_sub_sub_self {F : Type u_3} [inner_product_space ℝ F] {x y : F} :
inner (x - y) (x - y) = inner x x - 2 * inner x y + inner y y

Expand ⟪x - y, x - y⟫_ℝ

source
theorem parallelogram_law {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {x y : E} :
inner (x + y) (x + y) + inner (x - y) (x - y) = 2 * (inner x x + inner y y)

Parallelogram law

source
theorem inner_mul_inner_self_le {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (x y : E) :
(is_R_or_C.abs (inner x y)) * is_R_or_C.abs (inner y x) ≤ (⇑is_R_or_C.re (inner x x)) * ⇑is_R_or_C.re (inner y y)

Cauchy–Schwarz inequality. This proof follows "Proof 2" on Wikipedia.

source
theorem real_inner_mul_inner_self_le {F : Type u_3} [inner_product_space ℝ F] (x y : F) :
(inner x y) * inner x y ≤ (inner x x) * inner y y

Cauchy–Schwarz inequality for real inner products.

source
theorem linear_independent_of_ne_zero_of_inner_eq_zero {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {ι : Type u_3} {v : ι → E} (hz : ∀ (i : ι), v i ≠ 0) (ho : ∀ (i j : ι), i ≠ j → inner (v i) (v j) = 0) :
linear_independent 𝕜 v

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

source
def orthonormal (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {ι : Type u_4} (v : ι → E) :
Prop

An orthonormal set of vectors in an inner_product_space

Equations
source
theorem orthonormal_iff_ite {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {ι : Type u_4} {v : ι → E} :
orthonormal 𝕜 v ↔ ∀ (i j : ι), inner (v i) (v j) = ite (i = j) 1 0

if ... then ... else characterization of an indexed set of vectors being orthonormal. (Inner product equals Kronecker delta.)

source
theorem orthonormal_subtype_iff_ite {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {s : set E} :
orthonormal 𝕜 coe ↔ ∀ (v : E), v ∈ s → ∀ (w : E), w ∈ s → inner v w = ite (v = w) 1 0

if ... then ... else characterization of a set of vectors being orthonormal. (Inner product equals Kronecker delta.)

source
theorem orthonormal.inner_right_finsupp {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {ι : Type u_4} {v : ι → E} (hv : orthonormal 𝕜 v) (l : ι →₀ 𝕜) (i : ι) :
inner (v i) (⇑(finsupp.total ι E 𝕜 v) l) = ⇑l i

The inner product of a linear combination of a set of orthonormal vectors with one of those vectors picks out the coefficient of that vector.

source
theorem orthonormal.inner_right_fintype {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {ι : Type u_4} [fintype ι] {v : ι → E} (hv : orthonormal 𝕜 v) (l : ι → 𝕜) (i : ι) :
inner (v i) (∑ (i : ι), l i • v i) = l i

The inner product of a linear combination of a set of orthonormal vectors with one of those vectors picks out the coefficient of that vector.

source
theorem orthonormal.inner_left_finsupp {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {ι : Type u_4} {v : ι → E} (hv : orthonormal 𝕜 v) (l : ι →₀ 𝕜) (i : ι) :
inner (⇑(finsupp.total ι E 𝕜 v) l) (v i) = ⇑is_R_or_C.conj (⇑l i)

The inner product of a linear combination of a set of orthonormal vectors with one of those vectors picks out the coefficient of that vector.

source
theorem orthonormal.inner_left_fintype {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {ι : Type u_4} [fintype ι] {v : ι → E} (hv : orthonormal 𝕜 v) (l : ι → 𝕜) (i : ι) :
inner (∑ (i : ι), l i • v i) (v i) = ⇑is_R_or_C.conj (l i)

The inner product of a linear combination of a set of orthonormal vectors with one of those vectors picks out the coefficient of that vector.

source
theorem orthonormal.linear_independent {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {ι : Type u_4} {v : ι → E} (hv : orthonormal 𝕜 v) :
linear_independent 𝕜 v

An orthonormal set is linearly independent.

source
theorem orthonormal.comp {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {ι : Type u_4} {ι' : Type u_3} {v : ι → E} (hv : orthonormal 𝕜 v) (f : ι' → ι) (hf : function.injective f) :
orthonormal 𝕜 (v ∘ f)

A subfamily of an orthonormal family (i.e., a composition with an injective map) is an orthonormal family.

source
theorem orthonormal.inner_finsupp_eq_zero {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {ι : Type u_4} {v : ι → E} (hv : orthonormal 𝕜 v) {s : set ι} {i : ι} (hi : i ∉ s) {l : ι →₀ 𝕜} (hl : l ∈ finsupp.supported 𝕜 𝕜 s) :
inner (⇑(finsupp.total ι E 𝕜 v) l) (v i) = 0

A linear combination of some subset of an orthonormal set is orthogonal to other members of the set.

source
theorem orthonormal_empty (𝕜 : Type u_1) (E : Type u_2) [is_R_or_C 𝕜] [inner_product_space 𝕜 E] :
orthonormal 𝕜 (λ (x : ↥∅), ↑x)
source
theorem orthonormal_Union_of_directed {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {η : Type u_3} {s : η → set E} (hs : directed has_subset.subset s) (h : ∀ (i : η), orthonormal 𝕜 (λ (x : ↥(s i)), ↑x)) :
orthonormal 𝕜 (λ (x : ↥⋃ (i : η), s i), ↑x)
source
theorem orthonormal_sUnion_of_directed {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {s : set (set E)} (hs : directed_on has_subset.subset s) (h : ∀ (a : set E), a ∈ s → orthonormal 𝕜 (λ (x : ↥a), ↑x)) :
orthonormal 𝕜 (λ (x : ↥⋃₀s), ↑x)
source
theorem exists_maximal_orthonormal {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {s : set E} (hs : orthonormal 𝕜 coe) :
∃ (w : set E) (H : w ⊇ s), orthonormal 𝕜 coe ∧ ∀ (u : set E), u ⊇ w → orthonormal 𝕜 coe → u = w

Given an orthonormal set v of vectors in E, there exists a maximal orthonormal set containing it.

source
theorem orthonormal.ne_zero {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {ι : Type u_4} {v : ι → E} (hv : orthonormal 𝕜 v) (i : ι) :
v i ≠ 0
source
def basis_of_orthonormal_of_card_eq_finrank {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {ι : Type u_4} [fintype ι] [nonempty ι] {v : ι → E} (hv : orthonormal 𝕜 v) (card_eq : fintype.card ι = finite_dimensional.finrank 𝕜 E) :
basis ι 𝕜 E

A family of orthonormal vectors with the correct cardinality forms a basis.

Equations
source
@[simp]
theorem coe_basis_of_orthonormal_of_card_eq_finrank {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {ι : Type u_4} [fintype ι] [nonempty ι] {v : ι → E} (hv : orthonormal 𝕜 v) (card_eq : fintype.card ι = finite_dimensional.finrank 𝕜 E) :
⇑(basis_of_orthonormal_of_card_eq_finrank hv card_eq) = v
source
theorem norm_eq_sqrt_inner {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (x : E) :
∥x∥ = real.sqrt (⇑is_R_or_C.re (inner x x))
source
theorem norm_eq_sqrt_real_inner {F : Type u_3} [inner_product_space ℝ F] (x : F) :
∥x∥ = real.sqrt (inner x x)
source
theorem inner_self_eq_norm_sq {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (x : E) :
⇑is_R_or_C.re (inner x x) = ∥x∥ * ∥x∥
source
theorem real_inner_self_eq_norm_sq {F : Type u_3} [inner_product_space ℝ F] (x : F) :
inner x x = ∥x∥ * ∥x∥
source
theorem norm_add_sq {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {x y : E} :
∥x + y∥ ^ 2 = ∥x∥ ^ 2 + 2 * ⇑is_R_or_C.re (inner x y) + ∥y∥ ^ 2

Expand the square

source
theorem norm_add_pow_two {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {x y : E} :
∥x + y∥ ^ 2 = ∥x∥ ^ 2 + 2 * ⇑is_R_or_C.re (inner x y) + ∥y∥ ^ 2

Alias of norm_add_sq.

source
theorem norm_add_sq_real {F : Type u_3} [inner_product_space ℝ F] {x y : F} :
∥x + y∥ ^ 2 = ∥x∥ ^ 2 + 2 * inner x y + ∥y∥ ^ 2

Expand the square

source
theorem norm_add_pow_two_real {F : Type u_3} [inner_product_space ℝ F] {x y : F} :
∥x + y∥ ^ 2 = ∥x∥ ^ 2 + 2 * inner x y + ∥y∥ ^ 2

Alias of norm_add_sq_real.

source
theorem norm_add_mul_self {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {x y : E} :
∥x + y∥ * ∥x + y∥ = ∥x∥ * ∥x∥ + 2 * ⇑is_R_or_C.re (inner x y) + ∥y∥ * ∥y∥

Expand the square

source
theorem norm_add_mul_self_real {F : Type u_3} [inner_product_space ℝ F] {x y : F} :
∥x + y∥ * ∥x + y∥ = ∥x∥ * ∥x∥ + 2 * inner x y + ∥y∥ * ∥y∥

Expand the square

source
theorem norm_sub_sq {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {x y : E} :
∥x - y∥ ^ 2 = ∥x∥ ^ 2 - 2 * ⇑is_R_or_C.re (inner x y) + ∥y∥ ^ 2

Expand the square

source
theorem norm_sub_pow_two {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {x y : E} :
∥x - y∥ ^ 2 = ∥x∥ ^ 2 - 2 * ⇑is_R_or_C.re (inner x y) + ∥y∥ ^ 2

Alias of norm_sub_sq.

source
theorem norm_sub_sq_real {F : Type u_3} [inner_product_space ℝ F] {x y : F} :
∥x - y∥ ^ 2 = ∥x∥ ^ 2 - 2 * inner x y + ∥y∥ ^ 2

Expand the square

source
theorem norm_sub_pow_two_real {F : Type u_3} [inner_product_space ℝ F] {x y : F} :
∥x - y∥ ^ 2 = ∥x∥ ^ 2 - 2 * inner x y + ∥y∥ ^ 2

Alias of norm_sub_sq_real.

source
theorem norm_sub_mul_self {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {x y : E} :
∥x - y∥ * ∥x - y∥ = ∥x∥ * ∥x∥ - 2 * ⇑is_R_or_C.re (inner x y) + ∥y∥ * ∥y∥

Expand the square

source
theorem norm_sub_mul_self_real {F : Type u_3} [inner_product_space ℝ F] {x y : F} :
∥x - y∥ * ∥x - y∥ = ∥x∥ * ∥x∥ - 2 * inner x y + ∥y∥ * ∥y∥

Expand the square

source
theorem abs_inner_le_norm {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (x y : E) :
is_R_or_C.abs (inner x y) ≤ ∥x∥ * ∥y∥

Cauchy–Schwarz inequality with norm

source
theorem abs_real_inner_le_norm {F : Type u_3} [inner_product_space ℝ F] (x y : F) :
abs (inner x y) ≤ ∥x∥ * ∥y∥

Cauchy–Schwarz inequality with norm

source
theorem real_inner_le_norm {F : Type u_3} [inner_product_space ℝ F] (x y : F) :
inner x y ≤ ∥x∥ * ∥y∥

Cauchy–Schwarz inequality with norm

source
theorem parallelogram_law_with_norm {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {x y : E} :
∥x + y∥ * ∥x + y∥ + ∥x - y∥ * ∥x - y∥ = 2 * (∥x∥ * ∥x∥ + ∥y∥ * ∥y∥)
source
theorem parallelogram_law_with_norm_real {F : Type u_3} [inner_product_space ℝ F] {x y : F} :
∥x + y∥ * ∥x + y∥ + ∥x - y∥ * ∥x - y∥ = 2 * (∥x∥ * ∥x∥ + ∥y∥ * ∥y∥)
source
theorem re_inner_eq_norm_add_mul_self_sub_norm_mul_self_sub_norm_mul_self_div_two {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (x y : E) :
⇑is_R_or_C.re (inner x y) = (∥x + y∥ * ∥x + y∥ - ∥x∥ * ∥x∥ - ∥y∥ * ∥y∥) / 2

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

source
theorem re_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (x y : E) :
⇑is_R_or_C.re (inner x y) = (∥x∥ * ∥x∥ + ∥y∥ * ∥y∥ - ∥x - y∥ * ∥x - y∥) / 2

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

source
theorem re_inner_eq_norm_add_mul_self_sub_norm_sub_mul_self_div_four {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (x y : E) :
⇑is_R_or_C.re (inner x y) = (∥x + y∥ * ∥x + y∥ - ∥x - y∥ * ∥x - y∥) / 4

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

source
theorem im_inner_eq_norm_sub_I_smul_mul_self_sub_norm_add_I_smul_mul_self_div_four {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (x y : E) :
⇑is_R_or_C.im (inner x y) = (∥x - is_R_or_C.I • y∥ * ∥x - is_R_or_C.I • y∥ - ∥x + is_R_or_C.I • y∥ * ∥x + is_R_or_C.I • y∥) / 4

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

source
theorem inner_eq_sum_norm_sq_div_four {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (x y : E) :
inner x y = (↑∥x + y∥ ^ 2 - ↑∥x - y∥ ^ 2 + (↑∥x - is_R_or_C.I • y∥ ^ 2 - ↑∥x + is_R_or_C.I • y∥ ^ 2) * is_R_or_C.I) / 4

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

source
@[simp]
theorem linear_isometry.inner_map_map {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {E' : Type u_4} [inner_product_space 𝕜 E'] (f : E →ₗᵢ[𝕜] E') (x y : E) :
inner (⇑f x) (⇑f y) = inner x y

A linear isometry preserves the inner product.

source
@[simp]
theorem linear_isometry_equiv.inner_map_map {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {E' : Type u_4} [inner_product_space 𝕜 E'] (f : E ≃ₗᵢ[𝕜] E') (x y : E) :
inner (⇑f x) (⇑f y) = inner x y

A linear isometric equivalence preserves the inner product.

source
def linear_map.isometry_of_inner {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {E' : Type u_4} [inner_product_space 𝕜 E'] (f : E →ₗ[𝕜] E') (h : ∀ (x y : E), inner (⇑f x) (⇑f y) = inner x y) :
E →ₗᵢ[𝕜] E'

A linear map that preserves the inner product is a linear isometry.

Equations
source
@[simp]
theorem linear_map.coe_isometry_of_inner {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {E' : Type u_4} [inner_product_space 𝕜 E'] (f : E →ₗ[𝕜] E') (h : ∀ (x y : E), inner (⇑f x) (⇑f y) = inner x y) :
⇑(f.isometry_of_inner h) = ⇑f
source
@[simp]
theorem linear_map.isometry_of_inner_to_linear_map {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {E' : Type u_4} [inner_product_space 𝕜 E'] (f : E →ₗ[𝕜] E') (h : ∀ (x y : E), inner (⇑f x) (⇑f y) = inner x y) :
(f.isometry_of_inner h).to_linear_map = f
source
def linear_equiv.isometry_of_inner {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {E' : Type u_4} [inner_product_space 𝕜 E'] (f : E ≃ₗ[𝕜] E') (h : ∀ (x y : E), inner (⇑f x) (⇑f y) = inner x y) :
E ≃ₗᵢ[𝕜] E'

A linear equivalence that preserves the inner product is a linear isometric equivalence.

Equations
source
@[simp]
theorem linear_equiv.coe_isometry_of_inner {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {E' : Type u_4} [inner_product_space 𝕜 E'] (f : E ≃ₗ[𝕜] E') (h : ∀ (x y : E), inner (⇑f x) (⇑f y) = inner x y) :
⇑(f.isometry_of_inner h) = ⇑f
source
@[simp]
theorem linear_equiv.isometry_of_inner_to_linear_equiv {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {E' : Type u_4} [inner_product_space 𝕜 E'] (f : E ≃ₗ[𝕜] E') (h : ∀ (x y : E), inner (⇑f x) (⇑f y) = inner x y) :
(f.isometry_of_inner h).to_linear_equiv = f
source
theorem real_inner_eq_norm_add_mul_self_sub_norm_mul_self_sub_norm_mul_self_div_two {F : Type u_3} [inner_product_space ℝ F] (x y : F) :
inner x y = (∥x + y∥ * ∥x + y∥ - ∥x∥ * ∥x∥ - ∥y∥ * ∥y∥) / 2

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

source
theorem real_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two {F : Type u_3} [inner_product_space ℝ F] (x y : F) :
inner x y = (∥x∥ * ∥x∥ + ∥y∥ * ∥y∥ - ∥x - y∥ * ∥x - y∥) / 2

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

source
theorem norm_add_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero {F : Type u_3} [inner_product_space ℝ F] (x y : F) :
∥x + y∥ * ∥x + y∥ = ∥x∥ * ∥x∥ + ∥y∥ * ∥y∥ ↔ inner x y = 0

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

source
theorem norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (x y : E) (h : inner x y = 0) :
∥x + y∥ * ∥x + y∥ = ∥x∥ * ∥x∥ + ∥y∥ * ∥y∥

Pythagorean theorem, vector inner product form.

source
theorem norm_add_sq_eq_norm_sq_add_norm_sq_real {F : Type u_3} [inner_product_space ℝ F] {x y : F} (h : inner x y = 0) :
∥x + y∥ * ∥x + y∥ = ∥x∥ * ∥x∥ + ∥y∥ * ∥y∥

Pythagorean theorem, vector inner product form.

source
theorem norm_sub_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero {F : Type u_3} [inner_product_space ℝ F] (x y : F) :
∥x - y∥ * ∥x - y∥ = ∥x∥ * ∥x∥ + ∥y∥ * ∥y∥ ↔ inner x y = 0

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

source
theorem norm_sub_sq_eq_norm_sq_add_norm_sq_real {F : Type u_3} [inner_product_space ℝ F] {x y : F} (h : inner x y = 0) :
∥x - y∥ * ∥x - y∥ = ∥x∥ * ∥x∥ + ∥y∥ * ∥y∥

Pythagorean theorem, subtracting vectors, vector inner product form.

source
theorem real_inner_add_sub_eq_zero_iff {F : Type u_3} [inner_product_space ℝ F] (x y : F) :
inner (x + y) (x - y) = 0 ↔ ∥x∥ = ∥y∥

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

source
theorem abs_real_inner_div_norm_mul_norm_le_one {F : Type u_3} [inner_product_space ℝ F] (x y : F) :
abs (inner x y / ∥x∥ * ∥y∥) ≤ 1

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

source
theorem real_inner_smul_self_left {F : Type u_3} [inner_product_space ℝ F] (x : F) (r : ℝ) :
inner (r • x) x = r * ∥x∥ * ∥x∥

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

source
theorem real_inner_smul_self_right {F : Type u_3} [inner_product_space ℝ F] (x : F) (r : ℝ) :
inner x (r • x) = r * ∥x∥ * ∥x∥

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

source
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 𝕜] [inner_product_space 𝕜 E] {x : E} {r : 𝕜} (hx : x ≠ 0) (hr : r ≠ 0) :
is_R_or_C.abs (inner x (r • x)) / ∥x∥ * ∥r • x∥ = 1

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

source
theorem abs_real_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul {F : Type u_3} [inner_product_space ℝ F] {x : F} {r : ℝ} (hx : x ≠ 0) (hr : r ≠ 0) :
abs (inner x (r • x)) / ∥x∥ * ∥r • x∥ = 1

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

source
theorem real_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_pos_mul {F : Type u_3} [inner_product_space ℝ F] {x : F} {r : ℝ} (hx : x ≠ 0) (hr : 0 < r) :
inner x (r • x) / ∥x∥ * ∥r • x∥ = 1

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

source
theorem real_inner_div_norm_mul_norm_eq_neg_one_of_ne_zero_of_neg_mul {F : Type u_3} [inner_product_space ℝ F] {x : F} {r : ℝ} (hx : x ≠ 0) (hr : r < 0) :
inner x (r • x) / ∥x∥ * ∥r • x∥ = -1

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

source
theorem abs_inner_div_norm_mul_norm_eq_one_iff {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (x y : E) :
is_R_or_C.abs (inner x y / (↑∥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.

source
theorem abs_real_inner_div_norm_mul_norm_eq_one_iff {F : Type u_3} [inner_product_space ℝ F] (x y : F) :
abs (inner x y / ∥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.

source
theorem abs_inner_eq_norm_iff {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (x y : E) (hx0 : x ≠ 0) (hy0 : y ≠ 0) :
is_R_or_C.abs (inner x y) = ∥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. Compare inner_eq_norm_mul_iff, which takes the stronger hypothesis ⟪x, y⟫ = ∥x∥ * ∥y∥.

source
theorem real_inner_div_norm_mul_norm_eq_one_iff {F : Type u_3} [inner_product_space ℝ F] (x y : F) :
inner x y / ∥x∥ * ∥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.

source
theorem real_inner_div_norm_mul_norm_eq_neg_one_iff {F : Type u_3} [inner_product_space ℝ F] (x y : F) :
inner x y / ∥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 value -1 if and only if they are nonzero and one is a negative multiple of the other.

source
theorem inner_eq_norm_mul_iff {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {x y : E} :
inner x y = (↑∥x∥) * ↑∥y∥ ↔ ↑∥y∥ • x = ↑∥x∥ • y

If the inner product of two vectors is equal to the product of their norms (i.e., ⟪x, y⟫ = ∥x∥ * ∥y∥), then the two vectors are nonnegative real multiples of each other. One form of the equality case for Cauchy-Schwarz. Compare abs_inner_eq_norm_iff, which takes the weaker hypothesis abs ⟪x, y⟫ = ∥x∥ * ∥y∥.

source
theorem inner_eq_norm_mul_iff_real {F : Type u_3} [inner_product_space ℝ F] {x y : F} :
inner x y = ∥x∥ * ∥y∥ ↔ ∥y∥ • x = ∥x∥ • y

If the inner product of two vectors is equal to the product of their norms (i.e., ⟪x, y⟫ = ∥x∥ * ∥y∥), then the two vectors are nonnegative real multiples of each other. One form of the equality case for Cauchy-Schwarz. Compare abs_inner_eq_norm_iff, which takes the weaker hypothesis abs ⟪x, y⟫ = ∥x∥ * ∥y∥.

source
theorem inner_eq_norm_mul_iff_of_norm_one {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {x y : E} (hx : ∥x∥ = 1) (hy : ∥y∥ = 1) :
inner x y = 1 ↔ x = y

If the inner product of two unit vectors is 1, then the two vectors are equal. One form of the equality case for Cauchy-Schwarz.

source
theorem inner_lt_norm_mul_iff_real {F : Type u_3} [inner_product_space ℝ F] {x y : F} :
inner x y < ∥x∥ * ∥y∥ ↔ ∥y∥ • x ≠ ∥x∥ • y
source
theorem inner_lt_one_iff_real_of_norm_one {F : Type u_3} [inner_product_space ℝ F] {x y : F} (hx : ∥x∥ = 1) (hy : ∥y∥ = 1) :
inner x y < 1 ↔ x ≠ y

If the inner product of two unit vectors is strictly less than 1, then the two vectors are distinct. One form of the equality case for Cauchy-Schwarz.

source
theorem inner_sum_smul_sum_smul_of_sum_eq_zero {F : Type u_3} [inner_product_space ℝ F] {ι₁ : 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.

source
def inner_right {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (v : E) :
E →L[𝕜] 𝕜

The inner product with a fixed left element, as a continuous linear map. This can be upgraded to a continuous map which is jointly conjugate-linear in the left argument and linear in the right argument, once (TODO) conjugate-linear maps have been defined.

Equations
source
@[simp]
theorem inner_right_coe {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (v : E) :
⇑(inner_right v) = λ (w : E), inner v w
source
@[simp]
theorem inner_right_apply {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (v w : E) :
⇑(inner_right v) w = inner v w

Inner product space structure on product spaces #

source
@[protected, instance]
def pi_Lp.inner_product_space {𝕜 : Type u_1} [is_R_or_C 𝕜] {ι : Type u_2} [fintype ι] (f : ι → Type u_3) [Π (i : ι), inner_product_space 𝕜 (f i)] :
inner_product_space 𝕜 (pi_Lp 2 one_le_two f)
Equations
source
@[simp]
theorem pi_Lp.inner_apply {𝕜 : Type u_1} [is_R_or_C 𝕜] {ι : Type u_2} [fintype ι] {f : ι → Type u_3} [Π (i : ι), inner_product_space 𝕜 (f i)] (x y : pi_Lp 2 one_le_two f) :
inner x y = ∑ (i : ι), inner (x i) (y i)
source
theorem pi_Lp.norm_eq_of_L2 {𝕜 : Type u_1} [is_R_or_C 𝕜] {ι : Type u_2} [fintype ι] {f : ι → Type u_3} [Π (i : ι), inner_product_space 𝕜 (f i)] (x : pi_Lp 2 one_le_two f) :
∥x∥ = real.sqrt (∑ (i : ι), ∥x i∥ ^ 2)
source
@[protected, instance]
def is_R_or_C.inner_product_space {𝕜 : Type u_1} [is_R_or_C 𝕜] :
inner_product_space 𝕜 𝕜

A field 𝕜 satisfying is_R_or_C is itself a 𝕜-inner product space.

Equations
source
@[simp]
theorem is_R_or_C.inner_apply {𝕜 : Type u_1} [is_R_or_C 𝕜] (x y : 𝕜) :
inner x y = (⇑is_R_or_C.conj x) * y
source
@[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
source
theorem euclidean_space.norm_eq {𝕜 : Type u_1} [is_R_or_C 𝕜] {n : Type u_2} [fintype n] (x : euclidean_space 𝕜 n) :
∥x∥ = real.sqrt (∑ (i : n), ∥x i∥ ^ 2)

Inner product space structure on subspaces #

source
@[protected, instance]
def submodule.inner_product_space {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (W : submodule 𝕜 E) :
inner_product_space 𝕜 ↥W

Induced inner product on a submodule.

Equations
source
@[simp]
theorem submodule.coe_inner {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (W : submodule 𝕜 E) (x y : ↥W) :
inner x y = inner ↑x ↑y

The inner product on submodules is the same as on the ambient space.

source
def has_inner.is_R_or_C_to_real (𝕜 : Type u_1) (E : Type u_2) [is_R_or_C 𝕜] [inner_product_space 𝕜 E] :
has_inner ℝ 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
source
def inner_product_space.is_R_or_C_to_real (𝕜 : Type u_1) (E : Type u_2) [is_R_or_C 𝕜] [inner_product_space 𝕜 E] :
inner_product_space ℝ 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
source
theorem real_inner_eq_re_inner (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (x y : E) :
inner x y = ⇑is_R_or_C.re (inner x y)
source
@[protected, instance]
def inner_product_space.complex_to_real {G : Type u_4} [inner_product_space ℂ G] :
inner_product_space ℝ G

A complex inner product implies a real inner product

Equations

Derivative of the inner product #

In this section we prove that the inner product and square of the norm in an inner space are infinitely ℝ-smooth. In order to state these results, we need a normed_space ℝ E instance. Though we can deduce this structure from inner_product_space 𝕜 E, this instance may be not definitionally equal to some other “natural” instance. So, we assume [normed_space ℝ E] and [is_scalar_tower ℝ 𝕜 E]. In both interesting cases 𝕜 = ℝ and 𝕜 = ℂ we have these instances.

source
theorem is_bounded_bilinear_map_inner {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space ℝ E] [is_scalar_tower ℝ 𝕜 E] :
is_bounded_bilinear_map ℝ (λ (p : E × E), inner p.fst p.snd)
source
def fderiv_inner_clm {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space ℝ E] [is_scalar_tower ℝ 𝕜 E] (p : E × E) :
E × E →L[ℝ] 𝕜

Derivative of the inner product.

Equations
source
@[simp]
theorem fderiv_inner_clm_apply {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space ℝ E] [is_scalar_tower ℝ 𝕜 E] (p x : E × E) :
⇑(fderiv_inner_clm p) x = inner p.fst x.snd + inner x.fst p.snd
source
theorem times_cont_diff_inner {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space ℝ E] [is_scalar_tower ℝ 𝕜 E] {n : with_top ℕ} :
times_cont_diff ℝ n (λ (p : E × E), inner p.fst p.snd)
source
theorem times_cont_diff_at_inner {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space ℝ E] [is_scalar_tower ℝ 𝕜 E] {p : E × E} {n : with_top ℕ} :
times_cont_diff_at ℝ n (λ (p : E × E), inner p.fst p.snd) p
source
theorem differentiable_inner {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space ℝ E] [is_scalar_tower ℝ 𝕜 E] :
differentiable ℝ (λ (p : E × E), inner p.fst p.snd)
source
theorem times_cont_diff_within_at.inner {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space ℝ E] [is_scalar_tower ℝ 𝕜 E] {G : Type u_4} [normed_group G] [normed_space ℝ G] {f g : G → E} {s : set G} {x : G} {n : with_top ℕ} (hf : times_cont_diff_within_at ℝ n f s x) (hg : times_cont_diff_within_at ℝ n g s x) :
times_cont_diff_within_at ℝ n (λ (x : G), inner (f x) (g x)) s x
source
theorem times_cont_diff_at.inner {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space ℝ E] [is_scalar_tower ℝ 𝕜 E] {G : Type u_4} [normed_group G] [normed_space ℝ G] {f g : G → E} {x : G} {n : with_top ℕ} (hf : times_cont_diff_at ℝ n f x) (hg : times_cont_diff_at ℝ n g x) :
times_cont_diff_at ℝ n (λ (x : G), inner (f x) (g x)) x
source
theorem times_cont_diff_on.inner {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space ℝ E] [is_scalar_tower ℝ 𝕜 E] {G : Type u_4} [normed_group G] [normed_space ℝ G] {f g : G → E} {s : set G} {n : with_top ℕ} (hf : times_cont_diff_on ℝ n f s) (hg : times_cont_diff_on ℝ n g s) :
times_cont_diff_on ℝ n (λ (x : G), inner (f x) (g x)) s
source
theorem times_cont_diff.inner {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space ℝ E] [is_scalar_tower ℝ 𝕜 E] {G : Type u_4} [normed_group G] [normed_space ℝ G] {f g : G → E} {n : with_top ℕ} (hf : times_cont_diff ℝ n f) (hg : times_cont_diff ℝ n g) :
times_cont_diff ℝ n (λ (x : G), inner (f x) (g x))
source
theorem has_fderiv_within_at.inner {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space ℝ E] [is_scalar_tower ℝ 𝕜 E] {G : Type u_4} [normed_group G] [normed_space ℝ G] {f g : G → E} {f' g' : G →L[ℝ] E} {s : set G} {x : G} (hf : has_fderiv_within_at f f' s x) (hg : has_fderiv_within_at g g' s x) :
has_fderiv_within_at (λ (t : G), inner (f t) (g t)) ((fderiv_inner_clm (f x, g x)).comp (f'.prod g')) s x
source
theorem has_fderiv_at.inner {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space ℝ E] [is_scalar_tower ℝ 𝕜 E] {G : Type u_4} [normed_group G] [normed_space ℝ G] {f g : G → E} {f' g' : G →L[ℝ] E} {x : G} (hf : has_fderiv_at f f' x) (hg : has_fderiv_at g g' x) :
has_fderiv_at (λ (t : G), inner (f t) (g t)) ((fderiv_inner_clm (f x, g x)).comp (f'.prod g')) x
source
theorem has_deriv_within_at.inner {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space ℝ E] [is_scalar_tower ℝ 𝕜 E] {f g : ℝ → E} {f' g' : E} {s : set ℝ} {x : ℝ} (hf : has_deriv_within_at f f' s x) (hg : has_deriv_within_at g g' s x) :
has_deriv_within_at (λ (t : ℝ), inner (f t) (g t)) (inner (f x) g' + inner f' (g x)) s x
source
theorem has_deriv_at.inner {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space ℝ E] [is_scalar_tower ℝ 𝕜 E] {f g : ℝ → E} {f' g' : E} {x : ℝ} :
has_deriv_at f f' x → has_deriv_at g g' x → has_deriv_at (λ (t : ℝ), inner (f t) (g t)) (inner (f x) g' + inner f' (g x)) x
source
theorem differentiable_within_at.inner {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space ℝ E] [is_scalar_tower ℝ 𝕜 E] {G : Type u_4} [normed_group G] [normed_space ℝ G] {f g : G → E} {s : set G} {x : G} (hf : differentiable_within_at ℝ f s x) (hg : differentiable_within_at ℝ g s x) :
differentiable_within_at ℝ (λ (x : G), inner (f x) (g x)) s x
source
theorem differentiable_at.inner {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space ℝ E] [is_scalar_tower ℝ 𝕜 E] {G : Type u_4} [normed_group G] [normed_space ℝ G] {f g : G → E} {x : G} (hf : differentiable_at ℝ f x) (hg : differentiable_at ℝ g x) :
differentiable_at ℝ (λ (x : G), inner (f x) (g x)) x
source
theorem differentiable_on.inner {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space ℝ E] [is_scalar_tower ℝ 𝕜 E] {G : Type u_4} [normed_group G] [normed_space ℝ G] {f g : G → E} {s : set G} (hf : differentiable_on ℝ f s) (hg : differentiable_on ℝ g s) :
differentiable_on ℝ (λ (x : G), inner (f x) (g x)) s
source
theorem differentiable.inner {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space ℝ E] [is_scalar_tower ℝ 𝕜 E] {G : Type u_4} [normed_group G] [normed_space ℝ G] {f g : G → E} (hf : differentiable ℝ f) (hg : differentiable ℝ g) :
differentiable ℝ (λ (x : G), inner (f x) (g x))
source
theorem fderiv_inner_apply {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space ℝ E] [is_scalar_tower ℝ 𝕜 E] {G : Type u_4} [normed_group G] [normed_space ℝ G] {f g : G → E} {x : G} (hf : differentiable_at ℝ f x) (hg : differentiable_at ℝ g x) (y : G) :
⇑(fderiv ℝ (λ (t : G), inner (f t) (g t)) x) y = inner (f x) (⇑(fderiv ℝ g x) y) + inner (⇑(fderiv ℝ f x) y) (g x)
source
theorem deriv_inner_apply {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space ℝ E] [is_scalar_tower ℝ 𝕜 E] {f g : ℝ → E} {x : ℝ} (hf : differentiable_at ℝ f x) (hg : differentiable_at ℝ g x) :
deriv (λ (t : ℝ), inner (f t) (g t)) x = inner (f x) (deriv g x) + inner (deriv f x) (g x)
source
theorem times_cont_diff_norm_sq {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space ℝ E] [is_scalar_tower ℝ 𝕜 E] {n : with_top ℕ} :
times_cont_diff ℝ n (λ (x : E), ∥x∥ ^ 2)
source
theorem times_cont_diff.norm_sq {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space ℝ E] [is_scalar_tower ℝ 𝕜 E] {G : Type u_4} [normed_group G] [normed_space ℝ G] {f : G → E} {n : with_top ℕ} (hf : times_cont_diff ℝ n f) :
times_cont_diff ℝ n (λ (x : G), ∥f x∥ ^ 2)
source
theorem times_cont_diff_within_at.norm_sq {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space ℝ E] [is_scalar_tower ℝ 𝕜 E] {G : Type u_4} [normed_group G] [normed_space ℝ G] {f : G → E} {s : set G} {x : G} {n : with_top ℕ} (hf : times_cont_diff_within_at ℝ n f s x) :
times_cont_diff_within_at ℝ n (λ (y : G), ∥f y∥ ^ 2) s x
source
theorem times_cont_diff_at.norm_sq {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space ℝ E] [is_scalar_tower ℝ 𝕜 E] {G : Type u_4} [normed_group G] [normed_space ℝ G] {f : G → E} {x : G} {n : with_top ℕ} (hf : times_cont_diff_at ℝ n f x) :
times_cont_diff_at ℝ n (λ (y : G), ∥f y∥ ^ 2) x
source
theorem times_cont_diff_at_norm {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space ℝ E] [is_scalar_tower ℝ 𝕜 E] {n : with_top ℕ} {x : E} (hx : x ≠ 0) :
times_cont_diff_at ℝ n norm x
source
theorem times_cont_diff_at.norm {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space ℝ E] [is_scalar_tower ℝ 𝕜 E] {G : Type u_4} [normed_group G] [normed_space ℝ G] {f : G → E} {x : G} {n : with_top ℕ} (hf : times_cont_diff_at ℝ n f x) (h0 : f x ≠ 0) :
times_cont_diff_at ℝ n (λ (y : G), ∥f y∥) x
source
theorem times_cont_diff_at.dist {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space ℝ E] [is_scalar_tower ℝ 𝕜 E] {G : Type u_4} [normed_group G] [normed_space ℝ G] {f g : G → E} {x : G} {n : with_top ℕ} (hf : times_cont_diff_at ℝ n f x) (hg : times_cont_diff_at ℝ n g x) (hne : f x ≠ g x) :
times_cont_diff_at ℝ n (λ (y : G), dist (f y) (g y)) x
source
theorem times_cont_diff_within_at.norm {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space ℝ E] [is_scalar_tower ℝ 𝕜 E] {G : Type u_4} [normed_group G] [normed_space ℝ G] {f : G → E} {s : set G} {x : G} {n : with_top ℕ} (hf : times_cont_diff_within_at ℝ n f s x) (h0 : f x ≠ 0) :
times_cont_diff_within_at ℝ n (λ (y : G), ∥f y∥) s x
source
theorem times_cont_diff_within_at.dist {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space ℝ E] [is_scalar_tower ℝ 𝕜 E] {G : Type u_4} [normed_group G] [normed_space ℝ G] {f g : G → E} {s : set G} {x : G} {n : with_top ℕ} (hf : times_cont_diff_within_at ℝ n f s x) (hg : times_cont_diff_within_at ℝ n g s x) (hne : f x ≠ g x) :
times_cont_diff_within_at ℝ n (λ (y : G), dist (f y) (g y)) s x
source
theorem times_cont_diff_on.norm_sq {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space ℝ E] [is_scalar_tower ℝ 𝕜 E] {G : Type u_4} [normed_group G] [normed_space ℝ G] {f : G → E} {s : set G} {n : with_top ℕ} (hf : times_cont_diff_on ℝ n f s) :
times_cont_diff_on ℝ n (λ (y : G), ∥f y∥ ^ 2) s
source
theorem times_cont_diff_on.norm {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space ℝ E] [is_scalar_tower ℝ 𝕜 E] {G : Type u_4} [normed_group G] [normed_space ℝ G] {f : G → E} {s : set G} {n : with_top ℕ} (hf : times_cont_diff_on ℝ n f s) (h0 : ∀ (x : G), x ∈ s → f x ≠ 0) :
times_cont_diff_on ℝ n (λ (y : G), ∥f y∥) s
source
theorem times_cont_diff_on.dist {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space ℝ E] [is_scalar_tower ℝ 𝕜 E] {G : Type u_4} [normed_group G] [normed_space ℝ G] {f g : G → E} {s : set G} {n : with_top ℕ} (hf : times_cont_diff_on ℝ n f s) (hg : times_cont_diff_on ℝ n g s) (hne : ∀ (x : G), x ∈ s → f x ≠ g x) :
times_cont_diff_on ℝ n (λ (y : G), dist (f y) (g y)) s
source
theorem times_cont_diff.norm {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space ℝ E] [is_scalar_tower ℝ 𝕜 E] {G : Type u_4} [normed_group G] [normed_space ℝ G] {f : G → E} {n : with_top ℕ} (hf : times_cont_diff ℝ n f) (h0 : ∀ (x : G), f x ≠ 0) :
times_cont_diff ℝ n (λ (y : G), ∥f y∥)
source
theorem times_cont_diff.dist {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space ℝ E] [is_scalar_tower ℝ 𝕜 E] {G : Type u_4} [normed_group G] [normed_space ℝ G] {f g : G → E} {n : with_top ℕ} (hf : times_cont_diff ℝ n f) (hg : times_cont_diff ℝ n g) (hne : ∀ (x : G), f x ≠ g x) :
times_cont_diff ℝ n (λ (y : G), dist (f y) (g y))
source
theorem differentiable_at.norm_sq {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space ℝ E] [is_scalar_tower ℝ 𝕜 E] {G : Type u_4} [normed_group G] [normed_space ℝ G] {f : G → E} {x : G} (hf : differentiable_at ℝ f x) :
differentiable_at ℝ (λ (y : G), ∥f y∥ ^ 2) x
source
theorem differentiable_at.norm {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space ℝ E] [is_scalar_tower ℝ 𝕜 E] {G : Type u_4} [normed_group G] [normed_space ℝ G] {f : G → E} {x : G} (hf : differentiable_at ℝ f x) (h0 : f x ≠ 0) :
differentiable_at ℝ (λ (y : G), ∥f y∥) x
source
theorem differentiable_at.dist {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space ℝ E] [is_scalar_tower ℝ 𝕜 E] {G : Type u_4} [normed_group G] [normed_space ℝ G] {f g : G → E} {x : G} (hf : differentiable_at ℝ f x) (hg : differentiable_at ℝ g x) (hne : f x ≠ g x) :
differentiable_at ℝ (λ (y : G), dist (f y) (g y)) x
source
theorem differentiable.norm_sq {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space ℝ E] [is_scalar_tower ℝ 𝕜 E] {G : Type u_4} [normed_group G] [normed_space ℝ G] {f : G → E} (hf : differentiable ℝ f) :
differentiable ℝ (λ (y : G), ∥f y∥ ^ 2)
source
theorem differentiable.norm {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space ℝ E] [is_scalar_tower ℝ 𝕜 E] {G : Type u_4} [normed_group G] [normed_space ℝ G] {f : G → E} (hf : differentiable ℝ f) (h0 : ∀ (x : G), f x ≠ 0) :
differentiable ℝ (λ (y : G), ∥f y∥)
source
theorem differentiable.dist {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space ℝ E] [is_scalar_tower ℝ 𝕜 E] {G : Type u_4} [normed_group G] [normed_space ℝ G] {f g : G → E} (hf : differentiable ℝ f) (hg : differentiable ℝ g) (hne : ∀ (x : G), f x ≠ g x) :
differentiable ℝ (λ (y : G), dist (f y) (g y))
source
theorem differentiable_within_at.norm_sq {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space ℝ E] [is_scalar_tower ℝ 𝕜 E] {G : Type u_4} [normed_group G] [normed_space ℝ G] {f : G → E} {s : set G} {x : G} (hf : differentiable_within_at ℝ f s x) :
differentiable_within_at ℝ (λ (y : G), ∥f y∥ ^ 2) s x
source
theorem differentiable_within_at.norm {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space ℝ E] [is_scalar_tower ℝ 𝕜 E] {G : Type u_4} [normed_group G] [normed_space ℝ G] {f : G → E} {s : set G} {x : G} (hf : differentiable_within_at ℝ f s x) (h0 : f x ≠ 0) :
differentiable_within_at ℝ (λ (y : G), ∥f y∥) s x
source
theorem differentiable_within_at.dist {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space ℝ E] [is_scalar_tower ℝ 𝕜 E] {G : Type u_4} [normed_group G] [normed_space ℝ G] {f g : G → E} {s : set G} {x : G} (hf : differentiable_within_at ℝ f s x) (hg : differentiable_within_at ℝ g s x) (hne : f x ≠ g x) :
differentiable_within_at ℝ (λ (y : G), dist (f y) (g y)) s x
source
theorem differentiable_on.norm_sq {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space ℝ E] [is_scalar_tower ℝ 𝕜 E] {G : Type u_4} [normed_group G] [normed_space ℝ G] {f : G → E} {s : set G} (hf : differentiable_on ℝ f s) :
differentiable_on ℝ (λ (y : G), ∥f y∥ ^ 2) s
source
theorem differentiable_on.norm {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space ℝ E] [is_scalar_tower ℝ 𝕜 E] {G : Type u_4} [normed_group G] [normed_space ℝ G] {f : G → E} {s : set G} (hf : differentiable_on ℝ f s) (h0 : ∀ (x : G), x ∈ s → f x ≠ 0) :
differentiable_on ℝ (λ (y : G), ∥f y∥) s
source
theorem differentiable_on.dist {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space ℝ E] [is_scalar_tower ℝ 𝕜 E] {G : Type u_4} [normed_group G] [normed_space ℝ G] {f g : G → E} {s : set G} (hf : differentiable_on ℝ f s) (hg : differentiable_on ℝ g s) (hne : ∀ (x : G), x ∈ s → f x ≠ g x) :
differentiable_on ℝ (λ (y : G), dist (f y) (g y)) s

Continuity and measurability of the inner product #

Since the inner product is ℝ-smooth, it is continuous. We do not need a [normed_space ℝ E] structure to state this fact and its corollaries, so we introduce them in the proof instead.

source
theorem continuous_inner {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] :
continuous (λ (p : E × E), inner p.fst p.snd)
source
theorem filter.tendsto.inner {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {α : Type u_4} {f g : α → E} {l : filter α} {x y : E} (hf : filter.tendsto f l (𝓝 x)) (hg : filter.tendsto g l (𝓝 y)) :
filter.tendsto (λ (t : α), inner (f t) (g t)) l (𝓝 (inner x y))
source
theorem measurable.inner {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {α : Type u_4} [measurable_space α] [measurable_space E] [opens_measurable_space E] [topological_space.second_countable_topology E] [measurable_space 𝕜] [borel_space 𝕜] {f g : α → E} (hf : measurable f) (hg : measurable g) :
measurable (λ (t : α), inner (f t) (g t))
source
theorem ae_measurable.inner {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {α : Type u_4} [measurable_space α] [measurable_space E] [opens_measurable_space E] [topological_space.second_countable_topology E] [measurable_space 𝕜] [borel_space 𝕜] {μ : measure_theory.measure α} {f g : α → E} (hf : ae_measurable f μ) (hg : ae_measurable g μ) :
ae_measurable (λ (x : α), inner (f x) (g x)) μ
source
theorem continuous_within_at.inner {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {α : Type u_4} [topological_space α] {f g : α → E} {x : α} {s : set α} (hf : continuous_within_at f s x) (hg : continuous_within_at g s x) :
continuous_within_at (λ (t : α), inner (f t) (g t)) s x
source
theorem continuous_at.inner {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {α : Type u_4} [topological_space α] {f g : α → E} {x : α} (hf : continuous_at f x) (hg : continuous_at g x) :
continuous_at (λ (t : α), inner (f t) (g t)) x
source
theorem continuous_on.inner {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {α : Type u_4} [topological_space α] {f g : α → E} {s : set α} (hf : continuous_on f s) (hg : continuous_on g s) :
continuous_on (λ (t : α), inner (f t) (g t)) s
source
theorem continuous.inner {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {α : Type u_4} [topological_space α] {f g : α → E} (hf : continuous f) (hg : continuous g) :
continuous (λ (t : α), inner (f t) (g t))
source
@[protected, instance]
def euclidean_space.finite_dimensional {𝕜 : Type u_1} [is_R_or_C 𝕜] {ι : Type u_4} [fintype ι] :
finite_dimensional 𝕜 (euclidean_space 𝕜 ι)
source
@[protected, instance]
def euclidean_space.inner_product_space {𝕜 : Type u_1} [is_R_or_C 𝕜] {ι : Type u_4} [fintype ι] :
inner_product_space 𝕜 (euclidean_space 𝕜 ι)
Equations
source
@[simp]
theorem finrank_euclidean_space {𝕜 : Type u_1} [is_R_or_C 𝕜] {ι : Type u_4} [fintype ι] :
finite_dimensional.finrank 𝕜 (euclidean_space 𝕜 ι) = fintype.card ι
source
theorem finrank_euclidean_space_fin {𝕜 : Type u_1} [is_R_or_C 𝕜] {n : ℕ} :
finite_dimensional.finrank 𝕜 (euclidean_space 𝕜 (fin n)) = n
source
def basis.isometry_euclidean_of_orthonormal {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {ι : Type u_4} [fintype ι] (v : basis ι 𝕜 E) (hv : orthonormal 𝕜 ⇑v) :
E ≃ₗᵢ[𝕜] euclidean_space 𝕜 ι

An orthonormal basis on a fintype ι for an inner product space induces an isometry with euclidean_space 𝕜 ι.

Equations
source
def complex.isometry_euclidean  :
ℂ ≃ₗᵢ[ℝ] euclidean_space ℝ (fin 2)

ℂ is isometric to ℝ² with the Euclidean inner product.

Equations
source
@[simp]
theorem complex.isometry_euclidean_symm_apply (x : euclidean_space ℝ (fin 2)) :
⇑(complex.isometry_euclidean.symm) x = ↑(x 0) + (↑(x 1)) * is_R_or_C.I
source
theorem complex.isometry_euclidean_proj_eq_self (z : ℂ) :
↑(⇑complex.isometry_euclidean z 0) + (↑(⇑complex.isometry_euclidean z 1)) * is_R_or_C.I = z
source
@[simp]
theorem complex.isometry_euclidean_apply_zero (z : ℂ) :
⇑complex.isometry_euclidean z 0 = z.re
source
@[simp]
theorem complex.isometry_euclidean_apply_one (z : ℂ) :
⇑complex.isometry_euclidean z 1 = z.im

Orthogonal projection in inner product spaces #

source
theorem exists_norm_eq_infi_of_complete_convex {F : Type u_3} [inner_product_space ℝ F] {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.

source
theorem norm_eq_infi_iff_real_inner_le_zero {F : Type u_3} [inner_product_space ℝ F] {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.

source
theorem exists_norm_eq_infi_of_complete_subspace {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (K : submodule 𝕜 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.

source
theorem norm_eq_infi_iff_real_inner_eq_zero {F : Type u_3} [inner_product_space ℝ F] (K : submodule ℝ 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.

source
theorem norm_eq_infi_iff_inner_eq_zero {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (K : submodule 𝕜 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)

source
def orthogonal_projection_fn {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (K : submodule 𝕜 E) [complete_space ↥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
source
theorem orthogonal_projection_fn_mem {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {K : submodule 𝕜 E} [complete_space ↥K] (v : E) :
orthogonal_projection_fn K v ∈ K

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.

source
theorem orthogonal_projection_fn_inner_eq_zero {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {K : submodule 𝕜 E} [complete_space ↥K] (v w : E) (H : w ∈ K) :
inner (v - orthogonal_projection_fn K 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.

source
theorem eq_orthogonal_projection_fn_of_mem_of_inner_eq_zero {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {K : submodule 𝕜 E} [complete_space ↥K] {u v : E} (hvm : v ∈ K) (hvo : ∀ (w : E), w ∈ K → inner (u - v) w = 0) :
orthogonal_projection_fn K u = v

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.

source
theorem orthogonal_projection_fn_norm_sq {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (K : submodule 𝕜 E) [complete_space ↥K] (v : E) :
∥v∥ * ∥v∥ = ∥v - orthogonal_projection_fn K v∥ * ∥v - orthogonal_projection_fn K v∥ + ∥orthogonal_projection_fn K v∥ * ∥orthogonal_projection_fn K v∥
source
def orthogonal_projection {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (K : submodule 𝕜 E) [complete_space ↥K] :
E →L[𝕜] ↥K

The orthogonal projection onto a complete subspace.

Equations
source
@[simp]
theorem orthogonal_projection_fn_eq {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {K : submodule 𝕜 E} [complete_space ↥K] (v : E) :
orthogonal_projection_fn K v = ↑(⇑(orthogonal_projection K) v)
source
@[simp]
theorem orthogonal_projection_inner_eq_zero {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {K : submodule 𝕜 E} [complete_space ↥K] (v w : E) (H : w ∈ K) :
inner (v - ↑(⇑(orthogonal_projection K) v)) w = 0

The characterization of the orthogonal projection.

source
theorem eq_orthogonal_projection_of_mem_of_inner_eq_zero {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {K : submodule 𝕜 E} [complete_space ↥K] {u v : E} (hvm : v ∈ K) (hvo : ∀ (w : E), w ∈ K → inner (u - v) w = 0) :
↑(⇑(orthogonal_projection K) u) = v

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

source
theorem eq_orthogonal_projection_of_eq_submodule {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {K : submodule 𝕜 E} [complete_space ↥K] {K' : submodule 𝕜 E} [complete_space ↥K'] (h : K = K') (u : E) :
↑(⇑(orthogonal_projection K) u) = ↑(⇑(orthogonal_projection K') u)

The orthogonal projections onto equal subspaces are coerced back to the same point in E.

source
@[simp]
theorem orthogonal_projection_mem_subspace_eq_self {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {K : submodule 𝕜 E} [complete_space ↥K] (v : ↥K) :
⇑(orthogonal_projection K) ↑v = v

The orthogonal projection sends elements of K to themselves.

source
@[simp]
theorem orthogonal_projection_bot {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] :
orthogonal_projection ⊥ = 0

The orthogonal projection onto the trivial submodule is the zero map.

source
theorem orthogonal_projection_norm_le {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (K : submodule 𝕜 E) [complete_space ↥K] :
∥orthogonal_projection K∥ ≤ 1

The orthogonal projection has norm ≤ 1.

source
theorem smul_orthogonal_projection_singleton (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {v : E} (w : E) :
↑∥v∥ ^ 2 • ↑(⇑(orthogonal_projection (submodule.span 𝕜 {v})) w) = inner v w • v
source
theorem orthogonal_projection_singleton (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {v : E} (w : E) :
↑(⇑(orthogonal_projection (submodule.span 𝕜 {v})) w) = (inner v w / ↑∥v∥ ^ 2) • v

Formula for orthogonal projection onto a single vector.

source
theorem orthogonal_projection_unit_singleton (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {v : E} (hv : ∥v∥ = 1) (w : E) :
↑(⇑(orthogonal_projection (submodule.span 𝕜 {v})) w) = inner v w • v

Formula for orthogonal projection onto a single unit vector.

source
def submodule.orthogonal {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (K : submodule 𝕜 E) :
submodule 𝕜 E

The subspace of vectors orthogonal to a given subspace.

Equations
source
theorem submodule.mem_orthogonal {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (K : submodule 𝕜 E) (v : E) :
v ∈ Kᗮ ↔ ∀ (u : E), u ∈ K → inner u v = 0

When a vector is in Kᗮ.

source
theorem submodule.mem_orthogonal' {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (K : submodule 𝕜 E) (v : E) :
v ∈ Kᗮ ↔ ∀ (u : E), u ∈ K → inner v u = 0

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

source
theorem submodule.inner_right_of_mem_orthogonal {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {K : submodule 𝕜 E} {u v : E} (hu : u ∈ K) (hv : v ∈ Kᗮ) :
inner u v = 0

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

source
theorem submodule.inner_left_of_mem_orthogonal {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {K : submodule 𝕜 E} {u v : E} (hu : u ∈ K) (hv : v ∈ Kᗮ) :
inner v u = 0

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

source
theorem inner_right_of_mem_orthogonal_singleton {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (u : E) {v : E} (hv : v ∈ (submodule.span 𝕜 {u})ᗮ) :
inner u v = 0

A vector in (𝕜 ∙ u)ᗮ is orthogonal to u.

source
theorem inner_left_of_mem_orthogonal_singleton {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (u : E) {v : E} (hv : v ∈ (submodule.span 𝕜 {u})ᗮ) :
inner v u = 0

A vector in (𝕜 ∙ u)ᗮ is orthogonal to u.

source
theorem submodule.inf_orthogonal_eq_bot {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (K : submodule 𝕜 E) :
K ⊓ Kᗮ = ⊥

K and Kᗮ have trivial intersection.

source
theorem submodule.orthogonal_disjoint {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (K : submodule 𝕜 E) :
disjoint K Kᗮ

K and Kᗮ have trivial intersection.

source
theorem orthogonal_eq_inter {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (K : submodule 𝕜 E) :
Kᗮ = ⨅ (v : ↥K), (inner_right ↑v).ker

Kᗮ can be characterized as the intersection of the kernels of the operations of inner product with each of the elements of K.

source
theorem submodule.is_closed_orthogonal {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (K : submodule 𝕜 E) :
is_closed ↑Kᗮ

The orthogonal complement of any submodule K is closed.

source
@[protected, instance]
def submodule.orthogonal.complete_space {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (K : submodule 𝕜 E) [complete_space E] :
complete_space ↥Kᗮ

In a complete space, the orthogonal complement of any submodule K is complete.

source
theorem submodule.orthogonal_gc (𝕜 : Type u_1) (E : Type u_2) [is_R_or_C 𝕜] [inner_product_space 𝕜 E] :
galois_connection submodule.orthogonal submodule.orthogonal

submodule.orthogonal gives a galois_connection between submodule 𝕜 E and its order_dual.

source
theorem submodule.orthogonal_le {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {K₁ K₂ : submodule 𝕜 E} (h : K₁ ≤ K₂) :
K₂ᗮ ≤ K₁ᗮ

submodule.orthogonal reverses the ≤ ordering of two subspaces.

source
theorem submodule.orthogonal_orthogonal_monotone {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {K₁ K₂ : submodule 𝕜 E} (h : K₁ ≤ K₂) :
K₁ᗮᗮ ≤ K₂ᗮᗮ

submodule.orthogonal.orthogonal preserves the ≤ ordering of two subspaces.

source
theorem submodule.le_orthogonal_orthogonal {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (K : submodule 𝕜 E) :
K ≤ Kᗮᗮ

K is contained in Kᗮᗮ.

source
theorem submodule.inf_orthogonal {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (K₁ K₂ : submodule 𝕜 E) :
K₁ᗮ ⊓ K₂ᗮ = (K₁ ⊔ K₂)ᗮ

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

source
theorem submodule.infi_orthogonal {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {ι : Type u_3} (K : ι → submodule 𝕜 E) :
(⨅ (i : ι), (K i)ᗮ) = (supr K)ᗮ

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

source
theorem submodule.Inf_orthogonal {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (s : set (submodule 𝕜 E)) :
(⨅ (K : submodule 𝕜 E) (H : K ∈ s), Kᗮ) = (Sup s)ᗮ

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

source
theorem submodule.sup_orthogonal_inf_of_is_complete {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {K₁ K₂ : submodule 𝕜 E} (h : K₁ ≤ K₂) (hc : is_complete ↑K₁) :
K₁ ⊔ K₁ᗮ ⊓ K₂ = K₂

If K₁ is complete and contained in K₂, K₁ and K₁ᗮ ⊓ K₂ span K₂.

source
theorem submodule.sup_orthogonal_of_is_complete {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {K : submodule 𝕜 E} (h : is_complete ↑K) :
K ⊔ Kᗮ = ⊤

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

source
theorem submodule.sup_orthogonal_of_complete_space {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {K : submodule 𝕜 E} [complete_space ↥K] :
K ⊔ Kᗮ = ⊤

If K is complete, K and Kᗮ span the whole space. Version using complete_space.

source
theorem submodule.exists_sum_mem_mem_orthogonal {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (K : submodule 𝕜 E) [complete_space ↥K] (v : E) :
∃ (y : E) (H : y ∈ K) (z : E) (H : z ∈ Kᗮ), v = y + z

If K is complete, any v in E can be expressed as a sum of elements of K and Kᗮ.

source
@[simp]
theorem submodule.orthogonal_orthogonal {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (K : submodule 𝕜 E) [complete_space ↥K] :
Kᗮᗮ = K

If K is complete, then the orthogonal complement of its orthogonal complement is itself.

source
theorem submodule.orthogonal_orthogonal_eq_closure {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (K : submodule 𝕜 E) [complete_space E] :
Kᗮᗮ = K.topological_closure
source
theorem submodule.is_compl_orthogonal_of_is_complete {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {K : submodule 𝕜 E} (h : is_complete ↑K) :
is_compl K Kᗮ

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

source
@[simp]
theorem submodule.top_orthogonal_eq_bot {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] :
⊤ᗮ = ⊥
source
@[simp]
theorem submodule.bot_orthogonal_eq_top {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] :
⊥ᗮ = ⊤
source
@[simp]
theorem submodule.orthogonal_eq_bot_iff {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {K : submodule 𝕜 E} (hK : is_complete ↑K) :
Kᗮ = ⊥ ↔ K = ⊤
source
@[simp]
theorem submodule.orthogonal_eq_top_iff {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {K : submodule 𝕜 E} :
Kᗮ = ⊤ ↔ K = ⊥
source
theorem eq_orthogonal_projection_of_mem_orthogonal {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {K : submodule 𝕜 E} [complete_space ↥K] {u v : E} (hv : v ∈ K) (hvo : u - v ∈ Kᗮ) :
↑(⇑(orthogonal_projection K) u) = v

A point in K with the orthogonality property (here characterized in terms of Kᗮ) must be the orthogonal projection.

source
theorem eq_orthogonal_projection_of_mem_orthogonal' {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {K : submodule 𝕜 E} [complete_space ↥K] {u v z : E} (hv : v ∈ K) (hz : z ∈ Kᗮ) (hu : u = v + z) :
↑(⇑(orthogonal_projection K) u) = v

A point in K with the orthogonality property (here characterized in terms of Kᗮ) must be the orthogonal projection.

source
theorem orthogonal_projection_mem_subspace_orthogonal_complement_eq_zero {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {K : submodule 𝕜 E} [complete_space ↥K] {v : E} (hv : v ∈ Kᗮ) :
⇑(orthogonal_projection K) v = 0

The orthogonal projection onto K of an element of Kᗮ is zero.

source
theorem orthogonal_projection_mem_subspace_orthogonal_precomplement_eq_zero {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {K : submodule 𝕜 E} [complete_space E] {v : E} (hv : v ∈ K) :
⇑(orthogonal_projection Kᗮ) v = 0

The orthogonal projection onto Kᗮ of an element of K is zero.

source
theorem orthogonal_projection_orthogonal_complement_singleton_eq_zero {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [complete_space E] (v : E) :
⇑(orthogonal_projection (submodule.span 𝕜 {v})ᗮ) v = 0

The orthogonal projection onto (𝕜 ∙ v)ᗮ of v is zero.

source
theorem eq_sum_orthogonal_projection_self_orthogonal_complement {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (K : submodule 𝕜 E) [complete_space E] [complete_space ↥K] (w : E) :
w = ↑(⇑(orthogonal_projection K) w) + ↑(⇑(orthogonal_projection Kᗮ) w)

In a complete space E, a vector splits as the sum of its orthogonal projections onto a complete submodule K and onto the orthogonal complement of K.

source
theorem id_eq_sum_orthogonal_projection_self_orthogonal_complement {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (K : submodule 𝕜 E) [complete_space E] [complete_space ↥K] :
continuous_linear_map.id 𝕜 E = K.subtypeL.comp (orthogonal_projection K) + Kᗮ.subtypeL.comp (orthogonal_projection Kᗮ)

In a complete space E, the projection maps onto a complete subspace K and its orthogonal complement sum to the identity.

source
theorem submodule.finrank_add_inf_finrank_orthogonal {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {K₁ K₂ : submodule 𝕜 E} [finite_dimensional 𝕜 ↥K₂] (h : K₁ ≤ K₂) :
finite_dimensional.finrank 𝕜 ↥K₁ + finite_dimensional.finrank 𝕜 ↥(K₁ᗮ ⊓ K₂) = finite_dimensional.finrank 𝕜 ↥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₂.

source
theorem submodule.finrank_add_inf_finrank_orthogonal' {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {K₁ K₂ : submodule 𝕜 E} [finite_dimensional 𝕜 ↥K₂] (h : K₁ ≤ K₂) {n : ℕ} (h_dim : finite_dimensional.finrank 𝕜 ↥K₁ + n = finite_dimensional.finrank 𝕜 ↥K₂) :
finite_dimensional.finrank 𝕜 ↥(K₁ᗮ ⊓ K₂) = n

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₂.

source
theorem submodule.finrank_add_finrank_orthogonal {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [finite_dimensional 𝕜 E] {K : submodule 𝕜 E} :
finite_dimensional.finrank 𝕜 ↥K + finite_dimensional.finrank 𝕜 ↥Kᗮ = finite_dimensional.finrank 𝕜 E

Given a finite-dimensional space E and subspace K, the dimensions of K and Kᗮ add to that of E.

source
theorem submodule.finrank_add_finrank_orthogonal' {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [finite_dimensional 𝕜 E] {K : submodule 𝕜 E} {n : ℕ} (h_dim : finite_dimensional.finrank 𝕜 ↥K + n = finite_dimensional.finrank 𝕜 E) :
finite_dimensional.finrank 𝕜 ↥Kᗮ = n

Given a finite-dimensional space E and subspace K, the dimensions of K and Kᗮ add to that of E.

source
theorem finrank_orthogonal_span_singleton {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {n : ℕ} [fact (finite_dimensional.finrank 𝕜 E = n + 1)] {v : E} (hv : v ≠ 0) :
finite_dimensional.finrank 𝕜 ↥(submodule.span 𝕜 {v})ᗮ = n

In a finite-dimensional inner product space, the dimension of the orthogonal complement of the span of a nonzero vector is one less than the dimension of the space.

Existence of Hilbert basis, orthonormal basis, etc. #

source
theorem maximal_orthonormal_iff_orthogonal_complement_eq_bot {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {v : set E} (hv : orthonormal 𝕜 coe) :
(∀ (u : set E), u ⊇ v → orthonormal 𝕜 coe → u = v) ↔ (submodule.span 𝕜 v)ᗮ = ⊥

An orthonormal set in an inner_product_space is maximal, if and only if the orthogonal complement of its span is empty.

source
theorem maximal_orthonormal_iff_dense_span {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {v : set E} [complete_space E] (hv : orthonormal 𝕜 coe) :
(∀ (u : set E), u ⊇ v → orthonormal 𝕜 coe → u = v) ↔ (submodule.span 𝕜 v).topological_closure = ⊤

An orthonormal set in an inner_product_space is maximal, if and only if the closure of its span is the whole space.

source
theorem exists_subset_is_orthonormal_dense_span {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {v : set E} [complete_space E] (hv : orthonormal 𝕜 coe) :
∃ (u : set E) (H : u ⊇ v), orthonormal 𝕜 coe ∧ (submodule.span 𝕜 u).topological_closure = ⊤

Any orthonormal subset can be extended to an orthonormal set whose span is dense.

source
theorem exists_is_orthonormal_dense_span (𝕜 : Type u_1) (E : Type u_2) [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [complete_space E] :
∃ (u : set E), orthonormal 𝕜 coe ∧ (submodule.span 𝕜 u).topological_closure = ⊤

An inner product space admits an orthonormal set whose span is dense.

source
theorem maximal_orthonormal_iff_basis_of_finite_dimensional {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {v : set E} [finite_dimensional 𝕜 E] (hv : orthonormal 𝕜 coe) :
(∀ (u : set E), u ⊇ v → orthonormal 𝕜 coe → u = v) ↔ ∃ (b : basis ↥v 𝕜 E), ⇑b = coe

An orthonormal set in a finite-dimensional inner_product_space is maximal, if and only if it is a basis.

source
theorem exists_subset_is_orthonormal_basis {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {v : set E} [finite_dimensional 𝕜 E] (hv : orthonormal 𝕜 coe) :
∃ (u : set E) (H : u ⊇ v) (b : basis ↥u 𝕜 E), orthonormal 𝕜 ⇑b ∧ ⇑b = coe

In a finite-dimensional inner_product_space, any orthonormal subset can be extended to an orthonormal basis.

source
def orthonormal_basis_index (𝕜 : Type u_1) (E : Type u_2) [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [finite_dimensional 𝕜 E] :
set E

Index for an arbitrary orthonormal basis on a finite-dimensional inner_product_space.

Equations
source
def orthonormal_basis (𝕜 : Type u_1) (E : Type u_2) [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [finite_dimensional 𝕜 E] :
basis ↥(orthonormal_basis_index 𝕜 E) 𝕜 E

A finite-dimensional inner_product_space has an orthonormal basis.

Equations
source
theorem orthonormal_basis_orthonormal (𝕜 : Type u_1) (E : Type u_2) [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [finite_dimensional 𝕜 E] :
orthonormal 𝕜 ⇑(orthonormal_basis 𝕜 E)
source
@[simp]
theorem coe_orthonormal_basis (𝕜 : Type u_1) (E : Type u_2) [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [finite_dimensional 𝕜 E] :
⇑(orthonormal_basis 𝕜 E) = coe
source
@[protected, instance]
def orthonormal_basis_index.fintype (𝕜 : Type u_1) (E : Type u_2) [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [finite_dimensional 𝕜 E] :
fintype ↥(orthonormal_basis_index 𝕜 E)
Equations
source
def fin_orthonormal_basis {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [finite_dimensional 𝕜 E] {n : ℕ} (hn : finite_dimensional.finrank 𝕜 E = n) :
basis (fin n) 𝕜 E

An n-dimensional inner_product_space has an orthonormal basis indexed by fin n.

Equations
source
theorem fin_orthonormal_basis_orthonormal {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [finite_dimensional 𝕜 E] {n : ℕ} (hn : finite_dimensional.finrank 𝕜 E = n) :
orthonormal 𝕜 ⇑(fin_orthonormal_basis hn)
source
def linear_isometry_equiv.of_inner_product_space {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [finite_dimensional 𝕜 E] {n : ℕ} (hn : finite_dimensional.finrank 𝕜 E = n) :
E ≃ₗᵢ[𝕜] euclidean_space 𝕜 (fin n)

Given a natural number n equal to the finrank of a finite-dimensional inner product space, there exists an isometry from the space to euclidean_space 𝕜 (fin n).

Equations
source
def linear_isometry_equiv.from_orthogonal_span_singleton {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (n : ℕ) [fact (finite_dimensional.finrank 𝕜 E = n + 1)] {v : E} (hv : v ≠ 0) :
↥(submodule.span 𝕜 {v})ᗮ ≃ₗᵢ[𝕜] euclidean_space 𝕜 (fin n)

Given a natural number n one less than the finrank of a finite-dimensional inner product space, there exists an isometry from the orthogonal complement of a nonzero singleton to euclidean_space 𝕜 (fin n).

Equations