English
The trailing coefficient of a scalar product is the scalar product of the trailing coefficients.
Русский
Хвостовой коэффициент скалярного произведения равен произведению хвостовых коэффициентов.
LaTeX
$$$$ \mathrm{meromorphicTrailingCoeffAt}(f_1 \cdot f_2, x) = \mathrm{meromorphicTrailingCoeffAt}(f_1,x) \cdot \mathrm{meromorphicTrailingCoeffAt}(f_2,x). $$$$
Lean4
/-- The trailing coefficient of a scalar product is the scalar product of the trailing coefficients.
-/
theorem meromorphicTrailingCoeffAt_smul {f₁ : 𝕜 → 𝕜} {f₂ : 𝕜 → E} (hf₁ : MeromorphicAt f₁ x)
(hf₂ : MeromorphicAt f₂ x) :
meromorphicTrailingCoeffAt (f₁ • f₂) x = (meromorphicTrailingCoeffAt f₁ x) • (meromorphicTrailingCoeffAt f₂ x) :=
by
by_cases h₁f₁ : meromorphicOrderAt f₁ x = ⊤
· simp_all [meromorphicOrderAt_smul hf₁ hf₂]
by_cases h₁f₂ : meromorphicOrderAt f₂ x = ⊤
· simp_all [meromorphicOrderAt_smul hf₁ hf₂]
obtain ⟨g₁, h₁g₁, h₂g₁, h₃g₁⟩ := (meromorphicOrderAt_ne_top_iff hf₁).1 h₁f₁
obtain ⟨g₂, h₁g₂, h₂g₂, h₃g₂⟩ := (meromorphicOrderAt_ne_top_iff hf₂).1 h₁f₂
have : f₁ • f₂ =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ (meromorphicOrderAt (f₁ • f₂) x).untop₀ • (g₁ • g₂) z :=
by
filter_upwards [h₃g₁, h₃g₂, self_mem_nhdsWithin] with y h₁y h₂y h₃y
simp_all [meromorphicOrderAt_smul hf₁ hf₂, zpow_add₀ (sub_ne_zero.2 h₃y)]
module
rw [h₁g₁.meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE h₂g₁ h₃g₁,
h₁g₂.meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE h₂g₂ h₃g₂,
(h₁g₁.smul h₁g₂).meromorphicTrailingCoeffAt_of_eq_nhdsNE this]
simp
