The zero set of an analytic function

An analytic function that does not vanish identically has isolated zeros, and this file records what that gives on a compact set: only finitely many zeros lie there. It is the fact any zero count rests on, and it mentions neither the analytic order nor any particular field, so it lives apart from both the order calculus of TauCeti.Analysis.Analytic.Order and the complex-specific estimates of TauCeti.Analysis.Complex.IsolatedZero. The name follows Mathlib's own Mathlib.Analysis.Analytic.IsolatedZeros, where the identity principle and the codiscreteness of the zero set live.

Main declarations

• TauCeti.finite_setOf_mem_and_eq_zero_of_isCompact: an analytic function somewhere nonzero on a preconnected set has finitely many zeros in any compact subset of it.

References

• The AINTLIB LeanModularForms valence-formula development (ForMathlib/ValenceFormula/PVChain/ResidueSideInfra.lean), whose modular-form-specific finiteness this generalises.

theorem TauCeti.finite_setOf_mem_and_eq_zero_of_isCompact {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {g : 𝕜 → E} {U K : Set 𝕜} {x : 𝕜} (hg : AnalyticOnNhd 𝕜 g U) (hU : IsPreconnected U) (hx : x ∈ U) (hgx : g x ≠ 0) (hK : IsCompact K) (hKU : K ⊆ U) : {z : 𝕜 | z ∈ K ∧ g z = 0}.Finite

An analytic function somewhere nonzero has finitely many zeros in a compact. If f is analytic on a neighbourhood of a preconnected set U and nonzero at some point of U, then every compact subset of U contains only finitely many zeros of f.

Generalized from the modular-form-specific finiteness of the AINTLIB LeanModularForms valence-formula development (ForMathlib/ValenceFormula/PVChain/ResidueSideInfra.lean) to arbitrary analytic functions on a preconnected set.