Commit 2025-11-24 08:57 d3a92048

View on Github →

feat: behavior of the proximity function under addition (#31556) Establish the behavior of the "Proximity Function" of Value Distribution theory with respect to addition. 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 part of a larger package discussing the behavior of the Nenvanlinna height under algebraic manipulations of the functions.

Estimated changes

Modified Mathlib/Analysis/Complex/ValueDistribution/ProximityFunction.lean

added theorem ValueDistribution.proximity_add_top_le

added theorem ValueDistribution.proximity_sum_top_le

Modified Mathlib/MeasureTheory/Integral/CircleAverage.lean

modified theorem Real.circleAverage_fun_add

added theorem Real.circleAverage_fun_sub

added theorem Real.circleAverage_fun_sum

added theorem Real.circleAverage_map_add_const

Modified Mathlib/MeasureTheory/Integral/CircleIntegral.lean

added theorem CircleIntegrable.fun_sum