English
The analytic order of a sum is at least the minimum of the orders of the summands.
Русский
Порядок аналитичности суммы не меньше минимума порядков слагаемых.
LaTeX
$$$\min(\operatorname{analyticOrderAt} f z_0, \operatorname{analyticOrderAt} g z_0) \le \operatorname{analyticOrderAt} (f+g) z_0$$$
Lean4
/-- The order of a sum is at least the minimum of the orders of the summands. -/
theorem le_analyticOrderAt_add : min (analyticOrderAt f z₀) (analyticOrderAt g z₀) ≤ analyticOrderAt (f + g) z₀ :=
by
by_cases hf : AnalyticAt 𝕜 f z₀
· by_cases hg : AnalyticAt 𝕜 g z₀
· refine ENat.forall_natCast_le_iff_le.mp fun n ↦ ?_
simp only [le_min_iff, natCast_le_analyticOrderAt, hf, hg, hf.add hg]
refine fun ⟨⟨F, hF, hF'⟩, ⟨G, hG, hG'⟩⟩ ↦ ⟨F + G, hF.add hG, ?_⟩
filter_upwards [hF', hG'] with z using by simp +contextual
· simp [*]
· simp [*]
