Identity-principle consequences for zero sets

The nonvanishing locus of a nonzero analytic function is dense in its connected open domain, which gives uniqueness of continuous extensions across its zero set. A product of two scalar analytic functions vanishes near a point only if one factor does. These results support removability and analytic germs without depending on Hartogs extension or local-ring theory.

References: [Scheidemann][Scheidemann2005] (2005), Sections 4.1--4.2; [Korevaar–Wiegerinck][KorevaarWiegerinck2017] (2017), Sections 4.6--4.7. The density and extension-uniqueness results allow normed vector targets.

Main results

subset_closure_nonzero_of_analyticOnNhd is density of the nonvanishing locus. eqOn_of_eqOn_nonzero_of_analyticOnNhd is uniqueness of continuous extensions across a zero set. eventuallyEq_zero_or_eventuallyEq_zero_of_mul is the product rule for vanishing germs.

References

• [J. Korevaar and J. Wiegerinck, Several Complex Variables][KorevaarWiegerinck2017]
• [V. Scheidemann, Introduction to Complex Analysis in Several Variables][Scheidemann2005]

theorem SeveralComplexVariables.exists_ne_zero_mem_ball_of_analyticOnNhd {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] {U : Set E} {f : E → F} (hU : IsOpen U) (hconn : IsPreconnected U) (hf : AnalyticOnNhd ℂ f U) (hne : ∃ z ∈ U, f z ≠ 0) {x : E} (hx : x ∈ U) {r : ℝ} (hr : 0 < r) : ∃ y ∈ U, y ∈ Metric.ball x r ∧ f y ≠ 0

A nonzero analytic function on a connected open set is nonzero arbitrarily near each point of that set. No completeness or finite-dimensionality assumption is needed.

theorem SeveralComplexVariables.subset_closure_nonzero_of_analyticOnNhd {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] {U : Set E} {f : E → F} (hU : IsOpen U) (hconn : IsPreconnected U) (hf : AnalyticOnNhd ℂ f U) (hne : ∃ z ∈ U, f z ≠ 0) : U ⊆ closure {z : E | z ∈ U ∧ f z ≠ 0}

The nonvanishing locus of a nonzero analytic function is dense in its connected open domain. The closure is taken in the ambient normed space.

theorem SeveralComplexVariables.eqOn_of_eqOn_nonzero_of_analyticOnNhd {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] {G : Type u_3} [TopologicalSpace G] [T2Space G] {U : Set E} {f : E → F} {g h : E → G} (hU : IsOpen U) (hconn : IsPreconnected U) (hf : AnalyticOnNhd ℂ f U) (hne : ∃ z ∈ U, f z ≠ 0) (hg : ContinuousOn g U) (hh : ContinuousOn h U) (heq : Set.EqOn g h {z : E | z ∈ U ∧ f z ≠ 0}) : Set.EqOn g h U

Continuous extensions across the zero set of a nonzero analytic function are unique on the domain. Their values outside the domain are unrestricted.

theorem SeveralComplexVariables.eventuallyEq_zero_or_eventuallyEq_zero_of_mul {𝕜 : Type u_3} {E : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f g : E → 𝕜} {x : E} (hf : AnalyticAt 𝕜 f x) (hg : AnalyticAt 𝕜 g x) (hfg : (fun (y : E) => f y * g y) =ᶠ[nhds x] 0) : f =ᶠ[nhds x] 0 ∨ g =ᶠ[nhds x] 0

If a product of two analytic functions vanishes near a point, one factor vanishes near that point. This is the identity principle on a sufficiently small connected ball.