NYLL
Module

fwdDiff_iter_succ_eq_zero_iff_exists_polynomial_natDegree_le.lean

Nyll.AlgebraicCurves.Foundations.Polynomial.fwdDiff_iter_succ_eq_zero_iff_exists_polynomial_natDegree_le
14 declarations indexed from sourceView source ↗

Module documentation

fwd Diff iter succ eq zero iff exists polynomial nat Degree le

Imports6
  • Mathlib.Algebra.Group.ForwardDiff
  • Mathlib.Algebra.Polynomial.Roots
  • Mathlib.RingTheory.Polynomial.Pochhammer
  • Mathlib.Tactic.Ring.RingNF
  • Mathlib.Tactic.SimpRw
  • Mathlib.Tactic.WLOG
Imported by4

Declarations

def

binom

L37 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.fwdDiff_iter_succ_eq_zero_iff_exists_polynomial_natDegree_le.P2mNewton.binom
Documentation

The binomial polynomial obtained by dividing the descending Pochhammer polynomial by the factorial.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace fwdDiff_iter_succ_eq_zero_iff_exists_polynomial_natDegree_le
open _root_.Polynomial Finset
namespace P2mNewton
variable {R : Type*} [Field R]
Lean source · statement
def binom (k : ℕ) : R[X]
theorem

binom_eval_natCast

L39 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.fwdDiff_iter_succ_eq_zero_iff_exists_polynomial_natDegree_le.P2mNewton.binom_eval_natCast
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace fwdDiff_iter_succ_eq_zero_iff_exists_polynomial_natDegree_le
open _root_.Polynomial Finset
namespace P2mNewton
variable {R : Type*} [Field R]
Lean source · statement
theorem binom_eval_natCast [CharZero R] (k n : ℕ) :
    (binom k : R[X]).eval (n : R) = (n.choose k : R)
theorem

natDegree_binom_le

L46 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.fwdDiff_iter_succ_eq_zero_iff_exists_polynomial_natDegree_le.P2mNewton.natDegree_binom_le
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace fwdDiff_iter_succ_eq_zero_iff_exists_polynomial_natDegree_le
open _root_.Polynomial Finset
namespace P2mNewton
variable {R : Type*} [Field R]
Lean source · statement
theorem natDegree_binom_le (k : ℕ) : (binom k : R[X]).natDegree ≤ k
def

newton

L53 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.fwdDiff_iter_succ_eq_zero_iff_exists_polynomial_natDegree_le.P2mNewton.newton
Documentation

The truncated Newton interpolation polynomial formed from forward differences at the base point.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace fwdDiff_iter_succ_eq_zero_iff_exists_polynomial_natDegree_le
open _root_.Polynomial Finset
namespace P2mNewton
variable {R : Type*} [Field R]
Lean source · statement
def newton (f : ℤ → R) (d : ℕ) (y : ℤ) : R[X]
theorem

natDegree_newton_le

L56 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.fwdDiff_iter_succ_eq_zero_iff_exists_polynomial_natDegree_le.P2mNewton.natDegree_newton_le
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace fwdDiff_iter_succ_eq_zero_iff_exists_polynomial_natDegree_le
open _root_.Polynomial Finset
namespace P2mNewton
variable {R : Type*} [Field R]
Lean source · statement
theorem natDegree_newton_le (f : ℤ → R) (d : ℕ) (y : ℤ) : (newton f d y).natDegree ≤ d
theorem

newton_eval

L64 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.fwdDiff_iter_succ_eq_zero_iff_exists_polynomial_natDegree_le.P2mNewton.newton_eval
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace fwdDiff_iter_succ_eq_zero_iff_exists_polynomial_natDegree_le
open _root_.Polynomial Finset
namespace P2mNewton
variable {R : Type*} [Field R]
Lean source · statement
theorem newton_eval [CharZero R] (f : ℤ → R) (d : ℕ) (y : ℤ) (n : ℕ) :
    (newton f d y).eval ((y + n : ℤ) : R) =
      ∑ k ∈ range (d + 1), (n.choose k : R) * (fwdDiff (1 : ℤ))^[k] f y
theorem

iter_zero

L73 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.fwdDiff_iter_succ_eq_zero_iff_exists_polynomial_natDegree_le.P2mNewton.iter_zero
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace fwdDiff_iter_succ_eq_zero_iff_exists_polynomial_natDegree_le
open _root_.Polynomial Finset
namespace P2mNewton
variable {R : Type*} [Field R]
Lean source · statement
theorem iter_zero (i : ℕ) : (fwdDiff (1 : ℤ))^[i] (0 : ℤ → R) = 0
theorem

iter_eq_zero_of_le

