Monlib.LinearAlgebra.PosMap

source

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

Instances For

source

@[reducible, inline]

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

Equations

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

Instances For

source

theorem selfAdjointDecomposition_left_one {B : Type u_1} [AddCommMonoid B] [MulOneClass B] [StarMul B] [Module ℂ B] :

selfAdjointDecomposition_left 1 = 1

source

@[reducible, inline]

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

Equations

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

Instances For

source

theorem selfAdjointDecomposition_right_one {B : Type u_1} [AddCommGroup B] [MulOneClass B] [StarMul B] [SMulZeroClass ℂ B] :

selfAdjointDecomposition_right 1 = 0

source

theorem selfAdjointDecomposition_right_eq_zero_iff {B : Type u_1} [Star B] [AddGroup B] [SMulWithZero ℂ B] [NoZeroSMulDivisors ℂ B] (a : B) :

selfAdjointDecomposition_right a = 0 ↔ IsSelfAdjoint a

source

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

IsSelfAdjoint (selfAdjointDecomposition_left a)

source

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

IsSelfAdjoint (selfAdjointDecomposition_right a)

source

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

a = selfAdjointDecomposition_left a + RCLike.I • selfAdjointDecomposition_right a

source

noncomputable def ContinuousLinearMap.toLinearMapAlgEquiv {𝕜 : Type u_1} {B : Type u_2} [RCLike 𝕜] [NormedAddCommGroup B] [InnerProductSpace 𝕜 B] [FiniteDimensional 𝕜 B] :

(B →L[𝕜] B) ≃ₐ[𝕜] B →ₗ[𝕜] B

Equations

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

Instances For

source

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

ContinuousLinearMap.toLinearMapAlgEquiv f = ↑f

source

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

ContinuousLinearMap.toLinearMapAlgEquiv.symm f = LinearMap.toContinuousLinearMap f

source

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

source

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}

source

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

source

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

orthogonalProjection' (LinearMap.ker T) * S = S

source

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)

Instances For

source

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

Equations

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

Instances For

source

theorem Matrix.toEuclideanLin_symm {𝕜 : Type u_3} {n : Type u_4} [RCLike 𝕜] [Fintype n] [DecidableEq n] (x : EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n) :

Matrix.toEuclideanLin.symm x = LinearMap.toMatrix' x

source

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

source

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

Matrix.toEuclideanCLM.symm A = Matrix.toEuclideanLin.symm ↑A

source

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

(Matrix.orthogonalProjection U).trace = ↑(Module.finrank ℂ ↥U)

source

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' (PiMat.orthogonalProjection U)).trace = ↑(∑ i : k, Module.finrank ℂ ↥(U i))

source

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

IsIdempotentElem x ↔ IsIdempotentElem (Matrix.toEuclideanCLM x)

source

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

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

source

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

Matrix.orthogonalProjection Uᗮ = 1 - Matrix.orthogonalProjection U

source

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

(Matrix.orthogonalProjection U).PosSemidef

source

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

Matrix.orthogonalProjection (LinearMap.ker (Matrix.toEuclideanCLM x)) * x = 0

source

theorem Matrix.nonneg_def {n : Type u_2} [Fintype n] [DecidableEq n] {x : Matrix n n ℂ} :

0 ≤ x ↔ x.PosSemidef

source

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

Instances For

source

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

hx.sqSqrt = (Matrix.innerAut hx.eigenvectorUnitary) (Matrix.diagonal (RCLike.ofReal ∘ |hx.eigenvalues|))

source

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

hx.sqSqrt.PosSemidef

source

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

source

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

Matrix n n ℂ

Equations

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

Instances For

source

def posL.delab :

Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

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

Instances For

source

def posL :

Lean.TrailingParserDescr

Equations

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

Instances For

source

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

x₊.IsHermitian

source

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

Matrix n n ℂ

Equations

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

Instances For

source

def posR :

Lean.TrailingParserDescr

Equations

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

Instances For

source

def posR.delab :

Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

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

Instances For

source

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

x₋.IsHermitian

source

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.

source

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

x₊ * x₋ = 0

source

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

x₋ * x₊ = 0

source

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

x = x₊ - x₋

source

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

source

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

∃ (a : Matrix n n ℂ) (b : Matrix n n ℂ), x = a.conjTranspose * a - b.conjTranspose * b

source

theorem PiMat.IsSelfAdjoint.posSemidefDecomposition {k : Type u_3} {n : k → Type u_4} [(i : k) → Fintype (n i)] [(i : k) → DecidableEq (n i)] {x : PiMat ℂ k n} (hx : IsSelfAdjoint x) :

∃ (a : PiMat ℂ k n) (b : PiMat ℂ k n), x = star a * a - star b * b

source

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

source

structure isEquivToPiMat (A : Type u_3) [Add A] [Mul A] [Star A] [SMul ℂ A] :

Type (max (max u_3 (u_4 + 1)) (u_5 + 1))

