Commit 2025-09-29 05:27 5cde0ddc

feat: representation of log⁺ as a circle average (#29725) If a is any complex number, show that the circle average of log ‖· - a‖ over the unit circle equals the positive part of the logarithm, log⁺ ‖a‖. This material is used in Project VD, which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane. The formula established here is a key ingredient in Jensen's formula of complex analysis.