Commit 2025-03-31 09:17 ca1ee28a

View on Github →

feat: meromorphic functions in normal form on sets (#23337) In analogy to existing code concerning meromorphic functions at are in normal form at a given point, define meromorphic functions that are in normal form on a given set. This material is used in Project VD, which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane.

Estimated changes

Modified Mathlib/Algebra/Order/WithTop/Untop0.lean

added theorem WithTop.untop₀_nonneg

Modified Mathlib/Analysis/Meromorphic/NormalFormAt.lean

added theorem AnalyticOnNhd.meromorphicNFOn

added theorem MeromorphicNFAt.inv

added theorem MeromorphicNFOn.divisor_nonneg_iff_analyticOnNhd

added theorem MeromorphicNFOn.meromorphicOn

added theorem MeromorphicNFOn.zero_set_eq_divisor_support

added def MeromorphicNFOn

added theorem MeromorphicOn.divisor_of_toMeromorphicNFOn

added theorem MeromorphicOn.toMeromorphicNFOn_eq_self_on_nhdNE

added theorem meromorphicNFAt_inv

added theorem meromorphicNFOn_inv

added theorem meromorphicNFOn_mul_iff_left_of_analyticOnNhd

added theorem meromorphicNFOn_mul_iff_right_of_analyticOnNhd

added theorem meromorphicNFOn_smul_iff_right_of_analyticOnNhd

added theorem meromorphicNFOn_toMeromorphicNFOn

added theorem order_toMeromorphicNFOn

added theorem toMeromorphicNFOn_eqOn_codiscrete

added theorem toMeromorphicNFOn_eq_self

added theorem toMeromorphicNFOn_eq_self_on_compl

added theorem toMeromorphicNFOn_eq_toMeromorphicNFAt

added theorem toMeromorphicNFOn_eq_toMeromorphicNFAt_on_nhd

added theorem toMeromorphicNFOn_of_not_meromorphicOn