Numerical polynomials and mixed finite differences

This file supplies an algebraic finite-difference API for integer-valued functions on integer lattices. A point of the lattice is a function ι → ℤ, and a numerical function is simply a function (ι → ℤ) → ℤ. No scheme, sheaf, or line-bundle vocabulary enters this root; geometric polynomiality theorems such as Snapper's theorem consume it from algebraic geometry.

Upstream audit

Mathlib's Mathlib.Algebra.Group.ForwardDiff already provides the one-direction operator fwdDiff, its iterates, the Gregory--Newton formula, additivity, and the expected vanishing theorems for ordinary polynomials. We reuse that operator rather than defining a competing univariate theory.

jjaassoonn/DimensionTheory contains substantial theory of univariate integer-valued and Hilbert polynomials, including binomial-polynomial coefficient extraction. At the time of this audit it does not provide arbitrary-direction mixed differences, is pinned to a different Mathlib commit, and would add a large dependency for an API which is otherwise elementary. Consequently DerivedAlgGeo uses it as design precedent but does not depend on it. The definitions below form the small multivariable layer missing from Mathlib and specialize back to Mathlib's fwdDiff in one variable.

Main definitions

• Lattice ι is the exponent lattice ι → ℤ.
• mixedDifference directions f successively applies forward differences in every direction.
• DegreeLE n f means that every (n + 1)-fold mixed difference vanishes.
• coefficient directions f evaluates a mixed difference at the origin; in top degree this is a symmetric multilinear function of the directions.
• surfacePairing bundles the degree-two specialization as a symmetric bilinear form.

@[reducible, inline]

abbrev NumericalPolynomial.Lattice (ι : Type u_1) : Type u_1

The exponent lattice for a family indexed by ι. For ι = Fin r, this is ℤ^r.

Equations

• NumericalPolynomial.Lattice ι = (ι → ℤ)

@[reducible, inline]

abbrev NumericalPolynomial.NumericalFunction (ι : Type u_1) : Type u_1

An integer-valued function on an exponent lattice.

Equations

• NumericalPolynomial.NumericalFunction ι = (NumericalPolynomial.Lattice ι → ℤ)

def NumericalPolynomial.difference {ι : Type u_1} (v : Lattice ι) (f : NumericalFunction ι) : NumericalFunction ι

The forward difference of f in the lattice direction v.

Equations

• NumericalPolynomial.difference v f = fwdDiff v f

@[simp]

theorem NumericalPolynomial.difference_apply {ι : Type u_1} (v : Lattice ι) (f : NumericalFunction ι) (x : Lattice ι) : difference v f x = f (x + v) - f x

@[simp]

theorem NumericalPolynomial.difference_zero_direction {ι : Type u_1} (f : NumericalFunction ι) : difference 0 f = 0

@[simp]

theorem NumericalPolynomial.difference_zero_function {ι : Type u_1} (v : Lattice ι) : difference v 0 = 0

@[simp]

theorem NumericalPolynomial.difference_add_function {ι : Type u_1} (v : Lattice ι) (f g : NumericalFunction ι) : difference v (f + g) = difference v f + difference v g

theorem NumericalPolynomial.difference_comm {ι : Type u_1} (v w : Lattice ι) (f : NumericalFunction ι) : difference v (difference w f) = difference w (difference v f)

Forward differences in two lattice directions commute.

theorem NumericalPolynomial.difference_add_direction {ι : Type u_1} (v w : Lattice ι) (f : NumericalFunction ι) : difference (v + w) f = difference v f + difference w f + difference v (difference w f)

Splitting a direction introduces one second-order correction term.

def NumericalPolynomial.coordinateDirection {ι : Type u_1} [DecidableEq ι] (i : ι) : Lattice ι

The positive unit vector in coordinate i.

Equations

• NumericalPolynomial.coordinateDirection i = Pi.single i 1

def NumericalPolynomial.coordinateDifference {ι : Type u_1} [DecidableEq ι] (i : ι) (f : NumericalFunction ι) : NumericalFunction ι

The forward difference in coordinate i.

Equations

• NumericalPolynomial.coordinateDifference i f = NumericalPolynomial.difference (NumericalPolynomial.coordinateDirection i) f

@[simp]

theorem NumericalPolynomial.coordinateDifference_apply {ι : Type u_1} [DecidableEq ι] (i : ι) (f : NumericalFunction ι) (x : Lattice ι) : coordinateDifference i f x = f (x + coordinateDirection i) - f x

