Representation of log⁺ as a Circle Average

If a is any complex number of norm one, then log ‖· - a‖ is circle integrable over every circle in the complex plane, and the circle average circleAverage (log ‖· - a‖) 0 1 vanishes.

• Integrability is recalled in circleIntegrability_log_norm_id_sub_const, as a consequence of the general fact that functions of the form log ‖meromorphic‖ are circle integrable.

• The value of the integral is computed in circleAverage_log_norm_id_sub_const₁.

TODO: As soon as the mean value theorem for harmonic functions becomes available, extend this result to arbitrary complex numbers a, showing that the circle average equals the positive part of the logarithm, circleAverage (log ‖· - a‖) 0 1 = = log⁺ ‖a‖. This result, in turn, is a major ingredient in the proof of Jensen's formula in complex analysis.

Circle Integrability

theorem circleIntegrable_log_norm_sub_const {a c : ℂ} (r : ℝ) : CircleIntegrable (fun (x : ℂ) => Real.log ‖x - a‖) c r

If a is any complex number, the function (log ‖· - a‖) is circle integrable over every circle.

Computing circleAverage (log ‖· - a‖) 0 1 in case where ‖a‖ = 1.

@[simp]

theorem circleAverage_log_norm_sub_const₁ {a : ℂ} (h : ‖a‖ = 1) : Real.circleAverage (fun (x : ℂ) => Real.log ‖x - a‖) 0 1 = 0

If a : ℂ has norm one, then the circle average circleAverage (log ‖· - a‖) 0 1 vanishes.