OAI/Combinatorics/EditApproximation/Geometry/ActualBandBitEnvelope.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A fixed polynomial bounds the complete envelope construction and band optimizer. In particular the child masses are computed from the initial table, rather than supplied as already constructed binary fractions.

  1. theorem OAI.EditApproximation.square_work_cap line 12
  2. theorem OAI.EditApproximation.square_work_with_constant_cap line 18
  3. theorem OAI.EditApproximation.bandEnvelopeBitBudget_le_power line 27
  4. def OAI.EditApproximation.actualBandOptimizerBitDegree line 71
  5. theorem OAI.EditApproximation.actualBandOptimizerBitBudget_le_fixed_power line 73