Analytic preparation along a fixed direction

If a polynomial has constant finite ambient order along an analytic parametrization, a single affine direction detects that order on every nearby slice. Consequently evaluation along that direction is a power of the line parameter times an analytic unit. This converts ambient polynomial order into the distinguished-variable form used in analytic preparation of discriminants. The direction and unit are constructed; no slice-order hypothesis is needed.

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.

theorem MvPolynomial.analyticAt_coeff_aeval_C_add_C_mul_X {σ : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (p : MvPolynomial σ 𝕜) {φ ψ : E → σ → 𝕜} {x₀ : E} (hφ : ∀ (i : σ), AnalyticAt 𝕜 (fun (x : E) => φ x i) x₀) (hψ : ∀ (i : σ), AnalyticAt 𝕜 (fun (x : E) => ψ x i) x₀) (m : ℕ) : AnalyticAt 𝕜 (fun (x : E) => ((aeval fun (i : σ) => Polynomial.C (φ x i) + Polynomial.C (ψ x i) * Polynomial.X) p).coeff m) x₀

The coefficients of a polynomial restricted to an analytic family of affine lines depend analytically on the base point and direction.

theorem MvPolynomial.exists_eventually_analyticOrderAt_eval_add_smul_eq {σ : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [NontriviallyNormedField 𝕜] [TopologicalSpace E] (p : MvPolynomial σ 𝕜) {φ : E → σ → 𝕜} {x₀ : E} {m : ℕ} (hφ : ContinuousAt φ x₀) (hm : ∀ᶠ (x : E) in nhds x₀, p.orderAt (φ x) = ↑m) : ∃ (v : σ → 𝕜), ∀ᶠ (x : E) in nhds x₀, analyticOrderAt (fun (t : 𝕜) => (eval (φ x + t • v)) p) 0 = ↑m

Along a continuous parametrization of a set of constant finite ambient order, a single direction detects that order analytically on every nearby slice.

theorem MvPolynomial.exists_analyticAt_eval_add_smul_eq_pow_mul {σ : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (p : MvPolynomial σ 𝕜) {φ : E → σ → 𝕜} {x₀ : E} {m : ℕ} (hφ : ∀ (i : σ), AnalyticAt 𝕜 (fun (x : E) => φ x i) x₀) (hm : ∀ᶠ (x : E) in nhds x₀, p.orderAt (φ x) = ↑m) : ∃ (v : σ → 𝕜) (u : E × 𝕜 → 𝕜), AnalyticAt 𝕜 u (x₀, 0) ∧ u (x₀, 0) ≠ 0 ∧ ∀ᶠ (z : E × 𝕜) in nhds (x₀, 0), (eval (φ z.1 + z.2 • v)) p = z.2 ^ m * u z

Constant finite ambient order along an analytic parametrization gives a fixed direction and a local power-times-unit factorization in the line parameter.