L83 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.fwdDiff_iter_succ_eq_zero_iff_exists_polynomial_natDegree_le.P2mNewton.iter_eq_zero_of_le
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace fwdDiff_iter_succ_eq_zero_iff_exists_polynomial_natDegree_le
open _root_.Polynomial Finset
namespace P2mNewton
variable {R : Type*} [Field R]
Lean source · statement
theorem iter_eq_zero_of_le {f : ℤ → R} {d : ℕ} (h : ∀ n, (fwdDiff (1 : ℤ))^[d + 1] f n = 0)
    {j : ℕ} (hj : d + 1 ≤ j) (n : ℤ) : (fwdDiff (1 : ℤ))^[j] f n = 0
theorem

eq_newton_eval

L91 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.fwdDiff_iter_succ_eq_zero_iff_exists_polynomial_natDegree_le.P2mNewton.eq_newton_eval
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace fwdDiff_iter_succ_eq_zero_iff_exists_polynomial_natDegree_le
open _root_.Polynomial Finset
namespace P2mNewton
variable {R : Type*} [Field R]
Lean source · statement
theorem eq_newton_eval [CharZero R] {f : ℤ → R} {d : ℕ}
    (h : ∀ n, (fwdDiff (1 : ℤ))^[d + 1] f n = 0) (y : ℤ) (n : ℕ) :
    f (y + n) = (newton f d y).eval ((y + n : ℤ) : R)
theorem

newton_eq_newton

L116 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.fwdDiff_iter_succ_eq_zero_iff_exists_polynomial_natDegree_le.P2mNewton.newton_eq_newton
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace fwdDiff_iter_succ_eq_zero_iff_exists_polynomial_natDegree_le
open _root_.Polynomial Finset
namespace P2mNewton
variable {R : Type*} [Field R]
Lean source · statement
theorem newton_eq_newton [CharZero R] {f : ℤ → R} {d : ℕ}
    (h : ∀ n, (fwdDiff (1 : ℤ))^[d + 1] f n = 0) (y y' : ℤ) :
    newton f d y = newton f d y'
theorem

exists_polynomial

L133 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.fwdDiff_iter_succ_eq_zero_iff_exists_polynomial_natDegree_le.P2mNewton.exists_polynomial
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace fwdDiff_iter_succ_eq_zero_iff_exists_polynomial_natDegree_le
open _root_.Polynomial Finset
namespace P2mNewton
variable {R : Type*} [Field R]
Lean source · statement
theorem exists_polynomial [CharZero R] {f : ℤ → R} {d : ℕ}
    (h : ∀ n, (fwdDiff (1 : ℤ))^[d + 1] f n = 0) :
    ∃ p : R[X], p.natDegree ≤ d ∧ ∀ n : ℤ, f n = p.eval (n : R)
theorem

iter_eq_zero_of_polynomial

L142 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.fwdDiff_iter_succ_eq_zero_iff_exists_polynomial_natDegree_le.P2mNewton.iter_eq_zero_of_polynomial
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace fwdDiff_iter_succ_eq_zero_iff_exists_polynomial_natDegree_le
open _root_.Polynomial Finset
namespace P2mNewton
variable {R : Type*} [Field R]
Lean source · statement
theorem iter_eq_zero_of_polynomial {f : ℤ → R} {d : ℕ} (p : R[X]) (hp : p.natDegree ≤ d)
    (hf : ∀ n : ℤ, f n = p.eval (n : R)) (n : ℤ) :
    (fwdDiff (1 : ℤ))^[d + 1] f n = 0
theorem

main

L155 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.fwdDiff_iter_succ_eq_zero_iff_exists_polynomial_natDegree_le.P2mNewton.main
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace fwdDiff_iter_succ_eq_zero_iff_exists_polynomial_natDegree_le
open _root_.Polynomial Finset
namespace P2mNewton
variable {R : Type*} [Field R]
Lean source · statement
theorem main [CharZero R] (f : ℤ → R) (d : ℕ) :
    (∀ n : ℤ, (fwdDiff (1 : ℤ))^[d + 1] f n = 0) ↔
      ∃ p : Polynomial R, p.natDegree ≤ d ∧ ∀ n : ℤ, f n = p.eval (n : R)
theorem

fwdDiff_iter_succ_eq_zero_iff_exists_polynomial_natDegree_le

L162 ↗
Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace fwdDiff_iter_succ_eq_zero_iff_exists_polynomial_natDegree_le
open _root_.Polynomial Finset
Lean source · statement
theorem _root_.fwdDiff_iter_succ_eq_zero_iff_exists_polynomial_natDegree_le
    {R : Type*} [Field R] [CharZero R] (f : ℤ → R) (d : ℕ) :
    (∀ n : ℤ, (fwdDiff (1 : ℤ))^[d + 1] f n = 0) ↔
      ∃ p : Polynomial R, p.natDegree ≤ d ∧ ∀ n : ℤ, f n = p.eval (n : R)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.