refactor(analysis/convex/function): generalize definition of `convex_…

…on`/`concave_on` to allow any (ordered) scalars (#9389)

`convex_on` and `concave_on` are currently only defined for real vector spaces. This generalizes ℝ to an arbitrary `ordered_semiring` in the definition.

src/analysis/calculus/mean_value.lean

@@ -973,7 +973,7 @@ 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 ℝ D f :=
 convex_on_real_of_slope_mono_adjacent hD
 begin
   intros x y z hx hz hxy hyz,
@@ -999,7 +999,7 @@ and `f'` is antimonotone on the interior, then `f` is concave on `D`. -/
 theorem concave_on_of_deriv_antimono {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 y ≤ deriv f x) :
-  concave_on D f :=
+  concave_on ℝ D f :=
 begin
   have : ∀ x y ∈ interior D, x ≤ y → deriv (-f) x ≤ deriv (-f) y,
   { intros x y hx hy hxy,
@@ -1011,13 +1011,13 @@ end
 
 /-- If a function `f` is differentiable and `f'` is monotone on `ℝ` then `f` is convex. -/
 theorem convex_on_univ_of_deriv_mono {f : ℝ → ℝ} (hf : differentiable ℝ f)
-  (hf'_mono : monotone (deriv f)) : convex_on univ 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 differentiable and `f'` is antimonotone on `ℝ` then `f` is concave. -/
 theorem concave_on_univ_of_deriv_antimono {f : ℝ → ℝ} (hf : differentiable ℝ f)
-  (hf'_antimono : ∀⦃a b⦄, a ≤ b → (deriv f) b ≤ (deriv f) a) : concave_on univ f :=
+  (hf'_antimono : ∀⦃a b⦄, a ≤ b → (deriv f) b ≤ (deriv f) a) : concave_on ℝ univ f :=
 concave_on_of_deriv_antimono convex_univ hf.continuous.continuous_on hf.differentiable_on
   (λ x y _ _ h, hf'_antimono h)
 
@@ -1027,7 +1027,7 @@ 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 ℝ 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])
@@ -1039,7 +1039,7 @@ theorem concave_on_of_deriv2_nonpos {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''_nonpos : ∀ x ∈ interior D, (deriv^[2] f x) ≤ 0) :
-  concave_on D f :=
+  concave_on ℝ D f :=
 concave_on_of_deriv_antimono hD hf hf' $
 assume x y hx hy hxy,
 hD.interior.antimono_of_deriv_nonpos hf''.continuous_on (by rwa [interior_interior])
@@ -1049,31 +1049,31 @@ hD.interior.antimono_of_deriv_nonpos hf''.continuous_on (by rwa [interior_interi
 `f''` is nonnegative on `D`, then `f` is convex on `D`. -/
 theorem convex_on_open_of_deriv2_nonneg {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)) : convex_on D f :=
+  (hf''_nonneg : ∀ x ∈ D, 0 ≤ (deriv^[2] f x)) : convex_on ℝ D f :=
 convex_on_of_deriv2_nonneg 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 a open convex set `D ⊆ ℝ` and
 `f''` is nonpositive on `D`, then `f` is concave on `D`. -/
 theorem concave_on_open_of_deriv2_nonpos {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) : concave_on D f :=
+  (hf''_nonpos : ∀ x ∈ D, (deriv^[2] f x) ≤ 0) : concave_on ℝ D f :=
 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 `ℝ`, 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 ℝ univ f :=
 convex_on_open_of_deriv2_nonneg 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 nonpositive on `ℝ`,
 then `f` is concave on `ℝ`. -/
 theorem concave_on_univ_of_deriv2_nonpos {f : ℝ → ℝ} (hf' : differentiable ℝ f)
   (hf'' : differentiable ℝ (deriv f)) (hf''_nonpos : ∀ x, (deriv^[2] f x) ≤ 0) :
-  concave_on univ f :=
+  concave_on ℝ univ f :=
 concave_on_open_of_deriv2_nonpos convex_univ is_open_univ hf'.differentiable_on
   hf''.differentiable_on (λ x _, hf''_nonpos x)
 

src/analysis/convex/basic.lean

@@ -401,14 +401,14 @@ section ordered_semiring
 variables [ordered_semiring 𝕜]
 
 section add_comm_monoid
-variables [add_comm_monoid E] [module 𝕜 E] [add_comm_monoid F] [module 𝕜 F]
+variables [add_comm_monoid E]
 
 /-- Convexity of sets. -/
-def convex (s : set E) :=
+def convex [has_scalar 𝕜 E] (s : set E) :=
 ∀ ⦃x y : E⦄, x ∈ s → y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 →
   a • x + b • y ∈ s
 
-variables {𝕜} {s : set E}
+variables {𝕜} [module 𝕜 E] [add_comm_monoid F] [module 𝕜 F] {s : set E}
 
 lemma convex_iff_forall_pos :
   convex 𝕜 s ↔ ∀ ⦃x y⦄, x ∈ s → y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1

src/analysis/convex/exposed.lean

@@ -169,7 +169,7 @@ protected lemma is_extreme [normed_space ℝ E]  (hAB : is_exposed ℝ A B) :
 begin
   refine ⟨hAB.subset, λ x₁ x₂ hx₁A hx₂A x hxB hx, _⟩,
   obtain ⟨l, rfl⟩ := hAB ⟨x, hxB⟩,
-  have hl : convex_on univ l := l.to_linear_map.convex_on convex_univ,
+  have hl : convex_on ℝ univ l := l.to_linear_map.convex_on convex_univ,
   have hlx₁ := hxB.2 x₁ hx₁A,
   have hlx₂ := hxB.2 x₂ hx₂A,
   refine ⟨⟨hx₁A, λ y hy, _⟩, ⟨hx₂A, λ y hy, _⟩⟩,

src/analysis/convex/extrema.lean

@@ -27,7 +27,7 @@ open_locale classical
 Helper lemma for the more general case: `is_min_on.of_is_local_min_on_of_convex_on`.
 -/
 lemma is_min_on.of_is_local_min_on_of_convex_on_Icc {f : ℝ → β} {a b : ℝ} (a_lt_b : a < b)
-  (h_local_min : is_local_min_on f (Icc a b) a) (h_conv : convex_on (Icc a b) f) :
+  (h_local_min : is_local_min_on f (Icc a b) a) (h_conv : convex_on ℝ (Icc a b) f) :
   ∀ x ∈ Icc a b, f a ≤ f x :=
 begin
   by_contradiction H_cont,
@@ -61,7 +61,7 @@ end
 A local minimum of a convex function is a global minimum, restricted to a set `s`.
 -/
 lemma is_min_on.of_is_local_min_on_of_convex_on {f : E → β} {a : E}
-  (a_in_s : a ∈ s) (h_localmin : is_local_min_on f s a) (h_conv : convex_on s f) :
+  (a_in_s : a ∈ s) (h_localmin : is_local_min_on f s a) (h_conv : convex_on ℝ s f) :
   ∀ x ∈ s, f a ≤ f x :=
 begin
   by_contradiction H_cont,
@@ -92,18 +92,18 @@ end
 
 /-- A local maximum of a concave function is a global maximum, restricted to a set `s`. -/
 lemma is_max_on.of_is_local_max_on_of_concave_on {f : E → β} {a : E}
-  (a_in_s : a ∈ s) (h_localmax: is_local_max_on f s a) (h_conc : concave_on s f) :
+  (a_in_s : a ∈ s) (h_localmax: is_local_max_on f s a) (h_conc : concave_on ℝ s f) :
   ∀ x ∈ s, f x ≤ f a :=
 @is_min_on.of_is_local_min_on_of_convex_on
   _ (order_dual β) _ _ _ _ _ _ _ _ s f a a_in_s h_localmax h_conc
 
 /-- A local minimum of a convex function is a global minimum. -/
 lemma is_min_on.of_is_local_min_of_convex_univ {f : E → β} {a : E}
-  (h_local_min : is_local_min f a) (h_conv : convex_on univ f) : ∀ x, f a ≤ f x :=
+  (h_local_min : is_local_min f a) (h_conv : convex_on ℝ univ f) : ∀ x, f a ≤ f x :=
 λ x, (is_min_on.of_is_local_min_on_of_convex_on (mem_univ a)
         (is_local_min.on h_local_min univ) h_conv) x (mem_univ x)
 
 /-- A local maximum of a concave function is a global maximum. -/
 lemma is_max_on.of_is_local_max_of_convex_univ {f : E → β} {a : E}
-  (h_local_max : is_local_max f a) (h_conc : concave_on univ f) : ∀ x, f x ≤ f a :=
+  (h_local_max : is_local_max f a) (h_conc : concave_on ℝ univ f) : ∀ x, f x ≤ f a :=
 @is_min_on.of_is_local_min_of_convex_univ _ (order_dual β) _ _ _ _ _ _ _ _ f a h_local_max h_conc