English
If f and g are analytic and have finite orders, then the natural-order of their product equals the sum of their natural-orders.
Русский
Если f и g аналитичны и имеют конечные порядки, то натуральный порядок их произведения равен сумме натуральных порядков.
LaTeX
$$$analyticOrderNatAt\,(f\cdot g)\, z_0 = analyticOrderNatAt\, f\, z_0 + analyticOrderNatAt\, g\, z_0$$$
Lean4
/-- The order is additive when multiplying analytic functions. -/
theorem analyticOrderNatAt_mul (hf : AnalyticAt 𝕜 f z₀) (hg : AnalyticAt 𝕜 g z₀) (hf' : analyticOrderAt f z₀ ≠ ⊤)
(hg' : analyticOrderAt g z₀ ≠ ⊤) :
analyticOrderNatAt (f * g) z₀ = analyticOrderNatAt f z₀ + analyticOrderNatAt g z₀ := by
simp [analyticOrderNatAt, analyticOrderAt_mul, ENat.toNat_add, *]
