Global Laurent unit forms #
An analytic, nowhere-zero function off a coordinate hyperplane that has Laurent unit germs at every point of that hyperplane has a single Laurent exponent and an analytic, nowhere-zero unit on the entire product domain, provided the parameter domain is connected and open. This turns local forms of meromorphic root differences into global forms, allowing both poles and collisions on the hyperplane.
References #
- S. McCallum, A. Parusiński, L. Paunescu, Validity proof of Lazard's method for CAD construction, Journal of Symbolic Computation 92 (2019), §4, Corollary 4.2.
theorem
TauCeti.exists_analyticOnNhd_eq_zpow_mul
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℂ E]
[FiniteDimensional ℂ E]
{f : E × ℂ → ℂ}
{U : Set E}
{s : Set ℂ}
(hU : IsOpen U)
(hUc : IsConnected U)
(hs : IsOpen s)
(h0 : 0 ∈ s)
(hf : AnalyticOnNhd ℂ f (U ×ˢ (s \ {0})))
(hf0 : ∀ p ∈ U ×ˢ (s \ {0}), f p ≠ 0)
(hlocal :
∀ x ∈ U,
∃ (e : ℤ) (w : E × ℂ → ℂ),
AnalyticAt ℂ w (x, 0) ∧ w (x, 0) ≠ 0 ∧ ∀ᶠ (p : E × ℂ) in nhds (x, 0), p.2 ≠ 0 → f p = p.2 ^ e * w p)
:
Local Laurent unit forms of an analytic, nowhere-zero function off a coordinate hyperplane glue to one exponent and one analytic unit on the full product. The unit is nowhere zero, including on the hyperplane. No value of the original function there is used.