OAI/Combinatorics/EditApproximation/Coarse/CoarseRootExecution.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.BinaryFraction.coarseRootDenominator_value line 14
2. theorem OAI.EditApproximation.BinaryFraction.coarseRootDenominator_length line 18
3. theorem OAI.EditApproximation.BinaryFraction.coarseRootDenominator_pos line 22
4. def OAI.EditApproximation.BinaryFraction.coarseRootWithWork line 30

   Source documentation

   Counted root setup and array lookup around the complete binary coarse recursion. The common denominator is built from bits, not a free conversion.

   def coarseRootWithWork {B d : ℕ} {α : Type*} [DecidableEq α]
       (k q L : ℕ) (hB : 0 < B) (hq : 0 < q) (hL : 0 < L)
       (frame : List (Option α)) (tree : CoarseSourceTree B α d)
       (draws : CoarseThresholdDraws B d) (start : ℕ) (shift : Fin (2 * k + 1)) :
       BinaryFraction × ℕ :=
   …

   Mentions: OAI.EditApproximation.CoarseSourceTree, OAI.EditApproximation.CoarseThresholdDraws, OAI.EditApproximation.BinaryFraction

5. theorem OAI.EditApproximation.BinaryFraction.coarseRootWithWork_value line 43