QuantumInfo.ForMathlib.HermitianMat.Basic

def HermitianMat (n : Type u_1) (α : Type u_2) [AddGroup α] [StarAddMonoid α] :

Type (max u_1 u_2)

The type of Hermitian matrices, as a Subtype. Equivalent to a Matrix n n α bundled with the fact that Matrix.IsHermitian.

Equations

HermitianMat n α = ↥(selfAdjoint (Matrix n n α))

Instances For

source

theorem HermitianMat.eq_IsHermitian {α : Type u_1} {n : Type u_5} [AddGroup α] [StarAddMonoid α] :

HermitianMat n α = { m : Matrix n n α // m.IsHermitian }

source

def HermitianMat.mat {α : Type u_1} {n : Type u_5} [AddGroup α] [StarAddMonoid α] :

HermitianMat n α → Matrix n n α

Equations

HermitianMat.mat = Subtype.val

Instances For

source

instance HermitianMat.instCoeMatrix {α : Type u_1} {n : Type u_5} [AddGroup α] [StarAddMonoid α] :

Coe (HermitianMat n α) (Matrix n n α)

Equations

HermitianMat.instCoeMatrix = { coe := HermitianMat.mat }

source

@[simp]

theorem HermitianMat.val_eq_coe {α : Type u_1} {n : Type u_5} [AddGroup α] [StarAddMonoid α] (A : HermitianMat n α) :

↑A = ↑A

source

@[simp]

theorem HermitianMat.mat_mk {α : Type u_1} {n : Type u_5} [AddGroup α] [StarAddMonoid α] (x : Matrix n n α) (h : x ∈ selfAdjoint (Matrix n n α)) :

↑⟨x, h⟩ = x

source

@[simp]

theorem HermitianMat.mk_mat {α : Type u_1} {n : Type u_5} [AddGroup α] [StarAddMonoid α] {A : HermitianMat n α} (h : (↑A).IsHermitian) :

⟨↑A, h⟩ = A

source

theorem HermitianMat.H {α : Type u_1} {n : Type u_5} [AddGroup α] [StarAddMonoid α] (A : HermitianMat n α) :

(↑A).IsHermitian

Alias for HermitianMat.property or HermitianMat.2, this gets the fact that the value is actually IsHermitian.

source

theorem HermitianMat.ext {α : Type u_1} {n : Type u_5} [AddGroup α] [StarAddMonoid α] {A B : HermitianMat n α} :

↑A = ↑B → A = B

source

theorem HermitianMat.ext_iff {α : Type u_1} {n : Type u_5} [AddGroup α] [StarAddMonoid α] {A B : HermitianMat n α} :

A = B ↔ ↑A = ↑B

source

instance HermitianMat.instFun {α : Type u_1} {n : Type u_5} [AddGroup α] [StarAddMonoid α] :

FunLike (HermitianMat n α) n (n → α)

Equations

HermitianMat.instFun = { coe := fun (M : HermitianMat n α) => ↑M, coe_injective' := ⋯ }

source

@[simp]

theorem HermitianMat.mat_apply {α : Type u_1} {n : Type u_5} [AddGroup α] [StarAddMonoid α] {A : HermitianMat n α} {i j : n} :

↑A i j = A i j

source

@[simp]

theorem HermitianMat.conjTranspose_mat {α : Type u_1} {n : Type u_5} [AddGroup α] [StarAddMonoid α] (A : HermitianMat n α) :

(↑A).conjTranspose = ↑A

source

instance HermitianMat.instAddGroup {α : Type u_1} {n : Type u_5} [AddGroup α] [StarAddMonoid α] :

AddGroup (HermitianMat n α)

Equations

HermitianMat.instAddGroup = (selfAdjoint (Matrix n n α)).toAddGroup

source

instance HermitianMat.instUniqueOfIsEmpty {α : Type u_1} {n : Type u_5} [AddGroup α] [StarAddMonoid α] [IsEmpty n] :

Unique (HermitianMat n α)

Equations

HermitianMat.instUniqueOfIsEmpty = { default := 0, uniq := ⋯ }

source

@[simp]

theorem HermitianMat.mat_zero {α : Type u_1} {n : Type u_5} [AddGroup α] [StarAddMonoid α] :

↑0 = 0

source

@[simp]

theorem HermitianMat.mk_zero {α : Type u_1} {n : Type u_5} [AddGroup α] [StarAddMonoid α] (h : Matrix.IsHermitian 0) :

⟨0, h⟩ = 0

source

@[simp]

theorem HermitianMat.zero_apply {𝕜 : Type u_3} {n : Type u_5} [RCLike 𝕜] (i j : n) :

0 i j = 0

source

@[simp]

theorem HermitianMat.mat_add {α : Type u_1} {n : Type u_5} [AddGroup α] [StarAddMonoid α] (A B : HermitianMat n α) :

↑(A + B) = ↑A + ↑B

source

@[simp]

theorem HermitianMat.mat_sub {α : Type u_1} {n : Type u_5} [AddGroup α] [StarAddMonoid α] (A B : HermitianMat n α) :

↑(A - B) = ↑A - ↑B

source

@[simp]

theorem HermitianMat.mat_neg {α : Type u_1} {n : Type u_5} [AddGroup α] [StarAddMonoid α] (A : HermitianMat n α) :

↑(-A) = -↑A

source

instance HermitianMat.instSMul {α : Type u_1} {R : Type u_2} {n : Type u_5} [Star R] [TrivialStar R] [AddGroup α] [StarAddMonoid α] [SMul R α] [StarModule R α] :

SMul R (HermitianMat n α)

Equations

HermitianMat.instSMul = { smul := fun (c : R) (A : HermitianMat n α) => ⟨c • ↑A, ⋯⟩ }

source

@[simp]

theorem HermitianMat.mat_smul {α : Type u_1} {R : Type u_2} {n : Type u_5} [Star R] [TrivialStar R] [AddGroup α] [StarAddMonoid α] [SMul R α] [StarModule R α] (c : R) (A : HermitianMat n α) :

↑(c • A) = c • ↑A

source

@[simp]

theorem HermitianMat.smul_apply {α : Type u_1} {R : Type u_2} {n : Type u_5} [Star R] [TrivialStar R] [AddGroup α] [StarAddMonoid α] [SMul R α] [StarModule R α] (c : R) (A : HermitianMat n α) (i j : n) :

(c • A) i j = c • A i j

source

instance HermitianMat.instTopologicalSpace {α : Type u_1} {n : Type u_5} [AddGroup α] [StarAddMonoid α] [TopologicalSpace α] :

TopologicalSpace (HermitianMat n α)

Equations

HermitianMat.instTopologicalSpace = inferInstanceAs (TopologicalSpace ↥(selfAdjoint (Matrix n n α)))

source

theorem HermitianMat.continuous_mat {α : Type u_1} {n : Type u_5} [AddGroup α] [StarAddMonoid α] [TopologicalSpace α] :

Continuous mat

source

theorem HermitianMat.continuousOn_iff_coe {α : Type u_1} {n : Type u_5} [AddGroup α] [StarAddMonoid α] [TopologicalSpace α] {X : Type u_6} [TopologicalSpace X] {s : Set X} (f : X → HermitianMat n α) :

ContinuousOn f s ↔ ContinuousOn (fun (x : X) => ↑(f x)) s

source

instance HermitianMat.instContinuousAdd {α : Type u_1} {n : Type u_5} [AddGroup α] [StarAddMonoid α] [TopologicalSpace α] [IsTopologicalAddGroup α] :

ContinuousAdd (HermitianMat n α)

source

instance HermitianMat.instContinuousNeg {α : Type u_1} {n : Type u_5} [AddGroup α] [StarAddMonoid α] [TopologicalSpace α] [IsTopologicalAddGroup α] :

ContinuousNeg (HermitianMat n α)

source

instance HermitianMat.instIsTopologicalAddGroup {α : Type u_1} {n : Type u_5} [AddGroup α] [StarAddMonoid α] [TopologicalSpace α] [IsTopologicalAddGroup α] :

IsTopologicalAddGroup (HermitianMat n α)

source

instance HermitianMat.instContinuousSMul {α : Type u_1} {R : Type u_2} {n : Type u_5} [Star R] [TrivialStar R] [AddGroup α] [StarAddMonoid α] [TopologicalSpace α] [TopologicalSpace R] [SMul R α] [ContinuousSMul R α] [StarModule R α] :

ContinuousSMul R (HermitianMat n α)

source

instance HermitianMat.instIsTopologicalAddGroup_1 {𝕜 : Type u_3} {n : Type u_5} [RCLike 𝕜] :

IsTopologicalAddGroup (HermitianMat n 𝕜)

source

instance HermitianMat.instContinuousSMulRealComplex {n : Type u_5} :

ContinuousSMul ℝ (HermitianMat n ℂ)

source

instance HermitianMat.instT3Space {𝕜 : Type u_3} {n : Type u_5} [RCLike 𝕜] :

T3Space (HermitianMat n 𝕜)

source

instance HermitianMat.instMulAction {α : Type u_1} {R : Type u_2} {n : Type u_5} [Star R] [TrivialStar R] [AddGroup α] [StarAddMonoid α] [Monoid R] [MulAction R α] [StarModule R α] :

MulAction R (HermitianMat n α)

Equations

HermitianMat.instMulAction = Function.Injective.mulAction Subtype.val ⋯ ⋯

source

instance HermitianMat.instAddCommGroup {α : Type u_1} {n : Type u_5} [AddCommGroup α] [StarAddMonoid α] :

AddCommGroup (HermitianMat n α)

Equations

HermitianMat.instAddCommGroup = (selfAdjoint (Matrix n n α)).toAddCommGroup

source

@[simp]

theorem HermitianMat.mat_finset_sum {α : Type u_1} {n : Type u_5} [AddCommGroup α] [StarAddMonoid α] {ι : Type u_6} (f : ι → HermitianMat n α) (s : Finset ι) :

↑(∑ i ∈ s, f i) = ∑ i ∈ s, ↑(f i)

source

instance HermitianMat.instModule {α : Type u_1} {R : Type u_2} {n : Type u_5} [Star R] [TrivialStar R] [AddCommGroup α] [StarAddMonoid α] [Semiring R] [Module R α] [StarModule R α] :

Module R (HermitianMat n α)

Equations

HermitianMat.instModule = inferInstanceAs (Module R ↥(selfAdjoint (Matrix n n α)))

source

def HermitianMat.matₗ {α : Type u_1} {R : Type u_2} {n : Type u_5} [Star R] [TrivialStar R] [AddCommGroup α] [StarAddMonoid α] [Semiring R] [Module R α] [StarModule R α] [TopologicalSpace α] :

HermitianMat n α →L[R] Matrix n n α

The projection from HermitianMat to Matrix, as a continuous linear map.

Equations

HermitianMat.matₗ = { toFun := HermitianMat.mat, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

Instances For

source

@[simp]

theorem HermitianMat.matₗ_apply {α : Type u_1} {R : Type u_2} {n : Type u_5} [Star R] [TrivialStar R] [AddCommGroup α] [StarAddMonoid α] [Semiring R] [Module R α] [StarModule R α] [TopologicalSpace α] (a✝ : HermitianMat n α) :

matₗ a✝ = ↑a✝

source

instance HermitianMat.instOne {α : Type u_1} {n : Type u_5} [NonAssocRing α] [StarRing α] [DecidableEq n] :

One (HermitianMat n α)

Equations

HermitianMat.instOne = { one := ⟨1, ⋯⟩ }

source

@[simp]

theorem HermitianMat.mat_one {α : Type u_1} {n : Type u_5} [NonAssocRing α] [StarRing α] [DecidableEq n] :

↑1 = 1

source

@[simp]

theorem HermitianMat.mk_one {α : Type u_1} {n : Type u_5} [NonAssocRing α] [StarRing α] [DecidableEq n] (h : Matrix.IsHermitian 1) :

⟨1, h⟩ = 1

source

@[simp]

theorem HermitianMat.one_apply {α : Type u_1} {n : Type u_5} [NonAssocRing α] [StarRing α] [DecidableEq n] (i j : n) :

1 i j = 1 i j

source

noncomputable instance HermitianMat.instAddCommMonoidWithOne {𝕜 : Type u_3} {n : Type u_5} [RCLike 𝕜] [DecidableEq n] :

AddCommMonoidWithOne (HermitianMat n 𝕜)

Equations

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

source

instance HermitianMat.instNeZeroOfNatOfNonempty {𝕜 : Type u_3} {n : Type u_5} [RCLike 𝕜] [DecidableEq n] [i : Nonempty n] :

NeZero 1

source

noncomputable instance HermitianMat.instInv {α : Type u_1} {m : Type u_4} [CommRing α] [StarRing α] [DecidableEq m] [Fintype m] :

Inv (HermitianMat m α)

Equations

HermitianMat.instInv = { inv := fun (x : HermitianMat m α) => ⟨(↑x)⁻¹, ⋯⟩ }

source

@[simp]

theorem HermitianMat.mat_inv {α : Type u_1} {m : Type u_4} [CommRing α] [StarRing α] [DecidableEq m] [Fintype m] (A : HermitianMat m α) :

↑A⁻¹ = (↑A)⁻¹

source

@[simp]

theorem HermitianMat.zero_inv {α : Type u_1} {m : Type u_4} [CommRing α] [StarRing α] [DecidableEq m] [Fintype m] :

0⁻¹ = 0

source

@[simp]

theorem HermitianMat.one_inv {α : Type u_1} {m : Type u_4} [CommRing α] [StarRing α] [DecidableEq m] [Fintype m] :

1⁻¹ = 1

source

noncomputable instance HermitianMat.instPow {α : Type u_1} {m : Type u_4} [CommRing α] [StarRing α] [DecidableEq m] [Fintype m] :

Pow (HermitianMat m α) ℕ

Equations

HermitianMat.instPow = { pow := fun (x : HermitianMat m α) (n : ℕ) => ⟨↑x ^ n, ⋯⟩ }

source

@[simp]

theorem HermitianMat.mat_pow {α : Type u_1} {m : Type u_4} [CommRing α] [StarRing α] [DecidableEq m] [Fintype m] (A : HermitianMat m α) (n : ℕ) :

↑(A ^ n) = ↑A ^ n

source

@[simp]

theorem HermitianMat.pow_zero {α : Type u_1} {m : Type u_4} [CommRing α] [StarRing α] [DecidableEq m] [Fintype m] (A : HermitianMat m α) :

A ^ 0 = 1

source

@[simp]

theorem HermitianMat.zero_pow {α : Type u_1} {m : Type u_4} [CommRing α] [StarRing α] [DecidableEq m] [Fintype m] (n : ℕ) (hn : n ≠ 0) :

0 ^ n = 0

source

@[simp]

theorem HermitianMat.one_pow {α : Type u_1} {m : Type u_4} [CommRing α] [StarRing α] [DecidableEq m] [Fintype m] (n : ℕ) :

1 ^ n = 1

source

noncomputable instance HermitianMat.instZPow {α : Type u_1} {m : Type u_4} [CommRing α] [StarRing α] [DecidableEq m] [Fintype m] :

Pow (HermitianMat m α) ℤ

Equations

HermitianMat.instZPow = { pow := fun (x : HermitianMat m α) (z : ℤ) => ⟨↑x ^ z, ⋯⟩ }

source

@[simp]

theorem HermitianMat.mat_zpow {α : Type u_1} {m : Type u_4} [CommRing α] [StarRing α] [DecidableEq m] [Fintype m] (A : HermitianMat m α) (z : ℤ) :

↑(A ^ z) = ↑A ^ z

source

@[simp]

theorem HermitianMat.zpow_natCast {α : Type u_1} {m : Type u_4} [CommRing α] [StarRing α] [DecidableEq m] [Fintype m] (A : HermitianMat m α) (n : ℕ) :

A ^ ↑n = A ^ n

source

@[simp]

theorem HermitianMat.zpow_zero {α : Type u_1} {m : Type u_4} [CommRing α] [StarRing α] [DecidableEq m] [Fintype m] (A : HermitianMat m α) :

A ^ 0 = 1

source

@[simp]

theorem HermitianMat.zpow_one {α : Type u_1} {m : Type u_4} [CommRing α] [StarRing α] [DecidableEq m] [Fintype m] (A : HermitianMat m α) :

A ^ 1 = A

source

@[simp]

theorem HermitianMat.one_zpow {α : Type u_1} {m : Type u_4} [CommRing α] [StarRing α] [DecidableEq m] [Fintype m] (z : ℤ) :

1 ^ z = 1

source

@[simp]

theorem HermitianMat.zpow_neg_one {α : Type u_1} {m : Type u_4} [CommRing α] [StarRing α] [DecidableEq m] [Fintype m] (A : HermitianMat m α) :

A ^ (-1) = A⁻¹

source

@[simp]

theorem HermitianMat.inv_zpow {α : Type u_1} {m : Type u_4} [CommRing α] [StarRing α] [DecidableEq m] [Fintype m] (A : HermitianMat m α) (z : ℤ) :

A⁻¹ ^ z = (A ^ z)⁻¹

source

theorem Matrix.inv_commute {m : Type u_4} [DecidableEq m] [Fintype m] {α : Type u_6} {A : Matrix m m α} [CommRing α] :

Commute A⁻¹ A

source

theorem HermitianMat.commute_inv_self {α : Type u_1} {m : Type u_4} [CommRing α] [StarRing α] [DecidableEq m] [Fintype m] (A : HermitianMat m α) :

Commute ↑A⁻¹ ↑A

source

theorem HermitianMat.commute_self_inv {α : Type u_1} {m : Type u_4} [CommRing α] [StarRing α] [DecidableEq m] [Fintype m] (A : HermitianMat m α) :

Commute ↑A ↑A⁻¹

source

instance HermitianMat.FiniteDimensional {𝕜 : Type u_3} {n : Type u_5} [RCLike 𝕜] [Finite n] :

_root_.FiniteDimensional ℝ (HermitianMat n 𝕜)

source

@[simp]

theorem HermitianMat.im_diag_eq_zero {𝕜 : Type u_3} {n : Type u_5} [RCLike 𝕜] (A : HermitianMat n 𝕜) (x : n) :

RCLike.im (A x x) = 0

source

@[simp]

theorem HermitianMat.complex_im_eq_zero {n : Type u_5} (A : HermitianMat n ℂ) (x : n) :

(A x x).im = 0

source

def HermitianMat.conj {α : Type u_1} {n : Type u_5} [CommRing α] [StarRing α] [Fintype n] {m : Type u_6} (B : Matrix m n α) :

HermitianMat n α →+ HermitianMat m α

The Hermitian matrix given by conjugating by a (possibly rectangular) Matrix. If we required B to be square, this would apply to any Semigroup+StarMul (as proved by IsSelfAdjoint.conjugate). But this lets us conjugate to other sizes too, as is done in e.g. Kraus operators. That is, it's a heterogeneous conjguation.

Equations

HermitianMat.conj B = { toFun := fun (A : HermitianMat n α) => ⟨B * ↑A * B.conjTranspose, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }

Instances For

source

theorem HermitianMat.conj_apply {α : Type u_1} {m : Type u_4} {n : Type u_5} [CommRing α] [StarRing α] [Fintype n] (B : Matrix m n α) (A : HermitianMat n α) :

(conj B) A = ⟨B * ↑A * B.conjTranspose, ⋯⟩

source

@[simp]

theorem HermitianMat.conj_apply_mat {α : Type u_1} {m : Type u_4} {n : Type u_5} [CommRing α] [StarRing α] [Fintype n] (B : Matrix m n α) (A : HermitianMat n α) :

↑((conj B) A) = B * ↑A * B.conjTranspose

source

theorem HermitianMat.conj_conj {α : Type u_1} {n : Type u_5} [CommRing α] [StarRing α] [Fintype n] (A : HermitianMat n α) {m : Type u_6} {l : Type u_7} [Fintype m] (B : Matrix m n α) (C : Matrix l m α) :

(conj C) ((conj B) A) = (conj (C * B)) A

source

@[simp]

theorem HermitianMat.conj_zero {α : Type u_1} {m : Type u_4} {n : Type u_5} [CommRing α] [StarRing α] [Fintype n] (A : HermitianMat n α) [DecidableEq n] :

(conj 0) A = 0

source

@[simp]

theorem HermitianMat.conj_one {α : Type u_1} {n : Type u_5} [CommRing α] [StarRing α] [Fintype n] (A : HermitianMat n α) [DecidableEq n] :

(conj 1) A = A

source

@[simp]

theorem HermitianMat.conj_one_unitary {α : Type u_1} {n : Type u_5} [CommRing α] [StarRing α] [Fintype n] [DecidableEq n] (U : ↥(Matrix.unitaryGroup n α)) :

(conj ↑U) 1 = 1

source

def HermitianMat.conjLinear {α : Type u_1} {n : Type u_5} [CommRing α] [StarRing α] [Fintype n] (R : Type u_6) [Star R] [TrivialStar R] [CommSemiring R] [Algebra R α] [StarModule R α] {m : Type u_7} (B : Matrix m n α) :

HermitianMat n α →ₗ[R] HermitianMat m α

HermitianMat.conj as an R-linear map, where R is the ring of relevant reals.

Equations

HermitianMat.conjLinear R B = { toAddHom := ↑(HermitianMat.conj B), map_smul' := ⋯ }

Instances For

source

@[simp]

theorem HermitianMat.conjLinear_apply {α : Type u_1} {m : Type u_4} {n : Type u_5} [CommRing α] [StarRing α] [Fintype n] (A : HermitianMat n α) (R : Type u_6) [Star R] [TrivialStar R] [CommSemiring R] [Algebra R α] [StarModule R α] (B : Matrix m n α) :

(conjLinear R B) A = (conj B) A

source

theorem HermitianMat.continuous_conj {𝕜 : Type u_3} {m : Type u_4} {n : Type u_5} [RCLike 𝕜] [Fintype n] (ρ : HermitianMat n 𝕜) :

Continuous fun (x : Matrix m n 𝕜) => (conj x) ρ

source

instance HermitianMat.instFaithfulSMulRealOfNonempty {𝕜 : Type u_3} {n : Type u_5} [RCLike 𝕜] [DecidableEq n] [i : Nonempty n] :

FaithfulSMul ℝ (HermitianMat n 𝕜)

source

def HermitianMat.lin {𝕜 : Type u_3} {n : Type u_5} [RCLike 𝕜] [Fintype n] [DecidableEq n] (A : HermitianMat n 𝕜) :

EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n

The continuous linear map associated with a Hermitian matrix.

Equations

A.lin = { toLinearMap := Matrix.toEuclideanLin ↑A, cont := ⋯ }

Instances For

source

@[simp]

theorem HermitianMat.isSymmetric {𝕜 : Type u_3} {n : Type u_5} [RCLike 𝕜] [Fintype n] [DecidableEq n] (A : HermitianMat n 𝕜) :

(↑A.lin).IsSymmetric

source

@[simp]

theorem HermitianMat.lin_zero {𝕜 : Type u_3} {n : Type u_5} [RCLike 𝕜] [Fintype n] [DecidableEq n] :

lin 0 = 0

source

@[simp]

theorem HermitianMat.lin_one {𝕜 : Type u_3} {n : Type u_5} [RCLike 𝕜] [Fintype n] [DecidableEq n] :

lin 1 = 1

source

noncomputable def HermitianMat.eigenspace {𝕜 : Type u_3} {n : Type u_5} [RCLike 𝕜] [Fintype n] [DecidableEq n] (A : HermitianMat n 𝕜) (μ : 𝕜) :

Submodule 𝕜 (EuclideanSpace 𝕜 n)

Equations

A.eigenspace μ = Module.End.eigenspace (↑A.lin) μ

Instances For

source

def HermitianMat.ker {𝕜 : Type u_3} {n : Type u_5} [RCLike 𝕜] [Fintype n] [DecidableEq n] (A : HermitianMat n 𝕜) :

Submodule 𝕜 (EuclideanSpace 𝕜 n)

The kernel of a Hermitian matrix A as a submodule of Euclidean space, defined by LinearMap.ker A.toMat.toEuclideanLin. Equivalently, the zero-eigenspace.

Equations

A.ker = (↑A.lin).ker

Instances For

source

theorem HermitianMat.mem_ker_iff_mulVec_zero {𝕜 : Type u_3} {n : Type u_5} [RCLike 𝕜] [Fintype n] [DecidableEq n] (A : HermitianMat n 𝕜) (x : EuclideanSpace 𝕜 n) :

x ∈ A.ker ↔ (↑A).mulVec x.ofLp = 0

source

theorem HermitianMat.ker_eq_eigenspace_zero {𝕜 : Type u_3} {n : Type u_5} [RCLike 𝕜] [Fintype n] [DecidableEq n] (A : HermitianMat n 𝕜) :

A.ker = A.eigenspace 0

The kernel of a Hermitian matrix is its zero eigenspace.

source

@[simp]

theorem HermitianMat.ker_zero {𝕜 : Type u_3} {n : Type u_5} [RCLike 𝕜] [Fintype n] [DecidableEq n] :

ker 0 = ⊤

source

@[simp]

theorem HermitianMat.ker_one {𝕜 : Type u_3} {n : Type u_5} [RCLike 𝕜] [Fintype n] [DecidableEq n] :

ker 1 = ⊥

source

theorem HermitianMat.ker_pos_smul {𝕜 : Type u_3} {n : Type u_5} [RCLike 𝕜] [Fintype n] [DecidableEq n] (A : HermitianMat n 𝕜) {c : ℝ} (hc : c ≠ 0) :

(c • A).ker = A.ker

source

def HermitianMat.support {𝕜 : Type u_3} {n : Type u_5} [RCLike 𝕜] [Fintype n] [DecidableEq n] (A : HermitianMat n 𝕜) :

Submodule 𝕜 (EuclideanSpace 𝕜 n)

The support of a Hermitian matrix A as a submodule of Euclidean space, defined by LinearMap.range A.toMat.toEuclideanLin. Equivalently, the sum of all nonzero eigenspaces.

Equations

A.support = (↑A.lin).range

Instances For

source

theorem HermitianMat.support_eq_sup_eigenspace_nonzero {𝕜 : Type u_3} {n : Type u_5} [RCLike 𝕜] [Fintype n] [DecidableEq n] (A : HermitianMat n 𝕜) :

A.support = ⨆ (μ : 𝕜), ⨆ (_ : μ ≠ 0), A.eigenspace μ

The support of a Hermitian matrix is the sum of its nonzero eigenspaces.

source

@[simp]

theorem HermitianMat.support_zero {𝕜 : Type u_3} {n : Type u_5} [RCLike 𝕜] [Fintype n] [DecidableEq n] :

support 0 = ⊥

source

@[simp]

theorem HermitianMat.support_one {𝕜 : Type u_3} {n : Type u_5} [RCLike 𝕜] [Fintype n] [DecidableEq n] :

support 1 = ⊤

source

@[simp]

theorem HermitianMat.ker_orthogonal_eq_support {𝕜 : Type u_3} {n : Type u_5} [RCLike 𝕜] [Fintype n] [DecidableEq n] (A : HermitianMat n 𝕜) :

A.kerᗮ = A.support

source

@[simp]

theorem HermitianMat.support_orthogonal_eq_range {𝕜 : Type u_3} {n : Type u_5} [RCLike 𝕜] [Fintype n] [DecidableEq n] (A : HermitianMat n 𝕜) :

A.supportᗮ = A.ker

source

def HermitianMat.diagonal {n : Type u_5} (𝕜 : Type u_6) [RCLike 𝕜] [DecidableEq n] (f : n → ℝ) :

HermitianMat n 𝕜

Equations

HermitianMat.diagonal 𝕜 f = ⟨Matrix.diagonal fun (x : n) => ↑(f x), ⋯⟩

Instances For

source

@[simp]

theorem HermitianMat.diagonal_mat {n : Type u_5} {𝕜 : Type u_6} [RCLike 𝕜] [DecidableEq n] (f : n → ℝ) :

↑(diagonal 𝕜 f) = Matrix.diagonal fun (x : n) => ↑(f x)

source

@[simp]

theorem HermitianMat.diagonal_zero {n : Type u_5} {𝕜 : Type u_6} [RCLike 𝕜] [DecidableEq n] :

diagonal 𝕜 0 = 0

source

@[simp]

theorem HermitianMat.diagonal_one {n : Type u_5} {𝕜 : Type u_6} [RCLike 𝕜] [DecidableEq n] :

diagonal 𝕜 1 = 1

source

theorem HermitianMat.diagonal_add {n : Type u_5} {𝕜 : Type u_6} [RCLike 𝕜] [DecidableEq n] (f g : n → ℝ) :

diagonal 𝕜 (f + g) = diagonal 𝕜 f + diagonal 𝕜 g

source

theorem HermitianMat.diagonal_add_apply {n : Type u_5} {𝕜 : Type u_6} [RCLike 𝕜] [DecidableEq n] (f g : n → ℝ) :

(diagonal 𝕜 fun (x : n) => f x + g x) = diagonal 𝕜 f + diagonal 𝕜 g

source

theorem HermitianMat.diagonal_sub {n : Type u_5} {𝕜 : Type u_6} [RCLike 𝕜] [DecidableEq n] (f g : n → ℝ) :

diagonal 𝕜 (f - g) = diagonal 𝕜 f - diagonal 𝕜 g

source

theorem HermitianMat.diagonal_mul {n : Type u_5} {𝕜 : Type u_6} [RCLike 𝕜] [DecidableEq n] (f : n → ℝ) (c : ℝ) :

(diagonal 𝕜 fun (x : n) => c * f x) = c • diagonal 𝕜 f

source

theorem HermitianMat.diagonal_conj_diagonal {n : Type u_5} {𝕜 : Type u_6} [RCLike 𝕜] [DecidableEq n] (f g : n → ℝ) [Fintype n] :

(conj ↑(diagonal 𝕜 g)) (diagonal 𝕜 f) = diagonal 𝕜 fun (i : n) => f i * g i ^ 2

source

theorem HermitianMat.eq_conj_diagonal {n : Type u_5} {𝕜 : Type u_6} [RCLike 𝕜] [DecidableEq n] [Fintype n] (A : HermitianMat n 𝕜) :

A = (conj ↑⋯.eigenvectorUnitary) (diagonal 𝕜 ⋯.eigenvalues)

A Hermitian matrix is equal to its diagonalization conjugated by its eigenvector unitary matrix.

source

def HermitianMat.kronecker {α : Type u_1} {m : Type u_4} {n : Type u_5} [CommRing α] [StarRing α] (A : HermitianMat m α) (B : HermitianMat n α) :

HermitianMat (m × n) α

The kronecker product of two HermitianMats, see Matrix.kroneckerMap.

Equations

A.kronecker B = ⟨Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) ↑A ↑B, ⋯⟩

Instances For

source

def HermitianMat.«term_⊗ₖ_» :

Lean.TrailingParserDescr

The kronecker product of two HermitianMats, see Matrix.kroneckerMap.

Equations

HermitianMat.«term_⊗ₖ_» = Lean.ParserDescr.trailingNode `HermitianMat.«term_⊗ₖ_» 100 100 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊗ₖ ") (Lean.ParserDescr.cat `term 101))

Instances For

source

@[simp]

theorem HermitianMat.kronecker_mat {α : Type u_1} {m : Type u_4} {n : Type u_5} [CommRing α] [StarRing α] (A : HermitianMat m α) (B : HermitianMat n α) :

↑(A.kronecker B) = Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) ↑A ↑B

