OAI/Combinatorics/EditApproximation/Coarse/CoarseBinaryWeight.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

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

   Source documentation

   Sum the weights of exactly those child calls made by the binary loop.

   def coarseBinaryChildrenWeight {B d : ℕ} {α : Type*} (q L : ℕ)
       (weight : CoarseSourceTree B α d → CoarseThresholdDraws B d → BinaryFraction → ℕ)
       (allowance : BinaryFraction) :
       List (CoarseSourceTree B α d × Fin B × CoarseThresholdDraws B d) → ℕ
     | [] => 0
     | (child, draw, below) :: rest =>
       weight child below (coarseChildAllowanceWithWork L
         (coarseChildThresholdWithWork B q allowance draw).1).1 +
       coarseBinaryChildrenWeight q L weight allowance rest
   
   /-- One array unit per expanded child shift and one unit per visited node.
   This counter follows the executed pruning and threshold branches. -/

   Mentions: OAI.EditApproximation.CoarseSourceTree, OAI.EditApproximation.CoarseThresholdDraws, OAI.EditApproximation.BinaryFraction, OAI.EditApproximation.BinaryFraction.coarseChildAllowanceWithWork, OAI.EditApproximation.BinaryFraction.coarseChildThresholdWithWork, OAI.EditApproximation.BinaryFraction.one

2. def OAI.EditApproximation.BinaryFraction.coarseBinaryWeight line 22

   Source documentation

   One array unit per expanded child shift and one unit per visited node. This counter follows the executed pruning and threshold branches.

   def coarseBinaryWeight {B : ℕ} {α : Type*} (k q L : ℕ) :
       {d : ℕ} → CoarseSourceTree B α d → CoarseThresholdDraws B d → BinaryFraction → ℕ
     | _, tree, draws, allowance =>
       if (leWithWork (nat tree.word.length) allowance).1 then 1 else
       match tree, draws with
       | .leaf _, _ => B * (2 * k + 1) + 1
       | .branch children, (draws, below) => B * (2 * k + 1) + 1 +
         coarseBinaryChildrenWeight q L (fun child => coarseBinaryWeight k q L child) allowance
           (List.ofFn fun i => (children i, draws i, below i))

   Mentions: OAI.EditApproximation.CoarseSourceTree, OAI.EditApproximation.CoarseThresholdDraws, OAI.EditApproximation.BinaryFraction, OAI.EditApproximation.BinaryFraction.leWithWork, OAI.EditApproximation.BinaryFraction.nat, OAI.EditApproximation.BinaryFraction.coarseBinaryChildrenWeight

3. def OAI.EditApproximation.BinaryFraction.coarseChildrenSpan line 32
4. theorem OAI.EditApproximation.BinaryFraction.coarseChildrenSpan_eq line 37
5. theorem OAI.EditApproximation.BinaryFraction.coarseChildrenSpan_ofFn line 45