Showing a number is a root of a polynomial

Stream: Is there code for X?

[Janitha]

I know the roots of the polynomial f = X^4 - 4 * X^3 + 6 * X^2 - 4 * X - 2005, and one of them is 1 + √(-√(2006)). How do I show that it's indeed a root of f?

[Kevin Buzzard]

If you are expecting Lean code as an answer, then you would be far more likely to get it if you wrote Lean code for your question and asked it as a #mwe . The informal answer to your informal question is: just show $f(X)=(X-1)^4-2006$ and now it's easy.

[Robin Arnez]

In Lean I would've done:

def myFun (x : ℂ) : ℂ := x^4 - 4 * x^3 + 6 * x^2 - 4 * x - 2005

example : myFun (1 + (2006)^(4⁻¹ : ℂ) * Complex.I) = 0 := by
  unfold myFun
  ring_nf
  rw [one_div]
  rw [← Nat.cast_ofNat (n := 4)]
  rw [Complex.cpow_nat_inv_pow 2006 four_ne_zero]
  rw [Complex.I_pow_four]
  simp

ring_nf does most of the work here.

[Damiano Testa]

After, ring_nf, simp closes the goal.

[Janitha]

Here's what I'm trying to formalize.

import Mathlib
open Polynomial Complex Finset

example (P : ℝ) (f : ℝ [X]) (h : (f.map Complex.ofRealHom).roots.prod = Complex.ofReal P)
    (hP : f = X^4 - 4 * X^3 + 6 * X^2 - 4 * X - 2005): ⌊P⌋ = 45 := by



  have h1 : f.IsRoot (1 + (2006)^(4⁻¹ : ℂ) * Complex.I) := by sorry
  --(1 + (2006)^(4⁻¹ : ℂ) * Complex.I) gives an error, how do I fix it?


  have h2 : f.IsRoot (1 + (2006)^(4⁻¹ : ℂ) * Complex.I) := by sorry



  have h3 : f.IsRoot (1 + (2006)^(4⁻¹)) := by sorry
  --get an error here (4⁻¹) as well, how do I fix it?

  have h4 : f.IsRoot (1 - (2006)^(4⁻¹)) := by sorry


  have h5 : P = (1 + (2006)^(4⁻¹))  * (1 - (2006)^(4⁻¹)) := by sorry

  have h6 : P = 1 + 2006^(2⁻¹) := by sorry


  have h7 : ⌊P⌋ = 45 := by sorry

  apply h7

[Kevin Buzzard]

Instead of saying "I got an error here", you should read the error and then fix it, or post the error, because the error contains the instructions about what you should do.

[Janitha]

Fixed it:

have h1 : (Polynomial.map Complex.ofRealHom f).IsRoot (1 + (2006)^(4⁻¹ : ℂ) * Complex.I) := by

[Jz Pan]

Why don't you use Vieta's formula? And your theorem seems incorrect.

[Janitha]

@Jz Pan Why does it seem incorrect?

[Jz Pan]

I think f has no multiple roots, so P should be exactly -2005 so ⌊P⌋ = 45 is not true. See https://en.wikipedia.org/wiki/Vieta%27s_formulas

[Janitha]

Maybe my theorem statement is wrong? I wanted to express that P is the product of the complex roots of f and \floor P = 45.

[Aaron Liu]

The product of the complex roots of f is -2005, so the statement you have is impossible to prove.

[Jz Pan]

Regarding your sketch of proof, seems that P is the product of real roots of f.

[Janitha]

For some reason, I keep getting the complex roots as 1 + (\sqrt (\sqrt(2006)))i and 1 - (\sqrt (\sqrt(2006)))i. Is this wrong?

[Jz Pan]

What calculation program do you use?

[Aaron Liu]

"Complex roots" usually means all the complex roots, not just the complex roots which are not purely real. Do you mean the complex roots or the complex roots which are not real?

[Janitha]

I did it by hand.

[Janitha]

I meant the roots that are not real.

[Janitha]

I was able to get to:

import Mathlib
open Polynomial Complex Finset


example (P : ℝ) (f : ℝ[X]) (h : ((f.map Complex.ofRealHom).roots.filter (·.im ≠ 0)).prod = Complex.ofReal P)
    (hP : f = X ^ 4 - 4 * X ^ 3 + 6 * X ^ 2 - 4 * X - 2005) : ⌊P⌋ = 45 := by

  have h0 : f = (X - 1)^4 - 2006 := by
    rw [hP]
    ring

  have h1 : (f.map Complex.ofRealHom).IsRoot (1 + (2006)^(4⁻¹ : ℂ) * Complex.I) := by
    rw [h0]
    simp
    ring_nf
    simp


  have h2 : (f.map Complex.ofRealHom).IsRoot (1 - (2006)^(4⁻¹ : ℂ) * Complex.I) := by
    rw [h0]
    simp
    ring_nf
    simp

  have h3 : (f.map Complex.ofRealHom).IsRoot (1 + (2006)^(4⁻¹ : ℂ)) := by
    rw [h0]
    simp

  have h4 : (f.map Complex.ofRealHom).IsRoot (1 - (2006)^(4⁻¹ : ℂ)) := by
    rw [h0]
    simp
    ring_nf
    simp

  have h5 : P = (1 + (2006 : ℝ)^(2⁻¹ : ℝ)) := by
    sorry

  have h5' : 45 < P := by
    have h51 : 1936 < 2006 := by trivial
    have h51' : (1936 : ℝ)^(2⁻¹ : ℝ) = Real.sqrt 1936 := by
      rw [Real.sqrt_eq_rpow]
      norm_num
    have h51'' : (2006 : ℝ)^(2⁻¹ : ℝ) = Real.sqrt 2006 := by
      rw [Real.sqrt_eq_rpow]
      norm_num
    have h53 : (1936 : ℝ)^(2⁻¹ : ℝ) < (2006 : ℝ)^(2⁻¹ : ℝ) := by
      rw [h51', h51'']
      apply Real.sqrt_lt_sqrt
      linarith
      linarith
    have h53' : (1936 : ℝ)^(2⁻¹ : ℝ) = 44 := by
      rw [h51']
      calc Real.sqrt 1936 = Real.sqrt (44 * 44) := by norm_num
                        _ = 44 := by simp
    have h54 : 1 + (1936 : ℝ)^(2⁻¹ : ℝ) < (1 + (2006 : ℝ)^(2⁻¹ : ℝ)) := by
      exact (Real.add_lt_add_iff_left 1).mpr h53
    have h55 : 1 + 44 < (1 + (2006 : ℝ)^(2⁻¹ : ℝ)) := by
      rw [h53'] at h54
      exact h54
    rw [←h5] at h55
    linarith

  have h5'' : P < 46 := by sorry
  --Emulate the proof of `h5'` with minor adjustments.

  have h6 : ⌊P⌋ = 45 := by
    have : 45 ≤ ⌊P⌋ := Int.le_floor.mpr (le_of_lt h5')
    have : ⌊P⌋ < 46 := Int.floor_lt.mpr h5''
    linarith

  exact h6

I have no clue on how to fill in the sorry at h5. Can I get a hint?

My idea was the following. Since I know four distinct roots of the polynomial and the polynomial can have at most four roots, I can find P using h1 and h2.