L² inner product space structure on finite products of inner product spaces

The L² norm on a finite product of inner product spaces is compatible with an inner product $$ \langle x, y\rangle = \sum \langle x_i, y_i \rangle. $$ This is recorded in this file as an inner product space instance on PiLp 2.

This file develops the notion of a finite dimensional Hilbert space over 𝕜 = ℂ, ℝ, referred to as E. We define an OrthonormalBasis 𝕜 ι E as a linear isometric equivalence between E and EuclideanSpace 𝕜 ι. Then stdOrthonormalBasis shows that such an equivalence always exists if E is finite dimensional. We provide language for converting between a basis that is orthonormal and an orthonormal basis (e.g. Basis.toOrthonormalBasis). We show that orthonormal bases for each summand in a direct sum of spaces can be combined into an orthonormal basis for the whole sum in DirectSum.IsInternal.subordinateOrthonormalBasis. In the last section, various properties of matrices are explored.

Main definitions

• EuclideanSpace 𝕜 n: defined to be PiLp 2 (n → 𝕜) for any Fintype n, i.e., the space from functions to n to 𝕜 with the L² norm. We register several instances on it (notably that it is a finite-dimensional inner product space), and provide a !ₚ[] notation (for numeric subscripts like ₂) for the case when the indexing type is Fin n.

• OrthonormalBasis 𝕜 ι: defined to be an isometry to Euclidean space from a given finite-dimensional inner product space, E ≃ₗᵢ[𝕜] EuclideanSpace 𝕜 ι.

• Basis.toOrthonormalBasis: constructs an OrthonormalBasis for a finite-dimensional Euclidean space from a Basis which is Orthonormal.

• Orthonormal.exists_orthonormalBasis_extension: provides an existential result of an OrthonormalBasis extending a given orthonormal set

• exists_orthonormalBasis: provides an orthonormal basis on a finite dimensional vector space

• stdOrthonormalBasis: provides an arbitrarily-chosen OrthonormalBasis of a given finite dimensional inner product space

For consequences in infinite dimension (Hilbert bases, etc.), see the file Analysis.InnerProductSpace.L2Space.

instance PiLp.innerProductSpace {𝕜 : Type u_3} [RCLike 𝕜] {ι : Type u_7} [Fintype ι] (f : ι → Type u_8) [(i : ι) → NormedAddCommGroup (f i)] [(i : ι) → InnerProductSpace 𝕜 (f i)] : InnerProductSpace 𝕜 (PiLp 2 f)

Equations

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

@[simp]

theorem PiLp.inner_apply {𝕜 : Type u_3} [RCLike 𝕜] {ι : Type u_7} [Fintype ι] {f : ι → Type u_8} [(i : ι) → NormedAddCommGroup (f i)] [(i : ι) → InnerProductSpace 𝕜 (f i)] (x y : PiLp 2 f) : inner 𝕜 x y = ∑ i : ι, inner 𝕜 (x i) (y i)

@[reducible, inline]

abbrev EuclideanSpace (𝕜 : Type u_7) (n : Type u_8) : Type (max u_7 u_8)

The standard real/complex Euclidean space, functions on a finite type. For an n-dimensional space use EuclideanSpace 𝕜 (Fin n).

For the case when n = Fin _, there is !₂[x, y, ...] notation for building elements of this type, analogous to ![x, y, ...] notation.

Equations

• EuclideanSpace 𝕜 n = PiLp 2 fun (x : n) => 𝕜

def PiLp.vecNotation : Lean.ParserDescr

Notation for vectors in Lp space. !₂[x, y, ...] is a shorthand for (WithLp.equiv 2 _ _).symm ![x, y, ...], of type EuclideanSpace _ (Fin _).

This also works for other subscripts.

Equations

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

def EuclideanSpace.delabVecNotation : Lean.PrettyPrinter.Delaborator.Delab

Unexpander for the !₂[x, y, ...] notation.

Equations

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

theorem EuclideanSpace.nnnorm_eq {𝕜 : Type u_7} [RCLike 𝕜] {n : Type u_8} [Fintype n] (x : EuclideanSpace 𝕜 n) : ‖x‖₊ = NNReal.sqrt (∑ i : n, ‖x i‖₊ ^ 2)

theorem EuclideanSpace.norm_eq {𝕜 : Type u_7} [RCLike 𝕜] {n : Type u_8} [Fintype n] (x : EuclideanSpace 𝕜 n) : ‖x‖ = √(∑ i : n, ‖x i‖ ^ 2)

theorem EuclideanSpace.dist_eq {𝕜 : Type u_7} [RCLike 𝕜] {n : Type u_8} [Fintype n] (x y : EuclideanSpace 𝕜 n) : dist x y = √(∑ i : n, dist (x i) (y i) ^ 2)

theorem EuclideanSpace.nndist_eq {𝕜 : Type u_7} [RCLike 𝕜] {n : Type u_8} [Fintype n] (x y : EuclideanSpace 𝕜 n) : nndist x y = NNReal.sqrt (∑ i : n, nndist (x i) (y i) ^ 2)

theorem EuclideanSpace.edist_eq {𝕜 : Type u_7} [RCLike 𝕜] {n : Type u_8} [Fintype n] (x y : EuclideanSpace 𝕜 n) : edist x y = (∑ i : n, edist (x i) (y i) ^ 2) ^ (1 / 2)

theorem EuclideanSpace.ball_zero_eq {n : Type u_7} [Fintype n] (r : ℝ) (hr : 0 ≤ r) : Metric.ball 0 r = {x : EuclideanSpace ℝ n | ∑ i : n, x i ^ 2 < r ^ 2}

theorem EuclideanSpace.closedBall_zero_eq {n : Type u_7} [Fintype n] (r : ℝ) (hr : 0 ≤ r) : Metric.closedBall 0 r = {x : EuclideanSpace ℝ n | ∑ i : n, x i ^ 2 ≤ r ^ 2}

theorem EuclideanSpace.sphere_zero_eq {n : Type u_7} [Fintype n] (r : ℝ) (hr : 0 ≤ r) : Metric.sphere 0 r = {x : EuclideanSpace ℝ n | ∑ i : n, x i ^ 2 = r ^ 2}

