OAI/Combinatorics/EditApproximation/Coarse/CoarseIndexedValue.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.BinaryFraction.coarseIndexedWithWork_value line 12

   Source documentation

   Charging descriptor/read operations leaves the indexed arithmetic result unchanged, on every draw and every pruning branch.

   theorem coarseIndexedWithWork_value {B : ℕ} (k q L n : ℕ) (source target : List ℕ)
       (two : BinaryFraction) (d offset : ℕ) (draws : CoarseThresholdDraws B d)
       (allowance : BinaryFraction) (start : ℕ) :
       (coarseIndexedWithWork k q L n source target two d offset draws allowance start).1 =
         (coarseReadCore k q L n source target two d offset draws allowance start).1 := by
   …

   Mentions: OAI.EditApproximation.BinaryFraction, OAI.EditApproximation.CoarseThresholdDraws, OAI.EditApproximation.BinaryFraction.coarseIndexedWithWork, OAI.EditApproximation.BinaryFraction.coarseReadCore