Hilbert operators and unitary gates

HilbertOperator n is the raw 2^n × 2^n complex matrix type. It is used for observables, projectors, matrix sums, and block-encoding operators that are not necessarily unitary.

Gate n is a unitary Hilbert operator. Gate application maps pure states to pure states; arbitrary linear combinations stay at the raw StateVector layer until separately normalized.

Pinned Mathlib API: Matrix.mulVec (and mulVec_add/smul/single_one, one_mulVec, mulVec_mulVec), Matrix.mem_unitaryGroup_iff, Equiv.Perm.permMatrix (and Matrix.permMatrix_mulVec, Matrix.conjTranspose_permMatrix, Matrix.permMatrix_mul, Matrix.permMatrix_one), Finset.sum_ite_eq'.

@[reducible, inline]

abbrev QuantumAlg.HilbertOperator (n : ℕ) : Type

Raw linear operator on an n-qubit Hilbert space.

Equations

• QuantumAlg.HilbertOperator n = Matrix (Fin (2 ^ n)) (Fin (2 ^ n)) ℂ

noncomputable def QuantumAlg.HilbertOperator.applyVec {n : ℕ} (A : HilbertOperator n) (ψ : StateVector n) : StateVector n

A Hilbert operator acts on a raw state vector by matrix-vector multiplication.

Equations

• A.applyVec ψ = WithLp.toLp 2 (Matrix.mulVec A ψ.ofLp)

@[simp]

theorem QuantumAlg.HilbertOperator.applyVec_apply {n : ℕ} (A : HilbertOperator n) (ψ : StateVector n) (i : Fin (2 ^ n)) : (A.applyVec ψ).ofLp i = ∑ j : Fin (2 ^ n), A i j * ψ.ofLp j

@[simp]

theorem QuantumAlg.HilbertOperator.applyVec_add {n : ℕ} (A : HilbertOperator n) (ψ φ : StateVector n) : A.applyVec (ψ + φ) = A.applyVec ψ + A.applyVec φ

@[simp]

theorem QuantumAlg.HilbertOperator.applyVec_sub {n : ℕ} (A : HilbertOperator n) (ψ φ : StateVector n) : A.applyVec (ψ - φ) = A.applyVec ψ - A.applyVec φ

@[simp]

theorem QuantumAlg.HilbertOperator.applyVec_smul {n : ℕ} (A : HilbertOperator n) (c : ℂ) (ψ : StateVector n) : A.applyVec (c • ψ) = c • A.applyVec ψ

@[simp]

theorem QuantumAlg.HilbertOperator.applyVec_neg {n : ℕ} (A : HilbertOperator n) (ψ : StateVector n) : A.applyVec (-ψ) = -A.applyVec ψ

@[simp]

theorem QuantumAlg.HilbertOperator.add_applyVec {n : ℕ} (A B : HilbertOperator n) (ψ : StateVector n) : (A + B).applyVec ψ = A.applyVec ψ + B.applyVec ψ

@[simp]

theorem QuantumAlg.HilbertOperator.smul_applyVec {n : ℕ} (c : ℂ) (A : HilbertOperator n) (ψ : StateVector n) : (c • A).applyVec ψ = c • A.applyVec ψ

@[simp]

theorem QuantumAlg.HilbertOperator.one_applyVec {n : ℕ} (ψ : StateVector n) : applyVec 1 ψ = ψ

theorem QuantumAlg.HilbertOperator.mul_applyVec {n : ℕ} (A B : HilbertOperator n) (ψ : StateVector n) : applyVec (A * B) ψ = A.applyVec (B.applyVec ψ)

theorem QuantumAlg.HilbertOperator.applyVec_ket {n : ℕ} (A : HilbertOperator n) (x i : Fin (2 ^ n)) : (A.applyVec (PureState.ket x).vec).ofLp i = A i x

A Hilbert operator sends a basis ket to its corresponding column.

theorem QuantumAlg.HilbertOperator.inner_applyVec_applyVec_of_mem_unitaryGroup {n : ℕ} {U : HilbertOperator n} (hU : U ∈ Matrix.unitaryGroup (Fin (2 ^ n)) ℂ) (ψ φ : StateVector n) : inner ℂ (U.applyVec ψ) (U.applyVec φ) = inner ℂ ψ φ

A unitary Hilbert operator preserves inner products on raw state vectors.

theorem QuantumAlg.HilbertOperator.norm_applyVec_of_mem_unitaryGroup {n : ℕ} {U : HilbertOperator n} (hU : U ∈ Matrix.unitaryGroup (Fin (2 ^ n)) ℂ) (ψ : StateVector n) : ‖U.applyVec ψ‖ = ‖ψ‖

A unitary Hilbert operator preserves raw vector norms.

structure QuantumAlg.Gate (n : ℕ) : Type

A unitary gate on an n-qubit Hilbert space.

• op : HilbertOperator n

  Underlying Hilbert-space operator.

• unitary : self.op ∈ Matrix.unitaryGroup (Fin (2 ^ n)) ℂ

  Gates are unitary by definition.

