QuantumInfo.ForMathlib.Matrix

source

theorem Matrix.zero_rank_eq_zero {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {A : Matrix n n 𝕜} [Fintype n] (hA : A.rank = 0) :

A = 0

source

theorem Matrix.IsHermitian.smul_selfAdjoint {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {A : Matrix n n 𝕜} (hA : A.IsHermitian) {c : 𝕜} (hc : _root_.IsSelfAdjoint c) :

(c • A).IsHermitian

source

theorem Matrix.IsHermitian.smul_im_zero {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {A : Matrix n n 𝕜} (hA : A.IsHermitian) {c : 𝕜} (h : RCLike.im c = 0) :

(c • A).IsHermitian

source

theorem Matrix.IsHermitian.smul_real {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {A : Matrix n n 𝕜} (hA : A.IsHermitian) (c : ℝ) :

(c • A).IsHermitian

source

def Matrix.IsHermitian.HermitianSubspace (n : Type u_3) (𝕜 : Type u_4) [Fintype n] [RCLike 𝕜] :

Subspace ℝ (Matrix n n 𝕜)

Equations

Matrix.IsHermitian.HermitianSubspace n 𝕜 = { carrier := {A : Matrix n n 𝕜 | A.IsHermitian}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

Instances For

source

@[simp]

theorem Matrix.IsHermitian.re_trace_eq_trace {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {A : Matrix n n 𝕜} (hA : A.IsHermitian) [Fintype n] :

↑(RCLike.re A.trace) = A.trace

source

def Matrix.IsHermitian.rtrace {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] {A : Matrix n n 𝕜} :

A.IsHermitian → ℝ

The trace of a Hermitian matrix, as a real number.

Equations

x✝.rtrace = RCLike.re A.trace

Instances For

source

@[simp]

theorem Matrix.IsHermitian.rtrace_eq_trace {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {A : Matrix n n 𝕜} (hA : A.IsHermitian) [Fintype n] :

↑hA.rtrace = A.trace

source

theorem Matrix.IsHermitian.sum_eigenvalues_eq_trace {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {A : Matrix n n 𝕜} (hA : A.IsHermitian) [Fintype n] :

↑(∑ i : n, hA.eigenvalues i) = A.trace

The sum of the eigenvalues of a Hermitian matrix is equal to its trace.

source

theorem Matrix.IsHermitian.sum_eigenvalues_eq_rtrace {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {A : Matrix n n 𝕜} (hA : A.IsHermitian) [Fintype n] :

∑ i : n, hA.eigenvalues i = hA.rtrace

source

theorem Matrix.IsHermitian.eigenvalues_zero_eq_zero {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {A : Matrix n n 𝕜} (hA : A.IsHermitian) [Fintype n] (h : ∀ (i : n), hA.eigenvalues i = 0) :

A = 0

If all eigenvalues are equal to zero, then the matrix is zero.

source

theorem Matrix.kroneckerMap_conjTranspose {R : Type u_3} {m : Type u_4} {n : Type u_1} [CommRing R] [StarRing R] (A : Matrix m m R) (B : Matrix n n R) :

(kroneckerMap (fun (x1 x2 : R) => x1 * x2) A B).conjTranspose = kroneckerMap (fun (x1 x2 : R) => x1 * x2) A.conjTranspose B.conjTranspose

source

theorem Matrix.kroneckerMap_IsHermitian {R : Type u_3} {m : Type u_4} {n : Type u_1} [CommRing R] [StarRing R] {A : Matrix m m R} {B : Matrix n n R} (hA : A.IsHermitian) (hB : B.IsHermitian) :

(kroneckerMap (fun (x1 x2 : R) => x1 * x2) A B).IsHermitian

source

theorem Matrix.PosSemidef.diag_nonneg {m : Type u_3} {𝕜 : Type u_5} [Fintype m] [RCLike 𝕜] {A : Matrix m m 𝕜} (hA : A.PosSemidef) (i : m) :

0 ≤ A.diag i

source

theorem Matrix.PosSemidef.trace_nonneg {m : Type u_3} {𝕜 : Type u_5} [Fintype m] [RCLike 𝕜] {A : Matrix m m 𝕜} (hA : A.PosSemidef) :

0 ≤ A.trace

source

theorem Matrix.PosSemidef.trace_zero {m : Type u_3} {𝕜 : Type u_5} [Fintype m] [RCLike 𝕜] {A : Matrix m m 𝕜} (hA : A.PosSemidef) :

A.trace = 0 → A = 0

source

@[simp]

theorem Matrix.PosSemidef.trace_zero_iff {m : Type u_3} {𝕜 : Type u_5} [Fintype m] [RCLike 𝕜] {A : Matrix m m 𝕜} (hA : A.PosSemidef) :

A.trace = 0 ↔ A = 0

source

theorem Matrix.PosSemidef.rtrace_nonneg {m : Type u_3} {𝕜 : Type u_5} [Fintype m] [RCLike 𝕜] {A : Matrix m m 𝕜} (hA : A.PosSemidef) :

0 ≤ ⋯.rtrace

source

@[simp]

theorem Matrix.PosSemidef.rtrace_zero_iff {m : Type u_3} {𝕜 : Type u_5} [Fintype m] [RCLike 𝕜] {A : Matrix m m 𝕜} (hA : A.PosSemidef) :

⋯.rtrace = 0 ↔ A = 0

source

theorem Matrix.PosSemidef.smul {m : Type u_3} {𝕜 : Type u_5} [Fintype m] [RCLike 𝕜] {A : Matrix m m 𝕜} (hA : A.PosSemidef) {c : 𝕜} (h : 0 ≤ c) :

(c • A).PosSemidef

source

theorem Matrix.PosSemidef.convex_cone {m : Type u_3} {𝕜 : Type u_5} [Fintype m] [RCLike 𝕜] {A B : Matrix m m 𝕜} (hA : A.PosSemidef) (hB : B.PosSemidef) {c₁ c₂ : 𝕜} (hc₁ : 0 ≤ c₁) (hc₂ : 0 ≤ c₂) :

(c₁ • A + c₂ • B).PosSemidef

source

theorem Matrix.PosSemidef.stdBasisMatrix_iff_eq {m : Type u_3} {𝕜 : Type u_5} [Fintype m] [RCLike 𝕜] (i j : m) {c : 𝕜} (hc : 0 < c) :

(stdBasisMatrix i j c).PosSemidef ↔ i = j

A standard basis matrix (with a positive entry) is positive semidefinite iff the entry is on the diagonal.

source

theorem Matrix.PosSemidef.PosSemidef_kronecker {m : Type u_3} {n : Type u_4} {𝕜 : Type u_5} [Fintype m] [Fintype n] [RCLike 𝕜] [DecidableEq n] {A : Matrix m m 𝕜} {B : Matrix n n 𝕜} (hA : A.PosSemidef) (hB : B.PosSemidef) :

(kroneckerMap (fun (x1 x2 : 𝕜) => x1 * x2) A B).PosSemidef

source

theorem Matrix.PosSemidef.sqrt_eq {m : Type u_3} {𝕜 : Type u_5} [Fintype m] [RCLike 𝕜] {A B : Matrix m m 𝕜} (h : A = B) (hA : A.PosSemidef) (hB : B.PosSemidef) :

hA.sqrt = hB.sqrt

source

theorem Matrix.PosSemidef.sqrt_eq' {m : Type u_3} {𝕜 : Type u_5} [Fintype m] [RCLike 𝕜] {A B : Matrix m m 𝕜} (h : A = B) (hA : A.PosSemidef) :

hA.sqrt = (⋯ : B.PosSemidef).sqrt

source

@[simp]

theorem Matrix.PosSemidef.sqrt_0 {n : Type u_4} {𝕜 : Type u_5} [Fintype n] [RCLike 𝕜] [DecidableEq n] :

(⋯ : PosSemidef 0).sqrt = 0

source

@[simp]

theorem Matrix.PosSemidef.sqrt_1 {n : Type u_4} {𝕜 : Type u_5} [Fintype n] [RCLike 𝕜] [DecidableEq n] :

(⋯ : PosSemidef 1).sqrt = 1

source

theorem Matrix.PosSemidef.nonneg_smul {m : Type u_3} {𝕜 : Type u_5} [Fintype m] [RCLike 𝕜] {A : Matrix m m 𝕜} {c : 𝕜} (hA : A.PosSemidef) (hc : 0 ≤ c) :

(c • A).PosSemidef

source

theorem Matrix.PosSemidef.pos_smul {m : Type u_3} {𝕜 : Type u_5} [Fintype m] [RCLike 𝕜] {A : Matrix m m 𝕜} {c : 𝕜} (hA : (c • A).PosSemidef) (hc : 0 < c) :

A.PosSemidef

source

theorem Matrix.PosSemidef.nonneg_smul_Real_smul {m : Type u_3} {𝕜 : Type u_5} [Fintype m] [RCLike 𝕜] {A : Matrix m m 𝕜} {c : ℝ} (hA : A.PosSemidef) (hc : 0 ≤ c) :

(c • A).PosSemidef

source

theorem Matrix.PosSemidef.pos_Real_smul {m : Type u_3} {𝕜 : Type u_5} [Fintype m] [RCLike 𝕜] {A : Matrix m m 𝕜} {c : ℝ} (hA : (c • A).PosSemidef) (hc : 0 < c) :

A.PosSemidef

source

theorem Matrix.PosSemidef.sqrt_nonneg_smul {m : Type u_3} {𝕜 : Type u_5} [Fintype m] [RCLike 𝕜] {A : Matrix m m 𝕜} {c : 𝕜} (hA : (c ^ 2 • A).PosSemidef) (hc : 0 < c) :

hA.sqrt = c • (⋯ : A.PosSemidef).sqrt

source

theorem Matrix.PosSemidef.zero_dotProduct_zero_iff {m : Type u_3} {𝕜 : Type u_5} [Fintype m] [RCLike 𝕜] {A : Matrix m m 𝕜} (hA : A.PosSemidef) :

(∀ (x : m → 𝕜), 0 = star x ⬝ᵥ A.mulVec x) ↔ A = 0

source

theorem Matrix.PosSemidef.zero_posSemidef_neg_posSemidef_iff {m : Type u_3} {𝕜 : Type u_5} [Fintype m] [RCLike 𝕜] {A : Matrix m m 𝕜} :

A.PosSemidef ∧ (-A).PosSemidef ↔ A = 0

source

instance Matrix.PosSemidef.instOrderedCancelAddCommMonoid {n : Type u_3} {𝕜 : Type u_4} [Fintype n] [RCLike 𝕜] :

OrderedCancelAddCommMonoid (Matrix n n 𝕜)

Loewner partial order of square matrices induced by positive-semi-definiteness: A ≤ B ↔ (B - A).PosSemidef alongside properties that make it an "OrderedCancelAddCommMonoid" TODO : Equivalence to CStarAlgebra.spectralOrder

Equations

Matrix.PosSemidef.instOrderedCancelAddCommMonoid = OrderedCancelAddCommMonoid.mk ⋯

source

theorem Matrix.PosSemidef.le_iff_sub_posSemidef {n : Type u_3} {𝕜 : Type u_4} [Fintype n] [RCLike 𝕜] {A B : Matrix n n 𝕜} :

A ≤ B ↔ (B - A).PosSemidef

source

theorem Matrix.PosSemidef.zero_le_iff_posSemidef {n : Type u_3} {𝕜 : Type u_4} [Fintype n] [RCLike 𝕜] {A : Matrix n n 𝕜} :

0 ≤ A ↔ A.PosSemidef

source

instance Matrix.PosSemidef.instStarOrderedRing {n : Type u_3} {𝕜 : Type u_4} [Fintype n] [RCLike 𝕜] :

StarOrderedRing (Matrix n n 𝕜)

Basically, the instance states A ≤ B ↔ B = A + Sᴴ * S

source

instance Matrix.PosSemidef.instNonnegSpectrumClass {n : Type u_3} {𝕜 : Type u_4} [Fintype n] [RCLike 𝕜] :

NonnegSpectrumClass ℝ (Matrix n n 𝕜)

Basically, the instance states 0 ≤ A → ∀ x ∈ spectrum ℝ A, 0 ≤ x

source

theorem Matrix.PosSemidef.le_iff_sub_nonneg {n : Type u_3} {𝕜 : Type u_4} [Fintype n] [RCLike 𝕜] {A B : Matrix n n 𝕜} :

A ≤ B ↔ 0 ≤ B - A

source

theorem Matrix.PosSemidef.le_of_nonneg_imp {n : Type u_3} {𝕜 : Type u_4} [Fintype n] [RCLike 𝕜] {A B : Matrix n n 𝕜} {R : Type u_5} [OrderedAddCommGroup R] (f : Matrix n n 𝕜 →+ R) (h : ∀ (A : Matrix n n 𝕜), A.PosSemidef → 0 ≤ f A) :

A ≤ B → f A ≤ f B

source

theorem Matrix.PosSemidef.le_of_nonneg_imp' {n : Type u_3} {𝕜 : Type u_4} [Fintype n] [RCLike 𝕜] {R : Type u_5} [OrderedAddCommGroup R] {x y : R} (f : R →+ Matrix n n 𝕜) (h : ∀ (x : R), 0 ≤ x → (f x).PosSemidef) :

x ≤ y → f x ≤ f y

source

theorem Matrix.PosSemidef.diag_monotone {n : Type u_3} {𝕜 : Type u_4} [Fintype n] [RCLike 𝕜] :

Monotone diag

source

theorem Matrix.PosSemidef.diag_mono {n : Type u_3} {𝕜 : Type u_4} [Fintype n] [RCLike 𝕜] {A B : Matrix n n 𝕜} :

A ≤ B → ∀ (i : n), A.diag i ≤ B.diag i

source

theorem Matrix.PosSemidef.trace_monotone {n : Type u_3} {𝕜 : Type u_4} [Fintype n] [RCLike 𝕜] :

Monotone trace

source

theorem Matrix.PosSemidef.trace_mono {n : Type u_3} {𝕜 : Type u_4} [Fintype n] [RCLike 𝕜] {A B : Matrix n n 𝕜} :

A ≤ B → A.trace ≤ B.trace

source

theorem Matrix.PosSemidef.mul_mul_conjTranspose_mono {n : Type u_3} {𝕜 : Type u_4} [Fintype n] [RCLike 𝕜] {A B : Matrix n n 𝕜} {m : Type u_5} [Fintype m] (C : Matrix m n 𝕜) :

A ≤ B → C * A * C.conjTranspose ≤ C * B * C.conjTranspose

source

theorem Matrix.PosSemidef.conjTranspose_mul_mul_mono {n : Type u_3} {𝕜 : Type u_4} [Fintype n] [RCLike 𝕜] {A B : Matrix n n 𝕜} {m : Type u_5} [Fintype m] (C : Matrix n m 𝕜) :

A ≤ B → C.conjTranspose * A * C ≤ C.conjTranspose * B * C

source

theorem Matrix.PosSemidef.diagonal_monotone {n : Type u_3} {𝕜 : Type u_4} [Fintype n] [RCLike 𝕜] :

Monotone diagonal

source

theorem Matrix.PosSemidef.diagonal_mono {n : Type u_3} {𝕜 : Type u_4} [Fintype n] [RCLike 𝕜] {d₁ d₂ : n → 𝕜} :

d₁ ≤ d₂ → diagonal d₁ ≤ diagonal d₂

source

theorem Matrix.PosSemidef.diagonal_le_iff {n : Type u_3} {𝕜 : Type u_4} [Fintype n] [RCLike 𝕜] {d₁ d₂ : n → 𝕜} :

d₁ ≤ d₂ ↔ diagonal d₁ ≤ diagonal d₂

source

theorem Matrix.PosSemidef.le_smul_one_of_eigenvalues_iff {n : Type u_3} {𝕜 : Type u_4} [Fintype n] [RCLike 𝕜] {A : Matrix n n 𝕜} (hA : A.PosSemidef) (c : ℝ) :

(∀ (i : n), ⋯.eigenvalues i ≤ c) ↔ A ≤ c • 1

source

theorem Matrix.PosSemidef.le_trace_smul_one {n : Type u_3} {𝕜 : Type u_4} [Fintype n] [RCLike 𝕜] {A : Matrix n n 𝕜} (hA : A.PosSemidef) :

A ≤ ⋯.rtrace • 1

source

def Matrix.traceLeft {R : Type u_3} {d : Type u_4} [AddCommMonoid R] [Fintype d] {d₁ : Type u_5} {d₂ : Type u_6} (m : Matrix (d × d₁) (d × d₂) R) :

Matrix d₁ d₂ R

Equations

m.traceLeft = Matrix.of fun (i₁ : d₁) (j₁ : d₂) => ∑ i₂ : d, m (i₂, i₁) (i₂, j₁)

Instances For

source

def Matrix.traceRight {R : Type u_3} {d : Type u_4} [AddCommMonoid R] [Fintype d] {d₁ : Type u_5} {d₂ : Type u_6} (m : Matrix (d₁ × d) (d₂ × d) R) :

Matrix d₁ d₂ R

Equations

m.traceRight = Matrix.of fun (i₂ : d₁) (j₂ : d₂) => ∑ i₁ : d, m (i₂, i₁) (j₂, i₁)

Instances For

source

@[simp]

theorem Matrix.traceLeft_trace {R : Type u_5} {d₁ : Type u_4} {d₂ : Type u_3} [AddCommMonoid R] [Fintype d₁] [Fintype d₂] (A : Matrix (d₁ × d₂) (d₁ × d₂) R) :

A.traceLeft.trace = A.trace

source

@[simp]

theorem Matrix.traceRight_trace {R : Type u_5} {d₁ : Type u_4} {d₂ : Type u_3} [AddCommMonoid R] [Fintype d₁] [Fintype d₂] (A : Matrix (d₁ × d₂) (d₁ × d₂) R) :

A.traceRight.trace = A.trace

source

theorem Matrix.IsHermitian.traceLeft {R : Type u_5} {d : Type u_4} [AddCommMonoid R] [Fintype d] [StarAddMonoid R] {d₁ : Type u_3} {A : Matrix (d × d₁) (d × d₁) R} (hA : A.IsHermitian) :

A.traceLeft.IsHermitian

source

theorem Matrix.IsHermitian.traceRight {R : Type u_5} {d : Type u_4} [AddCommMonoid R] [Fintype d] [StarAddMonoid R] {d₁ : Type u_3} {A : Matrix (d₁ × d) (d₁ × d) R} (hA : A.IsHermitian) :

A.traceRight.IsHermitian

source

theorem Matrix.PosSemidef.traceLeft {d₁ : Type u_4} {d₂ : Type u_3} {𝕜 : Type u_2} [RCLike 𝕜] {A : Matrix (d₁ × d₂) (d₁ × d₂) 𝕜} [Fintype d₂] [Fintype d₁] (hA : A.PosSemidef) :

A.traceLeft.PosSemidef

source

theorem Matrix.PosSemidef.traceRight {d₁ : Type u_4} {d₂ : Type u_3} {𝕜 : Type u_2} [RCLike 𝕜] {A : Matrix (d₁ × d₂) (d₁ × d₂) 𝕜} [Fintype d₂] [Fintype d₁] (hA : A.PosSemidef) :

A.traceRight.PosSemidef