Estimates near an isolated zero

A lower bound on a circle around a point at whose centre the function has its only zero, and two ways of concluding that the analytic order at a point is finite.

The first two are the standing hypotheses of every Rouché comparison made on such a disc: both TauCeti.Analysis.Complex.Conformal.LocalDegree and TauCeti.Analysis.Complex.Conformal.Hurwitz set up such a comparison, and each needs the same two facts about the disc before Rouché can be applied. The third has no Rouché content at all: it draws the same finiteness from the global hypothesis a zero count comes with, that the zeros in an open set lie in a finite set, and serves the arbitrary-cycle argument principle (TauCeti.Contour.argumentPrinciple_nullHomologous_of_analyticOnNhd). No result here mentions Rouché's theorem, so this module does not import it:

Main results

• TauCeti.exists_pos_le_norm_of_mem_sphere: on the bounding circle the function is bounded below by a positive constant — this is what a competitor has to beat.
• TauCeti.analyticOrderAt_ne_top_of_forall_ne_zero: the analytic order at the centre is finite, so the count Rouché produces is a natural number rather than ⊤.
• TauCeti.analyticOrderAt_ne_top_of_zeros_subset: the same finiteness under the hypothesis a global zero count comes with, that the zeros in an open set lie in a finite set.

They are separated here only because several files need them.

theorem TauCeti.exists_pos_le_norm_of_mem_sphere {E : Type u_1} {F : Type u_2} [PseudoMetricSpace E] [ProperSpace E] [NormedAddGroup F] {f : E → F} {a : E} {ρ : ℝ} (hcont : ContinuousOn f (Metric.sphere a ρ)) (hne : ∀ z ∈ Metric.sphere a ρ, f z ≠ 0) : ∃ δ > 0, ∀ z ∈ Metric.sphere a ρ, δ ≤ ‖f z‖

A continuous zero-free function on a sphere is bounded below there by a positive constant.

No hypothesis on the radius. At ρ = 0 the sphere is the set of points at zero distance from a — the single point a when E is a metric space, but not in general, since the domain is only assumed pseudometric. For ρ < 0 it is empty, nothing is attained, and the bound holds vacuously.

theorem TauCeti.analyticOrderAt_ne_top_of_forall_ne_zero {f : ℂ → ℂ} {a : ℂ} {ρ : ℝ} (hρ : 0 < ρ) (hzf : ∀ z ∈ Metric.ball a ρ, z ≠ a → f z ≠ 0) : analyticOrderAt f a ≠ ⊤

A function with no zero off the centre does not vanish identically there. If f is nonzero at every point of an open ball of positive radius other than its centre a, then f has finite analytic order at a.

Nothing is assumed about f a, which may or may not be zero, nor about analyticity of f.

theorem TauCeti.analyticOrderAt_ne_top_of_zeros_subset {f : ℂ → ℂ} {U : Set ℂ} {S : Finset ℂ} {z : ℂ} (hU : IsOpen U) (hz : z ∈ U) (hzeros : ∀ w ∈ U, f w = 0 → w ∈ S) : analyticOrderAt f z ≠ ⊤

A function whose zeros are confined to a finite set has finite order. If every zero of f in an open set U lies in a finite set S, then f does not vanish identically near any point of U, so analyticOrderAt f z ≠ ⊤ there.

The point z itself is allowed to be a zero, indeed to lie in S. This is the finite-set form of TauCeti.analyticOrderAt_ne_top_of_forall_ne_zero.