The zero locus of a nonzero multivariate polynomial is null

A nonzero polynomial in finitely many variables over a measurable integral domain vanishes on a null set of any finite product of σ-finite measures without atoms; in particular, a nonzero real polynomial vanishes on a Lebesgue-null set. Determinants and minors are polynomials in the entries of a matrix, so this shows that generic polynomial conditions, such as nonsingularity, hold almost everywhere.

Main declarations

• MvPolynomial.measurable_eval — evaluation is measurable in the coordinates.
• MvPolynomial.measurableSet_setOfPred_eval_eq_zero — the zero locus of a multivariate polynomial is measurable.
• MvPolynomial.measure_pi_setOfPred_eval_eq_zero — the zero locus of a nonzero multivariate polynomial is null for a finite product of σ-finite measures without atoms.
• MvPolynomial.volume_setOfPred_eval_eq_zero — the same for the product volume.

theorem MvPolynomial.measurable_eval {R : Type u_1} {ι : Type u_2} [CommSemiring R] [MeasurableSpace R] [MeasurableAdd₂ R] [MeasurableMul₂ R] (P : MvPolynomial ι R) : Measurable fun (x : ι → R) => (eval x) P

Evaluating a multivariate polynomial is measurable in the coordinates: a polynomial is built from finitely many coordinate projections by addition and multiplication.

theorem MvPolynomial.measurableSet_setOfPred_eval_eq_zero {R : Type u_1} {ι : Type u_2} [CommSemiring R] [MeasurableSpace R] [MeasurableAdd₂ R] [MeasurableMul₂ R] [MeasurableSingletonClass R] (P : MvPolynomial ι R) : MeasurableSet {x : ι → R | (eval x) P = 0}

The zero locus of a multivariate polynomial is measurable.

theorem MvPolynomial.measure_pi_setOfPred_eval_eq_zero {R : Type u_1} {ι : Type u_2} [CommRing R] [IsDomain R] [MeasurableSpace R] [MeasurableSingletonClass R] [MeasurableAdd₂ R] [MeasurableMul₂ R] [Fintype ι] (μ : ι → MeasureTheory.Measure R) [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] [∀ (i : ι), MeasureTheory.NullSingletonClass (μ i)] (P : MvPolynomial ι R) (hP : P ≠ 0) : (MeasureTheory.Measure.pi μ) {x : ι → R | (eval x) P = 0} = 0

The zero locus of a nonzero multivariate polynomial is null for a finite product of σ-finite measures without atoms.

theorem MvPolynomial.volume_setOfPred_eval_eq_zero {R : Type u_1} {ι : Type u_2} [CommRing R] [IsDomain R] [MeasureTheory.MeasureSpace R] [MeasurableSingletonClass R] [MeasurableAdd₂ R] [MeasurableMul₂ R] [MeasureTheory.SigmaFinite MeasureTheory.volume] [MeasureTheory.NullSingletonClass MeasureTheory.volume] [Fintype ι] (P : MvPolynomial ι R) (hP : P ≠ 0) : MeasureTheory.volume {x : ι → R | (eval x) P = 0} = 0

The zero locus of a nonzero multivariate polynomial is volume-null when volume is a σ-finite measure without atoms; for instance, for real polynomials and Lebesgue measure.