Commit 2025-01-31 20:04 96ae2980

feat: add function log⁺ (=positive part of the logarithm) and prove standard estimates (#21289) Introduce the function log⁺, the positive part of the logarithm, as used in (Complex|Functional|Harmonic) Analysis and Probability Theory. Provide standard estimates for log⁺ of sums and products, as discussed on p.168 of Introduction of Complex Hyperbolic Spaces or p.4 of Nevanlinna Theory in Several Complex Variables and Diophantine Approximation. This material is used in Project VD, which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane.