def Matrix.Isometry {d : Type u_1} {d₂ : Type u_2} {R : Type u_4} [Fintype d] [DecidableEq d₂] [CommRing R] [StarRing R] (A : Matrix d d₂ R) : Prop

An isometry is a matrix A such that AAᴴ = 1. Compare with a unitary, which requires AAᴴ = AᴴA = 1. It is common to claim that, in a finite-dimensional vector space, a two-sided isometry (A.Isometry ∧ Aᴴ.Isometry) must be square and therefore unitary; this is does not work out so well here, since a Matrix m n R can be a two-sided isometry, but cannot be a unitary since the rows and columns are index by different labels.

Equations

• A.Isometry = (A.conjTranspose * A = 1)

theorem Matrix.submatrix_one_isometry {d : Type u_1} {d₂ : Type u_2} {d₃ : Type u_3} {R : Type u_4} [Fintype d] [DecidableEq d] [Fintype d₂] [DecidableEq d₃] [CommRing R] [StarRing R] {e : d₂ → d} {f : d₃ → d} (he : Function.Bijective e) (hf : Function.Injective f) : (submatrix 1 e f).Isometry

theorem Matrix.submatrix_one_id_left_isometry {d : Type u_1} {d₂ : Type u_2} {R : Type u_4} [Fintype d] [DecidableEq d] [Fintype d₂] [CommRing R] [StarRing R] {e : d₂ → d} (he : Function.Bijective e) : (submatrix 1 e id).Isometry

theorem Matrix.submatrix_one_id_right_isometry {d : Type u_1} {d₂ : Type u_2} {R : Type u_4} [Fintype d] [DecidableEq d] [DecidableEq d₂] [CommRing R] [StarRing R] {e : d₂ → d} (he : Function.Injective e) : (submatrix 1 id e).Isometry

theorem Matrix.mem_unitaryGroup_iff_isometry {d : Type u_1} {R : Type u_4} [Fintype d] [DecidableEq d] [CommRing R] [StarRing R] (A : Matrix d d R) : A ∈ unitaryGroup d R ↔ A.Isometry ∧ A.conjTranspose.Isometry

theorem Equiv.Perm.permMatrix_mem_unitaryGroup {d : Type u_1} {R : Type u_4} [Fintype d] [DecidableEq d] [CommRing R] [StarRing R] (e : Perm d) : permMatrix R e ∈ Matrix.unitaryGroup d R

theorem Matrix.reindex_one_isometry {d : Type u_1} {d₂ : Type u_2} {d₃ : Type u_3} {R : Type u_4} [Fintype d] [DecidableEq d] [Fintype d₂] [DecidableEq d₃] [CommRing R] [StarRing R] (e : d ≃ d₂) (f : d ≃ d₃) : ((reindex e f) 1).Isometry

theorem Matrix.reindex_one_mem_unitaryGroup {d : Type u_1} {d₂ : Type u_2} {R : Type u_4} [DecidableEq d] [Fintype d₂] [DecidableEq d₂] [CommRing R] [StarRing R] (e : d ≃ d₂) : (reindex e e) 1 ∈ unitaryGroup d₂ R

theorem Matrix.reindex_eq_conj {d : Type u_1} {d₂ : Type u_2} {R : Type u_4} [Fintype d] [DecidableEq d] [CommRing R] (A : Matrix d d R) (e : d ≃ d₂) : (reindex e e) A = (reindex e (Equiv.refl d)) 1 * A * (reindex (Equiv.refl d) e) 1

theorem Matrix.reindex_eq_conj_unitaryGroup' {d : Type u_1} {R : Type u_4} [Fintype d] [DecidableEq d] [CommRing R] [StarRing R] (A : Matrix d d R) (e : Equiv.Perm d) : (reindex e e) A = ↑⟨Equiv.Perm.permMatrix R e⁻¹, ⋯⟩ * A * ↑⟨Equiv.Perm.permMatrix R e, ⋯⟩

theorem Matrix.IsHermitian.eigenvalue_ext {d : Type u_1} [Fintype d] [DecidableEq d] {𝕜 : Type u_5} [RCLike 𝕜] {A B : Matrix d d 𝕜} (hA : A.IsHermitian) (h : ∀ (v : d → 𝕜) (lam : 𝕜), A.mulVec v = lam • v → B.mulVec v = lam • v) : A = B

