feat(analysis/calculus/mean_value): Strict convexity from derivatives (…

…#10034)

This duplicates all the results relating convex/concave function and their derivatives to strictly convex/strictly concave functions.

src/analysis/calculus/mean_value.lean

@@ -975,7 +975,7 @@ antitone_on_univ.1 $ convex_univ.antitone_on_of_deriv_nonpos hf.continuous.conti
 
 /-- 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_monotone_on {D : set ℝ} (hD : convex ℝ D) {f : ℝ → ℝ}
+theorem monotone_on.convex_on_of_deriv {D : set ℝ} (hD : convex ℝ D) {f : ℝ → ℝ}
   (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D))
   (hf'_mono : monotone_on (deriv f) (interior D)) :
   convex_on ℝ D f :=
@@ -1001,7 +1001,7 @@ end
 
 /-- If a function `f` is continuous on a convex set `D ⊆ ℝ`, is differentiable on its interior,
 and `f'` is antitone on the interior, then `f` is concave on `D`. -/
-theorem concave_on_of_deriv_antitone_on {D : set ℝ} (hD : convex ℝ D) {f : ℝ → ℝ}
+theorem antitone_on.concave_on_of_deriv {D : set ℝ} (hD : convex ℝ D) {f : ℝ → ℝ}
   (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D))
   (h_anti : antitone_on (deriv f) (interior D)) :
   concave_on ℝ D f :=
@@ -1010,20 +1010,75 @@ begin
   { intros x hx y hy hxy,
     convert neg_le_neg (h_anti hx hy hxy);
     convert deriv.neg },
