QuantumInfo.ForMathlib.Matrix

source

theorem Matrix.fromBlocks_gram_posSemidef {m : Type u_3} {n : Type u_4} {k : Type u_5} [Fintype m] [Fintype n] [Fintype k] (X : Matrix k n ℂ) (Y : Matrix k m ℂ) :

(fromBlocks (Y.conjTranspose * Y) (Y.conjTranspose * X) (X.conjTranspose * Y) (X.conjTranspose * X)).PosSemidef

The block Gram matrix [[YᴴY, YᴴX], [XᴴY, XᴴX]] is positive semidefinite.

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.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.Finsupp.sum_eq_ite {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [AddCommMonoid N] [Fintype α] [DecidableEq M] (f : α →₀ M) (g : α → M → N) :

f.sum g = ∑ i : α, if f i ≠ 0 then g i (f i) else 0

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} [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.pos_smul {m : Type u_3} {𝕜 : Type u_5} [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) :

(toLin' A).ker = ⊥

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 : (toLin' A).ker = ⊥) (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) :

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

source

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

Monotone diag

source

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

Monotone diagonal

source

theorem Matrix.PosSemidef.diagonal_mono {n : Type u_3} {𝕜 : Type u_5} [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} [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.trace_mul_kron_one_right {dB : Type u_4} {dA : Type u_5} [DecidableEq dB] [Fintype dA] [Fintype dB] {R : Type u_3} [Ring R] (M : Matrix (dA × dB) (dA × dB) R) (A : Matrix dA dA R) :

(M * kroneckerMap (fun (x1 x2 : R) => x1 * x2) A 1).trace = (M.traceRight * A).trace

Tr(M (A ⊗ I)) = Tr(Tr_B(M) A)

source

theorem Matrix.trace_mul_one_kron_right {dA : Type u_5} {dB : Type u_4} [DecidableEq dA] [Fintype dA] [Fintype dB] {R : Type u_3} [Ring R] (M : Matrix (dA × dB) (dA × dB) R) (B : Matrix dB dB R) :

(M * kroneckerMap (fun (x1 x2 : R) => x1 * x2) 1 B).trace = (M.traceLeft * B).trace

Tr(M (I ⊗ B)) = Tr(Tr_A(M) B)

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} {𝕜 : Type u_4} [Fintype n] [RCLike 𝕜] :

_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.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

theorem Matrix.IsHermitian.eigenvalues_eq_of_unitary_similarity_diagonal {d : Type u_5} {𝕜 : Type u_6} [Fintype d] [DecidableEq d] [RCLike 𝕜] {A : Matrix d d 𝕜} (hA : A.IsHermitian) {U : Matrix d d 𝕜} (hU : U ∈ unitaryGroup d 𝕜) {f : d → ℝ} (h : A = (U * diagonal fun (i : d) => ↑(f i)) * U.conjTranspose) :

∃ (σ : d ≃ d), hA.eigenvalues ∘ ⇑σ = f

If a Hermitian matrix A is unitarily similar to a diagonal matrix with real entries f, then the eigenvalues of A are a permutation of f.

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 {𝕜 : Type u_2} [RCLike 𝕜] {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

source

theorem Matrix.PosDef.zero_lt {n : Type u_3} [Nonempty n] [Fintype n] {A : Matrix n n ℂ} (hA : A.PosDef) :

0 < A

source

theorem Matrix.IsHermitian.spectrum_eq_image_eigenvalues {n : Type u_1} [DecidableEq n] [Fintype n] {A : Matrix n n ℂ} (hA : A.IsHermitian) :

spectrum ℝ A = ↑(Finset.image hA.eigenvalues Finset.univ)

source

theorem Matrix.IsHermitian.card_spectrum_eq_image {n : Type u_1} [DecidableEq n] [Fintype n] {A : Matrix n n ℂ} (hA : A.IsHermitian) [Fintype ↑(spectrum ℝ A)] :

Fintype.card ↑(spectrum ℝ A) = (Finset.image hA.eigenvalues Finset.univ).card

source

theorem Matrix.IsHermitian.sub_iInf_eignevalues {d : Type u_3} [Fintype d] [DecidableEq d] {A : Matrix d d ℂ} (hA : A.IsHermitian) :

(A - iInf hA.eigenvalues • 1).PosSemidef

source

theorem Matrix.IsHermitian.iInf_eigenvalues_le_dotProduct_mulVec {d : Type u_3} [Fintype d] [DecidableEq d] {A : Matrix d d ℂ} (hA : A.IsHermitian) (v : d → ℂ) :

↑(iInf hA.eigenvalues) * star v ⬝ᵥ v ≤ star v ⬝ᵥ A.mulVec v

source

theorem Matrix.IsHermitian.iInf_eigenvalues_le_of_posSemidef {d : Type u_3} [Fintype d] [DecidableEq d] {A B : Matrix d d ℂ} (hAB : (B - A).PosSemidef) (hA : A.IsHermitian) (hB : B.IsHermitian) :

iInf hA.eigenvalues ≤ iInf hB.eigenvalues

source

theorem Matrix.IsHermitian.iInf_eigenvalues_le {d : Type u_3} [Fintype d] [DecidableEq d] {A B : Matrix d d ℂ} (hAB : A ≤ B) (hA : A.IsHermitian) (hB : B.IsHermitian) :

iInf hA.eigenvalues ≤ iInf hB.eigenvalues

source

theorem Matrix.IsHermitian.iInf_eigenvalues_smul_one_le {d : Type u_3} [Fintype d] [DecidableEq d] {A : Matrix d d ℂ} (hA : A.IsHermitian) :

iInf hA.eigenvalues • 1 ≤ A

source

theorem Matrix.IsHermitian.spectrum_subset_Ici_of_sub {d : Type u_3} {𝕜 : Type u_4} [Fintype d] [DecidableEq d] [RCLike 𝕜] {A x : Matrix d d 𝕜} (hA : A.IsHermitian) (hl : (x - A).PosSemidef) :

spectrum ℝ x ⊆ Set.Ici (⨅ (i : d), hA.eigenvalues i)

source

theorem Matrix.IsHermitian.spectrum_subset_Iic_of_sub {d : Type u_3} {𝕜 : Type u_4} [Fintype d] [DecidableEq d] [RCLike 𝕜] {A x : Matrix d d 𝕜} (hA : A.IsHermitian) (hl : (A - x).PosSemidef) :

spectrum ℝ x ⊆ Set.Iic (⨆ (i : d), hA.eigenvalues i)

source

theorem Matrix.IsHermitian.spectrum_subset_of_mem_Icc {d : Type u_3} {𝕜 : Type u_4} [Fintype d] [DecidableEq d] [RCLike 𝕜] {A B x : Matrix d d 𝕜} (hA : A.IsHermitian) (hB : B.IsHermitian) (hl : (x - A).PosSemidef) (hr : (B - x).PosSemidef) :

spectrum ℝ x ⊆ Set.Icc (⨅ (i : d), hA.eigenvalues i) (⨆ (i : d), hB.eigenvalues i)

source

theorem Matrix.traceRight_eq_traceLeft_reindex {n : Type u_3} {m : Type u_4} {R : Type u_5} [Fintype m] [AddCommMonoid R] (M : Matrix (n × m) (n × m) R) :

M.traceRight = ((reindex (Equiv.prodComm n m) (Equiv.prodComm n m)) M).traceLeft

The right partial trace of a matrix is equal to the left partial trace of the matrix reindexed by swapping the tensor factors.

source

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

0 < A.trace

source

@[simp]

theorem Matrix.traceLeft_add {n : Type u_1} {m : Type u_3} {α : Type u_4} [AddCommGroup α] [Fintype m] {A B : Matrix (m × n) (m × n) α} :

(A + B).traceLeft = A.traceLeft + B.traceLeft

source

@[simp]

theorem Matrix.traceLeft_neg {n : Type u_1} {m : Type u_3} {α : Type u_4} [AddCommGroup α] [Fintype m] {A : Matrix (m × n) (m × n) α} :

(-A).traceLeft = -A.traceLeft

source

@[simp]

theorem Matrix.traceLeft_sub {n : Type u_1} {m : Type u_3} {α : Type u_4} [AddCommGroup α] [Fintype m] {A B : Matrix (m × n) (m × n) α} :

(A - B).traceLeft = A.traceLeft - B.traceLeft

source

@[simp]

theorem Matrix.traceRight_add {n : Type u_1} {m : Type u_3} {α : Type u_4} [AddCommGroup α] [Fintype m] {A B : Matrix (n × m) (n × m) α} :

(A + B).traceRight = A.traceRight + B.traceRight

source

@[simp]

theorem Matrix.traceRight_neg {n : Type u_1} {m : Type u_3} {α : Type u_4} [AddCommGroup α] [Fintype m] {A : Matrix (n × m) (n × m) α} :

(-A).traceRight = -A.traceRight

source

@[simp]

theorem Matrix.traceRight_sub {n : Type u_1} {m : Type u_3} {α : Type u_4} [AddCommGroup α] [Fintype m] {A B : Matrix (n × m) (n × m) α} :

(A - B).traceRight = A.traceRight - B.traceRight

source

@[simp]

theorem Matrix.traceLeft_smul {n : Type u_1} {m : Type u_3} {α : Type u_4} [AddCommGroup α] [Fintype m] {R : Type u_5} [DistribSMul R α] {A : Matrix (m × n) (m × n) α} (r : R) :

(r • A).traceLeft = r • A.traceLeft

source

@[simp]

theorem Matrix.traceRight_smul {n : Type u_1} {m : Type u_3} {α : Type u_4} [AddCommGroup α] [Fintype m] {R : Type u_5} [DistribSMul R α] {A : Matrix (n × m) (n × m) α} (r : R) :

(r • A).traceRight = r • A.traceRight

source

theorem Matrix.unitaryGroup_row_norm {n : Type u_1} [DecidableEq n] [Fintype n] (U : ↥(unitaryGroup n ℂ)) (i : n) :

∑ j : n, ‖↑U j i‖ ^ 2 = 1

source

def Matrix.piProd {ι : Type u_3} {d : ι → Type u_4} [fι : Fintype ι] {R : Type u_5} [CommMonoid R] (A : (i : ι) → Matrix (d i) (d i) R) :

Matrix ((i : ι) → d i) ((i : ι) → d i) R

Equations

Matrix.piProd A = Matrix.of fun (j k : (i : ι) → d i) => ∏ i : ι, A i (j i) (k i)

Instances For

source

theorem Matrix.IsHermitian.piProd {ι : Type u_3} {d : ι → Type u_4} [fι : Fintype ι] {R : Type u_5} {A : (i : ι) → Matrix (d i) (d i) R} [CommSemiring R] [StarRing R] (hA : ∀ (i : ι), (A i).IsHermitian) :

(Matrix.piProd A).IsHermitian

source

theorem Matrix.trace_piProd {ι : Type u_3} {d : ι → Type u_4} [fι : Fintype ι] {R : Type u_5} {A : (i : ι) → Matrix (d i) (d i) R} [DecidableEq ι] [(i : ι) → Fintype (d i)] [CommSemiring R] :

(piProd A).trace = ∏ i : ι, (A i).trace

source

theorem Matrix.PosSemidef.piProd {ι : Type u_3} {d : ι → Type u_4} [fι : Fintype ι] {R : Type u_5} {A : (i : ι) → Matrix (d i) (d i) R} [DecidableEq ι] [(i : ι) → Fintype (d i)] [RCLike R] (hA : ∀ (i : ι), (A i).PosSemidef) :

(Matrix.piProd A).PosSemidef

source

theorem Matrix.submatrix_eq_mul_mul {d : Type u_3} {d₂ : Type u_4} {d₃ : Type u_5} {R : Type u_6} [DecidableEq d] [Fintype d] [Semiring R] (A : Matrix d d R) (e : d₂ → d) (f : d₃ → d) :

A.submatrix e f = submatrix 1 e id * A * submatrix 1 id f

source

theorem Matrix.kronecker_conj_eq {m : Type u_3} {n : Type u_4} {p : Type u_5} {q : Type u_6} {α : Type u_7} [CommSemiring α] [StarRing α] [Fintype m] [Fintype n] (A : Matrix m m α) (B : Matrix n n α) (C : Matrix p m α) (D : Matrix q n α) :

kroneckerMap (fun (x1 x2 : α) => x1 * x2) C D * kroneckerMap (fun (x1 x2 : α) => x1 * x2) A B * (kroneckerMap (fun (x1 x2 : α) => x1 * x2) C D).conjTranspose = kroneckerMap (fun (x1 x2 : α) => x1 * x2) (C * A * C.conjTranspose) (D * B * D.conjTranspose)

The conjugate of a Kronecker product by a Kronecker product is the Kronecker product of the conjugates (for matrices).