Projectors associated to Hermitian matrices

• projector: The HermitianMat that projects onto a given submodule
• supportProj: The HermitianMat that projects onto the range (nonzero eigenvalues)
• kerProj: The HermitianMat that projects onto the kernel
• projLE: With notation {A ≤ₚ B}, projLE A B is the projector onto the nonnegative eigenspace of B - A.
• projLT: With notation {A <ₚ B}, projLT A B is the projector onto the positive eigenspace of B - A.
• Positive and negative part, written A⁺ and A⁻, give the restriction of a HermitianMat onto its positive (resp. negative) eigenvalues; equivalently, it's nonnegative (resp. nonpositive) eigenvalues.

noncomputable def HermitianMat.projector {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] (S : Submodule 𝕜 (EuclideanSpace 𝕜 n)) : HermitianMat n 𝕜

Given a Submodule (EuclideanSpace ...) to HermitianMat, this gives the projector onto that subspace, i.e. a matrix that squares to itself, preserves vectors in the submodule, and zeroes out anything in the orthogonal complement of that submodule.

Equations

• HermitianMat.projector S = ⟨(LinearMap.toMatrix (EuclideanSpace.basisFun n 𝕜).toBasis (EuclideanSpace.basisFun n 𝕜).toBasis) ↑(S.subtypeL.comp S.orthogonalProjection), ⋯⟩

theorem HermitianMat.projector_add_orthogonal {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] (S : Submodule 𝕜 (EuclideanSpace 𝕜 n)) : projector S + projector Sᗮ = 1

@[simp]

theorem HermitianMat.trace_projector {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] (S : Submodule 𝕜 (EuclideanSpace 𝕜 n)) : (projector S).trace = ↑(Module.finrank 𝕜 ↥S)

noncomputable def HermitianMat.supportProj {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] (A : HermitianMat n 𝕜) : HermitianMat n 𝕜

The HermitianMat.projector for the HermitianMat.support submodule.

Equations

• A.supportProj = HermitianMat.projector A.support

noncomputable def HermitianMat.kerProj {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] (A : HermitianMat n 𝕜) : HermitianMat n 𝕜

The HermitianMat.projector for the HermitianMat.ker submodule.

Equations

• A.kerProj = HermitianMat.projector A.ker

@[simp]

theorem HermitianMat.kerProj_add_supportProj {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] (A : HermitianMat n 𝕜) : A.kerProj + A.supportProj = 1

@[simp]

theorem HermitianMat.kerProj_of_nonSingular {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] (A : HermitianMat n 𝕜) [A.NonSingular] : A.kerProj = 0

@[simp]

theorem HermitianMat.supportProj_of_nonSingular {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] (A : HermitianMat n 𝕜) [A.NonSingular] : A.supportProj = 1

theorem HermitianMat.projector_eq_sum_rankOne {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] {ι : Type u_3} [Fintype ι] (S : Submodule 𝕜 (EuclideanSpace 𝕜 n)) (b : OrthonormalBasis ι 𝕜 ↥S) : ↑(projector S) = ∑ i : ι, Matrix.vecMulVec (S.subtype (b i)).ofLp (star (S.subtype (b i)).ofLp)

The projector onto a submodule S is the sum of the outer products of the vectors in an orthonormal basis of S.

theorem HermitianMat.projector_support_eq_sum {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] (A : HermitianMat n 𝕜) : ↑A.supportProj = ∑ i : n, (if ⋯.eigenvalues i = 0 then 0 else 1) • Matrix.vecMulVec (⋯.eigenvectorBasis i).ofLp (star (⋯.eigenvectorBasis i).ofLp)

The projector onto the support of A is the sum of the projections onto the eigenvectors with non-zero eigenvalues.

theorem HermitianMat.supportProj_eq_cfc {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] (A : HermitianMat n 𝕜) : A.supportProj = A.cfc fun (x : ℝ) => if x = 0 then 0 else 1

def HermitianMat.projLE {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] (A B : HermitianMat n 𝕜) : HermitianMat n 𝕜

Projector onto the non-negative eigenspace of B - A. Accessible by the notation {A ≤ₚ B}, which is scoped to HermitianMat. This is the unique maximum operator P such that P^2 = P and P * A * P ≤ P * B * P in the Loewner order.

Equations

• A.projLE B = (B - A).cfc fun (x : ℝ) => if 0 ≤ x then 1 else 0

noncomputable def HermitianMat.projLT {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] (A B : HermitianMat n 𝕜) : HermitianMat n 𝕜

Projector onto the positive eigenspace of B - A. Accessible by the notation {A <ₚ B}, which is scoped to HermitianMat. Compare with proj_le.

