OAI/Combinatorics/EditApproximation/Coarse/CoarseIndexedArrayHistory.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.EditApproximation.BinaryFraction.coarseIndexArrayHistory line 8
  2. theorem OAI.EditApproximation.BinaryFraction.coarseIndexArrayHistory_eq line 27
  3. def OAI.EditApproximation.BinaryFraction.coarseIndexedArrayHistory line 61

    Source documentation

    Every array footprint of the literal indexed recursion. Descriptor and address words are charged separately by the indexed bit counter.

    def coarseIndexedArrayHistory {B : ℕ} (k q L n : ℕ) (source target : List ℕ)
    (two : BinaryFraction) : (d offset : ℕ) → CoarseThresholdDraws B d → BinaryFraction → ℕ → ℕ
  | 0, offset, draws, allowance, start =>
    if (leWithWork (nat (coarseDescriptorLength B 0 n offset)) allowance).1 then 1 else
      coarseArrayStorage (coarseIndexedWithWork k q L n source target two 0 offset draws allowance start).1
  | d + 1, offset, (draws, below), allowance, start =>
    if (leWithWork (nat (coarseDescriptorLength B (d + 1) n offset)) allowance).1 then 1 else
      coarseArrayStorage (coarseIndexedWithWork k q L n source target two (d + 1) offset
        (draws, below) allowance start).1 +
      coarseIndexArrayHistory k q L two
        (fun i => coarseDescriptorLength B d n (offset + i.val * B ^ d))
        (fun i => coarseIndexedWithWork k q L n source target two d (offset + i.val * B ^ d) (below i))
…

    Mentions: OAI.EditApproximation.BinaryFraction, OAI.EditApproximation.CoarseThresholdDraws, OAI.EditApproximation.BinaryFraction.leWithWork, OAI.EditApproximation.BinaryFraction.nat, OAI.EditApproximation.coarseDescriptorLength, OAI.EditApproximation.BinaryFraction.coarseArrayStorage, OAI.EditApproximation.BinaryFraction.coarseIndexedWithWork, OAI.EditApproximation.BinaryFraction.coarseIndexArrayHistory

  4. theorem OAI.EditApproximation.BinaryFraction.coarseIndexedArrayHistory_eq line 78