QuantumInfo.ForMathlib.Matrix

source

theorem Matrix.zero_rank_eq_zero {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [DecidableEq n] {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 : 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

theorem Matrix.IsHermitian.sum_eigenvalues_eq_trace {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [DecidableEq n] {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.eigenvalues_zero_eq_zero {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [DecidableEq n] {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_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 RCLike.normSq_eq_conj_mul_self {𝕜 : Type u_5} [RCLike 𝕜] {z : 𝕜} :

↑(normSq z) = (starRingEnd 𝕜) z * z

source

theorem Matrix.PosSemidef.outer_self_conj {n : Type u_4} {𝕜 : Type u_5} [Fintype n] [RCLike 𝕜] (v : n → 𝕜) :

(vecMulVec v ((starRingEnd (n → 𝕜)) v)).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 𝕜] [dm : DecidableEq m] (i j : m) {c : 𝕜} (hc : 0 < c) :

(single 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 𝕜] [dn : 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.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.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.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

theorem Matrix.PosDef.toLin_ker_eq_bot {n : Type u_3} {𝕜 : Type u_5} [Fintype n] [RCLike 𝕜] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.PosDef) :

LinearMap.ker (toLin' A) = ⊥

source

theorem Matrix.PosDef.of_toLin_ker_eq_bot {n : Type u_3} {𝕜 : Type u_5} [Fintype n] [RCLike 𝕜] [DecidableEq n] {A : Matrix n n 𝕜} (hA : LinearMap.ker (toLin' A) = ⊥) (hA₂ : A.PosSemidef) :

A.PosDef

source

theorem Matrix.PosDef.ker_range_antitone {d : Type u_6} [Fintype d] [DecidableEq d] {A B : Matrix d d ℂ} (hA : A.IsHermitian) (hB : B.IsHermitian) :

LinearMap.ker (toEuclideanLin A) ≤ LinearMap.ker (toEuclideanLin B) ↔ LinearMap.range (toEuclideanLin B) ≤ LinearMap.range (toEuclideanLin A)

source

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

IsOrderedCancelAddMonoid (Matrix n n 𝕜)

source

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

StarOrderedRing (Matrix n n 𝕜)

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

source

theorem Matrix.PosSemidef.le_of_nonneg_imp {n : Type u_3} {𝕜 : Type u_5} [Fintype n] [RCLike 𝕜] {A B : Matrix n n 𝕜} {R : Type u_6} [AddCommGroup R] [PartialOrder R] [IsOrderedAddMonoid 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_5} [Fintype n] [RCLike 𝕜] {R : Type u_6} [AddCommGroup R] [PartialOrder R] [IsOrderedAddMonoid 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.mul_mul_conjTranspose_mono {n : Type u_3} {m : Type u_4} {𝕜 : Type u_5} [Fintype n] [Fintype m] [RCLike 𝕜] {A B : Matrix n n 𝕜} (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} {m : Type u_4} {𝕜 : Type u_5} [Fintype n] [Fintype m] [RCLike 𝕜] {A B : Matrix n n 𝕜} (C : Matrix n m 𝕜) :

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

source

theorem Matrix.PosSemidef.nonneg_iff_eigenvalue_nonneg {n : Type u_3} {𝕜 : Type u_5} [Fintype n] [RCLike 𝕜] {A : Matrix n n 𝕜} (hA : A.IsHermitian) [DecidableEq n] :

0 ≤ A ↔ ∀ (x : n), 0 ≤ hA.eigenvalues x

source

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

Monotone diag

source

theorem Matrix.PosSemidef.diag_mono {n : Type u_3} {𝕜 : Type u_5} [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_5} [Fintype n] [RCLike 𝕜] :

Monotone trace

source

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

A ≤ B → A.trace ≤ B.trace

source

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

Monotone diagonal

source

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

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

source

theorem Matrix.PosSemidef.diagonal_le_iff {n : Type u_3} {𝕜 : Type u_5} [Fintype n] [RCLike 𝕜] [DecidableEq n] {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_5} [Fintype n] [RCLike 𝕜] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) (c : ℝ) :

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

source

theorem Matrix.PosSemidef.smul_one_le_of_eigenvalues_iff {n : Type u_3} {𝕜 : Type u_5} [Fintype n] [RCLike 𝕜] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) (c : ℝ) :

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

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 {𝕜 : Type u_2} [RCLike 𝕜] {d₁ : Type u_3} {d₂ : Type u_4} {A : Matrix (d₁ × d₂) (d₁ × d₂) 𝕜} [Fintype d₂] [Fintype d₁] [DecidableEq d₁] (hA : A.PosSemidef) :

A.traceLeft.PosSemidef

source

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

A.traceRight.PosSemidef

source

theorem Matrix.PosDef.kron {d₁ : Type u_3} {d₂ : Type u_4} {𝕜 : Type u_5} [Fintype d₁] [DecidableEq d₁] [Fintype d₂] [DecidableEq d₂] [RCLike 𝕜] {A : Matrix d₁ d₁ 𝕜} {B : Matrix d₂ d₂ 𝕜} (hA : A.PosDef) (hB : B.PosDef) :

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

source

theorem Matrix.PosDef.submatrix {d₁ : Type u_3} {d₂ : Type u_4} {𝕜 : Type u_5} [Fintype d₁] [DecidableEq d₁] [Fintype d₂] [DecidableEq d₂] [RCLike 𝕜] {M : Matrix d₁ d₁ 𝕜} (hM : M.PosDef) {e : d₂ → d₁} (he : Function.Injective e) :

(M.submatrix e e).PosDef

source

theorem Matrix.PosDef.reindex {d₁ : Type u_3} {d₂ : Type u_4} {𝕜 : Type u_5} [Fintype d₁] [DecidableEq d₁] [Fintype d₂] [DecidableEq d₂] [RCLike 𝕜] {M : Matrix d₁ d₁ 𝕜} (hM : M.PosDef) (e : d₁ ≃ d₂) :

((Matrix.reindex e e) M).PosDef

source

@[simp]

theorem Matrix.PosDef.reindex_iff {d₁ : Type u_3} {d₂ : Type u_4} {𝕜 : Type u_5} [Fintype d₁] [DecidableEq d₁] [Fintype d₂] [DecidableEq d₂] [RCLike 𝕜] {M : Matrix d₁ d₁ 𝕜} (e : d₁ ≃ d₂) :

((Matrix.reindex e e) M).PosDef ↔ M.PosDef

source

theorem Matrix.PosSemidef.rsmul {n : Type u_3} [Fintype n] {M : Matrix n n ℂ} (hM : M.PosSemidef) {c : ℝ} (hc : 0 ≤ c) :

(c • M).PosSemidef

source

theorem Matrix.PosDef.Convex {n : Type u_3} [Fintype n] :

_root_.Convex ℝ PosDef

source

theorem Matrix.PosDef_iff_eigenvalues' {d : Type u_3} {𝕜 : Type u_4} [Fintype d] [DecidableEq d] [RCLike 𝕜] (M : Matrix d d 𝕜) :

M.PosDef ↔ ∃ (h : M.IsHermitian), ∀ (i : d), 0 < h.eigenvalues i

source

theorem Matrix.IsHermitian.charpoly_roots_eq_eigenvalues {d : Type u_3} {𝕜 : Type u_4} [Fintype d] [DecidableEq d] [RCLike 𝕜] {M : Matrix d d 𝕜} (hM : M.IsHermitian) :

M.charpoly.roots = Multiset.map (RCLike.ofReal ∘ hM.eigenvalues) Finset.univ.val

source

theorem Multiset.map_univ_eq_iff {α : Type u_5} {β : Type u_6} [Fintype α] [DecidableEq β] (f g : α → β) :

map f Finset.univ.val = map g Finset.univ.val ↔ ∃ (e : α ≃ α), f = g ∘ ⇑e

source

theorem Matrix.IsHermitian.cfc_eigenvalues {d : Type u_3} {𝕜 : Type u_4} [Fintype d] [DecidableEq d] [RCLike 𝕜] {M : Matrix d d 𝕜} (hM : M.IsHermitian) (f : ℝ → ℝ) :

∃ (e : d ≃ d), eigenvalues ⋯ = f ∘ hM.eigenvalues ∘ ⇑e

source

@[simp]

theorem Matrix.toEuclideanLin_one {α : Type u_3} {n : Type u_4} [RCLike α] [Fintype n] [DecidableEq n] :

toEuclideanLin 1 = LinearMap.id

source

@[simp]

theorem Matrix.cfc_diagonal {d : Type u_3} {𝕜 : Type u_4} [Fintype d] [DecidableEq d] [RCLike 𝕜] (g : d → ℝ) (f : ℝ → ℝ) :

cfc f (diagonal fun (x : d) => ↑(g x)) = diagonal (RCLike.ofReal ∘ f ∘ g)

source

theorem Matrix.PosSemidef.pos_of_mem_spectrum {d : Type u_3} {𝕜 : Type u_4} [Fintype d] [DecidableEq d] [RCLike 𝕜] {A : Matrix d d 𝕜} (hA : A.PosSemidef) (r : ℝ) :

r ∈ spectrum ℝ A → 0 ≤ r

source

theorem Matrix.PosSemidef.pow_add {d : Type u_3} {𝕜 : Type u_4} [Fintype d] [DecidableEq d] [RCLike 𝕜] {A : Matrix d d 𝕜} (hA : A.PosSemidef) {x y : ℝ} (hxy : x + y ≠ 0) :

cfc (fun (x_1 : ℝ) => x_1 ^ (x + y)) A = cfc (fun (r : ℝ) => r ^ x * r ^ y) A

source

theorem Matrix.PosSemidef.pow_mul {d : Type u_3} {𝕜 : Type u_4} [Fintype d] [DecidableEq d] [RCLike 𝕜] {A : Matrix d d 𝕜} {x y : ℝ} (hA : A.PosSemidef) :

cfc (fun (x_1 : ℝ) => x_1 ^ (x * y)) A = cfc (fun (r : ℝ) => (r ^ x) ^ y) A

source

@[simp]

theorem Matrix.trace_submatrix {α : Type u_3} [AddCommMonoid α] {d₁ : Type u_4} {d₂ : Type u_5} [Fintype d₁] [Fintype d₂] (A : Matrix d₁ d₁ α) (e : d₂ ≃ d₁) :

(A.submatrix ⇑e ⇑e).trace = A.trace

source

theorem Matrix.spectrum_prod {d : Type u_3} {d₂ : Type u_4} [Fintype d] [DecidableEq d] [Fintype d₂] [DecidableEq d₂] {A : Matrix d d ℂ} {B : Matrix d₂ d₂ ℂ} (hA : A.IsHermitian) (hB : B.IsHermitian) :

spectrum ℝ (kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) A B) = spectrum ℝ A * spectrum ℝ B