OAI/Combinatorics/EditApproximation/Refinement/PhysicalTreeGeneric.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Generic cumulative regret at actual comparison-tree slots, including stopped slots.

  1. def OAI.EditApproximation.physicalComparisonTreeRegret line 29
  2. theorem OAI.EditApproximation.physicalClippedTable_at_stopped line 34
  3. theorem OAI.EditApproximation.physicalComparisonTreeRegret_none line 42
  4. theorem OAI.EditApproximation.physicalComparisonTreeRegret_stopped line 52
  5. theorem OAI.EditApproximation.physicalComparisonTreeRegret_active line 71
  6. theorem OAI.EditApproximation.physicalComparisonTreeRegret_generic line 112
  7. theorem OAI.EditApproximation.physicalComparisonBadRegret_bound line 150