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)
:
Increasing concave functions preserve the ordered four-point inequality used for submodular logarithmic copula exponents.