Module

Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow.lean

Nyll.AlgebraicCurves.Foundations.Algebra.Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow

42 declarations indexed from sourceView source ↗

Module documentation

Nat exists forall eq macaulay Pow of forall le macaulay Pow

Imports24

Batteries.Tactic.Init
Mathlib.Algebra.Group.Monoid
Mathlib.Algebra.Group.Nat.Defs
Mathlib.Algebra.Group.Semigroup
Mathlib.Data.DFinsupp.WellFounded
Mathlib.Data.Fintype.Basic
Mathlib.Data.Fintype.EquivFin
Mathlib.Data.Nat.Basic
Mathlib.Data.Nat.Choose.Basic
Mathlib.Data.Nat.Find
Mathlib.Data.Nat.Init
Mathlib.Data.Set.Operations
Mathlib.Order.Basic
Mathlib.Order.Defs.LinearOrder
Mathlib.Order.Defs.PartialOrder
Mathlib.Order.Fin.Basic
Mathlib.Order.Monotone.Basic
Mathlib.Order.Monotone.Defs
Mathlib.Order.PiLex
Mathlib.Order.RelClasses
Mathlib.Order.WellFounded
Mathlib.Tactic.Push
Mathlib.Tactic.Set
Nyll.AlgebraicCurves.Foundations.Algebra.Nat_MacaulayPow

Imported by4

def

top

L51 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow.GotzNum.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.Algebra.Proofs
namespace Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow
namespace GotzNum

Lean source · statement

def top (d a : ℕ) : ℕ

def

rem

L54 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow.GotzNum.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.Algebra.Proofs
namespace Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow
namespace GotzNum

Lean source · statement

def rem (d a : ℕ) : ℕ

theorem

macaulayPow_zero

L56 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow.GotzNum.macaulayPow_zero

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow
namespace GotzNum

Lean source · statement

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

theorem

macaulayPow_succ

L59 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow.GotzNum.macaulayPow_succ

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow
namespace GotzNum

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.Algebra.Proofs.Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow.GotzNum.sub_le_choose

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow
namespace GotzNum

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.Algebra.Proofs.Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow.GotzNum.choose_top_le

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow
namespace GotzNum

Lean source · statement

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

theorem

top_le

L77 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow.GotzNum.top_le

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow
namespace GotzNum

Lean source · statement

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

theorem

lt_choose_of_top_lt

L79 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow.GotzNum.lt_choose_of_top_lt

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow
namespace GotzNum

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.Algebra.Proofs.Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow.GotzNum.lt_choose_top_succ

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow
namespace GotzNum

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.Algebra.Proofs.Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow.GotzNum.top_eq_of

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow
namespace GotzNum

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.Algebra.Proofs.Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow.GotzNum.le_top_of_choose_le

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow
namespace GotzNum

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.Algebra.Proofs.Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow.GotzNum.top_lt_of_lt_choose

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow
namespace GotzNum

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.Algebra.Proofs.Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow.GotzNum.d_le_top

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow
namespace GotzNum

Lean source · statement

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

theorem

top_zero_right

L118 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow.GotzNum.top_zero_right

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow
namespace GotzNum

Lean source · statement

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

theorem

d_lt_top_of_pos

L121 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow.GotzNum.d_lt_top_of_pos

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow
namespace GotzNum

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.Algebra.Proofs.Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow.GotzNum.top_zero_left

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow
namespace GotzNum

Lean source · statement

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

theorem

rem_zero_left

L128 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow.GotzNum.rem_zero_left

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow
namespace GotzNum

Lean source · statement

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

theorem

rem_add_choose

L131 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow.GotzNum.rem_add_choose

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow
namespace GotzNum

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.Algebra.Proofs.Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow.GotzNum.rem_lt

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow
namespace GotzNum

Lean source · statement

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

theorem

top_mono

