OAI/Combinatorics/EditApproximation/Geometry/PrefixBitEnvelope.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Fixed-degree polynomial envelope for the literal prefix and band-test arithmetic. The finite expression represents the bit counters; its degree is independent of every input length and parameter.

  1. abbrev OAI.EditApproximation.PE line 12
  2. def OAI.EditApproximation.ps line 14
  3. def OAI.EditApproximation.pn line 15
  4. def OAI.EditApproximation.peSumWord line 17
  5. def OAI.EditApproximation.peSumBit line 19
  6. def OAI.EditApproximation.peSumStorage line 20
  7. def OAI.EditApproximation.peConnectionWord line 21
  8. def OAI.EditApproximation.peConnectionBit line 22
  9. def OAI.EditApproximation.pePrefixWord line 25
  10. def OAI.EditApproximation.pePrefixBit line 27
  11. def OAI.EditApproximation.pePrefixMinimumBit line 32
  12. def OAI.EditApproximation.peAffineBit line 35
  13. def OAI.EditApproximation.peCutWord line 38
  14. def OAI.EditApproximation.peCutBit line 39
  15. def OAI.EditApproximation.peNaturalDistanceBit line 42
  16. def OAI.EditApproximation.peToleranceBit line 44
  17. def OAI.EditApproximation.prefixAggregateExpression line 46
  18. def OAI.EditApproximation.prefixArithmeticDegree line 55

    Source documentation

    Fixed degree of the prefix/guard arithmetic implementation.

    def prefixArithmeticDegree : ℕ := prefixAggregateExpression.degree
  19. def OAI.EditApproximation.prefixEnv line 57
  20. theorem OAI.EditApproximation.prefixAggregateExpression_eval line 63
  21. theorem OAI.EditApproximation.prefix_guard_budgets_le_fixed_power line 70