English
If the iterated dslope/fslope map applied to a nonzero p-order yields nonzero value at z0, then the iteration preserves nonvanishing.
Русский
Если применённая к p-order итерация dslope/fslope даёт ненулевое значение, то итерация сохраняет ненулевость.
LaTeX
$$$(swap dslope z0)^{[p.order]} f(z0) \neq 0$ when hp and h ≠ 0$$
Lean4
/-- For a function `f` on `𝕜`, and `z₀ ∈ 𝕜`, there exists at most one `n` such that on a
neighbourhood of `z₀` we have `f z = (z - z₀) ^ n • g z`, with `g` analytic and nonvanishing at
`z₀`. -/
theorem unique_eventuallyEq_pow_smul_nonzero {m n : ℕ}
(hm : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ z in 𝓝 z₀, f z = (z - z₀) ^ m • g z)
(hn : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ z in 𝓝 z₀, f z = (z - z₀) ^ n • g z) : m = n :=
by
simp_rw [← zpow_natCast] at hm hn
exact
Int.ofNat_inj.mp <|
unique_eventuallyEq_zpow_smul_nonzero
(let ⟨g, h₁, h₂, h₃⟩ := hm;
⟨g, h₁, h₂, h₃.filter_mono nhdsWithin_le_nhds⟩)
(let ⟨g, h₁, h₂, h₃⟩ := hn;
⟨g, h₁, h₂, h₃.filter_mono nhdsWithin_le_nhds⟩)