source

@[simp]

theorem HermitianMat.zero_kronecker {α : Type u_1} {m : Type u_4} {n : Type u_5} [CommRing α] [StarRing α] (A : HermitianMat m α) :

kronecker 0 A = 0

source

@[simp]

theorem HermitianMat.kronecker_zero {α : Type u_1} {m : Type u_4} {n : Type u_5} [CommRing α] [StarRing α] (A : HermitianMat m α) :

A.kronecker 0 = 0

source

@[simp]

theorem HermitianMat.kronecker_one_one {α : Type u_1} {m : Type u_4} {n : Type u_5} [CommRing α] [StarRing α] [DecidableEq m] [DecidableEq n] :

kronecker 1 1 = 1

source

theorem HermitianMat.add_kronecker {α : Type u_1} {m : Type u_4} {n : Type u_5} [CommRing α] [StarRing α] (A B : HermitianMat m α) (C : HermitianMat n α) :

(A + B).kronecker C = A.kronecker C + B.kronecker C

source

theorem HermitianMat.kronecker_add {α : Type u_1} {m : Type u_4} {n : Type u_5} [CommRing α] [StarRing α] (A : HermitianMat m α) (B C : HermitianMat n α) :

A.kronecker (B + C) = A.kronecker B + A.kronecker C

