OAI/Combinatorics/EditApproximation/Refinement/PhysicalTreeNear.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Actual non-bad nodes with near-unit length-gap prediction have small regret.

  1. theorem OAI.EditApproximation.physicalComparisonTreeRegret_near line 30
  2. theorem OAI.EditApproximation.physicalComparisonNearRegret_bound line 104