polynomial help

Stream: new members

[liu]

屏幕截图 2025-02-04 171158.png
how to prove h4?who can help me

[Ilmārs Cīrulis]

Can you paste it here as a text?

import Mathlib

theorem max_solution etc.

[liu]

import Mathlib

theorem max_solution(p : Polynomial ℤ ) (h:p.eval 100=100) : {k : ℤ | p.eval k =k^3}.Finite ∧ {k : ℤ | p.eval k=k^3}.ncard≤10:=by

have h1 : ∃ q : Polynomial ℤ, q = p - Polynomial.X ^ 3 := by

-- 定义q为p - X^3

exact ⟨p - Polynomial.X ^ 3, by ring⟩

-- 解构存在量词，获取q及其定义

cases h1 with

| intro q hq =>

-- 现在q是p - X^3，hq是q = p - X^3的证明

-- 应用h到hq上，得到q.eval 100 = 100 - 100^3    

have h2:Polynomial.eval 100 q=-999900:=by

rw[hq];simp [Polynomial.eval_sub,h];ring;

-- 使用多项式根的有限性定理

have h3 : {k : ℤ | q.eval k = 0}.Finite := by

apply Polynomial.finite_setOf_isRoot

-- 证明q(k) ≠ 0，即q(k)有有限个根

intro k

have h_1:Polynomial.eval 100 q=-999900->False:=by

rw[k];

norm_num

apply h_1;linarith;

have h4 : {k : ℤ | q.eval k = 0}.ncard ≤ 10 := by

-- 根据多项式次数限制根的数量

apply le_of_not_gt

intro h_gt

-- 假设根的数量超过10，导致矛盾

have h_contra := {k : ℤ | q.eval k = 0}.ncard

exact ⟨h3, h4⟩

[liu]

新建 文本文档.txt

[Kevin Buzzard]

Please read #backticks and edit your post above

[liu]

import Mathlib
theorem max_solution(p : Polynomial ℤ ) (h:p.eval 100=100) : {k : ℤ | p.eval k =k^3}.Finite ∧ {k : ℤ | p.eval k=k^3}.ncard≤10:=by
  have h1 : ∃ q : Polynomial ℤ, q = p - Polynomial.X ^ 3 := by
    -- 定义q为p - X^3
    exact ⟨p - Polynomial.X ^ 3, by ring⟩
  -- 解构存在量词，获取q及其定义
  cases h1 with
  | intro q hq =>
    -- 现在q是p - X^3，hq是q = p - X^3的证明
    -- 应用h到hq上，得到q.eval 100 = 100 - 100^3
  have h2:Polynomial.eval 100 q=-999900:=by
    rw[hq];simp [Polynomial.eval_sub,h];ring;
  -- 使用多项式根的有限性定理
  have h3 : {k : ℤ | q.eval k = 0}.Finite := by
    apply Polynomial.finite_setOf_isRoot
    -- 证明q(k) ≠ 0，即q(k)有有限个根
    intro k
    have h_1:Polynomial.eval 100 q=-999900->False:=by
      rw[k];
      norm_num
    apply h_1;linarith;

  have h4 : {k : ℤ | q.eval k = 0}.ncard ≤ 10 := by
    -- 根据多项式次数限制根的数量

    apply le_of_not_gt
    intro h_gt
    -- 假设根的数量超过10，导致矛盾
    have h_contra := {k : ℤ | q.eval k = 0}.ncard
  exact ⟨h3, h4⟩

[liu]

sorry

[Ruben Van de Velde]

There's an error on line 12 that you need to fix first. What's the proof in English?

[liu]

A polynomial p(x) is called self - centered if it has integer coefficients and p(100)=100. If p(x) is a self - centered polynomial, what is the maximum number of integer solutions k to the equation p(k)=k^{3}?

[liu]

Is my train of thought feasible?If it is feasible,how can i proof h4

[Kevin Buzzard]

Can you get your code compiling? We're trying to teach you how to ask a good question, rather than just asking a question. Right now if I click on "view in lean 4 playground" I get an error. Please feel free to edit the post above rather than posting more messages. Right now I don't want to read beyond the first error in your code.

