OAI/Computability/QuantumFactoring/TriangularAlgebra.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ExactQuantumFactoring.Triangular.pathShift_prefix line 13
  2. lemma OAI.ExactQuantumFactoring.Triangular.pathShift_full_sum line 23
  3. lemma OAI.ExactQuantumFactoring.Triangular.pathWeight_prefix line 29
  4. def OAI.ExactQuantumFactoring.Triangular.dot line 35
  5. lemma OAI.ExactQuantumFactoring.Triangular.hEntry_pow line 37
  6. lemma OAI.ExactQuantumFactoring.Triangular.pathWeight_full line 41
  7. lemma OAI.ExactQuantumFactoring.Triangular.selected_evolve line 48
  8. def OAI.ExactQuantumFactoring.Triangular.inputNumber line 68

    Source documentation

    The input word is reversed physically, while the output wire j is k_j.

    def inputNumber {b : ℕ} (x : Bits b) : ℕ := ∑ i, 2^(b-1-i.val)*(x i).toNat

    Mentions: OAI.ExactQuantumFactoring.Triangular.Bits

  9. def OAI.ExactQuantumFactoring.Triangular.outputNumber line 69
  10. def OAI.ExactQuantumFactoring.Triangular.lowTerm line 71
  11. def OAI.ExactQuantumFactoring.Triangular.highTerm line 74
  12. lemma OAI.ExactQuantumFactoring.Triangular.productTerm line 77
  13. lemma OAI.ExactQuantumFactoring.Triangular.product_decomposition line 99
  14. def OAI.ExactQuantumFactoring.Triangular.rowShift line 115

    Source documentation

    One shift after H_j combines all the prescribed mutually commuting controlled power-of-two shifts in that row.

    def rowShift {b : ℕ} (j : Fin b) (z : Bits b) : ℕ :=
…

    Mentions: OAI.ExactQuantumFactoring.Triangular.Bits

  15. lemma OAI.ExactQuantumFactoring.Triangular.rowShift_hybrid line 118
  16. lemma OAI.ExactQuantumFactoring.Triangular.pathShift_rows line 128