Choosing finite order detectors in an open set

Finitely many transverse planes with directions in any prescribed nonempty open set detect ambient polynomial order uniformly at every center, for all polynomials of bounded degree. This permits restricting to directions that are good for analytic preparation of a discriminant, while retaining enough directions to recover the ambient order of the original polynomial on its root sections.

As a consequence, if the order of every transverse restriction in such an open set is locally constant along a family of points, then the ambient order is locally constant as well. Only finitely many restrictions are needed on a neighborhood of each point, even though the hypothesis is stated on the whole open set of analytically admissible directions.

The scalar field need only be a perfect T1 topological space; no compatibility between the field operations and the topology is used. In particular the result applies over ℝ and ℂ.

theorem TauCeti.exists_finset_orderAt_eq_iInf_transverse_of_isOpen {K : Type u_1} [Field K] [TopologicalSpace K] [T1Space K] [PerfectSpace K] (n D : ℕ) {U : Set (Fin n → K)} (hU : IsOpen U) (hne : U.Nonempty) : ∃ (T : Finset (Fin n → K)), ↑T ⊆ U ∧ ∀ (p : MvPolynomial (Fin (n + 1)) K), p.totalDegree ≤ D → ∀ (a : Fin (n + 1) → K), p.orderAt a = ⨅ (v : ↥T), ((MvPolynomial.aeval (Fin.cons (MvPolynomial.C (a 0) + MvPolynomial.X 1) fun (i : Fin n) => MvPolynomial.C (a i.succ) + MvPolynomial.C (↑v i) * MvPolynomial.X 0)) p).orderAt 0

A finite collection of transverse plane directions in any nonempty open set detects ambient order at every point for every polynomial with a prescribed total degree bound.

theorem TauCeti.eventually_orderAt_eq_of_transverse {K : Type u_1} {X : Type u_2} [Field K] [TopologicalSpace K] [T1Space K] [PerfectSpace K] [TopologicalSpace X] (n D : ℕ) {U : Set (Fin n → K)} (hU : IsOpen U) (hne : U.Nonempty) (p : X → MvPolynomial (Fin (n + 1)) K) (a : X → Fin (n + 1) → K) {x : X} (hp : ∀ᶠ (y : X) in nhds x, (p y).totalDegree ≤ D) (hlocal : ∀ v ∈ U, ∀ᶠ (y : X) in nhds x, ((MvPolynomial.aeval (Fin.cons (MvPolynomial.C (a y 0) + MvPolynomial.X 1) fun (i : Fin n) => MvPolynomial.C (a y i.succ) + MvPolynomial.C (v i) * MvPolynomial.X 0)) (p y)).orderAt 0 = ((MvPolynomial.aeval (Fin.cons (MvPolynomial.C (a x 0) + MvPolynomial.X 1) fun (i : Fin n) => MvPolynomial.C (a x i.succ) + MvPolynomial.C (v i) * MvPolynomial.X 0)) (p x)).orderAt 0) : ∀ᶠ (y : X) in nhds x, (p y).orderAt (a y) = (p x).orderAt (a x)

If every transverse-plane order in a nonempty open set of directions agrees with its value at a fixed parameter throughout some neighborhood, then the ambient orders agree on one common neighborhood. The neighborhoods for the individual directions may differ, and the total-degree bound is needed only near the fixed parameter.

theorem TauCeti.isLocallyConstant_orderAt_of_transverse {K : Type u_1} {X : Type u_2} [Field K] [TopologicalSpace K] [T1Space K] [PerfectSpace K] [TopologicalSpace X] (n D : ℕ) {U : Set (Fin n → K)} (hU : IsOpen U) (hne : U.Nonempty) (p : X → MvPolynomial (Fin (n + 1)) K) (a : X → Fin (n + 1) → K) (hp : ∀ (x : X), (p x).totalDegree ≤ D) (hlocal : ∀ v ∈ U, IsLocallyConstant fun (x : X) => ((MvPolynomial.aeval (Fin.cons (MvPolynomial.C (a x 0) + MvPolynomial.X 1) fun (i : Fin n) => MvPolynomial.C (a x i.succ) + MvPolynomial.C (v i) * MvPolynomial.X 0)) (p x)).orderAt 0) : IsLocallyConstant fun (x : X) => (p x).orderAt (a x)

Local constancy of all transverse-plane orders in a nonempty open set of directions implies local constancy of ambient polynomial order. The polynomial and the point may both vary with the parameter; only a uniform total-degree bound is required.