L139 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow.GotzNum.top_mono

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow
namespace GotzNum

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.Algebra.Proofs.Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow.GotzNum.macaulayPow_lt_choose

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow
namespace GotzNum

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.Algebra.Proofs.Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow.GotzNum.top_macaulayPow

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow
namespace GotzNum

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.Algebra.Proofs.Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow.GotzNum.rem_macaulayPow

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow
namespace GotzNum

Lean source · statement

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

def

vec

L179 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow.GotzNum.vec

Documentation

The sequence obtained recursively from the top indices and remainders of the binomial expansion.

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow
namespace GotzNum

Lean source · full declaration

def vec : ℕ → ℕ → ℕ → ℕ
  | 0, _, _ => 0
  | d + 1, a, 0 => top d a - d
  | d + 1, a, p + 1 => vec d (rem d a) p

theorem

vec_zero

L184 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow.GotzNum.vec_zero

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow
namespace GotzNum

Lean source · statement

theorem vec_zero (a p : ℕ) : vec 0 a p = 0

theorem

vec_succ_zero

L185 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow.GotzNum.vec_succ_zero

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow
namespace GotzNum

Lean source · statement

theorem vec_succ_zero (d a : ℕ) : vec (d + 1) a 0 = top d a - d

theorem

vec_succ_succ

L186 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow.GotzNum.vec_succ_succ

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow
namespace GotzNum

Lean source · statement

theorem vec_succ_succ (d a p : ℕ) : vec (d + 1) a (p + 1) = vec d (rem d a) p

theorem

vec_macaulayPow

L188 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow.GotzNum.vec_macaulayPow

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow
namespace GotzNum

Lean source · full declaration

theorem vec_macaulayPow : ∀ (d a : ℕ), vec (d + 1) (Nat.macaulayPow d a) = vec d a
  | 0, a => by
      funext p
      cases p with
      | zero => simp [macaulayPow_zero, top_zero_right]
      | succ p => simp
  | d + 1, a => by
      funext p
      cases p with
      | zero =>
          simp only [vec_succ_zero, top_macaulayPow]
          omega
      | succ p =>
          simp only [vec_succ_succ, rem_macaulayPow]
          rw [vec_macaulayPow d (rem d a)]

theorem

vec_eq_zero_of_le

L204 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow.GotzNum.vec_eq_zero_of_le

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow
namespace GotzNum

Lean source · full declaration

theorem vec_eq_zero_of_le : ∀ (d a p : ℕ), d ≤ p → vec d a p = 0
  | 0, _, _, _ => rfl
  | d + 1, a, 0, h => by omega
  | d + 1, a, p + 1, h => by
      simp only [vec_succ_succ]; exact vec_eq_zero_of_le d _ p (by omega)

theorem

vec_succ_le

L210 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow.GotzNum.vec_succ_le

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow
namespace GotzNum

Lean source · full declaration

theorem vec_succ_le : ∀ (d a p : ℕ), vec d a (p + 1) ≤ vec d a p
  | 0, _, _ => by simp
  | d + 1, a, p + 1 => by
      simp only [vec_succ_succ]; exact vec_succ_le d _ p
  | 0 + 1, a, 0 => by simp
  | (e + 1) + 1, a, 0 => by
      simp only [vec_succ_succ, vec_succ_zero]
      have h := rem_lt (e + 1) a
      have := top_lt_of_lt_choose e (rem (e + 1) a) (top (e + 1) a) h
      omega

theorem

vec_antitone

L221 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow.GotzNum.vec_antitone

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow
namespace GotzNum

Lean source · statement

theorem vec_antitone (d a : ℕ) : Antitone (vec d a)

theorem

lex_vec_of_lt

L224 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow.GotzNum.lex_vec_of_lt

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow
namespace GotzNum

Lean source · full declaration

