English
The divisor of a meromorphic-in-normal-form function is nonnegative iff the function is analytic in a neighborhood.
Русский
Дивизор функции мероморфной в нормальной форме неотрицателен тогда и только тогда, когда функция аналитична в окрестности.
LaTeX
$$$0 \le MeromorphicOn.divisor\ f\ U \iff AnalyticOnNhd\ 𝕜\ f\ U$$$
Lean4
/-- If a function is meromorphic in normal form on `U`, then its divisor is
non-negative iff it is analytic.
-/
theorem divisor_nonneg_iff_analyticOnNhd (h₁f : MeromorphicNFOn f U) :
0 ≤ MeromorphicOn.divisor f U ↔ AnalyticOnNhd 𝕜 f U :=
by
constructor <;> intro h x
· intro hx
rw [← (h₁f hx).meromorphicOrderAt_nonneg_iff_analyticAt]
have := h x
simp only [Function.locallyFinsuppWithin.coe_zero, Pi.zero_apply, h₁f.meromorphicOn, hx,
MeromorphicOn.divisor_apply, untop₀_nonneg] at this
assumption
· by_cases hx : x ∈ U
· simp only [Function.locallyFinsuppWithin.coe_zero, Pi.zero_apply, h₁f.meromorphicOn, hx,
MeromorphicOn.divisor_apply, untop₀_nonneg]
exact (h₁f hx).meromorphicOrderAt_nonneg_iff_analyticAt.2 (h x hx)
· simp [hx]
