A polynomial with real coeffs and odd degree has a real root

Stream: Is there code for X?

[Ilmārs Cīrulis]

Is there a proof of this fact in Mathlib?

[Yaël Dillies]

This is very close to what @Artie Khovanov is currently doing in Lean

[Kenny Lau]

What is Khovanov working on?

[Kenny Lau]

Ilmārs Cīrulis said:

Is there a proof of this fact in Mathlib?

The main ingredient, which is lim[x→∞] P(x) = ∞, is Polynomial.tendsto_atTop_of_leadingCoeff_nonneg:

theorem tendsto_atTop_of_leadingCoeff_nonneg (hdeg : 0 < P.degree) (hnng : 0 ≤ P.leadingCoeff) :
    Tendsto (fun x => eval x P) atTop atTop :=

[Artie Khovanov]

@Yaël Dillies yes, this will be generalised in the proof that IVT for polys implies a field is real closed

[Artie Khovanov]

the proof is IVT + some estimate
the limit Kenny posted is sufficient but also overkill; it holds in every ordered field that an odd-degree polynomial attains both positive and negative values

[Artie Khovanov]

@Kenny Lau I'm working on the algebraic theory of real closed fields

[Junyan Xu]

Quick proof:
(factor into irreducible factors, one of which must be odd degree; it's known irreducible polynomials over R has degree at most two, so the factor has degree 1 and must have a root.)

import Mathlib.Analysis.Complex.Polynomial.Basic

open UniqueFactorizationMonoid
open Polynomial

-- move next to Finset.even_sum
theorem Multiset.even_sum {α} {s : Multiset α} [AddCommMonoid α]
    (h : ∀ a ∈ s, Even a) : Even s.sum := by
  apply s.induction_on' (by simp)
  intro a s ha hs even
  simpa using (h a ha).add even

example {f : ℝ[X]} (hf : Odd f.natDegree) : ∃ r, f.IsRoot r := by
  rw [← Nat.not_even_iff_odd] at hf
  have hf0 : f ≠ 0 := by rintro rfl; simp at hf
  have hff0 : 0 ∉ factors f := fun h ↦ (irreducible_of_factor _ h).ne_zero rfl
  have ⟨u, eq⟩ := factors_prod hf0
  rw [← natDegree_eq_natDegree (degree_eq_degree_of_associated (factors_prod hf0)),
    natDegree_multiset_prod _ hff0] at hf
  rw [← eq]
  simp_rw [IsRoot, eval_mul, eval_multiset_prod, mul_eq_zero, Multiset.prod_eq_zero_iff,
    Multiset.mem_map, ← IsRoot.def]
  contrapose! hf
  refine Multiset.even_sum fun n hn ↦ ?_
  obtain ⟨g, hg, rfl⟩ := Multiset.mem_map.mp hn
  rw [(irreducible_of_factor g hg).natDegree_le_two.lt_or_eq.resolve_left]
  · exact even_two
  intro lt
  have irr := irreducible_of_factor g hg
  have := irr.natDegree_pos
  have hg1 : g.natDegree = 1 := by omega
  have ⟨r, hr⟩ := exists_root_of_degree_eq_one ((degree_eq_iff_natDegree_eq irr.ne_zero).mpr hg1)
  exact (hf r).1 g hg hr

[Kenny Lau]

Nice proof! I wonder if this would be shorter than the one using analysis; and I also wonder if there is some code used in the proof of "irred -> deg <= 2" that somehow implies this result already

[Junyan Xu]

The proof of "irred -> deg <= 2" basically uses that the complexes have dimension 2 over the reals; I think it can by using minpoly rather than explicitly constructing the polynomials.

[Artie Khovanov]

This proof surely uses the analytic proof somewhere. (Or maybe it goes via a complex-analytic proof of FTA!)

[Artie Khovanov]

But yeah in mathematical terms this is overkill; all you need is that odd-degree polynomials attain different signs, and then completeness/IVT
However the algebraic theory of ordered fields is not very developed in Mathlib compared to the analytic theory of R/C...

[Kenny Lau]

another overkill using the same idea:

1. The absolute Galois group acts on the roots.
2. no real root -> no fixed-point.
3. Absolute Galois group is C2, which is prime, so 2 | #roots :slight_smile:

[Junyan Xu]

The proof of "irred -> deg <= 2" basically uses that the complexes have dimension 2 over the reals; I think it can by using minpoly rather than explicitly constructing the polynomials.

golfed at #26525 (it indeed uses FTA which is proven using Liouville since mathlib3#17343)

[Robin Arnez]

Here's also the analytic proof (an odd-degree polynomial tends to negative infinity on one end and to positive infinity on the other, use wlog so we only need to consider one case, then the existence of a root follows by continuity):

import Mathlib

theorem Polynomial.exists_isRoot_of_odd_natDegree
    {𝕜 : Type*} [NormedField 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
    [OrderTopology 𝕜] [PreconnectedSpace 𝕜]
    {p : Polynomial 𝕜} (hp : Odd p.natDegree) :
    ∃ x, p.IsRoot x := by
  simp only [IsRoot.def]
  suffices 0 ∈ (eval · p) '' Set.univ by simpa using this
  wlog h : 0 ≤ p.leadingCoeff
  · simpa using this (p := -p) (by simpa using hp) (by simpa using le_of_not_ge h)
  by_cases ne_zero : p = 0
  · simp_all
  apply isPreconnected_univ.intermediate_value_Iii (l₁ := Filter.atBot) (l₂ := Filter.atTop) _ _ _ _ _ (Set.mem_univ _)
  · simp
  · simp
  · fun_prop
  · suffices Filter.Tendsto (fun x => eval x (-(p.comp (- X)))) Filter.atTop Filter.atTop by
      simp only [eval_neg, eval_comp, eval_X, Filter.tendsto_neg_atTop_iff] at this
      simpa [Function.comp_def] using this.comp Filter.tendsto_neg_atBot_atTop
    apply tendsto_atTop_of_leadingCoeff_nonneg
    · rw [degree_eq_natDegree]
      · simpa [natDegree_comp] using hp.pos
      · simpa [comp_eq_zero_iff] using ne_zero
    · simpa [hp.neg_one_pow] using h
  · apply p.tendsto_atTop_of_leadingCoeff_nonneg _ h
    rw [degree_eq_natDegree ne_zero]
    simpa using hp.pos

[Ilmārs Cīrulis]

Big thanks to all!

[Kenny Lau]

So, now we shall have a poll on whether the analytic one gets to stay, or the algebraic one gets to stay

[Artie Khovanov]

I mean if this ends up in Mathlib I'll end up generalising it quite soon so it's a bit of a moot point

[Antoine Chambert-Loir]

Indeed, you'll certainly wish to prove that if R is real closed, then R(i) is algebraically closed.

[Artie Khovanov]

Well the result originally asked about is just one of the axioms of a real closed field (at least, the way I define them)
So really I'd be showing that the reals form a real closed field
Easiest way imo is basically the proof that an ordered field with IVT for polys is real closed
(And it is this proof that I gave above!)

[Jz Pan]

Junyan Xu said:

irreducible polynomials over R has degree at most two

I think this is also true for real closed fields. So these proofs essentially point to the same thing: the reals is real closed.