def «term𝐔[_]» : Lean.ParserDescr

Equations

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

@[simp]

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

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

theorem Matrix.kron_unitary {α : Type u_2} {β : Type u_3} [DecidableEq α] [Fintype α] [DecidableEq β] [Fintype β] (a : ↥𝐔[α]) (b : ↥𝐔[β]) : kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) ↑a ↑b ∈ 𝐔[α × β]

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, ⋯⟩

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

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

@[simp]

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

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.

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.