theorem Matrix.IsHermitian.cfc_eq_any_isometry {n : Type u_6} {m : Type u_7} {𝕜 : Type u_8} [RCLike 𝕜] [Fintype n] [DecidableEq n] [Fintype m] [DecidableEq m] {A : Matrix n n 𝕜} (hA : A.IsHermitian) {U : Matrix n m 𝕜} (hU₁ : U * U.conjTranspose = 1) (hU₂ : U.conjTranspose * U = 1) {D : m → ℝ} (hUD : A = U * diagonal (RCLike.ofReal ∘ D) * U.conjTranspose) (f : ℝ → ℝ) : hA.cfc f = U * diagonal (RCLike.ofReal ∘ f ∘ D) * U.conjTranspose

Generalizes Matrix.IsHermitian.cfc.eq_1, which gives a definition for the matrix CFC in terms of Matrix.IsHermitian.eigenvalues and Matrix.IsHermitian.eigenvectorUnitary, to show that the CFC works similarly for any diagonalization by a two-sided isometry.

theorem Matrix.IsHermitian.cfc_eq_any_unitary {n : Type u_6} {𝕜 : Type u_7} [RCLike 𝕜] [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.IsHermitian) {U : ↥(unitaryGroup n 𝕜)} {D : n → ℝ} (hUD : A = ↑U * diagonal (RCLike.ofReal ∘ D) * star ↑U) (f : ℝ → ℝ) : hA.cfc f = ↑U * diagonal (RCLike.ofReal ∘ f ∘ D) * star ↑U

Generalizes Matrix.IsHermitian.cfc.eq_1, which gives a definition for the matrix CFC in terms of Matrix.IsHermitian.eigenvalues and Matrix.IsHermitian.eigenvectorUnitary, to show that the CFC works similarly for any diagonalization.

theorem Matrix.cfc_conj_isometry {d : Type u_1} {d₂ : Type u_2} [Fintype d] [DecidableEq d] [Fintype d₂] [DecidableEq d₂] {𝕜 : Type u_5} [RCLike 𝕜] {A : Matrix d d 𝕜} (f : ℝ → ℝ) {u : Matrix d₂ d 𝕜} (hu₁ : u.Isometry) (hu₂ : u.conjTranspose.Isometry) : cfc f (u * A * u.conjTranspose) = u * cfc f A * u.conjTranspose

theorem Matrix.cfc_conj_unitary {d : Type u_1} [Fintype d] [DecidableEq d] {𝕜 : Type u_5} [RCLike 𝕜] {A : Matrix d d 𝕜} (f : ℝ → ℝ) (u : ↥(unitaryGroup d 𝕜)) : cfc f (↑u * A * ↑u⁻¹) = ↑u * cfc f A * ↑u⁻¹

theorem Matrix.cfc_conj_unitary' {d : Type u_1} [Fintype d] [DecidableEq d] {𝕜 : Type u_5} [RCLike 𝕜] {A : Matrix d d 𝕜} (f : ℝ → ℝ) (u : ↥(unitaryGroup d 𝕜)) : cfc f ((↑u).conjTranspose * A * ↑u) = (↑u).conjTranspose * cfc f A * ↑u

theorem Matrix.cfc_reindex {d : Type u_1} {d₂ : Type u_2} [Fintype d] [DecidableEq d] [Fintype d₂] [DecidableEq d₂] {𝕜 : Type u_5} [RCLike 𝕜] {A : Matrix d d 𝕜} (f : ℝ → ℝ) (e : d ≃ d₂) : cfc f ((reindex e e) A) = (reindex e e) (cfc f A)

theorem Matrix.commute_euclideanLin {d : Type u_1} [Fintype d] [DecidableEq d] {𝕜 : Type u_5} [RCLike 𝕜] {A B : Matrix d d 𝕜} (hAB : Commute A B) : Commute (toEuclideanLin A) (toEuclideanLin B)

theorem LinearMap.IsSymmetric.orthogonalFamily_eigenspace_inf_eigenspace' {𝕜 : Type u_6} {E : Type u_7} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A B : E →ₗ[𝕜] E} (hA : A.IsSymmetric) (hB : B.IsSymmetric) : OrthogonalFamily 𝕜 (fun (μ₁₂ : Module.End.Eigenvalues A × Module.End.Eigenvalues B) => ↥(Module.End.eigenspace A (↑A 1 μ₁₂.1) ⊓ Module.End.eigenspace B (↑B 1 μ₁₂.2))) fun (μ₁₂ : Module.End.Eigenvalues A × Module.End.Eigenvalues B) => (Module.End.eigenspace A (↑A 1 μ₁₂.1) ⊓ Module.End.eigenspace B (↑B 1 μ₁₂.2)).subtypeₗᵢ

