OAI/Computability/QuantumFactoring/RationalHeightResources.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ExactQuantumFactoring.nat_size_mul_le line 11
  2. lemma OAI.ExactQuantumFactoring.nat_size_add_le line 16
  3. lemma OAI.ExactQuantumFactoring.nat_size_pow_le line 24
  4. lemma OAI.ExactQuantumFactoring.PolyBound.sizeMul line 33
  5. lemma OAI.ExactQuantumFactoring.PolyBound.sizeAdd line 36
  6. lemma OAI.ExactQuantumFactoring.PolyBound.sizePow line 39
  7. def OAI.ExactQuantumFactoring.RatHeightPoly line 46

    Source documentation

    Bit-length bounds for exact normalized rational constants appearing in the emitted circuit. These are not bounds on their exponentially large values.

    def RatHeightPoly (a : ℕ → ℚ) : Prop :=
…
  8. lemma OAI.ExactQuantumFactoring.RatHeightPoly.constant line 50
  9. lemma OAI.ExactQuantumFactoring.RatHeightPoly.natCast line 51
  10. lemma OAI.ExactQuantumFactoring.RatHeightPoly.intCast line 56
  11. lemma OAI.ExactQuantumFactoring.RatHeightPoly.add line 61
  12. lemma OAI.ExactQuantumFactoring.RatHeightPoly.neg line 75
  13. lemma OAI.ExactQuantumFactoring.RatHeightPoly.sub line 79
  14. lemma OAI.ExactQuantumFactoring.RatHeightPoly.mul line 81
  15. lemma OAI.ExactQuantumFactoring.RatHeightPoly.inv line 94
  16. lemma OAI.ExactQuantumFactoring.RatHeightPoly.div line 107
  17. lemma OAI.ExactQuantumFactoring.RatHeightPoly.pow line 109
  18. lemma OAI.ExactQuantumFactoring.RatHeightPoly.constExpr line 114