Equations

• A.projLT B = (B - A).cfc fun (x : ℝ) => if 0 < x then 1 else 0

def HermitianMat.«term{_≥ₚ_}» : Lean.ParserDescr

Equations

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

def HermitianMat.«term{_≤ₚ_}» : Lean.ParserDescr

Equations

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

def HermitianMat.«term{_>ₚ_}» : Lean.ParserDescr

Equations

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

def HermitianMat.«term{_<ₚ_}» : Lean.ParserDescr

Equations

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

theorem HermitianMat.projLE_def {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] (A B : HermitianMat n 𝕜) : A.projLE B = (B - A).cfc fun (x : ℝ) => if 0 ≤ x then 1 else 0

theorem HermitianMat.projLT_def {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] (A B : HermitianMat n 𝕜) : A.projLT B = (B - A).cfc fun (x : ℝ) => if 0 < x then 1 else 0

theorem HermitianMat.projLE_sq {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] (A B : HermitianMat n 𝕜) : A.projLE B ^ 2 = A.projLE B

theorem HermitianMat.projLT_sq {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] (A B : HermitianMat n 𝕜) : A.projLT B ^ 2 = A.projLT B

theorem HermitianMat.projLE_zero_cfc {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] (A : HermitianMat n 𝕜) : projLE 0 A = A.cfc fun (x : ℝ) => if 0 ≤ x then 1 else 0

theorem HermitianMat.projLT_zero_cfc {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] (A : HermitianMat n 𝕜) : projLT 0 A = A.cfc fun (x : ℝ) => if 0 < x then 1 else 0

theorem HermitianMat.projLE_zero_cfc' {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] (A : HermitianMat n 𝕜) : A.projLE 0 = A.cfc fun (x : ℝ) => if x ≤ 0 then 1 else 0

theorem HermitianMat.projLT_zero_cfc' {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] (A : HermitianMat n 𝕜) : A.projLT 0 = A.cfc fun (x : ℝ) => if x < 0 then 1 else 0

theorem HermitianMat.projLE_nonneg {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] (A B : HermitianMat n 𝕜) : 0 ≤ A.projLE B

theorem HermitianMat.projLT_nonneg {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] (A B : HermitianMat n 𝕜) : 0 ≤ A.projLT B

theorem HermitianMat.projLE_le_one {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] (A B : HermitianMat n 𝕜) : A.projLE B ≤ 1

theorem HermitianMat.projLE_mul_nonneg {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] (A B : HermitianMat n 𝕜) : 0 ≤ ↑(A.projLE B) * ↑(B - A)

theorem HermitianMat.projLE_mul_le {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] (A B : HermitianMat n 𝕜) : ↑(A.projLE B) * ↑A ≤ ↑(A.projLE B) * ↑B

@[simp]

theorem HermitianMat.proj_le_add_lt {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] (A B : HermitianMat n 𝕜) : A.projLT B + B.projLE A = 1

theorem HermitianMat.conj_lt_add_conj_le {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] (A : HermitianMat n 𝕜) : (conj ↑(A.projLT 0)) A + (conj ↑(projLE 0 A)) A = A

theorem HermitianMat.supportProj_eq_proj_lt_add_proj_lt {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] (A : HermitianMat n 𝕜) : A.supportProj = A.projLT 0 + projLT 0 A

instance HermitianMat.instPosPart {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] : PosPart (HermitianMat n 𝕜)

The positive part of a Hermitian matrix: the projection onto its positive eigenvalues.

Equations

• HermitianMat.instPosPart = { posPart := fun (A : HermitianMat n 𝕜) => A.cfc fun (x : ℝ) => max x 0 }

instance HermitianMat.instNegPart {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] : NegPart (HermitianMat n 𝕜)

The negative part of a Hermitian matrix: the projection onto its negative eigenvalues.

Equations

• HermitianMat.instNegPart = { negPart := fun (A : HermitianMat n 𝕜) => A.cfc fun (x : ℝ) => max (-x) 0 }

theorem HermitianMat.posPart_eq_cfc_max {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] (A : HermitianMat n 𝕜) : A⁺ = A.cfc fun (x : ℝ) => max x 0

theorem HermitianMat.negPart_eq_cfc_min {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] (A : HermitianMat n 𝕜) : A⁻ = A.cfc fun (x : ℝ) => max (-x) 0

theorem HermitianMat.posPart_eq_cfc_ite {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] (A : HermitianMat n 𝕜) : A⁺ = A.cfc fun (x : ℝ) => if 0 ≤ x then x else 0

