← Mathematical handbook

theorem Verification.decreasing_weighted_sum_nonneg (f g : ℕ → ℝ) (n : ℕ) (hf : ∀ i < n - 1, f (i + 1) ≤ f i) (hg : ∀ k ≤ n, 0 ≤ ∑ i ∈ Finset.range k, g i) (ht : ∑ i ∈ Finset.range n, g i = 0) : 0 ≤ ∑ i ∈ Finset.range n, f i * g i

Summation by parts against a decreasing sequence and nonnegative partial sums.

theorem Verification.majorization_sum_sq (a b : ℕ → ℝ) (n : ℕ) (hb : ∀ i < n - 1, b (i + 1) ≤ b i) (hp : ∀ k ≤ n, ∑ i ∈ Finset.range k, b i ≤ ∑ i ∈ Finset.range k, a i) (ht : ∑ i ∈ Finset.range n, a i = ∑ i ∈ Finset.range n, b i) : ∑ i ∈ Finset.range n, b i ^ 2 ≤ ∑ i ∈ Finset.range n, a i ^ 2

The quadratic Karamata inequality needed in the checkerboard comparison.