OAI/MathematicalPhysics/ContinuumCoulomb/Programs/ManufacturedVelocityProgram.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

The manufactured Moser velocity has a literal polynomial TM2 evaluator. It composes the already certified field sampler, three fixed rational coordinate differences, and the clamped positive-density quotient.

  1. abbrev OAI.ContinuumCoulomb.ManufacturedVelocityEvaluation.Environment line 16
  2. def OAI.ContinuumCoulomb.ManufacturedVelocityEvaluation.environmentCode line 17
  3. def OAI.ContinuumCoulomb.ManufacturedVelocityEvaluation.sampleCode line 19
  4. abbrev OAI.ContinuumCoulomb.ManufacturedVelocityEvaluation.Input line 20
  5. def OAI.ContinuumCoulomb.ManufacturedVelocityEvaluation.inputCode line 21
  6. opaque OAI.ContinuumCoulomb.ManufacturedVelocityEvaluation.envPrecisionProgram line 23
  7. opaque OAI.ContinuumCoulomb.ManufacturedVelocityEvaluation.envDataProgram line 25
  8. opaque OAI.ContinuumCoulomb.ManufacturedVelocityEvaluation.envParametersProgram line 28
  9. opaque OAI.ContinuumCoulomb.ManufacturedVelocityEvaluation.envSitesProgram line 30
  10. opaque OAI.ContinuumCoulomb.ManufacturedVelocityEvaluation.innerPrecisionProgram line 32
  11. opaque OAI.ContinuumCoulomb.ManufacturedVelocityEvaluation.sampleEnvironmentProgram line 36
  12. opaque OAI.ContinuumCoulomb.ManufacturedVelocityEvaluation.samplePointProgram line 38
  13. opaque OAI.ContinuumCoulomb.ManufacturedVelocityEvaluation.samplePrecisionProgram line 40
  14. opaque OAI.ContinuumCoulomb.ManufacturedVelocityEvaluation.sampleDataProgram line 43
  15. opaque OAI.ContinuumCoulomb.ManufacturedVelocityEvaluation.scalarSampleProgram line 48
  16. opaque OAI.ContinuumCoulomb.ManufacturedVelocityEvaluation.spatialStepProgram line 53
  17. opaque OAI.ContinuumCoulomb.ManufacturedVelocityEvaluation.gradientProgram line 57
  18. opaque OAI.ContinuumCoulomb.ManufacturedVelocityEvaluation.laplacianProgram line 64
  19. opaque OAI.ContinuumCoulomb.ManufacturedVelocityEvaluation.piProgram line 71
  20. opaque OAI.ContinuumCoulomb.ManufacturedVelocityEvaluation.inputEnvironmentProgram line 75
  21. opaque OAI.ContinuumCoulomb.ManufacturedVelocityEvaluation.inputTimePointProgram line 77
  22. opaque OAI.ContinuumCoulomb.ManufacturedVelocityEvaluation.inputTimeProgram line 79
  23. opaque OAI.ContinuumCoulomb.ManufacturedVelocityEvaluation.inputPointProgram line 81
  24. opaque OAI.ContinuumCoulomb.ManufacturedVelocityEvaluation.inputSampleProgram line 83
  25. opaque OAI.ContinuumCoulomb.ManufacturedVelocityEvaluation.rawDenominatorProgram line 85
  26. opaque OAI.ContinuumCoulomb.ManufacturedVelocityEvaluation.maxDensityProgram line 93
  27. opaque OAI.ContinuumCoulomb.ManufacturedVelocityEvaluation.denominatorProgram line 104
  28. opaque OAI.ContinuumCoulomb.ManufacturedVelocityEvaluation.coreComponentProgram line 108
  29. opaque OAI.ContinuumCoulomb.ManufacturedVelocityEvaluation.preparedEnvironmentProgram line 114
  30. opaque OAI.ContinuumCoulomb.ManufacturedVelocityEvaluation.preparedInputProgram line 117
  31. opaque OAI.ContinuumCoulomb.ManufacturedVelocityEvaluation.componentProgram line 120
  32. opaque OAI.ContinuumCoulomb.ManufacturedVelocityEvaluation.program line 125
  33. def OAI.ContinuumCoulomb.ManufacturedVelocityEvaluation.certificate line 129