OAI/Combinatorics/EditApproximation/Probability/FiniteBufferRanges.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The default-zero finite buffers preserve the nonnegative bounds of paired initial/history coordinates when the initial buffer covers them.

  1. theorem OAI.EditApproximation.finiteAnswerTable_eq_zero_of_not_mem line 10
  2. theorem OAI.EditApproximation.finiteAnswerTable_nonneg line 23
  3. theorem OAI.EditApproximation.finiteAnswerTable_map_le_of_subset line 37