OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/NormalizationQuadrature.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Literal quadrature of the actual squared resolvent. Each sample is computed by the fixed Taylor/heat program, with its proved error.

  1. abbrev OAI.ContinuumCoulomb.NormalizationQuadrature.Settings line 14
  2. abbrev OAI.ContinuumCoulomb.NormalizationQuadrature.Input line 15
  3. def OAI.ContinuumCoulomb.NormalizationQuadrature.settingsCode line 17
  4. def OAI.ContinuumCoulomb.NormalizationQuadrature.sample line 19
  5. def OAI.ContinuumCoulomb.NormalizationQuadrature.value line 22
  6. opaque OAI.ContinuumCoulomb.NormalizationQuadrature.sampleProgram line 24
  7. opaque OAI.ContinuumCoulomb.NormalizationQuadrature.program line 38
  8. def OAI.ContinuumCoulomb.NormalizationQuadrature.certificate line 42
  9. theorem OAI.ContinuumCoulomb.NormalizationQuadrature.sample_error line 46
  10. theorem OAI.ContinuumCoulomb.NormalizationQuadrature.error line 57