@[implicit_reducible]

instance QuantumAlg.Gate.instCoeHilbertOperator {n : ℕ} : Coe (Gate n) (HilbertOperator n)

Equations

• QuantumAlg.Gate.instCoeHilbertOperator = { coe := QuantumAlg.Gate.op }

@[implicit_reducible]

instance QuantumAlg.Gate.instCoeFunForallFinHPowNatOfNatForallComplex {n : ℕ} : CoeFun (Gate n) fun (x : Gate n) => Fin (2 ^ n) → Fin (2 ^ n) → ℂ

Equations

• QuantumAlg.Gate.instCoeFunForallFinHPowNatOfNatForallComplex = { coe := fun (G : QuantumAlg.Gate n) => G.op }

@[implicit_reducible]

instance QuantumAlg.Gate.instHMulHilbertOperator {n : ℕ} : HMul (Gate n) (HilbertOperator n) (HilbertOperator n)

Equations

• QuantumAlg.Gate.instHMulHilbertOperator = { hMul := fun (G : QuantumAlg.Gate n) (A : QuantumAlg.HilbertOperator n) => G.op * A }

@[implicit_reducible]

instance QuantumAlg.Gate.instHMulHilbertOperator_1 {n : ℕ} : HMul (HilbertOperator n) (Gate n) (HilbertOperator n)

Equations

• QuantumAlg.Gate.instHMulHilbertOperator_1 = { hMul := fun (A : QuantumAlg.HilbertOperator n) (G : QuantumAlg.Gate n) => A * G.op }

theorem QuantumAlg.Gate.ext {n : ℕ} {G K : Gate n} (h : ∀ (i j : Fin (2 ^ n)), G.op i j = K.op i j) : G = K

theorem QuantumAlg.Gate.ext_iff {n : ℕ} {G K : Gate n} : G = K ↔ ∀ (i j : Fin (2 ^ n)), G.op i j = K.op i j

def QuantumAlg.Gate.ofUnitary {n : ℕ} (U : HilbertOperator n) (hU : U ∈ Matrix.unitaryGroup (Fin (2 ^ n)) ℂ) : Gate n

Build a gate from a unitary Hilbert operator.

Equations

• QuantumAlg.Gate.ofUnitary U hU = { op := U, unitary := hU }

@[simp]

theorem QuantumAlg.Gate.coe_ofUnitary {n : ℕ} (U : HilbertOperator n) (hU : U ∈ Matrix.unitaryGroup (Fin (2 ^ n)) ℂ) : (ofUnitary U hU).op = U

@[implicit_reducible]

instance QuantumAlg.Gate.instMonoid {n : ℕ} : Monoid (Gate n)

Equations

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

@[simp]

theorem QuantumAlg.Gate.coe_one {n : ℕ} : op 1 = 1

@[simp]

theorem QuantumAlg.Gate.coe_mul {n : ℕ} (G K : Gate n) : (G * K).op = G.op * K.op

def QuantumAlg.Gate.conjTranspose {n : ℕ} (G : Gate n) : Gate n

Conjugate transpose of a unitary gate, again as a gate.

Equations

• G.conjTranspose = QuantumAlg.Gate.ofUnitary (Matrix.conjTranspose G.op) ⋯

@[implicit_reducible]

instance QuantumAlg.Gate.instInv {n : ℕ} : Inv (Gate n)

Equations

• QuantumAlg.Gate.instInv = { inv := QuantumAlg.Gate.conjTranspose }

@[simp]

theorem QuantumAlg.Gate.coe_conjTranspose {n : ℕ} (G : Gate n) : G.conjTranspose.op = Matrix.conjTranspose G.op

noncomputable def QuantumAlg.Gate.applyVec {n : ℕ} (G : Gate n) (ψ : StateVector n) : StateVector n

A gate acts on a raw vector by its underlying Hilbert operator.

Equations

• G.applyVec ψ = G.op.applyVec ψ

noncomputable def QuantumAlg.Gate.apply {n : ℕ} (G : Gate n) (ψ : PureState n) : PureState n

A gate evolves a pure state to a pure state.

Equations

• G.apply ψ = QuantumAlg.PureState.ofVec (G.applyVec ψ.vec) ⋯

noncomputable def QuantumAlg.Gate.evolve {n : ℕ} (G : Gate n) (ψ : PureState n) : PureState n

Alias for apply, emphasizing unitary time evolution.

Equations

• G.evolve ψ = G.apply ψ

@[simp]

theorem QuantumAlg.Gate.applyVec_apply {n : ℕ} (G : Gate n) (ψ : StateVector n) (i : Fin (2 ^ n)) : (G.applyVec ψ).ofLp i = ∑ j : Fin (2 ^ n), G.op i j * ψ.ofLp j

@[simp]

theorem QuantumAlg.Gate.apply_apply {n : ℕ} (G : Gate n) (ψ : PureState n) (i : Fin (2 ^ n)) : (G.apply ψ).vec.ofLp i = ∑ j : Fin (2 ^ n), G.op i j * ψ.vec.ofLp j

