← Mathematical handbook

Convex Karamata inequality from ordered partial sums

theorem Verification.convex_right_support {φ : ℝ → ℝ} (hφ : ConvexOn ℝ (Set.Icc 0 1) φ) {x y : ℝ} (hx : x ∈ Set.Ioo 0 1) (hy : y ∈ Set.Icc 0 1) : derivWithin φ (Set.Ioi x) x * (y - x) ≤ φ y - φ x

The right derivative supplies a supporting slope at every interior point.

theorem Verification.majorization_sum_convex_interior (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) (ha : ∀ i < n, a i ∈ Set.Icc 0 1) (hbi : ∀ i < n, b i ∈ Set.Ioo 0 1) (φ : ℝ → ℝ) (hφ : ConvexOn ℝ (Set.Icc 0 1) φ) : ∑ i ∈ Finset.range n, φ (b i) ≤ ∑ i ∈ Finset.range n, φ (a i)

An interior version; endpoint values will follow by continuity.

theorem Verification.majorization_sum_convex_unitInterval (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) (ha : ∀ i < n, a i ∈ Set.Icc 0 1) (hbi : ∀ i < n, b i ∈ Set.Icc 0 1) (φ : ℝ → ℝ) (hc : Continuous φ) (hφ : ConvexOn ℝ (Set.Icc 0 1) φ) : ∑ i ∈ Finset.range n, φ (b i) ≤ ∑ i ∈ Finset.range n, φ (a i)

Karamata's inequality on the full closed interval, including endpoint singularities of slopes.

theorem Verification.majorization_fin_sum_convex {n : ℕ} (a b : Fin n → ℝ) (hb : Antitone b) (hp : ∀ (k : Fin (n + 1)), (∑ i : Fin n, if ↑i < ↑k then b i else 0) ≤ ∑ i : Fin n, if ↑i < ↑k then a i else 0) (ht : ∑ i : Fin n, a i = ∑ i : Fin n, b i) (ha : ∀ (i : Fin n), a i ∈ Set.Icc 0 1) (hbi : ∀ (i : Fin n), b i ∈ Set.Icc 0 1) (φ : ℝ → ℝ) (hc : Continuous φ) (hφ : ConvexOn ℝ (Set.Icc 0 1) φ) : ∑ i : Fin n, φ (b i) ≤ ∑ i : Fin n, φ (a i)

Finite-index form used for equal-width copula sections.