OAI/Combinatorics/EditApproximation/Binary/BinaryGroupSourceSpace.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.BinaryFraction.groupScaleSourceAllocation_le_work line 13

   Source documentation

   Index decoding, the sampled index spine and the exact/sample reduction.

   theorem groupScaleSourceAllocation_le_work {M : ℕ} (k : ℕ) (h : BinaryFraction)
       (envelope values : Vector BinaryFraction M) (draw : Fin k → Fin M × ℕ)
       (allocation : Fin k → ℕ) (ha : ∀ i, allocation i ≤ (draw i).2) :
       groupScaleSourceAllocation k h envelope values draw allocation ≤
         (groupScaleSourceWithWork k h envelope values draw).2 := by
   …

   Mentions: OAI.EditApproximation.BinaryFraction, OAI.EditApproximation.BinaryFraction.groupScaleSourceAllocation, OAI.EditApproximation.BinaryFraction.groupScaleSourceWithWork

2. theorem OAI.EditApproximation.BinaryFraction.groupMemberSourceAllocation_le_work line 36
3. theorem OAI.EditApproximation.BinaryFraction.countedGroupMemberSourceAllocation_le_work line 57