English
The analytic order of a product of analytic functions equals the sum of their orders.
Русский
Порядок аналитического нуля произведения двух аналитических функций равен сумме их порядков.
LaTeX
$$$analyticOrderAt\,(f\cdot g)\, z_0 = analyticOrderAt\, f\, z_0 + analyticOrderAt\, g\, z_0$$$
Lean4
/-- The order is additive when scalar multiplying analytic functions. -/
theorem analyticOrderAt_smul {f : 𝕜 → 𝕜} (hf : AnalyticAt 𝕜 f z₀) (hg : AnalyticAt 𝕜 g z₀) :
analyticOrderAt (f • g) z₀ = analyticOrderAt f z₀ + analyticOrderAt g z₀ := by
-- Trivial cases: one of the functions vanishes around z₀
by_cases hf' : analyticOrderAt f z₀ = ⊤
· simp [analyticOrderAt_smul_eq_top_of_left, *]
by_cases hg' : analyticOrderAt g z₀ = ⊤
·
simp [analyticOrderAt_smul_eq_top_of_right, *]
-- Non-trivial case: both functions do not vanish around z₀
obtain ⟨f', h₁f', h₂f', h₃f'⟩ := hf.analyticOrderAt_ne_top.1 hf'
obtain ⟨g', h₁g', h₂g', h₃g'⟩ := hg.analyticOrderAt_ne_top.1 hg'
rw [← Nat.cast_analyticOrderNatAt hf', ← Nat.cast_analyticOrderNatAt hg', ← ENat.coe_add,
(hf.smul hg).analyticOrderAt_eq_natCast]
refine ⟨f' • g', h₁f'.smul h₁g', ?_, ?_⟩
· simp
tauto
· obtain ⟨t, h₁t, h₂t, h₃t⟩ := eventually_nhds_iff.1 h₃f'
obtain ⟨s, h₁s, h₂s, h₃s⟩ := eventually_nhds_iff.1 h₃g'
exact eventually_nhds_iff.2 ⟨t ∩ s, fun y hy ↦ (by simp [h₁t y hy.1, h₁s y hy.2]; module), h₂t.inter h₂s, h₃t, h₃s⟩
