CoulombPoisson.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The Coulomb fundamental solution with finite smoothness

The manufactured planar well in the unit-charge paper has bounded continuous derivatives through a finite order. Its density synthesis therefore needs the fundamental-solution identity for compactly supported C² functions. This extends the smooth-test identity by the same regularized kernel argument, using only two integrations by parts.

theorem OAI.ContinuumCoulomb.integral_mul_laplacian_C2 line 22
theorem OAI.ContinuumCoulomb.coulomb_laplacian_C2 line 77
theorem OAI.ContinuumCoulomb.coulomb_translated_laplacian_C2 line 100
def OAI.ContinuumCoulomb.manufacturedCharge line 113
theorem OAI.ContinuumCoulomb.manufacturedCharge_integral_zero line 116
theorem OAI.ContinuumCoulomb.manufacturedCharge_potential line 125
Source documentation
Exact Green identity, with the sign for an attractive positive density.
```
theorem manufacturedCharge_potential (V : Position → ℝ) (hV : ContDiff ℝ 2 V)
    (hc : HasCompactSupport V) (y : Position) :
    -(∫ x, Coulomb.coulombKernel (y - x) * manufacturedCharge V x) = V y := by
…
```
Mentions: OAI.ContinuumCoulomb.Position, OAI.Coulomb.coulombKernel, OAI.ContinuumCoulomb.manufacturedCharge