OperatorRank.lean`

23 declarations, 0 contain sorry, 0 declared as axioms

Bigraded polynomial spaces used by the differentiation--multiplication rank measure. The Boolean partition assigns derivative variables to true and multiplication variables to false.

def OAI.Problem335.bidegreeWeight line 19
Source documentation
Degree in derivative variables and in multiplication variables, respectively.
```
def bidegreeWeight (isV : σ → Bool) (i : σ) : ℕ × ℕ :=
…
```
theorem OAI.Problem335.bidegreeWeight_true line 22
theorem OAI.Problem335.bidegreeWeight_false line 25

theorem OAI.Problem335.bidegreeWeight_total line 29

Source documentation

The sum of the two partial degrees is total degree.

theorem bidegreeWeight_total (isV : σ → Bool) (d : σ →₀ ℕ) :
    (Finsupp.weight (bidegreeWeight isV) d).1 +
      (Finsupp.weight (bidegreeWeight isV) d).2 = d.degree := by
…

Mentions: OAI.Problem335.bidegreeWeight

def OAI.Problem335.bidegreeSubmodule line 43
Source documentation
The polynomial subspace of fixed bidegree.
```
def bidegreeSubmodule (isV : σ → Bool) (a b : ℕ) : Submodule K (MvPolynomial σ K) :=
…
```

def OAI.Problem335.bidegreeComponent line 47

Source documentation

Linear projection to a fixed bidegree.

def bidegreeComponent (isV : σ → Bool) (a b : ℕ) :
    MvPolynomial σ K →ₗ[K] MvPolynomial σ K :=
…

theorem OAI.Problem335.mem_bidegreeSubmodule line 51
theorem OAI.Problem335.coeff_bidegreeComponent line 56
theorem OAI.Problem335.bidegreeComponent_mem line 63
theorem OAI.Problem335.bidegreeComponent_eq_self line 68
theorem OAI.Problem335.bidegreeSubmodule_isHomogeneous line 73
theorem OAI.Problem335.finite_bidegreeMonomials line 81
instance OAI.Problem335.bidegreeSubmodule_finite line 89
theorem OAI.Problem335.bidegreeSubmodule_mul line 98
theorem OAI.Problem335.bidegreeSubmodule_pderiv_true line 104
theorem OAI.Problem335.bidegreeSubmodule_pderiv_false line 117
theorem OAI.Problem335.bidegreeSubmodule_X_mul_true line 130
theorem OAI.Problem335.bidegreeSubmodule_X_mul_false line 138

theorem OAI.Problem335.bidegree_decomposition line 147

Source documentation

A homogeneous polynomial splits into its finitely many possible bidegrees.

theorem bidegree_decomposition (isV : σ → Bool) {n : ℕ}
    {p : MvPolynomial σ K} (hp : p.IsHomogeneous n) :
    p = ∑ i : Fin (n + 1), bidegreeComponent isV i (n - i) p := by
…

Mentions: OAI.Problem335.bidegreeComponent

theorem OAI.Problem335.bidegreeComponent_of_mem line 176
Source documentation
Projection acts diagonally on a polynomial already of a fixed bidegree.
```
theorem bidegreeComponent_of_mem {isV : σ → Bool} {a b k m : ℕ}
    {p : MvPolynomial σ K} (hp : p ∈ bidegreeSubmodule isV a b) :
    bidegreeComponent isV k m p = if k = a ∧ m = b then p else 0 := by
…
```
Mentions: OAI.Problem335.bidegreeSubmodule, OAI.Problem335.bidegreeComponent

theorem OAI.Problem335.bidegreeSubmodule_prod line 184

Source documentation

Finite products add both partial degrees.

theorem bidegreeSubmodule_prod {ι : Type*} (s : Finset ι)
    {isV : σ → Bool} {a b : ι → ℕ} {p : ι → MvPolynomial σ K}
    (hp : ∀ j ∈ s, p j ∈ bidegreeSubmodule isV (a j) (b j)) :
    (∏ j ∈ s, p j) ∈ bidegreeSubmodule isV (∑ j ∈ s, a j) (∑ j ∈ s, b j) := by
…

Mentions: OAI.Problem335.bidegreeSubmodule

theorem OAI.Problem335.product_bidegree_decomposition line 194

Source documentation

Expansion of a product into all choices of factor bidegrees.

theorem product_bidegree_decomposition {ι : Type*} [Fintype ι] [DecidableEq ι]
    (isV : σ → Bool) (e : ι → ℕ) (p : ι → MvPolynomial σ K)
    (hp : ∀ j, (p j).IsHomogeneous (e j)) :
    (∏ j, p j) = ∑ a : (∀ j : ι, Fin (e j + 1)),
      ∏ j, bidegreeComponent isV (a j) (e j - a j) (p j) := by
…

Mentions: OAI.Problem335.bidegreeComponent

theorem OAI.Problem335.bidegreeComponent_product line 209

Source documentation

The fixed-bidegree component of a product is the constrained assignment sum.

theorem bidegreeComponent_product {ι : Type*} [Fintype ι] [DecidableEq ι]
    (isV : σ → Bool) (e : ι → ℕ) (p : ι → MvPolynomial σ K)
    (hp : ∀ j, (p j).IsHomogeneous (e j)) (k m : ℕ) :
    bidegreeComponent isV k m (∏ j, p j) =
      ∑ a : (∀ j : ι, Fin (e j + 1)),
        if (∑ j : ι, (a j : ℕ)) = k ∧ (∑ j : ι, (e j - (a j : ℕ))) = m then
          ∏ j, bidegreeComponent isV (a j) (e j - a j) (p j)
        else 0 := by
…

Mentions: OAI.Problem335.bidegreeComponent