Analytic preparation along Lazard monomial curves

A polynomial of constant Lazard valuation along analytic parameterized centers has a power-times-unit form along an evaluator's monomial curve. The unit is jointly analytic in the parameters and the curve variable, including at the curve origin. Its exponent is the evaluator weight of the Lazard valuation.

For a finite family, one evaluator works simultaneously for every polynomial and any prescribed finite set of extra exponents. This gives constant slice orders and analytic units for the discriminant, leading coefficient, and trailing coefficient on the same curve used to deform Lazard evaluations. Centers need only have constant valuations locally; no openness of their image or nonvanishing of ordinary specialization is required.

The construction uses MvPolynomial.exists_aeval_monomialCurve_eq_pow_mul: the remainder and leading Taylor coefficient are polynomial in the center, so their composition with analytic parameters is jointly analytic.

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 Propositions 5.4 and 5.6.

theorem MvPolynomial.exists_analyticAt_eval_add_pow_eq_pow_mul {𝕜 : Type u_1} {E : Type u_2} {σ : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [LinearOrder σ] [WellFoundedGT σ] (p : MvPolynomial σ 𝕜) {φ : E → σ → 𝕜} {x₀ : E} (hφ : ∀ (i : σ), AnalyticAt 𝕜 (fun (x : E) => φ x i) x₀) {V : Set (σ →₀ ℕ)} {v : σ →₀ ℕ} {c : σ → ℕ} (hv : v ∈ V) (hc : TauCeti.IsLazardEvaluator V c) (hval : ∀ᶠ (x : E) in nhds x₀, p.lazardValuation (φ x) = ↑(toLex v)) : ∃ (u : E × 𝕜 → 𝕜), AnalyticAt 𝕜 u (x₀, 0) ∧ u (x₀, 0) ≠ 0 ∧ ∀ᶠ (z : E × 𝕜) in nhds (x₀, 0), (eval fun (i : σ) => φ z.1 i + z.2 ^ c i) p = z.2 ^ (Finsupp.weight c) v * u z

Along analytic parameterized centers with locally constant Lazard valuation, an evaluator's monomial curve gives a power of its parameter times a jointly analytic unit. The power is exactly the evaluator weight of the valuation. Only coordinatewise analyticity of the center map is needed.

theorem TauCeti.exists_isLazardEvaluator_analytic_units {𝕜 : Type u_1} {E : Type u_2} {σ : Type u_3} {ι : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [LinearOrder σ] [WellFoundedGT σ] [Finite ι] (P : ι → MvPolynomial σ 𝕜) {φ : E → σ → 𝕜} {x₀ : E} (hφ : ∀ (j : σ), AnalyticAt 𝕜 (fun (x : E) => φ x j) x₀) (v : ι → σ →₀ ℕ) (hval : ∀ (i : ι), ∀ᶠ (x : E) in nhds x₀, (P i).lazardValuation (φ x) = ↑(toLex (v i))) {V : Set (σ →₀ ℕ)} (hV : V.Finite) : ∃ (c : σ → ℕ), IsLazardEvaluator (Set.range v ∪ V) c ∧ ∃ (u : ι → E × 𝕜 → 𝕜), (∀ (i : ι), AnalyticAt 𝕜 (u i) (x₀, 0)) ∧ (∀ (i : ι), u i (x₀, 0) ≠ 0) ∧ (∀ᶠ (z : E × 𝕜) in nhds (x₀, 0), ∀ (i : ι), u i z ≠ 0 ∧ (MvPolynomial.eval fun (j : σ) => φ z.1 j + z.2 ^ c j) (P i) = z.2 ^ (Finsupp.weight c) (v i) * u i z) ∧ ∀ᶠ (x : E) in nhds x₀, ∀ (i : ι), analyticOrderAt (fun (y : 𝕜) => (MvPolynomial.eval fun (j : σ) => φ x j + y ^ c j) (P i)) 0 = ↑((Finsupp.weight c) (v i))

A finite family of polynomials with locally constant Lazard valuations along analytic centers admits one evaluator and jointly analytic unit forms on a common neighborhood. All slice orders equal the corresponding evaluator weights. The evaluator also separates any prescribed finite set of extra exponents, so the same curve can be used for the removed base exponents of a polynomial being lifted. Empty families and zero valuations are included; finite valuations exclude zero polynomials.