OAI/Combinatorics/EditApproximation/Refinement/PhysicalTreeRegret.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The time and comparison-tree telescope for the actual clipped refinement values.

  1. theorem OAI.EditApproximation.comparisonPhysicalLift_mono line 13
  2. def OAI.EditApproximation.physicalClippedTable line 45
  3. def OAI.EditApproximation.physicalClippedLift line 49
  4. theorem OAI.EditApproximation.physicalClippedLift_antitone line 57
  5. theorem OAI.EditApproximation.physicalClippedLift_root line 66
  6. theorem OAI.EditApproximation.physicalClippedLift_terminal line 79
  7. theorem OAI.EditApproximation.physical_tree_regret_time line 84