Gradient of the planar Newtonian kernel

This file computes the full Fréchet derivative of the planar Newtonian kernel away from its pole. The result is the covector

-(2π ‖z‖²)⁻¹ ⟪z, ·⟫,

whose operator norm is (2π ‖z‖)⁻¹. Translated versions give the corresponding formulas for a pole at an arbitrary point. These inverse-distance estimates are the pointwise kernel input for forming and differentiating planar Newtonian potentials.

The calculation uses Mathlib's derivative of the squared norm and the Fréchet chain rule for the real logarithm. It complements FundamentalSolution.Flux, which computes only the derivative in the radial direction needed for the circle flux.

The normalization and inverse-distance gradient formula follow Evans, Partial Differential Equations, Section 2.2.

Main declarations

• TauCeti.hasFDerivAt_planarNewtonianKernel: the full derivative at a nonzero point.
• TauCeti.fderiv_planarNewtonianKernel_apply: its value in an arbitrary direction.
• TauCeti.norm_fderiv_planarNewtonianKernel: its inverse-distance operator norm.
• TauCeti.hasFDerivAt_planarNewtonianKernel_sub: the translated full derivative.
• TauCeti.fderiv_planarNewtonianKernel_sub_apply: the corresponding translated formula.

theorem TauCeti.hasFDerivAt_planarNewtonianKernel {z : ℂ} (hz : z ≠ 0) : HasFDerivAt planarNewtonianKernel ((-(2 * Real.pi)⁻¹ * (‖z‖ ^ 2)⁻¹) • (innerSL ℝ) z) z

Away from the origin, the planar Newtonian kernel has derivative -(2π)⁻¹ ‖z‖⁻² ⟪z, ·⟫.

theorem TauCeti.hasDerivAt_planarNewtonianKernel_affine (b v : ℂ) {t : ℝ} (h : b + t • v ≠ 0) : HasDerivAt (fun (s : ℝ) => planarNewtonianKernel (b + s • v)) (-(2 * Real.pi)⁻¹ * (‖b + t • v‖ ^ 2)⁻¹ * inner ℝ (b + t • v) v) t

The derivative of the planar Newtonian kernel along an affine real curve away from the origin.

theorem TauCeti.fderiv_planarNewtonianKernel {z : ℂ} (hz : z ≠ 0) : fderiv ℝ planarNewtonianKernel z = (-(2 * Real.pi)⁻¹ * (‖z‖ ^ 2)⁻¹) • (innerSL ℝ) z

The Fréchet derivative of the planar Newtonian kernel as a continuous linear functional.

theorem TauCeti.fderiv_planarNewtonianKernel_apply {z : ℂ} (hz : z ≠ 0) (v : ℂ) : (fderiv ℝ planarNewtonianKernel z) v = -(2 * Real.pi)⁻¹ * (‖z‖ ^ 2)⁻¹ * inner ℝ z v

The directional derivative of the planar Newtonian kernel is the radial inner-product covector scaled by -(2π ‖z‖²)⁻¹.

@[simp]

theorem TauCeti.norm_fderiv_planarNewtonianKernel {z : ℂ} (hz : z ≠ 0) : ‖fderiv ℝ planarNewtonianKernel z‖ = (2 * Real.pi * ‖z‖)⁻¹

The derivative of the planar Newtonian kernel has inverse-distance operator norm.

theorem TauCeti.hasFDerivAt_planarNewtonianKernel_sub {z a : ℂ} (hza : z ≠ a) : HasFDerivAt (fun (w : ℂ) => planarNewtonianKernel (w - a)) ((-(2 * Real.pi)⁻¹ * (‖z - a‖ ^ 2)⁻¹) • (innerSL ℝ) (z - a)) z

A planar Newtonian kernel with pole at a has the translated Fréchet derivative.

theorem TauCeti.fderiv_planarNewtonianKernel_sub {z a : ℂ} (hza : z ≠ a) : fderiv ℝ (fun (w : ℂ) => planarNewtonianKernel (w - a)) z = (-(2 * Real.pi)⁻¹ * (‖z - a‖ ^ 2)⁻¹) • (innerSL ℝ) (z - a)

The Fréchet derivative of a planar Newtonian kernel with pole at a.

theorem TauCeti.fderiv_planarNewtonianKernel_sub_apply {z a : ℂ} (hza : z ≠ a) (v : ℂ) : (fderiv ℝ (fun (w : ℂ) => planarNewtonianKernel (w - a)) z) v = -(2 * Real.pi)⁻¹ * (‖z - a‖ ^ 2)⁻¹ * inner ℝ (z - a) v

The directional derivative of a planar Newtonian kernel with pole at a.

@[simp]

theorem TauCeti.norm_fderiv_planarNewtonianKernel_sub {z a : ℂ} (hza : z ≠ a) : ‖fderiv ℝ (fun (w : ℂ) => planarNewtonianKernel (w - a)) z‖ = (2 * Real.pi * ‖z - a‖)⁻¹

The derivative of a planar Newtonian kernel with pole at a has inverse-distance norm.