English
If two functions agree near z0, their analytic orders at z0 coincide.
Русский
Если две функции совпадают в окрестности z0, их аналитические порядки совпадают.
LaTeX
$$$\text{analyticOrderAt}_f z_0 = \text{analyticOrderAt}_g z_0$ whenever $f=g$ near z0$$
Lean4
/-- If two functions agree in a neighborhood of `z₀`, then their orders at `z₀` agree. -/
theorem analyticOrderAt_congr (hfg : f =ᶠ[𝓝 z₀] g) : analyticOrderAt f z₀ = analyticOrderAt g z₀ :=
by
by_cases hf : AnalyticAt 𝕜 f z₀
· refine ENat.eq_of_forall_natCast_le_iff fun n ↦ ?_
simp only [natCast_le_analyticOrderAt, hf, hf.congr hfg]
congr! 3
exact hfg.congr_left
· rw [analyticOrderAt_of_not_analyticAt hf, analyticOrderAt_of_not_analyticAt fun hg ↦ hf <| hg.congr hfg.symm]