def NumericalPolynomial.mixedDifference {ι : Type u_1} : List (Lattice ι) → NumericalFunction ι → NumericalFunction ι

Successive forward differences in the listed directions.

Equations

• NumericalPolynomial.mixedDifference [] x✝ = x✝
• NumericalPolynomial.mixedDifference (v :: directions) x✝ = NumericalPolynomial.difference v (NumericalPolynomial.mixedDifference directions x✝)

@[simp]

theorem NumericalPolynomial.mixedDifference_nil {ι : Type u_1} (f : NumericalFunction ι) : mixedDifference [] f = f

@[simp]

theorem NumericalPolynomial.mixedDifference_cons {ι : Type u_1} (v : Lattice ι) (directions : List (Lattice ι)) (f : NumericalFunction ι) : mixedDifference (v :: directions) f = difference v (mixedDifference directions f)

@[simp]

theorem NumericalPolynomial.mixedDifference_zero {ι : Type u_1} (directions : List (Lattice ι)) : mixedDifference directions 0 = 0

@[simp]

theorem NumericalPolynomial.mixedDifference_add {ι : Type u_1} (directions : List (Lattice ι)) (f g : NumericalFunction ι) : mixedDifference directions (f + g) = mixedDifference directions f + mixedDifference directions g

theorem NumericalPolynomial.mixedDifference_difference {ι : Type u_1} (directions : List (Lattice ι)) (v : Lattice ι) (f : NumericalFunction ι) : mixedDifference directions (difference v f) = difference v (mixedDifference directions f)

Applying one more difference can be moved past any list of mixed differences.

theorem NumericalPolynomial.mixedDifference_eq_of_perm {ι : Type u_1} {directions directions' : List (Lattice ι)} (h : directions.Perm directions') (f : NumericalFunction ι) : mixedDifference directions f = mixedDifference directions' f

A mixed difference depends only on the multiset of its directions.

def NumericalPolynomial.DegreeLE {ι : Type u_1} (n : ℕ) (f : NumericalFunction ι) : Prop

A numerical function has degree at most n when all (n + 1)-fold mixed differences vanish.

This is the Eilenberg--Mac Lane finite-difference characterization in exactly the form used by Snapper's theorem: the directions are arbitrary lattice vectors, not merely coordinate vectors.

Equations

• NumericalPolynomial.DegreeLE n f = ∀ (directions : List (NumericalPolynomial.Lattice ι)), directions.length = n + 1 → NumericalPolynomial.mixedDifference directions f = 0

theorem NumericalPolynomial.degreeLE_iff_vanishing {ι : Type u_1} (n : ℕ) (f : NumericalFunction ι) : DegreeLE n f ↔ ∀ (directions : List (Lattice ι)), directions.length = n + 1 → mixedDifference directions f = 0

theorem NumericalPolynomial.degreeLE_iff_fin {ι : Type u_1} (n : ℕ) (f : NumericalFunction ι) : DegreeLE n f ↔ ∀ (directions : Fin (n + 1) → Lattice ι), mixedDifference (List.ofFn directions) f = 0

Equivalent fixed-arity form of the degree criterion. This is convenient when a later construction already presents its directions as an (n + 1)-tuple.

@[simp]

theorem NumericalPolynomial.degreeLE_zero {ι : Type u_1} (n : ℕ) : DegreeLE n 0

theorem NumericalPolynomial.DegreeLE.add {ι : Type u_1} {n : ℕ} {f g : NumericalFunction ι} (hf : DegreeLE n f) (hg : DegreeLE n g) : DegreeLE n (f + g)

theorem NumericalPolynomial.DegreeLE.succ {ι : Type u_1} {n : ℕ} {f : NumericalFunction ι} (hf : DegreeLE n f) : DegreeLE (n + 1) f

A function of degree at most n also has degree at most n + 1.

theorem NumericalPolynomial.DegreeLE.mono {ι : Type u_1} {n m : ℕ} {f : NumericalFunction ι} (hf : DegreeLE n f) (hnm : n ≤ m) : DegreeLE m f

Monotonicity of the degree bound.

theorem NumericalPolynomial.DegreeLE.difference {ι : Type u_1} {n : ℕ} {f : NumericalFunction ι} (hf : DegreeLE (n + 1) f) (v : Lattice ι) : DegreeLE n (NumericalPolynomial.difference v f)