theorem lex_vec_of_lt : ∀ (d : ℕ) {a b : ℕ}, a < b →
    Pi.Lex (· < ·) (fun {_} => (· < ·)) (vec (d + 1) a) (vec (d + 1) b)
  | 0, a, b, h => ⟨0, fun j hj => (Nat.not_lt_zero j hj).elim, by simpa [top_zero_left] using h⟩
  | d + 1, a, b, h => by
      rcases lt_trichotomy (top (d + 1) a) (top (d + 1) b) with ht | ht | ht
      · refine ⟨0, fun j hj => (Nat.not_lt_zero j hj).elim, ?_⟩
        have := d_le_top (d + 1) a
        simp only [vec_succ_zero]
        omega
      · have hrem : rem (d + 1) a < rem (d + 1) b := by
          have ha := rem_add_choose (d + 1) a
          have hb := rem_add_choose (d + 1) b
          rw [ht] at ha; omega
        obtain ⟨i, hi, hlt⟩ := lex_vec_of_lt d hrem
        refine ⟨i + 1, fun j hj => ?_, by simpa using hlt⟩
        cases j with
        | zero => simp [ht]
        | succ j => simpa using hi j (by omega)
      · exfalso
        have h1 := lt_choose_top_succ (d + 1) b
        have h2 : (top (d + 1) b + 1).choose (d + 1 + 1) ≤ (top (d + 1) a).choose (d + 1 + 1) :=
          Nat.choose_le_choose _ ht
        have h3 := choose_top_le (d + 1) a
        omega

theorem

not_lex_self

L249 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow.GotzNum.not_lex_self

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow
namespace GotzNum

Lean source · full declaration

theorem not_lex_self (x : ℕ → ℕ) : ¬ Pi.Lex (· < ·) (fun {_} => (· < ·)) x x := by
  rintro ⟨i, -, h⟩; exact lt_irrefl _ h

theorem

vec_injective

L252 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow.GotzNum.vec_injective

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow
namespace GotzNum

Lean source · statement

theorem vec_injective (d : ℕ) {a b : ℕ} (h : vec (d + 1) a = vec (d + 1) b) : a = b

theorem

eq_or_lex_of_le

L258 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow.GotzNum.eq_or_lex_of_le

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow
namespace GotzNum

Lean source · full declaration

theorem eq_or_lex_of_le (d : ℕ) {a b : ℕ} (h : a ≤ b) :
    vec (d + 1) a = vec (d + 1) b ∨
      Pi.Lex (· < ·) (fun {_} => (· < ·)) (vec (d + 1) a) (vec (d + 1) b) := by
  rcases h.eq_or_lt with h | h
  · exact Or.inl (by rw [h])
  · exact Or.inr (lex_vec_of_lt d h)

theorem

head_le_of_eq_or_lex

L265 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow.GotzNum.head_le_of_eq_or_lex

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow
namespace GotzNum

Lean source · full declaration

theorem head_le_of_eq_or_lex {x y : ℕ → ℕ}
    (h : x = y ∨ Pi.Lex (· < ·) (fun {_} => (· < ·)) x y) : x 0 ≤ y 0 := by
  rcases h with h | ⟨i, hi, hlt⟩
  · rw [h]
  · cases i with
    | zero => exact hlt.le
    | succ i => exact (hi 0 (by omega)).le

def

cnt

L276 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow.GotzNum.cnt

Documentation

The first index where the sequence falls below the threshold, or zero if there is no such index.

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow
namespace GotzNum
open Classical in

Lean source · statement

def cnt (t : ℕ) (x : ℕ → ℕ) : ℕ

theorem

cnt_eq

L279 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow.GotzNum.cnt_eq

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow
namespace GotzNum

Lean source · statement

theorem cnt_eq (t : ℕ) (x : ℕ → ℕ) (h : ∃ p, x p < t) : cnt t x = Nat.find h

def

cv

L283 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow.GotzNum.cv

Documentation

The finite vector of threshold-crossing indices for descending thresholds.

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow
namespace GotzNum

Lean source · statement

def cv (M : ℕ) (x : ℕ → ℕ) : Fin M → ℕ

theorem

cv_lex

L285 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow.GotzNum.cv_lex

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow
namespace GotzNum

Lean source · full declaration

