QuantumBlockEncoding/TextbookStatePreparation.lean

This definition gives the library's named construction or computation for “zero index”.

def zeroIndex : Fin (gridSize 1) := ⟨0, Nat.pow_pos (by decide)⟩

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one index”.

def oneIndex : Fin (gridSize 1) := ⟨1, by native_decide⟩

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “pauli x”.

def pauliX : FiniteMatrix (gridSize 1) (gridSize 1) ℂ :=
  _root_.Matrix.swap ℂ zeroIndex oneIndex

/-- The Pauli X matrix is unitary in Mathlib's standard unitary group. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “pauli x unitary”; the hypotheses and conclusion in the code panel fix its exact scope. The Pauli X matrix is unitary in Mathlib's standard unitary group.

theorem pauliX_unitary :
    pauliX ∈ _root_.Matrix.unitaryGroup (Fin (gridSize 1)) ℂ := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one state”.

def oneState : StateVector (gridSize 1) ℂ :=
  basisKet (gridSize 1) oneIndex

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one target”.

def oneTarget : StatePreparationTarget ℂ 1 where
  amplitudes := oneState
  normalization := ∑ index, Complex.normSq (oneState index) = 1
  source := "Pauli X textbook example"

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “one target normalized”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem oneTarget_normalized : oneTarget.normalization := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “pauli x prepares one”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem pauliX_prepares_one :
    applyVec pauliX (zeroKet 1) = oneTarget.amplitudes := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “pauli x gate”.

def pauliXGate : ComplexUnitaryGate 1 where
  matrix := pauliX
  unitary := pauliX_unitary

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “pauli x certificate”.

def pauliXCertificate : ComplexStatePreparationCertificate 1 where
  target := oneTarget
  gate := pauliXGate
  normalizationProof := oneTarget_normalized
  preparationProof := pauliX_prepares_one

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “pauli x circuit”.

def pauliXCircuit : Circuit := [Gate.oneQubit "X" 0]

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “pauli x verified”.

def pauliXVerified : VerifiedStatePreparation ℂ 1 :=
  pauliXCertificate.verified pauliXCircuit [[Gate.oneQubit "X" 0]]
    pauliXCircuit.resource

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “pauli x verified cost”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem pauliXVerified_cost :
    pauliXVerified.candidate.cost =
      { auxiliaryQubits := 0, gateCount := 1, depth := 1, oracleCalls := 0 } := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “inv sqrt two”.

noncomputable def invSqrtTwo : ℂ :=
  (Real.sqrt 2 / 2 : ℝ)

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “inv sqrt two mul self”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem invSqrtTwo_mul_self : invSqrtTwo * invSqrtTwo = (1 : ℂ) / 2 := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “hadamard”.

noncomputable def hadamard :
    FiniteMatrix (gridSize 1) (gridSize 1) ℂ :=
  fun row column =>
    if row.val = 1 ∧ column.val = 1 then -invSqrtTwo else invSqrtTwo

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “star hadamard”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem star_hadamard : star hadamard = hadamard := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “hadamard unitary”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem hadamard_unitary :
    hadamard ∈ _root_.Matrix.unitaryGroup (Fin (gridSize 1)) ℂ := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “plus state”.

noncomputable def plusState : StateVector (gridSize 1) ℂ :=
  fun _ => invSqrtTwo

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “plus target”.

noncomputable def plusTarget : StatePreparationTarget ℂ 1 where
  amplitudes := plusState
  normalization := ∑ index, Complex.normSq (plusState index) = 1
  source := "Hadamard textbook example"

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “plus target normalized”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem plusTarget_normalized : plusTarget.normalization := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “hadamard prepares plus”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem hadamard_prepares_plus :
    applyVec hadamard (zeroKet 1) = plusTarget.amplitudes := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “hadamard gate”.

noncomputable def hadamardGate : ComplexUnitaryGate 1 where
  matrix := hadamard
  unitary := hadamard_unitary

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “hadamard certificate”.

noncomputable def hadamardCertificate :
    ComplexStatePreparationCertificate 1 where
  target := plusTarget
  gate := hadamardGate
  normalizationProof := plusTarget_normalized
  preparationProof := hadamard_prepares_plus

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “hadamard circuit”.

def hadamardCircuit : Circuit := [Gate.oneQubit "H" 0]

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “hadamard verified”.

noncomputable def hadamardVerified : VerifiedStatePreparation ℂ 1 :=
  hadamardCertificate.verified hadamardCircuit [[Gate.oneQubit "H" 0]]
    hadamardCircuit.resource

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “hadamard verified cost”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem hadamardVerified_cost :
    hadamardVerified.candidate.cost =
      { auxiliaryQubits := 0, gateCount := 1, depth := 1, oracleCalls := 0 } := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “pauli x certificate prepares one”; the hypotheses and conclusion in the code panel fix its exact scope. The certified Pauli X example states the familiar textbook equation.

theorem pauliXCertificate_prepares_one :
    applyVec pauliXCertificate.gate.matrix (zeroKet 1) =
      pauliXCertificate.target.amplitudes :=
  pauliXCertificate.preparesVector

/-- The certified Hadamard example prepares the equal superposition. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “hadamard certificate prepares plus”; the hypotheses and conclusion in the code panel fix its exact scope. The certified Hadamard example prepares the equal superposition.

theorem hadamardCertificate_prepares_plus :
    applyVec hadamardCertificate.gate.matrix (zeroKet 1) =
      hadamardCertificate.target.amplitudes :=
  hadamardCertificate.preparesVector

commit-pinned source · Verso Blueprint panel