theorem HermitianMat.negPart_eq_cfc_ite {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] (A : HermitianMat n 𝕜) : A⁻ = A.cfc fun (x : ℝ) => if x ≤ 0 then -x else 0

theorem HermitianMat.posPart_eq_posPart_toMat {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] (A : HermitianMat n 𝕜) : ↑A⁺ = (↑A)⁺

There is an existing (very slow) PosPart instance on Matrix n n 𝕜, this shows that this is equal.

theorem HermitianMat.negPart_eq_negPart_toMat {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] (A : HermitianMat n 𝕜) : ↑A⁻ = (↑A)⁻

There is an existing (very slow) PosPart instance on Matrix n n 𝕜, this shows that this is equal.

theorem HermitianMat.posPart_eq_cfc_lt {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] (A : HermitianMat n 𝕜) : A⁺ = A.cfc fun (x : ℝ) => if 0 < x then x else 0

The positive part can be equivalently described as the nonnegative part.

theorem HermitianMat.negPart_eq_cfc_lt {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] (A : HermitianMat n 𝕜) : A⁻ = A.cfc fun (x : ℝ) => if x < 0 then -x else 0

The negative part can be equivalently described as the nonpositive part.

theorem HermitianMat.posPart_add_negPart {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] (A : HermitianMat n 𝕜) : A⁺ - A⁻ = A

theorem HermitianMat.posPart_eq_self {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] {A : HermitianMat n 𝕜} (hA : 0 ≤ A) : A⁺ = A

theorem HermitianMat.posPart_nonneg {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] (A : HermitianMat n 𝕜) : 0 ≤ A⁺

theorem HermitianMat.negPart_nonneg {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] (A : HermitianMat n 𝕜) : 0 ≤ A⁻

theorem HermitianMat.posPart_le {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] (A : HermitianMat n 𝕜) : A ≤ A⁺

theorem HermitianMat.posPart_mul_negPart {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] (A : HermitianMat n 𝕜) : ↑A⁺ * ↑A⁻ = 0

theorem HermitianMat.projLE_inner_nonneg {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] (A B : HermitianMat n 𝕜) : 0 ≤ inner ℝ (A.projLE B) (B - A)

theorem HermitianMat.projLE_inner_le {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] (A B : HermitianMat n 𝕜) : inner ℝ (A.projLE B) A ≤ inner ℝ (A.projLE B) B

theorem HermitianMat.inner_projLE_nonneg {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] (A B : HermitianMat n 𝕜) : 0 ≤ inner ℝ (A.projLE B) (B - A)

theorem HermitianMat.inner_projLE_le {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] (A B : HermitianMat n 𝕜) : inner ℝ (A.projLE B) A ≤ inner ℝ (A.projLE B) B

theorem HermitianMat.posPart_Continuous {n : Type u_1} [Fintype n] [DecidableEq n] : Continuous fun (x : HermitianMat n ℂ) => x⁺

theorem HermitianMat.negPart_Continuous {n : Type u_1} [Fintype n] [DecidableEq n] : Continuous fun (x : HermitianMat n ℂ) => x⁻

theorem HermitianMat.one_sub_projLT {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] (A B : HermitianMat n 𝕜) : 1 - B.projLE A = A.projLT B

theorem HermitianMat.projLT_mul_nonneg {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] (A B : HermitianMat n 𝕜) : 0 ≤ ↑(A.projLT B) * ↑(B - A)

theorem HermitianMat.proj_lt_mul_lt {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] (A B : HermitianMat n 𝕜) : ↑(A.projLT B) * ↑A ≤ ↑(A.projLT B) * ↑B

theorem HermitianMat.inner_negPart_nonpos {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] (A : HermitianMat n 𝕜) : inner ℝ A A⁻ ≤ 0

@[simp]

theorem HermitianMat.posPart_inner_negPart_zero {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] (A : HermitianMat n 𝕜) : inner ℝ A⁺ A⁻ = 0

theorem HermitianMat.inner_negPart_zero_iff {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] (A : HermitianMat n 𝕜) : inner ℝ A A⁻ = 0 ↔ 0 ≤ A

theorem HermitianMat.inner_negPart_neg_iff {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] (A : HermitianMat n 𝕜) : inner ℝ A A⁻ < 0 ↔ ¬0 ≤ A

theorem HermitianMat.nonneg_iff_inner_nonneg {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] (A : HermitianMat n 𝕜) : 0 ≤ A ↔ ∀ (B : HermitianMat n 𝕜), 0 ≤ B → 0 ≤ inner ℝ A B

The self-duality of the PSD cone: a matrix is PSD iff its inner product with all nonnegative matrices is non-negative.