English
If two analytic functions f and g have distinct finite orders at z0, the order of their sum is the minimum of the two orders.
Русский
Если две аналитические функции f и g имеют различные конечные порядки в z0, порядок их суммы равен минимальному из двух порядков.
LaTeX
$$$analyticOrderAt\, f\, z_0 \neq analyticOrderAt\, g\, z_0 \;\implies\; analyticOrderAt\,(f+g)\, z_0 = \min\big(analyticOrderAt\, f\, z_0,\ analyticOrderAt\, g\, z_0\big)$$$
Lean4
/-- If two functions have unequal orders, then the order of their sum is exactly the minimum
of the orders of the summands. -/
theorem analyticOrderAt_add_of_ne (hfg : analyticOrderAt f z₀ ≠ analyticOrderAt g z₀) :
analyticOrderAt (f + g) z₀ = min (analyticOrderAt f z₀) (analyticOrderAt g z₀) :=
by
obtain hfg | hgf := hfg.lt_or_gt
· simpa [hfg.le] using analyticOrderAt_add_eq_left_of_lt hfg
· simpa [hgf.le] using analyticOrderAt_add_eq_right_of_lt hgf
