Analytic cells of Lazard stacks

Every ambient cell of a Lazard delineation over a real analytic submanifold is again an analytic submanifold: sections retain the dimension of the base, and sectors have one more dimension. Thus the analytic base condition is preserved by successive Lazard liftings, including liftings where ordinary polynomial fibers are nullified.

Main declarations

• TauCeti.LazardDelineation.isAnalyticSubmanifold_sectionSet: every ambient section over an analytic submanifold is analytic of the same dimension.
• TauCeti.LazardDelineation.exists_isAnalyticSubmanifold_of_mem_stackCells: every ambient stack cell over an analytic submanifold is analytic, with the section or sector dimension.

References

S. McCallum, A. Parusiński, L. Paunescu, Validity proof of Lazard's method for CAD construction, Journal of Symbolic Computation 92 (2019), 52–69, Section 5.

theorem TauCeti.LazardDelineation.isAnalyticSubmanifold_sectionSet {ι : Type u_1} {n d : ℕ} {F : ι → MvPolynomial (Fin (n + 1)) ℝ} {S : Set (Fin n → ℝ)} (D : LazardDelineation F S) (hS : IsAnalyticSubmanifold d S) (i : Fin D.count) : IsAnalyticSubmanifold d (cylinder S '' sectionSet D.root i)

Every ambient section of a Lazard delineation over an analytic submanifold is an analytic submanifold of the same dimension, even if ordinary fibers are nullified.

theorem TauCeti.LazardDelineation.exists_isAnalyticSubmanifold_of_mem_stackCells {ι : Type u_1} {n d : ℕ} {F : ι → MvPolynomial (Fin (n + 1)) ℝ} {S : Set (Fin n → ℝ)} (D : LazardDelineation F S) (hS : IsAnalyticSubmanifold d S) {E : Set (Fin (n + 1) → ℝ)} (hE : E ∈ stackCells S D.root) : ∃ (e : ℕ), (e = d ∨ e = d + 1) ∧ IsAnalyticSubmanifold e E

Every ambient cell of a Lazard delineation over a d-dimensional analytic submanifold is analytic, of dimension d for sections and d + 1 for sectors.