OAI/Combinatorics/EditApproximation/Coarse/CoarseArrayStorage.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

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

   Source documentation

   The stored numerator bits, denominator bits, sign and list links.

   def coarseArrayStorage : CoarseBinaryArray → ℕ
     | none => 1
     | some cells => 1 + (cells.map fun a => a.numerator.bits.length + a.denominator.length + 3).sum

   Mentions: OAI.EditApproximation.BinaryFraction.CoarseBinaryArray

2. theorem OAI.EditApproximation.BinaryFraction.coarseArrayStorage_le line 14
3. def OAI.EditApproximation.BinaryFraction.coarseRootArray line 41

   Source documentation

   The actual array immediately before the root lookup.

   def coarseRootArray {B d : ℕ} {α : Type*} [DecidableEq α]
       (k q L : ℕ) (hB : 0 < B) (hq : 0 < q) (hL : 0 < L)
       (frame : List (Option α)) (tree : CoarseSourceTree B α d)
       (draws : CoarseThresholdDraws B d) (start : ℕ) : CoarseBinaryArray :=
   …

   Mentions: OAI.EditApproximation.CoarseSourceTree, OAI.EditApproximation.CoarseThresholdDraws, OAI.EditApproximation.BinaryFraction.CoarseBinaryArray

4. theorem OAI.EditApproximation.BinaryFraction.coarseRootArray_storage line 51
5. def OAI.EditApproximation.BinaryFraction.coarseIndexedRootArray line 91
6. theorem OAI.EditApproximation.BinaryFraction.coarseIndexedRootArray_eq line 100