English
The order is additive under scalar-valued meromorphic multiplication: meromorphicOrderAt(f · g) = meromorphicOrderAt f + meromorphicOrderAt g.
Русский
Порядок сохраняет аддитивность при произведении скалярной и векторной мероморфных функций: meromorphicOrderAt(f · g) = meromorphicOrderAt f + meromorphicOrderAt g.
LaTeX
$$$\\operatorname{meromorphicOrderAt} (f \\cdot g) x = \\operatorname{meromorphicOrderAt} f x + \\operatorname{meromorphicOrderAt} g x$$$
Lean4
/-- The order is additive when multiplying scalar-valued and vector-valued meromorphic functions. -/
theorem meromorphicOrderAt_smul {f : 𝕜 → 𝕜} {g : 𝕜 → E} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) :
meromorphicOrderAt (f • g) x = meromorphicOrderAt f x + meromorphicOrderAt g x := by
-- Trivial cases: one of the functions vanishes around z₀
cases h₂f : meromorphicOrderAt f x with
| top =>
simp only [top_add, meromorphicOrderAt_eq_top_iff] at h₂f ⊢
filter_upwards [h₂f] with z hz using by simp [hz]
| coe m =>
cases h₂g : meromorphicOrderAt g x with
| top =>
simp only [add_top, meromorphicOrderAt_eq_top_iff] at h₂g ⊢
filter_upwards [h₂g] with z hz using by simp [hz]
| coe n => -- Non-trivial case: both functions do not vanish around z₀
rw [← WithTop.coe_add, meromorphicOrderAt_eq_int_iff (hf.smul hg)]
obtain ⟨F, h₁F, h₂F, h₃F⟩ := (meromorphicOrderAt_eq_int_iff hf).1 h₂f
obtain ⟨G, h₁G, h₂G, h₃G⟩ := (meromorphicOrderAt_eq_int_iff hg).1 h₂g
use F • G, h₁F.smul h₁G, by simp [h₂F, h₂G]
filter_upwards [self_mem_nhdsWithin, h₃F, h₃G] with a ha hfa hga
simp [hfa, hga, smul_comm (F a), zpow_add₀ (sub_ne_zero.mpr ha), mul_smul]
