OAI/Combinatorics/EditApproximation/Geometry/BandNumericalBits.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The probability vectors actually stored for band actions have polynomial encodings in the input child masses. No accuracy event is needed.

  1. def OAI.EditApproximation.bandVertexEncodingBudget line 14
  2. theorem OAI.EditApproximation.actionVector_encoding_le line 17
  3. theorem OAI.EditApproximation.actionVector_zero_one line 36
  4. def OAI.EditApproximation.storedBandVertices line 48
  5. theorem OAI.EditApproximation.storedBandVertices_nonempty line 53
  6. theorem OAI.EditApproximation.storedBandVertices_input_bounds line 59
  7. theorem OAI.EditApproximation.storedBandOptimizer_history_bits line 77