English
Adding an analytic function on the right does not change the pole divisor.
Русский
Добавление аналитической функции справа не изменяет полю делителя.
LaTeX
$$$ (\text{divisor}(f_1+ f_2)U)^- = (\text{divisor}(f_1)U)^- $ if f_1 meromorphic on U and f_2 analytic near U$$
Lean4
/-- Adding an analytic function to a meromorphic one does not change the pole divisor. -/
theorem negPart_divisor_add_of_analyticNhdOn_right {f₁ f₂ : 𝕜 → E} (hf₁ : MeromorphicOn f₁ U)
(hf₂ : AnalyticOnNhd 𝕜 f₂ U) : (divisor (f₁ + f₂) U)⁻ = (divisor f₁ U)⁻ :=
by
ext x
by_cases hx : x ∈ U
· suffices -(meromorphicOrderAt (f₁ + f₂) x).untop₀ ⊔ 0 = -(meromorphicOrderAt f₁ x).untop₀ ⊔ 0 by
simpa [negPart_def, hx, hf₁, hf₁.add hf₂.meromorphicOn]
by_cases h : 0 ≤ meromorphicOrderAt f₁ x
· suffices 0 ≤ meromorphicOrderAt (f₁ + f₂) x by simp_all
calc
0
_ ≤ min (meromorphicOrderAt f₁ x) (meromorphicOrderAt f₂ x) := (le_inf h (hf₂ x hx).meromorphicOrderAt_nonneg)
_ ≤ meromorphicOrderAt (f₁ + f₂) x := meromorphicOrderAt_add (hf₁ x hx) (hf₂ x hx).meromorphicAt
· suffices meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x by
rwa [meromorphicOrderAt_add_eq_left_of_lt (hf₂.meromorphicOn x hx)]
calc
meromorphicOrderAt f₁ x
_ < 0 := by simpa using h
_ ≤ meromorphicOrderAt f₂ x := (hf₂ x hx).meromorphicOrderAt_nonneg
simp [hx]
