Flux of the planar Newtonian kernel

This file computes the outward normal derivative of the planar Newtonian kernel on a circle. The resulting flux is -1, as required for the fundamental solution of the negative Laplacian. This calculation fixes the normalization of planarNewtonianKernel and is the boundary calculation needed for its later distributional identity -Δ G = δ₀.

Main declarations

• TauCeti.fderiv_planarNewtonianKernel_self: the radial derivative of the kernel.
• TauCeti.fderiv_planarNewtonianKernel_sub_circle_normal: its outward normal derivative on a circle centered at the pole.
• TauCeti.integral_fderiv_planarNewtonianKernel_sub_circle_normal: the total circle flux is -1.

@[simp]

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

The derivative of the planar Newtonian kernel in the radial direction is -(2π)⁻¹.

@[simp]

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

The derivative of a translated planar Newtonian kernel in the radial direction from its pole is -(2π)⁻¹.

@[simp]

theorem TauCeti.fderiv_planarNewtonianKernel_sub_circle_normal {a : ℂ} {r θ : ℝ} (hr : 0 < r) : (fderiv ℝ (fun (w : ℂ) => planarNewtonianKernel (w - a)) (circleMap a r θ)) ((↑r)⁻¹ * circleMap 0 r θ) = -(2 * Real.pi * r)⁻¹

On the circle of radius r, the outward normal derivative of the planar Newtonian kernel is -(2πr)⁻¹.

@[simp]

theorem TauCeti.fderiv_planarNewtonianKernel_circle_normal {r θ : ℝ} (hr : 0 < r) : (fderiv ℝ planarNewtonianKernel (circleMap 0 r θ)) ((↑r)⁻¹ * circleMap 0 r θ) = -(2 * Real.pi * r)⁻¹

On the circle of radius r centered at the origin, the outward normal derivative of the planar Newtonian kernel is -(2πr)⁻¹.

theorem TauCeti.radius_mul_fderiv_planarNewtonianKernel_sub_circle_normal {a : ℂ} {r θ : ℝ} (hr : 0 < r) : r * (fderiv ℝ (fun (w : ℂ) => planarNewtonianKernel (w - a)) (circleMap a r θ)) ((↑r)⁻¹ * circleMap 0 r θ) = -(2 * Real.pi)⁻¹

The arclength-weighted normal derivative of the planar Newtonian kernel is constant on every positively oriented circle around its pole.

theorem TauCeti.radius_mul_fderiv_planarNewtonianKernel_circle_normal {r θ : ℝ} (hr : 0 < r) : r * (fderiv ℝ planarNewtonianKernel (circleMap 0 r θ)) ((↑r)⁻¹ * circleMap 0 r θ) = -(2 * Real.pi)⁻¹

The arclength-weighted normal derivative of the planar Newtonian kernel is constant on every positively oriented circle centered at the origin.

theorem TauCeti.integral_fderiv_planarNewtonianKernel_sub_circle_normal {a : ℂ} {r : ℝ} (hr : 0 < r) : r * ∫ (θ : ℝ) in 0..2 * Real.pi, (fderiv ℝ (fun (w : ℂ) => planarNewtonianKernel (w - a)) (circleMap a r θ)) ((↑r)⁻¹ * circleMap 0 r θ) = -1

The outward flux of the planar Newtonian kernel through any circle centered at its pole is -1. The factor r is the arclength Jacobian in the angular parametrization.

theorem TauCeti.integral_fderiv_planarNewtonianKernel_circle_normal {r : ℝ} (hr : 0 < r) : r * ∫ (θ : ℝ) in 0..2 * Real.pi, (fderiv ℝ planarNewtonianKernel (circleMap 0 r θ)) ((↑r)⁻¹ * circleMap 0 r θ) = -1

The outward flux of the planar Newtonian kernel through any circle centered at the origin is -1. The factor r is the arclength Jacobian in the angular parametrization.