OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Programs/NonperiodicAtoms.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Certified evaluation of a flat smooth atom at an approximate real argument. A global derivative bound controls the argument error.

  1. def OAI.ForcedComputation.profileNoCoord line 14
  2. theorem OAI.ForcedComputation.profileNoCoord_bound line 19
  3. def OAI.ForcedComputation.SmoothAtom.derivativeBound line 36
  4. theorem OAI.ForcedComputation.SmoothAtom.lipschitz_bound line 38
  5. def OAI.ForcedComputation.ProfileEvaluation.Ready line 51
  6. instance OAI.ForcedComputation.ProfileEvaluation.(instance at line 53) line 53
  7. theorem OAI.ForcedComputation.ProfileEvaluation.ready_exists line 56
  8. def OAI.ForcedComputation.ProfileEvaluation.evaluate line 62
  9. theorem OAI.ForcedComputation.ProfileEvaluation.evaluate_spec line 65
  10. def OAI.ForcedComputation.SmoothAtom.enclose line 72
  11. theorem OAI.ForcedComputation.SmoothAtom.enclose_contains line 77
  12. theorem OAI.ForcedComputation.SmoothAtom.enclose_converges line 92