Similar to LinearMap.IsSymmetric.orthogonalFamily_eigenspace_inf_eigenspace, but here the direct sum is indexed by only the pairs of eigenvalues, as opposed to all pairs of 𝕜 values, giving a finite decomposition.

theorem iSup_mono_bot {α : Type u_6} {ι : Sort u_7} {ι' : Sort u_8} [CompleteLattice α] {f : ι → α} {g : ι' → α} (h : ∀ (i : ι), f i = ⊥ ∨ ∃ (i' : ι'), f i ≤ g i') : iSup f ≤ iSup g

Variant of iSup_mono' that allows for an easier handling of bottom elements.

noncomputable def Commute.isSymmetric_directSumDecomposition {𝕜 : Type u_6} {E : Type u_7} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A B : E →ₗ[𝕜] E} [FiniteDimensional 𝕜 E] (hA : A.IsSymmetric) (hB : B.IsSymmetric) (hAB : Commute A B) : DirectSum.Decomposition fun (μ₁₂ : Module.End.Eigenvalues A × Module.End.Eigenvalues B) => Module.End.eigenspace A (↑A 1 μ₁₂.1) ⊓ Module.End.eigenspace B (↑B 1 μ₁₂.2)

Equations

• Commute.isSymmetric_directSumDecomposition hA hB hAB = ⋯.decomposition ⋯

theorem LinearMap.IsSymmetric.directSum_isInternal_of_commute' {𝕜 : Type u_6} {E : Type u_7} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A B : E →ₗ[𝕜] E} [FiniteDimensional 𝕜 E] (hA : A.IsSymmetric) (hB : B.IsSymmetric) (hAB : Commute A B) : DirectSum.IsInternal fun (μ₁₂ : Module.End.Eigenvalues A × Module.End.Eigenvalues B) => Module.End.eigenspace A (↑A 1 μ₁₂.1) ⊓ Module.End.eigenspace B (↑B 1 μ₁₂.2)

Similar to LinearMap.IsSymmetric.directSum_isInternal_of_commute, but here the direct sum is indexed by only the pairs of eigenvalues, as opposed to all pairs of 𝕜 values, giving a finite decomposition.

noncomputable def LinearMap.sharedEigenbasis {d : Type u_1} [Fintype d] {𝕜 : Type u_5} [RCLike 𝕜] {A B : EuclideanSpace 𝕜 d →ₗ[𝕜] EuclideanSpace 𝕜 d} (hA : A.IsSymmetric) (hB : B.IsSymmetric) (hAB : Commute A B) : OrthonormalBasis d 𝕜 (EuclideanSpace 𝕜 d)

Equations

• LinearMap.sharedEigenbasis hA hB hAB = (DirectSum.IsInternal.subordinateOrthonormalBasis ⋯ ⋯ ⋯).reindex (Fintype.equivOfCardEq ⋯)

noncomputable def LinearMap.sharedEigenvaluesA {d : Type u_1} [Fintype d] {𝕜 : Type u_5} [RCLike 𝕜] {A B : EuclideanSpace 𝕜 d →ₗ[𝕜] EuclideanSpace 𝕜 d} (hA : A.IsSymmetric) (hB : B.IsSymmetric) (hAB : Commute A B) : d → ℝ

Equations

• LinearMap.sharedEigenvaluesA hA hB hAB i = RCLike.re (inner 𝕜 ((LinearMap.sharedEigenbasis hA hB hAB) i) (A ((LinearMap.sharedEigenbasis hA hB hAB) i)))

noncomputable def LinearMap.sharedEigenvaluesB {d : Type u_1} [Fintype d] {𝕜 : Type u_5} [RCLike 𝕜] {A B : EuclideanSpace 𝕜 d →ₗ[𝕜] EuclideanSpace 𝕜 d} (hA : A.IsSymmetric) (hB : B.IsSymmetric) (hAB : Commute A B) : d → ℝ

Equations

• LinearMap.sharedEigenvaluesB hA hB hAB i = RCLike.re (inner 𝕜 ((LinearMap.sharedEigenbasis hA hB hAB) i) (B ((LinearMap.sharedEigenbasis hA hB hAB) i)))

theorem LinearMap.mem_eigenspace_inf_of_sharedEigenbasis {d : Type u_1} [Fintype d] {𝕜 : Type u_5} [RCLike 𝕜] {A B : EuclideanSpace 𝕜 d →ₗ[𝕜] EuclideanSpace 𝕜 d} (hA : A.IsSymmetric) (hB : B.IsSymmetric) (hAB : Commute A B) (i : d) : ∃ (μ : Module.End.Eigenvalues A) (ν : Module.End.Eigenvalues B), (sharedEigenbasis hA hB hAB) i ∈ Module.End.eigenspace A (↑A 1 μ) ⊓ Module.End.eigenspace B (↑B 1 ν)

