SumShift.lean`

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.Problem346.PolynomialShift.Vars line 13
abbrev OAI.Problem346.PolynomialShift.Poly line 14
def OAI.Problem346.PolynomialShift.down line 20
Source documentation
Shift one unit of degree from the first coordinate block to the second.
```
def down : Derivation R (Poly R ι σ) (Poly R ι σ) :=
…
```
Mentions: OAI.Problem346.PolynomialShift.Poly
def OAI.Problem346.PolynomialShift.up line 24
Source documentation
The opposite shift.
```
def up : Derivation R (Poly R ι σ) (Poly R ι σ) :=
…
```
Mentions: OAI.Problem346.PolynomialShift.Poly
def OAI.Problem346.PolynomialShift.sourceEuler line 29
Source documentation
Euler operator of the first coordinate block.
```
def sourceEuler : Derivation R (Poly R ι σ) (Poly R ι σ) :=
…
```
Mentions: OAI.Problem346.PolynomialShift.Poly
def OAI.Problem346.PolynomialShift.targetEuler line 33
Source documentation
Euler operator of the second coordinate block.
```
def targetEuler : Derivation R (Poly R ι σ) (Poly R ι σ) :=
…
```
Mentions: OAI.Problem346.PolynomialShift.Poly
def OAI.Problem346.PolynomialShift.weight line 38
Source documentation
Source degree minus destination degree.
```
def weight : Derivation R (Poly R ι σ) (Poly R ι σ) :=
…
```
Mentions: OAI.Problem346.PolynomialShift.Poly
theorem OAI.Problem346.PolynomialShift.down_source line 41
theorem OAI.Problem346.PolynomialShift.down_target line 45
theorem OAI.Problem346.PolynomialShift.down_spectator line 49
theorem OAI.Problem346.PolynomialShift.up_source line 53
theorem OAI.Problem346.PolynomialShift.up_target line 57
theorem OAI.Problem346.PolynomialShift.up_spectator line 61
theorem OAI.Problem346.PolynomialShift.weight_source line 65
theorem OAI.Problem346.PolynomialShift.weight_target line 69
theorem OAI.Problem346.PolynomialShift.weight_spectator line 73
theorem OAI.Problem346.PolynomialShift.up_down_commutator line 78
Source documentation
The fundamental commutator, with arbitrary spectator variables.
```
theorem up_down_commutator :
    ⁅up R ι σ, down R ι σ⁆ = weight R ι σ := by
…
```
Mentions: OAI.Problem346.PolynomialShift.up, OAI.Problem346.PolynomialShift.down, OAI.Problem346.PolynomialShift.weight
theorem OAI.Problem346.PolynomialShift.weight_up_commutator line 85
Source documentation
The opposite shift raises the source-minus-destination weight by two.
```
theorem weight_up_commutator :
    ⁅weight R ι σ, up R ι σ⁆ = (2 : R) • up R ι σ := by
…
```
Mentions: OAI.Problem346.PolynomialShift.weight, OAI.Problem346.PolynomialShift.up
theorem OAI.Problem346.PolynomialShift.weight_down_commutator line 93
Source documentation
The forward shift lowers the source-minus-destination weight by two.
```
theorem weight_down_commutator :
    ⁅weight R ι σ, down R ι σ⁆ = -(2 : R) • down R ι σ := by
…
```
Mentions: OAI.Problem346.PolynomialShift.weight, OAI.Problem346.PolynomialShift.down