ShiftInjectivity.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem346.ShiftInjectivity.weight_pow line 14

Source documentation

A weight-raising operator increases the weight of its iterates by two.

theorem weight_pow (E H : Module.End K M)
    (hHE : ∀ z, H (E z) = E (H z) + (2 : K) • E z)
    (x : M) (w : K) (hx : H x = w • x) (n : ℕ) :
    H ((E ^ n) x) = (w + 2 * (n : K)) • (E ^ n) x := by
…

theorem OAI.Problem346.ShiftInjectivity.lowering_pow line 28

Source documentation

The lowering operator on a string generated from a vector in its kernel.

theorem lowering_pow (D E H : Module.End K M)
    (hDE : ∀ z, D (E z) = E (D z) - H z)
    (hHE : ∀ z, H (E z) = E (H z) + (2 : K) • E z)
    (x : M) (w : K) (hx : H x = w • x) (hDx : D x = 0) (n : ℕ) :
    D ((E ^ (n + 1)) x) =
      (-((n + 1 : K) * (w + n))) • (E ^ n) x := by
…

theorem OAI.Problem346.ShiftInjectivity.eq_zero_of_positive_weight line 48
Source documentation
Positive-weight vectors killed by a lowering operator vanish provided that the opposite operator acts nilpotently on that vector. This is the algebraic form of positive-weight differential injectivity and requires no inner product.
```
theorem eq_zero_of_positive_weight (D E H : Module.End K M)
    (hDE : ∀ z, D (E z) = E (D z) - H z)
    (hHE : ∀ z, H (E z) = E (H z) + (2 : K) • E z)
    (x : M) (w : ℕ) (hw : 0 < w) (hx : H x = (w : K) • x)
    (hDx : D x = 0) (hnil : ∃ N : ℕ, (E ^ N) x = 0) : x = 0 := by
…
```