Documentation

Verification.ConcaveFourPoint

← Mathematical handbook
theorem Verification.concave_monotone_four_point {f : ℝ → ℝ} (hf : ConcaveOn ℝ (Set.Ici 0) f) (hm : MonotoneOn f (Set.Ici 0)) {a b c d : ℝ} (ha : 0 ≤ a) (hab : a ≤ b) (hbd : b ≤ d) (hac : a ≤ c) (hs : a + d ≤ b + c) :
f a + f d ≤ f b + f c

Increasing concave functions preserve the ordered four-point inequality used for submodular logarithmic copula exponents.