Orders of factors in analytic families

The order of a slice of a jointly analytic function cannot increase near a parameter where it is finite. Consequently, if a finite product has constant finite slice order, each factor has constant slice order. Over ℝ or ℂ, each factor is therefore a power of the distinguished variable times an analytic unit, locally at the base point.

Applied to the product of squared differences of analytic polynomial roots, this gives the power-times-unit form of each root difference from the corresponding form of the discriminant.

References

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

theorem TauCeti.eventually_analyticOrderAt_curry_right_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [CharZero 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {G : E × 𝕜 → F} {x₀ : E} {y₀ : 𝕜} (hG : AnalyticAt 𝕜 G (x₀, y₀)) {m : ℕ} (hm : analyticOrderAt (fun (y : 𝕜) => G (x₀, y)) y₀ = ↑m) : ∀ᶠ (x : E) in nhds x₀, analyticOrderAt (fun (y : 𝕜) => G (x, y)) y₀ ≤ ↑m

Near a parameter where a jointly analytic function has finite slice order m, its slice orders are at most m.

theorem TauCeti.eventually_analyticOrderAt_factor_eq {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [NontriviallyNormedField 𝕜] [CharZero 𝕜] [CompleteSpace 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Finset ι} {G : ι → E × 𝕜 → 𝕜} {x₀ : E} {y₀ : 𝕜} (hG : ∀ i ∈ s, AnalyticAt 𝕜 (G i) (x₀, y₀)) {m : ℕ} (hm : ∀ᶠ (x : E) in nhds x₀, analyticOrderAt (fun (y : 𝕜) => ∏ i ∈ s, G i (x, y)) y₀ = ↑m) : ∀ᶠ (x : E) in nhds x₀, ∀ i ∈ s, analyticOrderAt (fun (y : 𝕜) => G i (x, y)) y₀ = analyticOrderAt (fun (y : 𝕜) => G i (x₀, y)) y₀

If a finite product of jointly analytic functions has constant finite slice order, then every factor has constant slice order near the parameter.

theorem TauCeti.exists_factor_eq_pow_mul_unit {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Finset ι} {G : ι → E × 𝕜 → 𝕜} {x₀ : E} {y₀ : 𝕜} (hG : ∀ i ∈ s, AnalyticAt 𝕜 (G i) (x₀, y₀)) {m : ℕ} (hm : ∀ᶠ (x : E) in nhds x₀, analyticOrderAt (fun (y : 𝕜) => ∏ i ∈ s, G i (x, y)) y₀ = ↑m) (i : ι) : i ∈ s → ∃ (n : ℕ) (u : E × 𝕜 → 𝕜), AnalyticAt 𝕜 u (x₀, y₀) ∧ u (x₀, y₀) ≠ 0 ∧ ∀ᶠ (p : E × 𝕜) in nhds (x₀, y₀), G i p = (p.2 - y₀) ^ n * u p

Every factor of a jointly analytic product of constant finite slice order is locally a centered power of the distinguished variable times an analytic unit.