Documentation

TauCeti.Algebra.Order.BigOperators.WeightedGrowth

Linear growth of weighted sums under a second-order inequality #

Let d_m(j) ≥ 0 be a family of vectors indexed by m : ℕ, and c a square matrix, with

d_1(j) ≥ ∑_i c_{ij} d_0(i),        d_{m+2}(j) + d_m(j) ≥ ∑_i c_{ij} d_{m+1}(i).

If a nonnegative weight δ satisfies 2 δ_i ≤ ∑_j c_{ij} δ_j, the weighted sums s_m = ∑_j δ_j d_m(j) satisfy s_1 ≥ 2 s_0 and s_{m+2} + s_m ≥ 2 s_{m+1}, so their successive differences never decrease and never fall below s_0, whence s_m ≥ (m + 1) s_0.

These are the inequalities satisfied by the graded pieces of an algebra with quadratic relations in the Golod--Shafarevich/Anick bound, where c counts the generators and δ witnesses that the matrix 2I - c is not positive definite; see TauCeti.PathAlgebra.not_module_finite_quotient_span_range_of_two_mul_le_sum.

Main results #

theorem TauCeti.add_one_mul_sum_mul_le_sum_mul {ι : Type u_1} [Fintype ι] {S : Type u_2} [CommRing S] [LinearOrder S] [IsStrictOrderedRing S] (c : ι → ι → S) {δ : ι → S} (hδ0 : 0 ≤ δ) (hδ : ∀ (i : ι), 2 * δ i ≤ ∑ j : ι, c i j * δ j) {d : ℕ → ι → S} (hd0 : ∀ (m : ℕ) (j : ι), 0 ≤ d m j) (h1 : ∀ (j : ι), ∑ i : ι, c i j * d 0 i ≤ d 1 j) (h2 : ∀ (m : ℕ) (j : ι), ∑ i : ι, c i j * d (m + 1) i ≤ d (m + 2) j + d m j) (m : ℕ) :
(↑m + 1) * ∑ j : ι, δ j * d 0 j ≤ ∑ j : ι, δ j * d m j

Linear growth of weighted sums under a second-order inequality. If d_m(j) ≥ 0 satisfy ∑_i c_{ij} d_0(i) ≤ d_1(j) and ∑_i c_{ij} d_{m+1}(i) ≤ d_{m+2}(j) + d_m(j), and a nonnegative weight δ satisfies 2 δ_i ≤ ∑_j c_{ij} δ_j, then the weighted sums s_m = ∑_j δ_j d_m(j) grow at least linearly: (m + 1) s_0 ≤ s_m.