OAI/Computability/QuantumFactoring/ContinuedFractionPairs.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.OrderTrial.convergentPair line 15

   Source documentation

   Reduced nonnegative numerator/positive denominator representation; the zero case is essential because the total rational inverse sends zero to zero.

   def convergentPair (a b : ℕ) : ℕ → ℕ×ℕ
     | 0 => (a/b,1)
     | k+1 =>
       let p := convergentPair b (a%b) k
   …

2. lemma OAI.ExactQuantumFactoring.OrderTrial.convergentPair_reduced line 21
3. lemma OAI.ExactQuantumFactoring.OrderTrial.convergentPair_ratio line 35
4. lemma OAI.ExactQuantumFactoring.OrderTrial.convergentPair_label line 48
5. lemma OAI.ExactQuantumFactoring.OrderTrial.convergentPair_bound line 55

   Source documentation

   Linear bit growth, rather than syntactic nested rational inverses.

   lemma convergentPair_bound {s a b : ℕ} (ha : a<2^s) (hb : b<2^s) (k : ℕ) :
       (convergentPair a b k).1<2^(s*(k+1)+1) ∧
         (convergentPair a b k).2<2^(s*(k+1)+1) := by
   …

   Mentions: OAI.ExactQuantumFactoring.OrderTrial.convergentPair