OAI/Combinatorics/EditApproximation/Refinement/PhysicalSubtreeNear.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.subtreeComparisonTreeRegret_near line 30
  2. theorem OAI.EditApproximation.subtreeComparisonNearRegret_bound line 104