ShiftHomogeneity.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem346.weightedHomogeneous_pderiv line 15
Source documentation
Differentiating a weighted homogeneous polynomial lowers its weighted degree by the weight of the differentiated variable. The statement also covers degree zero, since a zero derivative is homogeneous in every degree.
```
theorem weightedHomogeneous_pderiv
    {σ R : Type*} [CommSemiring R] {w : σ → ℕ}
    {f : MvPolynomial σ R} {m : ℕ}
    (hf : IsWeightedHomogeneous w f m) (i : σ) :
    IsWeightedHomogeneous w (pderiv i f) (m - w i) := by
…
```

theorem OAI.Problem346.weightedHomogeneous_directional line 29

Source documentation

A weighted directional derivative has the expected homogeneous degree when all source variables and all destination variables have common weights.

theorem weightedHomogeneous_directional
    {σ κ R : Type*} [Fintype κ] [CommSemiring R]
    {w : σ → ℕ} {f : MvPolynomial σ R} {m a b : ℕ}
    (hf : IsWeightedHomogeneous w f m) (s t : κ → σ)
    (hs : ∀ i, w (s i) = a) (ht : ∀ i, w (t i) = b) :
    IsWeightedHomogeneous w (∑ i, X (t i) * pderiv (s i) f) (b + (m - a)) := by
…

theorem OAI.Problem346.derivation_sum_apply line 40
theorem OAI.Problem346.blockShift_eq_sum_pderiv line 50
Source documentation
The generator-defined block shift agrees with the usual sum of partial derivatives over its coordinate block.
```
theorem blockShift_eq_sum_pderiv
    {ι κ R : Type*} [DecidableEq ι] [Fintype κ] [CommRing R] (u v : ι) :
    blockShift (κ := κ) R u v =
…
```
Mentions: OAI.Problem346.blockShift
theorem OAI.Problem346.blockShift_apply_eq_sum line 63

theorem OAI.Problem346.blockShift_isWeightedHomogeneous line 72

Source documentation

A block shift changes the degree in an observed block by adding one for the destination and subtracting one for the source.

theorem blockShift_isWeightedHomogeneous
    {ι κ R : Type*} [DecidableEq ι] [Fintype κ] [CommRing R]
    (u v k : ι) {f : MvPolynomial (ι × κ) R} {m : ℕ}
    (hf : IsWeightedHomogeneous (fun z : ι × κ => if z.1 = k then 1 else 0) f m) :
    IsWeightedHomogeneous (fun z : ι × κ => if z.1 = k then 1 else 0)
      (blockShift R u v f)
      ((if v = k then 1 else 0) + (m - (if u = k then 1 else 0))) := by
…

Mentions: OAI.Problem346.blockShift

theorem OAI.Problem346.blockShift_source_homogeneous line 84

Source documentation

The source block loses one unit of degree under a directional shift.

theorem blockShift_source_homogeneous
    {ι κ R : Type*} [DecidableEq ι] [Fintype κ] [CommRing R]
    (u v : ι) (huv : u ≠ v) {f : MvPolynomial (ι × κ) R} {m : ℕ}
    (hf : IsWeightedHomogeneous (fun z : ι × κ => if z.1 = u then 1 else 0) f m) :
    IsWeightedHomogeneous (fun z : ι × κ => if z.1 = u then 1 else 0)
      (blockShift R u v f) (m - 1) := by
…

Mentions: OAI.Problem346.blockShift

theorem OAI.Problem346.blockShift_destination_homogeneous line 93

Source documentation

The destination block gains one unit of degree under a directional shift.

theorem blockShift_destination_homogeneous
    {ι κ R : Type*} [DecidableEq ι] [Fintype κ] [CommRing R]
    (u v : ι) (huv : u ≠ v) {f : MvPolynomial (ι × κ) R} {m : ℕ}
    (hf : IsWeightedHomogeneous (fun z : ι × κ => if z.1 = v then 1 else 0) f m) :
    IsWeightedHomogeneous (fun z : ι × κ => if z.1 = v then 1 else 0)
      (blockShift R u v f) (m + 1) := by
…

Mentions: OAI.Problem346.blockShift

theorem OAI.Problem346.blockShift_spectator_homogeneous line 102

Source documentation

Spectator block degrees are unchanged by a directional shift.

theorem blockShift_spectator_homogeneous
    {ι κ R : Type*} [DecidableEq ι] [Fintype κ] [CommRing R]
    (u v k : ι) (hu : u ≠ k) (hv : v ≠ k)
    {f : MvPolynomial (ι × κ) R} {m : ℕ}
    (hf : IsWeightedHomogeneous (fun z : ι × κ => if z.1 = k then 1 else 0) f m) :
    IsWeightedHomogeneous (fun z : ι × κ => if z.1 = k then 1 else 0)
      (blockShift R u v f) m := by
…

Mentions: OAI.Problem346.blockShift

theorem OAI.Problem346.blockShift_pow_source_homogeneous line 112

Source documentation

Repeated shifts lower the source degree by the number of operations.

theorem blockShift_pow_source_homogeneous
    {ι κ R : Type*} [DecidableEq ι] [Fintype κ] [CommRing R]
    (u v : ι) (huv : u ≠ v) {f : MvPolynomial (ι × κ) R} {m : ℕ}
    (hf : IsWeightedHomogeneous (fun z : ι × κ => if z.1 = u then 1 else 0) f m)
    (n : ℕ) :
    IsWeightedHomogeneous (fun z : ι × κ => if z.1 = u then 1 else 0)
      (((blockShift R u v).toLinearMap ^ n) f) (m - n) := by
…

Mentions: OAI.Problem346.blockShift

theorem OAI.Problem346.blockShift_pow_destination_homogeneous line 126

Source documentation

Repeated shifts increase the destination degree by the number of operations.

theorem blockShift_pow_destination_homogeneous
    {ι κ R : Type*} [DecidableEq ι] [Fintype κ] [CommRing R]
    (u v : ι) (huv : u ≠ v) {f : MvPolynomial (ι × κ) R} {m : ℕ}
    (hf : IsWeightedHomogeneous (fun z : ι × κ => if z.1 = v then 1 else 0) f m)
    (n : ℕ) :
    IsWeightedHomogeneous (fun z : ι × κ => if z.1 = v then 1 else 0)
      (((blockShift R u v).toLinearMap ^ n) f) (m + n) := by
…

Mentions: OAI.Problem346.blockShift

theorem OAI.Problem346.blockShift_pow_spectator_homogeneous line 140

Source documentation

Repeated shifts leave all spectator block degrees unchanged.

theorem blockShift_pow_spectator_homogeneous
    {ι κ R : Type*} [DecidableEq ι] [Fintype κ] [CommRing R]
    (u v k : ι) (hu : u ≠ k) (hv : v ≠ k)
    {f : MvPolynomial (ι × κ) R} {m : ℕ}
    (hf : IsWeightedHomogeneous (fun z : ι × κ => if z.1 = k then 1 else 0) f m)
    (n : ℕ) :
    IsWeightedHomogeneous (fun z : ι × κ => if z.1 = k then 1 else 0)
      (((blockShift R u v).toLinearMap ^ n) f) m := by
…

Mentions: OAI.Problem346.blockShift