Sign-invariance on the cells of a stack

Let θ₀ < θ₁ < … < θₖ₋₁ be continuous functions on a preconnected base X, and let f be a continuous function on the cylinder X × ℝ. If every zero of f lies on one of the sections, then f has no zero on any sector, so it is sign-invariant on each sector, because the sectors are preconnected. If moreover the zeros of f are exactly the points of the sections indexed by some I, then f vanishes on the sections indexed by I and has no zero on the others, so it is sign-invariant on each section as well.

For a family P : X → ℝ[X] of polynomials whose evaluation is jointly continuous, this is the step of delineability that turns root data into sign data. Suppose either every P x is zero, or none is and the roots of each P x are exactly the values θ i x for i ∈ I. Then (x, t) ↦ (P x).eval t is sign-invariant on every section and every sector of the stack. Only the location of the roots matters here; their multiplicities do not.

Main declarations

• TauCeti.signInvariant_sectionSet, TauCeti.signInvariant_sectorSet: sign-invariance on the sections and sectors of a continuous function whose zeros lie on sections.
• TauCeti.signInvariant_eval_sectionSet, TauCeti.signInvariant_eval_sectorSet: the same for the evaluation of a polynomial family whose roots are given by the stack.
• TauCeti.exists_forall_eq_zero_or_exists_forall_mem_sectorSet: if whether 0 is a value of the stack does not depend on the base point, then either a section vanishes identically or 0 lies in one fixed sector.

References

S. Basu, R. Pollack, and M.-F. Roy, Algorithms in Real Algebraic Geometry, second edition, Section 5.1.

theorem TauCeti.signInvariant_sectionSet {X : Type u_1} {α : Type u_2} {R : Type u_3} {k : ℕ} [TopologicalSpace X] [PreconnectedSpace X] [Zero R] [LinearOrder R] [TopologicalSpace R] [OrderTopology R] [TopologicalSpace α] {θ : Fin k → X → α} {f : X × α → R} {I : Set (Fin k)} {i : Fin k} (hf : ContinuousOn f (sectionSet θ i)) (hc : Continuous (θ i)) (hθ : ∀ (x : X), Function.Injective fun (i : Fin k) => θ i x) (hzero : ∀ (z : X × α), f z = 0 ↔ ∃ i ∈ I, z ∈ sectionSet θ i) : SignInvariant f (sectionSet θ i)

Over a preconnected base, a function on the cylinder is sign-invariant on the section of a continuous function θ i of a stack whose sections are disjoint, provided its zeros are exactly the points of the sections indexed by some set I. It vanishes on the section if i ∈ I, and is nowhere zero on it otherwise.

theorem TauCeti.signInvariant_sectorSet {X : Type u_1} {R : Type u_3} {k : ℕ} [TopologicalSpace X] [PreconnectedSpace X] [Zero R] [LinearOrder R] [TopologicalSpace R] [OrderTopology R] {θ : Fin k → X → ℝ} {f : X × ℝ → R} {j : Fin (k + 1)} (hf : ContinuousOn f (sectorSet θ j)) (hc : ∀ (i : Fin k), Continuous (θ i)) (hθ : ∀ (x : X), StrictMono fun (i : Fin k) => θ i x) (hzero : ∀ (z : X × ℝ), f z = 0 → ∃ (i : Fin k), z ∈ sectionSet θ i) : SignInvariant f (sectorSet θ j)

Over a preconnected base, a function on the cylinder whose zeros all lie on sections is sign-invariant on each sector of a stack of continuous, pointwise strictly ordered real functions.

theorem TauCeti.signInvariant_eval_sectionSet {X : Type u_1} {k : ℕ} [TopologicalSpace X] [PreconnectedSpace X] {K : Type u_4} [Semiring K] [LinearOrder K] [TopologicalSpace K] [OrderTopology K] {θ : Fin k → X → K} {P : X → Polynomial K} {I : Set (Fin k)} {i : Fin k} (hP : Continuous fun (z : X × K) => Polynomial.eval z.2 (P z.1)) (hc : Continuous (θ i)) (hθ : ∀ (x : X), Function.Injective fun (i : Fin k) => θ i x) (hnull : (∀ (x : X), P x = 0) ∨ ∀ (x : X), P x ≠ 0) (hroots : ∀ (x : X), P x ≠ 0 → ∀ (t : K), Polynomial.eval t (P x) = 0 ↔ ∃ i ∈ I, θ i x = t) : SignInvariant (fun (z : X × K) => Polynomial.eval z.2 (P z.1)) (sectionSet θ i)

Let P be a family of polynomials over a preconnected base, with jointly continuous evaluation, which is either zero everywhere or nowhere zero. If the roots of each nonzero P x are exactly the values θ i x for i ∈ I, where the θ i x are pointwise distinct, then the evaluation of P is sign-invariant on the section of each continuous θ i.

theorem TauCeti.signInvariant_eval_sectorSet {X : Type u_1} {k : ℕ} [TopologicalSpace X] [PreconnectedSpace X] {θ : Fin k → X → ℝ} {P : X → Polynomial ℝ} {j : Fin (k + 1)} (hP : Continuous fun (z : X × ℝ) => Polynomial.eval z.2 (P z.1)) (hc : ∀ (i : Fin k), Continuous (θ i)) (hθ : ∀ (x : X), StrictMono fun (i : Fin k) => θ i x) (hnull : (∀ (x : X), P x = 0) ∨ ∀ (x : X), P x ≠ 0) (hroots : ∀ (x : X), P x ≠ 0 → ∀ (t : ℝ), Polynomial.eval t (P x) = 0 → ∃ (i : Fin k), θ i x = t) : SignInvariant (fun (z : X × ℝ) => Polynomial.eval z.2 (P z.1)) (sectorSet θ j)

Let P be a family of real polynomials over a preconnected base, with jointly continuous evaluation, which is either zero everywhere or nowhere zero. If every root of each nonzero P x is one of the values θ i x of a stack of continuous, pointwise strictly ordered functions, then the evaluation of P is sign-invariant on each sector of the stack.

theorem TauCeti.exists_forall_eq_zero_or_exists_forall_mem_sectorSet {X : Type u_1} {k : ℕ} [TopologicalSpace X] [PreconnectedSpace X] {θ : Fin k → X → ℝ} (hθc : ∀ (i : Fin k), Continuous (θ i)) (hθ : ∀ (x : X), StrictMono fun (i : Fin k) => θ i x) (h : ∀ (x y : X), (∃ (i : Fin k), θ i x = 0) → ∃ (i : Fin k), θ i y = 0) (x₀ : X) : (∃ (i : Fin k), ∀ (x : X), θ i x = 0) ∨ ∃ (j : Fin (k + 1)), ∀ (x : X), (x, 0) ∈ sectorSet θ j

Let θ be a stack of continuous, pointwise strictly ordered real functions over a preconnected base, such that whether 0 is one of the values θ i x does not depend on the base point x. Then either one of the θ i vanishes identically, or 0 lies in one fixed sector over every base point.