OAI/Combinatorics/EditApproximation/Coarse/CoarseIndexedAllocation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.EditApproximation.BinaryFraction.coarseIndexedAllocation line 14

   Source documentation

   Fresh bit and list cells in the actual indexed coarse evaluator. Input arrays and random draws are shared; virtual source trees are never materialized. Child offsets/descriptors follow the repeated reads charged by the executable evaluator.

   def coarseIndexedAllocation {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

2. theorem OAI.EditApproximation.BinaryFraction.coarseIndexedAllocation_le_work line 58