Inner product space

This file defines inner product spaces and proves the basic properties. We do not formally define Hilbert spaces, but they can be obtained using the set of assumptions [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E].

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 RCLike typeclass.

This file proves general results on inner product spaces. For the specific construction of an inner product structure on n → 𝕜 for 𝕜 = ℝ or ℂ, see EuclideanSpace in Analysis.InnerProductSpace.PiL2.

Main results

• We define the class InnerProductSpace 𝕜 E extending NormedSpace 𝕜 E with a number of basic properties, most notably the Cauchy-Schwarz inequality. Here 𝕜 is understood to be either ℝ or ℂ, through the RCLike typeclass.
• We show that the inner product is continuous, continuous_inner, and bundle it as the continuous sesquilinear map innerSL (see also innerₛₗ for the non-continuous version).
• We define Orthonormal, a predicate on a function v : ι → E, and prove the existence of a maximal orthonormal set, exists_maximal_orthonormal. Bessel's inequality, Orthonormal.tsum_inner_products_le, states that given an orthonormal set v and a vector x, the sum of the norm-squares of the inner products ⟪v i, x⟫ is no more than the norm-square of x. For the existence of orthonormal bases, Hilbert bases, etc., see the file Analysis.InnerProductSpace.projection.

Notation

We globally denote the real and complex inner products by ⟪·, ·⟫_ℝ and ⟪·, ·⟫_ℂ respectively. We also provide two notation namespaces: RealInnerProductSpace, ComplexInnerProductSpace, which respectively introduce the plain notation ⟪·, ·⟫ for 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.

Tags

inner product space, Hilbert 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 Inner (𝕜 : Type u_4) (E : Type u_5) : Type (max u_4 u_5)

Syntactic typeclass for types endowed with an inner product

• inner : E → E → 𝕜

  The inner product function.

def «term⟪_,_⟫__».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

def «term⟪_,_⟫__» : Lean.ParserDescr

The inner product with values in 𝕜.

Equations

• One or more equations did not get rendered due to their size.

def RealInnerProductSpace.«term⟪_,_⟫» : Lean.ParserDescr

The inner product with values in ℝ.

Equations

• One or more equations did not get rendered due to their size.

def ComplexInnerProductSpace.«term⟪_,_⟫» : Lean.ParserDescr

The inner product with values in ℂ.

Equations

• One or more equations did not get rendered due to their size.

class InnerProductSpace (𝕜 : Type u_4) (E : Type u_5) [RCLike 𝕜] [NormedAddCommGroup E] extends NormedSpace , Inner : 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 InnerProductSpace.ofCore.

• smul : 𝕜 → E → E
• one_smul : ∀ (b : E), 1 • b = b
• mul_smul : ∀ (x y : 𝕜) (b : E), (x * y) • b = x • y • b
• smul_zero : ∀ (a : 𝕜), a • 0 = 0
• smul_add : ∀ (a : 𝕜) (x y : E), a • (x + y) = a • x + a • y
• add_smul : ∀ (r s : 𝕜) (x : E), (r + s) • x = r • x + s • x
• zero_smul : ∀ (x : E), 0 • x = 0
• norm_smul_le : ∀ (a : 𝕜) (b : E), ‖a • b‖ ≤ ‖a‖ * ‖b‖
• inner : E → E → 𝕜
• norm_sq_eq_inner : ∀ (x : E), ‖x‖ ^ 2 = RCLike.re ⟪x, x⟫_𝕜

  The inner product induces the norm.

• conj_symm : ∀ (x y : E), (starRingEnd 𝕜) ⟪y, x⟫_𝕜 = ⟪x, y⟫_𝕜

  The inner product is hermitian, taking the conj swaps the arguments.

• add_left : ∀ (x y z : E), ⟪x + y, z⟫_𝕜 = ⟪x, z⟫_𝕜 + ⟪y, z⟫_𝕜

  The inner product is additive in the first coordinate.

• smul_left : ∀ (x y : E) (r : 𝕜), ⟪r • x, y⟫_𝕜 = (starRingEnd 𝕜) r * ⟪x, y⟫_𝕜

  The inner product is conjugate linear in the first coordinate.