theorem LinearMap.apply_A_sharedEigenbasis {d : Type u_1} [Fintype d] {𝕜 : Type u_5} [RCLike 𝕜] {A B : EuclideanSpace 𝕜 d →ₗ[𝕜] EuclideanSpace 𝕜 d} (hA : A.IsSymmetric) (hB : B.IsSymmetric) (hAB : Commute A B) (i : d) : A ((sharedEigenbasis hA hB hAB) i) = ↑(sharedEigenvaluesA hA hB hAB i) • (sharedEigenbasis hA hB hAB) i

theorem LinearMap.apply_B_sharedEigenbasis {d : Type u_1} [Fintype d] {𝕜 : Type u_5} [RCLike 𝕜] {A B : EuclideanSpace 𝕜 d →ₗ[𝕜] EuclideanSpace 𝕜 d} (hA : A.IsSymmetric) (hB : B.IsSymmetric) (hAB : Commute A B) (i : d) : B ((sharedEigenbasis hA hB hAB) i) = ↑(sharedEigenvaluesB hA hB hAB i) • (sharedEigenbasis hA hB hAB) i

noncomputable def Matrix.sharedEigenbasis {d : Type u_1} [Fintype d] [DecidableEq d] {𝕜 : Type u_5} [RCLike 𝕜] {A B : Matrix d d 𝕜} (hA : A.IsHermitian) (hB : B.IsHermitian) (hAB : Commute A B) : OrthonormalBasis d 𝕜 (EuclideanSpace 𝕜 d)

Equations

• Matrix.sharedEigenbasis hA hB hAB = LinearMap.sharedEigenbasis ⋯ ⋯ ⋯

noncomputable def Matrix.sharedEigenvectorUnitary {d : Type u_1} [Fintype d] [DecidableEq d] {𝕜 : Type u_5} [RCLike 𝕜] {A B : Matrix d d 𝕜} (hA : A.IsHermitian) (hB : B.IsHermitian) (hAB : Commute A B) : ↥(unitaryGroup d 𝕜)

Equations

• Matrix.sharedEigenvectorUnitary hA hB hAB = ⟨(EuclideanSpace.basisFun d 𝕜).toBasis.toMatrix ⇑(Matrix.sharedEigenbasis hA hB hAB).toBasis, ⋯⟩

theorem Matrix.SharedEigenbasis.sharedEigenvectorUnitary_mulVec {d : Type u_1} [Fintype d] [DecidableEq d] {𝕜 : Type u_5} [RCLike 𝕜] {A B : Matrix d d 𝕜} (hA : A.IsHermitian) (hB : B.IsHermitian) (hAB : Commute A B) (j : d) : (↑(sharedEigenvectorUnitary hA hB hAB)).mulVec (Pi.single j 1) = ((sharedEigenbasis hA hB hAB) j).ofLp

Analogous to Matrix.IsHermitian.eigenvectorUnitary_mulVec for the shared basis.

noncomputable def Matrix.SharedEigenbasis.sharedEigenvalueA {d : Type u_1} [Fintype d] [DecidableEq d] {𝕜 : Type u_5} [RCLike 𝕜] {A B : Matrix d d 𝕜} (hA : A.IsHermitian) (hB : B.IsHermitian) (hAB : Commute A B) (j : d) : ℝ

Equations

• Matrix.SharedEigenbasis.sharedEigenvalueA hA hB hAB j = LinearMap.sharedEigenvaluesA ⋯ ⋯ ⋯ j

noncomputable def Matrix.SharedEigenbasis.sharedEigenvalueB {d : Type u_1} [Fintype d] [DecidableEq d] {𝕜 : Type u_5} [RCLike 𝕜] {A B : Matrix d d 𝕜} (hA : A.IsHermitian) (hB : B.IsHermitian) (hAB : Commute A B) (j : d) : ℝ

Equations

• Matrix.SharedEigenbasis.sharedEigenvalueB hA hB hAB j = LinearMap.sharedEigenvaluesB ⋯ ⋯ ⋯ j

theorem Matrix.SharedEigenbasis.mulVec_sharedEigenbasisA {d : Type u_1} [Fintype d] [DecidableEq d] {𝕜 : Type u_5} [RCLike 𝕜] {A B : Matrix d d 𝕜} (hA : A.IsHermitian) (hB : B.IsHermitian) (hAB : Commute A B) (j : d) : A.mulVec ((sharedEigenbasis hA hB hAB) j).ofLp = sharedEigenvalueA hA hB hAB j • ((sharedEigenbasis hA hB hAB) j).ofLp

