OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/RationalHeatSample.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Actual rational evaluation of the heat-resolvent integrand. Both π and the exponential are computed by rational approximation programs. Clamping the computed π below by one keeps every denominator quantitative.

  1. def OAI.ContinuumCoulomb.RationalHeatSample.safePi line 15
  2. theorem OAI.ContinuumCoulomb.RationalHeatSample.safePi_ge_one line 17
  3. theorem OAI.ContinuumCoulomb.RationalHeatSample.safePi_error line 20
  4. def OAI.ContinuumCoulomb.RationalHeatSample.safePiProgram line 32
  5. abbrev OAI.ContinuumCoulomb.RationalHeatSample.Point line 45
  6. abbrev OAI.ContinuumCoulomb.RationalHeatSample.Arguments line 46
  7. abbrev OAI.ContinuumCoulomb.RationalHeatSample.Settings line 47
  8. abbrev OAI.ContinuumCoulomb.RationalHeatSample.Input line 48
  9. def OAI.ContinuumCoulomb.RationalHeatSample.pointCode line 50
  10. def OAI.ContinuumCoulomb.RationalHeatSample.argumentsCode line 51
  11. def OAI.ContinuumCoulomb.RationalHeatSample.settingsCode line 52
  12. def OAI.ContinuumCoulomb.RationalHeatSample.inputCode line 53
  13. def OAI.ContinuumCoulomb.RationalHeatSample.exponent line 55
  14. def OAI.ContinuumCoulomb.RationalHeatSample.value line 58
  15. def OAI.ContinuumCoulomb.RationalHeatSample.exponentProgram line 62
  16. def OAI.ContinuumCoulomb.RationalHeatSample.program line 79
  17. def OAI.ContinuumCoulomb.RationalHeatSample.certificate line 98
  18. theorem OAI.ContinuumCoulomb.RationalHeatSample.ratio_error line 101
  19. theorem OAI.ContinuumCoulomb.RationalHeatSample.exponent_nonpos line 126
  20. theorem OAI.ContinuumCoulomb.RationalHeatSample.position_sub_norm_sq line 134
  21. theorem OAI.ContinuumCoulomb.RationalHeatSample.exact_density line 142
  22. theorem OAI.ContinuumCoulomb.RationalHeatSample.error line 158