OperatorHomogeneity.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Weighted-degree preservation for differential/multiplication substitution.

theorem OAI.Problem335.pderiv_isWeightedHomogeneous line 17
Source documentation
A partial derivative subtracts the weight of its variable. The use of a weight group avoids artificial truncation at degree zero.
```
theorem pderiv_isWeightedHomogeneous {w : σ → M} {p : MvPolynomial σ K}
    {a : M} (hp : p.IsWeightedHomogeneous w a) (i : σ) :
    (pderiv i p).IsWeightedHomogeneous w (a - w i) := by
…
```
def OAI.Problem335.operatorWeight line 31
Source documentation
The weighted-degree shift assigned to an operator variable: differentiation has negative weight, while multiplication has positive weight.
```
def operatorWeight (isV : σ → Bool) (w : σ → M) (i : σ) : M :=
…
```
theorem OAI.Problem335.variableOperator_isWeightedHomogeneous line 34

theorem OAI.Problem335.mixedOperator_X_pow_isWeightedHomogeneous line 44

Source documentation

A power of a variable shifts degree by the corresponding multiple.

theorem mixedOperator_X_pow_isWeightedHomogeneous (isV : σ → Bool) (w : σ → M)
    (i : σ) (r : ℕ) {p : MvPolynomial σ K} {a : M}
    (hp : p.IsWeightedHomogeneous w a) :
    (mixedOperator isV (X i ^ r) p).IsWeightedHomogeneous w
      (a + r • operatorWeight isV w i) := by
…

Mentions: OAI.Problem335.mixedOperator, OAI.Problem335.operatorWeight

theorem OAI.Problem335.mixedOperator_monomial_one_isWeightedHomogeneous line 57

Source documentation

Monomial operators shift weighted degree by the sum of their variable shifts.

theorem mixedOperator_monomial_one_isWeightedHomogeneous (isV : σ → Bool) (w : σ → M)
    (d : σ →₀ ℕ) {p : MvPolynomial σ K} {a : M}
    (hp : p.IsWeightedHomogeneous w a) :
    (mixedOperator isV (monomial d 1) p).IsWeightedHomogeneous w
      (a + Finsupp.weight (operatorWeight isV w) d) := by
…

Mentions: OAI.Problem335.mixedOperator, OAI.Problem335.operatorWeight

theorem OAI.Problem335.mixedOperator_isWeightedHomogeneous line 76
Source documentation
The full mixed operator sends homogeneous inputs to the degree obtained by adding the (signed) homogeneous degree of its defining polynomial.
```
theorem mixedOperator_isWeightedHomogeneous (isV : σ → Bool) (w : σ → M)
    {q p : MvPolynomial σ K} {d a : M}
    (hq : q.IsWeightedHomogeneous (operatorWeight isV w) d)
    (hp : p.IsWeightedHomogeneous w a) :
    (mixedOperator isV q p).IsWeightedHomogeneous w (a + d) := by
…
```
Mentions: OAI.Problem335.operatorWeight, OAI.Problem335.mixedOperator