OAI/Combinatorics/EditApproximation/Coarse/CoarseInitialExecution.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.BinaryFraction.naturalListEqualWithWork_value line 13
2. def OAI.EditApproximation.BinaryFraction.coarseInitialWithWork line 31

   Source documentation

   Entire dyadic initial estimator, including direct cases, every root execution, binary minimum, ceiling, and final integer clamp.

   def coarseInitialWithWork {B d : ℕ} (q L N : ℕ)
       (hB : 0 < B) (hq : 0 < q) (hL : 0 < L) (x y : List ℕ)
       (draws : CoarseGuessIndex (coarseEntryWidth x y) → CoarseThresholdDraws B d) : ℕ × ℕ :=
   …

   Mentions: OAI.EditApproximation.CoarseGuessIndex, OAI.EditApproximation.coarseEntryWidth, OAI.EditApproximation.CoarseThresholdDraws

3. theorem OAI.EditApproximation.BinaryFraction.coarseInitialWithWork_value line 46