OAI/Combinatorics/EditApproximation/Coarse/CoarseInitialLabels.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.coarseInitialLabelCount_le_arrayWork line 13

   Source documentation

   Only labels in roots actually reached by the dyadic initializer are drawn.

   theorem coarseInitialLabelCount_le_arrayWork {α : Type*} [DecidableEq α]
       (B d : ℕ) (Q lam : ℚ) (x y : List α)
       (draws : CoarseGuessIndex (coarseEntryWidth x y) → CoarseThresholdDraws B d) :
       coarseInitialLabelCount B d Q lam x y draws ≤ coarseInitialArrayWork B d Q lam x y draws := by
   …

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

2. def OAI.EditApproximation.coarseInitialSamplingBits line 24
3. theorem OAI.EditApproximation.coarseInitialSamplingBits_le line 29