The planar Newtonian kernel is a fundamental solution of -Δ

The logarithmic kernel G(z) = -(2π)⁻¹ log ‖z‖ on the plane ℂ satisfies the distributional identity -Δ G = δ₀: for every C² function f : ℂ → ℝ with compact support,

∫ z, Δ f z * G z = -f 0,

and, with the pole moved to a, ∫ z, Δ f z * G (z - a) = -f a. This is the two-dimensional counterpart of TauCeti.integral_laplacian_mul_newtonianKernel for ℝⁿ, n ≥ 3, and it is the identity that makes the planar Newtonian potential G ⋆ f solve Poisson's equation.

The argument has the same two steps as in higher dimensions.

• The weak gradient. G and its derivative -(2π)⁻¹ ‖z‖⁻² ⟪z, ·⟫ are locally integrable, and integration by parts against G holds across the pole: for a C¹ function g with compact support, ∫ G ∂ᵥg = -∫ (∂ᵥG) g. The kernel is replaced by the smooth regularizations -(4π)⁻¹ (log (‖z‖² + t) - log (1 + t)), which are dominated by |G| and converge to G as t → 0⁺, and dominated convergence passes to the limit. In particular G is weakly differentiable on every open set, with weak derivative its classical one.
• The flux. Summing over an orthonormal basis turns ∫ Δ f G into -∫ ∇G · ∇f = (2π)⁻¹ ∫ ‖z‖⁻² f' z z, which the radial fundamental theorem of calculus TauCeti.integral_norm_rpow_neg_finrank_mul_fderiv_apply_self evaluates to -f 0.

Main declarations

• TauCeti.locallyIntegrable_planarNewtonianKernel: G is locally integrable.
• TauCeti.locallyIntegrable_fderiv_planarNewtonianKernel: so is its derivative.
• TauCeti.integral_planarNewtonianKernel_mul_fderiv_eq_neg_fderiv_mul: integration by parts against G.
• TauCeti.hasWeakFDerivOn_planarNewtonianKernel: the classical derivative of G is its weak derivative.
• TauCeti.integral_laplacian_mul_planarNewtonianKernel: -Δ G = δ₀.
• TauCeti.integral_laplacian_mul_planarNewtonianKernel_sub: the same identity with the pole at a.

References

• L. C. Evans, Partial Differential Equations, Section 2.2.1, Theorem 1 (the case n = 2).
• D. Gilbarg, N. S. Trudinger, Elliptic Partial Differential Equations of Second Order, Section 2.4.

theorem TauCeti.locallyIntegrable_planarNewtonianKernel : MeasureTheory.LocallyIntegrable planarNewtonianKernel MeasureTheory.volume

The planar Newtonian kernel is locally integrable.

theorem TauCeti.locallyIntegrable_fderiv_planarNewtonianKernel : MeasureTheory.LocallyIntegrable (fderiv ℝ planarNewtonianKernel) MeasureTheory.volume

The Fréchet derivative of the planar Newtonian kernel is locally integrable: its norm is (2π ‖z‖)⁻¹, an integrable singularity in two dimensions.

theorem TauCeti.integral_planarNewtonianKernel_mul_fderiv_eq_neg_fderiv_mul {g : ℂ → ℝ} (hg : ContDiff ℝ 1 g) (hc : HasCompactSupport g) (v : ℂ) : ∫ (z : ℂ), planarNewtonianKernel z * (fderiv ℝ g z) v = -∫ (z : ℂ), (fderiv ℝ planarNewtonianKernel z) v * g z

Integration by parts against the planar Newtonian kernel. For a C¹ function g with compact support on ℂ, ∫ G ∂ᵥg = -∫ (∂ᵥG) g, although G is singular at the origin.

theorem TauCeti.hasWeakFDerivOn_planarNewtonianKernel (Ω : TopologicalSpace.Opens ℂ) : HasWeakFDerivOn MeasureTheory.volume Ω planarNewtonianKernel (fderiv ℝ planarNewtonianKernel)

The planar Newtonian kernel is weakly differentiable. On every open subset of ℂ, the classical derivative of G, which exists away from the origin, is a weak derivative of G.

theorem TauCeti.integral_laplacian_mul_planarNewtonianKernel {f : ℂ → ℝ} (hf : ContDiff ℝ 2 f) (hc : HasCompactSupport f) : ∫ (z : ℂ), Laplacian.laplacian f z * planarNewtonianKernel z = -f 0

The planar Newtonian kernel is a fundamental solution of -Δ. For every C² function f with compact support on ℂ, ∫ Δ f · G = -f 0; that is, -Δ G = δ₀ in the sense of distributions.

theorem TauCeti.integral_laplacian_mul_planarNewtonianKernel_sub {f : ℂ → ℝ} (hf : ContDiff ℝ 2 f) (hc : HasCompactSupport f) (a : ℂ) : ∫ (z : ℂ), Laplacian.laplacian f z * planarNewtonianKernel (z - a) = -f a

The planar Newtonian kernel with pole a is a fundamental solution of -Δ. For every C² function f with compact support on ℂ, ∫ Δ f · G(· - a) = -f a.