OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/PlanarLaplaceIBP.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Two integrations by parts transfer the planar Laplacian from the Gaussian kernel to the compact forcing.

  1. theorem OAI.ContinuumCoulomb.planarPartial_reflect line 13
  2. theorem OAI.ContinuumCoulomb.planarPartial_neg line 23
  3. theorem OAI.ContinuumCoulomb.planarLaplacian_reflect line 31
  4. theorem OAI.ContinuumCoulomb.planar_integral_mul_laplacian_C2 line 44
  5. theorem OAI.ContinuumCoulomb.planarLaplacian_continuous line 93
  6. theorem OAI.ContinuumCoulomb.planarLaplacian_hasCompactSupport line 98
  7. theorem OAI.ContinuumCoulomb.planarHeatAverage_hasDerivAt_laplacian line 106