OAI/Combinatorics/EditApproximation/Refinement/PhysicalGenericRegret.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The generic regret bound for the actual complete physical recurrence.

  1. theorem OAI.EditApproximation.physicalNode_generic_regret line 43
  2. theorem OAI.EditApproximation.physicalComparison_mass_upper line 109
  3. theorem OAI.EditApproximation.physicalNode_generic_regret_upper line 131
  4. theorem OAI.EditApproximation.physicalNode_near_length_gap_regret line 138