Magnitude conjecture

QuotientSubmoduleEquidistribution.ConvexGeometry.LevelPolynomial

Level generating polynomials #

For a closure operator on a finite ground type, the manuscript records the number of closed sets at each cardinality level in a polynomial. This file defines that invariant independently of the later module-theoretic instantiations.

source
noncomputable def QuotientSubmoduleEquidistribution.SetClosure.levelCount {E : Type u_1} [Finite E] (c : SetClosure E) (n : ℕ) :
ℕ

The number of closed sets having cardinality n.

Instances For
    source
    noncomputable def QuotientSubmoduleEquidistribution.SetClosure.levelPolynomial {E : Type u_1} [Finite E] (c : SetClosure E) :
    Polynomial ℕ

    The cardinality generating polynomial of the closed-set lattice.

    Instances For
      source
      @[simp]
      theorem QuotientSubmoduleEquidistribution.SetClosure.levelPolynomial_coeff {E : Type u_1} [Finite E] (c : SetClosure E) (n : ℕ) :
      c.levelPolynomial.coeff n = c.levelCount n

      The coefficient of X ^ n is the number of closed sets at level n.

      source
      @[simp]
      theorem QuotientSubmoduleEquidistribution.SetClosure.levelPolynomial_eval_one {E : Type u_1} [Finite E] (c : SetClosure E) :
      Polynomial.eval 1 c.levelPolynomial = Nat.card (ClosureOperator.Closeds c)

      Evaluating the level polynomial at one counts all closed sets.

      source
      theorem QuotientSubmoduleEquidistribution.SetClosure.levelPolynomial_eq_iff {E : Type u_1} [Finite E] (c d : SetClosure E) :
      c.levelPolynomial = d.levelPolynomial ↔ ∀ (n : ℕ), c.levelCount n = d.levelCount n

      Equality of level polynomials is equivalent to equality at every cardinality level.

      source
      theorem QuotientSubmoduleEquidistribution.SetClosure.levelPolynomial_eq_sum_equiv {E : Type u_1} [Finite E] {W : Type u_2} [Fintype W] (c : SetClosure E) (e : W ≃ ClosureOperator.Closeds c) :
      c.levelPolynomial = ∑ w : W, Polynomial.X ^ (↑(e w)).ncard

      Enumerating the closed sets by a finite type rewrites the level polynomial as the corresponding cardinality sum.

      source
      theorem QuotientSubmoduleEquidistribution.SetClosure.levelPolynomial_eq_sum_stat {E : Type u_1} [Finite E] {W : Type u_2} [Fintype W] (c : SetClosure E) (e : W ≃ ClosureOperator.Closeds c) (stat : W → ℕ) (hstat : ∀ (w : W), (↑(e w)).ncard = stat w) :
      c.levelPolynomial = ∑ w : W, Polynomial.X ^ stat w

      If the enumerating parameter carries an explicit size statistic, that statistic is the exponent in the level polynomial.

      source
      theorem QuotientSubmoduleEquidistribution.SetClosure.levelCount_eq_zero_of_card_lt {E : Type u_1} [Finite E] (c : SetClosure E) {n : ℕ} (hn : Nat.card E < n) :
      c.levelCount n = 0

      No subset of a finite ground type can occur above its cardinality.

      source
      theorem QuotientSubmoduleEquidistribution.SetClosure.levelPolynomial_eq_of_bottom_top_four {E : Type u_1} [Finite E] (c d : SetClosure E) (hcard : Nat.card E ≤ 9) (hbottom : ∀ i ≤ 4, c.levelCount i = d.levelCount i) (htop : ∀ i ≤ 4, c.levelCount (Nat.card E - i) = d.levelCount (Nat.card E - i)) :
      c.levelPolynomial = d.levelPolynomial

      Equality through the bottom and top four levels determines the entire level polynomial when the ground set has at most nine elements.