LeanPool.Monlib4.LinearAlgebra.PosMapIsReal

Imported Lean Pool material for LeanPool.Monlib4.LinearAlgebra.PosMapIsReal.

def LinearMap.IsPosMap {M₁ : Type u_1} {M₂ : Type u_2} [Zero M₁] [Zero M₂] [PartialOrder M₁] [PartialOrder M₂] {F : Type u_3} [FunLike F M₁ M₂] (f : F) : Prop

we say a map $f \colon M_1 \to M_2$ is a positive map if for all positive $x \in M_1$, we also get $f(x)$ is positive

Equations

• LinearMap.IsPosMap f = ∀ ⦃x : M₁⦄, 0 ≤ x → 0 ≤ f x

@[reducible, inline]

noncomputable abbrev selfAdjointDecompositionLeft {B : Type u_1} [Star B] [Add B] [SMul ℂ B] (a : B) : B

The self-adjoint real part of an element.

Equations

• selfAdjointDecompositionLeft a = (1 / 2) • (a + star a)

theorem selfAdjointDecompositionLeft_one {B : Type u_1} [AddCommMonoid B] [MulOneClass B] [StarMul B] [Module ℂ B] : selfAdjointDecompositionLeft 1 = 1

@[reducible, inline]

noncomputable abbrev selfAdjointDecompositionRight {B : Type u_1} [Star B] [Sub B] [SMul ℂ B] (a : B) : B

The self-adjoint imaginary part of an element.

Equations

• selfAdjointDecompositionRight a = RCLike.I • (1 / 2) • (star a - a)

theorem selfAdjointDecompositionRight_one {B : Type u_1} [AddCommGroup B] [MulOneClass B] [StarMul B] [SMulZeroClass ℂ B] : selfAdjointDecompositionRight 1 = 0

theorem selfAdjointDecompositionRight_eq_zero_iff {B : Type u_1} [Star B] [AddGroup B] [SMulWithZero ℂ B] [NoZeroSMulDivisors ℂ B] (a : B) : selfAdjointDecompositionRight a = 0 ↔ IsSelfAdjoint a

theorem selfAdjointDecompositionLeft_isSelfAdjoint {B : Type u_1} [AddCommMonoid B] [StarAddMonoid B] [SMul ℂ B] [StarModule ℂ B] (a : B) : IsSelfAdjoint (selfAdjointDecompositionLeft a)

theorem selfAdjointDecompositionRight_isSelfAdjoint {B : Type u_1} [AddCommGroup B] [StarAddMonoid B] [Module ℂ B] [StarModule ℂ B] (a : B) : IsSelfAdjoint (selfAdjointDecompositionRight a)

theorem selfAdjointDecomposition {B : Type u_1} [AddCommGroup B] [StarAddMonoid B] [Module ℂ B] [StarModule ℂ B] (a : B) : a = selfAdjointDecompositionLeft a + RCLike.I • selfAdjointDecompositionRight a

noncomputable def ContinuousLinearMap.toLinearMapAlgEquiv {𝕜 : Type u_1} {B : Type u_2} [RCLike 𝕜] [NormedAddCommGroup B] [InnerProductSpace 𝕜 B] [FiniteDimensional 𝕜 B] : (B →L[𝕜] B) ≃ₐ[𝕜] B →ₗ[𝕜] B

The algebra equivalence between continuous endomorphisms and linear endomorphisms in finite-dimensional inner product spaces.

Equations

• ContinuousLinearMap.toLinearMapAlgEquiv = AlgEquiv.ofLinearEquiv LinearMap.toContinuousLinearMap.symm ⋯ ⋯

theorem ContinuousLinearMap.toLinearMapAlgEquiv_apply {𝕜 : Type u_1} {B : Type u_2} [RCLike 𝕜] [NormedAddCommGroup B] [InnerProductSpace 𝕜 B] [FiniteDimensional 𝕜 B] (f : B →L[𝕜] B) : toLinearMapAlgEquiv f = ↑f

theorem ContinuousLinearMap.toLinearMapAlgEquiv_symm_apply {𝕜 : Type u_1} {B : Type u_2} [RCLike 𝕜] [NormedAddCommGroup B] [InnerProductSpace 𝕜 B] [FiniteDimensional 𝕜 B] (f : B →ₗ[𝕜] B) : toLinearMapAlgEquiv.symm f = LinearMap.toContinuousLinearMap f