theorem cv_lex {M : ℕ} {x y : ℕ → ℕ} (hy : Antitone y) (hyM : y 0 ≤ M) (hy0 : ∃ q, y q = 0)
    (h : Pi.Lex (· < ·) (fun {_} => (· < ·)) x y) :
    Pi.Lex (· < ·) (fun {_} => (· < ·)) (cv M x) (cv M y) := by
  obtain ⟨p, hp, hlt⟩ := h
  set t := y p with ht
  have ht1 : 1 ≤ t := by simp only [ht]; omega
  have htM : t ≤ M := (hy (Nat.zero_le p)).trans hyM
  refine ⟨⟨M - t, by omega⟩, fun j hj => ?_, ?_⟩
  · have hj' : (j : ℕ) < M - t := hj
    set t' := M - (j : ℕ) with ht'
    have htt' : t < t' := by omega
    have hey : ∃ q, y q < t' := ⟨p, by omega⟩
    change cnt t' x = cnt t' y
    rw [cnt_eq t' y hey]
    set c := Nat.find hey with hc
    have hcspec : y c < t' := Nat.find_spec hey
    have hcmin : ∀ q < c, ¬ y q < t' := fun q hq => Nat.find_min hey hq
    have hcp : c ≤ p := Nat.find_min' hey (show y p < t' by omega)
    have hex : ∃ q, x q < t' := ⟨c, by
      rcases hcp.eq_or_lt with h | h
      · rw [h]; omega
      · rw [hp c h]; exact hcspec⟩
    rw [cnt_eq t' x hex, Nat.find_eq_iff]
    refine ⟨?_, fun q hq => ?_⟩
    · rcases hcp.eq_or_lt with h | h
      · rw [h]; omega
      · rw [hp c h]; exact hcspec
    · rw [hp q (by omega)]; exact hcmin q hq
  · change cnt (M - (M - t)) x < cnt (M - (M - t)) y
    have hMt : M - (M - t) = t := by omega
    rw [hMt]
    have hex : ∃ q, x q < t := ⟨p, hlt⟩
    have hey : ∃ q, y q < t := by obtain ⟨q, hq⟩ := hy0; exact ⟨q, by omega⟩
    rw [cnt_eq t x hex, cnt_eq t y hey]
    have h1 : Nat.find hex = p := by
      rw [Nat.find_eq_iff]
      refine ⟨hlt, fun q hq => ?_⟩
      rw [hp q hq]
      have := hy hq.le
      omega
    rw [h1, Nat.lt_find_iff]
    intro q hq
    have := hy hq
    omega

theorem

eventually_eq

L330 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow.GotzNum.eventually_eq

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow
namespace GotzNum

Lean source · statement

theorem eventually_eq (H : ℕ → ℕ) (d₀ : ℕ)
    (hH : ∀ d, d₀ ≤ d → H (d + 1) ≤ Nat.macaulayPow d (H d)) :
    ∃ D₀ : ℕ, ∀ e, D₀ ≤ e → H (e + 1) = Nat.macaulayPow e (H e)

theorem

exists_forall_eq_macaulayPow_of_forall_le_macaulayPow

L379 ↗

Nat.exists_forall_eq_macaulayPow_of_forall_le_macaulayPow

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow
attribute [local simp] GotzNum.vec_zero
attribute [local simp] GotzNum.vec_succ_zero
attribute [local simp] GotzNum.vec_succ_succ
open GotzNum in

Lean source · statement

theorem _root_.Nat.exists_forall_eq_macaulayPow_of_forall_le_macaulayPow
    (H : ℕ → ℕ) (d₀ : ℕ) (_hd₀ : 1 ≤ d₀)
    (hH : ∀ d, d₀ ≤ d → H (d + 1) ≤ Nat.macaulayPow d (H d)) :
    ∃ D₀ : ℕ, ∀ e, D₀ ≤ e → H (e + 1) = Nat.macaulayPow e (H e)

Module documentation

Nat exists forall eq macaulay Pow of forall le macaulay Pow

Declarations