OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/PlanarHeatKernel.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The actual normalized two-dimensional Gaussian heat kernel and its convolution with the paper's explicit forcing. These prepare the positive resolvent mode, rather than assuming the manufactured well exists.

  1. def OAI.ContinuumCoulomb.planarHeatKernel line 14
  2. theorem OAI.ContinuumCoulomb.planarHeatKernel_positive line 17
  3. theorem OAI.ContinuumCoulomb.planarHeatKernel_continuous line 21
  4. theorem OAI.ContinuumCoulomb.planar_gaussian_integrable line 25
  5. theorem OAI.ContinuumCoulomb.planarHeatKernel_integrable line 34
  6. theorem OAI.ContinuumCoulomb.planarHeatKernel_integral line 44
  7. def OAI.ContinuumCoulomb.planarHeatAverage line 57
  8. theorem OAI.ContinuumCoulomb.planarHeatAverage_integrand_integrable line 60
  9. theorem OAI.ContinuumCoulomb.planarHeatAverage_positive line 69
  10. theorem OAI.ContinuumCoulomb.planarHeatAverage_le_one line 79