Constant order of vanishing in a distinguished variable

Let G (x, y) be analytic near (x₀, y₀), over ℝ or ℂ, with y a distinguished scalar variable. This file shows that G vanishes to order exactly m in y along y = y₀ for every x near x₀ if and only if G (x, y) = (y - y₀) ^ m • u (x, y) near (x₀, y₀) with u analytic and u (x₀, y₀) ≠ 0 (AnalyticAt.eventually_analyticOrderAt_eq_natCast_iff). This is McCallum–Parusiński–Paunescu, Lemma 4.4. Since u is then nonzero near (x₀, y₀), it writes a function of constant order in a distinguished variable as a centered power (y - y₀) ^ m times a nowhere-vanishing analytic factor, the form of the hypotheses of the Puiseux theorem with parameters (op. cit., §4).

The version with m ≤ the order in place of equality, and no condition on u, is AnalyticAt.eventually_natCast_le_analyticOrderAt_iff. It rests on Hadamard's lemma in a distinguished variable (AnalyticAt.exists_eventuallyEq_sub_smul): a function analytic at (x₀, y₀) that vanishes on y = y₀ near x₀ is (y - y₀) • H near (x₀, y₀) with H analytic.

References

• S. McCallum, A. Parusiński, L. Paunescu, Validity proof of Lazard's method for CAD construction, J. Symbolic Comput. 92 (2019), 52–69, Lemma 4.4.

theorem AnalyticAt.exists_eventuallyEq_sub_smul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {G : E × 𝕜 → F} {x₀ : E} {y₀ : 𝕜} (hG : AnalyticAt 𝕜 G (x₀, y₀)) (h0 : ∀ᶠ (x : E) in nhds x₀, G (x, y₀) = 0) : ∃ (H : E × 𝕜 → F), AnalyticAt 𝕜 H (x₀, y₀) ∧ ∀ᶠ (p : E × 𝕜) in nhds (x₀, y₀), G p = (p.2 - y₀) • H p

Hadamard's lemma in a distinguished variable: a function G analytic at (x₀, y₀) that vanishes on the hyperplane y = y₀ near x₀ is (y - y₀) • H (x, y) near (x₀, y₀), with H analytic at (x₀, y₀).

theorem AnalyticAt.eventually_natCast_le_analyticOrderAt_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {G : E × 𝕜 → F} {x₀ : E} {y₀ : 𝕜} (hG : AnalyticAt 𝕜 G (x₀, y₀)) {m : ℕ} : (∀ᶠ (x : E) in nhds x₀, ↑m ≤ analyticOrderAt (fun (y : 𝕜) => G (x, y)) y₀) ↔ ∃ (u : E × 𝕜 → F), AnalyticAt 𝕜 u (x₀, y₀) ∧ ∀ᶠ (p : E × 𝕜) in nhds (x₀, y₀), G p = (p.2 - y₀) ^ m • u p

Order in a distinguished variable, lower bound: a function G analytic at (x₀, y₀) vanishes to order at least m in y at y₀ along every slice x = const near x₀ if and only if G (x, y) = (y - y₀) ^ m • u (x, y) near (x₀, y₀) for some u analytic at (x₀, y₀).

theorem AnalyticAt.eventually_analyticOrderAt_eq_natCast_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {G : E × 𝕜 → F} {x₀ : E} {y₀ : 𝕜} (hG : AnalyticAt 𝕜 G (x₀, y₀)) {m : ℕ} : (∀ᶠ (x : E) in nhds x₀, analyticOrderAt (fun (y : 𝕜) => G (x, y)) y₀ = ↑m) ↔ ∃ (u : E × 𝕜 → F), AnalyticAt 𝕜 u (x₀, y₀) ∧ u (x₀, y₀) ≠ 0 ∧ ∀ᶠ (p : E × 𝕜) in nhds (x₀, y₀), G p = (p.2 - y₀) ^ m • u p

Order in a distinguished variable (McCallum–Parusiński–Paunescu, Lemma 4.4): a function G analytic at (x₀, y₀) vanishes to order exactly m in y at y₀ along every slice x = const near x₀ if and only if G (x, y) = (y - y₀) ^ m • u (x, y) near (x₀, y₀) for some u analytic at (x₀, y₀) with u (x₀, y₀) ≠ 0.