OAI/Combinatorics/EditApproximation/Binary/BinaryPreparedOnline.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The keyed online branch executes the actual endpoint grids before its guard and optimizer. The original finite source range is preserved.

  1. def OAI.EditApproximation.BinaryFraction.preparedOnlineBandReference line 12
  2. theorem OAI.EditApproximation.BinaryFraction.preparedOnlineBandReference_congr line 26
  3. def OAI.EditApproximation.BinaryFraction.preparedOnlineWithWork line 38
  4. theorem OAI.EditApproximation.BinaryFraction.preparedOnlineWithWork_value line 62