source

theorem HermitianMat.kronecker_diagonal {𝕜 : Type u_3} {m : Type u_4} {n : Type u_5} [RCLike 𝕜] [DecidableEq m] [DecidableEq n] (d₁ : m → ℝ) (d₂ : n → ℝ) :

(diagonal 𝕜 d₁).kronecker (diagonal 𝕜 d₂) = diagonal 𝕜 fun (i : m × n) => d₁ i.1 * d₂ i.2

source

theorem HermitianMat.kron_commute {α : Type u_1} {m : Type u_4} {n : Type u_5} [CommRing α] [StarRing α] [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] {A C : HermitianMat m α} {B D : HermitianMat n α} (hAC : Commute ↑A ↑C) (hBD : Commute ↑B ↑D) :

Commute ↑(A.kronecker B) ↑(C.kronecker D)

A ⊗ₖ B always commutes with C ⊗ₖ D if the pairs commute.

source

theorem HermitianMat.kron_id_commute_id_kro {α : Type u_1} {m : Type u_4} {n : Type u_5} [CommRing α] [StarRing α] [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] (A : HermitianMat m α) (B : HermitianMat n α) :

Commute ↑(A.kronecker 1) ↑(kronecker 1 B)

A ⊗ₖ 1 always commutes with 1 ⊗ₖ B

