OAI/Combinatorics/EditApproximation/Coarse/CoarseIndexedInitial.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.BinaryFraction.coarseIndexedRootWithWork_value line 13
2. theorem OAI.EditApproximation.BinaryFraction.coarseIndexedCandidateWithWork_value line 28
3. theorem OAI.EditApproximation.BinaryFraction.coarseIndexedInitialWithWork_value line 39

   Source documentation

   The final coarse initializer executes the indexed roots and retains only their integer-clamped minimum.

   theorem coarseIndexedInitialWithWork_value {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) :
       (coarseIndexedInitialWithWork q L N hB hq hL x y draws).1 =
         coarseInitialValue B d q (1 / L) N x y draws := by
   …

   Mentions: OAI.EditApproximation.CoarseGuessIndex, OAI.EditApproximation.coarseEntryWidth, OAI.EditApproximation.CoarseThresholdDraws, OAI.EditApproximation.BinaryFraction.coarseIndexedInitialWithWork, OAI.EditApproximation.coarseInitialValue