OAI/Combinatorics/EditApproximation/Coarse/CoarseIndexedControlSpace.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.EditApproximation.BinaryFraction.coarseIndexedInvocations line 12

   Source documentation

   Conservative recursive invocation count for the indexed evaluator, including scalar callees, index traversals and repeated descriptor reads.

   def coarseIndexedInvocations {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.arithmeticMapInvocations_with_indices_le_work line 54
3. theorem OAI.EditApproximation.BinaryFraction.coarseIndexedInvocations_le_work line 67