BlockDerivation.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Coordinate-block derivations used in the differential-shift argument.

def OAI.Problem346.blockShift line 19
Source documentation
Move one unit of polynomial degree from block u to block v. The other coordinate blocks are spectators.
```
def blockShift (u v : ι) :
    Derivation R (MvPolynomial (ι × κ) R) (MvPolynomial (ι × κ) R) :=
…
```
theorem OAI.Problem346.blockShift_X line 23
theorem OAI.Problem346.blockShift_commutator line 29
Source documentation
The commutator of opposite block shifts is the difference of the two block Euler operators. This identity needs no finiteness assumption.
```
theorem blockShift_commutator (u v : ι) :
    ⁅blockShift (κ := κ) R v u, blockShift (κ := κ) R u v⁆ =
…
```
Mentions: OAI.Problem346.blockShift
theorem OAI.Problem346.blockShift_weight_commutator line 42
Source documentation
The weight operator raises the weight of the reverse shift by two.
```
theorem blockShift_weight_commutator (u v : ι) (huv : u ≠ v) :
    ⁅blockShift (κ := κ) R u u - blockShift (κ := κ) R v v, blockShift (κ := κ) R v u⁆ =
…
```
Mentions: OAI.Problem346.blockShift
theorem OAI.Problem346.blockShift_commutator_apply line 53
Source documentation
Pointwise version of the opposite-shift commutator.
```
theorem blockShift_commutator_apply (u v : ι) (f : MvPolynomial (ι × κ) R) :
    blockShift (κ := κ) R v u (blockShift (κ := κ) R u v f) -
…
```
Mentions: OAI.Problem346.blockShift

theorem OAI.Problem346.blockShift_weight_commutator_apply line 62

Source documentation

Pointwise version of the weight/raising commutator.

theorem blockShift_weight_commutator_apply (u v : ι) (huv : u ≠ v)
    (f : MvPolynomial (ι × κ) R) :
    (blockShift (κ := κ) R u u - blockShift (κ := κ) R v v) (blockShift (κ := κ) R v u f) -
…

Mentions: OAI.Problem346.blockShift

theorem OAI.Problem346.blockShift_square_X line 72
Source documentation
An off-diagonal block shift squares to zero on each coordinate generator.
```
theorem blockShift_square_X (u v k : ι) (huv : u ≠ v) (l : κ) :
    blockShift (κ := κ) R u v (blockShift R u v (X (k, l))) = 0 := by
…
```
Mentions: OAI.Problem346.blockShift
theorem OAI.Problem346.blockShift_eq_sum line 78
Source documentation
With finitely many coordinates, blockShift is the usual directional partial derivative, written as a sum of coordinate derivations.
```
theorem blockShift_eq_sum [Fintype κ] (u v : ι) :
    blockShift (κ := κ) R u v =
…
```
Mentions: OAI.Problem346.blockShift