polynomial preimage of nonzero is dense

Stream: Is there code for X?

[Daniel Packer]

Hi y'all.
I was able to show the following for finite dimensional polynomials:

lemma poly_nonzero_dense {p : ℝ[X]} (hp : p ≠ 0) :
  dense {x : ℝ | polynomial.eval x p ≠ 0} := sorry

This should also hold for multivariable polynomials:

lemma mvpoly_nonzero_dense {σ : Type*} {p : mv_polynomial σ ℝ} (hp : p ≠ 0) :
  dense {x : σ → ℝ | mv_polynomial.eval x p ≠ 0} := sorry

Is this somewhere in mathlib? If not, does it seem plausible to prove with the state of mathlib right now?
I'd be okay with having [fintype σ] floating around if it makes it easier.

[Daniel Packer]

If it's helpful, here are my imports and locale:

import data.polynomial.basic
import data.polynomial.eval
import data.mv_polynomial.basic
import data.real.basic
import topology.basic
import data.polynomial.ring_division
import topology.instances.real
import data.set.prod

open_locale polynomial

[Yaël Dillies]

The first one is true for general 0 and because the complement of your set is finite, right?

[Daniel Packer]

What do you mean by general 0?

[Yaël Dillies]

Sorry :grinning:

lemma poly_nonzero_dense (a : ℝ) {p : ℝ[X]} (hp : p ≠ a) :
  dense {x : ℝ | polynomial.eval x p ≠ a} := sorry

[Yaël Dillies]

Or maybe you have to spell it a • C.

[Daniel Packer]

Oh yeah, this is also true, but this should also be true for the mv_poly case, since you can subtract by a and get the same example

[Daniel Packer]

But it is true that the way I showed it for the single variable case was just using that it was a finite subset of ℝ

[Daniel Packer]

Or rather, complement of a finite subset of ℝ

[Daniel Packer]

Speaking of which, is there code for:

lemma compl_finset_dense_in_R (S : finset ℝ) : dense (↑S : set ℝ)ᶜ := sorry,

?

[Yaël Dillies]

I would call it set.finite.dense_compl (by using docs#set.finite and the correct generality of topological spaces), and that doesn't seem to exist. But I find that mildly surprising.

[Daniel Packer]

I have code for it. Is it worth PRing?
I did use the auxiliary lemma:

lemma set.finite.min_diff (S : set ℝ) (hS : S.finite) : ∃ ε : ℝ, ε > 0 ∧ ∀ x y : ℝ, x ∈ S → y ∈ S → y ≠ x → |x - y| > ε := sorry

[Yaël Dillies]

If you have a greater generality, I would say yes. You can spell this auxiliary lemma using docs#set.pairwise.

[Daniel Packer]

Yaël Dillies said:

I would call it set.finite.dense_compl (by using docs#set.finite and the correct generality of topological spaces), and that doesn't seem to exist. But I find that mildly surprising.

This isn't always true, though, right? You need something like connected maybe?

[Kyle Miller]

I think the hypothesis for set.finite.dense_compl to be true for general S is that the space has no isolated points.

[Kyle Miller]

Oh, found it: docs#dense.diff_finset

[Kyle Miller]

docs#dense_compl_singleton does it for singleton sets without the t1 axiom.

[Kyle Miller]

It seems like you need the t1 axiom for finsets in general since, if you're inducting on the cardinality of the finset, you need to take intersections of dense sets, and it suffices having complements of points being open.

[Kyle Miller]

It would probably be good to have the docs#dense_compl_singleton version of docs#dense.diff_finset (maybe dense_compl_finset?)