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

• 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} [IsROrC 𝕜] {ι : Type u_8} [Fintype ι] (f : ι → Type u_9) [(i : ι) → NormedAddCommGroup (f i)] [(i : ι) → InnerProductSpace 𝕜 (f i)] : InnerProductSpace 𝕜 (PiLp 2 f)

@[simp]

theorem PiLp.inner_apply {𝕜 : Type u_3} [IsROrC 𝕜] {ι : Type u_8} [Fintype ι] {f : ι → Type u_9} [(i : ι) → NormedAddCommGroup (f i)] [(i : ι) → InnerProductSpace 𝕜 (f i)] (x : PiLp 2 f) (y : PiLp 2 f) : inner x y = Finset.sum Finset.univ fun i => inner (x i) (y i)

@[reducible]

def EuclideanSpace (𝕜 : Type u_8) [IsROrC 𝕜] (n : Type u_9) [Fintype n] : Type (max u_9 u_8)

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

theorem EuclideanSpace.nnnorm_eq {𝕜 : Type u_8} [IsROrC 𝕜] {n : Type u_9} [Fintype n] (x : EuclideanSpace 𝕜 n) : ‖x‖₊ = ↑NNReal.sqrt (Finset.sum Finset.univ fun i => ‖x i‖₊ ^ 2)

theorem EuclideanSpace.norm_eq {𝕜 : Type u_8} [IsROrC 𝕜] {n : Type u_9} [Fintype n] (x : EuclideanSpace 𝕜 n) : ‖x‖ = Real.sqrt (Finset.sum Finset.univ fun i => ‖x i‖ ^ 2)

theorem EuclideanSpace.dist_eq {𝕜 : Type u_8} [IsROrC 𝕜] {n : Type u_9} [Fintype n] (x : EuclideanSpace 𝕜 n) (y : EuclideanSpace 𝕜 n) : dist x y = Real.sqrt (Finset.sum Finset.univ fun i => dist (x i) (y i) ^ 2)

theorem EuclideanSpace.nndist_eq {𝕜 : Type u_8} [IsROrC 𝕜] {n : Type u_9} [Fintype n] (x : EuclideanSpace 𝕜 n) (y : EuclideanSpace 𝕜 n) : nndist x y = ↑NNReal.sqrt (Finset.sum Finset.univ fun i => nndist (x i) (y i) ^ 2)

theorem EuclideanSpace.edist_eq {𝕜 : Type u_8} [IsROrC 𝕜] {n : Type u_9} [Fintype n] (x : EuclideanSpace 𝕜 n) (y : EuclideanSpace 𝕜 n) : edist x y = (Finset.sum Finset.univ fun i => edist (x i) (y i) ^ 2) ^ (1 / 2)

instance EuclideanSpace.instFiniteDimensional {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] [Fintype ι] : FiniteDimensional 𝕜 (EuclideanSpace 𝕜 ι)

instance EuclideanSpace.instInnerProductSpace {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] [Fintype ι] : InnerProductSpace 𝕜 (EuclideanSpace 𝕜 ι)

@[simp]

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

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

theorem EuclideanSpace.inner_eq_star_dotProduct {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] [Fintype ι] (x : EuclideanSpace 𝕜 ι) (y : EuclideanSpace 𝕜 ι) : inner x y = Matrix.dotProduct (star (↑(WithLp.equiv 2 ((i : ι) → (fun x => 𝕜) i)) x)) (↑(WithLp.equiv 2 ((i : ι) → (fun x => 𝕜) i)) y)

theorem EuclideanSpace.inner_piLp_equiv_symm {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] [Fintype ι] (x : ι → 𝕜) (y : ι → 𝕜) : inner (↑(WithLp.equiv 2 (ι → 𝕜)).symm x) (↑(WithLp.equiv 2 (ι → 𝕜)).symm y) = Matrix.dotProduct (star x) y

