OAI/Combinatorics/EditApproximation/Refinement/ComputedBands.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The literal finite predicted band

The band is a rationally decidable filter of the enumerated wide actions. Its internal-cut diameter follows from the actual finite prefix predictor, without assuming a predictor Lipschitz contract.

  1. theorem OAI.EditApproximation.computedBandActions_mem line 27
  2. theorem OAI.EditApproximation.computedBandActions_complete line 43
  3. theorem OAI.EditApproximation.computedBand_cut_diameter line 54