OAI/Combinatorics/EditApproximation/Binary/BinaryCountedActionSpace.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

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

   Source documentation

   All counted optimizer allocations, including coordinate construction.

   theorem countedPreparedActionAllocation_le_work {M n : ℕ} (mass : Vector BinaryFraction M)
       (read : ℕ → Fin M × TargetInterval n → BinaryFraction × ℕ)
       (footprint : ℕ → Fin M × TargetInterval n → ℕ)
       (eta kappa : BinaryFraction) (band : List (Fin M → TargetInterval n)) (G j t : ℕ)
       (h : ∀ s coordinate, footprint s coordinate ≤ (read s coordinate).2) :
       countedPreparedActionAllocation mass read footprint eta kappa band G j t ≤
         3 * (countedPreparedActionReadWithWork mass read eta kappa band G j t).2 := by
   …

   Mentions: OAI.EditApproximation.BinaryFraction, OAI.EditApproximation.TargetInterval, OAI.EditApproximation.BinaryFraction.countedPreparedActionAllocation, OAI.EditApproximation.BinaryFraction.countedPreparedActionReadWithWork

2. theorem OAI.EditApproximation.BinaryFraction.countedBandActionAllocation_le_work line 33
3. def OAI.EditApproximation.BinaryFraction.queryCountedActionAllocation line 51

   Source documentation

   The actual gathered-history specialization of the labeled action sampler.

   def queryCountedActionAllocation {M n : ℕ} (mass : Vector BinaryFraction M)
       (keys : List (Fin M × ℕ × TargetInterval n)) (values : List BinaryFraction)
       (eta kappa : BinaryFraction) (band : List (Fin M → TargetInterval n)) (G j t : ℕ) : ℕ :=
   …

   Mentions: OAI.EditApproximation.BinaryFraction, OAI.EditApproximation.TargetInterval

4. theorem OAI.EditApproximation.BinaryFraction.queryCountedActionAllocation_le_work line 57