Conjugation of Laurent unit germs

If two Laurent forms are interchanged by conjugation near a fixed parameter, their integer exponents agree and their unit germs are interchanged as well. The exponents may be negative. Real analyticity of the units suffices; the parameter map need only be continuous at and fix the central parameter.

This comparison makes the Laurent forms of nonmonic polynomial roots compatible with the conjugation action on root labels. It uses Mathlib's uniqueness theorem AnalyticAt.unique_eventuallyEq_zpow_smul_nonzero on a real slice, where conjugation is a real linear map.

References

S. McCallum, A. Parusiński, L. Paunescu, Validity proof of Lazard's method for CAD construction, J. Symbolic Comput. 92 (2019), §4.

theorem AnalyticAt.laurent_eq_of_conj {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {u v : E × ℂ → ℂ} {x₀ : E} {m n : ℤ} {τ : E → E} (hu : AnalyticAt ℝ u (x₀, 0)) (hu0 : u (x₀, 0) ≠ 0) (hv : AnalyticAt ℝ v (x₀, 0)) (hv0 : v (x₀, 0) ≠ 0) (hτ : ContinuousAt τ x₀) (hτ0 : τ x₀ = x₀) (heq : ∀ᶠ (p : E × ℂ) in nhds (x₀, 0), p.2 ≠ 0 → p.2 ^ m * u p = (starRingEnd ℂ) ((starRingEnd ℂ) p.2 ^ n * v (τ p.1, (starRingEnd ℂ) p.2))) : m = n ∧ ∀ᶠ (p : E × ℂ) in nhds (x₀, 0), u p = (starRingEnd ℂ) (v (τ p.1, (starRingEnd ℂ) p.2))

Conjugate Laurent forms at a fixed parameter have the same integer exponent and conjugate unit germs, including on the exceptional hyperplane. No involutivity assumption on the parameter map is needed; continuity at the central parameter suffices.