Commit 2025-07-27 17:59 98480d69

feat: describe posLog in terms of circle averages (#27160) If a is any complex number of norm one, establish by direct computation that the circle average circleAverage (log ‖· - a‖) 0 1 vanishes. As soon as the mean value theorem for harmonic functions becomes available, this result will be extended 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.