Sign-invariant functions

A function f is sign-invariant on a set s when it has the same sign at any two points of s, where the sign SignType.sign takes the values -1, 0 and 1. In particular a function that vanishes somewhere on s is sign-invariant on s only if it vanishes on all of s. This is the invariance asked of the cells of a cylindrical algebraic decomposition adapted to a family of polynomials: each polynomial of the family is sign-invariant on each cell.

The basic source of sign-invariance is connectedness: a function that is continuous and nowhere zero on a preconnected set is sign-invariant there, since its sign is a continuous map to the discrete space SignType.

Sign-invariance is preserved by restriction, by precomposition, and by the operations whose result has a sign determined by the signs of the inputs: negation, products and powers.

A set on which each function of a family is sign-invariant lies inside or outside each set described by a condition on their signs. If the sets of a cover each have this property, one sample point from each of them realizes every sign vector that the functions take.

Main declarations

• TauCeti.SignInvariant: sign-invariance of a function on a set.
• TauCeti.signInvariant_iff_exists: a sign-invariant function has a single sign on the set.
• TauCeti.signInvariant_image: sign-invariance on an image is sign-invariance of the composite.
• TauCeti.SignInvariant.comp, TauCeti.SignInvariant.union: precomposition with a map into the set, and unions of two sets that meet.
• TauCeti.SignInvariant.neg, TauCeti.SignInvariant.mul, TauCeti.SignInvariant.pow, TauCeti.signInvariant_finsetProd: negations, products, powers and finite products of sign-invariant functions are sign-invariant.
• TauCeti.subset_or_disjoint_setOf_sign: a set on which the functions are sign-invariant lies inside or outside each sign-condition set.
• TauCeti.range_sign_sample_eq: sample points of a cover by sets on which the functions are sign-invariant realize all their sign vectors.
• IsPreconnected.signInvariant: a continuous, nowhere-zero function on a preconnected set is sign-invariant.
• IsPreconnected.signInvariant_of_eq_zero_iff: a continuous function on a preconnected set that vanishes everywhere or nowhere there is sign-invariant.

References

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

def TauCeti.SignInvariant {α : Type u_1} {R : Type u_3} [Zero R] [Preorder R] [DecidableLT R] (f : α → R) (s : Set α) : Prop

A function f is sign-invariant on s if it has the same sign, possibly zero, at any two points of s.

theorem TauCeti.signInvariant_def {α : Type u_1} {R : Type u_3} [Zero R] [Preorder R] [DecidableLT R] {f : α → R} {s : Set α} : SignInvariant f s ↔ ∀ x ∈ s, ∀ y ∈ s, SignType.sign (f x) = SignType.sign (f y)

theorem TauCeti.signInvariant_iff_exists {α : Type u_1} {R : Type u_3} [Zero R] [Preorder R] [DecidableLT R] {f : α → R} {s : Set α} : SignInvariant f s ↔ ∃ (σ : SignType), ∀ x ∈ s, SignType.sign (f x) = σ

A function is sign-invariant on s exactly when a single sign is taken at every point of s.

theorem TauCeti.SignInvariant.mono {α : Type u_1} {R : Type u_3} [Zero R] [Preorder R] [DecidableLT R] {f : α → R} {s t : Set α} (h : SignInvariant f t) (hst : s ⊆ t) : SignInvariant f s

theorem TauCeti.SignInvariant.congr {α : Type u_1} {R : Type u_3} [Zero R] [Preorder R] [DecidableLT R] {f g : α → R} {s : Set α} (h : SignInvariant f s) (hfg : Set.EqOn f g s) : SignInvariant g s

theorem TauCeti.signInvariant_image {α : Type u_1} {β : Type u_2} {R : Type u_3} [Zero R] [Preorder R] [DecidableLT R] {f : α → R} {u : β → α} {s : Set β} : SignInvariant f (u '' s) ↔ SignInvariant (f ∘ u) s

Sign-invariance on an image is sign-invariance of the composite on the source set.

theorem TauCeti.SignInvariant.comp {α : Type u_1} {β : Type u_2} {R : Type u_3} [Zero R] [Preorder R] [DecidableLT R] {f : α → R} {t : Set α} (h : SignInvariant f t) {u : β → α} {s : Set β} (hu : Set.MapsTo u s t) : SignInvariant (f ∘ u) s

Sign-invariance is preserved by precomposition with a map into the set.

theorem TauCeti.SignInvariant.union {α : Type u_1} {R : Type u_3} [Zero R] [Preorder R] [DecidableLT R] {f : α → R} {s t : Set α} (hs : SignInvariant f s) (ht : SignInvariant f t) (hst : (s ∩ t).Nonempty) : SignInvariant f (s ∪ t)

Sign-invariance on two sets that meet is sign-invariance on their union.

theorem Set.Subsingleton.signInvariant {α : Type u_1} {R : Type u_3} [Zero R] [Preorder R] [DecidableLT R] {f : α → R} {s : Set α} (hs : s.Subsingleton) : TauCeti.SignInvariant f s

A function is sign-invariant on a set containing at most one point.

@[simp]

theorem TauCeti.signInvariant_empty {α : Type u_1} {R : Type u_3} [Zero R] [Preorder R] [DecidableLT R] {f : α → R} : SignInvariant f ∅

@[simp]

theorem TauCeti.signInvariant_singleton {α : Type u_1} {R : Type u_3} [Zero R] [Preorder R] [DecidableLT R] {f : α → R} (a : α) : SignInvariant f {a}

