OAI/Combinatorics/EditApproximation/Refinement/ComputedComparisonBand.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The comparison band uses the computed numerical parameters, with its error budget proved.

  1. theorem OAI.EditApproximation.comparisonActionCurvature_nonneg line 12
  2. theorem OAI.EditApproximation.computed_comparison_band_mem line 37