Commit 2025-04-28 06:28 5d6aefec

View on Github →

feat: behavior of AnalyticAt.order under addition (#22680) Deliver on one of the open TODOs and establish the behavior of AnalyticAt.order under addition. Add missing fun_prop lemma on the stability of analytic functions under HPow.hPow. Generalize the statement on the behavior of AnalyticAt.order under multiplication to scalar multiplication. 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/Analysis/Analytic/Order.lean

added theorem AnalyticAt.analyticAt_centeredMonomial

added theorem AnalyticAt.analyticAt_order_centeredMonomial

added theorem AnalyticAt.order_add

added theorem AnalyticAt.order_add_of_order_lt_order

added theorem AnalyticAt.order_add_of_order_ne_order

added theorem AnalyticAt.order_congr

deleted theorem AnalyticAt.order_mul_of_order_eq_top

added theorem AnalyticAt.order_smul