MixedOperatorBidegree.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The mixed operator restricts to the finite bidegree spaces used by the rank measure.

theorem OAI.Problem335.weight_map_hom line 16
theorem OAI.Problem335.weighted_homogeneous_map line 21
def OAI.Problem335.bidegreeCast line 28
def OAI.Problem335.bidegreeSign line 31
theorem OAI.Problem335.bidegreeCast_injective line 34
theorem OAI.Problem335.operatorWeight_bidegree line 38

theorem OAI.Problem335.mixedOperator_mem_bidegreeSubmodule line 47

Source documentation

Differentiation by a polynomial of bidegree (k,m) lowers derivative degree by k and raises multiplication degree by m.

theorem mixedOperator_mem_bidegreeSubmodule (isV : σ → Bool)
    {q p : MvPolynomial σ K} {k m a b : ℕ} (hka : k ≤ a)
    (hq : q ∈ bidegreeSubmodule isV k m)
    (hp : p ∈ bidegreeSubmodule isV a b) :
    mixedOperator isV q p ∈ bidegreeSubmodule isV (a - k) (b + m) := by
…

Mentions: OAI.Problem335.bidegreeSubmodule, OAI.Problem335.mixedOperator

theorem OAI.Problem335.mixedOperator_eq_zero_of_bidegree_lt line 63

Source documentation

More differentiation than the available derivative degree annihilates the input.

theorem mixedOperator_eq_zero_of_bidegree_lt (isV : σ → Bool)
    {q p : MvPolynomial σ K} {k m a b : ℕ} (hka : a < k)
    (hq : q ∈ bidegreeSubmodule isV k m)
    (hp : p ∈ bidegreeSubmodule isV a b) : mixedOperator isV q p = 0 := by
…

Mentions: OAI.Problem335.bidegreeSubmodule, OAI.Problem335.mixedOperator

theorem OAI.Problem335.mixedOperator_mem_bidegreeSubmodule_all line 83
Source documentation
The degree-shift membership also holds without a degree inequality: when k > a, the output is zero and belongs to every homogeneous submodule.
```
theorem mixedOperator_mem_bidegreeSubmodule_all (isV : σ → Bool)
    {q p : MvPolynomial σ K} {k m a b : ℕ}
    (hq : q ∈ bidegreeSubmodule isV k m)
    (hp : p ∈ bidegreeSubmodule isV a b) :
    mixedOperator isV q p ∈ bidegreeSubmodule isV (a - k) (b + m) := by
…
```
Mentions: OAI.Problem335.bidegreeSubmodule, OAI.Problem335.mixedOperator