theorem InnerProductSpace.norm_sq_eq_inner {𝕜 : Type u_4} {E : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [self : InnerProductSpace 𝕜 E] (x : E) : ‖x‖ ^ 2 = RCLike.re ⟪x, x⟫_𝕜

The inner product induces the norm.

theorem InnerProductSpace.conj_symm {𝕜 : Type u_4} {E : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [self : InnerProductSpace 𝕜 E] (x : E) (y : E) : (starRingEnd 𝕜) ⟪y, x⟫_𝕜 = ⟪x, y⟫_𝕜

The inner product is hermitian, taking the conj swaps the arguments.

theorem InnerProductSpace.add_left {𝕜 : Type u_4} {E : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [self : InnerProductSpace 𝕜 E] (x : E) (y : E) (z : E) : ⟪x + y, z⟫_𝕜 = ⟪x, z⟫_𝕜 + ⟪y, z⟫_𝕜

The inner product is additive in the first coordinate.

theorem InnerProductSpace.smul_left {𝕜 : Type u_4} {E : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [self : InnerProductSpace 𝕜 E] (x : E) (y : E) (r : 𝕜) : ⟪r • x, y⟫_𝕜 = (starRingEnd 𝕜) r * ⟪x, y⟫_𝕜

The inner product is conjugate linear in the first coordinate.

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 InnerProductSpace.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 InnerProductSpace. 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!

class InnerProductSpace.Core (𝕜 : Type u_4) (F : Type u_5) [RCLike 𝕜] [AddCommGroup F] [Module 𝕜 F] extends Inner : Type (max u_4 u_5)

A structure requiring that a scalar product is positive definite and symmetric, from which one can construct an InnerProductSpace instance in InnerProductSpace.ofCore.

• inner : F → F → 𝕜
• conj_symm : ∀ (x y : F), (starRingEnd 𝕜) ⟪y, x⟫_𝕜 = ⟪x, y⟫_𝕜

  The inner product is hermitian, taking the conj swaps the arguments.

• nonneg_re : ∀ (x : F), 0 ≤ RCLike.re ⟪x, x⟫_𝕜

  The inner product is positive (semi)definite.

• definite : ∀ (x : F), ⟪x, x⟫_𝕜 = 0 → x = 0

  The inner product is positive definite.

• add_left : ∀ (x y z : F), ⟪x + y, z⟫_𝕜 = ⟪x, z⟫_𝕜 + ⟪y, z⟫_𝕜

  The inner product is additive in the first coordinate.

• smul_left : ∀ (x y : F) (r : 𝕜), ⟪r • x, y⟫_𝕜 = (starRingEnd 𝕜) r * ⟪x, y⟫_𝕜

  The inner product is conjugate linear in the first coordinate.

theorem InnerProductSpace.Core.conj_symm {𝕜 : Type u_4} {F : Type u_5} [RCLike 𝕜] [AddCommGroup F] [Module 𝕜 F] (self : InnerProductSpace.Core 𝕜 F) (x : F) (y : F) : (starRingEnd 𝕜) ⟪y, x⟫_𝕜 = ⟪x, y⟫_𝕜

The inner product is hermitian, taking the conj swaps the arguments.

theorem InnerProductSpace.Core.nonneg_re {𝕜 : Type u_4} {F : Type u_5} [RCLike 𝕜] [AddCommGroup F] [Module 𝕜 F] (self : InnerProductSpace.Core 𝕜 F) (x : F) : 0 ≤ RCLike.re ⟪x, x⟫_𝕜

The inner product is positive (semi)definite.

theorem InnerProductSpace.Core.definite {𝕜 : Type u_4} {F : Type u_5} [RCLike 𝕜] [AddCommGroup F] [Module 𝕜 F] (self : InnerProductSpace.Core 𝕜 F) (x : F) : ⟪x, x⟫_𝕜 = 0 → x = 0

The inner product is positive definite.

theorem InnerProductSpace.Core.add_left {𝕜 : Type u_4} {F : Type u_5} [RCLike 𝕜] [AddCommGroup F] [Module 𝕜 F] (self : InnerProductSpace.Core 𝕜 F) (x : F) (y : F) (z : F) : ⟪x + y, z⟫_𝕜 = ⟪x, z⟫_𝕜 + ⟪y, z⟫_𝕜

The inner product is additive in the first coordinate.

theorem InnerProductSpace.Core.smul_left {𝕜 : Type u_4} {F : Type u_5} [RCLike 𝕜] [AddCommGroup F] [Module 𝕜 F] (self : InnerProductSpace.Core 𝕜 F) (x : F) (y : F) (r : 𝕜) : ⟪r • x, y⟫_𝕜 = (starRingEnd 𝕜) r * ⟪x, y⟫_𝕜

The inner product is conjugate linear in the first coordinate.

def InnerProductSpace.toCore {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [c : InnerProductSpace 𝕜 E] : InnerProductSpace.Core 𝕜 E

Define InnerProductSpace.Core from InnerProductSpace. Defined to reuse lemmas about InnerProductSpace.Core for InnerProductSpaces. Note that the Norm instance provided by InnerProductSpace.Core.norm is propositionally but not definitionally equal to the original norm.

Equations

• InnerProductSpace.toCore = { toInner := InnerProductSpace.toInner, conj_symm := ⋯, nonneg_re := ⋯, definite := ⋯, add_left := ⋯, smul_left := ⋯ }

def InnerProductSpace.Core.toInner' {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [AddCommGroup F] [Module 𝕜 F] [c : InnerProductSpace.Core 𝕜 F] : Inner 𝕜 F

Inner product defined by the InnerProductSpace.Core structure. We can't reuse InnerProductSpace.Core.toInner because it takes InnerProductSpace.Core as an explicit argument.

Equations

• InnerProductSpace.Core.toInner' = c.toInner

def InnerProductSpace.Core.normSq {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [AddCommGroup F] [Module 𝕜 F] [c : InnerProductSpace.Core 𝕜 F] (x : F) : ℝ

The norm squared function for InnerProductSpace.Core structure.

Equations

• InnerProductSpace.Core.normSq x = RCLike.re ⟪x, x⟫_𝕜

theorem InnerProductSpace.Core.inner_conj_symm {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [AddCommGroup F] [Module 𝕜 F] [c : InnerProductSpace.Core 𝕜 F] (x : F) (y : F) : (starRingEnd 𝕜) ⟪y, x⟫_𝕜 = ⟪x, y⟫_𝕜

theorem InnerProductSpace.Core.inner_self_nonneg {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [AddCommGroup F] [Module 𝕜 F] [c : InnerProductSpace.Core 𝕜 F] {x : F} : 0 ≤ RCLike.re ⟪x, x⟫_𝕜

theorem InnerProductSpace.Core.inner_self_im {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [AddCommGroup F] [Module 𝕜 F] [c : InnerProductSpace.Core 𝕜 F] (x : F) : RCLike.im ⟪x, x⟫_𝕜 = 0

theorem InnerProductSpace.Core.inner_add_left {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [AddCommGroup F] [Module 𝕜 F] [c : InnerProductSpace.Core 𝕜 F] (x : F) (y : F) (z : F) : ⟪x + y, z⟫_𝕜 = ⟪x, z⟫_𝕜 + ⟪y, z⟫_𝕜

theorem InnerProductSpace.Core.inner_add_right {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [AddCommGroup F] [Module 𝕜 F] [c : InnerProductSpace.Core 𝕜 F] (x : F) (y : F) (z : F) : ⟪x, y + z⟫_𝕜 = ⟪x, y⟫_𝕜 + ⟪x, z⟫_𝕜

theorem InnerProductSpace.Core.ofReal_normSq_eq_inner_self {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [AddCommGroup F] [Module 𝕜 F] [c : InnerProductSpace.Core 𝕜 F] (x : F) : ↑(InnerProductSpace.Core.normSq x) = ⟪x, x⟫_𝕜

theorem InnerProductSpace.Core.inner_re_symm {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [AddCommGroup F] [Module 𝕜 F] [c : InnerProductSpace.Core 𝕜 F] (x : F) (y : F) : RCLike.re ⟪x, y⟫_𝕜 = RCLike.re ⟪y, x⟫_𝕜

theorem InnerProductSpace.Core.inner_im_symm {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [AddCommGroup F] [Module 𝕜 F] [c : InnerProductSpace.Core 𝕜 F] (x : F) (y : F) : RCLike.im ⟪x, y⟫_𝕜 = -RCLike.im ⟪y, x⟫_𝕜

theorem InnerProductSpace.Core.inner_smul_left {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [AddCommGroup F] [Module 𝕜 F] [c : InnerProductSpace.Core 𝕜 F] (x : F) (y : F) {r : 𝕜} : ⟪r • x, y⟫_𝕜 = (starRingEnd 𝕜) r * ⟪x, y⟫_𝕜

theorem InnerProductSpace.Core.inner_smul_right {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [AddCommGroup F] [Module 𝕜 F] [c : InnerProductSpace.Core 𝕜 F] (x : F) (y : F) {r : 𝕜} : ⟪x, r • y⟫_𝕜 = r * ⟪x, y⟫_𝕜

theorem InnerProductSpace.Core.inner_zero_left {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [AddCommGroup F] [Module 𝕜 F] [c : InnerProductSpace.Core 𝕜 F] (x : F) : ⟪0, x⟫_𝕜 = 0

theorem InnerProductSpace.Core.inner_zero_right {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [AddCommGroup F] [Module 𝕜 F] [c : InnerProductSpace.Core 𝕜 F] (x : F) : ⟪x, 0⟫_𝕜 = 0

theorem InnerProductSpace.Core.inner_self_eq_zero {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [AddCommGroup F] [Module 𝕜 F] [c : InnerProductSpace.Core 𝕜 F] {x : F} : ⟪x, x⟫_𝕜 = 0 ↔ x = 0

theorem InnerProductSpace.Core.normSq_eq_zero {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [AddCommGroup F] [Module 𝕜 F] [c : InnerProductSpace.Core 𝕜 F] {x : F} : InnerProductSpace.Core.normSq x = 0 ↔ x = 0

theorem InnerProductSpace.Core.inner_self_ne_zero {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [AddCommGroup F] [Module 𝕜 F] [c : InnerProductSpace.Core 𝕜 F] {x : F} : ⟪x, x⟫_𝕜 ≠ 0 ↔ x ≠ 0

theorem InnerProductSpace.Core.inner_self_ofReal_re {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [AddCommGroup F] [Module 𝕜 F] [c : InnerProductSpace.Core 𝕜 F] (x : F) : ↑(RCLike.re ⟪x, x⟫_𝕜) = ⟪x, x⟫_𝕜

theorem InnerProductSpace.Core.norm_inner_symm {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [AddCommGroup F] [Module 𝕜 F] [c : InnerProductSpace.Core 𝕜 F] (x : F) (y : F) : ‖⟪x, y⟫_𝕜‖ = ‖⟪y, x⟫_𝕜‖

theorem InnerProductSpace.Core.inner_neg_left {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [AddCommGroup F] [Module 𝕜 F] [c : InnerProductSpace.Core 𝕜 F] (x : F) (y : F) : ⟪-x, y⟫_𝕜 = -⟪x, y⟫_𝕜

theorem InnerProductSpace.Core.inner_neg_right {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [AddCommGroup F] [Module 𝕜 F] [c : InnerProductSpace.Core 𝕜 F] (x : F) (y : F) : ⟪x, -y⟫_𝕜 = -⟪x, y⟫_𝕜

theorem InnerProductSpace.Core.inner_sub_left {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [AddCommGroup F] [Module 𝕜 F] [c : InnerProductSpace.Core 𝕜 F] (x : F) (y : F) (z : F) : ⟪x - y, z⟫_𝕜 = ⟪x, z⟫_𝕜 - ⟪y, z⟫_𝕜

theorem InnerProductSpace.Core.inner_sub_right {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [AddCommGroup F] [Module 𝕜 F] [c : InnerProductSpace.Core 𝕜 F] (x : F) (y : F) (z : F) : ⟪x, y - z⟫_𝕜 = ⟪x, y⟫_𝕜 - ⟪x, z⟫_𝕜

theorem InnerProductSpace.Core.inner_mul_symm_re_eq_norm {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [AddCommGroup F] [Module 𝕜 F] [c : InnerProductSpace.Core 𝕜 F] (x : F) (y : F) : RCLike.re (⟪x, y⟫_𝕜 * ⟪y, x⟫_𝕜) = ‖⟪x, y⟫_𝕜 * ⟪y, x⟫_𝕜‖

theorem InnerProductSpace.Core.inner_add_add_self {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [AddCommGroup F] [Module 𝕜 F] [c : InnerProductSpace.Core 𝕜 F] (x : F) (y : F) : ⟪x + y, x + y⟫_𝕜 = ⟪x, x⟫_𝕜 + ⟪x, y⟫_𝕜 + ⟪y, x⟫_𝕜 + ⟪y, y⟫_𝕜

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

theorem InnerProductSpace.Core.inner_sub_sub_self {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [AddCommGroup F] [Module 𝕜 F] [c : InnerProductSpace.Core 𝕜 F] (x : F) (y : F) : ⟪x - y, x - y⟫_𝕜 = ⟪x, x⟫_𝕜 - ⟪x, y⟫_𝕜 - ⟪y, x⟫_𝕜 + ⟪y, y⟫_𝕜

theorem InnerProductSpace.Core.cauchy_schwarz_aux {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [AddCommGroup F] [Module 𝕜 F] [c : InnerProductSpace.Core 𝕜 F] (x : F) (y : F) : InnerProductSpace.Core.normSq (⟪x, y⟫_𝕜 • x - ⟪x, x⟫_𝕜 • y) = InnerProductSpace.Core.normSq x * (InnerProductSpace.Core.normSq x * InnerProductSpace.Core.normSq y - ‖⟪x, y⟫_𝕜‖ ^ 2)

An auxiliary equality useful to prove the Cauchy–Schwarz inequality: the square of the norm of ⟪x, y⟫ • x - ⟪x, x⟫ • y is equal to ‖x‖ ^ 2 * (‖x‖ ^ 2 * ‖y‖ ^ 2 - ‖⟪x, y⟫‖ ^ 2). We use InnerProductSpace.ofCore.normSq x etc (defeq to is_R_or_C.re ⟪x, x⟫) instead of ‖x‖ ^ 2 etc to avoid extra rewrites when applying it to an InnerProductSpace.

theorem InnerProductSpace.Core.inner_mul_inner_self_le {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [AddCommGroup F] [Module 𝕜 F] [c : InnerProductSpace.Core 𝕜 F] (x : F) (y : F) : ‖⟪x, y⟫_𝕜‖ * ‖⟪y, x⟫_𝕜‖ ≤ RCLike.re ⟪x, x⟫_𝕜 * RCLike.re ⟪y, y⟫_𝕜

Cauchy–Schwarz inequality. We need this for the Core structure to prove the triangle inequality below when showing the core is a normed group.

def InnerProductSpace.Core.toNorm {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [AddCommGroup F] [Module 𝕜 F] [c : InnerProductSpace.Core 𝕜 F] : Norm F

Norm constructed from an InnerProductSpace.Core structure, defined to be the square root of the scalar product.

Equations

• InnerProductSpace.Core.toNorm = { norm := fun (x : F) => √(RCLike.re ⟪x, x⟫_𝕜) }

theorem InnerProductSpace.Core.norm_eq_sqrt_inner {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [AddCommGroup F] [Module 𝕜 F] [c : InnerProductSpace.Core 𝕜 F] (x : F) : ‖x‖ = √(RCLike.re ⟪x, x⟫_𝕜)

theorem InnerProductSpace.Core.inner_self_eq_norm_mul_norm {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [AddCommGroup F] [Module 𝕜 F] [c : InnerProductSpace.Core 𝕜 F] (x : F) : RCLike.re ⟪x, x⟫_𝕜 = ‖x‖ * ‖x‖

theorem InnerProductSpace.Core.sqrt_normSq_eq_norm {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [AddCommGroup F] [Module 𝕜 F] [c : InnerProductSpace.Core 𝕜 F] (x : F) : √(InnerProductSpace.Core.normSq x) = ‖x‖

theorem InnerProductSpace.Core.norm_inner_le_norm {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [AddCommGroup F] [Module 𝕜 F] [c : InnerProductSpace.Core 𝕜 F] (x : F) (y : F) : ‖⟪x, y⟫_𝕜‖ ≤ ‖x‖ * ‖y‖

Cauchy–Schwarz inequality with norm

def InnerProductSpace.Core.toNormedAddCommGroup {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [AddCommGroup F] [Module 𝕜 F] [c : InnerProductSpace.Core 𝕜 F] : NormedAddCommGroup F

Normed group structure constructed from an InnerProductSpace.Core structure

Equations

• InnerProductSpace.Core.toNormedAddCommGroup = { toFun := fun (x : F) => √(RCLike.re ⟪x, x⟫_𝕜), map_zero' := ⋯, add_le' := ⋯, neg' := ⋯, eq_zero_of_map_eq_zero' := ⋯ }.toNormedAddCommGroup

def InnerProductSpace.Core.toNormedSpace {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [AddCommGroup F] [Module 𝕜 F] [c : InnerProductSpace.Core 𝕜 F] : NormedSpace 𝕜 F

Normed space structure constructed from an InnerProductSpace.Core structure

Equations

• InnerProductSpace.Core.toNormedSpace = NormedSpace.mk ⋯

def InnerProductSpace.ofCore {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [AddCommGroup F] [Module 𝕜 F] (c : InnerProductSpace.Core 𝕜 F) : InnerProductSpace 𝕜 F

Given an InnerProductSpace.Core structure on a space, one can use it to turn the space into an inner product space. The NormedAddCommGroup structure is expected to already be defined with InnerProductSpace.ofCore.toNormedAddCommGroup.

Equations

• InnerProductSpace.ofCore c = InnerProductSpace.mk ⋯ ⋯ ⋯ ⋯

Properties of inner product spaces

@[simp]

theorem inner_conj_symm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) (y : E) : (starRingEnd 𝕜) ⟪y, x⟫_𝕜 = ⟪x, y⟫_𝕜

theorem real_inner_comm {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (x : F) (y : F) : ⟪y, x⟫_ℝ = ⟪x, y⟫_ℝ

theorem inner_eq_zero_symm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {x : E} {y : E} : ⟪x, y⟫_𝕜 = 0 ↔ ⟪y, x⟫_𝕜 = 0

@[simp]

theorem inner_self_im {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) : RCLike.im ⟪x, x⟫_𝕜 = 0

theorem inner_add_left {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) (y : E) (z : E) : ⟪x + y, z⟫_𝕜 = ⟪x, z⟫_𝕜 + ⟪y, z⟫_𝕜

theorem inner_add_right {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) (y : E) (z : E) : ⟪x, y + z⟫_𝕜 = ⟪x, y⟫_𝕜 + ⟪x, z⟫_𝕜

theorem inner_re_symm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) (y : E) : RCLike.re ⟪x, y⟫_𝕜 = RCLike.re ⟪y, x⟫_𝕜

theorem inner_im_symm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) (y : E) : RCLike.im ⟪x, y⟫_𝕜 = -RCLike.im ⟪y, x⟫_𝕜

theorem inner_smul_left {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) (y : E) (r : 𝕜) : ⟪r • x, y⟫_𝕜 = (starRingEnd 𝕜) r * ⟪x, y⟫_𝕜

theorem real_inner_smul_left {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (x : F) (y : F) (r : ℝ) : ⟪r • x, y⟫_ℝ = r * ⟪x, y⟫_ℝ

theorem inner_smul_real_left {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) (y : E) (r : ℝ) : ⟪↑r • x, y⟫_𝕜 = r • ⟪x, y⟫_𝕜

theorem inner_smul_right {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) (y : E) (r : 𝕜) : ⟪x, r • y⟫_𝕜 = r * ⟪x, y⟫_𝕜

theorem real_inner_smul_right {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (x : F) (y : F) (r : ℝ) : ⟪x, r • y⟫_ℝ = r * ⟪x, y⟫_ℝ

theorem inner_smul_real_right {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) (y : E) (r : ℝ) : ⟪x, ↑r • y⟫_𝕜 = r • ⟪x, y⟫_𝕜

@[simp]

theorem sesqFormOfInner_apply_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (m : E) (y : E) : (sesqFormOfInner m) y = ⟪y, m⟫_𝕜

def sesqFormOfInner {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] : E →ₗ[𝕜] E →ₗ⋆[𝕜] 𝕜

The inner product as a sesquilinear form.

Note that in the case 𝕜 = ℝ this is a bilinear form.

Equations

• sesqFormOfInner = LinearMap.mk₂'ₛₗ (RingHom.id 𝕜) (starRingEnd 𝕜) (fun (x y : E) => ⟪y, x⟫_𝕜) ⋯ ⋯ ⋯ ⋯

@[simp]

theorem bilinFormOfRealInner_apply_apply {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (m : F) (m : F) : (bilinFormOfRealInner m✝) m = ⟪m✝, m⟫_ℝ

def bilinFormOfRealInner {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] : LinearMap.BilinForm ℝ F

The real inner product as a bilinear form.

Note that unlike sesqFormOfInner, this does not reverse the order of the arguments.

Equations

• bilinFormOfRealInner = sesqFormOfInner.flip

theorem sum_inner {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} (s : Finset ι) (f : ι → E) (x : E) : ⟪∑ i ∈ s, f i, x⟫_𝕜 = ∑ i ∈ s, ⟪f i, x⟫_𝕜

An inner product with a sum on the left.

theorem inner_sum {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} (s : Finset ι) (f : ι → E) (x : E) : ⟪x, ∑ i ∈ s, f i⟫_𝕜 = ∑ i ∈ s, ⟪x, f i⟫_𝕜

An inner product with a sum on the right.

theorem Finsupp.sum_inner {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} (l : ι →₀ 𝕜) (v : ι → E) (x : E) : ⟪l.sum fun (i : ι) (a : 𝕜) => a • v i, x⟫_𝕜 = l.sum fun (i : ι) (a : 𝕜) => (starRingEnd 𝕜) a • ⟪v i, x⟫_𝕜

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

theorem Finsupp.inner_sum {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} (l : ι →₀ 𝕜) (v : ι → E) (x : E) : ⟪x, l.sum fun (i : ι) (a : 𝕜) => a • v i⟫_𝕜 = l.sum fun (i : ι) (a : 𝕜) => a • ⟪x, v i⟫_𝕜

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

theorem DFinsupp.sum_inner {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} [DecidableEq ι] {α : ι → Type u_5} [(i : ι) → AddZeroClass (α i)] [(i : ι) → (x : α i) → Decidable (x ≠ 0)] (f : (i : ι) → α i → E) (l : Π₀ (i : ι), α i) (x : E) : ⟪l.sum f, x⟫_𝕜 = l.sum fun (i : ι) (a : α i) => ⟪f i a, x⟫_𝕜

theorem DFinsupp.inner_sum {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} [DecidableEq ι] {α : ι → Type u_5} [(i : ι) → AddZeroClass (α i)] [(i : ι) → (x : α i) → Decidable (x ≠ 0)] (f : (i : ι) → α i → E) (l : Π₀ (i : ι), α i) (x : E) : ⟪x, l.sum f⟫_𝕜 = l.sum fun (i : ι) (a : α i) => ⟪x, f i a⟫_𝕜

@[simp]

theorem inner_zero_left {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) : ⟪0, x⟫_𝕜 = 0

theorem inner_re_zero_left {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) : RCLike.re ⟪0, x⟫_𝕜 = 0

@[simp]

theorem inner_zero_right {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) : ⟪x, 0⟫_𝕜 = 0

theorem inner_re_zero_right {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) : RCLike.re ⟪x, 0⟫_𝕜 = 0

theorem inner_self_nonneg {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {x : E} : 0 ≤ RCLike.re ⟪x, x⟫_𝕜

theorem real_inner_self_nonneg {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {x : F} : 0 ≤ ⟪x, x⟫_ℝ

@[simp]

theorem inner_self_ofReal_re {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) : ↑(RCLike.re ⟪x, x⟫_𝕜) = ⟪x, x⟫_𝕜

theorem inner_self_eq_norm_sq_to_K {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) : ⟪x, x⟫_𝕜 = ↑‖x‖ ^ 2

theorem inner_self_re_eq_norm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) : RCLike.re ⟪x, x⟫_𝕜 = ‖⟪x, x⟫_𝕜‖

theorem inner_self_ofReal_norm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) : ↑‖⟪x, x⟫_𝕜‖ = ⟪x, x⟫_𝕜

theorem real_inner_self_abs {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (x : F) : |⟪x, x⟫_ℝ| = ⟪x, x⟫_ℝ

@[simp]

theorem inner_self_eq_zero {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {x : E} : ⟪x, x⟫_𝕜 = 0 ↔ x = 0

theorem inner_self_ne_zero {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {x : E} : ⟪x, x⟫_𝕜 ≠ 0 ↔ x ≠ 0

@[simp]

theorem inner_self_nonpos {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {x : E} : RCLike.re ⟪x, x⟫_𝕜 ≤ 0 ↔ x = 0

theorem real_inner_self_nonpos {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {x : F} : ⟪x, x⟫_ℝ ≤ 0 ↔ x = 0

theorem norm_inner_symm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) (y : E) : ‖⟪x, y⟫_𝕜‖ = ‖⟪y, x⟫_𝕜‖

@[simp]

theorem inner_neg_left {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) (y : E) : ⟪-x, y⟫_𝕜 = -⟪x, y⟫_𝕜

@[simp]

theorem inner_neg_right {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) (y : E) : ⟪x, -y⟫_𝕜 = -⟪x, y⟫_𝕜

theorem inner_neg_neg {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) (y : E) : ⟪-x, -y⟫_𝕜 = ⟪x, y⟫_𝕜

theorem inner_self_conj {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) : (starRingEnd 𝕜) ⟪x, x⟫_𝕜 = ⟪x, x⟫_𝕜

theorem inner_sub_left {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) (y : E) (z : E) : ⟪x - y, z⟫_𝕜 = ⟪x, z⟫_𝕜 - ⟪y, z⟫_𝕜

theorem inner_sub_right {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) (y : E) (z : E) : ⟪x, y - z⟫_𝕜 = ⟪x, y⟫_𝕜 - ⟪x, z⟫_𝕜

theorem inner_mul_symm_re_eq_norm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) (y : E) : RCLike.re (⟪x, y⟫_𝕜 * ⟪y, x⟫_𝕜) = ‖⟪x, y⟫_𝕜 * ⟪y, x⟫_𝕜‖

theorem inner_add_add_self {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) (y : E) : ⟪x + y, x + y⟫_𝕜 = ⟪x, x⟫_𝕜 + ⟪x, y⟫_𝕜 + ⟪y, x⟫_𝕜 + ⟪y, y⟫_𝕜

Expand ⟪x + y, x + y⟫

theorem real_inner_add_add_self {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (x : F) (y : F) : ⟪x + y, x + y⟫_ℝ = ⟪x, x⟫_ℝ + 2 * ⟪x, y⟫_ℝ + ⟪y, y⟫_ℝ

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

theorem inner_sub_sub_self {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) (y : E) : ⟪x - y, x - y⟫_𝕜 = ⟪x, x⟫_𝕜 - ⟪x, y⟫_𝕜 - ⟪y, x⟫_𝕜 + ⟪y, y⟫_𝕜

theorem real_inner_sub_sub_self {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (x : F) (y : F) : ⟪x - y, x - y⟫_ℝ = ⟪x, x⟫_ℝ - 2 * ⟪x, y⟫_ℝ + ⟪y, y⟫_ℝ

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

theorem ext_inner_left (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {x : E} {y : E} (h : ∀ (v : E), ⟪v, x⟫_𝕜 = ⟪v, y⟫_𝕜) : x = y

theorem ext_inner_right (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {x : E} {y : E} (h : ∀ (v : E), ⟪x, v⟫_𝕜 = ⟪y, v⟫_𝕜) : x = y

theorem parallelogram_law {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {x : E} {y : E} : ⟪x + y, x + y⟫_𝕜 + ⟪x - y, x - y⟫_𝕜 = 2 * (⟪x, x⟫_𝕜 + ⟪y, y⟫_𝕜)

Parallelogram law

theorem inner_mul_inner_self_le {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) (y : E) : ‖⟪x, y⟫_𝕜‖ * ‖⟪y, x⟫_𝕜‖ ≤ RCLike.re ⟪x, x⟫_𝕜 * RCLike.re ⟪y, y⟫_𝕜

Cauchy–Schwarz inequality.

theorem real_inner_mul_inner_self_le {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (x : F) (y : F) : ⟪x, y⟫_ℝ * ⟪x, y⟫_ℝ ≤ ⟪x, x⟫_ℝ * ⟪y, y⟫_ℝ

Cauchy–Schwarz inequality for real inner products.

theorem linearIndependent_of_ne_zero_of_inner_eq_zero {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {v : ι → E} (hz : ∀ (i : ι), v i ≠ 0) (ho : Pairwise fun (i j : ι) => ⟪v i, v j⟫_𝕜 = 0) : LinearIndependent 𝕜 v

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

def Orthonormal (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} (v : ι → E) : Prop

An orthonormal set of vectors in an InnerProductSpace

Equations

• Orthonormal 𝕜 v = ((∀ (i : ι), ‖v i‖ = 1) ∧ Pairwise fun (i j : ι) => ⟪v i, v j⟫_𝕜 = 0)

theorem orthonormal_iff_ite {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} [DecidableEq ι] {v : ι → E} : Orthonormal 𝕜 v ↔ ∀ (i j : ι), ⟪v i, v j⟫_𝕜 = if i = j then 1 else 0

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

theorem orthonormal_subtype_iff_ite {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [DecidableEq E] {s : Set E} : Orthonormal 𝕜 Subtype.val ↔ ∀ v ∈ s, ∀ w ∈ s, ⟪v, w⟫_𝕜 = if v = w then 1 else 0

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

theorem Orthonormal.inner_right_finsupp {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {v : ι → E} (hv : Orthonormal 𝕜 v) (l : ι →₀ 𝕜) (i : ι) : ⟪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.

theorem Orthonormal.inner_right_sum {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {v : ι → E} (hv : Orthonormal 𝕜 v) (l : ι → 𝕜) {s : Finset ι} {i : ι} (hi : i ∈ s) : ⟪v i, ∑ i ∈ s, 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.

theorem Orthonormal.inner_right_fintype {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} [Fintype ι] {v : ι → E} (hv : Orthonormal 𝕜 v) (l : ι → 𝕜) (i : ι) : ⟪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.

theorem Orthonormal.inner_left_finsupp {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {v : ι → E} (hv : Orthonormal 𝕜 v) (l : ι →₀ 𝕜) (i : ι) : ⟪(Finsupp.total ι E 𝕜 v) l, v i⟫_𝕜 = (starRingEnd 𝕜) (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.

theorem Orthonormal.inner_left_sum {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {v : ι → E} (hv : Orthonormal 𝕜 v) (l : ι → 𝕜) {s : Finset ι} {i : ι} (hi : i ∈ s) : ⟪∑ i ∈ s, l i • v i, v i⟫_𝕜 = (starRingEnd 𝕜) (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.

theorem Orthonormal.inner_left_fintype {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} [Fintype ι] {v : ι → E} (hv : Orthonormal 𝕜 v) (l : ι → 𝕜) (i : ι) : ⟪∑ i : ι, l i • v i, v i⟫_𝕜 = (starRingEnd 𝕜) (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.

theorem Orthonormal.inner_finsupp_eq_sum_left {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {v : ι → E} (hv : Orthonormal 𝕜 v) (l₁ : ι →₀ 𝕜) (l₂ : ι →₀ 𝕜) : ⟪(Finsupp.total ι E 𝕜 v) l₁, (Finsupp.total ι E 𝕜 v) l₂⟫_𝕜 = l₁.sum fun (i : ι) (y : 𝕜) => (starRingEnd 𝕜) y * l₂ i

The inner product of two linear combinations of a set of orthonormal vectors, expressed as a sum over the first Finsupp.

theorem Orthonormal.inner_finsupp_eq_sum_right {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {v : ι → E} (hv : Orthonormal 𝕜 v) (l₁ : ι →₀ 𝕜) (l₂ : ι →₀ 𝕜) : ⟪(Finsupp.total ι E 𝕜 v) l₁, (Finsupp.total ι E 𝕜 v) l₂⟫_𝕜 = l₂.sum fun (i : ι) (y : 𝕜) => (starRingEnd 𝕜) (l₁ i) * y

The inner product of two linear combinations of a set of orthonormal vectors, expressed as a sum over the second Finsupp.

theorem Orthonormal.inner_sum {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {v : ι → E} (hv : Orthonormal 𝕜 v) (l₁ : ι → 𝕜) (l₂ : ι → 𝕜) (s : Finset ι) : ⟪∑ i ∈ s, l₁ i • v i, ∑ i ∈ s, l₂ i • v i⟫_𝕜 = ∑ i ∈ s, (starRingEnd 𝕜) (l₁ i) * l₂ i

The inner product of two linear combinations of a set of orthonormal vectors, expressed as a sum.

theorem Orthonormal.inner_left_right_finset {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {s : Finset ι} {v : ι → E} (hv : Orthonormal 𝕜 v) {a : ι → ι → 𝕜} : ∑ i ∈ s, ∑ j ∈ s, a i j • ⟪v j, v i⟫_𝕜 = ∑ k ∈ s, a k k

The double sum of weighted inner products of pairs of vectors from an orthonormal sequence is the sum of the weights.

theorem Orthonormal.linearIndependent {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {v : ι → E} (hv : Orthonormal 𝕜 v) : LinearIndependent 𝕜 v

An orthonormal set is linearly independent.

theorem Orthonormal.comp {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {ι' : Type u_5} {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.

theorem orthonormal_subtype_range {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {v : ι → E} (hv : Function.Injective v) : Orthonormal 𝕜 Subtype.val ↔ Orthonormal 𝕜 v

An injective family v : ι → E is orthonormal if and only if Subtype.val : (range v) → E is orthonormal.

theorem Orthonormal.toSubtypeRange {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {v : ι → E} (hv : Orthonormal 𝕜 v) : Orthonormal 𝕜 Subtype.val

If v : ι → E is an orthonormal family, then Subtype.val : (range v) → E is an orthonormal family.

theorem Orthonormal.inner_finsupp_eq_zero {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {v : ι → E} (hv : Orthonormal 𝕜 v) {s : Set ι} {i : ι} (hi : i ∉ s) {l : ι →₀ 𝕜} (hl : l ∈ Finsupp.supported 𝕜 𝕜 s) : ⟪(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.

theorem Orthonormal.orthonormal_of_forall_eq_or_eq_neg {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {v : ι → E} {w : ι → E} (hv : Orthonormal 𝕜 v) (hw : ∀ (i : ι), w i = v i ∨ w i = -v i) : Orthonormal 𝕜 w

Given an orthonormal family, a second family of vectors is orthonormal if every vector equals the corresponding vector in the original family or its negation.

theorem orthonormal_empty (𝕜 : Type u_1) (E : Type u_2) [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] : Orthonormal 𝕜 fun (x : ↑∅) => ↑x

theorem orthonormal_iUnion_of_directed {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {η : Type u_5} {s : η → Set E} (hs : Directed (fun (x x_1 : Set E) => x ⊆ x_1) s) (h : ∀ (i : η), Orthonormal 𝕜 fun (x : ↑(s i)) => ↑x) : Orthonormal 𝕜 fun (x : ↑(⋃ (i : η), s i)) => ↑x

theorem orthonormal_sUnion_of_directed {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {s : Set (Set E)} (hs : DirectedOn (fun (x x_1 : Set E) => x ⊆ x_1) s) (h : ∀ a ∈ s, Orthonormal 𝕜 fun (x : ↑a) => ↑x) : Orthonormal 𝕜 fun (x : ↑(⋃₀ s)) => ↑x

theorem exists_maximal_orthonormal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {s : Set E} (hs : Orthonormal 𝕜 Subtype.val) : ∃ w ⊇ s, Orthonormal 𝕜 Subtype.val ∧ ∀ u ⊇ w, Orthonormal 𝕜 Subtype.val → u = w

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

theorem Orthonormal.ne_zero {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {v : ι → E} (hv : Orthonormal 𝕜 v) (i : ι) : v i ≠ 0

def basisOfOrthonormalOfCardEqFinrank {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} [Fintype ι] [Nonempty ι] {v : ι → E} (hv : Orthonormal 𝕜 v) (card_eq : Fintype.card ι = FiniteDimensional.finrank 𝕜 E) : Basis ι 𝕜 E

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

Equations

• basisOfOrthonormalOfCardEqFinrank hv card_eq = basisOfLinearIndependentOfCardEqFinrank ⋯ card_eq

@[simp]

theorem coe_basisOfOrthonormalOfCardEqFinrank {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} [Fintype ι] [Nonempty ι] {v : ι → E} (hv : Orthonormal 𝕜 v) (card_eq : Fintype.card ι = FiniteDimensional.finrank 𝕜 E) : ⇑(basisOfOrthonormalOfCardEqFinrank hv card_eq) = v

theorem norm_eq_sqrt_inner {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) : ‖x‖ = √(RCLike.re ⟪x, x⟫_𝕜)

theorem norm_eq_sqrt_real_inner {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (x : F) : ‖x‖ = √⟪x, x⟫_ℝ

theorem inner_self_eq_norm_mul_norm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) : RCLike.re ⟪x, x⟫_𝕜 = ‖x‖ * ‖x‖

theorem inner_self_eq_norm_sq {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) : RCLike.re ⟪x, x⟫_𝕜 = ‖x‖ ^ 2

theorem real_inner_self_eq_norm_mul_norm {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (x : F) : ⟪x, x⟫_ℝ = ‖x‖ * ‖x‖

theorem real_inner_self_eq_norm_sq {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (x : F) : ⟪x, x⟫_ℝ = ‖x‖ ^ 2

theorem norm_add_sq {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) (y : E) : ‖x + y‖ ^ 2 = ‖x‖ ^ 2 + 2 * RCLike.re ⟪x, y⟫_𝕜 + ‖y‖ ^ 2

Expand the square

theorem norm_add_pow_two {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) (y : E) : ‖x + y‖ ^ 2 = ‖x‖ ^ 2 + 2 * RCLike.re ⟪x, y⟫_𝕜 + ‖y‖ ^ 2

Alias of norm_add_sq.

---

Expand the square

theorem norm_add_sq_real {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (x : F) (y : F) : ‖x + y‖ ^ 2 = ‖x‖ ^ 2 + 2 * ⟪x, y⟫_ℝ + ‖y‖ ^ 2

Expand the square

theorem norm_add_pow_two_real {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (x : F) (y : F) : ‖x + y‖ ^ 2 = ‖x‖ ^ 2 + 2 * ⟪x, y⟫_ℝ + ‖y‖ ^ 2

Alias of norm_add_sq_real.

---

Expand the square

theorem norm_add_mul_self {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) (y : E) : ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + 2 * RCLike.re ⟪x, y⟫_𝕜 + ‖y‖ * ‖y‖

Expand the square

theorem norm_add_mul_self_real {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (x : F) (y : F) : ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + 2 * ⟪x, y⟫_ℝ + ‖y‖ * ‖y‖

Expand the square

theorem norm_sub_sq {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) (y : E) : ‖x - y‖ ^ 2 = ‖x‖ ^ 2 - 2 * RCLike.re ⟪x, y⟫_𝕜 + ‖y‖ ^ 2

Expand the square

theorem norm_sub_pow_two {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) (y : E) : ‖x - y‖ ^ 2 = ‖x‖ ^ 2 - 2 * RCLike.re ⟪x, y⟫_𝕜 + ‖y‖ ^ 2

Alias of norm_sub_sq.

---

Expand the square

theorem norm_sub_sq_real {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (x : F) (y : F) : ‖x - y‖ ^ 2 = ‖x‖ ^ 2 - 2 * ⟪x, y⟫_ℝ + ‖y‖ ^ 2

Expand the square

theorem norm_sub_pow_two_real {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (x : F) (y : F) : ‖x - y‖ ^ 2 = ‖x‖ ^ 2 - 2 * ⟪x, y⟫_ℝ + ‖y‖ ^ 2

Alias of norm_sub_sq_real.

---

Expand the square

theorem norm_sub_mul_self {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) (y : E) : ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ - 2 * RCLike.re ⟪x, y⟫_𝕜 + ‖y‖ * ‖y‖

Expand the square

theorem norm_sub_mul_self_real {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (x : F) (y : F) : ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ - 2 * ⟪x, y⟫_ℝ + ‖y‖ * ‖y‖

Expand the square

theorem norm_inner_le_norm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) (y : E) : ‖⟪x, y⟫_𝕜‖ ≤ ‖x‖ * ‖y‖

Cauchy–Schwarz inequality with norm

theorem nnnorm_inner_le_nnnorm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) (y : E) : ‖⟪x, y⟫_𝕜‖₊ ≤ ‖x‖₊ * ‖y‖₊

theorem re_inner_le_norm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) (y : E) : RCLike.re ⟪x, y⟫_𝕜 ≤ ‖x‖ * ‖y‖

theorem abs_real_inner_le_norm {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (x : F) (y : F) : |⟪x, y⟫_ℝ| ≤ ‖x‖ * ‖y‖

Cauchy–Schwarz inequality with norm

theorem real_inner_le_norm {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (x : F) (y : F) : ⟪x, y⟫_ℝ ≤ ‖x‖ * ‖y‖

Cauchy–Schwarz inequality with norm

theorem parallelogram_law_with_norm (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) (y : E) : ‖x + y‖ * ‖x + y‖ + ‖x - y‖ * ‖x - y‖ = 2 * (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)

theorem parallelogram_law_with_nnnorm (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) (y : E) : ‖x + y‖₊ * ‖x + y‖₊ + ‖x - y‖₊ * ‖x - y‖₊ = 2 * (‖x‖₊ * ‖x‖₊ + ‖y‖₊ * ‖y‖₊)

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} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) (y : E) : RCLike.re ⟪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.

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} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) (y : E) : RCLike.re ⟪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.

theorem re_inner_eq_norm_add_mul_self_sub_norm_sub_mul_self_div_four {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) (y : E) : RCLike.re ⟪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.

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} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) (y : E) : RCLike.im ⟪x, y⟫_𝕜 = (‖x - RCLike.I • y‖ * ‖x - RCLike.I • y‖ - ‖x + RCLike.I • y‖ * ‖x + RCLike.I • y‖) / 4

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

theorem inner_eq_sum_norm_sq_div_four {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) (y : E) : ⟪x, y⟫_𝕜 = (↑‖x + y‖ ^ 2 - ↑‖x - y‖ ^ 2 + (↑‖x - RCLike.I • y‖ ^ 2 - ↑‖x + RCLike.I • y‖ ^ 2) * RCLike.I) / 4

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

theorem dist_div_norm_sq_smul {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {x : F} {y : F} (hx : x ≠ 0) (hy : y ≠ 0) (R : ℝ) : dist ((R / ‖x‖) ^ 2 • x) ((R / ‖y‖) ^ 2 • y) = R ^ 2 / (‖x‖ * ‖y‖) * dist x y

Formula for the distance between the images of two nonzero points under an inversion with center zero. See also EuclideanGeometry.dist_inversion_inversion for inversions around a general point.

@[instance 100]

instance InnerProductSpace.toUniformConvexSpace {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] : UniformConvexSpace F

Equations

• ⋯ = ⋯

theorem inner_map_polarization {V : Type u_4} [NormedAddCommGroup V] [InnerProductSpace ℂ V] (T : V →ₗ[ℂ] V) (x : V) (y : V) : ⟪T y, x⟫_ℂ = (⟪T (x + y), x + y⟫_ℂ - ⟪T (x - y), x - y⟫_ℂ + Complex.I * ⟪T (x + Complex.I • y), x + Complex.I • y⟫_ℂ - Complex.I * ⟪T (x - Complex.I • y), x - Complex.I • y⟫_ℂ) / 4

A complex polarization identity, with a linear map

theorem inner_map_polarization' {V : Type u_4} [NormedAddCommGroup V] [InnerProductSpace ℂ V] (T : V →ₗ[ℂ] V) (x : V) (y : V) : ⟪T x, y⟫_ℂ = (⟪T (x + y), x + y⟫_ℂ - ⟪T (x - y), x - y⟫_ℂ - Complex.I * ⟪T (x + Complex.I • y), x + Complex.I • y⟫_ℂ + Complex.I * ⟪T (x - Complex.I • y), x - Complex.I • y⟫_ℂ) / 4

theorem inner_map_self_eq_zero {V : Type u_4} [NormedAddCommGroup V] [InnerProductSpace ℂ V] (T : V →ₗ[ℂ] V) : (∀ (x : V), ⟪T x, x⟫_ℂ = 0) ↔ T = 0

A linear map T is zero, if and only if the identity ⟪T x, x⟫_ℂ = 0 holds for all x.

theorem ext_inner_map {V : Type u_4} [NormedAddCommGroup V] [InnerProductSpace ℂ V] (S : V →ₗ[ℂ] V) (T : V →ₗ[ℂ] V) : (∀ (x : V), ⟪S x, x⟫_ℂ = ⟪T x, x⟫_ℂ) ↔ S = T

Two linear maps S and T are equal, if and only if the identity ⟪S x, x⟫_ℂ = ⟪T x, x⟫_ℂ holds for all x.

@[simp]

theorem LinearIsometry.inner_map_map {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {E' : Type u_7} [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] (f : E →ₗᵢ[𝕜] E') (x : E) (y : E) : ⟪f x, f y⟫_𝕜 = ⟪x, y⟫_𝕜

A linear isometry preserves the inner product.

@[simp]

theorem LinearIsometryEquiv.inner_map_map {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {E' : Type u_7} [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] (f : E ≃ₗᵢ[𝕜] E') (x : E) (y : E) : ⟪f x, f y⟫_𝕜 = ⟪x, y⟫_𝕜

A linear isometric equivalence preserves the inner product.

theorem LinearIsometryEquiv.inner_map_eq_flip {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {E' : Type u_7} [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] (f : E ≃ₗᵢ[𝕜] E') (x : E) (y : E') : ⟪f x, y⟫_𝕜 = ⟪x, f.symm y⟫_𝕜

The adjoint of a linear isometric equivalence is its inverse.

def LinearMap.isometryOfInner {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {E' : Type u_7} [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] (f : E →ₗ[𝕜] E') (h : ∀ (x y : E), ⟪f x, f y⟫_𝕜 = ⟪x, y⟫_𝕜) : E →ₗᵢ[𝕜] E'

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

Equations

• f.isometryOfInner h = { toLinearMap := f, norm_map' := ⋯ }

@[simp]

theorem LinearMap.coe_isometryOfInner {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {E' : Type u_7} [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] (f : E →ₗ[𝕜] E') (h : ∀ (x y : E), ⟪f x, f y⟫_𝕜 = ⟪x, y⟫_𝕜) : ⇑(f.isometryOfInner h) = ⇑f

@[simp]

theorem LinearMap.isometryOfInner_toLinearMap {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {E' : Type u_7} [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] (f : E →ₗ[𝕜] E') (h : ∀ (x y : E), ⟪f x, f y⟫_𝕜 = ⟪x, y⟫_𝕜) : (f.isometryOfInner h).toLinearMap = f

def LinearEquiv.isometryOfInner {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {E' : Type u_7} [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] (f : E ≃ₗ[𝕜] E') (h : ∀ (x y : E), ⟪f x, f y⟫_𝕜 = ⟪x, y⟫_𝕜) : E ≃ₗᵢ[𝕜] E'

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

Equations

• f.isometryOfInner h = { toLinearEquiv := f, norm_map' := ⋯ }

@[simp]

theorem LinearEquiv.coe_isometryOfInner {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {E' : Type u_7} [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] (f : E ≃ₗ[𝕜] E') (h : ∀ (x y : E), ⟪f x, f y⟫_𝕜 = ⟪x, y⟫_𝕜) : ⇑(f.isometryOfInner h) = ⇑f

@[simp]

theorem LinearEquiv.isometryOfInner_toLinearEquiv {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {E' : Type u_7} [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] (f : E ≃ₗ[𝕜] E') (h : ∀ (x y : E), ⟪f x, f y⟫_𝕜 = ⟪x, y⟫_𝕜) : (f.isometryOfInner h).toLinearEquiv = f

theorem LinearMap.norm_map_iff_inner_map_map {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {E' : Type u_7} [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] {F : Type u_9} [FunLike F E E'] [LinearMapClass F 𝕜 E E'] (f : F) : (∀ (x : E), ‖f x‖ = ‖x‖) ↔ ∀ (x y : E), ⟪f x, f y⟫_𝕜 = ⟪x, y⟫_𝕜

A linear map is an isometry if and it preserves the inner product.

theorem LinearIsometry.orthonormal_comp_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {E' : Type u_7} [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] {v : ι → E} (f : E →ₗᵢ[𝕜] E') : Orthonormal 𝕜 (⇑f ∘ v) ↔ Orthonormal 𝕜 v

A linear isometry preserves the property of being orthonormal.

theorem Orthonormal.comp_linearIsometry {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {E' : Type u_7} [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] {v : ι → E} (hv : Orthonormal 𝕜 v) (f : E →ₗᵢ[𝕜] E') : Orthonormal 𝕜 (⇑f ∘ v)

A linear isometry preserves the property of being orthonormal.

theorem Orthonormal.comp_linearIsometryEquiv {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {E' : Type u_7} [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] {v : ι → E} (hv : Orthonormal 𝕜 v) (f : E ≃ₗᵢ[𝕜] E') : Orthonormal 𝕜 (⇑f ∘ v)

A linear isometric equivalence preserves the property of being orthonormal.

theorem Orthonormal.mapLinearIsometryEquiv {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {E' : Type u_7} [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] {v : Basis ι 𝕜 E} (hv : Orthonormal 𝕜 ⇑v) (f : E ≃ₗᵢ[𝕜] E') : Orthonormal 𝕜 ⇑(v.map f.toLinearEquiv)

A linear isometric equivalence, applied with Basis.map, preserves the property of being orthonormal.

def LinearMap.isometryOfOrthonormal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {E' : Type u_7} [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] (f : E →ₗ[𝕜] E') {v : Basis ι 𝕜 E} (hv : Orthonormal 𝕜 ⇑v) (hf : Orthonormal 𝕜 (⇑f ∘ ⇑v)) : E →ₗᵢ[𝕜] E'

A linear map that sends an orthonormal basis to orthonormal vectors is a linear isometry.

Equations

• f.isometryOfOrthonormal hv hf = f.isometryOfInner ⋯

@[simp]

theorem LinearMap.coe_isometryOfOrthonormal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {E' : Type u_7} [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] (f : E →ₗ[𝕜] E') {v : Basis ι 𝕜 E} (hv : Orthonormal 𝕜 ⇑v) (hf : Orthonormal 𝕜 (⇑f ∘ ⇑v)) : ⇑(f.isometryOfOrthonormal hv hf) = ⇑f

@[simp]

theorem LinearMap.isometryOfOrthonormal_toLinearMap {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {E' : Type u_7} [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] (f : E →ₗ[𝕜] E') {v : Basis ι 𝕜 E} (hv : Orthonormal 𝕜 ⇑v) (hf : Orthonormal 𝕜 (⇑f ∘ ⇑v)) : (f.isometryOfOrthonormal hv hf).toLinearMap = f

def LinearEquiv.isometryOfOrthonormal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {E' : Type u_7} [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] (f : E ≃ₗ[𝕜] E') {v : Basis ι 𝕜 E} (hv : Orthonormal 𝕜 ⇑v) (hf : Orthonormal 𝕜 (⇑f ∘ ⇑v)) : E ≃ₗᵢ[𝕜] E'

A linear equivalence that sends an orthonormal basis to orthonormal vectors is a linear isometric equivalence.

Equations

• f.isometryOfOrthonormal hv hf = f.isometryOfInner ⋯

@[simp]

theorem LinearEquiv.coe_isometryOfOrthonormal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {E' : Type u_7} [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] (f : E ≃ₗ[𝕜] E') {v : Basis ι 𝕜 E} (hv : Orthonormal 𝕜 ⇑v) (hf : Orthonormal 𝕜 (⇑f ∘ ⇑v)) : ⇑(f.isometryOfOrthonormal hv hf) = ⇑f

@[simp]

theorem LinearEquiv.isometryOfOrthonormal_toLinearEquiv {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {E' : Type u_7} [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] (f : E ≃ₗ[𝕜] E') {v : Basis ι 𝕜 E} (hv : Orthonormal 𝕜 ⇑v) (hf : Orthonormal 𝕜 (⇑f ∘ ⇑v)) : (f.isometryOfOrthonormal hv hf).toLinearEquiv = f

def Orthonormal.equiv {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {ι' : Type u_5} {E' : Type u_7} [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] {v : Basis ι 𝕜 E} (hv : Orthonormal 𝕜 ⇑v) {v' : Basis ι' 𝕜 E'} (hv' : Orthonormal 𝕜 ⇑v') (e : ι ≃ ι') : E ≃ₗᵢ[𝕜] E'

A linear isometric equivalence that sends an orthonormal basis to a given orthonormal basis.

Equations

• hv.equiv hv' e = (v.equiv v' e).isometryOfOrthonormal hv ⋯

@[simp]

theorem Orthonormal.equiv_toLinearEquiv {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {ι' : Type u_5} {E' : Type u_7} [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] {v : Basis ι 𝕜 E} (hv : Orthonormal 𝕜 ⇑v) {v' : Basis ι' 𝕜 E'} (hv' : Orthonormal 𝕜 ⇑v') (e : ι ≃ ι') : (hv.equiv hv' e).toLinearEquiv = v.equiv v' e

@[simp]

theorem Orthonormal.equiv_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {E' : Type u_7} [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] {ι' : Type u_9} {v : Basis ι 𝕜 E} (hv : Orthonormal 𝕜 ⇑v) {v' : Basis ι' 𝕜 E'} (hv' : Orthonormal 𝕜 ⇑v') (e : ι ≃ ι') (i : ι) : (hv.equiv hv' e) (v i) = v' (e i)

@[simp]

theorem Orthonormal.equiv_refl {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {v : Basis ι 𝕜 E} (hv : Orthonormal 𝕜 ⇑v) : hv.equiv hv (Equiv.refl ι) = LinearIsometryEquiv.refl 𝕜 E

@[simp]

theorem Orthonormal.equiv_symm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {ι' : Type u_5} {E' : Type u_7} [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] {v : Basis ι 𝕜 E} (hv : Orthonormal 𝕜 ⇑v) {v' : Basis ι' 𝕜 E'} (hv' : Orthonormal 𝕜 ⇑v') (e : ι ≃ ι') : (hv.equiv hv' e).symm = hv'.equiv hv e.symm

@[simp]

theorem Orthonormal.equiv_trans {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {ι' : Type u_5} {ι'' : Type u_6} {E' : Type u_7} [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] {E'' : Type u_8} [NormedAddCommGroup E''] [InnerProductSpace 𝕜 E''] {v : Basis ι 𝕜 E} (hv : Orthonormal 𝕜 ⇑v) {v' : Basis ι' 𝕜 E'} (hv' : Orthonormal 𝕜 ⇑v') (e : ι ≃ ι') {v'' : Basis ι'' 𝕜 E''} (hv'' : Orthonormal 𝕜 ⇑v'') (e' : ι' ≃ ι'') : (hv.equiv hv' e).trans (hv'.equiv hv'' e') = hv.equiv hv'' (e.trans e')

theorem Orthonormal.map_equiv {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {ι' : Type u_5} {E' : Type u_7} [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] {v : Basis ι 𝕜 E} (hv : Orthonormal 𝕜 ⇑v) {v' : Basis ι' 𝕜 E'} (hv' : Orthonormal 𝕜 ⇑v') (e : ι ≃ ι') : v.map (hv.equiv hv' e).toLinearEquiv = v'.reindex e.symm

theorem real_inner_eq_norm_add_mul_self_sub_norm_mul_self_sub_norm_mul_self_div_two {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (x : F) (y : F) : ⟪x, y⟫_ℝ = (‖x + y‖ * ‖x + y‖ - ‖x‖ * ‖x‖ - ‖y‖ * ‖y‖) / 2

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

theorem real_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (x : F) (y : F) : ⟪x, y⟫_ℝ = (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - ‖x - y‖ * ‖x - y‖) / 2

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

theorem norm_add_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (x : F) (y : F) : ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ ↔ ⟪x, y⟫_ℝ = 0

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

theorem norm_add_eq_sqrt_iff_real_inner_eq_zero {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {x : F} {y : F} : ‖x + y‖ = √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖) ↔ ⟪x, y⟫_ℝ = 0

Pythagorean theorem, if-and-if vector inner product form using square roots.

theorem norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) (y : E) (h : ⟪x, y⟫_𝕜 = 0) : ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖

Pythagorean theorem, vector inner product form.

theorem norm_add_sq_eq_norm_sq_add_norm_sq_real {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {x : F} {y : F} (h : ⟪x, y⟫_ℝ = 0) : ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖

Pythagorean theorem, vector inner product form.

theorem norm_sub_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (x : F) (y : F) : ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ ↔ ⟪x, y⟫_ℝ = 0

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

theorem norm_sub_eq_sqrt_iff_real_inner_eq_zero {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {x : F} {y : F} : ‖x - y‖ = √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖) ↔ ⟪x, y⟫_ℝ = 0

Pythagorean theorem, subtracting vectors, if-and-if vector inner product form using square roots.

theorem norm_sub_sq_eq_norm_sq_add_norm_sq_real {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {x : F} {y : F} (h : ⟪x, y⟫_ℝ = 0) : ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖

Pythagorean theorem, subtracting vectors, vector inner product form.

theorem real_inner_add_sub_eq_zero_iff {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (x : F) (y : F) : ⟪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.

theorem norm_sub_eq_norm_add {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {v : E} {w : E} (h : ⟪v, w⟫_𝕜 = 0) : ‖w - v‖ = ‖w + v‖

Given two orthogonal vectors, their sum and difference have equal norms.

theorem abs_real_inner_div_norm_mul_norm_le_one {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (x : F) (y : F) : |⟪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.

theorem real_inner_smul_self_left {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (x : F) (r : ℝ) : ⟪r • x, x⟫_ℝ = r * (‖x‖ * ‖x‖)

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

theorem real_inner_smul_self_right {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (x : F) (r : ℝ) : ⟪x, r • x⟫_ℝ = r * (‖x‖ * ‖x‖)

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

theorem norm_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {x : E} {r : 𝕜} (hx : x ≠ 0) (hr : r ≠ 0) : ‖⟪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

theorem abs_real_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {x : F} {r : ℝ} (hx : x ≠ 0) (hr : r ≠ 0) : |⟪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

theorem real_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_pos_mul {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {x : F} {r : ℝ} (hx : x ≠ 0) (hr : 0 < r) : ⟪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.

theorem real_inner_div_norm_mul_norm_eq_neg_one_of_ne_zero_of_neg_mul {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {x : F} {r : ℝ} (hx : x ≠ 0) (hr : r < 0) : ⟪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.

theorem norm_inner_eq_norm_tfae {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) (y : E) : [‖⟪x, y⟫_𝕜‖ = ‖x‖ * ‖y‖, x = 0 ∨ y = (⟪x, y⟫_𝕜 / ⟪x, x⟫_𝕜) • x, x = 0 ∨ ∃ (r : 𝕜), y = r • x, x = 0 ∨ y ∈ Submodule.span 𝕜 {x}].TFAE

theorem norm_inner_eq_norm_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {x : E} {y : E} (hx₀ : x ≠ 0) (hy₀ : y ≠ 0) : ‖⟪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‖.

theorem norm_inner_div_norm_mul_norm_eq_one_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) (y : E) : ‖⟪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.

theorem abs_real_inner_div_norm_mul_norm_eq_one_iff {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (x : F) (y : F) : |⟪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.

theorem inner_eq_norm_mul_iff_div {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {x : E} {y : E} (h₀ : x ≠ 0) : ⟪x, y⟫_𝕜 = ↑‖x‖ * ↑‖y‖ ↔ (↑‖y‖ / ↑‖x‖) • x = y

theorem inner_eq_norm_mul_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {x : E} {y : E} : ⟪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 norm_inner_eq_norm_iff, which takes the weaker hypothesis abs ⟪x, y⟫ = ‖x‖ * ‖y‖.

theorem inner_eq_norm_mul_iff_real {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {x : F} {y : F} : ⟪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 norm_inner_eq_norm_iff, which takes the weaker hypothesis abs ⟪x, y⟫ = ‖x‖ * ‖y‖.

theorem real_inner_div_norm_mul_norm_eq_one_iff {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (x : F) (y : F) : ⟪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.

theorem real_inner_div_norm_mul_norm_eq_neg_one_iff {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (x : F) (y : F) : ⟪x, y⟫_ℝ / (‖x‖ * ‖y‖) = -1 ↔ x ≠ 0 ∧ ∃ 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_eq_one_iff_of_norm_one {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {x : E} {y : E} (hx : ‖x‖ = 1) (hy : ‖y‖ = 1) : ⟪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.

theorem inner_lt_norm_mul_iff_real {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {x : F} {y : F} : ⟪x, y⟫_ℝ < ‖x‖ * ‖y‖ ↔ ‖y‖ • x ≠ ‖x‖ • y

theorem inner_lt_one_iff_real_of_norm_one {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {x : F} {y : F} (hx : ‖x‖ = 1) (hy : ‖y‖ = 1) : ⟪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.

theorem eq_of_norm_le_re_inner_eq_norm_sq {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {x : E} {y : E} (hle : ‖x‖ ≤ ‖y‖) (h : RCLike.re ⟪x, y⟫_𝕜 = ‖y‖ ^ 2) : x = y

The sphere of radius r = ‖y‖ is tangent to the plane ⟪x, y⟫ = ‖y‖ ^ 2 at x = y.

theorem inner_sum_smul_sum_smul_of_sum_eq_zero {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {ι₁ : Type u_4} {s₁ : Finset ι₁} {w₁ : ι₁ → ℝ} (v₁ : ι₁ → F) (h₁ : ∑ i ∈ s₁, w₁ i = 0) {ι₂ : Type u_5} {s₂ : Finset ι₂} {w₂ : ι₂ → ℝ} (v₂ : ι₂ → F) (h₂ : ∑ i ∈ s₂, w₂ i = 0) : ⟪∑ i₁ ∈ s₁, w₁ i₁ • v₁ i₁, ∑ i₂ ∈ s₂, w₂ i₂ • v₂ i₂⟫_ℝ = (-∑ i₁ ∈ s₁, ∑ i₂ ∈ 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.

def innerₛₗ (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] : E →ₗ⋆[𝕜] E →ₗ[𝕜] 𝕜

The inner product as a sesquilinear map.

Equations

• innerₛₗ 𝕜 = LinearMap.mk₂'ₛₗ (starRingEnd 𝕜) (RingHom.id 𝕜) (fun (v w : E) => ⟪v, w⟫_𝕜) ⋯ ⋯ ⋯ ⋯

@[simp]

theorem innerₛₗ_apply_coe (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (v : E) : ⇑((innerₛₗ 𝕜) v) = fun (w : E) => ⟪v, w⟫_𝕜

@[simp]

theorem innerₛₗ_apply (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (v : E) (w : E) : ((innerₛₗ 𝕜) v) w = ⟪v, w⟫_𝕜

def innerₗ (F : Type u_3) [NormedAddCommGroup F] [InnerProductSpace ℝ F] : F →ₗ[ℝ] F →ₗ[ℝ] ℝ

The inner product as a bilinear map in the real case.

Equations

• innerₗ F = innerₛₗ ℝ

@[simp]

theorem flip_innerₗ (F : Type u_3) [NormedAddCommGroup F] [InnerProductSpace ℝ F] : (innerₗ F).flip = innerₗ F

@[simp]

theorem innerₗ_apply {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (v : F) (w : F) : ((innerₗ F) v) w = ⟪v, w⟫_ℝ

def innerSL (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] : E →L⋆[𝕜] E →L[𝕜] 𝕜

The inner product as a continuous sesquilinear map. Note that toDualMap (resp. toDual) in InnerProductSpace.Dual is a version of this given as a linear isometry (resp. linear isometric equivalence).

Equations

• innerSL 𝕜 = (innerₛₗ 𝕜).mkContinuous₂ 1 ⋯

@[simp]

theorem innerSL_apply_coe (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (v : E) : ⇑((innerSL 𝕜) v) = fun (w : E) => ⟪v, w⟫_𝕜

@[simp]

theorem innerSL_apply (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (v : E) (w : E) : ((innerSL 𝕜) v) w = ⟪v, w⟫_𝕜

@[simp]

theorem innerSL_apply_norm (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) : ‖(innerSL 𝕜) x‖ = ‖x‖

innerSL is an isometry. Note that the associated LinearIsometry is defined in InnerProductSpace.Dual as toDualMap.

theorem norm_innerSL_le (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] : ‖innerSL 𝕜‖ ≤ 1

def innerSLFlip (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] : E →L[𝕜] E →L⋆[𝕜] 𝕜

The inner product as a continuous sesquilinear map, with the two arguments flipped.

Equations

• innerSLFlip 𝕜 = (ContinuousLinearMap.flipₗᵢ' E E 𝕜 (RingHom.id 𝕜) (starRingEnd 𝕜)) (innerSL 𝕜)

@[simp]

theorem innerSLFlip_apply (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) (y : E) : ((innerSLFlip 𝕜) x) y = ⟪y, x⟫_𝕜

@[simp]

theorem innerSL_real_flip (F : Type u_3) [NormedAddCommGroup F] [InnerProductSpace ℝ F] : (innerSL ℝ).flip = innerSL ℝ

noncomputable def ContinuousLinearMap.toSesqForm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {E' : Type u_4} [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] : (E →L[𝕜] E') →L[𝕜] E' →L⋆[𝕜] E →L[𝕜] 𝕜

Given f : E →L[𝕜] E', construct the continuous sesquilinear form fun x y ↦ ⟪x, A y⟫, given as a continuous linear map.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ContinuousLinearMap.toSesqForm_apply_coe {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {E' : Type u_4} [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] (f : E →L[𝕜] E') (x : E') : (ContinuousLinearMap.toSesqForm f) x = ((innerSL 𝕜) x).comp f

theorem ContinuousLinearMap.toSesqForm_apply_norm_le {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {E' : Type u_4} [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] {f : E →L[𝕜] E'} {v : E'} : ‖(ContinuousLinearMap.toSesqForm f) v‖ ≤ ‖f‖ * ‖v‖

theorem isBoundedBilinearMap_inner {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedSpace ℝ E] : IsBoundedBilinearMap ℝ fun (p : E × E) => ⟪p.1, p.2⟫_𝕜

When an inner product space E over 𝕜 is considered as a real normed space, its inner product satisfies IsBoundedBilinearMap.

In order to state these results, we need a NormedSpace ℝ E instance. We will later establish such an instance by restriction-of-scalars, InnerProductSpace.rclikeToReal 𝕜 E, but this instance may be not definitionally equal to some other “natural” instance. So, we assume [NormedSpace ℝ E].

theorem Orthonormal.sum_inner_products_le {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} (x : E) {v : ι → E} {s : Finset ι} (hv : Orthonormal 𝕜 v) : ∑ i ∈ s, ‖⟪v i, x⟫_𝕜‖ ^ 2 ≤ ‖x‖ ^ 2

Bessel's inequality for finite sums.

theorem Orthonormal.tsum_inner_products_le {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} (x : E) {v : ι → E} (hv : Orthonormal 𝕜 v) : ∑' (i : ι), ‖⟪v i, x⟫_𝕜‖ ^ 2 ≤ ‖x‖ ^ 2

Bessel's inequality.

theorem Orthonormal.inner_products_summable {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} (x : E) {v : ι → E} (hv : Orthonormal 𝕜 v) : Summable fun (i : ι) => ‖⟪v i, x⟫_𝕜‖ ^ 2

The sum defined in Bessel's inequality is summable.

instance RCLike.innerProductSpace {𝕜 : Type u_1} [RCLike 𝕜] : InnerProductSpace 𝕜 𝕜

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

Equations

• RCLike.innerProductSpace = InnerProductSpace.mk ⋯ ⋯ ⋯ ⋯

@[simp]

theorem RCLike.inner_apply {𝕜 : Type u_1} [RCLike 𝕜] (x : 𝕜) (y : 𝕜) : ⟪x, y⟫_𝕜 = (starRingEnd 𝕜) x * y

Inner product space structure on subspaces

instance Submodule.innerProductSpace {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (W : Submodule 𝕜 E) : InnerProductSpace 𝕜 ↥W

Induced inner product on a submodule.

Equations

• W.innerProductSpace = let __src := W.normedSpace; InnerProductSpace.mk ⋯ ⋯ ⋯ ⋯

@[simp]

theorem Submodule.coe_inner {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (W : Submodule 𝕜 E) (x : ↥W) (y : ↥W) : ⟪x, y⟫_𝕜 = ⟪↑x, ↑y⟫_𝕜

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

theorem Orthonormal.codRestrict {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {v : ι → E} (hv : Orthonormal 𝕜 v) (s : Submodule 𝕜 E) (hvs : ∀ (i : ι), v i ∈ s) : Orthonormal 𝕜 (Set.codRestrict v (↑s) hvs)

theorem orthonormal_span {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {v : ι → E} (hv : Orthonormal 𝕜 v) : Orthonormal 𝕜 fun (i : ι) => ⟨v i, ⋯⟩

Families of mutually-orthogonal subspaces of an inner product space

def OrthogonalFamily (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} (G : ι → Type u_5) [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] (V : (i : ι) → G i →ₗᵢ[𝕜] E) : Prop

An indexed family of mutually-orthogonal subspaces of an inner product space E.

The simple way to express this concept would be as a condition on V : ι → Submodule 𝕜 E. We instead implement it as a condition on a family of inner product spaces each equipped with an isometric embedding into E, thus making it a property of morphisms rather than subobjects. The connection to the subobject spelling is shown in orthogonalFamily_iff_pairwise.

This definition is less lightweight, but allows for better definitional properties when the inner product space structure on each of the submodules is important -- for example, when considering their Hilbert sum (PiLp V 2). For example, given an orthonormal set of vectors v : ι → E, we have an associated orthogonal family of one-dimensional subspaces of E, which it is convenient to be able to discuss using ι → 𝕜 rather than Π i : ι, span 𝕜 (v i).

Equations

• OrthogonalFamily 𝕜 G V = Pairwise fun (i j : ι) => ∀ (v : G i) (w : G j), ⟪(V i) v, (V j) w⟫_𝕜 = 0

theorem Orthonormal.orthogonalFamily {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {v : ι → E} (hv : Orthonormal 𝕜 v) : OrthogonalFamily 𝕜 (fun (_i : ι) => 𝕜) fun (i : ι) => LinearIsometry.toSpanSingleton 𝕜 E ⋯

theorem OrthogonalFamily.eq_ite {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {G : ι → Type u_5} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] {V : (i : ι) → G i →ₗᵢ[𝕜] E} (hV : OrthogonalFamily 𝕜 G V) [DecidableEq ι] {i : ι} {j : ι} (v : G i) (w : G j) : ⟪(V i) v, (V j) w⟫_𝕜 = if i = j then ⟪(V i) v, (V j) w⟫_𝕜 else 0

theorem OrthogonalFamily.inner_right_dfinsupp {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {G : ι → Type u_5} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] {V : (i : ι) → G i →ₗᵢ[𝕜] E} (hV : OrthogonalFamily 𝕜 G V) [dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)] [DecidableEq ι] (l : DirectSum ι fun (i : ι) => G i) (i : ι) (v : G i) : ⟪(V i) v, DFinsupp.sum l fun (j : ι) => ⇑(V j)⟫_𝕜 = ⟪v, l i⟫_𝕜

theorem OrthogonalFamily.inner_right_fintype {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {G : ι → Type u_5} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] {V : (i : ι) → G i →ₗᵢ[𝕜] E} (hV : OrthogonalFamily 𝕜 G V) [Fintype ι] (l : (i : ι) → G i) (i : ι) (v : G i) : ⟪(V i) v, ∑ j : ι, (V j) (l j)⟫_𝕜 = ⟪v, l i⟫_𝕜

theorem OrthogonalFamily.inner_sum {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {G : ι → Type u_5} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] {V : (i : ι) → G i →ₗᵢ[𝕜] E} (hV : OrthogonalFamily 𝕜 G V) (l₁ : (i : ι) → G i) (l₂ : (i : ι) → G i) (s : Finset ι) : ⟪∑ i ∈ s, (V i) (l₁ i), ∑ j ∈ s, (V j) (l₂ j)⟫_𝕜 = ∑ i ∈ s, ⟪l₁ i, l₂ i⟫_𝕜

theorem OrthogonalFamily.norm_sum {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {G : ι → Type u_5} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] {V : (i : ι) → G i →ₗᵢ[𝕜] E} (hV : OrthogonalFamily 𝕜 G V) (l : (i : ι) → G i) (s : Finset ι) : ‖∑ i ∈ s, (V i) (l i)‖ ^ 2 = ∑ i ∈ s, ‖l i‖ ^ 2

theorem OrthogonalFamily.comp {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {G : ι → Type u_5} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] {V : (i : ι) → G i →ₗᵢ[𝕜] E} (hV : OrthogonalFamily 𝕜 G V) {γ : Type u_6} {f : γ → ι} (hf : Function.Injective f) : OrthogonalFamily 𝕜 (fun (g : γ) => G (f g)) fun (g : γ) => V (f g)

The composition of an orthogonal family of subspaces with an injective function is also an orthogonal family.

theorem OrthogonalFamily.orthonormal_sigma_orthonormal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {G : ι → Type u_5} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] {V : (i : ι) → G i →ₗᵢ[𝕜] E} (hV : OrthogonalFamily 𝕜 G V) {α : ι → Type u_6} {v_family : (i : ι) → α i → G i} (hv_family : ∀ (i : ι), Orthonormal 𝕜 (v_family i)) : Orthonormal 𝕜 fun (a : (i : ι) × α i) => (V a.fst) (v_family a.fst a.snd)

theorem OrthogonalFamily.norm_sq_diff_sum {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {G : ι → Type u_5} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] {V : (i : ι) → G i →ₗᵢ[𝕜] E} (hV : OrthogonalFamily 𝕜 G V) [DecidableEq ι] (f : (i : ι) → G i) (s₁ : Finset ι) (s₂ : Finset ι) : ‖∑ i ∈ s₁, (V i) (f i) - ∑ i ∈ s₂, (V i) (f i)‖ ^ 2 = ∑ i ∈ s₁ \ s₂, ‖f i‖ ^ 2 + ∑ i ∈ s₂ \ s₁, ‖f i‖ ^ 2

theorem OrthogonalFamily.summable_iff_norm_sq_summable {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {G : ι → Type u_5} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] {V : (i : ι) → G i →ₗᵢ[𝕜] E} (hV : OrthogonalFamily 𝕜 G V) [CompleteSpace E] (f : (i : ι) → G i) : (Summable fun (i : ι) => (V i) (f i)) ↔ Summable fun (i : ι) => ‖f i‖ ^ 2

A family f of mutually-orthogonal elements of E is summable, if and only if (fun i ↦ ‖f i‖ ^ 2) is summable.

theorem OrthogonalFamily.independent {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {V : ι → Submodule 𝕜 E} (hV : OrthogonalFamily 𝕜 (fun (i : ι) => ↥(V i)) fun (i : ι) => (V i).subtypeₗᵢ) : CompleteLattice.Independent V

An orthogonal family forms an independent family of subspaces; that is, any collection of elements each from a different subspace in the family is linearly independent. In particular, the pairwise intersections of elements of the family are 0.

theorem DirectSum.IsInternal.collectedBasis_orthonormal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} [DecidableEq ι] {V : ι → Submodule 𝕜 E} (hV : OrthogonalFamily 𝕜 (fun (i : ι) => ↥(V i)) fun (i : ι) => (V i).subtypeₗᵢ) (hV_sum : DirectSum.IsInternal fun (i : ι) => V i) {α : ι → Type u_6} {v_family : (i : ι) → Basis (α i) 𝕜 ↥(V i)} (hv_family : ∀ (i : ι), Orthonormal 𝕜 ⇑(v_family i)) : Orthonormal 𝕜 ⇑(hV_sum.collectedBasis v_family)

def Inner.rclikeToReal (𝕜 : Type u_1) (E : Type u_2) [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] : 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

• Inner.rclikeToReal 𝕜 E = { inner := fun (x y : E) => RCLike.re ⟪x, y⟫_𝕜 }

def InnerProductSpace.rclikeToReal (𝕜 : Type u_1) (E : Type u_2) [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] : InnerProductSpace ℝ 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

• InnerProductSpace.rclikeToReal 𝕜 E = let __src := Inner.rclikeToReal 𝕜 E; let __src_1 := NormedSpace.restrictScalars ℝ 𝕜 E; InnerProductSpace.mk ⋯ ⋯ ⋯ ⋯

theorem real_inner_eq_re_inner (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) (y : E) : ⟪x, y⟫_ℝ = RCLike.re ⟪x, y⟫_𝕜

theorem real_inner_I_smul_self (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) : ⟪x, RCLike.I • x⟫_ℝ = 0

def InnerProductSpace.complexToReal {G : Type u_4} [NormedAddCommGroup G] [InnerProductSpace ℂ G] : InnerProductSpace ℝ G

A complex inner product implies a real inner product. This cannot be an instance since it creates a diamond with PiLp.innerProductSpace because re (sum i, inner (x i) (y i)) and sum i, re (inner (x i) (y i)) are not defeq.

Equations

• InnerProductSpace.complexToReal = InnerProductSpace.rclikeToReal ℂ G

instance instInnerProductSpaceRealComplex : InnerProductSpace ℝ ℂ

Equations

• instInnerProductSpaceRealComplex = InnerProductSpace.complexToReal

@[simp]

theorem Complex.inner (w : ℂ) (z : ℂ) : ⟪w, z⟫_ℝ = ((starRingEnd ℂ) w * z).re

theorem inner_map_complex {G : Type u_4} [NormedAddCommGroup G] [InnerProductSpace ℝ G] (f : G ≃ₗᵢ[ℝ] ℂ) (x : G) (y : G) : ⟪x, y⟫_ℝ = ((starRingEnd ℂ) (f x) * f y).re

The inner product on an inner product space of dimension 2 can be evaluated in terms of a complex-number representation of the space.

Continuity of the inner product

theorem continuous_inner {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] : Continuous fun (p : E × E) => ⟪p.1, p.2⟫_𝕜

theorem Filter.Tendsto.inner {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {α : Type u_4} {f : α → E} {g : α → E} {l : Filter α} {x : E} {y : E} (hf : Filter.Tendsto f l (nhds x)) (hg : Filter.Tendsto g l (nhds y)) : Filter.Tendsto (fun (t : α) => ⟪f t, g t⟫_𝕜) l (nhds ⟪x, y⟫_𝕜)

theorem ContinuousWithinAt.inner {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {α : Type u_4} [TopologicalSpace α] {f : α → E} {g : α → E} {x : α} {s : Set α} (hf : ContinuousWithinAt f s x) (hg : ContinuousWithinAt g s x) : ContinuousWithinAt (fun (t : α) => ⟪f t, g t⟫_𝕜) s x

theorem ContinuousAt.inner {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {α : Type u_4} [TopologicalSpace α] {f : α → E} {g : α → E} {x : α} (hf : ContinuousAt f x) (hg : ContinuousAt g x) : ContinuousAt (fun (t : α) => ⟪f t, g t⟫_𝕜) x

theorem ContinuousOn.inner {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {α : Type u_4} [TopologicalSpace α] {f : α → E} {g : α → E} {s : Set α} (hf : ContinuousOn f s) (hg : ContinuousOn g s) : ContinuousOn (fun (t : α) => ⟪f t, g t⟫_𝕜) s

theorem Continuous.inner {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {α : Type u_4} [TopologicalSpace α] {f : α → E} {g : α → E} (hf : Continuous f) (hg : Continuous g) : Continuous fun (t : α) => ⟪f t, g t⟫_𝕜

def ContinuousLinearMap.reApplyInnerSelf {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (T : E →L[𝕜] E) (x : E) : ℝ

Extract a real bilinear form from an operator T, by taking the pairing fun x ↦ re ⟪T x, x⟫.

Equations

• T.reApplyInnerSelf x = RCLike.re ⟪T x, x⟫_𝕜

theorem ContinuousLinearMap.reApplyInnerSelf_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (T : E →L[𝕜] E) (x : E) : T.reApplyInnerSelf x = RCLike.re ⟪T x, x⟫_𝕜

theorem ContinuousLinearMap.reApplyInnerSelf_continuous {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (T : E →L[𝕜] E) : Continuous T.reApplyInnerSelf

theorem ContinuousLinearMap.reApplyInnerSelf_smul {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (T : E →L[𝕜] E) (x : E) {c : 𝕜} : T.reApplyInnerSelf (c • x) = ‖c‖ ^ 2 * T.reApplyInnerSelf x

instance UniformSpace.Completion.toInner {𝕜' : Type u_4} {E' : Type u_5} [TopologicalSpace 𝕜'] [UniformSpace E'] [Inner 𝕜' E'] : Inner 𝕜' (UniformSpace.Completion E')

Equations

• UniformSpace.Completion.toInner = { inner := Function.curry (⋯.extend (Function.uncurry inner)) }

@[simp]

theorem UniformSpace.Completion.inner_coe {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (a : E) (b : E) : ⟪↑E a, ↑E b⟫_𝕜 = ⟪a, b⟫_𝕜

theorem UniformSpace.Completion.continuous_inner {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] : Continuous (Function.uncurry inner)

theorem UniformSpace.Completion.Continuous.inner {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {α : Type u_4} [TopologicalSpace α] {f : α → UniformSpace.Completion E} {g : α → UniformSpace.Completion E} (hf : Continuous f) (hg : Continuous g) : Continuous fun (x : α) => ⟪f x, g x⟫_𝕜

instance UniformSpace.Completion.innerProductSpace {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] : InnerProductSpace 𝕜 (UniformSpace.Completion E)

Equations

• UniformSpace.Completion.innerProductSpace = InnerProductSpace.mk ⋯ ⋯ ⋯ ⋯