Commit 2025-03-16 12:35 3a944882

View on Github →

feat: API for continuous extension of meromorphic functions (#22867) Defines the normal form of meromorphic functions and provides API for continuous extension, as discussed on Zulip. More material will be provided in upcoming PRs. 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.lean

Created Mathlib/Analysis/Meromorphic/NormalFormAt.lean

added theorem AnalyticAt.meromorphicNFAt

added theorem MeromorphicAt.eqOn_compl_singleton_toMermomorphicNFAt

added theorem MeromorphicAt.eq_nhdNE_toMeromorphicNFAt

added theorem MeromorphicNFAt.meromorphicAt

added theorem MeromorphicNFAt.order_nonneg_iff_analyticAt

added def MeromorphicNFAt

added theorem meromorphicNFAt_congr

added theorem meromorphicNFAt_iff_analyticAt_or

added theorem meromorphicNFAt_toMeromorphicNFAt

added theorem toMeromorphicNFAt_eq_self

added theorem toMeromorphicNFAt_of_not_meromorphicAt

Modified Mathlib/Topology/ContinuousOn.lean

added theorem eventuallyEq_nhds_of_eventuallyEq_nhdsNE