English
The set of points within the domain where the analytic order equals infinity is both open and closed in the domain.
Русский
Множество точек в области определения, где аналитический порядок бесконечен, одновременно открыто и замкнуто внутри области.
LaTeX
$$The set {u ∈ U : analyticOrderAt f u = ∞} is clopen in U.$$
Lean4
/-- The set where an analytic function has infinite order is clopen in its domain of analyticity. -/
theorem isClopen_setOf_analyticOrderAt_eq_top (hf : AnalyticOnNhd 𝕜 f U) : IsClopen {u : U | analyticOrderAt f u = ⊤} :=
by
constructor
· rw [← isOpen_compl_iff, isOpen_iff_forall_mem_open]
intro z hz
rcases (hf z.1 z.2).eventually_eq_zero_or_eventually_ne_zero with h | h
· -- Case: f is locally zero in a punctured neighborhood of z
rw [← analyticOrderAt_eq_top] at h
tauto
· -- Case: f is locally nonzero in a punctured neighborhood of z
obtain ⟨t', h₁t', h₂t', h₃t'⟩ := eventually_nhds_iff.1 (eventually_nhdsWithin_iff.1 h)
use Subtype.val ⁻¹' t'
constructor
· intro w hw
simp only [mem_compl_iff, mem_setOf_eq]
by_cases h₁w : w = z
· rwa [h₁w]
· rw [(hf _ w.2).analyticOrderAt_eq_zero.2 ((h₁t' w hw) (Subtype.coe_ne_coe.mpr h₁w))]
exact ENat.zero_ne_top
· exact ⟨isOpen_induced h₂t', h₃t'⟩
· apply isOpen_iff_forall_mem_open.mpr
intro z hz
conv =>
arg 1; intro; left; right; arg 1; intro
rw [analyticOrderAt_eq_top, eventually_nhds_iff]
simp only [mem_setOf_eq] at hz
rw [analyticOrderAt_eq_top, eventually_nhds_iff] at hz
obtain ⟨t', h₁t', h₂t', h₃t'⟩ := hz
use Subtype.val ⁻¹' t'
simp only [isOpen_induced h₂t', mem_preimage, h₃t', and_self, and_true]
intro w hw
simp only [mem_setOf_eq]
grind