@[simp]

theorem QuantumAlg.Gate.applyVec_add {n : ℕ} (G : Gate n) (ψ φ : StateVector n) : G.applyVec (ψ + φ) = G.applyVec ψ + G.applyVec φ

@[simp]

theorem QuantumAlg.Gate.applyVec_sub {n : ℕ} (G : Gate n) (ψ φ : StateVector n) : G.applyVec (ψ - φ) = G.applyVec ψ - G.applyVec φ

@[simp]

theorem QuantumAlg.Gate.applyVec_smul {n : ℕ} (G : Gate n) (c : ℂ) (ψ : StateVector n) : G.applyVec (c • ψ) = c • G.applyVec ψ

@[simp]

theorem QuantumAlg.Gate.applyVec_neg {n : ℕ} (G : Gate n) (ψ : StateVector n) : G.applyVec (-ψ) = -G.applyVec ψ

theorem QuantumAlg.Gate.apply_add {n : ℕ} (G : Gate n) (ψ φ : StateVector n) : G.applyVec (ψ + φ) = G.applyVec ψ + G.applyVec φ

theorem QuantumAlg.Gate.apply_sub {n : ℕ} (G : Gate n) (ψ φ : StateVector n) : G.applyVec (ψ - φ) = G.applyVec ψ - G.applyVec φ

theorem QuantumAlg.Gate.apply_smul {n : ℕ} (G : Gate n) (c : ℂ) (ψ : StateVector n) : G.applyVec (c • ψ) = c • G.applyVec ψ

theorem QuantumAlg.Gate.apply_neg {n : ℕ} (G : Gate n) (ψ : StateVector n) : G.applyVec (-ψ) = -G.applyVec ψ

@[simp]

theorem QuantumAlg.Gate.one_apply {n : ℕ} (ψ : PureState n) : apply 1 ψ = ψ

@[simp]

theorem QuantumAlg.Gate.one_applyVec {n : ℕ} (ψ : StateVector n) : applyVec 1 ψ = ψ

theorem QuantumAlg.Gate.mul_applyVec {n : ℕ} (G K : Gate n) (ψ : StateVector n) : (G * K).applyVec ψ = G.applyVec (K.applyVec ψ)

theorem QuantumAlg.Gate.mul_apply {n : ℕ} (G K : Gate n) (ψ : PureState n) : (G * K).apply ψ = G.apply (K.apply ψ)

theorem QuantumAlg.Gate.apply_ket {n : ℕ} (G : Gate n) (x i : Fin (2 ^ n)) : (G.apply (PureState.ket x)).vec.ofLp i = G.op i x

A gate sends the basis ket |x⟩ to its x-th column.

Permutation gates

def QuantumAlg.Gate.ofPerm {n : ℕ} (σ : Equiv.Perm (Fin (2 ^ n))) : Gate n

The gate permuting the computational basis by σ: (ofPerm σ).apply (ket x) = ket (σ⁻¹ x). Unitary by construction.

Equations

• QuantumAlg.Gate.ofPerm σ = QuantumAlg.Gate.ofUnitary (Equiv.Perm.permMatrix ℂ σ) ⋯

theorem QuantumAlg.Gate.ofPerm_apply {n : ℕ} (σ : Equiv.Perm (Fin (2 ^ n))) (ψ : PureState n) (i : Fin (2 ^ n)) : ((ofPerm σ).apply ψ).vec.ofLp i = ψ.vec.ofLp (σ i)

theorem QuantumAlg.Gate.ofPerm_apply_ket {n : ℕ} (σ : Equiv.Perm (Fin (2 ^ n))) (x : Fin (2 ^ n)) : (ofPerm σ).apply (PureState.ket x) = PureState.ket (σ⁻¹ x)

theorem QuantumAlg.Gate.ofPerm_mem_unitaryGroup {n : ℕ} (σ : Equiv.Perm (Fin (2 ^ n))) : (ofPerm σ).op ∈ Matrix.unitaryGroup (Fin (2 ^ n)) ℂ

Unitary gates preserve inner products and norms

theorem QuantumAlg.Gate.inner_apply_apply_of_mem_unitaryGroup {n : ℕ} {U : Gate n} (_hU : U.op ∈ Matrix.unitaryGroup (Fin (2 ^ n)) ℂ) (ψ φ : PureState n) : inner ℂ (U.apply ψ).vec (U.apply φ).vec = inner ℂ ψ.vec φ.vec

Unitary gates preserve the inner product.

theorem QuantumAlg.Gate.norm_apply_of_mem_unitaryGroup {n : ℕ} {U : Gate n} (_hU : U.op ∈ Matrix.unitaryGroup (Fin (2 ^ n)) ℂ) (ψ : PureState n) : ‖(U.apply ψ).vec‖ = ‖ψ.vec‖

Unitary gates preserve the norm.

theorem QuantumAlg.Gate.norm_apply {n : ℕ} (U : Gate n) (ψ : PureState n) : ‖(U.apply ψ).vec‖ = 1