[liu]

sorry

[Kevin Buzzard]

You don't need to apologise, we're just showing you what a #mwe looks like. This is the best way to ask a question.

[Kevin Buzzard]

I think that set q := p - Polynomial.X ^ 3 with hq is better than your first few lines.

[Kevin Buzzard]

liu said:

Is my train of thought feasible?If it is feasible,how can i proof h4

Is this a maths question or a Lean question?

[liu]

Solve mathematical problems with Lean.

[Kevin Buzzard]

That's not how it works. Lean doesn't do the mathematics for you. You translate your maths proof into Lean so you need to know the maths proof first.

[liu]

Ok.Thanks for reminding

[liu]

how should I define the list?

import Mathlib
def factors:list ℕ :={1,1,2,3,3,3,5,5,11,101}

[Ilmārs Cīrulis]

import Mathlib

def factors: List ℕ := [1, 1, 2, 3, 3, 3, 5, 5, 11, 101]

[liu]

OK

[liu]

I want to define a polynomial with integer coefficients q(x) and I want to express q(x) as a product of its factors

q(x)=p(x)-x^3; q(x)=q\0(x)*(x-r\1)*(x-r\2)...(x-r\n)

[Julian Berman]

Can you share what you've tried and/or found already? Specifically you've found docs#Polynomial at least?

[Yaël Dillies]

It would be helpful if you wrote a #mwe, but here's a start:

import Mathlib

open Polynomial

example : True := by
  have p : ℤ[X] := sorry -- you told me you already had this
  let q : ℤ[X] := p - X ^ 3
  have := q.prod_multiset_X_sub_C_of_monic_of_roots_card_eq
  sorry

[liu]

Yes,the start is my need.But What should I use this

have := q.prod_multiset_X_sub_C_of_monic_of_roots_card_eq
  sorry

[Yaël Dillies]

docs#Polynomial.prod_multiset_X_sub_C_of_monic_of_roots_card_eq proves that a polynomial that has as many roots as its degree can be written as the product of linear factors

[Yaël Dillies]

Is this not what you want?

[liu]

No,No.This is my want.But I dont 't know how to use it to rewrite q(x)

[Yaël Dillies]

rw [← this] before the sorry

[liu]

Why ?There is a errro. Tactic 'rewrite' failed, did not find instance of the pattern in the target expression

import Mathlib

open Polynomial

example : True := by
  have p : ℤ[X] := sorry -- you told me you already had this
  let q : ℤ[X] := p - X ^ 3
  have := q.prod_multiset_X_sub_C_of_monic_of_roots_card_eq
  rw[<-this]

[Yaël Dillies]

You can't rewrite at the goal, there is no q there. Where do you want to rewrite q?

[Yaël Dillies]

Again, a #mwe would be helpful ( :point_left: this is a link you should click)

[liu]

I don't understand what's wrong with my question. Please point it out clearly. I've read the documentation, but I didn't find any problems. Sorry.

[Yaël Dillies]

There are many ways in which you could "define a polynomial", and which way is best for you depends on the context in which you need it. A #mwe would provide me with context to adapt my answer to your needs. Currently, I am forced to guess what you are trying to do

[liu]

I want to proof this

theorem max_solution(p : Polynomial ℤ ) (h:p.eval 100=100) : {k : ℤ | p.eval k =k^3}.Finite ∧ {k : ℤ | p.eval k=k^3}.ncard=10:=by

Now I want to define q(x)=p(x)-x^{3}, and then factorize q(100) into a product of its factors. For this theorem, I want to factorize q(100) as (x - m_1)*(x - m_2)...=p(100)-100^3. Then I factorize the right - hand side of the equation as -999900=(1)( - 1)(2)( - 2)(3)( - 3)(5)( - 5)( - 11)(101), and finally determine the number of these m's.

[Yaël Dillies]

Note that a #mwe should include imports

[Yaël Dillies]

