OperatorMonomials.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem335.derivExponent line 16
Source documentation
Exponents of the variables acting by differentiation.
```
def derivExponent (isV : σ → Bool) (d : σ →₀ ℕ) : σ →₀ ℕ :=
…
```
def OAI.Problem335.mulExponent line 20
Source documentation
Exponents of the variables acting by multiplication.
```
def mulExponent (isV : σ → Bool) (d : σ →₀ ℕ) : σ →₀ ℕ :=
…
```
def OAI.Problem335.operatorFactorial line 24
Source documentation
Integral coefficient supplied by a mixed derivative on a monomial.
```
def operatorFactorial (isV : σ → Bool) (d e : σ →₀ ℕ) : ℕ :=
…
```
theorem OAI.Problem335.variableOperator_pow_true_monomial line 27
theorem OAI.Problem335.variableOperator_pow_false_monomial line 34
theorem OAI.Problem335.operatorFactorial_single_add line 40
theorem OAI.Problem335.mixedOperator_monomial_one_apply line 54
Source documentation
The complete mixed operator sends a monomial to a single monomial.
```
theorem mixedOperator_monomial_one_apply (isV : σ → Bool) (d e : σ →₀ ℕ) (b : K) :
    mixedOperator isV (monomial d 1) (monomial e b) =
      monomial (e - derivExponent isV d + mulExponent isV d)
        (b * operatorFactorial isV d e) := by
…
```
Mentions: OAI.Problem335.mixedOperator, OAI.Problem335.derivExponent, OAI.Problem335.mulExponent, OAI.Problem335.operatorFactorial
theorem OAI.Problem335.mixedOperator_monomial_apply line 101
Source documentation
Exact arbitrary-coefficient monomial action, over every commutative semiring.
```
theorem mixedOperator_monomial_apply (isV : σ → Bool) (d e : σ →₀ ℕ) (a b : K) :
    mixedOperator isV (monomial d a) (monomial e b) =
      monomial (e - derivExponent isV d + mulExponent isV d)
        (a * b * operatorFactorial isV d e) := by
…
```
Mentions: OAI.Problem335.mixedOperator, OAI.Problem335.derivExponent, OAI.Problem335.mulExponent, OAI.Problem335.operatorFactorial

theorem OAI.Problem335.coeff_mixedOperator_monomial line 110

Source documentation

All matrix coefficients of a monomial mixed operator are explicit integral multiples.

theorem coeff_mixedOperator_monomial [DecidableEq σ] (isV : σ → Bool) (d e f : σ →₀ ℕ) (a b : K) :
    (mixedOperator isV (monomial d a) (monomial e b)).coeff f =
      if e - derivExponent isV d + mulExponent isV d = f
      then a * b * operatorFactorial isV d e else 0 := by
…

Mentions: OAI.Problem335.mixedOperator, OAI.Problem335.derivExponent, OAI.Problem335.mulExponent, OAI.Problem335.operatorFactorial

theorem OAI.Problem335.operatorFactorial_ne_zero_iff line 118
Source documentation
A mixed monomial has nonzero integral multiplier exactly when differentiation is possible.
```
theorem operatorFactorial_ne_zero_iff (isV : σ → Bool) (d e : σ →₀ ℕ) :
    operatorFactorial isV d e ≠ 0 ↔ derivExponent isV d ≤ e := by
…
```
Mentions: OAI.Problem335.operatorFactorial, OAI.Problem335.derivExponent
theorem OAI.Problem335.mixedOperator_monomial_ne_zero_iff line 142
Source documentation
Over characteristic zero without zero divisors, the only possible vanishing is an excessive differentiation exponent or a zero input coefficient.
```
theorem mixedOperator_monomial_ne_zero_iff [NoZeroDivisors K] [CharZero K]
    (isV : σ → Bool) (d e : σ →₀ ℕ) (a b : K) :
    mixedOperator isV (monomial d a) (monomial e b) ≠ 0 ↔
      a ≠ 0 ∧ b ≠ 0 ∧ derivExponent isV d ≤ e := by
…
```
Mentions: OAI.Problem335.mixedOperator, OAI.Problem335.derivExponent

theorem OAI.Problem335.mixedOperator_apply_monomial line 150

Source documentation

The action of an arbitrary polynomial on a monomial is an explicit finite sum.

theorem mixedOperator_apply_monomial (isV : σ → Bool) (p : MvPolynomial σ K)
    (e : σ →₀ ℕ) (b : K) :
    mixedOperator isV p (monomial e b) =
      ∑ d ∈ p.support, monomial (e - derivExponent isV d + mulExponent isV d)
        (p.coeff d * b * operatorFactorial isV d e) := by
…

Mentions: OAI.Problem335.mixedOperator, OAI.Problem335.derivExponent, OAI.Problem335.mulExponent, OAI.Problem335.operatorFactorial

theorem OAI.Problem335.operator_target_injective line 162

Source documentation

Distinct non-annihilated operator monomials have distinct output exponents on each fixed source monomial. This is the orthogonality behind the first trace.

theorem operator_target_injective (isV : σ → Bool) (e d₁ d₂ : σ →₀ ℕ)
    (h₁ : derivExponent isV d₁ ≤ e) (h₂ : derivExponent isV d₂ ≤ e)
    (h : e - derivExponent isV d₁ + mulExponent isV d₁ =
      e - derivExponent isV d₂ + mulExponent isV d₂) : d₁ = d₂ := by
…

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

theorem OAI.Problem335.coeff_mixedOperator_at_target line 177

Source documentation

At a surviving monomial's own target, no other operator monomial contributes.

theorem coeff_mixedOperator_at_target (isV : σ → Bool) (p : MvPolynomial σ K)
    (d e : σ →₀ ℕ) (b : K) (hd : derivExponent isV d ≤ e) :
    (mixedOperator isV p (monomial e b)).coeff
      (e - derivExponent isV d + mulExponent isV d) =
      p.coeff d * b * operatorFactorial isV d e := by
…

Mentions: OAI.Problem335.derivExponent, OAI.Problem335.mixedOperator, OAI.Problem335.mulExponent, OAI.Problem335.operatorFactorial