QuantumInfo.ForMathlib.HermitianMat.Basic

@[reducible, inline]

abbrev 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_3} [AddGroup α] [StarAddMonoid α] :

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

source

@[reducible]

def HermitianMat.toMat {α : Type u_1} {n : Type u_3} [AddGroup α] [StarAddMonoid α] :

HermitianMat n α → Matrix n n α

Equations

HermitianMat.toMat = Subtype.val

Instances For

source

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

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

Equations

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

source

@[simp]

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

↑A = ↑A

source

@[simp]

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

↑⟨x, h⟩ = x

source

theorem HermitianMat.H {α : Type u_1} {n : Type u_3} [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_3} [AddGroup α] [StarAddMonoid α] {A B : HermitianMat n α} :

↑A = ↑B → A = B

source

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

A = B ↔ ↑A = ↑B

source

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

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

Equations

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

source

instance HermitianMat.instStar {α : Type u_1} {n : Type u_3} [AddGroup α] [StarAddMonoid α] :

Star (HermitianMat n α)

Equations

HermitianMat.instStar = { star := fun (x : HermitianMat n α) => x }

source

instance HermitianMat.instTrivialStar {α : Type u_1} {n : Type u_3} [AddGroup α] [StarAddMonoid α] :

TrivialStar (HermitianMat n α)

source

@[simp]

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

(↑A).conjTranspose = ↑A

source

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

Inv (HermitianMat n α)

Equations

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

source

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

Pow (HermitianMat n α) ℤ

Equations

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

source

@[simp]

theorem HermitianMat.im_eq_zero {α : Type u_1} {n : Type u_3} [RCLike α] (A : HermitianMat n α) (x : n) :

RCLike.im (A x x) = 0

source

@[simp]

theorem HermitianMat.Complex_im_eq_zero {n : Type u_3} (A : HermitianMat n ℂ) (x : n) :

(A x x).im = 0

source

def HermitianMat.conj {α : Type u_1} {n : Type u_3} [CommRing α] [StarRing α] [Fintype n] {m : Type u_4} (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_2} {n : Type u_3} [CommRing α] [StarRing α] [Fintype n] (B : Matrix m n α) (A : HermitianMat n α) :

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

source

@[simp]

theorem HermitianMat.conj_apply_toMat {α : Type u_1} {m : Type u_2} {n : Type u_3} [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_3} [CommRing α] [StarRing α] [Fintype n] (A : HermitianMat n α) {m : Type u_4} {l : Type u_5} [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} {n : Type u_3} [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_3} [CommRing α] [StarRing α] [Fintype n] (A : HermitianMat n α) [DecidableEq n] :

(conj 1) A = A

source

def HermitianMat.conjLinear {α : Type u_1} {n : Type u_3} [CommRing α] [StarRing α] [Fintype n] (R : Type u_4) [Star R] [TrivialStar R] [CommSemiring R] [Algebra R α] [StarModule R α] {m : Type u_5} (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_2} {n : Type u_3} [CommRing α] [StarRing α] [Fintype n] (A : HermitianMat n α) (R : Type u_4) [Star R] [TrivialStar R] [CommSemiring R] [Algebra R α] [StarModule R α] (B : Matrix m n α) :

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

source

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

FaithfulSMul ℝ (HermitianMat n 𝕜)

source

def HermitianMat.lin {n : Type u_3} {𝕜 : Type u_4} [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 {n : Type u_3} {𝕜 : Type u_4} [RCLike 𝕜] [Fintype n] [DecidableEq n] (A : HermitianMat n 𝕜) :

(↑A.lin).IsSymmetric

source

@[simp]

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

lin 0 = 0

source

@[simp]

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

lin 1 = 1

source

noncomputable def HermitianMat.eigenspace {n : Type u_3} {𝕜 : Type u_4} [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 {n : Type u_3} {𝕜 : Type u_4} [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 = LinearMap.ker A.lin

Instances For

source

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

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

source

theorem HermitianMat.ker_eq_eigenspace_zero {n : Type u_3} {𝕜 : Type u_4} [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 {n : Type u_3} {𝕜 : Type u_4} [RCLike 𝕜] [Fintype n] [DecidableEq n] :

ker 0 = ⊤

source

@[simp]

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

ker 1 = ⊥

source

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

(c • A).ker = A.ker

source

def HermitianMat.support {n : Type u_3} {𝕜 : Type u_4} [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 = LinearMap.range A.lin

Instances For

source

theorem HermitianMat.support_eq_sup_eigenspace_nonzero {n : Type u_3} {𝕜 : Type u_4} [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 {n : Type u_3} {𝕜 : Type u_4} [RCLike 𝕜] [Fintype n] [DecidableEq n] :

support 0 = ⊥

source

@[simp]

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

support 1 = ⊤

source

@[simp]

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

A.kerᗮ = A.support

source

@[simp]

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

A.supportᗮ = A.ker

source

def HermitianMat.diagonal {n : Type u_3} [DecidableEq n] (f : n → ℝ) :

HermitianMat n ℂ

Equations

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

Instances For

source

theorem HermitianMat.diagonal_conj_diagonal {n : Type u_3} [Fintype n] [DecidableEq n] (f g : n → ℝ) :

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

source

def HermitianMat.kronecker {α : Type u_1} {m : Type u_2} {n : Type u_3} [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

@[simp]

theorem HermitianMat.kronecker_coe {α : Type u_1} {m : Type u_2} {n : Type u_3} [CommRing α] [StarRing α] (A : HermitianMat m α) (B : HermitianMat n α) :

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

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.zero_kronecker {α : Type u_1} {m : Type u_2} {n : Type u_3} [CommRing α] [StarRing α] (A : HermitianMat m α) :

kronecker 0 A = 0

source

@[simp]

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

A.kronecker 0 = 0

source

@[simp]

theorem HermitianMat.kronecker_one_one {α : Type u_1} {m : Type u_2} {n : Type u_3} [CommRing α] [StarRing α] [DecidableEq m] [DecidableEq n] [Fintype m] [Fintype n] :

kronecker 1 1 = 1

source

theorem HermitianMat.add_kronecker {α : Type u_1} {m : Type u_2} {n : Type u_3} [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_2} {n : Type u_3} [CommRing α] [StarRing α] (A : HermitianMat m α) (B C : HermitianMat n α) :

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