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.

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