OperatorExponentBidegree.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Degree and validity of the natural exponent produced by a mixed monomial operator.

theorem OAI.Problem335.bidegreeWeight_derivExponent line 15
Source documentation
Filtering to derivative variables retains precisely the first bidegree.
```
theorem bidegreeWeight_derivExponent (isV : σ → Bool) (d : σ →₀ ℕ) :
    Finsupp.weight (bidegreeWeight isV) (derivExponent isV d) =
      ((Finsupp.weight (bidegreeWeight isV) d).1, 0) := by
…
```
Mentions: OAI.Problem335.bidegreeWeight, OAI.Problem335.derivExponent
theorem OAI.Problem335.bidegreeWeight_mulExponent line 33
Source documentation
Filtering to multiplication variables retains precisely the second bidegree.
```
theorem bidegreeWeight_mulExponent (isV : σ → Bool) (d : σ →₀ ℕ) :
    Finsupp.weight (bidegreeWeight isV) (mulExponent isV d) =
      (0, (Finsupp.weight (bidegreeWeight isV) d).2) := by
…
```
Mentions: OAI.Problem335.bidegreeWeight, OAI.Problem335.mulExponent

theorem OAI.Problem335.bidegree_le_of_derivExponent_le line 51

Source documentation

Availability of every derivative implies availability of the total derivative degree.

theorem bidegree_le_of_derivExponent_le (isV : σ → Bool) (d e : σ →₀ ℕ)
    {k m a b : ℕ} (hd : Finsupp.weight (bidegreeWeight isV) d = (k,m))
    (he : Finsupp.weight (bidegreeWeight isV) e = (a,b))
    (hle : derivExponent isV d ≤ e) : k ≤ a := by
…

Mentions: OAI.Problem335.bidegreeWeight, OAI.Problem335.derivExponent

theorem OAI.Problem335.bidegreeWeight_operator_target line 64

Source documentation

A valid monomial action has a natural output exponent in exactly the required finite bidegree fiber, without any coefficient-field assumptions.

theorem bidegreeWeight_operator_target (isV : σ → Bool) (d e : σ →₀ ℕ)
    {k m a b : ℕ} (hd : Finsupp.weight (bidegreeWeight isV) d = (k,m))
    (he : Finsupp.weight (bidegreeWeight isV) e = (a,b))
    (hle : derivExponent isV d ≤ e) :
    Finsupp.weight (bidegreeWeight isV)
      (e - derivExponent isV d + mulExponent isV d) = (a-k,b+m) := by
…

Mentions: OAI.Problem335.bidegreeWeight, OAI.Problem335.derivExponent, OAI.Problem335.mulExponent