English
For any analytic f, n ≤ analyticOrderAt f z0 iff there exists a local representation with (z - z0)^n times an analytic nonvanishing factor.
Русский
Для аналитической функции f и любого натурального n выполняется: n ≤ analyticOrderAt f z0 тогда существует локальное представление с (z - z0)^n умноженным на аналитический фактор, не обращающийся в нуль в z0.
LaTeX
$$$n \le\ analyticOrderAt f z_0 \iff \exists g,\ AnalyticAt 𝕜 g z_0 \land \forall^ᶠ z \ in\nhds z_0, f z = (z - z_0)^n \cdot g z$$$
Lean4
/-- Characterization of which natural numbers are `≤ hf.order`. Useful for avoiding case splits,
since it applies whether or not the order is `∞`. -/
theorem natCast_le_analyticOrderAt (hf : AnalyticAt 𝕜 f z₀) {n : ℕ} :
n ≤ analyticOrderAt f z₀ ↔ ∃ g, AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ z in 𝓝 z₀, f z = (z - z₀) ^ n • g z :=
by
unfold analyticOrderAt
split_ifs with h
· simpa using ⟨0, analyticAt_const .., by simpa⟩
· let m := (hf.exists_eventuallyEq_pow_smul_nonzero_iff.mpr h).choose
obtain ⟨g, hg, hg_ne, hm⟩ := (hf.exists_eventuallyEq_pow_smul_nonzero_iff.mpr h).choose_spec
rw [ENat.coe_le_coe]
refine ⟨fun hmn ↦ ⟨fun z ↦ (z - z₀) ^ (m - n) • g z, by fun_prop, ?_⟩, fun ⟨h, hh, hfh⟩ ↦ ?_⟩
· filter_upwards [hm] with z hz using by rwa [← mul_smul, ← pow_add, Nat.add_sub_of_le hmn]
· contrapose! hg_ne
have : ContinuousAt (fun z ↦ (z - z₀) ^ (n - m) • h z) z₀ := by fun_prop
rw [tendsto_nhds_unique_of_eventuallyEq (l := 𝓝[≠] z₀) hg.continuousAt.continuousWithinAt this.continuousWithinAt
?_]
· simp [m, Nat.sub_ne_zero_of_lt hg_ne]
· filter_upwards [self_mem_nhdsWithin, hm.filter_mono nhdsWithin_le_nhds, hfh.filter_mono nhdsWithin_le_nhds] with
z hz hf' hf''
rw [← inv_smul_eq_iff₀ (pow_ne_zero _ <| sub_ne_zero_of_ne hz), hf'', smul_comm, ← mul_smul] at hf'
rw [pow_sub₀ _ (sub_ne_zero_of_ne hz) (by cutsat), ← hf']