Taking a finite difference lowers a positive degree bound by one.

def NumericalPolynomial.coefficient {ι : Type u_1} (directions : List (Lattice ι)) (f : NumericalFunction ι) : ℤ

The mixed finite-difference coefficient attached to a list of directions.

Equations

• NumericalPolynomial.coefficient directions f = NumericalPolynomial.mixedDifference directions f 0

@[simp]

theorem NumericalPolynomial.coefficient_nil {ι : Type u_1} (f : NumericalFunction ι) : coefficient [] f = f 0

@[simp]

theorem NumericalPolynomial.coefficient_zero {ι : Type u_1} (directions : List (Lattice ι)) : coefficient directions 0 = 0

theorem NumericalPolynomial.coefficient_add {ι : Type u_1} (directions : List (Lattice ι)) (f g : NumericalFunction ι) : coefficient directions (f + g) = coefficient directions f + coefficient directions g

theorem NumericalPolynomial.coefficient_eq_of_perm {ι : Type u_1} {directions directions' : List (Lattice ι)} (h : directions.Perm directions') (f : NumericalFunction ι) : coefficient directions f = coefficient directions' f

Coefficient extraction is symmetric in the chosen directions.

def NumericalPolynomial.topCoefficient {ι : Type u_1} {n : ℕ} (directions : Fin n → Lattice ι) (f : NumericalFunction ι) : ℤ

Coefficient extraction with n explicitly indexed directions.

Equations

• NumericalPolynomial.topCoefficient directions f = NumericalPolynomial.coefficient (List.ofFn directions) f

theorem NumericalPolynomial.topCoefficient_comp_perm {ι : Type u_1} {n : ℕ} (directions : Fin n → Lattice ι) (σ : Equiv.Perm (Fin n)) (f : NumericalFunction ι) : topCoefficient (directions ∘ ⇑σ) f = topCoefficient directions f

topCoefficient is invariant under every permutation of its n inputs.

noncomputable def NumericalPolynomial.coordinateDirections {ι : Type u_1} [Fintype ι] [DecidableEq ι] (powers : ι → ℕ) : List (Lattice ι)

The coordinate directions prescribed by a multi-index. The internal order chosen by Finset.toList is immaterial by coefficient_eq_of_perm.

Equations

• NumericalPolynomial.coordinateDirections powers = List.flatMap (fun (i : ι) => List.replicate (powers i) (NumericalPolynomial.coordinateDirection i)) Finset.univ.toList

@[simp]

theorem NumericalPolynomial.coordinateDirections_length {ι : Type u_1} [Fintype ι] [DecidableEq ι] (powers : ι → ℕ) : (coordinateDirections powers).length = ∑ i : ι, powers i

noncomputable def NumericalPolynomial.newtonCoefficient {ι : Type u_1} [Fintype ι] [DecidableEq ι] (powers : ι → ℕ) (f : NumericalFunction ι) : ℤ

The multivariable Newton coefficient indexed by coordinate multiplicities.

Equations

• NumericalPolynomial.newtonCoefficient powers f = NumericalPolynomial.coefficient (NumericalPolynomial.coordinateDirections powers) f

@[simp]

theorem NumericalPolynomial.newtonCoefficient_zero_index {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : NumericalFunction ι) : newtonCoefficient (fun (x : ι) => 0) f = f 0

theorem NumericalPolynomial.mixedDifference_eq_coefficient_of_degreeLE {ι : Type u_1} {n : ℕ} {f : NumericalFunction ι} (hf : DegreeLE n f) (directions : List (Lattice ι)) (hlength : directions.length = n) (x : Lattice ι) : mixedDifference directions f x = coefficient directions f

An n-fold mixed difference of a degree-≤ n function is constant, so evaluating it at the origin loses no information.

theorem NumericalPolynomial.coefficient_cons_add {ι : Type u_1} {f : NumericalFunction ι} (directions : List (Lattice ι)) (v w : Lattice ι) (hf : DegreeLE (directions.length + 1) f) : coefficient ((v + w) :: directions) f = coefficient (v :: directions) f + coefficient (w :: directions) f

Additivity of a top mixed coefficient in its first direction. The correction term in difference_add_direction vanishes because it has one direction too many.

