Order estimates for sums and products of finite sequences

A nonnegative finite sequence in which every term is at most half of the previous one sums to at most twice its first term. In Roth's lemma this bounds the sum of the weights rᵢ by 2 r₀.

A nonnegative monotone sequence of length D * k bounds the D-th power of the product of k of its terms, the j-th of which is taken no later than position D * j. This converts bounds for vectors selected from an ordered family, such as a family of successive minima, into a bound by the product of the whole family.

Main results

• Fin.sum_le_two_mul_of_two_mul_succ_le: if 0 ≤ rᵢ and 2 rᵢ₊₁ ≤ rᵢ, then ∑ᵢ rᵢ ≤ 2 r₀.
• Fin.prod_pow_le_prod_of_monotone: if c is nonnegative and monotone on Fin (D * k) and s j ≤ D * j, then (∏ⱼ c (s j)) ^ D ≤ ∏ᵢ cᵢ.

theorem Fin.sum_le_two_mul_of_two_mul_succ_le {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] {n : ℕ} {r : Fin (n + 1) → R} (hr : ∀ (i : Fin (n + 1)), 0 ≤ r i) (h : ∀ (i : Fin n), 2 * r i.succ ≤ r i.castSucc) : ∑ i : Fin (n + 1), r i ≤ 2 * r 0

A nonnegative sequence whose terms at least halve at each step sums to at most twice its first term.

theorem Fin.prod_pow_le_prod_of_monotone {R : Type u_1} [CommMonoidWithZero R] [Preorder R] [ZeroLEOneClass R] [PosMulMono R] {D k : ℕ} {c : Fin (D * k) → R} (hc0 : ∀ (i : Fin (D * k)), 0 ≤ c i) (hc : Monotone c) {s : Fin k → Fin (D * k)} (hs : ∀ (j : Fin k), ↑(s j) ≤ D * ↑j) : (∏ j : Fin k, c (s j)) ^ D ≤ ∏ i : Fin (D * k), c i

Selecting k terms of a nonnegative monotone sequence of length D * k, the j-th at position at most D * j, the product of the selected terms raised to the power D is at most the product of the whole sequence: the j-th block of D consecutive terms bounds the D-th power of the j-th selected term from above.