Commit 2025-03-11 19:41 39207cc6

View on Github →

feat: add elementary analyticity criteria (#21502) Add criteria for zpowers of analytic functions to remain analytic. Show that "f * g analytic" implies "g analytic" away from zeros of f. This material is used in Project VD, which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane.

Estimated changes

deleted theorem AnalyticAt.add'
deleted theorem AnalyticAt.const_smul'
deleted theorem AnalyticAt.div'
added theorem AnalyticAt.fun_add
added theorem AnalyticAt.fun_div
added theorem AnalyticAt.fun_inv
added theorem AnalyticAt.fun_mul
added theorem AnalyticAt.fun_neg
added theorem AnalyticAt.fun_pow
added theorem AnalyticAt.fun_smul
added theorem AnalyticAt.fun_sub
added theorem AnalyticAt.fun_zpow
deleted theorem AnalyticAt.inv'
deleted theorem AnalyticAt.mul'
deleted theorem AnalyticAt.neg'
deleted theorem AnalyticAt.smul'
deleted theorem AnalyticAt.sub'
added theorem AnalyticAt.zpow
added theorem AnalyticAt.zpow_nonneg
added theorem AnalyticOn.fun_inv
added theorem AnalyticOn.fun_pow
added theorem AnalyticOn.fun_zpow
modified theorem AnalyticOn.inv
added theorem AnalyticOn.zpow
added theorem AnalyticOn.zpow_nonneg
added theorem AnalyticOnNhd.fun_inv
added theorem AnalyticOnNhd.fun_pow
added theorem AnalyticOnNhd.fun_zpow
modified theorem AnalyticOnNhd.inv
added theorem AnalyticOnNhd.zpow
modified theorem AnalyticWithinAt.inv
modified theorem AnalyticWithinAt.pow
added theorem AnalyticWithinAt.zpow