QuantumInfo.ForMathlib.HermitianMat.Proj

The positive parts, or equivalently the projections, of Hermitian matrices onto each other.

def HermitianMat.proj_le {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.proj_le B = (B - A).cfc fun (x : ℝ) => if 0 ≤ x then 1 else 0

Instances For

source

noncomputable def HermitianMat.proj_lt {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.proj_lt B = (B - A).cfc fun (x : ℝ) => if 0 < x then 1 else 0

Instances For

source

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

Lean.ParserDescr

Equations

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

Instances For

source

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

Lean.ParserDescr

Equations

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

Instances For

source

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

Lean.ParserDescr

Equations

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

Instances For

source

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

Lean.ParserDescr

Equations

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

Instances For

source

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

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

source

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

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

source

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

A.proj_le B ^ 2 = A.proj_le B

source

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

A.proj_lt B ^ 2 = A.proj_lt B

source

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

proj_le 0 A = A.cfc fun (x : ℝ) => if 0 ≤ x then 1 else 0

source

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

proj_lt 0 A = A.cfc fun (x : ℝ) => if 0 < x then 1 else 0

source

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

A.proj_le 0 = A.cfc fun (x : ℝ) => if x ≤ 0 then 1 else 0

source

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

A.proj_lt 0 = A.cfc fun (x : ℝ) => if x < 0 then 1 else 0

source

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

0 ≤ A.proj_le B

source

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

0 ≤ A.proj_lt B

source

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

A.proj_le B ≤ 1

source

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

0 ≤ ↑(A.proj_le B) * ↑(B - A)

source

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

↑(A.proj_le B) * ↑A ≤ ↑(A.proj_le B) * ↑B

source

@[simp]

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

A.proj_lt B + B.proj_le A = 1

source

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

(conj ↑(A.proj_lt 0)) A + (conj ↑(proj_le 0 A)) A = A

source

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

HermitianMat n 𝕜

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

Equations

A.proj_pos = A.cfc fun (x : ℝ) => max x 0

Instances For

source

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

HermitianMat n 𝕜

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

Equations

A.proj_neg = A.cfc fun (x : ℝ) => max (-x) 0

Instances For

source

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

PosPart (HermitianMat n 𝕜)

Equations

HermitianMat.instPosPart = { posPart := HermitianMat.proj_pos }

source

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

NegPart (HermitianMat n 𝕜)

Equations

HermitianMat.instNegPart = { negPart := HermitianMat.proj_neg }

source

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

source

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

source

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

source

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

source

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.

source

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.

source

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.

source

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.

source

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

A⁺ - A⁻ = A

source

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

0 ≤ A⁺

source

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

0 ≤ A⁻

source

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

A ≤ A⁺

source

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

↑A⁺ * ↑A⁻ = 0

source

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

0 ≤ (A.proj_le B).inner (B - A)

source

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

(A.proj_le B).inner A ≤ (A.proj_le B).inner B

source

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

0 ≤ Inner.inner ℝ (A.proj_le B) (B - A)

source

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

Inner.inner ℝ (A.proj_le B) A ≤ Inner.inner ℝ (A.proj_le B) B

source

theorem HermitianMat.posPart_Continuous {n : Type u_1} [Fintype n] [DecidableEq n] :

Continuous fun (x : HermitianMat n ℂ) => x⁺

source

theorem HermitianMat.negPart_Continuous {n : Type u_1} [Fintype n] [DecidableEq n] :

Continuous fun (x : HermitianMat n ℂ) => x⁻