OAI/Combinatorics/EditApproximation/Refinement/StageParameterBounds.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Computed parameters for the actual local energy and online inequalities.

  1. theorem OAI.EditApproximation.refinementFactor_le line 10
  2. theorem OAI.EditApproximation.computed_initialFactor_twice_le_P line 18
  3. theorem OAI.EditApproximation.computed_refinementFactor_spacing line 35
  4. theorem OAI.EditApproximation.computed_online_range line 45