source

theorem HermitianMat.kronecker_conj {α : Type u_1} {m : Type u_4} {n : Type u_5} {p : Type u_6} {q : Type u_7} [CommRing α] [StarRing α] [Fintype m] [Fintype n] (A : HermitianMat m α) (B : HermitianMat n α) (C : Matrix p m α) (D : Matrix q n α) :

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

source

theorem HermitianMat.range_le_ker_imp_zero {𝕜 : Type u_3} [RCLike 𝕜] {d : Type u_6} [Fintype d] [DecidableEq d] {A : HermitianMat d 𝕜} (h : (Matrix.toEuclideanLin ↑A).range ≤ (Matrix.toEuclideanLin ↑A).ker) :

A = 0

source

theorem Matrix.range_mul_conjTranspose_of_ker_le_ker {𝕜 : Type u_3} [RCLike 𝕜] {d : Type u_6} {d₂ : Type u_7} [Fintype d] [DecidableEq d] [Fintype d₂] [DecidableEq d₂] {A : Matrix d d 𝕜} {M : Matrix d₂ d 𝕜} (h : (toEuclideanLin M).ker ≤ (toEuclideanLin A).ker) :

(toEuclideanLin (A * M.conjTranspose)).range = (toEuclideanLin A).range

If ker M ⊆ ker A, then range (A Mᴴ) = range A.