-  exact neg_convex_on_iff.mp (convex_on_of_deriv_monotone_on hD hf.neg hf'.neg this),
+  exact neg_convex_on_iff.mp (this.convex_on_of_deriv hD hf.neg hf'.neg),
+end
+
+/-- If a function `f` is continuous on a convex set `D ⊆ ℝ`, is differentiable on its interior,
+and `f'` is strictly monotone on the interior, then `f` is strictly convex on `D`. -/
+lemma strict_mono_on.strict_convex_on_of_deriv {D : set ℝ} (hD : convex ℝ D) {f : ℝ → ℝ}
+  (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D))
+  (hf'_mono : strict_mono_on (deriv f) (interior D)) :
+  strict_convex_on ℝ D f :=
+strict_convex_on_of_slope_strict_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 hD.ord_connected.out 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 (hxyD' ⟨hxa, hay⟩) (hyzD' ⟨hyb, hbz⟩) (hay.trans hyb)
+end
+
+/-- If a function `f` is continuous on a convex set `D ⊆ ℝ`, is differentiable on its interior,
+and `f'` is strictly antitone on the interior, then `f` is strictly concave on `D`. -/
+lemma strict_anti_on.strict_concave_on_of_deriv {D : set ℝ} (hD : convex ℝ D) {f : ℝ → ℝ}
+  (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D))
+  (h_anti : strict_anti_on (deriv f) (interior D)) :
+  strict_concave_on ℝ D f :=
+begin
+  have : strict_mono_on (deriv (-f)) (interior D),
+  { intros x hx y hy hxy,
+    convert neg_lt_neg (h_anti hx hy hxy);
+    convert deriv.neg },
+  exact neg_strict_convex_on_iff.mp (this.strict_convex_on_of_deriv hD hf.neg hf'.neg),
 end
 
 /-- If a function `f` is differentiable and `f'` is monotone on `ℝ` then `f` is convex. -/
-theorem convex_on_univ_of_deriv_monotone {f : ℝ → ℝ} (hf : differentiable ℝ f)
+theorem monotone.convex_on_univ_of_deriv {f : ℝ → ℝ} (hf : differentiable ℝ f)
   (hf'_mono : monotone (deriv f)) : convex_on ℝ univ f :=
-convex_on_of_deriv_monotone_on convex_univ hf.continuous.continuous_on hf.differentiable_on
-  (hf'_mono.monotone_on _)
+(hf'_mono.monotone_on _).convex_on_of_deriv convex_univ hf.continuous.continuous_on
+  hf.differentiable_on
 
 /-- If a function `f` is differentiable and `f'` is antitone on `ℝ` then `f` is concave. -/
-theorem antitone.concave_on_univ {f : ℝ → ℝ} (hf : differentiable ℝ f)
+theorem antitone.concave_on_univ_of_deriv {f : ℝ → ℝ} (hf : differentiable ℝ f)
   (hf'_anti : antitone (deriv f)) : concave_on ℝ univ f :=
-concave_on_of_deriv_antitone_on convex_univ hf.continuous.continuous_on hf.differentiable_on
-  (hf'_anti.antitone_on _)
+(hf'_anti.antitone_on _).concave_on_of_deriv convex_univ hf.continuous.continuous_on
+  hf.differentiable_on
+
+/-- If a function `f` is differentiable and `f'` is strictly monotone on `ℝ` then `f` is strictly
+convex. -/
+lemma strict_mono.strict_convex_on_univ_of_deriv {f : ℝ → ℝ} (hf : differentiable ℝ f)
+  (hf'_mono : strict_mono (deriv f)) :
+  strict_convex_on ℝ univ f :=
+(hf'_mono.strict_mono_on _).strict_convex_on_of_deriv convex_univ hf.continuous.continuous_on
+  hf.differentiable_on
+
+/-- If a function `f` is differentiable and `f'` is strictly antitone on `ℝ` then `f` is strictly
+concave. -/
+lemma strict_anti.strict_concave_on_univ_of_deriv {f : ℝ → ℝ} (hf : differentiable ℝ f)
+  (hf'_anti : strict_anti (deriv f)) : strict_concave_on ℝ univ f :=
+(hf'_anti.strict_anti_on _).strict_concave_on_of_deriv convex_univ hf.continuous.continuous_on
+  hf.differentiable_on
 
 /-- 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`. -/
@@ -1032,8 +1087,8 @@ theorem convex_on_of_deriv2_nonneg {D : set ℝ} (hD : convex ℝ D) {f : ℝ 
   (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_monotone_on hD hf hf' $ hD.interior.monotone_on_of_deriv_nonneg
-  hf''.continuous_on (by rwa interior_interior) (by rwa interior_interior)
+(hD.interior.monotone_on_of_deriv_nonneg hf''.continuous_on (by rwa interior_interior)
+  $ by rwa interior_interior).convex_on_of_deriv hD hf hf'
 
 /-- If a function `f` is continuous on a convex set `D ⊆ ℝ`, is twice differentiable on its
 interior, and `f''` is nonpositive on the interior, then `f` is concave on `D`. -/
@@ -1042,8 +1097,28 @@ theorem concave_on_of_deriv2_nonpos {D : set ℝ} (hD : convex ℝ D) {f : ℝ 
   (hf'' : differentiable_on ℝ (deriv f) (interior D))
   (hf''_nonpos : ∀ x ∈ interior D, (deriv^[2] f x) ≤ 0) :
   concave_on ℝ D f :=
-concave_on_of_deriv_antitone_on hD hf hf' $ hD.interior.antitone_on_of_deriv_nonpos
-  hf''.continuous_on (by rwa interior_interior) (by rwa interior_interior)
+(hD.interior.antitone_on_of_deriv_nonpos hf''.continuous_on (by rwa interior_interior)
+  $ by rwa interior_interior).concave_on_of_deriv hD hf hf'
+
+/-- If a function `f` is continuous on a convex set `D ⊆ ℝ`, is twice differentiable on its
+interior, and `f''` is strictly positive on the interior, then `f` is strictly convex on `D`. -/
+lemma strict_convex_on_of_deriv2_pos {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''_pos : ∀ x ∈ interior D, 0 < (deriv^[2] f x)) :
+  strict_convex_on ℝ D f :=
+(hD.interior.strict_mono_on_of_deriv_pos hf''.continuous_on (by rwa interior_interior)
+  $ by rwa interior_interior).strict_convex_on_of_deriv hD hf hf'
+
+/-- If a function `f` is continuous on a convex set `D ⊆ ℝ`, is twice differentiable on its
+interior, and `f''` is strictly negative on the interior, then `f` is strictly concave on `D`. -/
+lemma strict_concave_on_of_deriv2_neg {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''_neg : ∀ x ∈ interior D, (deriv^[2] f x) < 0) :
+  strict_concave_on ℝ D f :=
+(hD.interior.strict_anti_on_of_deriv_neg hf''.continuous_on (by rwa interior_interior)
+  $ by rwa interior_interior).strict_concave_on_of_deriv hD hf hf'
 
 /-- If a function `f` is twice differentiable on a open convex set `D ⊆ ℝ` and
 `f''` is nonnegative on `D`, then `f` is convex on `D`. -/
@@ -1061,6 +1136,24 @@ theorem concave_on_open_of_deriv2_nonpos {D : set ℝ} (hD : convex ℝ D) (hD
 concave_on_of_deriv2_nonpos hD hf'.continuous_on (by simpa [hD₂.interior_eq] using hf')
   (by simpa [hD₂.interior_eq] using hf'') (by simpa [hD₂.interior_eq] using hf''_nonpos)
 
+/-- If a function `f` is twice differentiable on a open convex set `D ⊆ ℝ` and
+`f''` is strictly positive on `D`, then `f` is strictly convex on `D`. -/
+lemma strict_convex_on_open_of_deriv2_pos {D : set ℝ} (hD : convex ℝ D) (hD₂ : is_open D)
+  {f : ℝ → ℝ} (hf' : differentiable_on ℝ f D) (hf'' : differentiable_on ℝ (deriv f) D)
+  (hf''_nonneg : ∀ x ∈ D, 0 < (deriv^[2] f x)) :
+  strict_convex_on ℝ D f :=
+strict_convex_on_of_deriv2_pos hD hf'.continuous_on (by simpa [hD₂.interior_eq] using hf')
+  (by simpa [hD₂.interior_eq] using hf'') (by simpa [hD₂.interior_eq] using hf''_nonneg)
+
+/-- If a function `f` is twice differentiable on an open convex set `D ⊆ ℝ` and
+`f''` is strictly negative on `D`, then `f` is strictly concave on `D`. -/
+lemma strict_concave_on_open_of_deriv2_neg {D : set ℝ} (hD : convex ℝ D) (hD₂ : is_open D)
+  {f : ℝ → ℝ} (hf' : differentiable_on ℝ f D) (hf'' : differentiable_on ℝ (deriv f) D)
+  (hf''_nonpos : ∀ x ∈ D, (deriv^[2] f x) < 0) :
+  strict_concave_on ℝ D f :=
+strict_concave_on_of_deriv2_neg hD hf'.continuous_on (by simpa [hD₂.interior_eq] using hf')
+  (by simpa [hD₂.interior_eq] using hf'') (by simpa [hD₂.interior_eq] using hf''_nonpos)
+
 /-- 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)
@@ -1077,6 +1170,22 @@ theorem concave_on_univ_of_deriv2_nonpos {f : ℝ → ℝ} (hf' : differentiable
 concave_on_open_of_deriv2_nonpos convex_univ is_open_univ hf'.differentiable_on
   hf''.differentiable_on (λ x _, hf''_nonpos x)
 
+/-- If a function `f` is twice differentiable on `ℝ`, and `f''` is strictly positive on `ℝ`,
+then `f` is strictly convex on `ℝ`. -/
+lemma strict_convex_on_univ_of_deriv2_pos {f : ℝ → ℝ} (hf' : differentiable ℝ f)
+  (hf'' : differentiable ℝ (deriv f)) (hf''_nonneg : ∀ x, 0 < (deriv^[2] f x)) :
+  strict_convex_on ℝ univ f :=
+strict_convex_on_open_of_deriv2_pos convex_univ is_open_univ hf'.differentiable_on
+  hf''.differentiable_on (λ x _, hf''_nonneg x)
+
+/-- If a function `f` is twice differentiable on `ℝ`, and `f''` is strictly negative on `ℝ`,
+then `f` is strictly concave on `ℝ`. -/
+lemma strict_concave_on_univ_of_deriv2_neg {f : ℝ → ℝ} (hf' : differentiable ℝ f)
+  (hf'' : differentiable ℝ (deriv f)) (hf''_nonpos : ∀ x, (deriv^[2] f x) < 0) :
+  strict_concave_on ℝ univ f :=
+strict_concave_on_open_of_deriv2_neg convex_univ is_open_univ hf'.differentiable_on
+  hf''.differentiable_on (λ x _, hf''_nonpos x)
+
 /-! ### Functions `f : E → ℝ` -/
 
 /-- Lagrange's Mean Value Theorem, applied to convex domains. -/