theorem NumericalPolynomial.coefficient_middle_add {ι : Type u_1} {f : NumericalFunction ι} (before after : List (Lattice ι)) (v w : Lattice ι) (hf : DegreeLE (before.length + after.length + 1) f) : coefficient (before ++ (v + w) :: after) f = coefficient (before ++ v :: after) f + coefficient (before ++ w :: after) f

Additivity of a top mixed coefficient in an arbitrary direction slot.

def NumericalPolynomial.coefficientAddHom {ι : Type u_1} {f : NumericalFunction ι} (before after : List (Lattice ι)) (hf : DegreeLE (before.length + after.length + 1) f) : Lattice ι →+ ℤ

A top mixed coefficient, with all but one direction fixed, as an additive homomorphism.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem NumericalPolynomial.coefficientAddHom_apply {ι : Type u_1} {f : NumericalFunction ι} (before after : List (Lattice ι)) (hf : DegreeLE (before.length + after.length + 1) f) (v : Lattice ι) : (coefficientAddHom before after hf) v = coefficient (before ++ v :: after) f

theorem NumericalPolynomial.coefficient_middle_zsmul {ι : Type u_1} {f : NumericalFunction ι} (before after : List (Lattice ι)) (c : ℤ) (v : Lattice ι) (hf : DegreeLE (before.length + after.length + 1) f) : coefficient (before ++ c • v :: after) f = c • coefficient (before ++ v :: after) f

Integer homogeneity in every slot; together with coefficient_middle_add, this is multilinearity of the top mixed difference.

One-variable specialization

def NumericalPolynomial.oneVariablePoint (x : ℤ) : Lattice (Fin 1)

Embed an integer as a point of the rank-one lattice.

Equations

• NumericalPolynomial.oneVariablePoint x x✝ = x

def NumericalPolynomial.oneVariable (f : ℤ → ℤ) : NumericalFunction (Fin 1)

Regard an ordinary integer-valued function as a function on the rank-one lattice.

Equations

• NumericalPolynomial.oneVariable f x = f (x 0)

def NumericalPolynomial.oneVariableDirection : Lattice (Fin 1)

The positive unit direction in the rank-one lattice.

Equations

• NumericalPolynomial.oneVariableDirection = NumericalPolynomial.oneVariablePoint 1

theorem NumericalPolynomial.mixedDifference_oneVariable (f : ℤ → ℤ) (n : ℕ) (x : ℤ) : mixedDifference (List.replicate n oneVariableDirection) (oneVariable f) (oneVariablePoint x) = (fwdDiff 1)^[n] f x

Repeated mixed differences in the unit direction agree with Mathlib's iterated fwdDiff.

theorem NumericalPolynomial.oneVariable_fwdDiff_vanishes {f : ℤ → ℤ} {n : ℕ} (hf : DegreeLE n (oneVariable f)) : (fwdDiff 1)^[n + 1] f = 0

The general degree predicate implies the familiar one-variable (n + 1)-st difference criterion.

theorem NumericalPolynomial.coefficient_oneVariable (f : ℤ → ℤ) (n : ℕ) : coefficient (List.replicate n oneVariableDirection) (oneVariable f) = (fwdDiff 1)^[n] f 0

In one variable, generic coefficient extraction is the usual Newton coefficient.

Surface specialization

noncomputable def NumericalPolynomial.surfacePairing {ι : Type u_1} (f : NumericalFunction ι) (hf : DegreeLE 2 f) : Lattice ι →ₗ[ℤ] Lattice ι →ₗ[ℤ] ℤ

The degree-two top mixed difference, bundled as a bilinear form over ℤ.

Equations

• NumericalPolynomial.surfacePairing f hf = { toFun := fun (v : NumericalPolynomial.Lattice ι) => (NumericalPolynomial.coefficientAddHom [v] [] ⋯).toIntLinearMap, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem NumericalPolynomial.surfacePairing_apply {ι : Type u_1} (f : NumericalFunction ι) (hf : DegreeLE 2 f) (v w : Lattice ι) : ((surfacePairing f hf) v) w = coefficient [v, w] f

theorem NumericalPolynomial.surfacePairing_symm {ι : Type u_1} (f : NumericalFunction ι) (hf : DegreeLE 2 f) (v w : Lattice ι) : ((surfacePairing f hf) v) w = ((surfacePairing f hf) w) v

The surface pairing is symmetric.