Zulip Chat Archive

Stream: general

Topic: Polymonial proof


Jiatong Gao (Apr 15 2025 at 01:16):

have h_Px :  i : Fin 3, Polynomial.eval (x i) P = 54 := by
    sorry

i want to ask how to prove this thing, I have no idea.
below is I defined

  let P : Polynomial  := 653 * ((X - C 1) * (X - C 2) * (X - C 4)) + C 2013
  let x : Fin 3   := ![1, 2, 4]

Jiatong Gao (Apr 15 2025 at 01:23):

I tried to cases it

  have h_Px :  i : Fin 3, Polynomial.eval (x i) P = 54 := by
    intro i
    fin_cases i
    · -- i = 0, x 0 = 1
      simp [x, P, Polynomial.eval_add, Polynomial.eval_mul, Polynomial.eval_sub,
            Polynomial.eval_X, Polynomial.eval_C]
      norm_num
    · -- i = 1, x 1 = 2
      simp [x, P, Polynomial.eval_add, Polynomial.eval_mul, Polynomial.eval_sub,
            Polynomial.eval_X, Polynomial.eval_C]
      norm_num
    · -- i = 2, x 2 = 4
      simp [x, P, Polynomial.eval_add, Polynomial.eval_mul, Polynomial.eval_sub,
            Polynomial.eval_X, Polynomial.eval_C]
      norm_num

But failed, it says that

unsolved goals
case «0»
P : [X] := 653 * ((X - C 1) * (X - C 2) * (X - C 4)) + C 2013
x : Fin 3   := ![1, 2, 4]
y : Fin 2   := ![0, 3]
h_x :  (i j : Fin 3), i  j  x i  x j
h_y :  (i j : Fin 2), i  j  y i  y j
 False

Ilmārs Cīrulis (Apr 15 2025 at 01:32):

That's because the value of the polynomial in each case is 2013, not 54, probably?

import Mathlib
open Polynomial

noncomputable def P : Polynomial  := 653 * ((X - C 1) * (X - C 2) * (X - C 4)) + C 2013

def x : Fin 3   := ![1, 2, 4]

theorem h_Px :  i : Fin 3, Polynomial.eval (x i) P = 2013 := by
  unfold P x
  intro i
  fin_cases i <;> simp

Jiatong Gao (Apr 15 2025 at 01:38):

Thanks a lot, there is full process now,I am the beginner and confused about how to figure there two polynomial out

import Mathlib
open Polynomial

/- Let $k$ and $n$ be positive integers and let $x_{1}, x_{2}, \ldots, x_{k}, y_{1}, y_{2}, \ldots, y_{n}$ be distinct integers. A polynomial $P$ with integer coefficients satisfies

$$
P\left(x_{1}\right)=P\left(x_{2}\right)=\ldots=P\left(x_{k}\right)=54
$$

and

$$
P\left(y_{1}\right)=P\left(y_{2}\right)=\ldots=P\left(y_{n}\right)=2013 .
$$

Determine the maximal value of $k n$. -/
theorem algebra_604776 :
   (k n : ),
    0 < k  0 < n 
     (x : Fin k  ) (y : Fin n  ),
      ( i j : Fin k, i  j  x i  x j) 
      ( i j : Fin n, i  j  y i  y j) 
       (P : Polynomial ),
        ( i, P.eval (x i) = 54) 
        ( i, P.eval (y i) = 2013) 
        k * n = 6 := by
  let P : Polynomial  := 653 * ((X - C 1) * (X - C 2) * (X - C 4)) + C 2013
  let x : Fin 3   := ![1, 2, 4]
  let y : Fin 2   := ![0, 3]
  have h_x :  i j : Fin 3, i  j  x i  x j := by
    intros i j hij
    fin_cases i <;> fin_cases j
    · contradiction
    · dsimp [x]; decide
    · dsimp [x]; decide
    · dsimp [x]; decide
    · contradiction
    · dsimp [x]; decide
    · dsimp [x]; decide
    · dsimp [x]; decide
    · contradiction


  have h_y :  i j : Fin 2, i  j  y i  y j := by
    intros i j hij
    fin_cases i <;> fin_cases j
    · contradiction
    · dsimp [y]; decide
    · dsimp [y]; decide
    · contradiction

  have h_Px :  i : Fin 3, Polynomial.eval (x i) P = 54 := by
    sorry

  have h_Py :  i, Polynomial.eval (y i) P = 2013 := by
    sorry


  exact 3, 2,
  by decide, by decide,
    x, y,
      h_x, h_y,
        P, h_Px, h_Py, by norm_num⟩⟩⟩⟩⟩⟩

Last updated: May 02 2025 at 03:31 UTC