English
Let f and g be analytic at z0. If the analytic order of f at z0 is strictly less than the analytic order of g at z0, then the analytic order of f+g at z0 equals the order of f.
Русский
Пусть f и g аналитичны в окрестности z0. Если аналитический порядок f в z0 строго меньше порядка g в z0, то порядок f+g в z0 равен порядку f в z0.
LaTeX
$$$analyticOrderAt\, f\, z_0 < analyticOrderAt\, g\, z_0 \;\implies\; analyticOrderAt\,(f+g)\, z_0 = analyticOrderAt\, f\, z_0$$$
Lean4
theorem analyticOrderAt_add_eq_left_of_lt (hfg : analyticOrderAt f z₀ < analyticOrderAt g z₀) :
analyticOrderAt (f + g) z₀ = analyticOrderAt f z₀ :=
le_antisymm (by simpa [hfg.not_ge] using le_analyticOrderAt_sub (f := f + g) (g := g) (z₀ := z₀))
(by simpa [hfg.le] using le_analyticOrderAt_add (f := f) (g := g) (z₀ := z₀))
