OAI/Combinatorics/EditApproximation/Coarse/CoarseIndexedChildren.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.BinaryFraction.coarseIndexChildren_eq line 14

   Source documentation

   The executable child loop carries indices and cached subtree lengths. In particular it never flattens a semantic source tree to obtain its length.

   theorem coarseIndexChildren_eq {B d : ℕ} {α : Type*} (k q L : ℕ) (two : BinaryFraction)
       (width : Fin B → ℕ) (children : Fin B → CoarseSourceTree B α d)
       (evaluate : CoarseSourceTree B α d → CoarseThresholdDraws B d → BinaryFraction → ℕ →
         CoarseBinaryArray × ℕ)
       (indexed : Fin B → BinaryFraction → ℕ → CoarseBinaryArray × ℕ)
       (draw : Fin B → Fin B) (below : Fin B → CoarseThresholdDraws B d)
       (hw : ∀ i, width i = (children i).word.length)
       (he : ∀ i a start, indexed i a start = evaluate (children i) (below i) a start)
       (allowance : BinaryFraction) (indices : List (Fin B)) (start : ℕ) :
       coarseIndexChildren k q L two width indexed draw allowance indices start =
         coarseBinaryChildren k q L two evaluate allowance
           (indices.map fun i => (children i, draw i, below i)) start := by
   …

   Mentions: OAI.EditApproximation.BinaryFraction, OAI.EditApproximation.BinaryFraction.width, OAI.EditApproximation.CoarseSourceTree, OAI.EditApproximation.CoarseThresholdDraws, OAI.EditApproximation.BinaryFraction.CoarseBinaryArray, OAI.EditApproximation.BinaryFraction.coarseIndexChildren, OAI.EditApproximation.BinaryFraction.coarseBinaryChildren