∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {f : ℝ → ℝ} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsProbabilityMeasure ν],
  ConvexOn ℝ (Set.Ici 0) f →
    ContinuousWithinAt f (Set.Ici 0) 0 →
      MeasureTheory.Integrable (fun x => f (μ.rnDeriv ν x).toReal) ν →
        μ.AbsolutelyContinuous ν → f (μ.real Set.univ) ≤ ∫ (x : α), f (μ.rnDeriv ν x).toReal ∂ν