QuantumInfo.ForMathlib.HermitianMat.Unitary

source

def «term𝐔[_]» :

Lean.ParserDescr

Equations

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

Instances For

source

@[simp]

theorem Matrix.neg_unitary_val {α : Type u_2} [DecidableEq α] [Fintype α] (u : ↥𝐔[α]) :

↑(-u) = -↑u

source

@[simp]

theorem Matrix.star_kron {α : Type u_2} {β : Type u_3} (a : Matrix α α ℂ) (b : Matrix β β ℂ) :

star (kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) a b) = kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (star a) (star b)

source

theorem Matrix.kron_unitary {α : Type u_2} {β : Type u_3} [DecidableEq α] [Fintype α] [DecidableEq β] [Fintype β] (a : ↥𝐔[α]) (b : ↥𝐔[β]) :

kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) ↑a ↑b ∈ 𝐔[α × β]

source

def Matrix.unitary_kron {α : Type u_2} {β : Type u_3} [DecidableEq α] [Fintype α] [DecidableEq β] [Fintype β] (a : ↥𝐔[α]) (b : ↥𝐔[β]) :

↥𝐔[α × β]

Equations

Matrix.unitary_kron a b = ⟨Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) ↑a ↑b, ⋯⟩

Instances For

source

def Matrix.«term_⊗ᵤ_» :

Lean.TrailingParserDescr

Equations

Matrix.«term_⊗ᵤ_» = Lean.ParserDescr.trailingNode `Matrix.«term_⊗ᵤ_» 60 60 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊗ᵤ ") (Lean.ParserDescr.cat `term 61))

Instances For

source

@[simp]

theorem Matrix.unitary_kron_apply {α : Type u_2} {β : Type u_3} [DecidableEq α] [Fintype α] [DecidableEq β] [Fintype β] (a : ↥𝐔[α]) (b : ↥𝐔[β]) (i₁ i₂ : α) (j₁ j₂ : β) :

↑(unitary_kron a b) (i₁, j₁) (i₂, j₂) = ↑a i₁ i₂ * ↑b j₁ j₂

source

@[simp]

theorem Matrix.unitary_kron_one_one {α : Type u_2} {β : Type u_3} [DecidableEq α] [Fintype α] [DecidableEq β] [Fintype β] :

unitary_kron 1 1 = 1

source

theorem Matrix.unitary_row_sum_norm_sq {d : Type u_4} [Fintype d] [DecidableEq d] (C : Matrix d d ℂ) (hC : C * C.conjTranspose = 1) (i : d) :

∑ j : d, ‖C i j‖ ^ 2 = 1

For a unitary matrix C, the row sums of ‖C i j‖^2 equal 1.

source

theorem Matrix.unitary_col_sum_norm_sq {d : Type u_4} [Fintype d] [DecidableEq d] (C : Matrix d d ℂ) (hC : C.conjTranspose * C = 1) (j : d) :

∑ i : d, ‖C i j‖ ^ 2 = 1

For a unitary matrix C, the column sums of ‖C i j‖^2 equal 1.

source

@[simp]

theorem HermitianMat.trace_conj_unitary {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] (A : HermitianMat n 𝕜) (U : ↥(Matrix.unitaryGroup n 𝕜)) :

((conj ↑U) A).trace = A.trace

source

@[simp]

theorem HermitianMat.le_conj_unitary {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] (A B : HermitianMat n 𝕜) (U : ↥(Matrix.unitaryGroup n 𝕜)) :

(conj ↑U) A ≤ (conj ↑U) B ↔ A ≤ B

source

@[simp]

theorem HermitianMat.inner_conj_unitary {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] (A B : HermitianMat n 𝕜) (U : ↥(Matrix.unitaryGroup n 𝕜)) :

inner ℝ ((conj ↑U) A) ((conj ↑U) B) = inner ℝ A B

source

@[simp]

theorem HermitianMat.eigenvalues_conj {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] (A : HermitianMat n 𝕜) (U : ↥(Matrix.unitaryGroup n 𝕜)) :

⋯.eigenvalues = ⋯.eigenvalues

The eigenvalues of a Hermitian matrix conjugated by a unitary matrix are the same as the eigenvalues of the original matrix.