OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/ManufacturedVelocityEvaluation.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The actual manufactured Moser velocity is sampled using rational coordinate differences, the certified scalar field evaluator and π. No value or derivative evaluator is assumed.

  1. def OAI.ContinuumCoulomb.ManufacturedVelocityEvaluation.precision line 17
  2. def OAI.ContinuumCoulomb.ManufacturedVelocityEvaluation.sample line 20
  3. def OAI.ContinuumCoulomb.ManufacturedVelocityEvaluation.gradient line 23
  4. def OAI.ContinuumCoulomb.ManufacturedVelocityEvaluation.laplacian line 26
  5. def OAI.ContinuumCoulomb.ManufacturedVelocityEvaluation.pi line 29
  6. def OAI.ContinuumCoulomb.ManufacturedVelocityEvaluation.component line 31
  7. def OAI.ContinuumCoulomb.ManufacturedVelocityEvaluation.value line 37
  8. theorem OAI.ContinuumCoulomb.ManufacturedVelocityEvaluation.pi_error line 41
  9. theorem OAI.ContinuumCoulomb.ManufacturedVelocityEvaluation.precision_budget line 48
  10. theorem OAI.ContinuumCoulomb.ManufacturedVelocityEvaluation.gradient_laplacian_error line 63
  11. theorem OAI.ContinuumCoulomb.ManufacturedVelocityEvaluation.approximation_error line 100