← Mathematical handbook

theorem Verification.convex_rightDeriv_support (f : ℝ → ℝ) (hf : ConvexOn ℝ Set.univ f) (x y : ℝ) : f x + derivWithin f (Set.Ioi x) x * (y - x) ≤ f y

theorem Verification.majorization_sum_convex (a b : ℕ → ℝ) (n : ℕ) (f : ℝ → ℝ) (hf : ConvexOn ℝ Set.univ f) (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, f (b i) ≤ ∑ i ∈ Finset.range n, f (a i)

Full Karamata inequality. Only the comparison vector needs to be decreasing.