Documentation

TauCeti.Analysis.PDE.FundamentalSolution.Planar.Basic

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 = δ₀ is TauCeti.integral_laplacian_mul_planarNewtonianKernel, in TauCeti.Analysis.PDE.FundamentalSolution.Planar.DistributionalLaplacian.

Harmonicity follows from Mathlib's AnalyticAt.harmonicAt_log_norm: G ∘ f is harmonic wherever f is analytic and nonzero. The remaining results record the smoothness, translation, symmetry, and scaling API used when the kernel is integrated against a source to form a Newtonian potential.

Main declarations #

source
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.

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

    The defining formula for the planar Newtonian kernel.

    source
    @[simp]
    theorem TauCeti.planarNewtonianKernel_zero :
    planarNewtonianKernel 0 = 0
    source
    @[simp]
    theorem TauCeti.planarNewtonianKernel_neg (z : ℂ) :
    planarNewtonianKernel (-z) = planarNewtonianKernel z
    source
    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.

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

    For nonzero factors, the planar Newtonian kernel turns products into sums.

    source
    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.

    source
    theorem AnalyticAt.harmonicAt_planarNewtonianKernel {f : ℂ → ℂ} {z : ℂ} (hf : AnalyticAt ℂ f z) (hfz : f z ≠ 0) :
    InnerProductSpace.HarmonicAt (fun (w : ℂ) => TauCeti.planarNewtonianKernel (f w)) z

    The planar Newtonian kernel composed with an analytic function f is harmonic at every point where f does not vanish.

    source
    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.

    source
    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.

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

    The planar Newtonian kernel is harmonic on the punctured plane.

    source
    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.

    source
    theorem TauCeti.contDiffAt_planarNewtonianKernel_sub {n : WithTop ℕ∞} {z a : ℂ} (hza : z ≠ a) :
    ContDiffAt ℝ n (fun (w : ℂ) => planarNewtonianKernel (w - a)) z

    Away from its pole, a translated planar Newtonian kernel is C^n for every n.

    source
    theorem TauCeti.contDiffAt_planarNewtonianKernel {n : WithTop ℕ∞} {z : ℂ} (hz : z ≠ 0) :
    ContDiffAt ℝ n planarNewtonianKernel z

    Away from its pole, the planar Newtonian kernel is C^n for every n.

    source
    @[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.

    source
    @[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.