OAI/Combinatorics/EditApproximation/Coarse/CoarseIndexedExtra.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.EditApproximation.BinaryFraction.coarseIndexedExtra line 10

   Source documentation

   All descriptor and original-input operations alongside the core arithmetic. Threshold decisions are exactly those of the evaluated call.

   def coarseIndexedExtra {B : ℕ} (k q L n : ℕ) (source target : List ℕ)
       (two : BinaryFraction) : (d offset : ℕ) → CoarseThresholdDraws B d →
       BinaryFraction → ℕ → ℕ
     | 0, offset, _, allowance, start =>
       let descriptor := coarseDescriptorWithWork B 0 n offset
   …

   Mentions: OAI.EditApproximation.BinaryFraction, OAI.EditApproximation.CoarseThresholdDraws, OAI.EditApproximation.coarseDescriptorWithWork