Laurent exponents in connected families

Suppose a function on a product has, near every point of a distinguished hyperplane, a Laurent-power expression in the transverse variable with an analytic nonvanishing unit. For a fixed global function the integer exponent is locally constant along the hyperplane: two such expressions at nearby points overlap, and uniqueness of the order of an analytic germ identifies their exponents. Consequently the exponent is constant on a preconnected set of parameters.

The pointwise uniqueness statement laurentExponent_eq is also exported, so that exponents obtained from independent constructions can be compared.

The globalization result is stated simultaneously for an arbitrary family of functions. It is used for global root labels in parameterized Puiseux factorizations: the labels having finite limits are precisely those with nonnegative exponent, so their set cannot change over a connected base.

References

• S. McCallum, A. Parusiński, L. Paunescu, Validity proof of Lazard's method for CAD construction, Journal of Symbolic Computation 92 (2019), 52–69, §5.2.

theorem TauCeti.laurentExponent_eq {E : Type u_2} {𝕜 : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {r u v : E × 𝕜 → 𝕜} {x : E} {m n : ℤ} (hu : AnalyticAt 𝕜 u (x, 0)) (hu0 : u (x, 0) ≠ 0) (hv : AnalyticAt 𝕜 v (x, 0)) (hv0 : v (x, 0) ≠ 0) (hm : ∀ᶠ (b : E × 𝕜) in nhds (x, 0), b.2 ≠ 0 → r b = b.2 ^ m * u b) (hn : ∀ᶠ (b : E × 𝕜) in nhds (x, 0), b.2 ≠ 0 → r b = b.2 ^ n * v b) : m = n

Uniqueness of the Laurent exponent at a point of the hyperplane. If, near (x, 0), the function r is both b.2 ^ m * u b and b.2 ^ n * v b off the hyperplane b.2 = 0, with u and v analytic and nonvanishing at (x, 0), then m = n. No connectedness is needed: the two expressions are compared on the transverse line through (x, 0).

theorem TauCeti.exists_laurentExponents_of_isPreconnected {I : Type u_1} {E : Type u_2} {𝕜 : Type u_3} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {S : Set E} (hSne : S.Nonempty) (hS : IsPreconnected S) (r : I → E × 𝕜 → 𝕜) {P : I → ℤ → Prop} (h : ∀ (i : I), ∀ x ∈ S, ∃ (e : ℤ), P i e ∧ ∃ (w : E × 𝕜 → 𝕜), AnalyticAt 𝕜 w (x, 0) ∧ w (x, 0) ≠ 0 ∧ ∀ᶠ (b : E × 𝕜) in nhds (x, 0), b.2 ≠ 0 → r i b = b.2 ^ e * w b) : ∃ (e : I → ℤ), (∀ (i : I), P i (e i)) ∧ ∀ (i : I), ∀ x ∈ S, ∃ (w : E × 𝕜 → 𝕜), AnalyticAt 𝕜 w (x, 0) ∧ w (x, 0) ≠ 0 ∧ ∀ᶠ (b : E × 𝕜) in nhds (x, 0), b.2 ≠ 0 → r i b = b.2 ^ e i * w b

Laurent exponents are constant in preconnected families. Suppose that, near every (x, 0) with x ∈ S, every function r i is a power of the transverse coordinate times an analytic unit. Then one exponent can be chosen for each global label i, independently of x. The analytic unit may still depend on the point.

No finiteness assumption on the label type is needed. Any pointwise property P i e of the exponents, such as a common lower bound, is retained. Negative exponents and an empty label type are allowed.