BlockWeight.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem346.PolynomialWeights.weightedEuler line 16
Source documentation
The Euler derivation associated with natural-number weights.
```
def weightedEuler (w : σ → ℕ) :
    Derivation R (MvPolynomial σ R) (MvPolynomial σ R) :=
…
```
theorem OAI.Problem346.PolynomialWeights.weightedEuler_apply line 20
theorem OAI.Problem346.PolynomialWeights.weightedEuler_X line 28
theorem OAI.Problem346.PolynomialWeights.weightedEuler_of_homogeneous line 34
Source documentation
Euler's identity, expressed using a bundled derivation.
```
theorem weightedEuler_of_homogeneous (w : σ → ℕ) {n : ℕ}
    {f : MvPolynomial σ R} (hf : f.IsWeightedHomogeneous w n) :
    weightedEuler w f = n • f := by
…
```
Mentions: OAI.Problem346.PolynomialWeights.weightedEuler
theorem OAI.Problem346.PolynomialWeights.derivation_eq_weightedEuler line 41
Source documentation
Any derivation with the prescribed diagonal action on generators is Euler.
```
theorem derivation_eq_weightedEuler (w : σ → ℕ)
    (N : Derivation R (MvPolynomial σ R) (MvPolynomial σ R))
    (hN : ∀ i, N (X i) = w i • X i) : N = weightedEuler w := by
…
```
Mentions: OAI.Problem346.PolynomialWeights.weightedEuler

theorem OAI.Problem346.PolynomialWeights.derivation_homogeneous_eigenvalue line 49

Source documentation

A homogeneous polynomial is an eigenvector for its weighted Euler derivation.

theorem derivation_homogeneous_eigenvalue (w : σ → ℕ)
    (N : Derivation R (MvPolynomial σ R) (MvPolynomial σ R))
    (hN : ∀ i, N (X i) = w i • X i)
    {n : ℕ} {f : MvPolynomial σ R} (hf : f.IsWeightedHomogeneous w n) :
    N f = n • f := by
…

def OAI.Problem346.PolynomialWeights.blockWeight line 62
Source documentation
Weight one on one coordinate block, and zero on all spectator blocks.
```
def blockWeight (u : β) (ki : β × ι) : ℕ := if ki.1 = u then 1 else 0
```
def OAI.Problem346.PolynomialWeights.IsBlockHomogeneous line 65
Source documentation
A polynomial is homogeneous of the specified degree in one block.
```
def IsBlockHomogeneous (u : β) (f : MvPolynomial (β × ι) R) (n : ℕ) : Prop :=
…
```
theorem OAI.Problem346.PolynomialWeights.blockWeight_apply line 69
theorem OAI.Problem346.PolynomialWeights.block_euler_eigenvalue line 72

theorem OAI.Problem346.PolynomialWeights.block_difference_eigenvalue line 84

Source documentation

The difference of block counting operators has the difference of the block degrees as eigenvalue. This is the weight used by the positive-weight shift lemma.

theorem block_difference_eigenvalue (u v : β)
    (Nu Nv : Derivation ℂ (MvPolynomial (β × ι) ℂ) (MvPolynomial (β × ι) ℂ))
    (hu : ∀ k i, Nu (X (k, i)) = if k = u then X (k, i) else 0)
    (hv : ∀ k i, Nv (X (k, i)) = if k = v then X (k, i) else 0)
    {p q : ℕ} {f : MvPolynomial (β × ι) ℂ}
    (hp : IsBlockHomogeneous u f p) (hq : IsBlockHomogeneous v f q) :
    (Nu - Nv) f = ((p : ℂ) - (q : ℂ)) • f := by
…

Mentions: OAI.Problem346.PolynomialWeights.IsBlockHomogeneous

theorem OAI.Problem346.PolynomialWeights.block_difference_nat_eigenvalue line 96
theorem OAI.Problem346.PolynomialWeights.block_pderiv_source line 108
Source documentation
Differentiating in a block lowers its degree by one, provided that degree is positive.
```
theorem block_pderiv_source {u : β} {n : ℕ} {f : MvPolynomial (β × ι) R}
    (hf : IsBlockHomogeneous u f n) (hn : 0 < n) (i : ι) :
    IsBlockHomogeneous u (pderiv (u, i) f) (n - 1) := by
…
```
Mentions: OAI.Problem346.PolynomialWeights.IsBlockHomogeneous
theorem OAI.Problem346.PolynomialWeights.block_pderiv_other line 117
Source documentation
Differentiating in another block leaves the indicated block degree unchanged.
```
theorem block_pderiv_other {u k : β} (hku : k ≠ u) {n : ℕ}
    {f : MvPolynomial (β × ι) R} (hf : IsBlockHomogeneous u f n) (i : ι) :
    IsBlockHomogeneous u (pderiv (k, i) f) n := by
…
```
Mentions: OAI.Problem346.PolynomialWeights.IsBlockHomogeneous

theorem OAI.Problem346.PolynomialWeights.block_shift_degree_source line 125

Source documentation

A directional shift lowers its source block degree by one.

theorem block_shift_degree_source {u v : β} (huv : u ≠ v) {n : ℕ}
    {f : MvPolynomial (β × ι) R} (hf : IsBlockHomogeneous u f n) (hn : 0 < n) :
    IsBlockHomogeneous u (∑ i : ι, X (v, i) * pderiv (u, i) f) (n - 1) := by
…

Mentions: OAI.Problem346.PolynomialWeights.IsBlockHomogeneous

theorem OAI.Problem346.PolynomialWeights.block_shift_degree_destination line 138

Source documentation

A directional shift raises its destination block degree by one.

theorem block_shift_degree_destination {u v : β} (huv : u ≠ v) {n : ℕ}
    {f : MvPolynomial (β × ι) R} (hf : IsBlockHomogeneous v f n) :
    IsBlockHomogeneous v (∑ i : ι, X (v, i) * pderiv (u, i) f) (n + 1) := by
…

Mentions: OAI.Problem346.PolynomialWeights.IsBlockHomogeneous

theorem OAI.Problem346.PolynomialWeights.block_shift_degree_spectator line 151

Source documentation

A directional shift leaves every spectator block degree unchanged.

theorem block_shift_degree_spectator {u v k : β} (huk : u ≠ k) (hvk : v ≠ k)
    {n : ℕ} {f : MvPolynomial (β × ι) R} (hf : IsBlockHomogeneous k f n) :
    IsBlockHomogeneous k (∑ i : ι, X (v, i) * pderiv (u, i) f) n := by
…

Mentions: OAI.Problem346.PolynomialWeights.IsBlockHomogeneous