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.Planar.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.not_differentiableAt_planarNewtonianKernel_zero : ¬DifferentiableAt ℝ planarNewtonianKernel 0

The planar Newtonian kernel is not differentiable at its pole: it is unbounded there, but takes the value 0 at the origin.

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

The Fréchet derivative of the planar Newtonian kernel as a continuous linear functional. At the pole, where the kernel is not differentiable, both sides are 0.

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

The evaluation of fderiv of the planar Newtonian kernel in the direction v is the radial inner product ⟪z, v⟫ scaled by -(2π ‖z‖²)⁻¹. Away from the pole this is the directional derivative; at the pole, where the kernel is not differentiable, fderiv takes the default value 0 and both sides are 0 (it is not an actual directional derivative).

@[simp]

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

The operator norm of fderiv of the planar Newtonian kernel is the inverse distance (at the pole fderiv is the default 0).

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 : ℂ) : fderiv ℝ (fun (w : ℂ) => planarNewtonianKernel (w - a)) z = (-(2 * Real.pi)⁻¹ * (‖z - a‖ ^ 2)⁻¹) • (innerSL ℝ) (z - a)

The formula for fderiv of a planar Newtonian kernel with pole at a; at the pole it is the default value 0, not an actual derivative.

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

The evaluation of fderiv of a planar Newtonian kernel with pole at a in the direction v. Away from a this is the directional derivative; at the pole fderiv takes the default value 0 and both sides are 0 (it is not an actual directional derivative).

@[simp]

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

The operator norm of fderiv of a planar Newtonian kernel with pole at a is the inverse distance (at the pole fderiv is the default 0).