Documentation

TauCeti.Algebra.LinearRecurrence.Inequality

Bounded solutions of a second-order recurrence inequality #

Let d ≥ 1 and r be natural numbers, and let c : ℕ → ℕ start at c 0 = 0 and satisfy

c (n + 2) + r c n ≥ 1 + d c (n + 1)       for every n.

If d² ≥ 4 r, the characteristic polynomial X² - d X + r has real roots α ≥ β ≥ 0 with α ≥ 1, and the differences w n = c (n + 1) - β c n satisfy w (n + 1) ≥ α w n + 1 ≥ w n + 1, so c (n + 1) ≥ w n ≥ n grows without bound. Hence a bounded such sequence forces d² < 4 r.

This is the numerical half of the Golod–Shafarevich inequality: for a finite-dimensional algebra with a presentation by d generators and r relations of degree at least two, the codimensions of the powers of the augmentation ideal satisfy this recurrence, and are bounded by the dimension.

Main results #

References #

theorem TauCeti.sq_lt_four_mul_of_forall_add_mul_le {d r : ℕ} (hd : 1 ≤ d) {c : ℕ → ℕ} (h0 : c 0 = 0) (hbdd : BddAbove (Set.range c)) (hrec : ∀ (n : ℕ), 1 + d * c (n + 1) ≤ c (n + 2) + r * c n) :
d ^ 2 < 4 * r

A bounded solution of c (n + 2) + r c n ≥ 1 + d c (n + 1) forces d² < 4 r. Let d ≥ 1, and let c : ℕ → ℕ be bounded, with c 0 = 0 and 1 + d c (n + 1) ≤ c (n + 2) + r c n for every n. Then d² < 4 r.