Reservoir

Weights

Formalization in Lean4 of some results in Minimization of hypersurfaces by A.-S. Elsenhans and myself.

Contents

The paper introduces the notion of a weight on forms of degree in variables, which is simply an -tuple of natural numbers. We index the entries from to . See Weight.

We can then compare weights in the following way. We first define to be the Set of -tuples of natural numbers whose sum is (Weight.testvecs n d). Then to a weight , we associate the map given by sending to (where denotes the sum of the entries of ). See Weight.f.

Then we say that a weight dominates another weight if point-wise. In this file, we write w ≤d w' for this relation. ≤d is a pre-order on the set of weights, but not a (partial) order. For example, a weight and dominate each other for each natural number . We can therefore restrict to weights whose minimal entry is zero.

We say that a weight that is (weakly) increasing and such that is normalized (Weight.normalized). We show that if a normalized weight dominates some weight , then it also dominates the increasing permutation of (Weight.dom_of_dom_perm). So up to permutations, it suffices to consider only normalized weights.

We say that a set of normalized weights is complete if every normalized weight is dominated by an element of (Weight.complete_set). We say that a complete set of weights is minimal if it is minimal with respect to inclusion among complete sets (Weight.minimal_complete_set). This is equivalent to saying that when and are in and dominates , then .

The first main result formalized here is that there is a unique minimal complete set of weights, which is given by the set Weight.M n d of all normalized weights that are minimal elements with respect to domination within the set of all normalized weights. This is Proposition 3.13 in the paper. See Weight.M_is_minimal and Weight.M_is_unique.

We show in addition that the entries of nonzero elements of M n d are coprime (Weight.gcd_eq_one_of_in_M) and that M n 1 consists of the single element (Weight.w1_unique).

The second main result is a proof of Theorem 1.6 in the paper, which says that in the case , the weights in a minimal complete set of normalized weights have entries bounded by the degree . See Weight.dom_by_max_le_d and Weight.theorem_1_6.