Analogous to Matrix.IsHermitian.mulVec_eigenvectorBasis for the shared basis.

theorem Matrix.SharedEigenbasis.mulVec_sharedEigenbasisB {d : Type u_1} [Fintype d] [DecidableEq d] {𝕜 : Type u_5} [RCLike 𝕜] {A B : Matrix d d 𝕜} (hA : A.IsHermitian) (hB : B.IsHermitian) (hAB : Commute A B) (j : d) : B.mulVec ((sharedEigenbasis hA hB hAB) j).ofLp = sharedEigenvalueB hA hB hAB j • ((sharedEigenbasis hA hB hAB) j).ofLp

theorem Matrix.SharedEigenbasis.star_shared_mul_A_mul_IsDiag {d : Type u_1} [Fintype d] [DecidableEq d] {𝕜 : Type u_5} [RCLike 𝕜] {A B : Matrix d d 𝕜} (hA : A.IsHermitian) (hB : B.IsHermitian) (hAB : Commute A B) : (star ↑(sharedEigenvectorUnitary hA hB hAB) * A * ↑(sharedEigenvectorUnitary hA hB hAB)).IsDiag

theorem Matrix.SharedEigenbasis.star_shared_mul_B_mul_IsDiag {d : Type u_1} [Fintype d] [DecidableEq d] {𝕜 : Type u_5} [RCLike 𝕜] {A B : Matrix d d 𝕜} (hA : A.IsHermitian) (hB : B.IsHermitian) (hAB : Commute A B) : (star ↑(sharedEigenvectorUnitary hA hB hAB) * B * ↑(sharedEigenvectorUnitary hA hB hAB)).IsDiag

Analogous to Matrix.IsHermitian.star_mul_self_mul_eq_diagonal for the shared basis.

theorem Commute.exists_unitary {d : Type u_1} [Fintype d] [DecidableEq d] {𝕜 : Type u_5} [RCLike 𝕜] {A B : Matrix d d 𝕜} (hA : A.IsHermitian) (hB : B.IsHermitian) (hAB : Commute A B) : ∃ (U : ↥(Matrix.unitaryGroup d 𝕜)), (↑U * A * (↑U).conjTranspose).IsDiag ∧ (↑U * B * (↑U).conjTranspose).IsDiag

instance instInvertibleUnitaryGroup {d : Type u_1} [Fintype d] [DecidableEq d] {𝕜 : Type u_5} [RCLike 𝕜] (U : ↥(Matrix.unitaryGroup d 𝕜)) : Invertible U

Equations

• instInvertibleUnitaryGroup U = invertibleOfGroup U

instance instInvertibleMatrixValMemSubmonoidUnitaryGroup_quantumInfo {d : Type u_1} [Fintype d] [DecidableEq d] {𝕜 : Type u_5} [RCLike 𝕜] (U : ↥(Matrix.unitaryGroup d 𝕜)) : Invertible ↑U

Equations

• instInvertibleMatrixValMemSubmonoidUnitaryGroup_quantumInfo U = { invOf := star ↑U, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }

theorem Matrix.IsDiag.exists_cfc {d : Type u_1} [Fintype d] [DecidableEq d] {𝕜 : Type u_5} [RCLike 𝕜] {U : ↥(unitaryGroup d 𝕜)} {M : Matrix d d 𝕜} (hU : (↑U * M * (↑U).conjTranspose).IsDiag) (hM : M.IsHermitian) (e : d ≃ Fin (Fintype.card d)) : ∃ (f : ℝ → ℝ), M = cfc f (((↑U).conjTranspose * diagonal fun (x : d) => ↑↑(e x)) * ↑U)

If a matrix is diagonalized by a unitary matrix, then it can be written as a CFC of a (particular, canonical) diagonal matrix.

theorem Commute.exists_cfc {d : Type u_1} [Fintype d] [DecidableEq d] {𝕜 : Type u_5} [RCLike 𝕜] {A B : Matrix d d 𝕜} (hA : A.IsHermitian) (hB : B.IsHermitian) (hAB : Commute A B) : ∃ (C : Matrix d d 𝕜), (∃ (f : ℝ → ℝ), A = cfc f C) ∧ ∃ (g : ℝ → ℝ), B = cfc g C

If two Hermitian matrices commute, there exists a common matrix that they are both a CFC of.