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

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

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

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

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' := ⋯ }

@[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

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.

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.

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

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

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

@[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

theorem RCLike.normSq_eq_conj_mul_self {𝕜 : Type u_5} [RCLike 𝕜] {z : 𝕜} : ↑(normSq z) = (starRingEnd 𝕜) z * z

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

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

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

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.

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

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

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

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

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 = ⊥

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

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

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

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

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

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

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

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

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

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

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

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

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

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₂

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

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

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₁)

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₁)

@[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

@[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

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

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

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)

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)

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

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

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

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

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

@[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

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

theorem Matrix.PosDef.Convex {n : Type u_3} {𝕜 : Type u_4} [Fintype n] [RCLike 𝕜] : _root_.Convex ℝ PosDef

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

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

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.

@[simp]

theorem Matrix.toEuclideanLin_one {α : Type u_3} {n : Type u_4} [RCLike α] [Fintype n] [DecidableEq n] : toEuclideanLin 1 = LinearMap.id

@[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)

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

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

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

@[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

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

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

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)

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

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

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

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

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

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

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)

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)

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)

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.

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

@[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

@[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

@[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

@[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

@[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

@[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

@[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

@[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

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

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)

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

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

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

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

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