Module

Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow.lean

Nyll.AlgebraicCurves.Foundations.Polynomial.Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow

36 declarations indexed from sourceView source ↗

Module documentation

Nat exists polynomial forall eval eq of forall eq macaulay Pow

Imports24

Batteries.Tactic.Init
Mathlib.Algebra.CharZero.Defs
Mathlib.Algebra.Field.Rat
Mathlib.Algebra.Group.Monoid
Mathlib.Algebra.Group.Nat.Defs
Mathlib.Algebra.Group.Semigroup
Mathlib.Algebra.Polynomial.Basic
Mathlib.Algebra.Polynomial.Eval.Defs
Mathlib.Algebra.Ring.Rat
Mathlib.Data.Nat.Basic
Mathlib.Data.Nat.Cast.Basic
Mathlib.Data.Nat.Cast.Defs
Mathlib.Data.Nat.Choose.Basic
Mathlib.Data.Nat.Factorial.Basic
Mathlib.Data.Nat.Find
Mathlib.Order.Basic
Mathlib.Order.Defs.LinearOrder
Mathlib.Order.Defs.PartialOrder
Mathlib.RingTheory.Polynomial.Pochhammer
Mathlib.Tactic.FieldSimp
Mathlib.Tactic.Push
Mathlib.Tactic.Ring.RingNF
Mathlib.Tactic.Set
Nyll.AlgebraicCurves.Foundations.Algebra.Nat_MacaulayPow

Imported by3

def

top

L51 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow.PolyMaxSol.top

Documentation

The largest index up to a + d + 1 whose binomial coefficient of order d + 1 is at most a.

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow
namespace PolyMaxSol

Lean source · statement

def top (d a : ℕ) : ℕ

def

rem

L54 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow.PolyMaxSol.rem

Documentation

The remainder after subtracting the largest admissible binomial coefficient from a.

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow
namespace PolyMaxSol

Lean source · statement

def rem (d a : ℕ) : ℕ

theorem

macaulayPow_zero

L56 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow.PolyMaxSol.macaulayPow_zero

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow
namespace PolyMaxSol

Lean source · statement

theorem macaulayPow_zero (a : ℕ) : Nat.macaulayPow 0 a = 0

theorem

macaulayPow_succ

L59 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow.PolyMaxSol.macaulayPow_succ

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow
namespace PolyMaxSol

Lean source · statement

theorem macaulayPow_succ (d a : ℕ) :
    Nat.macaulayPow (d + 1) a = (top d a + 1).choose (d + 2) + Nat.macaulayPow d (rem d a)

theorem

sub_le_choose

L63 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow.PolyMaxSol.sub_le_choose

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow
namespace PolyMaxSol

Lean source · full declaration