k : Type u_4
rk : self.k → Type u_5
hrk₁ : (i : self.k) → Fintype (self.rk i)
hrk₂ : (i : self.k) → DecidableEq (self.rk i)
φ : A ≃⋆ₐ[ℂ ] PiMat ℂ self.k self.rk

Instances For

source

noncomputable def Matrix.isEquivToPiMat {n : Type u_2} [Fintype n] [DecidableEq n] :

isEquivToPiMat (Matrix n n ℂ)

Equations

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

Instances For

source

theorem IsSelfAdjoint.isPositiveDecomposition_of_starAlgEquiv_piMat {A : Type u_3} [Ring A] [StarRing A] [Algebra ℂ A] [PartialOrder A] [StarOrderedRing A] (hφ : isEquivToPiMat A) {x : A} (hx : IsSelfAdjoint x) :

∃ (a : A) (b : A), x = star a * a - star b * b

source

theorem Matrix.isReal_of_isPosMap {n : Type u_2} [Fintype n] [DecidableEq 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

source

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

source

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} :

LinearMap.IsPosMap f ↔ ∀ (a : A), 0 ≤ f (star a * a)

source

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

LinearMap.IsPosMap φ ↔ ∀ ⦃x : B⦄, 0 ≤ x → 0 ≤ φ (ψ x)

source

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

LinearMap.IsReal φ ↔ ∀ (x : B), φ (ψ (star x)) = star (φ (ψ x))

source

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

source

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

source

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

source

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

source

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

(Matrix.innerAut U) x ^ z = (Matrix.innerAut U) (x ^ z)

source

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

(Matrix.diagonal d)⁻¹ = Matrix.diagonal d⁻¹

source

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

Matrix.diagonal x ^ z = Matrix.diagonal (x ^ z)

source

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)

source

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

source

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

source

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)

source

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

Q = R ^ z

source

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

Q = R

source

theorem selfAdjointDecomposition_ext_iff {B : Type u_3} [AddCommGroup B] [StarAddMonoid B] [Module ℂ B] [StarModule ℂ B] (a : B) (b : B) :

a = b ↔ selfAdjointDecomposition_left a = selfAdjointDecomposition_left b ∧ selfAdjointDecomposition_right a = selfAdjointDecomposition_right b

source

theorem selfAdjointDecomposition_left_of {B : Type u_3} [AddCommGroup B] [StarAddMonoid B] [Module ℂ B] [StarModule ℂ B] (a : B) (b : B) (ha : IsSelfAdjoint a) (hb : IsSelfAdjoint b) :

selfAdjointDecomposition_left (a + Complex.I • b) = a

source

theorem selfAdjointDecomposition_right_of {B : Type u_3} [AddCommGroup B] [StarAddMonoid B] [Module ℂ B] [StarModule ℂ B] (a : B) (b : B) (ha : IsSelfAdjoint a) (hb : IsSelfAdjoint b) :

selfAdjointDecomposition_right (a + Complex.I • b) = b

source

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) (b : B) (c : B) (d : B) :

(a + Complex.I • b) * (c + Complex.I • d) = a * c - b * d + Complex.I • (b * c + a * d)

source

theorem selfAdjointDecomposition_left_mul_self {B : Type u_3} [Ring B] [StarRing B] [Module ℂ B] [StarModule ℂ B] [IsScalarTower ℂ B B] [SMulCommClass ℂ B B] (a : B) :

selfAdjointDecomposition_left (a * a) = selfAdjointDecomposition_left a * selfAdjointDecomposition_left a - selfAdjointDecomposition_right a * selfAdjointDecomposition_right a

source

theorem selfAdjointDecomposition_right_mul_self {B : Type u_3} [Ring B] [StarRing B] [Module ℂ B] [StarModule ℂ B] [IsScalarTower ℂ B B] [SMulCommClass ℂ B B] (a : B) :

selfAdjointDecomposition_right (a * a) = selfAdjointDecomposition_right a * selfAdjointDecomposition_left a + selfAdjointDecomposition_left a * selfAdjointDecomposition_right a

source

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 (selfAdjointDecomposition_left p) (selfAdjointDecomposition_right p)

source

theorem isSelfAdjoint_iff_selfAdjointDecomposition_right_eq_zero {B : Type u_3} [Ring B] [StarRing B] [Module ℂ B] [StarModule ℂ B] [IsScalarTower ℂ B B] [SMulCommClass ℂ B B] (p : B) :

IsSelfAdjoint p ↔ selfAdjointDecomposition_right p = 0

source

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

source

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

LinearMap.ker (S + T) = LinearMap.ker S ⊓ LinearMap.ker T

source

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 ∧ selfAdjointDecomposition_left a ^ 2 + selfAdjointDecomposition_right a ^ 2 = 1

source

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

source

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

source

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

(LinearMap.adjoint T ∘ₗ T).IsSymmetric

Documentation

Monlib.LinearAlgebra.PosMap_isReal