Convexity lemmas

theorem ConcaveOn.le_add_deriv_mul {S : Set ℝ} {f : ℝ → ℝ} {x y : ℝ} (hfc : ConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hfd : DifferentiableAt ℝ f y) : f x ≤ f y + deriv f y * (x - y)

theorem ConvexOn.add_deriv_mul_le {S : Set ℝ} {f : ℝ → ℝ} {x y : ℝ} (hfc : ConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hfd : DifferentiableAt ℝ f y) : f y + deriv f y * (x - y) ≤ f x

theorem StrictConvexOn.add_deriv_mul_lt {S : Set ℝ} {f : ℝ → ℝ} {x y : ℝ} (hfc : StrictConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x ≠ y) (hfd : DifferentiableAt ℝ f y) : f y + deriv f y * (x - y) < f x

theorem strictConvexOn_inv_Ioi : StrictConvexOn ℝ (Set.Ioi 0) Inv.inv

theorem strictConvexOn_inv : StrictConvexOn ENNReal Set.univ Inv.inv

theorem convexOn_inv_Ioi : ConvexOn ℝ (Set.Ioi 0) Inv.inv

theorem convexOn_inv : ConvexOn ENNReal Set.univ Inv.inv

theorem ConcaveOn_log' : ConcaveOn ENNReal Set.univ ENNReal.log

theorem ConcaveOn_log : ConcaveOn NNReal Set.univ ENNReal.log