English
If meromorphicOrderAt f1 x < meromorphicOrderAt f2 x, then meromorphicOrderAt(f1+f2) x = meromorphicOrderAt f1 x.
Русский
Если meromorphicOrderAt f1 x меньше meromorphicOrderAt f2 x, то meromorphicOrderAt(f1+f2) x = meromorphicOrderAt f1 x.
LaTeX
$$$\\operatorname{meromorphicOrderAt} (f_1 + f_2) x = \\operatorname{meromorphicOrderAt} f_1 x$ при $\\operatorname{meromorphicOrderAt} f_1 x < \\operatorname{meromorphicOrderAt} f_2 x$$$
Lean4
/-- Helper lemma for meromorphicOrderAt_add_of_ne.
-/
theorem meromorphicOrderAt_add_eq_left_of_lt (hf₂ : MeromorphicAt f₂ x)
(h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x) :
meromorphicOrderAt (f₁ + f₂) x = meromorphicOrderAt f₁ x :=
by
by_cases hf₁ : MeromorphicAt f₁ x; swap
· have : ¬(MeromorphicAt (f₁ + f₂) x) := by
contrapose! hf₁
simpa using hf₁.sub hf₂
simp [this, hf₁]
-- Trivial case: f₂ vanishes identically around z₀
by_cases h₁f₂ : meromorphicOrderAt f₂ x = ⊤
· rw [meromorphicOrderAt_congr]
filter_upwards [meromorphicOrderAt_eq_top_iff.1 h₁f₂]
simp
-- General case
lift meromorphicOrderAt f₂ x to ℤ using h₁f₂ with n₂ hn₂
lift meromorphicOrderAt f₁ x to ℤ using h.ne_top with n₁ hn₁
obtain ⟨g₁, h₁g₁, h₂g₁, h₃g₁⟩ := (meromorphicOrderAt_eq_int_iff hf₁).1 hn₁.symm
obtain ⟨g₂, h₁g₂, h₂g₂, h₃g₂⟩ := (meromorphicOrderAt_eq_int_iff hf₂).1 hn₂.symm
rw [meromorphicOrderAt_eq_int_iff (hf₁.add hf₂)]
refine ⟨g₁ + (· - x) ^ (n₂ - n₁) • g₂, ?_, ?_, ?_⟩
· apply h₁g₁.add (AnalyticAt.smul _ h₁g₂)
apply AnalyticAt.zpow_nonneg (by fun_prop) (sub_nonneg.2 (le_of_lt (WithTop.coe_lt_coe.1 h)))
· simpa [zero_zpow _ <| sub_ne_zero.mpr (WithTop.coe_lt_coe.1 h).ne']
· filter_upwards [h₃g₁, h₃g₂, self_mem_nhdsWithin]
simp_all [smul_add, ← smul_assoc, ← zpow_add', sub_ne_zero]