theorem sub_le_choose (d : ℕ) : ∀ k : ℕ, k - d ≤ k.choose (d + 1)
  | 0 => by simp
  | k + 1 => by
      rw [Nat.choose_succ_succ']
      have ih := sub_le_choose d k
      rcases lt_or_ge k d with h | h
      · have : k + 1 - d = 0 := by omega
        omega
      · have hpos : 1 ≤ k.choose d := Nat.choose_pos h
        omega

theorem

choose_top_le

L74 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow.PolyMaxSol.choose_top_le

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow
namespace PolyMaxSol

Lean source · statement

theorem choose_top_le (d a : ℕ) : (top d a).choose (d + 1) ≤ a

theorem

top_le

L77 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow.PolyMaxSol.top_le

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow
namespace PolyMaxSol

Lean source · statement

theorem top_le (d a : ℕ) : top d a ≤ a + d + 1

theorem

lt_choose_of_top_lt

L79 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow.PolyMaxSol.lt_choose_of_top_lt

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow
namespace PolyMaxSol

Lean source · statement

theorem lt_choose_of_top_lt (d a : ℕ) {k : ℕ} (hk : top d a < k) : a < k.choose (d + 1)

theorem

lt_choose_top_succ

L86 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow.PolyMaxSol.lt_choose_top_succ

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow
namespace PolyMaxSol

Lean source · statement

theorem lt_choose_top_succ (d a : ℕ) : a < (top d a + 1).choose (d + 1)

theorem

top_eq_of

L89 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow.PolyMaxSol.top_eq_of

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow
namespace PolyMaxSol

Lean source · statement

theorem top_eq_of (d a k : ℕ) (h₁ : k.choose (d + 1) ≤ a) (h₂ : a < (k + 1).choose (d + 1)) :
    top d a = k

theorem

le_top_of_choose_le

L102 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow.PolyMaxSol.le_top_of_choose_le

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow
namespace PolyMaxSol

Lean source · statement

theorem le_top_of_choose_le (d a k : ℕ) (h : k.choose (d + 1) ≤ a) : k ≤ top d a

theorem

top_lt_of_lt_choose

L108 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow.PolyMaxSol.top_lt_of_lt_choose

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow
namespace PolyMaxSol

Lean source · statement

theorem top_lt_of_lt_choose (d a k : ℕ) (h : a < k.choose (d + 1)) : top d a < k

theorem

d_le_top

L115 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow.PolyMaxSol.d_le_top

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow
namespace PolyMaxSol

Lean source · statement

theorem d_le_top (d a : ℕ) : d ≤ top d a

theorem

top_zero_right

L118 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow.PolyMaxSol.top_zero_right

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow
namespace PolyMaxSol

Lean source · statement

theorem top_zero_right (d : ℕ) : top d 0 = d

theorem

d_lt_top_of_pos

L121 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow.PolyMaxSol.d_lt_top_of_pos

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow
namespace PolyMaxSol

Lean source · statement

theorem d_lt_top_of_pos (d a : ℕ) (ha : 0 < a) : d < top d a

theorem

top_zero_left

L125 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow.PolyMaxSol.top_zero_left

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow
namespace PolyMaxSol

Lean source · statement

theorem top_zero_left (a : ℕ) : top 0 a = a

theorem

rem_zero_left

L128 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow.PolyMaxSol.rem_zero_left

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow
namespace PolyMaxSol

Lean source · statement

theorem rem_zero_left (a : ℕ) : rem 0 a = 0

theorem

rem_add_choose

L131 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow.PolyMaxSol.rem_add_choose

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow
namespace PolyMaxSol

Lean source · statement

theorem rem_add_choose (d a : ℕ) : rem d a + (top d a).choose (d + 1) = a

theorem

rem_lt

L134 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow.PolyMaxSol.rem_lt

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow
namespace PolyMaxSol

Lean source · statement

theorem rem_lt (d a : ℕ) : rem d a < (top d a).choose d

theorem

top_mono

L139 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow.PolyMaxSol.top_mono

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow
namespace PolyMaxSol

Lean source · statement

theorem top_mono (d : ℕ) {a b : ℕ} (h : a ≤ b) : top d a ≤ top d b

theorem

macaulayPow_lt_choose

L142 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow.PolyMaxSol.macaulayPow_lt_choose

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow
namespace PolyMaxSol

Lean source · full declaration

theorem macaulayPow_lt_choose : ∀ (d m r : ℕ), r < m.choose d →
    Nat.macaulayPow d r < (m + 1).choose (d + 1)
  | 0, m, r, _ => by simp [macaulayPow_zero]
  | d + 1, m, r, h => by
      rw [macaulayPow_succ]
      change _ < (m + 1).choose (d + 2)
      have hK : top d r < m := top_lt_of_lt_choose d r m h
      have hrem : Nat.macaulayPow d (rem d r) < (top d r + 1).choose (d + 1) :=
        macaulayPow_lt_choose d (top d r) (rem d r) (rem_lt d r)
      have h1 : (top d r + 1).choose (d + 2) + (top d r + 1).choose (d + 1) =
          (top d r + 2).choose (d + 2) := by
        rw [Nat.choose_succ_succ' (top d r + 1) (d + 1), add_comm]
      have h2 : (top d r + 2).choose (d + 2) ≤ (m + 1).choose (d + 2) :=
        Nat.choose_le_choose _ (by omega)
      omega

theorem

top_macaulayPow

L158 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow.PolyMaxSol.top_macaulayPow

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow
namespace PolyMaxSol

Lean source · statement

theorem top_macaulayPow (d a : ℕ) :
    top (d + 1) (Nat.macaulayPow (d + 1) a) = top d a + 1

theorem

rem_macaulayPow

L170 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow.PolyMaxSol.rem_macaulayPow

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow
namespace PolyMaxSol

Lean source · statement

theorem rem_macaulayPow (d a : ℕ) :
    rem (d + 1) (Nat.macaulayPow (d + 1) a) = Nat.macaulayPow d (rem d a)

theorem

macaulayPow_zero_right

L177 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow.PolyMaxSol.macaulayPow_zero_right

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow
namespace PolyMaxSol

Lean source · full declaration

theorem macaulayPow_zero_right : ∀ d : ℕ, Nat.macaulayPow d 0 = 0
  | 0 => macaulayPow_zero 0
  | d + 1 => by
      rw [macaulayPow_succ, top_zero_right, Nat.choose_succ_self, zero_add]
      have : rem d 0 = 0 := by unfold rem; simp
      rw [this, macaulayPow_zero_right d]

def

G

L185 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow.PolyMaxSol.G

Documentation

The sequence obtained by iterating Macaulay powers with successively increasing degrees.

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow
namespace PolyMaxSol

Lean source · full declaration

def G (d a : ℕ) : ℕ → ℕ
  | 0 => a
  | j + 1 => Nat.macaulayPow (d + j + 1) (G d a j)

theorem

G_zero

L189 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow.PolyMaxSol.G_zero

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow
namespace PolyMaxSol

Lean source · statement

theorem G_zero (d a : ℕ) : G d a 0 = a

theorem

G_succ

L190 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow.PolyMaxSol.G_succ

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow
namespace PolyMaxSol

Lean source · statement

theorem G_succ (d a j : ℕ) : G d a (j + 1) = Nat.macaulayPow (d + j + 1) (G d a j)

theorem

G_zero_mid

L192 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow.PolyMaxSol.G_zero_mid

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow
namespace PolyMaxSol

Lean source · full declaration

theorem G_zero_mid : ∀ (d j : ℕ), G d 0 j = 0
  | d, 0 => rfl
  | d, j + 1 => by rw [G_succ, G_zero_mid d j, macaulayPow_zero_right]

theorem

top_G

L196 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow.PolyMaxSol.top_G

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow
namespace PolyMaxSol

Lean source · full declaration

theorem top_G (d a : ℕ) : ∀ j : ℕ, top (d + j) (G d a j) = top d a + j
  | 0 => rfl
  | j + 1 => by
      rw [G_succ, show d + (j + 1) = (d + j) + 1 from rfl, top_macaulayPow, top_G d a j]; omega

def

tail

L202 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow.PolyMaxSol.tail

Documentation

The auxiliary Macaulay-growth sequence, with the degree-zero case set to zero.

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow
namespace PolyMaxSol

Lean source · full declaration

def tail : ℕ → ℕ → ℕ → ℕ
  | 0, _, _ => 0
  | d + 1, r, j => G d r j

theorem

rem_G

L206 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow.PolyMaxSol.rem_G

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow
namespace PolyMaxSol

Lean source · full declaration

theorem rem_G : ∀ (d a j : ℕ), rem (d + j) (G d a j) = tail d (rem d a) j
  | 0, a, 0 => by simp [tail, G_zero, rem_zero_left]
  | 0, a, j + 1 => by
      rw [G_succ, show 0 + (j + 1) = (0 + j) + 1 from rfl, rem_macaulayPow, rem_G 0 a j]
      simp [tail, macaulayPow_zero_right]
  | d + 1, a, 0 => by simp [tail, G_zero]
  | d + 1, a, j + 1 => by
      rw [G_succ, show d + 1 + (j + 1) = (d + 1 + j) + 1 from rfl, rem_macaulayPow, rem_G (d + 1) a
        j]
      simp only [tail]
      rw [G_succ, show d + 1 + j = d + j + 1 by omega]

theorem

G_eq

L218 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow.PolyMaxSol.G_eq

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow
namespace PolyMaxSol

Lean source · statement

theorem G_eq (d a j : ℕ) : G d a j = (top d a + j).choose (d + j + 1) + tail d (rem d a) j

theorem

exists_poly_choose

L223 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow.PolyMaxSol.exists_poly_choose

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow
namespace PolyMaxSol

Lean source · statement

theorem exists_poly_choose (t d : ℕ) (ht : d ≤ t) :
    ∃ P : Polynomial ℚ, ∀ j : ℕ, (((t + j).choose (d + j + 1) : ℕ) : ℚ) = P.eval (j : ℚ)

theorem

exists_poly_tail_zero

L243 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow.PolyMaxSol.exists_poly_tail_zero

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow
namespace PolyMaxSol

Lean source · statement

theorem exists_poly_tail_zero (r : ℕ) : ∃ P : Polynomial ℚ, ∀ j : ℕ, ((tail 0 r j : ℕ) : ℚ) =
  P.eval (j : ℚ)

theorem

exists_poly_G

L247 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow.PolyMaxSol.exists_poly_G

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow
namespace PolyMaxSol

Lean source · full declaration

theorem exists_poly_G : ∀ (d a : ℕ), ∃ P : Polynomial ℚ, ∀ j : ℕ, ((G d a j : ℕ) : ℚ) = P.eval (j :
  ℚ)
  | 0, a => by
      obtain ⟨P, hP⟩ := exists_poly_choose (top 0 a) 0 (d_le_top 0 a)
      refine ⟨P, fun j => ?_⟩
      rw [G_eq]; simp only [tail, add_zero]; rw [← hP]
  | d + 1, a => by
      obtain ⟨P, hP⟩ := exists_poly_choose (top (d + 1) a) (d + 1) (d_le_top (d + 1) a)
      obtain ⟨Q, hQ⟩ := exists_poly_G d (rem (d + 1) a)
      refine ⟨P + Q, fun j => ?_⟩
      rw [G_eq, Polynomial.eval_add, ← hP, ← hQ]
      simp only [tail]; push_cast; rfl

theorem

exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow

L263 ↗

Nat.exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow
open PolyMaxSol in

Lean source · statement

theorem _root_.Nat.exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow
    (H : ℕ → ℕ) (D₀ : ℕ) (hD₀ : 1 ≤ D₀)
    (hH : ∀ e, D₀ ≤ e → H (e + 1) = Nat.macaulayPow e (H e)) :
    ∃ P : Polynomial ℚ, ∀ e, D₀ ≤ e → (H e : ℚ) = P.eval (e : ℚ)

Module documentation

Nat exists polynomial forall eval eq of forall eq macaulay Pow

Declarations