The planar Newtonian kernel away from its pole

This file introduces the logarithmic kernel for the negative Laplacian on the complex plane,

G(z) = -(2 * π)⁻¹ * log ‖z‖,

and establishes its classical pointwise properties away from the pole. In particular, G and each translate z ↦ G (z - a) are harmonic away from their poles. The distributional identity -Δ G = δ₀, which fixes the normalization by computing the flux through a circle, is deliberately left to the later distributional development of the fundamental solution.

The harmonicity proof consumes Mathlib's AnalyticAt.harmonicAt_log_norm, applied to the identity or to z ↦ z - a. The remaining results record the translation, symmetry, and scaling API used when the kernel is integrated against a source to form a Newtonian potential.

Main declarations

• TauCeti.planarNewtonianKernel: the logarithmic kernel for -Δ on ℂ.
• TauCeti.harmonicAt_planarNewtonianKernel: harmonicity away from the origin.
• TauCeti.harmonicAt_planarNewtonianKernel_sub: harmonicity of a kernel with pole a.
• TauCeti.laplacian_planarNewtonianKernel: the pointwise equation Δ G = 0 off the pole.

noncomputable def TauCeti.planarNewtonianKernel (z : ℂ) : ℝ

The Newtonian kernel for the negative Laplacian on the plane, represented as ℂ.

The value assigned at the pole is immaterial for the pointwise theory in this file. Lean's convention Real.log 0 = 0 makes this a total function; analytically, the kernel has a logarithmic singularity there.

Equations

• TauCeti.planarNewtonianKernel z = -(2 * Real.pi)⁻¹ * Real.log ‖z‖

theorem TauCeti.planarNewtonianKernel_def (z : ℂ) : planarNewtonianKernel z = -(2 * Real.pi)⁻¹ * Real.log ‖z‖

The defining formula for the planar Newtonian kernel.

@[simp]

theorem TauCeti.planarNewtonianKernel_zero : planarNewtonianKernel 0 = 0

@[simp]

theorem TauCeti.planarNewtonianKernel_neg (z : ℂ) : planarNewtonianKernel (-z) = planarNewtonianKernel z

theorem TauCeti.planarNewtonianKernel_unit_mul {u z : ℂ} (hu : ‖u‖ = 1) : planarNewtonianKernel (u * z) = planarNewtonianKernel z

The planar Newtonian kernel is invariant under multiplication by a unit complex number.

theorem TauCeti.planarNewtonianKernel_mul (z w : ℂ) (hz : z ≠ 0) (hw : w ≠ 0) : planarNewtonianKernel (z * w) = planarNewtonianKernel z + planarNewtonianKernel w

Scaling the argument adds the logarithm of the scale to the planar Newtonian kernel.

theorem TauCeti.planarNewtonianKernel_sub_comm (z a : ℂ) : planarNewtonianKernel (z - a) = planarNewtonianKernel (a - z)

The kernel with pole a is symmetric in its two spatial arguments.

theorem TauCeti.harmonicAt_planarNewtonianKernel_sub {z a : ℂ} (hza : z ≠ a) : InnerProductSpace.HarmonicAt (fun (w : ℂ) => planarNewtonianKernel (w - a)) z

The translated kernel z ↦ G(z - a) is harmonic at every point other than its pole a.

theorem TauCeti.harmonicAt_planarNewtonianKernel {z : ℂ} (hz : z ≠ 0) : InnerProductSpace.HarmonicAt planarNewtonianKernel z

The logarithmic Newtonian kernel is harmonic at every point away from its pole at 0.

theorem TauCeti.harmonicOnNhd_planarNewtonianKernel : InnerProductSpace.HarmonicOnNhd planarNewtonianKernel {0}ᶜ

The planar Newtonian kernel is harmonic on the punctured plane.

theorem TauCeti.harmonicOnNhd_planarNewtonianKernel_sub (a : ℂ) : InnerProductSpace.HarmonicOnNhd (fun (z : ℂ) => planarNewtonianKernel (z - a)) {a}ᶜ

A planar Newtonian kernel with pole a is harmonic on the complement of that pole.

theorem TauCeti.contDiffAt_planarNewtonianKernel_sub {z a : ℂ} (hza : z ≠ a) : ContDiffAt ℝ 2 (fun (w : ℂ) => planarNewtonianKernel (w - a)) z

Away from its pole, a translated planar Newtonian kernel is twice continuously differentiable.

theorem TauCeti.contDiffAt_planarNewtonianKernel {z : ℂ} (hz : z ≠ 0) : ContDiffAt ℝ 2 planarNewtonianKernel z

Away from its pole, the planar Newtonian kernel is twice continuously differentiable.

@[simp]

theorem TauCeti.laplacian_planarNewtonianKernel {z : ℂ} (hz : z ≠ 0) : Laplacian.laplacian planarNewtonianKernel z = 0

The planar Newtonian kernel solves the homogeneous Laplace equation pointwise away from its pole. Its nonzero distributional Laplacian is concentrated at the omitted pole.

@[simp]

theorem TauCeti.laplacian_planarNewtonianKernel_sub {z a : ℂ} (hza : z ≠ a) : Laplacian.laplacian (fun (w : ℂ) => planarNewtonianKernel (w - a)) z = 0

A translated planar Newtonian kernel solves the homogeneous Laplace equation away from its pole.