OAI/Combinatorics/EditApproximation/Geometry/RefinementErrorTerms.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Explicit estimates for the actual four parts of the refinement error.

  1. theorem OAI.EditApproximation.refinement_grid_error line 9
  2. theorem OAI.EditApproximation.refinement_excluded_error line 26
  3. theorem OAI.EditApproximation.refinement_depth_ratios line 57
  4. theorem OAI.EditApproximation.refinement_ordinary_error line 88
  5. theorem OAI.EditApproximation.refinement_numerical_error line 119
  6. theorem OAI.EditApproximation.refinement_error_from_stage_bounds line 135
  7. def OAI.EditApproximation.computedRefinementError line 172
  8. theorem OAI.EditApproximation.computedRefinementError_lt line 188