OAI/Combinatorics/EditApproximation/Geometry/BandEnvelopeBits.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Encoding lengths of the actual finite maxima and dyadic envelopes. These estimates include the scales below one and require no good seed.

  1. theorem OAI.EditApproximation.positive_rational_binary_bounds line 11
  2. theorem OAI.EditApproximation.rationalDyadicCeiling_encoding line 35
  3. theorem OAI.EditApproximation.rationalMaximum_encoding line 65
  4. def OAI.EditApproximation.bandEnvelopeEncodingBudget line 79
  5. theorem OAI.EditApproximation.bandChildEnvelope_encoding line 82