Local persistence of a direction detecting polynomial order

The coefficients of the restriction of a polynomial to an affine line vary continuously with its base point and direction. On a set of constant finite ambient order, a direction that detects the order at one point therefore continues to detect it nearby. This is the uniformity step needed to apply analytic preparation along a parametrized base; it does not require the base to be smooth or connected.

theorem MvPolynomial.continuous_coeff_aeval_C_add_C_mul_X {σ : Type u_1} {R : Type u_2} [CommSemiring R] [TopologicalSpace R] [IsTopologicalSemiring R] (p : MvPolynomial σ R) (m : ℕ) : Continuous fun (av : (σ → R) × (σ → R)) => ((aeval fun (i : σ) => Polynomial.C (av.1 i) + Polynomial.C (av.2 i) * Polynomial.X) p).coeff m

Each coefficient of an affine-line restriction depends continuously on its base point and direction.

theorem MvPolynomial.eventually_natTrailingDegree_aeval_C_add_C_mul_X_eq {σ : Type u_1} {R : Type u_2} [CommSemiring R] [TopologicalSpace R] [IsTopologicalSemiring R] (p : MvPolynomial σ R) {S : Set (σ → R)} {a v : σ → R} {m : ℕ} [T1Space R] (horder : ∀ x ∈ S, p.orderAt x = ↑m) (hv : ((aeval fun (i : σ) => Polynomial.C (a i) + Polynomial.C (v i) * Polynomial.X) p).coeff m ≠ 0) : ∀ᶠ (x : σ → R) in nhdsWithin a S, (aeval fun (i : σ) => Polynomial.C (x i) + Polynomial.C (v i) * Polynomial.X) p ≠ 0 ∧ ((aeval fun (i : σ) => Polynomial.C (x i) + Polynomial.C (v i) * Polynomial.X) p).natTrailingDegree = m

On a set of constant finite ambient order, a direction detecting the order at one point continues to detect it locally, with nonzero line restrictions.