source

theorem HermitianMat.conj_ne_zero {𝕜 : Type u_3} [RCLike 𝕜] {d : Type u_6} {d₂ : Type u_7} [Fintype d] [DecidableEq d] [Fintype d₂] [DecidableEq d₂] {A : HermitianMat d 𝕜} {M : Matrix d₂ d 𝕜} (hA : A ≠ 0) (h : (Matrix.toEuclideanLin M).ker ≤ A.ker) :

(conj M) A ≠ 0

source

theorem HermitianMat.conj_ne_zero_iff {𝕜 : Type u_3} [RCLike 𝕜] {d : Type u_6} {d₂ : Type u_7} [Fintype d] [DecidableEq d] [Fintype d₂] [DecidableEq d₂] {A : HermitianMat d 𝕜} {M : Matrix d₂ d 𝕜} (h : (Matrix.toEuclideanLin M).ker ≤ A.ker) :

(conj M) A ≠ 0 ↔ A ≠ 0

source

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

RCLike.ofReal '' spectrum ℝ A = spectrum 𝕜 A

source

@[simp]

theorem HermitianMat.spectrum_rcLike {𝕜 : Type u_3} {n : Type u_5} [RCLike 𝕜] [Fintype n] [DecidableEq n] (A : HermitianMat n 𝕜) :

spectrum 𝕜 ↑A = RCLike.ofReal '' spectrum ℝ ↑A

We fix a simp-normal form that, for HermitianMat, we always work in terms of the real spectrum.

source

theorem HermitianMat.ne_zero_iff_ne_zero_spectrum {𝕜 : Type u_3} {n : Type u_5} [RCLike 𝕜] [Fintype n] [DecidableEq n] (A : HermitianMat n 𝕜) :

A ≠ 0 ↔ ∃ x ∈ spectrum ℝ ↑A, x ≠ 0

source

theorem HermitianMat.spectrum_prod {𝕜 : Type u_3} {m : Type u_4} {n : Type u_5} [RCLike 𝕜] [Fintype n] [DecidableEq n] [Fintype m] [DecidableEq m] {A : HermitianMat m 𝕜} {B : HermitianMat n 𝕜} :

spectrum ℝ ↑(A.kronecker B) = spectrum ℝ ↑A * spectrum ℝ ↑B

source

noncomputable instance HermitianMat.instAddCommMonoidComplex {d : Type u_6} [DecidableEq d] :

AddCommMonoid (HermitianMat d ℂ)

Equations

HermitianMat.instAddCommMonoidComplex = inferInstance