theorem ContinuousLinearMap.spectrum_coe {𝕜 : Type u_1} {B : Type u_2} [RCLike 𝕜] [NormedAddCommGroup B] [InnerProductSpace 𝕜 B] [FiniteDimensional 𝕜 B] (T : B →L[𝕜] B) : spectrum 𝕜 ↑T = spectrum 𝕜 T

theorem ContinuousLinearMap.nonneg_iff_isSelfAdjoint_and_nonneg_spectrum {B : Type u_1} [NormedAddCommGroup B] [InnerProductSpace ℂ B] [FiniteDimensional ℂ B] (T : B →L[ℂ] B) : 0 ≤ T ↔ IsSelfAdjoint T ∧ spectrum ℂ T ⊆ {a : ℂ | 0 ≤ a}

theorem ContinuousLinearMap.nonneg_iff_exists {B : Type u_1} [NormedAddCommGroup B] [InnerProductSpace ℂ B] [FiniteDimensional ℂ B] (T : B →L[ℂ] B) : 0 ≤ T ↔ ∃ (f : B →L[ℂ] B), T = star f * f

theorem orthogonalProjection_ker_comp_eq_of_comp_eq_zero {B : Type u_1} [NormedAddCommGroup B] [InnerProductSpace ℂ B] [FiniteDimensional ℂ B] {T S : B →L[ℂ] B} (h : T * S = 0) : orthogonalProjection' (↑T).ker * S = S

noncomputable def Matrix.orthogonalProjection {n : Type u_2} [Fintype n] [DecidableEq n] (U : Submodule ℂ (EuclideanSpace ℂ n)) : Matrix n n ℂ

matrix of orthogonalProjection

Equations

