Complex preparation of constant real Lazard valuations

A real polynomial with constant finite Lazard valuation along real parameterized centers has the same valuation along any analytic complexification of those centers, near the central real point. The vanishing Taylor coefficients extend by the identity theorem on real points; the leading Taylor coefficient stays nonzero by continuity. Only finitely many coefficient identities are needed, using the support of the Taylor expansion with formal center.

For a finite family and real analytic centers, construct one conjugation-compatible complexification, one evaluator, and complex analytic unit forms on a common polydisc. The evaluator may also separate a prescribed finite set of removed base exponents. Thus the discriminant, leading coefficient, and trailing coefficient can be prepared along the same monomial deformation used for Lazard evaluations, even when they vanish on the real centers. These are the complex unit hypotheses used in parameterized Puiseux splitting; neither complex valuation constancy nor prepared units are assumed.

The preparation reuses TauCeti.exists_isLazardEvaluator_analytic_units and the real-point identity theorem AnalyticAt.eventually_eq_zero_of_eventually_real.

References

• S. McCallum, A. Parusiński, L. Paunescu, Validity proof of Lazard's method for CAD construction, Journal of Symbolic Computation 92 (2019), Sections 4 and 5, Lemma 4.4 and Proposition 5.6.
• S. G. Krantz and H. R. Parks, A Primer of Real Analytic Functions, second edition, Birkhäuser (2002), Chapter 2.

theorem MvPolynomial.eventually_lazardValuation_complexification_eq {σ : Type u_1} {ι : Type u_2} [LinearOrder σ] [WellFoundedGT σ] [Fintype ι] (p : MvPolynomial σ ℝ) {φ : (ι → ℝ) → σ → ℝ} {Φ : (ι → ℂ) → σ → ℂ} {a : ι → ℝ} {v : σ →₀ ℕ} (hΦ : ∀ (i : σ), AnalyticAt ℂ (fun (z : ι → ℂ) => Φ z i) fun (j : ι) => ↑(a j)) (hreal : ∀ᶠ (x : ι → ℝ) in nhds a, (Φ fun (j : ι) => ↑(x j)) = fun (i : σ) => ↑(φ x i)) (hval : ∀ᶠ (x : ι → ℝ) in nhds a, p.lazardValuation (φ x) = ↑(toLex v)) : ∀ᶠ (z : ι → ℂ) in nhds fun (j : ι) => ↑(a j), ((map Complex.ofRealHom) p).lazardValuation (Φ z) = ↑(toLex v)

Constant finite Lazard valuation along real centers extends to any analytic complexification of those centers near the central real point. The variable type may be infinite: the support of the Taylor expansion with formal center is finite.

theorem TauCeti.exists_complexification_isLazardEvaluator_analytic_units {σ : Type u_1} {ι : Type u_2} {κ : Type u_3} [LinearOrder σ] [Fintype σ] [Fintype ι] [Finite κ] (P : κ → MvPolynomial σ ℝ) {φ : (ι → ℝ) → σ → ℝ} {a : ι → ℝ} (hφ : AnalyticAt ℝ φ a) (v : κ → σ →₀ ℕ) (hval : ∀ (i : κ), ∀ᶠ (x : ι → ℝ) in nhds a, (P i).lazardValuation (φ x) = ↑(toLex (v i))) {V : Set (σ →₀ ℕ)} (hV : V.Finite) : ∃ r > 0, ∃ (Φ : (ι → ℂ) → σ → ℂ) (c : σ → ℕ), IsLazardEvaluator (Set.range v ∪ V) c ∧ 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)) ∧ ∃ (u : κ → (ι → ℂ) × ℂ → ℂ), (∀ (i : κ), AnalyticOnNhd ℂ (u i) (Metric.ball (fun (j : ι) => ↑(a j)) r ×ˢ Metric.ball 0 r)) ∧ (∀ z ∈ Metric.ball (fun (j : ι) => ↑(a j)) r ×ˢ Metric.ball 0 r, ∀ (i : κ), u i z ≠ 0 ∧ (MvPolynomial.eval fun (j : σ) => Φ z.1 j + z.2 ^ c j) ((MvPolynomial.map Complex.ofRealHom) (P i)) = z.2 ^ (Finsupp.weight c) (v i) * u i z) ∧ ∀ z ∈ Metric.ball (fun (j : ι) => ↑(a j)) r, ∀ (i : κ), analyticOrderAt (fun (y : ℂ) => (MvPolynomial.eval fun (j : σ) => Φ z j + y ^ c j) ((MvPolynomial.map Complex.ofRealHom) (P i))) 0 = ↑((Finsupp.weight c) (v i))

Real analytic centers with locally constant finite Lazard valuations admit one conjugation-compatible complexification and one evaluator giving complex power-times-unit forms for the entire finite family on a common polydisc. The evaluator also separates any prescribed finite set V, allowing the same curve for the removed base exponents of a polynomial being lifted. The complex slice orders are the evaluator weights.