def DirectSum.IsInternal.isometryL2OfOrthogonalFamily {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [DecidableEq ι] {V : ι → Submodule 𝕜 E} (hV : DirectSum.IsInternal V) (hV' : OrthogonalFamily 𝕜 (fun i => { x // x ∈ V i }) fun i => Submodule.subtypeₗᵢ (V i)) : E ≃ₗᵢ[𝕜] PiLp 2 fun i => { x // x ∈ 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.

@[simp]

theorem DirectSum.IsInternal.isometryL2OfOrthogonalFamily_symm_apply {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [DecidableEq ι] {V : ι → Submodule 𝕜 E} (hV : DirectSum.IsInternal V) (hV' : OrthogonalFamily 𝕜 (fun i => { x // x ∈ V i }) fun i => Submodule.subtypeₗᵢ (V i)) (w : PiLp 2 fun i => { x // x ∈ V i }) : ↑(LinearIsometryEquiv.symm (DirectSum.IsInternal.isometryL2OfOrthogonalFamily hV hV')) w = Finset.sum Finset.univ fun i => ↑(w i)

@[inline, reducible]

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

A shorthand for PiLp.continuousLinearEquiv.

@[simp]

theorem EuclideanSpace.projₗ_apply {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] [Fintype ι] (i : ι) : ∀ (a : WithLp 2 (ι → 𝕜)), ↑(EuclideanSpace.projₗ i) a = a i

def EuclideanSpace.projₗ {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] [Fintype ι] (i : ι) : EuclideanSpace 𝕜 ι →ₗ[𝕜] 𝕜

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

@[simp]

theorem EuclideanSpace.proj_apply {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] [Fintype ι] (i : ι) : ∀ (a : WithLp 2 (ι → 𝕜)), ↑(EuclideanSpace.proj i) a = a i

@[simp]

theorem EuclideanSpace.proj_coe {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] [Fintype ι] (i : ι) : ↑(EuclideanSpace.proj i) = EuclideanSpace.projₗ i

def EuclideanSpace.proj {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] [Fintype ι] (i : ι) : EuclideanSpace 𝕜 ι →L[𝕜] 𝕜

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

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

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

@[simp]

theorem WithLp.equiv_single {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] [Fintype ι] [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} [IsROrC 𝕜] [Fintype ι] [DecidableEq ι] (i : ι) (a : 𝕜) : ↑(WithLp.equiv 2 ((j : ι) → (fun x => 𝕜) j)).symm (Pi.single i a) = EuclideanSpace.single i a

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

EuclideanSpace.single forms an orthonormal family.

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

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

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

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

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

instance OrthonormalBasis.instFunLike {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] : FunLike (OrthonormalBasis ι 𝕜 E) ι fun x => E

b i is the ith basis vector.

@[simp]

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

@[simp]

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

@[simp]

theorem OrthonormalBasis.repr_self {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] {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} [IsROrC 𝕜] {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} [IsROrC 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) : Orthonormal 𝕜 ↑b

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

The Basis ι 𝕜 E underlying the OrthonormalBasis

@[simp]

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

@[simp]

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

@[simp]

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

theorem OrthonormalBasis.sum_repr {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (x : E) : (Finset.sum Finset.univ fun i => ↑b.repr x i • ↑b i) = x

theorem OrthonormalBasis.sum_repr_symm {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (v : EuclideanSpace 𝕜 ι) : (Finset.sum Finset.univ fun i => v i • ↑b i) = ↑(LinearIsometryEquiv.symm b.repr) v

theorem OrthonormalBasis.sum_inner_mul_inner {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (x : E) (y : E) : (Finset.sum Finset.univ fun i => inner x (↑b i) * inner (↑b i) y) = inner x y

theorem OrthonormalBasis.orthogonalProjection_eq_sum {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] {U : Submodule 𝕜 E} [CompleteSpace { x // x ∈ U }] (b : OrthonormalBasis ι 𝕜 { x // x ∈ U }) (x : E) : ↑(orthogonalProjection U) x = Finset.sum Finset.univ fun i => inner (↑(↑b i)) x • ↑b i

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

Mapping an orthonormal basis along a LinearIsometryEquiv.

@[simp]

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

@[simp]

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

def Basis.toOrthonormalBasis {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] {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.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def OrthonormalBasis.mk {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] {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

@[simp]

theorem OrthonormalBasis.coe_mk {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] {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} [IsROrC 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [DecidableEq E] {v' : ι' → E} (h : Orthonormal 𝕜 v') (s : Finset ι') : OrthonormalBasis { x // x ∈ s } 𝕜 { x // x ∈ Submodule.span 𝕜 ↑(Finset.image v' s) }

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

@[simp]

theorem OrthonormalBasis.span_apply {ι' : Type u_2} {𝕜 : Type u_3} [IsROrC 𝕜] {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} [IsROrC 𝕜] {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.

@[simp]

theorem OrthonormalBasis.coe_of_orthogonal_eq_bot_mk {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] {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} [IsROrC 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [Fintype ι'] (b : OrthonormalBasis ι 𝕜 E) (e : ι ≃ ι') : OrthonormalBasis ι' 𝕜 E

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

theorem Complex.toBasis_orthonormalBasisOneI : OrthonormalBasis.toBasis Complex.orthonormalBasisOneI = Complex.basisOneI

@[simp]

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

def Complex.isometryOfOrthonormal {F : Type u_6} [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.

@[simp]

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

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

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

Matrix representation of an orthonormal basis with respect to another

theorem OrthonormalBasis.toMatrix_orthonormalBasis_mem_unitary {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [DecidableEq ι] (a : OrthonormalBasis ι 𝕜 E) (b : OrthonormalBasis ι 𝕜 E) : Basis.toMatrix (OrthonormalBasis.toBasis a) ↑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} [IsROrC 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [DecidableEq ι] (a : OrthonormalBasis ι 𝕜 E) (b : OrthonormalBasis ι 𝕜 E) : ‖↑(Basis.det (OrthonormalBasis.toBasis a)) ↑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_6} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [Fintype ι] [DecidableEq ι] (a : OrthonormalBasis ι ℝ F) (b : OrthonormalBasis ι ℝ F) : Basis.toMatrix (OrthonormalBasis.toBasis a) ↑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_6} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [Fintype ι] [DecidableEq ι] (a : OrthonormalBasis ι ℝ F) (b : OrthonormalBasis ι ℝ F) : ↑(Basis.det (OrthonormalBasis.toBasis a)) ↑b = 1 ∨ ↑(Basis.det (OrthonormalBasis.toBasis a)) ↑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} [IsROrC 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] {A : ι → Submodule 𝕜 E} (hV : OrthogonalFamily 𝕜 (fun i => { x // x ∈ A i }) fun i => Submodule.subtypeₗᵢ (A i)) [DecidableEq ι] (hV_sum : DirectSum.IsInternal fun i => A i) {α : ι → Type u_8} [(i : ι) → Fintype (α i)] (v_family : (i : ι) → OrthonormalBasis (α i) 𝕜 { x // x ∈ 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.

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

theorem Orthonormal.exists_orthonormalBasis_extension {𝕜 : Type u_3} [IsROrC 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {v : Set E} [FiniteDimensional 𝕜 E] (hv : Orthonormal 𝕜 Subtype.val) : ∃ u b, 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} [IsROrC 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {ι : Type u_8} [Fintype ι] (card_ι : FiniteDimensional.finrank 𝕜 E = Fintype.card ι) {v : ι → E} {s : Set ι} (hv : Orthonormal 𝕜 (Set.restrict s v)) : ∃ b, ∀ (i : ι), i ∈ s → ↑b i = v i

theorem exists_orthonormalBasis (𝕜 : Type u_3) [IsROrC 𝕜] (E : Type u_4) [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] : ∃ w b, ↑b = Subtype.val

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

@[irreducible]

def stdOrthonormalBasis (𝕜 : Type u_8) [IsROrC 𝕜] (E : Type u_9) [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] : OrthonormalBasis (Fin (FiniteDimensional.finrank 𝕜 E)) 𝕜 E

A finite-dimensional InnerProductSpace has an orthonormal basis.

theorem stdOrthonormalBasis_def (𝕜 : Type u_8) [IsROrC 𝕜] (E : Type u_9) [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] : stdOrthonormalBasis 𝕜 E = let b := Classical.choose (_ : ∃ b, ↑b = Subtype.val); Eq.mpr (_ : OrthonormalBasis (Fin (FiniteDimensional.finrank 𝕜 E)) 𝕜 E = OrthonormalBasis (Fin (Fintype.card { x // x ∈ Classical.choose (_ : ∃ w b, ↑b = Subtype.val) })) 𝕜 E) (OrthonormalBasis.reindex b (Fintype.equivFinOfCardEq (_ : Fintype.card { x // x ∈ Classical.choose (_ : ∃ w b, ↑b = Subtype.val) } = Fintype.card { x // x ∈ Classical.choose (_ : ∃ w b, ↑b = Subtype.val) })))

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_8} {𝕜 : Type u_9} [IsROrC 𝕜] {E : Type u_10} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [FiniteDimensional 𝕜 E] {n : ℕ} (hn : FiniteDimensional.finrank 𝕜 E = n) [DecidableEq ι] {V : ι → Submodule 𝕜 E} (hV : DirectSum.IsInternal V) (hV' : OrthogonalFamily 𝕜 (fun i => { x // x ∈ V i }) fun i => Submodule.subtypeₗᵢ (V i)) : DirectSum.IsInternal.sigmaOrthonormalBasisIndexEquiv hn hV hV' = let b := DirectSum.IsInternal.collectedOrthonormalBasis hV' hV fun i => stdOrthonormalBasis 𝕜 { x // x ∈ V i }; Fintype.equivFinOfCardEq (_ : Fintype.card ((i : ι) × Fin (FiniteDimensional.finrank 𝕜 { x // x ∈ V i })) = n)

@[irreducible]

def DirectSum.IsInternal.sigmaOrthonormalBasisIndexEquiv {ι : Type u_8} {𝕜 : Type u_9} [IsROrC 𝕜] {E : Type u_10} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [FiniteDimensional 𝕜 E] {n : ℕ} (hn : FiniteDimensional.finrank 𝕜 E = n) [DecidableEq ι] {V : ι → Submodule 𝕜 E} (hV : DirectSum.IsInternal V) (hV' : OrthogonalFamily 𝕜 (fun i => { x // x ∈ V i }) fun i => Submodule.subtypeₗᵢ (V i)) : (i : ι) × Fin (FiniteDimensional.finrank 𝕜 { x // x ∈ 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.

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

@[irreducible]

def DirectSum.IsInternal.subordinateOrthonormalBasis {ι : Type u_8} {𝕜 : Type u_9} [IsROrC 𝕜] {E : Type u_10} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [FiniteDimensional 𝕜 E] {n : ℕ} (hn : FiniteDimensional.finrank 𝕜 E = n) [DecidableEq ι] {V : ι → Submodule 𝕜 E} (hV : DirectSum.IsInternal V) (hV' : OrthogonalFamily 𝕜 (fun i => { x // x ∈ V i }) fun i => Submodule.subtypeₗᵢ (V i)) : 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.

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

@[irreducible]

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

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.

theorem DirectSum.IsInternal.subordinateOrthonormalBasis_subordinate {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [FiniteDimensional 𝕜 E] {n : ℕ} (hn : FiniteDimensional.finrank 𝕜 E = n) [DecidableEq ι] {V : ι → Submodule 𝕜 E} (hV : DirectSum.IsInternal V) (a : Fin n) (hV' : OrthogonalFamily 𝕜 (fun i => { x // x ∈ V i }) fun i => Submodule.subtypeₗᵢ (V i)) : ↑(DirectSum.IsInternal.subordinateOrthonormalBasis hn hV hV') a ∈ V (DirectSum.IsInternal.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} [IsROrC 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (n : ℕ) [Fact (FiniteDimensional.finrank 𝕜 E = n + 1)] {v : E} (hv : v ≠ 0) : OrthonormalBasis (Fin n) 𝕜 { x // x ∈ (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).

noncomputable def LinearIsometry.extend {𝕜 : Type u_3} [IsROrC 𝕜] {V : Type u_8} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [FiniteDimensional 𝕜 V] {S : Submodule 𝕜 V} (L : { x // x ∈ 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.

theorem LinearIsometry.extend_apply {𝕜 : Type u_3} [IsROrC 𝕜] {V : Type u_8} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [FiniteDimensional 𝕜 V] {S : Submodule 𝕜 V} (L : { x // x ∈ S } →ₗᵢ[𝕜] V) (s : { x // x ∈ S }) : ↑(LinearIsometry.extend L) ↑s = ↑L s

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

Matrix.toLin' adapted for EuclideanSpace 𝕜 _.

@[simp]

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

@[simp]

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

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

theorem inner_matrix_row_row {𝕜 : Type u_3} [IsROrC 𝕜] {m : Type u_8} {n : Type u_9} [Fintype n] (A : Matrix m n 𝕜) (B : Matrix m n 𝕜) (i : m) (j : m) : inner (↑(WithLp.equiv 2 (n → 𝕜)).symm (A i)) (↑(WithLp.equiv 2 (n → 𝕜)).symm (B j)) = (Matrix m n 𝕜 * Matrix n m 𝕜) (Matrix m m 𝕜) Matrix.instHMulMatrixMatrixMatrix B (Matrix.conjTranspose A) 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} [IsROrC 𝕜] {m : Type u_8} {n : Type u_9} [Fintype m] (A : Matrix m n 𝕜) (B : Matrix m n 𝕜) (i : n) (j : n) : inner (↑(WithLp.equiv 2 (m → 𝕜)).symm (Matrix.transpose A i)) (↑(WithLp.equiv 2 (m → 𝕜)).symm (Matrix.transpose B j)) = (Matrix n m 𝕜 * Matrix m n 𝕜) (Matrix n n 𝕜) Matrix.instHMulMatrixMatrixMatrix (Matrix.conjTranspose A) B i j

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