@[simp]

theorem finrank_euclideanSpace {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] [Fintype ι] : Module.finrank 𝕜 (EuclideanSpace 𝕜 ι) = Fintype.card ι

theorem finrank_euclideanSpace_fin {𝕜 : Type u_3} [RCLike 𝕜] {n : ℕ} : Module.finrank 𝕜 (EuclideanSpace 𝕜 (Fin n)) = n

theorem EuclideanSpace.inner_eq_star_dotProduct {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] [Fintype ι] (x y : EuclideanSpace 𝕜 ι) : inner 𝕜 x y = (WithLp.equiv 2 (ι → 𝕜)) y ⬝ᵥ star ((WithLp.equiv 2 (ι → 𝕜)) x)

theorem EuclideanSpace.inner_piLp_equiv_symm {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] [Fintype ι] (x y : ι → 𝕜) : inner 𝕜 ((WithLp.equiv 2 (ι → 𝕜)).symm x) ((WithLp.equiv 2 (ι → 𝕜)).symm y) = y ⬝ᵥ star x

def DirectSum.IsInternal.isometryL2OfOrthogonalFamily {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [DecidableEq ι] {V : ι → Submodule 𝕜 E} (hV : IsInternal V) (hV' : OrthogonalFamily 𝕜 (fun (i : ι) => ↥(V i)) fun (i : ι) => (V i).subtypeₗᵢ) : E ≃ₗᵢ[𝕜] PiLp 2 fun (i : ι) => ↥(V i)

A finite, mutually orthogonal family of subspaces of E, which span E, induce an isometry from E to PiLp 2 of the subspaces equipped with the L2 inner product.

Equations

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

@[simp]

theorem DirectSum.IsInternal.isometryL2OfOrthogonalFamily_symm_apply {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [DecidableEq ι] {V : ι → Submodule 𝕜 E} (hV : IsInternal V) (hV' : OrthogonalFamily 𝕜 (fun (i : ι) => ↥(V i)) fun (i : ι) => (V i).subtypeₗᵢ) (w : PiLp 2 fun (i : ι) => ↥(V i)) : (hV.isometryL2OfOrthogonalFamily hV').symm w = ∑ i : ι, ↑(w i)

@[reducible, inline]

abbrev EuclideanSpace.equiv (ι : Type u_1) (𝕜 : Type u_3) [RCLike 𝕜] : EuclideanSpace 𝕜 ι ≃L[𝕜] ι → 𝕜

A shorthand for PiLp.continuousLinearEquiv.

Equations

• EuclideanSpace.equiv ι 𝕜 = PiLp.continuousLinearEquiv 2 𝕜 fun (x : ι) => 𝕜

@[reducible, inline]

abbrev EuclideanSpace.projₗ {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] (i : ι) : EuclideanSpace 𝕜 ι →ₗ[𝕜] 𝕜

The projection on the i-th coordinate of EuclideanSpace 𝕜 ι, as a linear map.

Equations

• EuclideanSpace.projₗ i = PiLp.projₗ 2 (fun (x : ι) => 𝕜) i

@[reducible, inline]

abbrev EuclideanSpace.proj {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] (i : ι) : EuclideanSpace 𝕜 ι →L[𝕜] 𝕜

The projection on the i-th coordinate of EuclideanSpace 𝕜 ι, as a continuous linear map.

Equations

• EuclideanSpace.proj i = PiLp.proj 2 (fun (x : ι) => 𝕜) i

def EuclideanSpace.single {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] [DecidableEq ι] (i : ι) (a : 𝕜) : EuclideanSpace 𝕜 ι

The vector given in euclidean space by being a : 𝕜 at coordinate i : ι and 0 : 𝕜 at all other coordinates.

Equations

• EuclideanSpace.single i a = (WithLp.equiv 2 ((i : ι) → (fun (x : ι) => 𝕜) i)).symm (Pi.single i a)

@[simp]

theorem WithLp.equiv_single {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] [DecidableEq ι] (i : ι) (a : 𝕜) : (WithLp.equiv 2 ((i : ι) → (fun (x : ι) => 𝕜) i)) (EuclideanSpace.single i a) = Pi.single i a

@[simp]

theorem WithLp.equiv_symm_single {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] [DecidableEq ι] (i : ι) (a : 𝕜) : (WithLp.equiv 2 (ι → 𝕜)).symm (Pi.single i a) = EuclideanSpace.single i a

@[simp]

theorem EuclideanSpace.single_apply {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] [DecidableEq ι] (i : ι) (a : 𝕜) (j : ι) : single i a j = if j = i then a else 0

theorem EuclideanSpace.inner_single_left {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] [DecidableEq ι] [Fintype ι] (i : ι) (a : 𝕜) (v : EuclideanSpace 𝕜 ι) : inner 𝕜 (single i a) v = (starRingEnd 𝕜) a * v i

theorem EuclideanSpace.inner_single_right {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] [DecidableEq ι] [Fintype ι] (i : ι) (a : 𝕜) (v : EuclideanSpace 𝕜 ι) : inner 𝕜 v (single i a) = a * (starRingEnd ((fun (x : ι) => 𝕜) i)) (v i)

@[simp]

theorem EuclideanSpace.norm_single {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] [DecidableEq ι] [Fintype ι] (i : ι) (a : 𝕜) : ‖single i a‖ = ‖a‖

@[simp]

theorem EuclideanSpace.nnnorm_single {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] [DecidableEq ι] [Fintype ι] (i : ι) (a : 𝕜) : ‖single i a‖₊ = ‖a‖₊

@[simp]

theorem EuclideanSpace.dist_single_same {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] [DecidableEq ι] [Fintype ι] (i : ι) (a b : 𝕜) : dist (single i a) (single i b) = dist a b

@[simp]

theorem EuclideanSpace.nndist_single_same {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] [DecidableEq ι] [Fintype ι] (i : ι) (a b : 𝕜) : nndist (single i a) (single i b) = nndist a b

@[simp]

theorem EuclideanSpace.edist_single_same {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] [DecidableEq ι] [Fintype ι] (i : ι) (a b : 𝕜) : edist (single i a) (single i b) = edist a b

theorem EuclideanSpace.orthonormal_single {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] [DecidableEq ι] [Fintype ι] : Orthonormal 𝕜 fun (i : ι) => single i 1

EuclideanSpace.single forms an orthonormal family.

theorem EuclideanSpace.piLpCongrLeft_single {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] [DecidableEq ι] [Fintype ι] {ι' : Type u_7} [Fintype ι'] [DecidableEq ι'] (e : ι' ≃ ι) (i' : ι') (v : 𝕜) : (LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e) (single i' v) = single (e i') v

structure OrthonormalBasis (ι : Type u_1) (𝕜 : Type u_3) [RCLike 𝕜] (E : Type u_4) [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] : Type (max (max u_1 u_3) u_4)

An orthonormal basis on E is an identification of E with its dimensional-matching EuclideanSpace 𝕜 ι.

• ofRepr :: (
• repr : E ≃ₗᵢ[𝕜] EuclideanSpace 𝕜 ι

  Linear isometry between E and EuclideanSpace 𝕜 ι representing the orthonormal basis.

• )

theorem OrthonormalBasis.repr_injective {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] : Function.Injective repr

instance OrthonormalBasis.instFunLike {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] : FunLike (OrthonormalBasis ι 𝕜 E) ι E

b i is the ith basis vector.

Equations

• OrthonormalBasis.instFunLike = { coe := fun (b : OrthonormalBasis ι 𝕜 E) (i : ι) => b.repr.symm (EuclideanSpace.single i 1), coe_injective' := ⋯ }

@[simp]

theorem OrthonormalBasis.coe_ofRepr {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [DecidableEq ι] (e : E ≃ₗᵢ[𝕜] EuclideanSpace 𝕜 ι) : ⇑{ repr := e } = fun (i : ι) => e.symm (EuclideanSpace.single i 1)

@[simp]

theorem OrthonormalBasis.repr_symm_single {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [DecidableEq ι] (b : OrthonormalBasis ι 𝕜 E) (i : ι) : b.repr.symm (EuclideanSpace.single i 1) = b i

@[simp]

theorem OrthonormalBasis.repr_self {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [DecidableEq ι] (b : OrthonormalBasis ι 𝕜 E) (i : ι) : b.repr (b i) = EuclideanSpace.single i 1

theorem OrthonormalBasis.repr_apply_apply {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (v : E) (i : ι) : b.repr v i = inner 𝕜 (b i) v

@[simp]

theorem OrthonormalBasis.orthonormal {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) : Orthonormal 𝕜 ⇑b

@[simp]

theorem OrthonormalBasis.norm_eq_one {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (i : ι) : ‖b i‖ = 1

@[simp]

theorem OrthonormalBasis.nnnorm_eq_one {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (i : ι) : ‖b i‖₊ = 1

@[simp]

theorem OrthonormalBasis.enorm_eq_one {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (i : ι) : ‖b i‖ₑ = 1

@[simp]

theorem OrthonormalBasis.inner_eq_zero {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) {i j : ι} (hij : i ≠ j) : inner 𝕜 (b i) (b j) = 0

def OrthonormalBasis.toBasis {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) : Basis ι 𝕜 E

The Basis ι 𝕜 E underlying the OrthonormalBasis

Equations

• b.toBasis = Basis.ofEquivFun b.repr.toLinearEquiv

@[simp]

theorem OrthonormalBasis.coe_toBasis {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) : ⇑b.toBasis = ⇑b

@[simp]

theorem OrthonormalBasis.coe_toBasis_repr {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) : b.toBasis.equivFun = b.repr.toLinearEquiv

@[simp]

theorem OrthonormalBasis.coe_toBasis_repr_apply {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (x : E) (i : ι) : (b.toBasis.repr x) i = b.repr x i

theorem OrthonormalBasis.sum_repr {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (x : E) : ∑ i : ι, b.repr x i • b i = x

theorem OrthonormalBasis.sum_repr' {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (x : E) : ∑ i : ι, inner 𝕜 (b i) x • b i = x

theorem OrthonormalBasis.sum_repr_symm {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (v : EuclideanSpace 𝕜 ι) : ∑ i : ι, v i • b i = b.repr.symm v

theorem OrthonormalBasis.sum_inner_mul_inner {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (x y : E) : ∑ i : ι, inner 𝕜 x (b i) * inner 𝕜 (b i) y = inner 𝕜 x y

theorem OrthonormalBasis.sum_sq_norm_inner {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (x : E) : ∑ i : ι, ‖inner 𝕜 (b i) x‖ ^ 2 = ‖x‖ ^ 2

theorem OrthonormalBasis.norm_le_card_mul_iSup_norm_inner {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (x : E) : ‖x‖ ≤ √↑(Fintype.card ι) * ⨆ (i : ι), ‖inner 𝕜 (b i) x‖

theorem OrthonormalBasis.orthogonalProjection_eq_sum {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] {U : Submodule 𝕜 E} [CompleteSpace ↥U] (b : OrthonormalBasis ι 𝕜 ↥U) (x : E) : U.orthogonalProjection x = ∑ i : ι, inner 𝕜 (↑(b i)) x • b i

def OrthonormalBasis.map {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] {G : Type u_7} [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] (b : OrthonormalBasis ι 𝕜 E) (L : E ≃ₗᵢ[𝕜] G) : OrthonormalBasis ι 𝕜 G

Mapping an orthonormal basis along a LinearIsometryEquiv.

Equations

• b.map L = { repr := L.symm.trans b.repr }

@[simp]

theorem OrthonormalBasis.map_apply {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] {G : Type u_7} [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] (b : OrthonormalBasis ι 𝕜 E) (L : E ≃ₗᵢ[𝕜] G) (i : ι) : (b.map L) i = L (b i)

@[simp]

theorem OrthonormalBasis.toBasis_map {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] {G : Type u_7} [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] (b : OrthonormalBasis ι 𝕜 E) (L : E ≃ₗᵢ[𝕜] G) : (b.map L).toBasis = b.toBasis.map L.toLinearEquiv

def Basis.toOrthonormalBasis {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (v : Basis ι 𝕜 E) (hv : Orthonormal 𝕜 ⇑v) : OrthonormalBasis ι 𝕜 E

A basis that is orthonormal is an orthonormal basis.

Equations

• v.toOrthonormalBasis hv = { repr := v.equivFun.isometryOfInner ⋯ }

@[simp]

theorem Basis.coe_toOrthonormalBasis_repr {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (v : Basis ι 𝕜 E) (hv : Orthonormal 𝕜 ⇑v) : ⇑(v.toOrthonormalBasis hv).repr = ⇑v.equivFun

@[simp]

theorem Basis.coe_toOrthonormalBasis_repr_symm {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (v : Basis ι 𝕜 E) (hv : Orthonormal 𝕜 ⇑v) : ⇑(v.toOrthonormalBasis hv).repr.symm = ⇑v.equivFun.symm

@[simp]

theorem Basis.toBasis_toOrthonormalBasis {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (v : Basis ι 𝕜 E) (hv : Orthonormal 𝕜 ⇑v) : (v.toOrthonormalBasis hv).toBasis = v

@[simp]

theorem Basis.coe_toOrthonormalBasis {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (v : Basis ι 𝕜 E) (hv : Orthonormal 𝕜 ⇑v) : ⇑(v.toOrthonormalBasis hv) = ⇑v

def Pi.orthonormalBasis {η : Type u_7} [Fintype η] {ι : η → Type u_8} [(i : η) → Fintype (ι i)] {𝕜 : Type u_9} [RCLike 𝕜] {E : η → Type u_10} [(i : η) → NormedAddCommGroup (E i)] [(i : η) → InnerProductSpace 𝕜 (E i)] (B : (i : η) → OrthonormalBasis (ι i) 𝕜 (E i)) : OrthonormalBasis ((i : η) × ι i) 𝕜 (PiLp 2 E)

Pi.orthonormalBasis (B : ∀ i, OrthonormalBasis (ι i) 𝕜 (E i)) is the Σ i, ι i-indexed orthonormal basis on Π i, E i given by B i on each component.

Equations

• Pi.orthonormalBasis B = { repr := (LinearIsometryEquiv.piLpCongrRight 2 fun (i : η) => (B i).repr).trans (LinearIsometryEquiv.piLpCurry 𝕜 2 fun (x : η) (x : ι x) => 𝕜).symm }

theorem Pi.orthonormalBasis.toBasis {η : Type u_7} [Fintype η] {ι : η → Type u_8} [(i : η) → Fintype (ι i)] {𝕜 : Type u_9} [RCLike 𝕜] {E : η → Type u_10} [(i : η) → NormedAddCommGroup (E i)] [(i : η) → InnerProductSpace 𝕜 (E i)] (B : (i : η) → OrthonormalBasis (ι i) 𝕜 (E i)) : (Pi.orthonormalBasis B).toBasis = (Pi.basis fun (i : η) => (B i).toBasis).map (WithLp.linearEquiv 2 𝕜 ((j : η) → E j)).symm

@[simp]

theorem Pi.orthonormalBasis_apply {η : Type u_7} [Fintype η] [DecidableEq η] {ι : η → Type u_8} [(i : η) → Fintype (ι i)] {𝕜 : Type u_9} [RCLike 𝕜] {E : η → Type u_10} [(i : η) → NormedAddCommGroup (E i)] [(i : η) → InnerProductSpace 𝕜 (E i)] (B : (i : η) → OrthonormalBasis (ι i) 𝕜 (E i)) (j : (i : η) × ι i) : (Pi.orthonormalBasis B) j = (WithLp.equiv 2 ((j : η) → E j)).symm (single j.fst ((B j.fst) j.snd))

@[simp]

theorem Pi.orthonormalBasis_repr {η : Type u_7} [Fintype η] {ι : η → Type u_8} [(i : η) → Fintype (ι i)] {𝕜 : Type u_9} [RCLike 𝕜] {E : η → Type u_10} [(i : η) → NormedAddCommGroup (E i)] [(i : η) → InnerProductSpace 𝕜 (E i)] (B : (i : η) → OrthonormalBasis (ι i) 𝕜 (E i)) (x : (i : η) → E i) (j : (i : η) × ι i) : (Pi.orthonormalBasis B).repr x j = (B j.fst).repr (x j.fst) j.snd

def OrthonormalBasis.mk {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] {v : ι → E} (hon : Orthonormal 𝕜 v) (hsp : ⊤ ≤ Submodule.span 𝕜 (Set.range v)) : OrthonormalBasis ι 𝕜 E

A finite orthonormal set that spans is an orthonormal basis

Equations

• OrthonormalBasis.mk hon hsp = (Basis.mk ⋯ hsp).toOrthonormalBasis ⋯

@[simp]

theorem OrthonormalBasis.coe_mk {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] {v : ι → E} (hon : Orthonormal 𝕜 v) (hsp : ⊤ ≤ Submodule.span 𝕜 (Set.range v)) : ⇑(OrthonormalBasis.mk hon hsp) = v

def OrthonormalBasis.span {ι' : Type u_2} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [DecidableEq E] {v' : ι' → E} (h : Orthonormal 𝕜 v') (s : Finset ι') : OrthonormalBasis { x : ι' // x ∈ s } 𝕜 ↥(Submodule.span 𝕜 ↑(Finset.image v' s))

Any finite subset of an orthonormal family is an OrthonormalBasis for its span.

Equations

• OrthonormalBasis.span h s = (OrthonormalBasis.mk ⋯ ⋯).map (LinearIsometryEquiv.ofEq (Submodule.span 𝕜 ↑(Finset.image v' s)) (Submodule.span 𝕜 (Set.range (v' ∘ Subtype.val))) ⋯).symm

@[simp]

theorem OrthonormalBasis.span_apply {ι' : Type u_2} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [DecidableEq E] {v' : ι' → E} (h : Orthonormal 𝕜 v') (s : Finset ι') (i : { x : ι' // x ∈ s }) : ↑((OrthonormalBasis.span h s) i) = v' ↑i

def OrthonormalBasis.mkOfOrthogonalEqBot {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] {v : ι → E} (hon : Orthonormal 𝕜 v) (hsp : (Submodule.span 𝕜 (Set.range v))ᗮ = ⊥) : OrthonormalBasis ι 𝕜 E

A finite orthonormal family of vectors whose span has trivial orthogonal complement is an orthonormal basis.

Equations

• OrthonormalBasis.mkOfOrthogonalEqBot hon hsp = OrthonormalBasis.mk hon ⋯

@[simp]

theorem OrthonormalBasis.coe_of_orthogonal_eq_bot_mk {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] {v : ι → E} (hon : Orthonormal 𝕜 v) (hsp : (Submodule.span 𝕜 (Set.range v))ᗮ = ⊥) : ⇑(OrthonormalBasis.mkOfOrthogonalEqBot hon hsp) = v

def OrthonormalBasis.reindex {ι : Type u_1} {ι' : Type u_2} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [Fintype ι'] (b : OrthonormalBasis ι 𝕜 E) (e : ι ≃ ι') : OrthonormalBasis ι' 𝕜 E

b.reindex (e : ι ≃ ι') is an OrthonormalBasis indexed by ι'

Equations

• b.reindex e = { repr := b.repr.trans (LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e) }

theorem OrthonormalBasis.reindex_apply {ι : Type u_1} {ι' : Type u_2} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [Fintype ι'] (b : OrthonormalBasis ι 𝕜 E) (e : ι ≃ ι') (i' : ι') : (b.reindex e) i' = b (e.symm i')

@[simp]

theorem OrthonormalBasis.reindex_toBasis {ι : Type u_1} {ι' : Type u_2} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [Fintype ι'] (b : OrthonormalBasis ι 𝕜 E) (e : ι ≃ ι') : (b.reindex e).toBasis = b.toBasis.reindex e

@[simp]

theorem OrthonormalBasis.coe_reindex {ι : Type u_1} {ι' : Type u_2} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [Fintype ι'] (b : OrthonormalBasis ι 𝕜 E) (e : ι ≃ ι') : ⇑(b.reindex e) = ⇑b ∘ ⇑e.symm

@[simp]

theorem OrthonormalBasis.repr_reindex {ι : Type u_1} {ι' : Type u_2} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [Fintype ι'] (b : OrthonormalBasis ι 𝕜 E) (e : ι ≃ ι') (x : E) (i' : ι') : (b.reindex e).repr x i' = b.repr x (e.symm i')

noncomputable def EuclideanSpace.basisFun (ι : Type u_1) (𝕜 : Type u_3) [RCLike 𝕜] [Fintype ι] : OrthonormalBasis ι 𝕜 (EuclideanSpace 𝕜 ι)

The basis Pi.basisFun, bundled as an orthornormal basis of EuclideanSpace 𝕜 ι.

Equations

• EuclideanSpace.basisFun ι 𝕜 = { repr := LinearIsometryEquiv.refl 𝕜 (EuclideanSpace 𝕜 ι) }

@[simp]

theorem EuclideanSpace.basisFun_apply (ι : Type u_1) (𝕜 : Type u_3) [RCLike 𝕜] [Fintype ι] [DecidableEq ι] (i : ι) : (basisFun ι 𝕜) i = single i 1

@[simp]

theorem EuclideanSpace.basisFun_repr (ι : Type u_1) (𝕜 : Type u_3) [RCLike 𝕜] [Fintype ι] (x : EuclideanSpace 𝕜 ι) (i : ι) : (basisFun ι 𝕜).repr x i = x i

theorem EuclideanSpace.basisFun_toBasis (ι : Type u_1) (𝕜 : Type u_3) [RCLike 𝕜] [Fintype ι] : (basisFun ι 𝕜).toBasis = PiLp.basisFun 2 𝕜 ι

instance OrthonormalBasis.instInhabited {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] [Fintype ι] : Inhabited (OrthonormalBasis ι 𝕜 (EuclideanSpace 𝕜 ι))

Equations

• OrthonormalBasis.instInhabited = { default := EuclideanSpace.basisFun ι 𝕜 }

def Complex.orthonormalBasisOneI : OrthonormalBasis (Fin 2) ℝ ℂ

![1, I] is an orthonormal basis for ℂ considered as a real inner product space.

Equations

• Complex.orthonormalBasisOneI = Complex.basisOneI.toOrthonormalBasis Complex.orthonormalBasisOneI._proof_23

@[simp]

theorem Complex.orthonormalBasisOneI_repr_apply (z : ℂ) : orthonormalBasisOneI.repr z = ![z.re, z.im]

@[simp]

theorem Complex.orthonormalBasisOneI_repr_symm_apply (x : EuclideanSpace ℝ (Fin 2)) : orthonormalBasisOneI.repr.symm x = ↑(x 0) + ↑(x 1) * I

@[simp]

theorem Complex.toBasis_orthonormalBasisOneI : orthonormalBasisOneI.toBasis = basisOneI

@[simp]

theorem Complex.coe_orthonormalBasisOneI : ⇑orthonormalBasisOneI = ![1, I]

def Complex.isometryOfOrthonormal {F : Type u_5} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (v : OrthonormalBasis (Fin 2) ℝ F) : ℂ ≃ₗᵢ[ℝ] F

The isometry between ℂ and a two-dimensional real inner product space given by a basis.

Equations

• Complex.isometryOfOrthonormal v = Complex.orthonormalBasisOneI.repr.trans v.repr.symm

@[simp]

theorem Complex.map_isometryOfOrthonormal {F : Type u_5} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {F' : Type u_6} [NormedAddCommGroup F'] [InnerProductSpace ℝ F'] (v : OrthonormalBasis (Fin 2) ℝ F) (f : F ≃ₗᵢ[ℝ] F') : isometryOfOrthonormal (v.map f) = (isometryOfOrthonormal v).trans f

theorem Complex.isometryOfOrthonormal_symm_apply {F : Type u_5} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (v : OrthonormalBasis (Fin 2) ℝ F) (f : F) : (isometryOfOrthonormal v).symm f = ↑((v.toBasis.coord 0) f) + ↑((v.toBasis.coord 1) f) * I

theorem Complex.isometryOfOrthonormal_apply {F : Type u_5} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (v : OrthonormalBasis (Fin 2) ℝ F) (z : ℂ) : (isometryOfOrthonormal v) z = z.re • v 0 + z.im • v 1

Matrix representation of an orthonormal basis with respect to another

@[simp]

theorem OrthonormalBasis.toMatrix_orthonormalBasis_conjTranspose_mul_self {ι : Type u_1} {ι' : Type u_2} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [DecidableEq ι] [Fintype ι'] (a : OrthonormalBasis ι' 𝕜 E) (b : OrthonormalBasis ι 𝕜 E) : (a.toBasis.toMatrix ⇑b).conjTranspose * a.toBasis.toMatrix ⇑b = 1

A version of OrthonormalBasis.toMatrix_orthonormalBasis_mem_unitary that works for bases with different index types.

@[simp]

theorem OrthonormalBasis.toMatrix_orthonormalBasis_self_mul_conjTranspose {ι : Type u_1} {ι' : Type u_2} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [DecidableEq ι] [Fintype ι'] (a : OrthonormalBasis ι 𝕜 E) (b : OrthonormalBasis ι' 𝕜 E) : a.toBasis.toMatrix ⇑b * (a.toBasis.toMatrix ⇑b).conjTranspose = 1

A version of OrthonormalBasis.toMatrix_orthonormalBasis_mem_unitary that works for bases with different index types.

theorem OrthonormalBasis.toMatrix_orthonormalBasis_mem_unitary {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [DecidableEq ι] (a b : OrthonormalBasis ι 𝕜 E) : a.toBasis.toMatrix ⇑b ∈ Matrix.unitaryGroup ι 𝕜

The change-of-basis matrix between two orthonormal bases a, b is a unitary matrix.

@[simp]

theorem OrthonormalBasis.det_to_matrix_orthonormalBasis {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [DecidableEq ι] (a b : OrthonormalBasis ι 𝕜 E) : ‖a.toBasis.det ⇑b‖ = 1

The determinant of the change-of-basis matrix between two orthonormal bases a, b has unit length.

theorem OrthonormalBasis.toMatrix_orthonormalBasis_mem_orthogonal {ι : Type u_1} {F : Type u_5} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [Fintype ι] [DecidableEq ι] (a b : OrthonormalBasis ι ℝ F) : a.toBasis.toMatrix ⇑b ∈ Matrix.orthogonalGroup ι ℝ

The change-of-basis matrix between two orthonormal bases a, b is an orthogonal matrix.

theorem OrthonormalBasis.det_to_matrix_orthonormalBasis_real {ι : Type u_1} {F : Type u_5} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [Fintype ι] [DecidableEq ι] (a b : OrthonormalBasis ι ℝ F) : a.toBasis.det ⇑b = 1 ∨ a.toBasis.det ⇑b = -1

The determinant of the change-of-basis matrix between two orthonormal bases a, b is ±1.

Existence of orthonormal basis, etc.

noncomputable def DirectSum.IsInternal.collectedOrthonormalBasis {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] {A : ι → Submodule 𝕜 E} (hV : OrthogonalFamily 𝕜 (fun (i : ι) => ↥(A i)) fun (i : ι) => (A i).subtypeₗᵢ) [DecidableEq ι] (hV_sum : IsInternal fun (i : ι) => A i) {α : ι → Type u_7} [(i : ι) → Fintype (α i)] (v_family : (i : ι) → OrthonormalBasis (α i) 𝕜 ↥(A i)) : OrthonormalBasis ((i : ι) × α i) 𝕜 E

Given an internal direct sum decomposition of a module M, and an orthonormal basis for each of the components of the direct sum, the disjoint union of these orthonormal bases is an orthonormal basis for M.

Equations

• DirectSum.IsInternal.collectedOrthonormalBasis hV hV_sum v_family = (hV_sum.collectedBasis fun (i : ι) => (v_family i).toBasis).toOrthonormalBasis ⋯

theorem DirectSum.IsInternal.collectedOrthonormalBasis_mem {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] {A : ι → Submodule 𝕜 E} [DecidableEq ι] (h : IsInternal A) {α : ι → Type u_7} [(i : ι) → Fintype (α i)] (hV : OrthogonalFamily 𝕜 (fun (i : ι) => ↥(A i)) fun (i : ι) => (A i).subtypeₗᵢ) (v : (i : ι) → OrthonormalBasis (α i) 𝕜 ↥(A i)) (a : (i : ι) × α i) : (collectedOrthonormalBasis hV h v) a ∈ A a.fst

theorem Orthonormal.exists_orthonormalBasis_extension {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {v : Set E} [FiniteDimensional 𝕜 E] (hv : Orthonormal 𝕜 Subtype.val) : ∃ (u : Finset E) (b : OrthonormalBasis { x : E // x ∈ u } 𝕜 E), v ⊆ ↑u ∧ ⇑b = Subtype.val

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

theorem Orthonormal.exists_orthonormalBasis_extension_of_card_eq {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {ι : Type u_7} [Fintype ι] (card_ι : Module.finrank 𝕜 E = Fintype.card ι) {v : ι → E} {s : Set ι} (hv : Orthonormal 𝕜 (s.restrict v)) : ∃ (b : OrthonormalBasis ι 𝕜 E), ∀ i ∈ s, b i = v i

theorem exists_orthonormalBasis (𝕜 : Type u_3) [RCLike 𝕜] (E : Type u_4) [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] : ∃ (w : Finset E) (b : OrthonormalBasis { x : E // x ∈ w } 𝕜 E), ⇑b = Subtype.val

A finite-dimensional inner product space admits an orthonormal basis.

@[irreducible]

def stdOrthonormalBasis (𝕜 : Type u_7) [RCLike 𝕜] (E : Type u_8) [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] : OrthonormalBasis (Fin (Module.finrank 𝕜 E)) 𝕜 E

A finite-dimensional InnerProductSpace has an orthonormal basis.

Equations

• stdOrthonormalBasis 𝕜 E = let b := Classical.choose ⋯; ⋯.mpr (b.reindex (Fintype.equivFinOfCardEq ⋯))

theorem stdOrthonormalBasis_def (𝕜 : Type u_7) [RCLike 𝕜] (E : Type u_8) [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] : stdOrthonormalBasis 𝕜 E = let b := Classical.choose ⋯; ⋯.mpr (b.reindex (Fintype.equivFinOfCardEq ⋯))

theorem orthonormalBasis_one_dim {ι : Type u_1} [Fintype ι] (b : OrthonormalBasis ι ℝ ℝ) : (⇑b = fun (x : ι) => 1) ∨ ⇑b = fun (x : ι) => -1

An orthonormal basis of ℝ is made either of the vector 1, or of the vector -1.

theorem DirectSum.IsInternal.sigmaOrthonormalBasisIndexEquiv_def {ι : Type u_7} {𝕜 : Type u_8} [RCLike 𝕜] {E : Type u_9} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [FiniteDimensional 𝕜 E] {n : ℕ} (hn : Module.finrank 𝕜 E = n) [DecidableEq ι] {V : ι → Submodule 𝕜 E} (hV : IsInternal V) (hV' : OrthogonalFamily 𝕜 (fun (i : ι) => ↥(V i)) fun (i : ι) => (V i).subtypeₗᵢ) : sigmaOrthonormalBasisIndexEquiv hn hV hV' = let b := collectedOrthonormalBasis hV' hV fun (i : ι) => stdOrthonormalBasis 𝕜 ↥(V i); Fintype.equivFinOfCardEq ⋯

@[irreducible]

def DirectSum.IsInternal.sigmaOrthonormalBasisIndexEquiv {ι : Type u_7} {𝕜 : Type u_8} [RCLike 𝕜] {E : Type u_9} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [FiniteDimensional 𝕜 E] {n : ℕ} (hn : Module.finrank 𝕜 E = n) [DecidableEq ι] {V : ι → Submodule 𝕜 E} (hV : IsInternal V) (hV' : OrthogonalFamily 𝕜 (fun (i : ι) => ↥(V i)) fun (i : ι) => (V i).subtypeₗᵢ) : (i : ι) × Fin (Module.finrank 𝕜 ↥(V i)) ≃ Fin n

Exhibit a bijection between Fin n and the index set of a certain basis of an n-dimensional inner product space E. This should not be accessed directly, but only via the subsequent API.

Equations

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

@[irreducible]

def DirectSum.IsInternal.subordinateOrthonormalBasis {ι : Type u_7} {𝕜 : Type u_8} [RCLike 𝕜] {E : Type u_9} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [FiniteDimensional 𝕜 E] {n : ℕ} (hn : Module.finrank 𝕜 E = n) [DecidableEq ι] {V : ι → Submodule 𝕜 E} (hV : IsInternal V) (hV' : OrthogonalFamily 𝕜 (fun (i : ι) => ↥(V i)) fun (i : ι) => (V i).subtypeₗᵢ) : OrthonormalBasis (Fin n) 𝕜 E

An n-dimensional InnerProductSpace equipped with a decomposition as an internal direct sum has an orthonormal basis indexed by Fin n and subordinate to that direct sum.

Equations

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

theorem DirectSum.IsInternal.subordinateOrthonormalBasis_def {ι : Type u_7} {𝕜 : Type u_8} [RCLike 𝕜] {E : Type u_9} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [FiniteDimensional 𝕜 E] {n : ℕ} (hn : Module.finrank 𝕜 E = n) [DecidableEq ι] {V : ι → Submodule 𝕜 E} (hV : IsInternal V) (hV' : OrthogonalFamily 𝕜 (fun (i : ι) => ↥(V i)) fun (i : ι) => (V i).subtypeₗᵢ) : subordinateOrthonormalBasis hn hV hV' = (collectedOrthonormalBasis hV' hV fun (i : ι) => stdOrthonormalBasis 𝕜 ↥(V i)).reindex (sigmaOrthonormalBasisIndexEquiv hn hV hV')

@[irreducible]

def DirectSum.IsInternal.subordinateOrthonormalBasisIndex {ι : Type u_7} {𝕜 : Type u_8} [RCLike 𝕜] {E : Type u_9} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [FiniteDimensional 𝕜 E] {n : ℕ} (hn : Module.finrank 𝕜 E = n) [DecidableEq ι] {V : ι → Submodule 𝕜 E} (hV : IsInternal V) (a : Fin n) (hV' : OrthogonalFamily 𝕜 (fun (i : ι) => ↥(V i)) fun (i : ι) => (V i).subtypeₗᵢ) : ι

An n-dimensional InnerProductSpace equipped with a decomposition as an internal direct sum has an orthonormal basis indexed by Fin n and subordinate to that direct sum. This function provides the mapping by which it is subordinate.

Equations

• DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn hV a hV' = ((DirectSum.IsInternal.sigmaOrthonormalBasisIndexEquiv hn hV hV').symm a).fst

theorem DirectSum.IsInternal.subordinateOrthonormalBasisIndex_def {ι : Type u_7} {𝕜 : Type u_8} [RCLike 𝕜] {E : Type u_9} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [FiniteDimensional 𝕜 E] {n : ℕ} (hn : Module.finrank 𝕜 E = n) [DecidableEq ι] {V : ι → Submodule 𝕜 E} (hV : IsInternal V) (a : Fin n) (hV' : OrthogonalFamily 𝕜 (fun (i : ι) => ↥(V i)) fun (i : ι) => (V i).subtypeₗᵢ) : subordinateOrthonormalBasisIndex hn hV a hV' = ((sigmaOrthonormalBasisIndexEquiv hn hV hV').symm a).fst

theorem DirectSum.IsInternal.subordinateOrthonormalBasis_subordinate {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [FiniteDimensional 𝕜 E] {n : ℕ} (hn : Module.finrank 𝕜 E = n) [DecidableEq ι] {V : ι → Submodule 𝕜 E} (hV : IsInternal V) (a : Fin n) (hV' : OrthogonalFamily 𝕜 (fun (i : ι) => ↥(V i)) fun (i : ι) => (V i).subtypeₗᵢ) : (subordinateOrthonormalBasis hn hV hV') a ∈ V (subordinateOrthonormalBasisIndex hn hV a hV')

The basis constructed in DirectSum.IsInternal.subordinateOrthonormalBasis is subordinate to the OrthogonalFamily in question.

def OrthonormalBasis.fromOrthogonalSpanSingleton {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (n : ℕ) [Fact (Module.finrank 𝕜 E = n + 1)] {v : E} (hv : v ≠ 0) : OrthonormalBasis (Fin n) 𝕜 ↥(Submodule.span 𝕜 {v})ᗮ

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

Equations

• OrthonormalBasis.fromOrthogonalSpanSingleton n hv = (stdOrthonormalBasis 𝕜 ↥(Submodule.span 𝕜 {v})ᗮ).reindex (finCongr ⋯)

noncomputable def LinearIsometry.extend {𝕜 : Type u_3} [RCLike 𝕜] {V : Type u_7} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [FiniteDimensional 𝕜 V] {S : Submodule 𝕜 V} (L : ↥S →ₗᵢ[𝕜] V) : V →ₗᵢ[𝕜] V

Let S be a subspace of a finite-dimensional complex inner product space V. A linear isometry mapping S into V can be extended to a full isometry of V.

TODO: The case when S is a finite-dimensional subspace of an infinite-dimensional V.

Equations

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

theorem LinearIsometry.extend_apply {𝕜 : Type u_3} [RCLike 𝕜] {V : Type u_7} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [FiniteDimensional 𝕜 V] {S : Submodule 𝕜 V} (L : ↥S →ₗᵢ[𝕜] V) (s : ↥S) : L.extend ↑s = L s

def Matrix.toEuclideanLin {𝕜 : Type u_3} [RCLike 𝕜] {m : Type u_7} {n : Type u_8} [Fintype n] [DecidableEq n] : Matrix m n 𝕜 ≃ₗ[𝕜] EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 m

Matrix.toLin' adapted for EuclideanSpace 𝕜 _.

Equations

• Matrix.toEuclideanLin = Matrix.toLin'.trans ((WithLp.linearEquiv 2 𝕜 (n → 𝕜)).symm.arrowCongr (WithLp.linearEquiv 2 𝕜 (m → 𝕜)).symm)

@[simp]

theorem Matrix.toEuclideanLin_piLp_equiv_symm {𝕜 : Type u_3} [RCLike 𝕜] {m : Type u_7} {n : Type u_8} [Fintype n] [DecidableEq n] (A : Matrix m n 𝕜) (x : n → 𝕜) : (toEuclideanLin A) ((WithLp.equiv 2 ((i : n) → (fun (x : n) => 𝕜) i)).symm x) = (WithLp.equiv 2 (m → 𝕜)).symm ((toLin' A) x)

@[simp]

theorem Matrix.piLp_equiv_toEuclideanLin {𝕜 : Type u_3} [RCLike 𝕜] {m : Type u_7} {n : Type u_8} [Fintype n] [DecidableEq n] (A : Matrix m n 𝕜) (x : EuclideanSpace 𝕜 n) : (WithLp.equiv 2 ((i : m) → (fun (x : m) => 𝕜) i)) ((toEuclideanLin A) x) = (toLin' A) ((WithLp.equiv 2 (n → 𝕜)) x)

theorem Matrix.toEuclideanLin_apply {𝕜 : Type u_3} [RCLike 𝕜] {m : Type u_7} {n : Type u_8} [Fintype n] [DecidableEq n] (M : Matrix m n 𝕜) (v : EuclideanSpace 𝕜 n) : (toEuclideanLin M) v = (WithLp.equiv 2 (m → 𝕜)).symm (M.mulVec ((WithLp.equiv 2 (n → 𝕜)) v))

@[simp]

theorem Matrix.piLp_equiv_toEuclideanLin_apply {𝕜 : Type u_3} [RCLike 𝕜] {m : Type u_7} {n : Type u_8} [Fintype n] [DecidableEq n] (M : Matrix m n 𝕜) (v : EuclideanSpace 𝕜 n) : (WithLp.equiv 2 (m → 𝕜)) ((toEuclideanLin M) v) = M.mulVec ((WithLp.equiv 2 (n → 𝕜)) v)

@[simp]

theorem Matrix.toEuclideanLin_apply_piLp_equiv_symm {𝕜 : Type u_3} [RCLike 𝕜] {m : Type u_7} {n : Type u_8} [Fintype n] [DecidableEq n] (M : Matrix m n 𝕜) (v : n → 𝕜) : (toEuclideanLin M) ((WithLp.equiv 2 (n → 𝕜)).symm v) = (WithLp.equiv 2 (m → 𝕜)).symm (M.mulVec v)

theorem Matrix.toEuclideanLin_eq_toLin {𝕜 : Type u_3} [RCLike 𝕜] {m : Type u_7} {n : Type u_8} [Fintype n] [DecidableEq n] [Finite m] : toEuclideanLin = toLin (PiLp.basisFun 2 𝕜 n) (PiLp.basisFun 2 𝕜 m)

theorem Matrix.toEuclideanLin_eq_toLin_orthonormal {𝕜 : Type u_3} [RCLike 𝕜] {m : Type u_7} {n : Type u_8} [Fintype n] [DecidableEq n] [Fintype m] : toEuclideanLin = toLin (EuclideanSpace.basisFun n 𝕜).toBasis (EuclideanSpace.basisFun m 𝕜).toBasis

theorem inner_matrix_row_row {𝕜 : Type u_3} [RCLike 𝕜] {m : Type u_7} {n : Type u_8} [Fintype n] (A B : Matrix m n 𝕜) (i j : m) : inner 𝕜 ((WithLp.equiv 2 (n → 𝕜)).symm (A i)) ((WithLp.equiv 2 (n → 𝕜)).symm (B j)) = (B * A.conjTranspose) j i

The inner product of a row of A and a row of B is an entry of B * Aᴴ.

theorem inner_matrix_col_col {𝕜 : Type u_3} [RCLike 𝕜] {m : Type u_7} {n : Type u_8} [Fintype m] (A B : Matrix m n 𝕜) (i j : n) : inner 𝕜 ((WithLp.equiv 2 (m → 𝕜)).symm (A.transpose i)) ((WithLp.equiv 2 (m → 𝕜)).symm (B.transpose j)) = (A.conjTranspose * B) i j

The inner product of a column of A and a column of B is an entry of Aᴴ * B.