OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/RationalHeatBox.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Three literal nested quadratures for the heat representation of the planar resolvent. The two spatial integrals run over [-1,1], which contains the support of the forcing. All sample counts are unary.

  1. abbrev OAI.ContinuumCoulomb.RationalHeatBox.Settings line 13
  2. abbrev OAI.ContinuumCoulomb.RationalHeatBox.PlaneEnvironment line 14
  3. abbrev OAI.ContinuumCoulomb.RationalHeatBox.LineEnvironment line 15
  4. def OAI.ContinuumCoulomb.RationalHeatBox.settingsCode line 17
  5. def OAI.ContinuumCoulomb.RationalHeatBox.planeCode line 20
  6. def OAI.ContinuumCoulomb.RationalHeatBox.lineCode line 21
  7. def OAI.ContinuumCoulomb.RationalHeatBox.sample line 23
  8. def OAI.ContinuumCoulomb.RationalHeatBox.lineInput line 26
  9. def OAI.ContinuumCoulomb.RationalHeatBox.line line 29
  10. def OAI.ContinuumCoulomb.RationalHeatBox.planeInput line 32
  11. def OAI.ContinuumCoulomb.RationalHeatBox.plane line 35
  12. abbrev OAI.ContinuumCoulomb.RationalHeatBox.Input line 38
  13. def OAI.ContinuumCoulomb.RationalHeatBox.inputCode line 40
  14. def OAI.ContinuumCoulomb.RationalHeatBox.value line 42
  15. def OAI.ContinuumCoulomb.RationalHeatBox.sampleProgram line 44
  16. def OAI.ContinuumCoulomb.RationalHeatBox.lineInputProgram line 60
  17. def OAI.ContinuumCoulomb.RationalHeatBox.lineProgram line 75
  18. def OAI.ContinuumCoulomb.RationalHeatBox.planeInputProgram line 80
  19. def OAI.ContinuumCoulomb.RationalHeatBox.planeProgram line 94
  20. def OAI.ContinuumCoulomb.RationalHeatBox.program line 99
  21. def OAI.ContinuumCoulomb.RationalHeatBox.certificate line 103