Inner product spaces

This file defines inner product spaces. 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.

Rather than defining the norm on an inner product space to be √(re ⟪x, x⟫), we assume that a norm is given, and add a hypothesis stating that ‖x‖ ^ 2 = re (inner x x). This makes it possible to handle spaces where the norm is equal, but not defeq, to the square root of the inner product. Defining a norm starting from an inner product is handled via the InnerProductSpace.Core structure.

This file is intended to contain the minimal amount of machinery needed to define inner product spaces, and to construct a normed space from an inner product space. Many more general lemmas can be found in Analysis.InnerProductSpace.Basic. 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.

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 InnerProductSpace.«term⟪_,_⟫__» : Lean.ParserDescr

The inner product with values in 𝕜.

Equations

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

def InnerProductSpace.«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 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 𝕜] [SeminormedAddCommGroup E] extends NormedSpace 𝕜 E, Inner 𝕜 E : Type (max u_4 u_5)

A (pre) inner product space is a vector space with an additional operation called inner product. The (semi)norm could be derived from the inner product, instead we require the existence of a seminorm and the fact that ‖x‖^2 = re ⟪x, x⟫ to be able to put instances on 𝕂 or product spaces.

Note that NormedSpace does not assume that ‖x‖=0 implies x=0 (it is rather a seminorm).

To construct a seminorm from an inner product, see PreInnerProductSpace.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 (inner x x)

  The inner product induces the norm.

• conj_symm (x y : E) : (starRingEnd 𝕜) (inner y x) = inner x y

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

• add_left (x y z : E) : inner (x + y) z = inner x z + inner y z

  The inner product is additive in the first coordinate.

• smul_left (x y : E) (r : 𝕜) : inner (r • x) y = (starRingEnd 𝕜) r * inner 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 PreInnerProductSpace.Core (𝕜 : Type u_4) (F : Type u_5) [RCLike 𝕜] [AddCommGroup F] [Module 𝕜 F] extends Inner 𝕜 F : Type (max u_4 u_5)

A structure requiring that a scalar product is positive semidefinite and symmetric.

• inner : F → F → 𝕜
• conj_symm (x y : F) : (starRingEnd 𝕜) (inner y x) = inner x y

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

• nonneg_re (x : F) : 0 ≤ RCLike.re (inner x x)

  The inner product is positive (semi)definite.

• add_left (x y z : F) : inner (x + y) z = inner x z + inner y z

  The inner product is additive in the first coordinate.

• smul_left (x y : F) (r : 𝕜) : inner (r • x) y = (starRingEnd 𝕜) r * inner x y

  The inner product is conjugate linear in the first coordinate.

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

A structure requiring that a scalar product is positive definite. Some theorems that require this assumptions are put under section InnerProductSpace.Core.

• inner : F → F → 𝕜
• conj_symm (x y : F) : (starRingEnd 𝕜) (inner y x) = inner x y
• nonneg_re (x : F) : 0 ≤ RCLike.re (inner x x)
• add_left (x y z : F) : inner (x + y) z = inner x z + inner y z
• smul_left (x y : F) (r : 𝕜) : inner (r • x) y = (starRingEnd 𝕜) r * inner x y
• definite (x : F) : inner x x = 0 → x = 0

  The inner product is positive definite.

instance instCoreOfCore (𝕜 : Type u_4) (F : Type u_5) [RCLike 𝕜] [AddCommGroup F] [Module 𝕜 F] [cd : InnerProductSpace.Core 𝕜 F] : PreInnerProductSpace.Core 𝕜 F

Equations

• instCoreOfCore 𝕜 F = { inner := inner, conj_symm := ⋯, nonneg_re := ⋯, add_left := ⋯, smul_left := ⋯ }

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

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

Equations

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

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 := ⋯, add_left := ⋯, smul_left := ⋯, definite := ⋯ }

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

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

Equations

• InnerProductSpace.Core.toPreInner' = c.toInner

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

The norm squared function for PreInnerProductSpace.Core structure.

Equations

• InnerProductSpace.Core.normSq x = RCLike.re (inner x x)

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

