OAI/Combinatorics/EditApproximation/Binary/BinaryReductionSpace.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Actual reduction scratch: comparisons retain their cross-products; sums retain all dot-product intermediates and the materialized vectors.

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

    Source documentation

    Two materialized index/value list spines fit the dot loop's per-cell charge.

    theorem dotListAllocation_with_spines_le_work {d : ℕ}
    (left right : Vector BinaryFraction d) (indices : List (Fin d)) :
    dotListAllocation left right indices + 2 * indices.length ≤ (dotListWithWork left right indices).2 := by
…

    Mentions: OAI.EditApproximation.BinaryFraction, OAI.EditApproximation.BinaryFraction.dotListAllocation, OAI.EditApproximation.BinaryFraction.dotListWithWork

  2. theorem OAI.EditApproximation.BinaryFraction.dotListInvocations_with_spines_le_work line 26
  3. def OAI.EditApproximation.BinaryFraction.bandMassInvocations line 40
  4. theorem OAI.EditApproximation.BinaryFraction.bandMassAllocation_le_work line 43
  5. theorem OAI.EditApproximation.BinaryFraction.bandMassInvocations_le_work line 48
  6. def OAI.EditApproximation.BinaryFraction.minInvocations line 55
  7. theorem OAI.EditApproximation.BinaryFraction.minAllocation_le_work line 57
  8. theorem OAI.EditApproximation.BinaryFraction.minInvocations_le_work line 61
  9. def OAI.EditApproximation.BinaryFraction.minimumInvocations line 67
  10. theorem OAI.EditApproximation.BinaryFraction.minimumAllocation_le_work line 72
  11. theorem OAI.EditApproximation.BinaryFraction.minimumInvocations_le_work line 81
  12. def OAI.EditApproximation.BinaryFraction.maxInvocations line 92
  13. theorem OAI.EditApproximation.BinaryFraction.maxAllocation_le_work line 94
  14. theorem OAI.EditApproximation.BinaryFraction.maxInvocations_le_work line 98
  15. def OAI.EditApproximation.BinaryFraction.maximumInvocations line 104
  16. theorem OAI.EditApproximation.BinaryFraction.maximumAllocation_le_work line 109
  17. theorem OAI.EditApproximation.BinaryFraction.maximumInvocations_le_work line 118
  18. def OAI.EditApproximation.BinaryFraction.sumListInvocations line 129
  19. theorem OAI.EditApproximation.BinaryFraction.sumListAllocation_le_work line 133
  20. theorem OAI.EditApproximation.BinaryFraction.sumListInvocations_le_work line 141
  21. def OAI.EditApproximation.BinaryFraction.warmupAverageAllocation line 149
  22. def OAI.EditApproximation.BinaryFraction.warmupAverageInvocations line 153
  23. theorem OAI.EditApproximation.BinaryFraction.warmupAverageAllocation_le_work line 156
  24. theorem OAI.EditApproximation.BinaryFraction.warmupAverageInvocations_le_work line 164