Complex preparation of constant real polynomial order

Suppose a real polynomial has constant finite ambient order along a real parametrization. For any analytic complexification of that parametrization, there is a real affine direction in which the complex polynomial slices have the same constant order. Evaluation on these slices is therefore a power of the distinguished coordinate times a complex analytic unit. In particular, the real constant-order hypothesis suffices to prepare a discriminant for complex analytic root splitting; constant order on complex points is a conclusion.

References

• S. McCallum, An improved projection operation for cylindrical algebraic decomposition, in Quantifier Elimination and Cylindrical Algebraic Decomposition, Springer (1998), Sections 2–3.
• S. McCallum, A. Parusiński, L. Paunescu, Validity proof of Lazard's method for CAD construction, J. Symbolic Comput. 92 (2019), §4, Lemma 4.4 and Theorem 4.1.
• S. G. Krantz and H. R. Parks, A Primer of Real Analytic Functions, second edition, Birkhäuser (2002), Chapter 2.

theorem MvPolynomial.exists_eventually_analyticOrderAt_complex_eval_add_smul_eq {σ : Type u_1} {ι : Type u_2} [Fintype ι] (p : MvPolynomial σ ℝ) {φ : (ι → ℝ) → σ → ℝ} {Φ : (ι → ℂ) → σ → ℂ} {a : ι → ℝ} {m : ℕ} (hΦ : ∀ (i : σ), AnalyticAt ℂ (fun (z : ι → ℂ) => Φ z i) fun (j : ι) => ↑(a j)) (hreal : ∀ᶠ (x : ι → ℝ) in nhds a, (Φ fun (j : ι) => ↑(x j)) = fun (i : σ) => ↑(φ x i)) (hm : ∀ᶠ (x : ι → ℝ) in nhds a, p.orderAt (φ x) = ↑m) : ∃ (v : σ → ℝ), ∀ᶠ (z : ι → ℂ) in nhds fun (j : ι) => ↑(a j), analyticOrderAt (fun (t : ℂ) => (eval (Φ z + t • fun (i : σ) => ↑(v i))) ((map Complex.ofRealHom) p)) 0 = ↑m

Constant real ambient polynomial order gives constant complex slice order along a real direction, for any analytic complexification of the parametrization.

theorem MvPolynomial.exists_analyticAt_complex_eval_add_smul_eq_pow_mul {σ : Type u_1} {ι : Type u_2} [Fintype ι] (p : MvPolynomial σ ℝ) {φ : (ι → ℝ) → σ → ℝ} {Φ : (ι → ℂ) → σ → ℂ} {a : ι → ℝ} {m : ℕ} (hΦ : ∀ (i : σ), AnalyticAt ℂ (fun (z : ι → ℂ) => Φ z i) fun (j : ι) => ↑(a j)) (hreal : ∀ᶠ (x : ι → ℝ) in nhds a, (Φ fun (j : ι) => ↑(x j)) = fun (i : σ) => ↑(φ x i)) (hm : ∀ᶠ (x : ι → ℝ) in nhds a, p.orderAt (φ x) = ↑m) : ∃ (v : σ → ℝ) (u : (ι → ℂ) × ℂ → ℂ), AnalyticAt ℂ u (fun (j : ι) => ↑(a j), 0) ∧ u (fun (j : ι) => ↑(a j), 0) ≠ 0 ∧ ∀ᶠ (z : (ι → ℂ) × ℂ) in nhds (fun (j : ι) => ↑(a j), 0), (eval (Φ z.1 + z.2 • fun (i : σ) => ↑(v i))) ((map Complex.ofRealHom) p) = z.2 ^ m * u z

For an analytic complexification of a real parametrization of constant finite ambient order, polynomial evaluation along a real direction is a complex power times an analytic unit near the central parameter and line coordinate zero.

theorem MvPolynomial.exists_complexification_eval_add_smul_eq_pow_mul {σ : Type u_1} {ι : Type u_2} [Fintype ι] [Fintype σ] (p : MvPolynomial σ ℝ) {φ : (ι → ℝ) → σ → ℝ} {a : ι → ℝ} {m : ℕ} (hφ : AnalyticAt ℝ φ a) (hm : ∀ᶠ (x : ι → ℝ) in nhds a, p.orderAt (φ x) = ↑m) : ∃ r > 0, ∃ (Φ : (ι → ℂ) → σ → ℂ) (v : σ → ℝ) (u : (ι → ℂ) × ℂ → ℂ), AnalyticOnNhd ℂ Φ (Metric.ball (fun (j : ι) => ↑(a j)) r) ∧ (∀ x ∈ Metric.ball a r, (Φ fun (j : ι) => ↑(x j)) = fun (i : σ) => ↑(φ x i)) ∧ (∀ (z : ι → ℂ), Φ (star z) = star (Φ z)) ∧ AnalyticOnNhd ℂ u (Metric.ball (fun (j : ι) => ↑(a j)) r ×ˢ Metric.ball 0 r) ∧ ∀ z ∈ Metric.ball (fun (j : ι) => ↑(a j)) r ×ˢ Metric.ball 0 r, u z ≠ 0 ∧ (eval (Φ z.1 + z.2 • fun (i : σ) => ↑(v i))) ((map Complex.ofRealHom) p) = z.2 ^ m * u z

A finite-dimensional real analytic parametrization of constant finite polynomial order admits a conjugation-compatible complexification and a real direction on a polydisc where polynomial evaluation is a distinguished-coordinate power times a nowhere-zero analytic unit. Neither complex constant order nor a power-times-unit representation is assumed.