theorem InnerProductSpace.Core.inner_self_nonneg {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [AddCommGroup F] [Module 𝕜 F] [c : PreInnerProductSpace.Core 𝕜 F] {x : F} : 0 ≤ RCLike.re (inner x x)

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

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

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

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

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

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

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

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

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

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

theorem InnerProductSpace.Core.inner_self_of_eq_zero {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [AddCommGroup F] [Module 𝕜 F] [c : PreInnerProductSpace.Core 𝕜 F] {x : F} : x = 0 → inner x x = 0

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

theorem InnerProductSpace.Core.ne_zero_of_inner_self_ne_zero {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [AddCommGroup F] [Module 𝕜 F] [c : PreInnerProductSpace.Core 𝕜 F] {x : F} : inner 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 : PreInnerProductSpace.Core 𝕜 F] (x : F) : ↑(RCLike.re (inner x x)) = inner x x

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

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

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

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

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

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

theorem InnerProductSpace.Core.inner_add_add_self {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [AddCommGroup F] [Module 𝕜 F] [c : PreInnerProductSpace.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)

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

theorem InnerProductSpace.Core.inner_smul_ofReal_left {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [AddCommGroup F] [Module 𝕜 F] [c : PreInnerProductSpace.Core 𝕜 F] (x y : F) {t : ℝ} : inner (↑t • x) y = inner x y * ↑t

theorem InnerProductSpace.Core.inner_smul_ofReal_right {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [AddCommGroup F] [Module 𝕜 F] [c : PreInnerProductSpace.Core 𝕜 F] (x y : F) {t : ℝ} : inner x (↑t • y) = inner x y * ↑t

theorem InnerProductSpace.Core.re_inner_smul_ofReal_smul_self {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [AddCommGroup F] [Module 𝕜 F] [c : PreInnerProductSpace.Core 𝕜 F] (x : F) {t : ℝ} : RCLike.re (inner (↑t • x) (↑t • x)) = InnerProductSpace.Core.normSq x * t * t

theorem InnerProductSpace.Core.cauchy_schwarz_aux' {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [AddCommGroup F] [Module 𝕜 F] [c : PreInnerProductSpace.Core 𝕜 F] (x y : F) (t : ℝ) : 0 ≤ InnerProductSpace.Core.normSq x * t * t + 2 * RCLike.re (inner x y) * t + InnerProductSpace.Core.normSq y

An auxiliary equality useful to prove the Cauchy–Schwarz inequality. Here we use the standard argument involving the discriminant of quadratic form.

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

Another auxiliary equality related with the Cauchy–Schwarz inequality: the square of the seminorm 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 : PreInnerProductSpace.Core 𝕜 F] (x y : F) : ‖inner x y‖ * ‖inner y x‖ ≤ RCLike.re (inner x x) * RCLike.re (inner y y)

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

(This is not intended for general use; see Analysis.InnerProductSpace.Basic for a variety of versions of Cauchy-Schwartz for an inner product space, rather than a PreInnerProductSpace.Core).

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

(Semi)norm constructed from an PreInnerProductSpace.Core structure, defined to be the square root of the scalar product.

Equations

• InnerProductSpace.Core.toNorm = { norm := fun (x : F) => √(RCLike.re (inner x x)) }

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

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

theorem InnerProductSpace.Core.sqrt_normSq_eq_norm {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [AddCommGroup F] [Module 𝕜 F] [c : PreInnerProductSpace.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 : PreInnerProductSpace.Core 𝕜 F] (x y : F) : ‖inner x y‖ ≤ ‖x‖ * ‖y‖

Cauchy–Schwarz inequality with norm

def InnerProductSpace.Core.toSeminormedAddCommGroup {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [AddCommGroup F] [Module 𝕜 F] [c : PreInnerProductSpace.Core 𝕜 F] : SeminormedAddCommGroup F

Seminormed group structure constructed from an PreInnerProductSpace.Core structure

Equations

• InnerProductSpace.Core.toSeminormedAddCommGroup = { toFun := fun (x : F) => √(RCLike.re (inner x x)), map_zero' := ⋯, add_le' := ⋯, neg' := ⋯ }.toSeminormedAddCommGroup

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

Normed space (which is actually a seminorm) structure constructed from an PreInnerProductSpace.Core structure

Equations

• InnerProductSpace.Core.toSeminormedSpace = NormedSpace.mk ⋯

def InnerProductSpace.Core.toInner' {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [AddCommGroup F] [Module 𝕜 F] [cd : 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' = cd.toInner

theorem InnerProductSpace.Core.inner_self_eq_zero {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [AddCommGroup F] [Module 𝕜 F] [cd : InnerProductSpace.Core 𝕜 F] {x : F} : inner x x = 0 ↔ x = 0

theorem InnerProductSpace.Core.normSq_eq_zero {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [AddCommGroup F] [Module 𝕜 F] [cd : 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] [cd : InnerProductSpace.Core 𝕜 F] {x : F} : inner x x ≠ 0 ↔ x ≠ 0

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

Normed group structure constructed from an InnerProductSpace.Core structure

Equations

• InnerProductSpace.Core.toNormedAddCommGroup = { toFun := fun (x : F) => √(RCLike.re (inner 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] [cd : 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] (cd : 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 cd = InnerProductSpace.mk ⋯ ⋯ ⋯ ⋯