Analytic root sections of delineations

A delineation of a polynomial family with intrinsically analytic coefficients over an analytic submanifold has intrinsically analytic root functions. Multiplicities may be greater than one: constant positive multiplicity, already part of a delineation, suffices. Consequently every ambient section of the stack is an analytic submanifold of the same dimension as the base.

The analyticity statement is expressed using any ambient function agreeing with the root function on the base. This matches AnalyticOnSubmanifold, which depends only on values on the submanifold, and imposes no regularity on the function away from the base.

References

S. McCallum, An improved projection operation for cylindrical algebraic decomposition, Springer (1998), 242–268 (analytic delineability and lifting).

theorem TauCeti.isAnalyticSubmanifold_image_cylinder_sectionSet {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n d k : ℕ} {S : Set (Fin n → 𝕜)} {θ : Fin k → ↑S → 𝕜} (hS : IsAnalyticSubmanifold d S) (i : Fin k) {r : (Fin n → 𝕜) → 𝕜} (hr : ∀ (x : ↑S), r ↑x = θ i x) (ha : AnalyticOnSubmanifold d r S) : IsAnalyticSubmanifold d (cylinder S '' sectionSet θ i)

An ambient section whose defining function is analytic on the base is an analytic submanifold of the same dimension. Only the values of the extension on the base matter.

theorem TauCeti.Delineation.analyticOnSubmanifold_root {n d : ℕ} {S : Set (Fin n → ℝ)} {ι : Type u_1} {P : ι → (Fin n → ℝ) → Polynomial ℝ} (D : Delineation fun (k : ι) (x : ↑S) => P k ↑x) (hS : IsAnalyticSubmanifold d S) (hcoeff : ∀ (k : ι) (j : ℕ), AnalyticOnSubmanifold d (fun (x : Fin n → ℝ) => (P k x).coeff j) S) (i : Fin D.count) {r : (Fin n → ℝ) → ℝ} (hr : ∀ (x : ↑S), r ↑x = D.root i x) : AnalyticOnSubmanifold d r S

The root functions of a delineation with intrinsically analytic coefficients over an analytic submanifold are intrinsically analytic, including roots of multiplicity greater than one. Any ambient extension of a root function gives the same conclusion.

theorem TauCeti.Delineation.isAnalyticSubmanifold_sectionSet {n d : ℕ} {S : Set (Fin n → ℝ)} {ι : Type u_1} {P : ι → (Fin n → ℝ) → Polynomial ℝ} (D : Delineation fun (k : ι) (x : ↑S) => P k ↑x) (hS : IsAnalyticSubmanifold d S) (hcoeff : ∀ (k : ι) (j : ℕ), AnalyticOnSubmanifold d (fun (x : Fin n → ℝ) => (P k x).coeff j) S) (i : Fin D.count) : IsAnalyticSubmanifold d (cylinder S '' sectionSet D.root i)

Every ambient section of a delineation with intrinsically analytic coefficients is an analytic submanifold with the dimension of its base.