Module

Nat_macaulayPow_lt_macaulayPow_of_lt.lean

Nyll.AlgebraicCurves.Foundations.Algebra.Nat_macaulayPow_lt_macaulayPow_of_lt

15 declarations indexed from sourceView source ↗

Module documentation

Nat macaulay Pow lt macaulay Pow of lt

Imports5

Lean.Elab.Tactic.Omega
Mathlib.Data.Nat.Choose.Basic
Mathlib.Data.Nat.Find
Mathlib.Tactic.Ring.RingNF
Nyll.AlgebraicCurves.Foundations.Algebra.Nat_MacaulayPow

Imported by2

def

top

L33 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Nat_macaulayPow_lt_macaulayPow_of_lt.MacMono.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.Nat_macaulayPow_lt_macaulayPow_of_lt
namespace MacMono
open Nat

Lean source · statement

def top (d a : ℕ) : ℕ

theorem

macaulayPow_succ

L35 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Nat_macaulayPow_lt_macaulayPow_of_lt.MacMono.macaulayPow_succ

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Nat_macaulayPow_lt_macaulayPow_of_lt
namespace MacMono
open Nat

Lean source · statement

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

theorem

succ_le_choose

L40 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Nat_macaulayPow_lt_macaulayPow_of_lt.MacMono.succ_le_choose

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Nat_macaulayPow_lt_macaulayPow_of_lt
namespace MacMono
open Nat

Lean source · statement

theorem succ_le_choose (d j : ℕ) : j + 1 ≤ (j + d + 1).choose (d + 1)

theorem

le_bound

L50 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Nat_macaulayPow_lt_macaulayPow_of_lt.MacMono.le_bound

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Nat_macaulayPow_lt_macaulayPow_of_lt
namespace MacMono
open Nat

Lean source · statement

theorem le_bound {d a k : ℕ} (h : k.choose (d + 1) ≤ a) : k ≤ a + d + 1

theorem

choose_le_iff

L57 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Nat_macaulayPow_lt_macaulayPow_of_lt.MacMono.choose_le_iff

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Nat_macaulayPow_lt_macaulayPow_of_lt
namespace MacMono
open Nat

Lean source · statement

theorem choose_le_iff (d a k : ℕ) : k.choose (d + 1) ≤ a ↔ k ≤ top d a

theorem

top_choose_le

L66 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Nat_macaulayPow_lt_macaulayPow_of_lt.MacMono.top_choose_le

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Nat_macaulayPow_lt_macaulayPow_of_lt
namespace MacMono
open Nat

Lean source · statement

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

theorem

lt_succ_top_choose

L68 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Nat_macaulayPow_lt_macaulayPow_of_lt.MacMono.lt_succ_top_choose

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Nat_macaulayPow_lt_macaulayPow_of_lt
namespace MacMono
open Nat

Lean source · statement

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

theorem

top_eq

L73 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Nat_macaulayPow_lt_macaulayPow_of_lt.MacMono.top_eq

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Nat_macaulayPow_lt_macaulayPow_of_lt
namespace MacMono
open Nat

Lean source · statement

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

theorem

top_mono

L80 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Nat_macaulayPow_lt_macaulayPow_of_lt.MacMono.top_mono

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Nat_macaulayPow_lt_macaulayPow_of_lt
namespace MacMono
open Nat

Lean source · statement

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

theorem

macaulayPow_zero_right

L83 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Nat_macaulayPow_lt_macaulayPow_of_lt.MacMono.macaulayPow_zero_right

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Nat_macaulayPow_lt_macaulayPow_of_lt
namespace MacMono
open Nat

Lean source · statement

theorem macaulayPow_zero_right (d : ℕ) : macaulayPow d 0 = 0

theorem

macaulayPow_succ_choose

L90 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Nat_macaulayPow_lt_macaulayPow_of_lt.MacMono.macaulayPow_succ_choose

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Nat_macaulayPow_lt_macaulayPow_of_lt
namespace MacMono
open Nat

Lean source · statement

theorem macaulayPow_succ_choose (d K : ℕ) (hK : d ≤ K) :
    macaulayPow (d + 1) (K.choose (d + 1)) = (K + 1).choose (d + 2)

theorem

macaulayPow_one

L99 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Nat_macaulayPow_lt_macaulayPow_of_lt.MacMono.macaulayPow_one

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Nat_macaulayPow_lt_macaulayPow_of_lt
namespace MacMono
open Nat

Lean source · statement

theorem macaulayPow_one (a : ℕ) : macaulayPow 1 a = (a + 1).choose 2

theorem

strictMono_succ

L104 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Nat_macaulayPow_lt_macaulayPow_of_lt.MacMono.strictMono_succ

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Nat_macaulayPow_lt_macaulayPow_of_lt
namespace MacMono
open Nat

Lean source · statement

theorem strictMono_succ (d : ℕ) : ∀ a b : ℕ, a < b → macaulayPow (d + 1) a < macaulayPow (d + 1) b

theorem

macaulayPow_strictMono

L152 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Nat_macaulayPow_lt_macaulayPow_of_lt.MacMono.macaulayPow_strictMono

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Nat_macaulayPow_lt_macaulayPow_of_lt
namespace MacMono
open Nat

Lean source · statement

theorem macaulayPow_strictMono {d : ℕ} (hd : 1 ≤ d) {a b : ℕ} (h : a < b) :
    macaulayPow d a < macaulayPow d b

theorem

macaulayPow_lt_macaulayPow_of_lt

L159 ↗

Nat.macaulayPow_lt_macaulayPow_of_lt

Source context 2 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Nat_macaulayPow_lt_macaulayPow_of_lt

Lean source · statement

theorem _root_.Nat.macaulayPow_lt_macaulayPow_of_lt {d : ℕ} (hd : 1 ≤ d) {a b : ℕ} (h : a < b) :
    Nat.macaulayPow d a < Nat.macaulayPow d b

Module documentation

Nat macaulay Pow lt macaulay Pow of lt

Declarations