@[simp]

theorem TauCeti.signInvariant_const {α : Type u_1} {R : Type u_3} [Zero R] [Preorder R] [DecidableLT R] {s : Set α} (c : R) : SignInvariant (fun (x : α) => c) s

A constant function is sign-invariant on every set.

Sign conditions

theorem TauCeti.subset_or_disjoint_setOf_sign {α : Type u_1} {R : Type u_3} [Zero R] [Preorder R] [DecidableLT R] {t : Set α} {ι : Type u_4} {f : ι → α → R} (hf : ∀ (i : ι), SignInvariant (f i) t) (Φ : (ι → SignType) → Prop) : t ⊆ {x : α | Φ fun (i : ι) => SignType.sign (f i x)} ∨ Disjoint t {x : α | Φ fun (i : ι) => SignType.sign (f i x)}

If each function f i is sign-invariant on t, then t lies inside or outside every set described by a condition on the signs of the f i.

theorem TauCeti.range_sign_sample_eq {α : Type u_1} {R : Type u_3} [Zero R] [Preorder R] [DecidableLT R] {ι : Type u_4} {f : ι → α → R} {𝒞 : Set (Set α)} (h𝒞 : ⋃₀ 𝒞 = Set.univ) (hf : ∀ (i : ι), ∀ E ∈ 𝒞, SignInvariant (f i) E) (x : ↑𝒞 → α) (hx : ∀ (E : ↑𝒞), x E ∈ ↑E) : (Set.range fun (E : ↑𝒞) (i : ι) => SignType.sign (f i (x E))) = Set.range fun (y : α) (i : ι) => SignType.sign (f i y)

Sample points realize all sign conditions. Let the functions f i be sign-invariant on each set of a family 𝒞 covering α, and pick a sample point x E in each E ∈ 𝒞. Then the sign vectors of the f i at the sample points are exactly the sign vectors they take on α.

Algebraic operations

The sign of a negation, a product or a power is determined by the signs of its inputs, so these operations preserve sign-invariance.

theorem TauCeti.SignInvariant.neg {α : Type u_1} {R : Type u_3} [AddGroup R] [Preorder R] [DecidableLT R] [AddLeftStrictMono R] {f : α → R} {s : Set α} (h : SignInvariant f s) : SignInvariant (fun (x : α) => -f x) s

The negation of a sign-invariant function is sign-invariant.

@[simp]

theorem TauCeti.signInvariant_neg_iff {α : Type u_1} {R : Type u_3} [AddGroup R] [Preorder R] [DecidableLT R] [AddLeftStrictMono R] {f : α → R} {s : Set α} : SignInvariant (fun (x : α) => -f x) s ↔ SignInvariant f s

A function is sign-invariant exactly when its negation is.

theorem TauCeti.SignInvariant.mul {α : Type u_1} {R : Type u_3} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {f g : α → R} {s : Set α} (hf : SignInvariant f s) (hg : SignInvariant g s) : SignInvariant (fun (x : α) => f x * g x) s

The product of two sign-invariant functions is sign-invariant.

theorem TauCeti.SignInvariant.pow {α : Type u_1} {R : Type u_3} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {f : α → R} {s : Set α} (hf : SignInvariant f s) (n : ℕ) : SignInvariant (fun (x : α) => f x ^ n) s

A power of a sign-invariant function is sign-invariant.

theorem TauCeti.signInvariant_finsetProd {α : Type u_1} {R : Type u_3} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {ι : Type u_4} {f : ι → α → R} {s : Set α} (I : Finset ι) (hf : ∀ i ∈ I, SignInvariant (f i) s) : SignInvariant (fun (x : α) => ∏ i ∈ I, f i x) s

A finite product of sign-invariant functions is sign-invariant.

theorem IsPreconnected.signInvariant {α : Type u_1} {R : Type u_3} [Zero R] [LinearOrder R] [TopologicalSpace R] [OrderTopology R] [TopologicalSpace α] {f : α → R} {s : Set α} (hs : IsPreconnected s) (hf : ContinuousOn f s) (h0 : ∀ x ∈ s, f x ≠ 0) : TauCeti.SignInvariant f s

A function that is continuous and nowhere zero on a preconnected set is sign-invariant there.

theorem IsPreconnected.signInvariant_of_eq_zero_iff {α : Type u_1} {R : Type u_3} [Zero R] [LinearOrder R] [TopologicalSpace R] [OrderTopology R] [TopologicalSpace α] {f : α → R} {s : Set α} (hs : IsPreconnected s) (hf : ContinuousOn f s) (h0 : ∀ x ∈ s, ∀ y ∈ s, f x = 0 ↔ f y = 0) : TauCeti.SignInvariant f s

A function that is continuous on a preconnected set, and vanishes either at every point of the set or at none, is sign-invariant there.

theorem IsPreconnected.signInvariant_of_locally {α : Type u_1} {R : Type u_3} [Zero R] [Preorder R] [DecidableLT R] [TopologicalSpace α] {f : α → R} {s : Set α} (hs : IsPreconnected s) (hlocal : ∀ x ∈ s, ∃ (U : Set α), IsOpen U ∧ x ∈ U ∧ TauCeti.SignInvariant f (s ∩ U)) : TauCeti.SignInvariant f s

Local sign-invariance on relative neighborhoods implies sign-invariance on a preconnected set. No continuity of the function itself is required.