Harmonicity of the logarithm of the norm in two dimensions

Mathlib's AnalyticAt.harmonicAt_log_norm shows that z ↦ log ‖z‖ is harmonic away from 0 on ℂ. Transporting along a linear isometry onto ℂ, this file shows that x ↦ log ‖x - a‖ is harmonic away from a in every two-dimensional real inner product space, such as EuclideanSpace ℝ (Fin 2).

In the plane, x ↦ log ‖x - a‖ plays the role that the Newtonian kernel plays in higher dimensions. These results supply the harmonicity behind the logarithmic exterior sphere barrier TauCeti.isBarrier_log_norm_sub in TauCeti.Analysis.PDE.Perron.Barrier. That barrier handles the two-dimensional case of Perron's method for the Dirichlet problem on domains satisfying the exterior sphere condition.

Main declarations

• TauCeti.harmonicAt_log_norm_sub_of_finrank_eq_two: harmonicity of x ↦ log ‖x - a‖ away from a in a two-dimensional real inner product space.
• TauCeti.harmonicOnNhd_log_norm_sub_of_finrank_eq_two: the same on the complement of a.

theorem TauCeti.harmonicAt_log_norm_sub_of_finrank_eq_two {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (hE : Module.finrank ℝ E = 2) {x a : E} (hxa : x ≠ a) : InnerProductSpace.HarmonicAt (fun (y : E) => Real.log ‖y - a‖) x

In a two-dimensional real inner product space, x ↦ log ‖x - a‖ is harmonic at every point other than a.

theorem TauCeti.harmonicOnNhd_log_norm_sub_of_finrank_eq_two {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (hE : Module.finrank ℝ E = 2) (a : E) : InnerProductSpace.HarmonicOnNhd (fun (y : E) => Real.log ‖y - a‖) {a}ᶜ

In a two-dimensional real inner product space, x ↦ log ‖x - a‖ is harmonic on the complement of a.