Commit 2025-10-07 15:54 1f467e3c

View on Github →

feat: first main theorem of value distribution theory (#30103) Establish the first main theorem of value distribution theory in full. This PR completes a major milestone in Project VD, which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane.

Estimated changes

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

deleted theorem ValueDistribution.abs_characteristic_sub_characteristic_shift_eqO

added theorem ValueDistribution.characteristic_sub_characteristic_inv

added theorem ValueDistribution.characteristic_sub_characteristic_inv_at_zero

added theorem ValueDistribution.characteristic_sub_characteristic_inv_le

added theorem ValueDistribution.characteristic_sub_characteristic_inv_of_ne_zero

added theorem ValueDistribution.isBigO_characteristic_sub_characteristic_inv

added theorem ValueDistribution.isBigO_characteristic_sub_characteristic_shift

Modified docs/overview.yaml