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₀), the factorization holds on a product of balls ball x₀ r ×ˢ ball y₀ r, a polydisc when E is ι → 𝕜, on which u is analytic and nowhere zero (AnalyticAt.exists_ball_prod_eq_pow_smul and AnalyticAt.eventually_analyticOrderAt_eq_natCast_iff_exists_ball). This 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. Applied in both variables, it shows that a function of two variables vanishing on two crossing lines is divisible by the product of their equations (AnalyticAt.exists_eventuallyEq_mul_smul). After straightening, the same holds along the graph y = g x of an analytic function: a function vanishing there is (y - g x) • H (AnalyticAt.exists_eventuallyEq_sub_smul_of_graph). In particular a function of (b, x, y) vanishing on the hypersurface xy = S(b) away from x = y = 0 is a multiple of xy - S(b) (AnalyticAt.exists_eventuallyEq_mul_sub_smul_of_fst_ne_zero and AnalyticAt.exists_eventuallyEq_mul_sub_smul_of_snd_ne_zero).

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_ball_prod_eq_pow_smul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {G u : E × 𝕜 → F} {x₀ : E} {y₀ : 𝕜} {m : ℕ} (hu : AnalyticAt 𝕜 u (x₀, y₀)) (hu0 : u (x₀, y₀) ≠ 0) (hGu : ∀ᶠ (p : E × 𝕜) in nhds (x₀, y₀), G p = (p.2 - y₀) ^ m • u p) : ∃ r > 0, AnalyticOnNhd 𝕜 u (Metric.ball x₀ r ×ˢ Metric.ball y₀ r) ∧ ∀ p ∈ Metric.ball x₀ r ×ˢ Metric.ball y₀ r, u p ≠ 0 ∧ G p = (p.2 - y₀) ^ m • u p

Shrinking to a nowhere-vanishing unit. A local factorization G (x, y) = (y - y₀) ^ m • u (x, y) with u analytic at (x₀, y₀) and u (x₀, y₀) ≠ 0 holds on a product of balls ball x₀ r ×ˢ ball y₀ r on which u is analytic and nowhere zero. When E is ι → 𝕜 with its sup norm, this product is a polydisc.

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.exists_eventuallyEq_sub_smul_of_graph {𝕜 : 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} {g : E → 𝕜} {x₀ : E} (hG : AnalyticAt 𝕜 G (x₀, g x₀)) (hg : AnalyticAt 𝕜 g x₀) (h0 : ∀ᶠ (x : E) in nhds x₀, G (x, g x) = 0) : ∃ (H : E × 𝕜 → F), AnalyticAt 𝕜 H (x₀, g x₀) ∧ ∀ᶠ (p : E × 𝕜) in nhds (x₀, g x₀), G p = (p.2 - g p.1) • H p

Hadamard's lemma along a graph: a function G analytic at (x₀, g x₀) that vanishes on the graph y = g x of a function g analytic at x₀ is (y - g x) • H (x, y) near (x₀, g x₀), with H analytic at (x₀, g x₀).

theorem AnalyticAt.exists_eventuallyEq_mul_smul {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {G : 𝕜 × 𝕜 → F} {a b : 𝕜} (hG : AnalyticAt 𝕜 G (a, b)) (h₁ : ∀ᶠ (x : 𝕜) in nhds a, G (x, b) = 0) (h₂ : ∀ᶠ (y : 𝕜) in nhds b, G (a, y) = 0) : ∃ (K : 𝕜 × 𝕜 → F), AnalyticAt 𝕜 K (a, b) ∧ ∀ᶠ (p : 𝕜 × 𝕜) in nhds (a, b), G p = ((p.1 - a) * (p.2 - b)) • K p

Functions vanishing on two crossing lines. A function of two scalar variables which is analytic at (a, b) and vanishes near (a, b) on the lines y = b and x = a is (x - a) (y - b) times a function analytic at (a, b).

theorem AnalyticAt.exists_eventuallyEq_mul_sub_smul_of_fst_ne_zero {𝕜 : 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} {S : E → 𝕜} {p : E × 𝕜 × 𝕜} (hG : AnalyticAt 𝕜 G p) (hS : AnalyticAt 𝕜 S p.1) (hx : p.2.1 ≠ 0) (hp : S p.1 = p.2.1 * p.2.2) (h0 : ∀ᶠ (w : E × 𝕜) in nhds (p.1, p.2.1), G (w.1, w.2, S w.1 / w.2) = 0) : ∃ (K : E × 𝕜 × 𝕜 → F), AnalyticAt 𝕜 K p ∧ ∀ᶠ (q : E × 𝕜 × 𝕜) in nhds p, G q = (q.2.1 * q.2.2 - S q.1) • K q

Functions vanishing on xy = S(b) where x ≠ 0. A function G (b, x, y) analytic at a point p of the hypersurface xy = S(b) with x ≠ 0, for S analytic at the base point of p, that vanishes near p on the hypersurface (written as the graph y = S(b)/x), is (xy - S(b)) • K near p with K analytic at p.

theorem AnalyticAt.exists_eventuallyEq_mul_sub_smul_of_snd_ne_zero {𝕜 : 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} {S : E → 𝕜} {p : E × 𝕜 × 𝕜} (hG : AnalyticAt 𝕜 G p) (hS : AnalyticAt 𝕜 S p.1) (hy : p.2.2 ≠ 0) (hp : S p.1 = p.2.1 * p.2.2) (h0 : ∀ᶠ (w : E × 𝕜) in nhds (p.1, p.2.2), G (w.1, S w.1 / w.2, w.2) = 0) : ∃ (K : E × 𝕜 × 𝕜 → F), AnalyticAt 𝕜 K p ∧ ∀ᶠ (q : E × 𝕜 × 𝕜) in nhds p, G q = (q.2.1 * q.2.2 - S q.1) • K q

Functions vanishing on xy = S(b) where y ≠ 0. A function G (b, x, y) analytic at a point p of the hypersurface xy = S(b) with y ≠ 0, for S analytic at the base point of p, that vanishes near p on the hypersurface (written as the graph x = S(b)/y), is (xy - S(b)) • K near p with K analytic at p.

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.

theorem AnalyticAt.eventually_analyticOrderAt_eq_natCast_iff_exists_ball {𝕜 : 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) ↔ ∃ r > 0, ∃ (u : E × 𝕜 → F), AnalyticOnNhd 𝕜 u (Metric.ball x₀ r ×ˢ Metric.ball y₀ r) ∧ ∀ p ∈ Metric.ball x₀ r ×ˢ Metric.ball y₀ r, u p ≠ 0 ∧ G p = (p.2 - y₀) ^ m • u p

Order in a distinguished variable on a product of balls. 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, on some product of balls around (x₀, y₀), G (x, y) = (y - y₀) ^ m • u (x, y) with u analytic and nowhere zero there. When E is ι → 𝕜 with its sup norm, this product is a polydisc.