Here's how to test whether your code snippet is a #mwe: Hover over the top right corner of the snippet and click this button. If it compiles (or fails in the way you want to demonstrate), you've made a MWE :tada:

[liu]

import Mathlib

theorem max_solution(p : Polynomial ℤ ) (h:p.eval 100=100) : {k : ℤ | p.eval k =k^3}.Finite ∧ {k : ℤ | p.eval k=k^3}.ncard=10:=by sorry

Ok?So do you undestand my mind?

[Yaël Dillies]

Great! Now we can focus on the math

[Yaël Dillies]

liu said:

q(100) into a product of its factors

Do you mean prime factors here?

[liu]

Yes

[Yaël Dillies]

Okay, and when you say you want to "factorize q(100) as (x - m_1)*(x - m_2)...", what are m_1, m_2, ...? Are they integers? Complex numbers?

[liu]

They are the roots of the equation \(q(x) = 0\) and are integers.

[Yaël Dillies]

How do you know you can do that then? eg q could be X ^ 2 + 1 which has no integer roots

[liu]

Since \(p(x)\) is unknown and we only know that \(p(100) = 100\), what we need to find is the maximum number of integer solutions of \(q(x)\). Sorry, in this case, the theorem needs to be modified.

import Mathlib

theorem max_solution(p : Polynomial ℤ ) (h:p.eval 100=100) : {k : ℤ | p.eval k =k^3}.Finite ∧ {k : ℤ | p.eval k=k^3}.ncard≤10:=by sorry

[Yaël Dillies]

Ah! A point for Lean :smile:

[Yaël Dillies]

So you assume that m₁, m₂, ... are roots (possibly with multiplicity) of q, and factorise q as R * (X - m₁) * (X - m₂) ... for some polynomial R?

[liu]

Good

[Yaël Dillies]

I don't actually think we have the lemma to do that. Here's how I figured this out:

[Yaël Dillies]

@loogle Polynomial.roots, Finset.prod

[Yaël Dillies]

@loogle Polynomial.roots, Finset.prod

[loogle]

:search: Polynomial.roots_prod, Polynomial.roots_prod_X_sub_C, and 2 more

[Yaël Dillies]

None of these fit your informal description

[liu]

This is the original question:
A polynomial p(x) is called self - centered if it has integer coefficients and p(100)=100. If p(x) is a self - centered polynomial, what is the maximum number of integer solutions k to the equation p(k)=k^3?
Do you have any other ideas?

[Kevin Buzzard]

There are two issues at stake here. The first is the maths. The second is formalising the maths. Right now I think we have questions about the maths. You can't factorise q(100) as (x - m_1)(x -m_2)..., this makes no sense. q(100) is a number, not a polynomial. It's hopeless trying to formalise this question in lean until we see a full informal maths argument.

[Yaël Dillies]

Here's the lemma I think you should prove:

import Mathlib

open Polynomial

theorem Polynomial.exists_eq_mul_prod_of_le_roots {p : ℤ[X]} {m : Multiset ℤ} (hmp : m ≤ p.roots) :
    ∃ q : ℤ[X], p = q * (m.map (X - C ·)).prod := sorry

[Yaël Dillies]

Hopefully it is straightforward using induction on m and mathlib lemmas

[Yaël Dillies]

Then you can use it in your proof by setting m := p.roots

[Yaël Dillies]

Kevin Buzzard said:

There are two issues at stake here. The first is the maths. The second is formalising the maths. Right now I think we have questions about the maths. You can't factorise q(100) as (x - m_1)(x -m_2)..., this makes no sense. q(100) is a number, not a polynomial. It's hopeless trying to formalise this question in lean until we see a full informal maths argument.

I agree, but I think I've understood the informal maths argument. "q(100) as (x - m_1)(x -m_2)..." is abuse of notation for "factorise q, then evaluate that factorisation at 100"

[liu]

So we can factorize first and then substitute the value to ensure that there are no issues with types.But how should we use the method of induction? I'd like to hear your insightful opinions.

[Yaël Dillies]

Here's a start:

import Mathlib

open Polynomial

