OAI/Combinatorics/EditApproximation/Coarse/CoarseInitialBinary.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.BinaryFraction.rationalMinimum_lower line 15

   Source documentation

   The empty case is unreachable for the dyadic guess list. The fallback is its already computed first entry, so no coarse call is repeated.

   private theorem rationalMinimum_lower (fallback : ℚ) (values : List ℚ) (z : ℚ)
       (hf : z ≤ fallback) (hv : ∀ a ∈ values, z ≤ a) : z ≤ rationalMinimum fallback values := by
   …

   Mentions: OAI.EditApproximation.rationalMinimum

2. theorem OAI.EditApproximation.BinaryFraction.rationalMinimum_le_mem line 23
3. theorem OAI.EditApproximation.BinaryFraction.rationalMinimum_le_fallback line 32
4. theorem OAI.EditApproximation.BinaryFraction.coarseMinimumWithWork_ofFn line 38
5. def OAI.EditApproximation.BinaryFraction.coarseCandidateWithWork line 69

   Source documentation

   A candidate executes the whole root recurrence, then adds its literal guess and doubles the result using Boolean arithmetic.

   def coarseCandidateWithWork {B d : ℕ} {α : Type*} [DecidableEq α]
       (q L : ℕ) (hB : 0 < B) (hq : 0 < q) (hL : 0 < L) (x y : List α)
       (i : CoarseGuessIndex (coarseEntryWidth x y)) (draws : CoarseThresholdDraws B d) :
       BinaryFraction × ℕ :=
   …

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

6. theorem OAI.EditApproximation.BinaryFraction.coarseCandidateWithWork_value line 81