Commit 2025-06-18 09:36 30428f6a

feat: integrability of log ‖meromorphic‖ (#24845) For real-meromorphic functions f, establish interval integrability of log ‖f ·‖. In particular, show that log ∘ sin is interval integrable. For complex-meromorphic functions f, establish circle integrability of log ‖f ·‖. At the suggestion of @sgouezel, split the file Mathlib/Analysis/SpecialFunctions/Integrals.lean. The file establishes values of special interval integrals. As a prerequisite, it establishes interval integrability of numerous functions. Interval integrability of log ‖f ·‖, which is established in the current PR, naturally fits in there. Adding the material to Mathlib/Analysis/SpecialFunctions/Integrals.lean did however not seem advisable:

• The line of argumentation is different from what is used already, leading to massive new imports and cross-dependencies.
• The current file mixes two lines of results of independent interest that have only a clear one-way dependency (integral computation uses integrability)
• The file was very long already. As a clean solution, move the material on integrability to a new directory, Mathlib/Analysis/SpecialFunctions/Integrability, which contains a file with the original material and another one with the new material. That way, the results on integrability are all in one place and cross-imports are avoided. This material is used in Project VD, which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane. Integrability of log ∘ sin might be useful in future discussions of polylogarithms.