CompactLaplacian.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Zero total mass of a compactly supported weak Laplacian

A radial Sobolev cutoff supplies the test function equal to one on both supports. Locality makes its energy pairing vanish. No constant global Sobolev function or finiteness of the ambient measure is needed.

theorem OAI.RegularPointCoordinates.integral_weakLaplacian_eq_zero line 26
Source documentation
The integral of a weak Laplacian vanishes when the function and source are both supported in a fixed ball.
```
theorem integral_weakLaplacian_eq_zero (u : SobolevSpace μ hQ) (q : Lp ℝ 2 μ)
    (hd : IsWeakLaplacian μ hQ u q) (p : X) {R : ℝ} (hR : 0 < R)
    (hu : ∀ᵐ x ∂μ, R < dist p x → SobolevSpace.toLp μ hQ u x = 0)
    (hq : ∀ᵐ x ∂μ, R < dist p x → q x = 0) :
    ∫ x, q x ∂μ = 0 := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.IsWeakLaplacian, OAI.RegularPointCoordinates.SobolevSpace.toLp