feat(analysis/calculus/mean_value): more corollaries of the MVT (#1819)

* feat(analysis/calculus/mean_value): more corolaries of the MVT

* Fix compile, add "strict inequalities" versions of some theorems, add docs

* Update src/analysis/calculus/mean_value.lean

* Add theorems for `convex_on univ`

* Fix comments

* @sgouezel adds missing articles

Thanks a lot! We don't have them in Russian, so it's hard for me to put them right.

Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr>

* Update src/analysis/calculus/mean_value.lean

Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr>

* Add more `univ` versions

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

Author: 3 people

src/analysis/calculus/mean_value.lean

@@ -22,6 +22,19 @@ In this file we prove the following facts:
   Cauchy's Mean Value Theorem.
 
 * `exists_has_deriv_at_eq_slope` and `exists_deriv_eq_slope` : Lagrange's Mean Value Theorem.
+
+* `convex.image_sub_lt_mul_sub_of_deriv_lt`, `convex.mul_sub_lt_image_sub_of_lt_deriv`,
+  `convex.image_sub_le_mul_sub_of_deriv_le`, `convex.mul_sub_le_image_sub_of_le_deriv`,
+  if `∀ x, C (</≤/>/≥) (f' x)`, then `C * (y - x) (</≤/>/≥) (f y - f x)` whenever `x < y`.
+
+* `convex.mono_of_deriv_nonneg`, `convex.antimono_of_deriv_nonpos`,
+  `convex.strict_mono_of_deriv_pos`, `convex.strict_antimono_of_deriv_neg` :
+  if the derivative of a function is non-negative/non-positive/positive/negative, then
+  the function is monotone/monotonically decreasing/strictly monotone/strictly monotonically
+  decreasing.
+
+* `convex_on_of_deriv_mono`, `convex_on_of_deriv2_nonneg` : if the derivative of a function
+  is increasing or its second derivative is nonnegative, then the original function is convex.
 -/
 
 set_option class.instance_max_depth 120
@@ -162,6 +175,12 @@ have bound : ∀ x ∈ s, ∥fderiv_within ℝ f s x∥ ≤ 0,
 by simpa only [(dist_eq_norm _ _).symm, zero_mul, dist_le_zero, eq_comm]
   using hs.norm_image_sub_le_of_norm_deriv_le hf bound hx hy
 
+theorem is_const_of_fderiv_eq_zero {f : E → F} (hf : differentiable ℝ f)
+  (hf' : ∀ x, fderiv ℝ f x = 0) (x y : E) :
+  f x = f y :=
+convex_univ.is_const_of_fderiv_within_eq_zero hf.differentiable_on
+  (λ x _, by rw fderiv_within_univ; exact hf' x) trivial trivial
+
 /-! ### Functions `[a, b] → ℝ`. -/
 
 section interval
@@ -221,3 +240,229 @@ exists_has_deriv_at_eq_slope f (deriv f) hab hfc
   (λ x hx, ((hfd x hx).differentiable_at $ mem_nhds_sets is_open_Ioo hx).has_deriv_at)
 
 end interval
+
+/-- Let `f` be a function continuous on a convex (or, equivalently, connected) subset `D`
+of the real line. If `f` is differentiable on the interior of `D` and `C < f'`, then
+`f` grows faster than `C * x` on `D`, i.e., `C * (y - x) < f y - f x` whenever `x, y ∈ D`,
+`x < y`. -/
+theorem convex.mul_sub_lt_image_sub_of_lt_deriv {D : set ℝ} (hD : convex D) {f : ℝ → ℝ}
+  (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D))
+  {C} (hf'_gt : ∀ x ∈ interior D, C < deriv f x) :
+  ∀ x y ∈ D, x < y → C * (y - x) < f y - f x :=
+begin
+  assume x y hx hy hxy,
+  have hxyD : Icc x y ⊆ D, from convex_real_iff.1 hD hx hy,
+  have hxyD' : Ioo x y ⊆ interior D,
+    from subset_sUnion_of_mem ⟨is_open_Ioo, subset.trans Ioo_subset_Icc_self hxyD⟩,
+  obtain ⟨a, a_mem, ha⟩ : ∃ a ∈ Ioo x y, deriv f a = (f y - f x) / (y - x),
+    from exists_deriv_eq_slope f hxy (hf.mono hxyD) (hf'.mono hxyD'),
+  have : C < (f y - f x) / (y - x), by { rw [← ha], exact hf'_gt _ (hxyD' a_mem) },
+  exact (lt_div_iff (sub_pos.2 hxy)).1 this
+end
+
+/-- Let `f : ℝ → ℝ` be a differentiable function. If `C < f'`, then `f` grows faster than
+`C * x`, i.e., `C * (y - x) < f y - f x` whenever `x < y`. -/
+theorem mul_sub_lt_image_sub_of_lt_deriv {f : ℝ → ℝ} (hf : differentiable ℝ f)
+  {C} (hf'_gt : ∀ x, C < deriv f x) ⦃x y⦄ (hxy : x < y) :
+  C * (y - x) < f y - f x :=
+convex_univ.mul_sub_lt_image_sub_of_lt_deriv hf.continuous.continuous_on hf.differentiable_on
+  (λ x _, hf'_gt x) x y trivial trivial hxy
+
+/-- Let `f` be a function continuous on a convex (or, equivalently, connected) subset `D`
+of the real line. If `f` is differentiable on the interior of `D` and `C ≤ f'`, then
+`f` grows at least as fast as `C * x` on `D`, i.e., `C * (y - x) ≤ f y - f x` whenever `x, y ∈ D`,
+`x ≤ y`. -/
+theorem convex.mul_sub_le_image_sub_of_le_deriv {D : set ℝ} (hD : convex D) {f : ℝ → ℝ}
+  (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D))
+  {C} (hf'_ge : ∀ x ∈ interior D, C ≤ deriv f x) :
+  ∀ x y ∈ D, x ≤ y → C * (y - x) ≤ f y - f x :=
+begin
+  assume x y hx hy hxy,
+  cases eq_or_lt_of_le hxy with hxy' hxy', by rw [hxy', sub_self, sub_self, mul_zero],
+  have hxyD : Icc x y ⊆ D, from convex_real_iff.1 hD hx hy,
+  have hxyD' : Ioo x y ⊆ interior D,
+    from subset_sUnion_of_mem ⟨is_open_Ioo, subset.trans Ioo_subset_Icc_self hxyD⟩,
+  obtain ⟨a, a_mem, ha⟩ : ∃ a ∈ Ioo x y, deriv f a = (f y - f x) / (y - x),
+    from exists_deriv_eq_slope f hxy' (hf.mono hxyD) (hf'.mono hxyD'),
+  have : C ≤ (f y - f x) / (y - x), by { rw [← ha], exact hf'_ge _ (hxyD' a_mem) },
+  exact (le_div_iff (sub_pos.2 hxy')).1 this
+end
+
+/-- Let `f : ℝ → ℝ` be a differentiable function. If `C ≤ f'`, then `f` grows at least as fast
+as `C * x`, i.e., `C * (y - x) ≤ f y - f x` whenever `x ≤ y`. -/
+theorem mul_sub_le_image_sub_of_le_deriv {f : ℝ → ℝ} (hf : differentiable ℝ f)
+  {C} (hf'_ge : ∀ x, C ≤ deriv f x) ⦃x y⦄ (hxy : x ≤ y) :
+  C * (y - x) ≤ f y - f x :=
+convex_univ.mul_sub_le_image_sub_of_le_deriv hf.continuous.continuous_on hf.differentiable_on
+  (λ x _, hf'_ge x) x y trivial trivial hxy
+
+/-- Let `f` be a function continuous on a convex (or, equivalently, connected) subset `D`
+of the real line. If `f` is differentiable on the interior of `D` and `f' < C`, then
+`f` grows slower than `C * x` on `D`, i.e., `f y - f x < C * (y - x)` whenever `x, y ∈ D`,
+`x < y`. -/
+theorem convex.image_sub_lt_mul_sub_of_deriv_lt {D : set ℝ} (hD : convex D) {f : ℝ → ℝ}
+  (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D))
+  {C} (lt_hf' : ∀ x ∈ interior D, deriv f x < C) :
+  ∀ x y ∈ D, x < y → f y - f x < C * (y - x) :=
+begin
+  assume x y hx hy hxy,
+  have hf'_gt : ∀ x ∈ interior D, -C < deriv (λ y, -f y) x,
+  { assume x hx,
+    rw [deriv_neg, neg_lt_neg_iff],
+    exact lt_hf' x hx },
+  simpa [-neg_lt_neg_iff]
+    using neg_lt_neg (hD.mul_sub_lt_image_sub_of_lt_deriv hf.neg hf'.neg hf'_gt x y hx hy hxy)
+end
+
+/-- Let `f : ℝ → ℝ` be a differentiable function. If `f' < C`, then `f` grows slower than
+`C * x` on `D`, i.e., `f y - f x < C * (y - x)` whenever `x < y`. -/
+theorem image_sub_lt_mul_sub_of_deriv_lt {f : ℝ → ℝ} (hf : differentiable ℝ f)
+  {C} (lt_hf' : ∀ x, deriv f x < C) ⦃x y⦄ (hxy : x < y) :
+  f y - f x < C * (y - x) :=
+convex_univ.image_sub_lt_mul_sub_of_deriv_lt hf.continuous.continuous_on hf.differentiable_on
+  (λ x _, lt_hf' x) x y trivial trivial hxy
+
+/-- Let `f` be a function continuous on a convex (or, equivalently, connected) subset `D`
+of the real line. If `f` is differentiable on the interior of `D` and `f' ≤ C`, then
+`f` grows at most as fast as `C * x` on `D`, i.e., `f y - f x ≤ C * (y - x)` whenever `x, y ∈ D`,
+`x ≤ y`. -/
+theorem convex.image_sub_le_mul_sub_of_deriv_le {D : set ℝ} (hD : convex D) {f : ℝ → ℝ}
+  (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D))
+  {C} (le_hf' : ∀ x ∈ interior D, deriv f x ≤ C) :
+  ∀ x y ∈ D, x ≤ y → f y - f x ≤ C * (y - x) :=
+begin
+  assume x y hx hy hxy,
+  have hf'_ge : ∀ x ∈ interior D, -C ≤ deriv (λ y, -f y) x,
+  { assume x hx,
+    rw [deriv_neg, neg_le_neg_iff],
+    exact le_hf' x hx },
+  simpa [-neg_le_neg_iff]
+    using neg_le_neg (hD.mul_sub_le_image_sub_of_le_deriv hf.neg hf'.neg hf'_ge x y hx hy hxy)
+end
+
+/-- Let `f : ℝ → ℝ` be a differentiable function. If `f' ≤ C`, then `f` grows at most as fast
+as `C * x`, i.e., `f y - f x ≤ C * (y - x)` whenever `x ≤ y`. -/
+theorem image_sub_le_mul_sub_of_deriv_le {f : ℝ → ℝ} (hf : differentiable ℝ f)
+  {C} (le_hf' : ∀ x, deriv f x ≤ C) ⦃x y⦄ (hxy : x ≤ y) :
+  f y - f x ≤ C * (y - x) :=
+convex_univ.image_sub_le_mul_sub_of_deriv_le hf.continuous.continuous_on hf.differentiable_on
+  (λ x _, le_hf' x) x y trivial trivial hxy
+
+/-- Let `f` be a function continuous on a convex (or, equivalently, connected) subset `D`
+of the real line. If `f` is differentiable on the interior of `D` and `f'` is positive, then
+`f` is a strictly monotonically increasing function on `D`. -/
+theorem convex.strict_mono_of_deriv_pos {D : set ℝ} (hD : convex D) {f : ℝ → ℝ}
+  (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D))
+  (hf'_pos : ∀ x ∈ interior D, 0 < deriv f x) :
+  ∀ x y ∈ D, x < y → f x < f y :=
+by simpa only [zero_mul, sub_pos] using hD.mul_sub_lt_image_sub_of_lt_deriv hf hf' hf'_pos
+
+/-- Let `f : ℝ → ℝ` be a differentiable function. If `f'` is positive, then
+`f` is a strictly monotonically increasing function. -/
+theorem strict_mono_of_deriv_pos {f : ℝ → ℝ} (hf : differentiable ℝ f)
+  (hf'_pos : ∀ x, 0 < deriv f x) :
+  strict_mono f :=
+λ x y hxy, convex_univ.strict_mono_of_deriv_pos hf.continuous.continuous_on hf.differentiable_on
+  (λ x _, hf'_pos x) x y trivial trivial hxy
+
+/-- Let `f` be a function continuous on a convex (or, equivalently, connected) subset `D`
+of the real line. If `f` is differentiable on the interior of `D` and `f'` is nonnegative, then
+`f` is a monotonically increasing function on `D`. -/
+theorem convex.mono_of_deriv_nonneg {D : set ℝ} (hD : convex D) {f : ℝ → ℝ}
+  (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D))
+  (hf'_nonneg : ∀ x ∈ interior D, 0 ≤ deriv f x) :
+  ∀ x y ∈ D, x ≤ y → f x ≤ f y :=
+by simpa only [zero_mul, sub_nonneg] using hD.mul_sub_le_image_sub_of_le_deriv hf hf' hf'_nonneg
+
+/-- Let `f : ℝ → ℝ` be a differentiable function. If `f'` is nonnegative, then
+`f` is a monotonically increasing function. -/
+theorem mono_of_deriv_nonneg {f : ℝ → ℝ} (hf : differentiable ℝ f) (hf' : ∀ x, 0 ≤ deriv f x) :
+  monotone f :=
+λ x y hxy, convex_univ.mono_of_deriv_nonneg hf.continuous.continuous_on hf.differentiable_on
+  (λ x _, hf' x) x y trivial trivial hxy
+
+/-- Let `f` be a function continuous on a convex (or, equivalently, connected) subset `D`
+of the real line. If `f` is differentiable on the interior of `D` and `f'` is negative, then
+`f` is a strictly monotonically decreasing function on `D`. -/
+theorem convex.strict_antimono_of_deriv_neg {D : set ℝ} (hD : convex D) {f : ℝ → ℝ}
+  (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D))
+  (hf'_neg : ∀ x ∈ interior D, deriv f x < 0) :
+  ∀ x y ∈ D, x < y → f y < f x :=
+by simpa only [zero_mul, sub_lt_zero] using hD.image_sub_lt_mul_sub_of_deriv_lt hf hf' hf'_neg
+
+/-- Let `f : ℝ → ℝ` be a differentiable function. If `f'` is negative, then
+`f` is a strictly monotonically decreasing function. -/
+theorem strict_antimono_of_deriv_neg {f : ℝ → ℝ} (hf : differentiable ℝ f)
+  (hf' : ∀ x, deriv f x < 0) :
+  ∀ ⦃x y⦄, x < y → f y < f x :=
+λ x y hxy, convex_univ.strict_antimono_of_deriv_neg hf.continuous.continuous_on hf.differentiable_on
+  (λ x _, hf' x) x y trivial trivial hxy
+
+/-- Let `f` be a function continuous on a convex (or, equivalently, connected) subset `D`
+of the real line. If `f` is differentiable on the interior of `D` and `f'` is nonpositive, then
+`f` is a monotonically decreasing function on `D`. -/
+theorem convex.antimono_of_deriv_nonpos {D : set ℝ} (hD : convex D) {f : ℝ → ℝ}
+  (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D))
+  (hf'_nonpos : ∀ x ∈ interior D, deriv f x ≤ 0) :
+  ∀ x y ∈ D, x ≤ y → f y ≤ f x :=
+by simpa only [zero_mul, sub_nonpos] using hD.image_sub_le_mul_sub_of_deriv_le hf hf' hf'_nonpos
+
+/-- Let `f : ℝ → ℝ` be a differentiable function. If `f'` is nonpositive, then
+`f` is a monotonically decreasing function. -/
+theorem antimono_of_deriv_nonpos {f : ℝ → ℝ} (hf : differentiable ℝ f) (hf' : ∀ x, deriv f x ≤ 0) :
+  ∀ ⦃x y⦄, x ≤ y → f y ≤ f x :=
+λ x y hxy, convex_univ.antimono_of_deriv_nonpos hf.continuous.continuous_on hf.differentiable_on
+  (λ x _, hf' x) x y trivial trivial hxy
+
+/-- If a function `f` is continuous on a convex set `D ⊆ ℝ`, is differentiable on its interior,
+and `f'` is monotone on the interior, then `f` is convex on `D`. -/
+theorem convex_on_of_deriv_mono {D : set ℝ} (hD : convex D) {f : ℝ → ℝ}
+  (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D))
+  (hf'_mono : ∀ x y ∈ interior D, x ≤ y → deriv f x ≤ deriv f y) :
+  convex_on D f :=
+convex_on_real_of_slope_mono_adjacent hD
+begin
+  intros x y z hx hz hxy hyz,
+  -- First we prove some trivial inclusions
+  have hxzD : Icc x z ⊆ D, from convex_real_iff.1 hD hx hz,
+  have hxyD : Icc x y ⊆ D, from subset.trans (Icc_subset_Icc_right $ le_of_lt hyz) hxzD,
+  have hxyD' : Ioo x y ⊆ interior D,
+    from subset_sUnion_of_mem ⟨is_open_Ioo, subset.trans Ioo_subset_Icc_self hxyD⟩,
+  have hyzD : Icc y z ⊆ D, from subset.trans (Icc_subset_Icc_left $ le_of_lt hxy) hxzD,
+  have hyzD' : Ioo y z ⊆ interior D,
+    from subset_sUnion_of_mem ⟨is_open_Ioo, subset.trans Ioo_subset_Icc_self hyzD⟩,
+  -- Then we apply MVT to both `[x, y]` and `[y, z]`
+  obtain ⟨a, ⟨hxa, hay⟩, ha⟩ : ∃ a ∈ Ioo x y, deriv f a = (f y - f x) / (y - x),
+    from exists_deriv_eq_slope f hxy (hf.mono hxyD) (hf'.mono hxyD'),
+  obtain ⟨b, ⟨hyb, hbz⟩, hb⟩ : ∃ b ∈ Ioo y z, deriv f b = (f z - f y) / (z - y),
+    from exists_deriv_eq_slope f hyz (hf.mono hyzD) (hf'.mono hyzD'),
+  rw [← ha, ← hb],
+  exact hf'_mono a b (hxyD' ⟨hxa, hay⟩) (hyzD' ⟨hyb, hbz⟩) (le_of_lt $ lt_trans hay hyb)
+end
+
+/-- If a function `f` is continuous on a convex set `D ⊆ ℝ`, is differentiable on its interior,
+and `f'` is monotone on the interior, then `f` is convex on `ℝ`. -/
+theorem convex_on_univ_of_deriv_mono {f : ℝ → ℝ} (hf : differentiable ℝ f)
+  (hf'_mono : monotone (deriv f)) : convex_on univ f :=
+convex_on_of_deriv_mono convex_univ hf.continuous.continuous_on hf.differentiable_on
+  (λ x y _ _ h, hf'_mono h)
+
+/-- If a function `f` is continuous on a convex set `D ⊆ ℝ`, is twice differentiable on its interior,
+and `f''` is nonnegative on the interior, then `f` is convex on `D`. -/
+theorem convex_on_of_deriv2_nonneg {D : set ℝ} (hD : convex D) {f : ℝ → ℝ}
+  (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D))
+  (hf'' : differentiable_on ℝ (deriv f) (interior D))
+  (hf''_nonneg : ∀ x ∈ interior D, 0 ≤ (deriv^[2] f x)) :
+  convex_on D f :=
+convex_on_of_deriv_mono hD hf hf' $
+assume x y hx hy hxy,
+hD.interior.mono_of_deriv_nonneg hf''.continuous_on (by rwa [interior_interior])
+  (by rwa [interior_interior]) _ _ hx hy hxy
+
+/-- If a function `f` is twice differentiable on `ℝ`, and `f''` is nonnegative on `ℝ`,
+then `f` is convex on `ℝ`. -/
+theorem convex_on_univ_of_deriv2_nonneg {f : ℝ → ℝ} (hf' : differentiable ℝ f)
+  (hf'' : differentiable ℝ (deriv f)) (hf''_nonneg : ∀ x, 0 ≤ (deriv^[2] f x)) :
+  convex_on univ f :=
+convex_on_of_deriv2_nonneg convex_univ hf'.continuous.continuous_on hf'.differentiable_on
+  hf''.differentiable_on (λ x _, hf''_nonneg x)

src/analysis/convex.lean

@@ -412,18 +412,54 @@ begin
   simpa [hab, zero_lt_one] using h hx hy ha hb,
 end⟩
 
-lemma convex_on_linorder [linear_order α] {f : α → ℝ} : convex_on D f ↔
-  convex D ∧ ∀ {x y : α} {a b : ℝ}, x ∈ D → y ∈ D → x < y → 0 ≤ a → 0 ≤ b → a + b = 1 →
-    f (a • x + b • y) ≤ a * f x + b * f y :=
+/-- For a function on a convex set in a linear ordered space, in order to prove that it is convex
+it suffices to verify the inequality `f (a • x + b • y) ≤ a * f x + b * f y` only for `x < y`
+and positive `a`, `b`. The main use case is `α = ℝ` however one can apply it, e.g., to `ℝ^n` with
+lexicographic order. -/
+lemma linear_order.convex_on_of_lt [linear_order α] {f : α → ℝ} (hD : convex D)
+  (hf : ∀ {x y : α} {a b : ℝ}, x ∈ D → y ∈ D → x < y → 0 < a → 0 < b → a + b = 1 →
+    f (a • x + b • y) ≤ a * f x + b * f y) : convex_on D f :=
 begin
-  refine and_congr iff.rfl ⟨_, _⟩; intros h x y a b hx hy,
-  { intro hxy, exact h hx hy },
-  { intros ha hb hab,
-    wlog hxy : x<=y using [x y a b, y x b a],
-    exact le_total _ _,
-    apply or.elim (lt_or_eq_of_le hxy),
-    { intros hxy, exact h hx hy hxy ha hb hab },
-    { intros hxy, rw [hxy, ←add_smul, hab, one_smul, ←add_mul,hab,one_mul] } }
+  use hD,
+  intros x y a b hx hy ha hb hab,
+  wlog hxy : x<=y using [x y a b, y x b a],
+  { exact le_total _ _ },
+  { cases eq_or_lt_of_le hxy with hxy hxy,
+      by { subst y, rw [← add_smul, ← add_mul, hab, one_smul, one_mul] },
+    cases eq_or_lt_of_le ha with ha ha,
+      by { subst a, rw [zero_add] at hab, subst b, simp },
+    cases eq_or_lt_of_le hb with hb hb,
+      by { subst b, rw [add_zero] at hab, subst a, simp },
+    exact hf hx hy hxy ha hb hab }
+end
+
+/-- For a function `f` defined on a convex subset `D` of `ℝ`, if for any three points `x<y<z`
+the slope of the secant line of `f` on `[x, y]` is less than or equal to the slope
+of the secant line of `f` on `[x, z]`, then `f` is convex on `D`. This way of proving convexity
+of a function is used in the proof of convexity of a function with a monotone derivative. -/
+lemma convex_on_real_of_slope_mono_adjacent {D : set ℝ} (hD : convex D) {f : ℝ → ℝ}
+  (hf : ∀ {x y z : ℝ}, x ∈ D → z ∈ D → x < y → y < z →
+    (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)) :
+  convex_on D f :=
+linear_order.convex_on_of_lt hD
+begin
+  assume x z a b hx hz hxz ha hb hab,
+  let y := a * x + b * z,
+  have hxy : x < y,
+  { rw [← one_mul x, ← hab, add_mul],
+    exact add_lt_add_left ((mul_lt_mul_left hb).2 hxz) _ },
+  have hyz : y < z,
+  { rw [← one_mul z, ← hab, add_mul],
+    exact add_lt_add_right ((mul_lt_mul_left ha).2 hxz) _ },
+  have : (f y - f x) * (z - y) ≤ (f z - f y) * (y - x),
+    from (div_le_div_iff (sub_pos.2 hxy) (sub_pos.2 hyz)).1 (hf hx hz hxy hyz),
+  have A : z - y + (y - x) = z - x, by abel,
+  have B : 0 < z - x, from sub_pos.2 (lt_trans hxy hyz),
+  rw [sub_mul, sub_mul, sub_le_iff_le_add', ← add_sub_assoc, le_sub_iff_add_le, ← mul_add, A,
+    ← le_div_iff B, add_div, mul_div_assoc, mul_div_assoc,
+    mul_comm (f x), mul_comm (f z)] at this,
+  rw [eq_comm, ← sub_eq_iff_eq_add] at hab; subst a,
+  convert this; symmetry; simp only [div_eq_iff (ne_of_gt B), y]; ring
 end
 
 lemma convex_on.subset (h_convex_on : convex_on D f) (h_subset : A ⊆ D) (h_convex : convex A) :