Finite multivariate generic perturbations

A finite family of nonzero real multivariate polynomials can be made simultaneously nonzero by an arbitrarily small perturbation of any prescribed assignment. The proof avoids a separate density or transversality library.

First multiply the finite family. Since the real numbers form an infinite integral domain, MvPolynomial.funext implies that a nonzero polynomial has at least one nonzero evaluation. Join the original assignment to such an evaluation by a straight line. Every multivariate polynomial then becomes a nonzero univariate polynomial because its value at parameter one is nonzero. A small positive parameter avoiding the finitely many roots gives the required perturbation.

theorem NRR.FiniteMultivariateGenericPerturbation.exists_eval_ne_zero {J : Type u_1} (P : MvPolynomial J ℝ) (hP : P ≠ 0) : ∃ (b : J → ℝ), (MvPolynomial.eval b) P ≠ 0

A nonzero real multivariate polynomial has a nonzero evaluation.

theorem NRR.FiniteMultivariateGenericPerturbation.exists_common_eval_ne_zero {J : Type u_1} {I : Type u_2} [Finite I] (P : I → MvPolynomial J ℝ) (hP : ∀ (i : I), P i ≠ 0) : ∃ (b : J → ℝ), ∀ (i : I), (MvPolynomial.eval b) (P i) ≠ 0

A finite family of nonzero real multivariate polynomials has one common nonvanishing assignment.

noncomputable def NRR.FiniteMultivariateGenericPerturbation.linePolynomial {J : Type u_1} (a b : J → ℝ) (P : MvPolynomial J ℝ) : Polynomial ℝ

Substitute the affine line from a to b into a multivariate polynomial.

Equations

• NRR.FiniteMultivariateGenericPerturbation.linePolynomial a b P = MvPolynomial.eval₂ Polynomial.C (fun (j : J) => Polynomial.C (a j) + Polynomial.X * Polynomial.C (b j - a j)) P

theorem NRR.FiniteMultivariateGenericPerturbation.eval_linePolynomial {J : Type u_1} (a b : J → ℝ) (P : MvPolynomial J ℝ) (t : ℝ) : Polynomial.eval t (linePolynomial a b P) = (MvPolynomial.eval fun (j : J) => a j + t * (b j - a j)) P

Evaluation of the line polynomial is multivariate evaluation at the affine line.

@[simp]

theorem NRR.FiniteMultivariateGenericPerturbation.eval_one_linePolynomial {J : Type u_1} (a b : J → ℝ) (P : MvPolynomial J ℝ) : Polynomial.eval 1 (linePolynomial a b P) = (MvPolynomial.eval b) P

At parameter one, the line polynomial evaluates at the target assignment.

theorem NRR.FiniteMultivariateGenericPerturbation.linePolynomial_ne_zero_of_target {J : Type u_1} (a b : J → ℝ) (P : MvPolynomial J ℝ) (hb : (MvPolynomial.eval b) P ≠ 0) : linePolynomial a b P ≠ 0

A target nonvanishing evaluation makes the corresponding line polynomial nonzero.

theorem NRR.FiniteMultivariateGenericPerturbation.exists_small_positive_generic {J : Type u_1} {I : Type u_2} [Finite I] (P : I → MvPolynomial J ℝ) (hP : ∀ (i : I), P i ≠ 0) (a : J → ℝ) {eps : ℝ} (heps : 0 < eps) : ∃ (b : J → ℝ) (t : ℝ), 0 < t ∧ t < eps ∧ ∀ (i : I), (MvPolynomial.eval fun (j : J) => a j + t * (b j - a j)) (P i) ≠ 0

Simultaneously avoid a finite family of polynomial degeneracy conditions by an arbitrarily small positive displacement along one common affine line.