MixedOperator.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

The full differentiation/multiplication substitution used by the rank measure. The variables selected by isV act by partial differentiation; all others act by multiplication. Since these two sets are disjoint, the operators commute, and polynomial substitution is an algebra homomorphism.

theorem OAI.Problem335.pderiv_pderiv_comm line 20
Source documentation
Formal partial derivatives commute, over an arbitrary commutative semiring.
```
theorem pderiv_pderiv_comm (i j : σ) (p : MvPolynomial σ K) :
    pderiv i (pderiv j p) = pderiv j (pderiv i p) := by
…
```
def OAI.Problem335.variableOperator line 32
Source documentation
The endomorphism assigned to an individual variable.
```
def variableOperator (isV : σ → Bool) (i : σ) :
    Module.End K (MvPolynomial σ K) :=
…
```
theorem OAI.Problem335.variableOperator_of_true line 36
theorem OAI.Problem335.variableOperator_of_false line 41
theorem OAI.Problem335.variableOperator_comm line 47
Source documentation
Operators assigned to any two variables commute.
```
theorem variableOperator_comm (isV : σ → Bool) (i j : σ) :
    Commute (variableOperator (K := K) isV i) (variableOperator isV j) := by
…
```
Mentions: OAI.Problem335.variableOperator
def OAI.Problem335.mixedOperator line 68
Source documentation
Substitution of derivatives on V and multiplication on its complement. This is the full operator, before taking a bidegree component or restricting to finite-dimensional homogeneous source and target spaces.
```
def mixedOperator (isV : σ → Bool) :
    MvPolynomial σ K →ₐ[K] Module.End K (MvPolynomial σ K) := by
…
```
theorem OAI.Problem335.mixedOperator_X line 77
theorem OAI.Problem335.mixedOperator_C line 81
theorem OAI.Problem335.mixedOperator_add line 85
theorem OAI.Problem335.mixedOperator_mul line 90
Source documentation
The full operator respects products (unlike the projected finite rank map).
```
@[simp] theorem mixedOperator_mul (isV : σ → Bool) (p q : MvPolynomial σ K) :
    mixedOperator isV (p * q) = mixedOperator isV p * mixedOperator isV q :=
…
```
Mentions: OAI.Problem335.mixedOperator
theorem OAI.Problem335.mixedOperator_mul_apply line 94