OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/ManufacturedFieldEvaluation.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

A rational scalar evaluator for the actual manufactured well field. The well-depth factors are clipped to their proved interval [1,2]. This stabilizes every encoded input and preserves the valid-instance estimate.

  1. def OAI.ContinuumCoulomb.ManufacturedFieldEvaluation.coefficient line 16
  2. def OAI.ContinuumCoulomb.ManufacturedFieldEvaluation.translate line 19
  3. def OAI.ContinuumCoulomb.ManufacturedFieldEvaluation.planar line 21
  4. def OAI.ContinuumCoulomb.ManufacturedFieldEvaluation.rawValue line 25
  5. theorem OAI.ContinuumCoulomb.ManufacturedFieldEvaluation.coefficient_bounds line 30
  6. theorem OAI.ContinuumCoulomb.ManufacturedFieldEvaluation.translate_position line 36
  7. theorem OAI.ContinuumCoulomb.ManufacturedFieldEvaluation.coefficient_error line 42
  8. theorem OAI.ContinuumCoulomb.ManufacturedFieldEvaluation.well_abs_le_guard line 65
  9. theorem OAI.ContinuumCoulomb.ManufacturedFieldEvaluation.product_error line 71
  10. theorem OAI.ContinuumCoulomb.ManufacturedFieldEvaluation.planar_error line 82
  11. theorem OAI.ContinuumCoulomb.ManufacturedFieldEvaluation.planar_exact_bound line 124
  12. theorem OAI.ContinuumCoulomb.ManufacturedFieldEvaluation.raw_error line 149
  13. def OAI.ContinuumCoulomb.ManufacturedFieldEvaluation.precision line 181
  14. def OAI.ContinuumCoulomb.ManufacturedFieldEvaluation.value line 183
  15. theorem OAI.ContinuumCoulomb.ManufacturedFieldEvaluation.precision_budget line 186
  16. theorem OAI.ContinuumCoulomb.ManufacturedFieldEvaluation.approximation_error line 213