ExponentCardinality.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Cardinalities of homogeneous and bihomogeneous exponent sets

theorem OAI.Problem335.card_homogeneous_exponents line 15

Source documentation

Stars and bars for finitely supported natural exponent vectors.

theorem card_homogeneous_exponents (σ : Type*) [Fintype σ] (a : ℕ) :
    Nat.card {d : σ →₀ ℕ // d.sum (fun _ n => n) = a} =
      (Fintype.card σ).multichoose a := by
…

theorem OAI.Problem335.card_homogeneous_functions line 24

Source documentation

Stars and bars for ordinary natural exponent vectors on a finite type.

theorem card_homogeneous_functions (σ : Type*) [Fintype σ] (a : ℕ) :
    Nat.card {d : σ → ℕ // ∑ x, d x = a} =
      (Fintype.card σ).multichoose a := by
…

lemma OAI.Problem335.bidegreeWeight_fst_sum line 31
lemma OAI.Problem335.bidegreeWeight_snd_sum line 45

def OAI.Problem335.bidegreeExponentsEquiv line 60

Source documentation

Split a bihomogeneous monomial into its two independent exponent vectors.

def bidegreeExponentsEquiv [Fintype σ] (isV : σ → Bool) (a b : ℕ) :
    {d : σ →₀ ℕ // Finsupp.weight (bidegreeWeight isV) d = (a, b)} ≃
      {d : {x // isV x = true} → ℕ // ∑ x, d x = a} ×
      {d : {x // ¬ isV x = true} → ℕ // ∑ x, d x = b} := by
…

Mentions: OAI.Problem335.bidegreeWeight

theorem OAI.Problem335.card_bidegree_exponents line 81

Source documentation

Bihomogeneous monomials are counted by the product of two stars-and-bars numbers; the variable sets may be empty.

theorem card_bidegree_exponents [Fintype σ] (isV : σ → Bool) (a b : ℕ) :
    Nat.card {d : σ →₀ ℕ // Finsupp.weight (bidegreeWeight isV) d = (a, b)} =
      (Fintype.card {x // isV x = true}).multichoose a *
        (Fintype.card {x // ¬ isV x = true}).multichoose b := by
…

Mentions: OAI.Problem335.bidegreeWeight

theorem OAI.Problem335.card_bidegree_exponents_bool line 90

Source documentation

The same count with the explicit false Boolean fiber.

theorem card_bidegree_exponents_bool [Fintype σ] (isV : σ → Bool) (a b : ℕ) :
    Nat.card {d : σ →₀ ℕ // Finsupp.weight (bidegreeWeight isV) d = (a, b)} =
      (Fintype.card {x // isV x = true}).multichoose a *
        (Fintype.card {x // isV x = false}).multichoose b := by
…

Mentions: OAI.Problem335.bidegreeWeight

theorem OAI.Problem335.card_layer_variables line 97

Source documentation

Each selected matrix layer contributes all n² ambient variables.

theorem card_layer_variables {n : ℕ} (s : Finset (Fin n)) :
    Fintype.card {x : Fin n × Fin n × Fin n // x.1 ∈ s} = s.card * n ^ 2 := by
…

theorem OAI.Problem335.card_complement_layer_variables line 105

Source documentation

The complementary group has the expected number of ambient variables.

theorem card_complement_layer_variables {n : ℕ} (s : Finset (Fin n)) :
    Fintype.card {x : Fin n × Fin n × Fin n // x.1 ∉ s} =
      (n - s.card) * n ^ 2 := by
…

theorem OAI.Problem335.card_layer_bidegree_exponents line 114
Source documentation
The exact dimension index count for a partition by complete matrix layers. In particular, inactive endpoint coordinates remain part of both stars-and-bars counts, as required in the occupation-moment argument.
```
theorem card_layer_bidegree_exponents {n : ℕ} (s : Finset (Fin n)) (a b : ℕ) :
    Nat.card {d : (Fin n × Fin n × Fin n) →₀ ℕ //
      Finsupp.weight (bidegreeWeight (fun x => decide (x.1 ∈ s))) d = (a, b)} =
      (s.card * n ^ 2).multichoose a *
        ((n - s.card) * n ^ 2).multichoose b := by
…
```
Mentions: OAI.Problem335.bidegreeWeight
abbrev OAI.Problem335.homogeneousFunctionsFintype line 126
Source documentation
An explicit finite enumeration for a weak-composition function type. This is not installed globally, so consumers may choose their preferred enumeration.
```
abbrev homogeneousFunctionsFintype (σ : Type*) [Fintype σ] (a : ℕ) :
    Fintype {d : σ → ℕ // ∑ x, d x = a} := by
…
```
def OAI.Problem335.homogeneousFunctionsEquivAntidiag line 133
Source documentation
The weak-composition function representation and the finite antidiagonal representation used by power-series coefficient extraction are equivalent.
```
def homogeneousFunctionsEquivAntidiag [Fintype σ] [DecidableEq σ] (a : ℕ) :
    {d : σ → ℕ // ∑ x, d x = a} ≃
      ↥(Finset.finsuppAntidiag (Finset.univ : Finset σ) a) := by
…
```

theorem OAI.Problem335.sum_homogeneousFunctions_eq_antidiag line 142

Source documentation

Exact transport of a weak-composition sum to the finite antidiagonal.

theorem sum_homogeneousFunctions_eq_antidiag [Fintype σ] [DecidableEq σ] (a : ℕ)
    [Fintype {d : σ → ℕ // ∑ x, d x = a}]
    {M : Type*} [AddCommMonoid M] (f : (σ →₀ ℕ) → M) :
    (∑ d : {d : σ → ℕ // ∑ x, d x = a},
      f (Finsupp.equivFunOnFinite.symm d.val)) =
      ∑ d ∈ Finset.finsuppAntidiag (Finset.univ : Finset σ) a, f d := by
…