OAI/Combinatorics/EditApproximation/Binary/BinaryGroupKernel.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Literal group estimates on gathered stored fractions. Each child/scale comparison is executed, the supplied draw indices are reused, and ordered selection uses the same tie rule as the mathematical group program.

  1. theorem OAI.EditApproximation.BinaryFraction.equalWithWork_value line 19
  2. theorem OAI.EditApproximation.BinaryFraction.equalWithWork_cost line 24
  3. theorem OAI.EditApproximation.BinaryFraction.groupTermsWithWork_value line 33
  4. theorem OAI.EditApproximation.BinaryFraction.groupIndexWithWork_value line 50
  5. def OAI.EditApproximation.BinaryFraction.groupIndexBitBudget line 56
  6. theorem OAI.EditApproximation.BinaryFraction.groupIndexWithWork_bounds line 59
  7. def OAI.EditApproximation.BinaryFraction.groupScaleWithWork line 90
  8. theorem OAI.EditApproximation.BinaryFraction.groupScaleWithWork_value line 98
  9. def OAI.EditApproximation.BinaryFraction.groupScaleTermCount line 110
  10. def OAI.EditApproximation.BinaryFraction.groupScaleWordBudget line 112
  11. def OAI.EditApproximation.BinaryFraction.groupScaleBitBudget line 115
  12. theorem OAI.EditApproximation.BinaryFraction.groupScaleWithWork_bounds line 119
  13. def OAI.EditApproximation.BinaryFraction.groupMemberWithWork line 156

    Source documentation

    Every scale is accumulated using the same finite child arrays.

    def groupMemberWithWork {M T : ℕ} (scales : Fin T → BinaryFraction) (count : Fin T → ℕ)
    (connection : BinaryFraction) (envelope values : Vector BinaryFraction M)
    (draw : ∀ s : Fin T, Fin (count s) → Fin M) : BinaryFraction × ℕ :=
…

    Mentions: OAI.EditApproximation.BinaryFraction

  14. theorem OAI.EditApproximation.BinaryFraction.groupMemberWithWork_value line 165
  15. def OAI.EditApproximation.BinaryFraction.groupMemberWordBudget line 176
  16. def OAI.EditApproximation.BinaryFraction.groupMemberBitBudget line 179
  17. theorem OAI.EditApproximation.BinaryFraction.groupMemberWithWork_bounds line 183
  18. theorem OAI.EditApproximation.BinaryFraction.selectGroupWithWork_value line 220
  19. theorem OAI.EditApproximation.BinaryFraction.selectGroupWithWork_cost line 229