• Matrix.orthogonalProjection U = Matrix.toEuclideanCLM.symm (orthogonalProjection' U)

noncomputable def PiMat.orthogonalProjection {k : Type u_3} {n : k → Type u_4} [(i : k) → Fintype (n i)] [(i : k) → DecidableEq (n i)] (U : (i : k) → Submodule ℂ (EuclideanSpace ℂ (n i))) : PiMat ℂ k n

The blockwise matrix of orthogonal projections for a PiMat.

Equations

• PiMat.orthogonalProjection U i = Matrix.orthogonalProjection (U i)

theorem Matrix.toEuclideanLin_symm {𝕜 : Type u_3} {n : Type u_4} [RCLike 𝕜] [Fintype n] [DecidableEq n] (x : EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n) : toEuclideanLin.symm x = (LinearMap.toMatrix (EuclideanSpace.basisFun n 𝕜).toBasis (EuclideanSpace.basisFun n 𝕜).toBasis) x

theorem EuclideanSpace.trace_eq_matrix_trace' {𝕜 : Type u_3} {n : Type u_4} [RCLike 𝕜] [Fintype n] [DecidableEq n] (f : EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n) : (LinearMap.trace 𝕜 (EuclideanSpace 𝕜 n)) f = (Matrix.toEuclideanLin.symm f).trace

theorem Matrix.coe_toEuclideanCLM_symm_eq_toEuclideanLin_symm {𝕜 : Type u_3} {n : Type u_4} [RCLike 𝕜] [Fintype n] [DecidableEq n] (A : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) : toEuclideanCLM.symm A = toEuclideanLin.symm ↑A

theorem Matrix.orthogonalProjection_trace {n : Type u_2} [Fintype n] [DecidableEq n] {U : Submodule ℂ (EuclideanSpace ℂ n)} : (orthogonalProjection U).trace = ↑(Module.finrank ℂ ↥U)

theorem PiMat.orthogonalProjection_trace {k : Type u_3} {n : k → Type u_4} [Fintype k] [DecidableEq k] [(i : k) → Fintype (n i)] [(i : k) → DecidableEq (n i)] (U : (i : k) → Submodule ℂ (EuclideanSpace ℂ (n i))) : (Matrix.blockDiagonal' (orthogonalProjection U)).trace = ↑(∑ i : k, Module.finrank ℂ ↥(U i))

theorem Matrix.isIdempotentElem_toEuclideanCLM {n : Type u_3} [Fintype n] [DecidableEq n] (x : Matrix n n ℂ) : IsIdempotentElem x ↔ IsIdempotentElem (toEuclideanCLM x)

theorem Matrix.CLM_apply_orthogonalProjection {n : Type u_2} [Fintype n] [DecidableEq n] {U : Submodule ℂ (EuclideanSpace ℂ n)} : toEuclideanCLM (orthogonalProjection U) = orthogonalProjection' U

theorem Matrix.orthogonalProjection_ortho_eq {n : Type u_2} [Fintype n] [DecidableEq n] {U : Submodule ℂ (EuclideanSpace ℂ n)} : orthogonalProjection Uᗮ = 1 - orthogonalProjection U

theorem Matrix.orthogonalProjection_isPosSemidef {n : Type u_2} [Fintype n] [DecidableEq n] {U : Submodule ℂ (EuclideanSpace ℂ n)} : (orthogonalProjection U).PosSemidef

theorem Matrix.IsHermitian.orthogonalProjection_ker_apply_self {n : Type u_2} [Fintype n] [DecidableEq n] {x : Matrix n n ℂ} (hx : x.IsHermitian) : orthogonalProjection (↑(toEuclideanCLM x)).ker * x = 0

theorem Matrix.nonneg_def {n : Type u_2} {x : Matrix n n ℂ} : 0 ≤ x ↔ x.PosSemidef

noncomputable def Matrix.IsHermitian.sqSqrt {n : Type u_2} [Fintype n] [DecidableEq n] {x : Matrix n n ℂ} (hx : x.IsHermitian) : Matrix n n ℂ

the positive square root of the square of a Hermitian matrix x, in other words, √(x ^ 2)

Equations

• hx.sqSqrt = (Matrix.innerAut hx.eigenvectorUnitary) (Matrix.diagonal (RCLike.ofReal ∘ fun (i : n) => √(hx.eigenvalues i ^ 2)))

theorem Matrix.IsHermitian.sqSqrt_eq {n : Type u_2} [Fintype n] [DecidableEq n] {x : Matrix n n ℂ} (hx : x.IsHermitian) : hx.sqSqrt = (innerAut hx.eigenvectorUnitary) (diagonal (RCLike.ofReal ∘ |hx.eigenvalues|))

theorem Matrix.IsHermitian.sqSqrt_isPosSemidef {n : Type u_2} [Fintype n] [DecidableEq n] {x : Matrix n n ℂ} (hx : x.IsHermitian) : hx.sqSqrt.PosSemidef

theorem Matrix.IsHermitian.sqSqrt_sq {n : Type u_2} [Fintype n] [DecidableEq n] {x : Matrix n n ℂ} (hx : x.IsHermitian) : hx.sqSqrt ^ 2 = x ^ 2

the square of the positive square root of a Hermitian matrix is equal to the square of the matrix

noncomputable def Matrix.IsHermitian.posSemidefDecompositionLeft {n : Type u_2} [Fintype n] [DecidableEq n] (x : Matrix n n ℂ) [hx : Fact x.IsHermitian] : Matrix n n ℂ

The positive part in the decomposition of a Hermitian matrix.

Equations

• x₊ = (1 / 2) • (⋯.sqSqrt + x)

def posL : Lean.TrailingParserDescr

Notation for the positive part in the decomposition of a Hermitian matrix.

Equations

• posL = Lean.ParserDescr.trailingNode `posL 80 81 (Lean.ParserDescr.symbol "₊")

theorem Matrix.IsHermitian.sqSqrt_isHermitian {n : Type u_2} [Fintype n] [DecidableEq n] {x : Matrix n n ℂ} (hx : x.IsHermitian) : hx.sqSqrt.IsHermitian

theorem Matrix.IsHermitian.posSemidefDecompositionLeft_isHermitian {n : Type u_2} [Fintype n] [DecidableEq n] {x : Matrix n n ℂ} [hx : Fact x.IsHermitian] : x₊.IsHermitian

noncomputable def Matrix.IsHermitian.posSemidefDecompositionRight {n : Type u_2} [Fintype n] [DecidableEq n] (x : Matrix n n ℂ) [hx : Fact x.IsHermitian] : Matrix n n ℂ

The negative part in the decomposition of a Hermitian matrix.

Equations

• x₋ = (1 / 2) • (⋯.sqSqrt - x)

def posR : Lean.TrailingParserDescr

Notation for the negative part in the decomposition of a Hermitian matrix.

Equations

• posR = Lean.ParserDescr.trailingNode `posR 80 81 (Lean.ParserDescr.symbol "₋")

theorem Matrix.IsHermitian.posSemidefDecompositionRight_isHermitian {n : Type u_2} [Fintype n] [DecidableEq n] {x : Matrix n n ℂ} [hx : Fact x.IsHermitian] : x₋.IsHermitian

theorem Matrix.IsHermitian.commute_sqSqrt {n : Type u_2} [Fintype n] [DecidableEq n] {x : Matrix n n ℂ} (hx : x.IsHermitian) : Commute x hx.sqSqrt

a Hermitian matrix commutes with its positive squared-square-root, i.e., x * √(x^2) = √(x^2) * x.

theorem Matrix.IsHermitian.posSemidefDecompositionLeft_mul_right {n : Type u_2} [Fintype n] [DecidableEq n] (x : Matrix n n ℂ) [hx : Fact x.IsHermitian] : x₊ * x₋ = 0

theorem Matrix.IsHermitian.posSemidefDecompositionRight_mul_left {n : Type u_2} [Fintype n] [DecidableEq n] (x : Matrix n n ℂ) [hx : Fact x.IsHermitian] : x₋ * x₊ = 0

theorem Matrix.IsHermitian.posSemidefDecomposition_eq {n : Type u_2} [Fintype n] [DecidableEq n] (x : Matrix n n ℂ) [hx : Fact x.IsHermitian] : x = x₊ - x₋

theorem Matrix.IsHermitian.posSemidefDecomposition_posSemidef_left_right {n : Type u_2} [Fintype n] [DecidableEq n] {x : Matrix n n ℂ} (hx : Fact x.IsHermitian) : x₊.PosSemidef ∧ x₋.PosSemidef

theorem Matrix.IsHermitian.posSemidefDecomposition' {n : Type u_2} [Fintype n] {x : Matrix n n ℂ} (hx : x.IsHermitian) : ∃ (a : Matrix n n ℂ) (b : Matrix n n ℂ), x = a.conjTranspose * a - b.conjTranspose * b

theorem PiMat.IsSelfAdjoint.posSemidefDecomposition {k : Type u_3} {n : k → Type u_4} [(i : k) → Fintype (n i)] {x : PiMat ℂ k n} (hx : IsSelfAdjoint x) : ∃ (a : PiMat ℂ k n) (b : PiMat ℂ k n), x = star a * a - star b * b

theorem IsSelfAdjoint.isPositiveDecomposition {B : Type u_1} [NormedAddCommGroup B] [InnerProductSpace ℂ B] [FiniteDimensional ℂ B] {x : B →L[ℂ] B} (hx : IsSelfAdjoint x) : ∃ (a : B →L[ℂ] B) (b : B →L[ℂ] B), x = star a * a - star b * b

structure isEquivToPiMat (A : Type u) [Add A] [Mul A] [Star A] [SMul ℂ A] : Type (u + 1)

Data exhibiting a star algebra as equivalent to a finite product of matrix algebras.

• k : Type u

  The index type for the product of matrix algebras.

• rk : self.k → Type u

  The matrix index type in each summand.

• hrk₁ (i : self.k) : Fintype (self.rk i)

  Finiteness of each matrix index type.

• hrk₂ (i : self.k) : DecidableEq (self.rk i)

  Decidable equality for each matrix index type.

• φ : A ≃⋆ₐ[ℂ] PiMat ℂ self.k self.rk

  The star algebra equivalence to the product of matrix algebras.

noncomputable def Matrix.isEquivToPiMat {n : Type u_2} [Fintype n] [DecidableEq n] : _root_.isEquivToPiMat (Matrix n n ℂ)

Matrices are trivially equivalent to a one-summand product of matrix algebras.

Equations

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

theorem IsSelfAdjoint.isPositiveDecomposition_of_starAlgEquiv_piMat {A : Type u_3} [Ring A] [StarRing A] [Algebra ℂ A] (hφ : isEquivToPiMat A) {x : A} (hx : IsSelfAdjoint x) : ∃ (a : A) (b : A), x = star a * a - star b * b

theorem Matrix.isReal_of_isPosMap {n : Type u_2} [Finite n] {K : Type u_3} [Ring K] [StarRing K] [PartialOrder K] [Algebra ℂ K] [StarOrderedRing K] [StarModule ℂ K] {φ : Matrix n n ℂ →ₗ[ℂ] K} (hφ : LinearMap.IsPosMap φ) : LinearMap.IsReal φ

if a map preserves positivity, then it is star-preserving

theorem StarNonUnitalAlgHom.toLinearMap_apply {R : Type u_3} {A : Type u_4} {B : Type u_5} [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [Star A] [Star B] (f : A →⋆ₙₐ[R] B) (x : A) : ↑f x = f x

theorem LinearMap.isPosMap_iff_star_mul_self_nonneg {A : Type u_3} {K : Type u_4} [NonUnitalSemiring A] [PartialOrder A] [StarRing A] [StarOrderedRing A] [NonUnitalSemiring K] [PartialOrder K] [StarRing K] [StarOrderedRing K] (hA : ∀ ⦃a : A⦄, 0 ≤ a ↔ ∃ (b : A), a = star b * b) {F : Type u_5} [FunLike F A K] {f : F} : IsPosMap f ↔ ∀ (a : A), 0 ≤ f (star a * a)

theorem LinearMap.isPosMap_iff_comp_starAlgEquiv {K : Type u_3} {A : Type u_4} {B : Type u_5} [Mul K] [Mul A] [Mul B] [Star K] [Star A] [Star B] [Zero A] [Zero B] [Zero K] [PartialOrder A] [PartialOrder B] [PartialOrder K] (hA : ∀ ⦃a : A⦄, 0 ≤ a ↔ ∃ (b : A), a = star b * b) (hB : ∀ ⦃a : B⦄, 0 ≤ a ↔ ∃ (b : B), a = star b * b) {F : Type u_6} {S : Type u_7} [FunLike F A K] {φ : F} [EquivLike S B A] [MulEquivClass S B A] [StarHomClass S B A] (ψ : S) : IsPosMap φ ↔ ∀ ⦃x : B⦄, 0 ≤ x → 0 ≤ φ (ψ x)

theorem LinearMap.isReal_iff_comp_starEquiv {K : Type u_3} {A : Type u_4} {B : Type u_5} [Star K] [Star A] [Star B] {F : Type u_6} {S : Type u_7} [FunLike F A K] [EquivLike S B A] [StarHomClass S B A] {φ : F} (ψ : S) : IsReal φ ↔ ∀ (x : B), φ (ψ (star x)) = star (φ (ψ x))

theorem isReal_of_isPosMap {B : Type u_1} [NormedAddCommGroup B] [InnerProductSpace ℂ B] [FiniteDimensional ℂ B] {K : Type u_3} [Ring K] [StarRing K] [PartialOrder K] [Algebra ℂ K] [StarOrderedRing K] [StarModule ℂ K] {φ : (B →L[ℂ] B) →ₗ[ℂ] K} (hφ : LinearMap.IsPosMap φ) : LinearMap.IsReal φ

if a map preserves positivity, then it is star-preserving

theorem isReal_of_isPosMap_of_starAlgEquiv_piMat {A : Type u_4} [Ring A] [StarRing A] [Algebra ℂ A] [StarModule ℂ A] [PartialOrder A] [StarOrderedRing A] (hφ : isEquivToPiMat A) {K : Type u_3} [Ring K] [StarRing K] [PartialOrder K] [Algebra ℂ K] [StarOrderedRing K] [StarModule ℂ K] {f : A →ₗ[ℂ] K} (hf : LinearMap.IsPosMap f) : LinearMap.IsReal f

theorem starMulHom_isPosMap {A : Type u_3} {K : Type u_4} [Semiring A] [PartialOrder A] [StarRing A] [StarOrderedRing A] [Semiring K] [PartialOrder K] [StarRing K] [StarOrderedRing K] (hA : ∀ ⦃a : A⦄, 0 ≤ a ↔ ∃ (b : A), a = star b * b) {F : Type u_5} [FunLike F A K] [StarHomClass F A K] [MulHomClass F A K] (f : F) : LinearMap.IsPosMap f

a $^*$-homomorphism from $A$ to $B$ is a positive map

theorem NonUnitalAlgHom.isPosMap_iff_isReal_of_nonUnitalStarAlgEquiv_piMat {A : Type u_4} [Ring A] [StarRing A] [Algebra ℂ A] [StarModule ℂ A] [PartialOrder A] [StarOrderedRing A] (hφ : isEquivToPiMat A) (hA : ∀ ⦃a : A⦄, 0 ≤ a ↔ ∃ (b : A), a = star b * b) {K : Type u_3} [Ring K] [StarRing K] [PartialOrder K] [Algebra ℂ K] [StarOrderedRing K] [StarModule ℂ K] {f : A →ₙₐ[ℂ] K} : LinearMap.IsPosMap f ↔ LinearMap.IsReal f

theorem Matrix.innerAut.map_zpow {n : Type u_3} [Fintype n] [DecidableEq n] {𝕜 : Type u_4} [RCLike 𝕜] (U : ↥(unitaryGroup n 𝕜)) (x : Matrix n n 𝕜) (z : ℤ) : (innerAut U) x ^ z = (innerAut U) (x ^ z)

theorem Matrix.inv_diagonal' {R : Type u_3} {n : Type u_4} [Field R] [Fintype n] [DecidableEq n] (d : n → R) [Invertible d] : (diagonal d)⁻¹ = diagonal d⁻¹

theorem Matrix.diagonal_zpow {n : Type u_2} [Fintype n] [DecidableEq n] {𝕜 : Type u_3} [Field 𝕜] (x : n → 𝕜) [Invertible x] (z : ℤ) : diagonal x ^ z = diagonal (x ^ z)

theorem Matrix.PosDef.rpow_zpow {n : Type u_2} [Fintype n] [DecidableEq n] {𝕜 : Type u_3} [RCLike 𝕜] {Q : Matrix n n 𝕜} (hQ : Q.PosDef) (r : ℝ) (z : ℤ) : hQ.rpow r ^ z = hQ.rpow (r * ↑z)

theorem Matrix.PosDef.rpow_eq_pow {n : Type u_2} [Fintype n] [DecidableEq n] {𝕜 : Type u_3} [RCLike 𝕜] {Q : Matrix n n 𝕜} (hQ : Q.PosDef) (r : ℕ) : hQ.rpow ↑r = Q ^ r

theorem Matrix.PosDef.rpow_eq_zpow {n : Type u_2} [Fintype n] [DecidableEq n] {𝕜 : Type u_3} [RCLike 𝕜] {Q : Matrix n n 𝕜} (hQ : Q.PosDef) (r : ℤ) : hQ.rpow ↑r = Q ^ r

theorem Matrix.PosDef.rpow_rzpow {n : Type u_2} [Fintype n] [DecidableEq n] {𝕜 : Type u_3} [RCLike 𝕜] {Q : Matrix n n 𝕜} (hQ : Q.PosDef) (r : ℝ) (z : ℤ) : ⋯.rpow ↑z = hQ.rpow (r * ↑z)

theorem Matrix.PosDef.eq_zpow_of_zpow_inv_eq {n : Type u_2} [Fintype n] [DecidableEq n] {𝕜 : Type u_3} [RCLike 𝕜] {Q R : Matrix n n 𝕜} (hQ : Q.PosDef) {z : ℤ} (hz : z ≠ 0) (h : hQ.rpow (↑z)⁻¹ = R) : Q = R ^ z

theorem Matrix.PosDef.eq_of_zpow_inv_eq_zpow_inv {n : Type u_2} [Fintype n] [DecidableEq n] {𝕜 : Type u_3} [RCLike 𝕜] {Q R : Matrix n n 𝕜} (hQ : Q.PosDef) (hR : R.PosDef) {r : ℤ} (hr : r ≠ 0) (hQR : hQ.rpow (↑r)⁻¹ = hR.rpow (↑r)⁻¹) : Q = R

theorem selfAdjointDecomposition_ext_iff {B : Type u_3} [AddCommGroup B] [StarAddMonoid B] [Module ℂ B] [StarModule ℂ B] (a b : B) : a = b ↔ selfAdjointDecompositionLeft a = selfAdjointDecompositionLeft b ∧ selfAdjointDecompositionRight a = selfAdjointDecompositionRight b

theorem selfAdjointDecompositionLeft_of {B : Type u_3} [AddCommGroup B] [StarAddMonoid B] [Module ℂ B] [StarModule ℂ B] (a b : B) (ha : IsSelfAdjoint a) (hb : IsSelfAdjoint b) : selfAdjointDecompositionLeft (a + Complex.I • b) = a

theorem selfAdjointDecompositionRight_of {B : Type u_3} [AddCommGroup B] [StarAddMonoid B] [Module ℂ B] [StarModule ℂ B] (a b : B) (ha : IsSelfAdjoint a) (hb : IsSelfAdjoint b) : selfAdjointDecompositionRight (a + Complex.I • b) = b

theorem complex_decomposition_mul_decomposition {B : Type u_3} [Ring B] [StarRing B] [Module ℂ B] [StarModule ℂ B] [IsScalarTower ℂ B B] [SMulCommClass ℂ B B] (a b c d : B) : (a + Complex.I • b) * (c + Complex.I • d) = a * c - b * d + Complex.I • (b * c + a * d)

theorem selfAdjointDecompositionLeft_mul_self {B : Type u_3} [Ring B] [StarRing B] [Module ℂ B] [StarModule ℂ B] [IsScalarTower ℂ B B] [SMulCommClass ℂ B B] (a : B) : selfAdjointDecompositionLeft (a * a) = selfAdjointDecompositionLeft a * selfAdjointDecompositionLeft a - selfAdjointDecompositionRight a * selfAdjointDecompositionRight a

theorem selfAdjointDecompositionRight_mul_self {B : Type u_3} [Ring B] [StarRing B] [Module ℂ B] [StarModule ℂ B] [IsScalarTower ℂ B B] [SMulCommClass ℂ B B] (a : B) : selfAdjointDecompositionRight (a * a) = selfAdjointDecompositionRight a * selfAdjointDecompositionLeft a + selfAdjointDecompositionLeft a * selfAdjointDecompositionRight a

theorem isStarNormal_iff_selfAdjointDecomposition_commute {B : Type u_3} [Ring B] [StarRing B] [Module ℂ B] [StarModule ℂ B] [IsScalarTower ℂ B B] [SMulCommClass ℂ B B] (p : B) : IsStarNormal p ↔ Commute (selfAdjointDecompositionLeft p) (selfAdjointDecompositionRight p)

theorem isSelfAdjoint_iff_selfAdjointDecompositionRight_eq_zero {B : Type u_3} [Ring B] [StarRing B] [Module ℂ B] [StarModule ℂ B] [IsScalarTower ℂ B B] [SMulCommClass ℂ B B] (p : B) : IsSelfAdjoint p ↔ selfAdjointDecompositionRight p = 0

theorem IsIdempotentElem.isSelfAdjoint_iff_isStarNormal {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ℂ V] (p : V →L[ℂ] V) (hp : IsIdempotentElem p) [CompleteSpace V] : IsSelfAdjoint p ↔ IsStarNormal p

theorem LinearMap.IsPositive'.add_ker_eq_inf_ker {𝕜 : Type u_3} {V : Type u_4} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [FiniteDimensional 𝕜 V] {S T : V →ₗ[𝕜] V} (hS : S.IsPositive') (hT : T.IsPositive') : (S + T).ker = S.ker ⊓ T.ker

theorem mem_unitary_iff_isStarNormal_and_decomposition_left_sq_add_right_sq_eq_one {B : Type u_3} [Ring B] [StarRing B] [Module ℂ B] [StarModule ℂ B] [IsScalarTower ℂ B B] [SMulCommClass ℂ B B] (a : B) : a ∈ unitary B ↔ IsStarNormal a ∧ selfAdjointDecompositionLeft a ^ 2 + selfAdjointDecompositionRight a ^ 2 = 1

theorem LinearMap.exists_scalar_isometry_iff_preserves_ortho_of_ne_zero {𝕜 : Type u_3} {V : Type u_4} {W : Type u_5} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [NormedAddCommGroup W] [InnerProductSpace 𝕜 W] (hV : 0 < Module.finrank 𝕜 V) {T : V →ₗ[𝕜] W} (hT : T ≠ 0) : (∃ (α : 𝕜ˣ), Isometry ⇑(↑α • T)) ↔ ∀ (x y : V), inner 𝕜 x y = 0 → inner 𝕜 (T x) (T y) = 0

theorem LinearMap.exists_scalar_isometry_iff_preserves_ortho {𝕜 : Type u_3} {V : Type u_4} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [Module.Finite 𝕜 V] {T : V →ₗ[𝕜] V} : (∃ (α : 𝕜) (S : V →ₗᵢ[𝕜] V), T = α • S.toLinearMap) ↔ ∀ (x y : V), inner 𝕜 x y = 0 → inner 𝕜 (T x) (T y) = 0

theorem LinearMap.isSymmetric_adjoint_mul_self' {𝕜 : Type u_3} {V : Type u_4} {W : Type u_5} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [NormedAddCommGroup W] [InnerProductSpace 𝕜 W] [FiniteDimensional 𝕜 V] [FiniteDimensional 𝕜 W] (T : V →ₗ[𝕜] W) : (adjoint T ∘ₗ T).IsSymmetric