theorem Polynomial.exists_eq_mul_prod_of_le_roots {p : ℤ[X]} {m : Multiset ℤ} (hmp : m ≤ p.roots) :
    ∃ q : ℤ[X], p = q * (m.map (X - C ·)).prod := by
  induction m using Multiset.induction with
  | empty =>
    sorry
  | cons r m ih =>
    obtain ⟨q, rfl⟩ := ih <| (m.le_cons_self _).trans hmp
    sorry

[liu]

I don't know What's the function of “using Multiset.induction” in the seventh line? Can you explain it?

[Yaël Dillies]

If you hover over the induction keyword, you'll see an explanation. It instructs induction to use docs#Multiset.induction (the standard induction principle for multisets) as the induction principle

[liu]

What should I do next?

import Mathlib

open Polynomial

theorem Polynomial.exists_eq_mul_prod_of_le_roots {p : ℤ[X]} {m : Multiset ℤ} (hmp : m ≤ p.roots) :
    ∃ q : ℤ[X], p = q * (m.map (X - C ·)).prod := by
  induction m using Multiset.induction with
  | empty =>
    exact ⟨p, by simp⟩
  | cons r m ih =>
    obtain ⟨q, rfl⟩ := ih <| (m.le_cons_self _).trans hmp
    sorry

[liu]

I'm working on a problem about the number of roots of a polynomial, but I don't know how to formalize the problem statement. What should I do?
The problem statement:
A polynomial p(x) is called self - centered if it has integer coefficients and p(100)=100. If p(x) is a self - centered polynomial, what is the maximum number of integer solutions k to the equation p(k)=k^3?

[Luigi Massacci]

see docs#Polynomial

[Luigi Massacci]

This is not very hard. What have you tried so far?

[Metin Ersin Arıcan]

Also docs#IsGreatest is helpful.

[liu]

This is my idea, but I don't know how to prove that the number of roots of the polynomial \(q(x)\) is less than 10.

import Mathlib
example(p : Polynomial ℤ ) (h:p.eval 100=100) : {k : ℤ | p.eval k=k^3}.ncard≤ 10:=by
  have h1 : ∃ q : Polynomial ℤ, q = p - Polynomial.X ^ 3 := by
    exact ⟨p - Polynomial.X ^ 3, by ring⟩
  cases h1 with
  | intro q hq =>
  have h2:Polynomial.eval 100 q=-999900:=by
    rw[hq];simp [Polynomial.eval_sub,h]
  have h3 : {k : ℤ | q.eval k = 0}.Finite := by
    apply Polynomial.finite_setOf_isRoot
    intro k
    have h_1:Polynomial.eval 100 q=-999900->False:=by
      rw[k];
      norm_num
    apply h_1;linarith;
  have h4 : {k : ℤ | q.eval k = 0}.ncard ≤ 10 := by sorry
  have h5:{k | Polynomial.eval k p = k ^ 3}.Finite:=by sorry

[Ruben Van de Velde]

You've asked this exact same question before, haven't you?

[liu]

yes

[Notification Bot]

7 messages were moved here from #new members > How to formalize the problem statement by Ruben Van de Velde.

[Ruben Van de Velde]

It's fine if you still need help, but you should reuse the thread so people can see the context

[Ruben Van de Velde]

In this case I still don't understand the mathematical proof. Defining q makes sense, and then you know $q(100)=100-100^3$, but I don't see how that gets you a bound on the number of roots

[liu]

微信图片_20250209170745.jpg
Why has it become blurry? Can you see it clearly?

[Luigi Massacci]

(and you should have a line of the sort that since you are searching for the max, you can suppose that $q_0$ is constant, and then a unit since $q$ is monic q doesn’t have to be monic, don’t know why I said that, but you can still suppose it’s a unit by maximality)

[Eric Wieser]

Note that you can write $\LaTeX$ directly into Zulip

[Notification Bot]

21 messages were moved here from #lean4 > polynomial by Eric Wieser.

[Notification Bot]

56 messages were moved here from #new members > How to define a polynomial by Eric Wieser.