refactor(analysis/convex/basic): generalize convexity to vector spaces (#9058)

`convex` and `convex_hull` are currently only defined in real vector spaces. This generalizes ℝ to arbitrary ordered_semirings in definitions and abstracts it away to the correct generality in lemmas. It also generalizes the space from `add_comm_group` to `add_comm_monoid` where possible.

Author: YaelDillies

src/analysis/calculus/darboux.lean

@@ -73,11 +73,11 @@ let ⟨c, cmem, hc⟩ := exists_has_deriv_within_at_eq_of_gt_of_lt hab (λ x hx,
 in ⟨c, cmem, neg_injective hc⟩
 
 /-- **Darboux's theorem**: the image of a convex set under `f'` is a convex set. -/
-theorem convex_image_has_deriv_at {s : set ℝ} (hs : convex s)
+theorem convex_image_has_deriv_at {s : set ℝ} (hs : convex ℝ s)
   (hf : ∀ x ∈ s, has_deriv_at f (f' x) x) :
-  convex (f' '' s) :=
+  convex ℝ (f' '' s) :=
 begin
-  refine real.convex_iff_ord_connected.2 ⟨_⟩,
+  refine ord_connected.convex ⟨_⟩,
   rintros _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩ m ⟨hma, hmb⟩,
   cases eq_or_lt_of_le hma with hma hma,
     by exact hma ▸ mem_image_of_mem f' ha,
@@ -98,7 +98,7 @@ end
 
 /-- If the derivative of a function is never equal to `m`, then either
 it is always greater than `m`, or it is always less than `m`. -/
-theorem deriv_forall_lt_or_forall_gt_of_forall_ne {s : set ℝ} (hs : convex s)
+theorem deriv_forall_lt_or_forall_gt_of_forall_ne {s : set ℝ} (hs : convex ℝ s)
   (hf : ∀ x ∈ s, has_deriv_at f (f' x) x) {m : ℝ} (hf' : ∀ x ∈ s, f' x ≠ m) :
   (∀ x ∈ s, f' x < m) ∨ (∀ x ∈ s, m < f' x) :=
 begin

src/analysis/calculus/extend_deriv.lean

@@ -31,7 +31,7 @@ local attribute [mono] prod_mono
 derivative converges to a limit `f'` at a point on the boundary, then `f` is differentiable there
 with derivative `f'`. -/
 theorem has_fderiv_at_boundary_of_tendsto_fderiv {f : E → F} {s : set E} {x : E} {f' : E →L[ℝ] F}
-  (f_diff : differentiable_on ℝ f s) (s_conv : convex s) (s_open : is_open s)
+  (f_diff : differentiable_on ℝ f s) (s_conv : convex ℝ s) (s_open : is_open s)
   (f_cont : ∀y ∈ closure s, continuous_within_at f s y)
   (h : tendsto (λy, fderiv ℝ f y) (𝓝[s] x) (𝓝 f')) :
   has_fderiv_within_at f f' (closure s) x :=
@@ -63,7 +63,7 @@ begin
   have key : ∀ p : E × E, p ∈ (B ∩ s).prod (B ∩ s) → ∥f p.2 - f p.1 - (f' p.2 - f' p.1)∥
     ≤ ε * ∥p.2 - p.1∥,
   { rintros ⟨u, v⟩ ⟨u_in, v_in⟩,
-    have conv : convex (B ∩ s) := (convex_ball _ _).inter s_conv,
+    have conv : convex ℝ (B ∩ s) := (convex_ball _ _).inter s_conv,
     have diff : differentiable_on ℝ f (B ∩ s) := f_diff.mono (inter_subset_right _ _),
     have bound : ∀ z ∈ (B ∩ s), ∥fderiv_within ℝ f (B ∩ s) z - f'∥ ≤ ε,
     { intros z z_in,
@@ -111,7 +111,7 @@ begin
   let t := Ioo a b,
   have ts : t ⊆ s := subset.trans Ioo_subset_Ioc_self sab,
   have t_diff : differentiable_on ℝ f t := f_diff.mono ts,
-  have t_conv : convex t := convex_Ioo a b,
+  have t_conv : convex ℝ t := convex_Ioo a b,
   have t_open : is_open t := is_open_Ioo,
   have t_closure : closure t = Icc a b := closure_Ioo ab,
   have t_cont : ∀y ∈ closure t, continuous_within_at f t y,
@@ -148,7 +148,7 @@ begin
   let t := Ioo b a,
   have ts : t ⊆ s := subset.trans Ioo_subset_Ico_self sab,
   have t_diff : differentiable_on ℝ f t := f_diff.mono ts,
-  have t_conv : convex t := convex_Ioo b a,
+  have t_conv : convex ℝ t := convex_Ioo b a,
   have t_open : is_open t := is_open_Ioo,
   have t_closure : closure t = Icc b a := closure_Ioo ba,
   have t_cont : ∀y ∈ closure t, continuous_within_at f t y,

src/analysis/calculus/fderiv_symmetric.lean

@@ -52,7 +52,7 @@ open_locale topological_space
 
 variables {E F : Type*} [normed_group E] [normed_space ℝ E]
 [normed_group F] [normed_space ℝ F]
-{s : set E} (s_conv : convex s)
+{s : set E} (s_conv : convex ℝ s)
 {f : E → F} {f' : E → (E →L[ℝ] F)} {f'' : E →L[ℝ] (E →L[ℝ] F)}
 (hf : ∀ x ∈ interior s, has_fderiv_at f (f' x) x)
 {x : E} (xs : x ∈ s) (hx : has_fderiv_within_at f' f'' (interior s) x)
@@ -283,7 +283,7 @@ omit s_conv xs hx hf
 /-- If a function is differentiable inside a convex set with nonempty interior, and has a second
 derivative at a point of this convex set, then this second derivative is symmetric. -/
 theorem convex.second_derivative_within_at_symmetric
-  {s : set E} (s_conv : convex s) (hne : (interior s).nonempty)
+  {s : set E} (s_conv : convex ℝ s) (hne : (interior s).nonempty)
   {f : E → F} {f' : E → (E →L[ℝ] F)} {f'' : E →L[ℝ] (E →L[ℝ] F)}
   (hf : ∀ x ∈ interior s, has_fderiv_at f (f' x) x)
   {x : E} (xs : x ∈ s) (hx : has_fderiv_within_at f' f'' (interior s) x) (v w : E) :

src/analysis/calculus/mean_value.lean

@@ -368,7 +368,7 @@ unique_diff_on.pi _ _ _ _ $ λ i _, h i
 
 /-- In a real vector space, a convex set with nonempty interior is a set of unique
 differentiability. -/
-theorem unique_diff_on_convex {s : set G} (conv : convex s) (hs : (interior s).nonempty) :
+theorem unique_diff_on_convex {s : set G} (conv : convex ℝ s) (hs : (interior s).nonempty) :
   unique_diff_on ℝ s :=
 begin
   assume x xs,

src/analysis/calculus/tangent_cone.lean

@@ -2734,7 +2734,7 @@ and `∥p x 1∥₊ < K`, then `f` is `K`-Lipschitz in a neighborhood of `x` wit
 lemma has_ftaylor_series_up_to_on.exists_lipschitz_on_with_of_nnnorm_lt {E F : Type*}
   [normed_group E] [normed_space ℝ E] [normed_group F] [normed_space ℝ F] {f : E → F}
   {p : E → formal_multilinear_series ℝ E F} {s : set E} {x : E}
-  (hf : has_ftaylor_series_up_to_on 1 f p (insert x s)) (hs : convex s) (K : ℝ≥0)
+  (hf : has_ftaylor_series_up_to_on 1 f p (insert x s)) (hs : convex ℝ s) (K : ℝ≥0)
   (hK : ∥p x 1∥₊ < K) :
   ∃ t ∈ 𝓝[s] x, lipschitz_on_with K f t :=
 begin
@@ -2754,15 +2754,15 @@ then `f` is Lipschitz in a neighborhood of `x` within `s`. -/
 lemma has_ftaylor_series_up_to_on.exists_lipschitz_on_with {E F : Type*}
   [normed_group E] [normed_space ℝ E] [normed_group F] [normed_space ℝ F] {f : E → F}
   {p : E → formal_multilinear_series ℝ E F} {s : set E} {x : E}
-  (hf : has_ftaylor_series_up_to_on 1 f p (insert x s)) (hs : convex s) :
+  (hf : has_ftaylor_series_up_to_on 1 f p (insert x s)) (hs : convex ℝ s) :
   ∃ K (t ∈ 𝓝[s] x), lipschitz_on_with K f t :=
 (no_top _).imp $ hf.exists_lipschitz_on_with_of_nnnorm_lt hs
 
 /-- If `f` is `C^1` within a conves set `s` at `x`, then it is Lipschitz on a neighborhood of `x`
 within `s`. -/
 lemma times_cont_diff_within_at.exists_lipschitz_on_with {E F : Type*} [normed_group E]
   [normed_space ℝ E] [normed_group F] [normed_space ℝ F] {f : E → F} {s : set E}
-  {x : E} (hf : times_cont_diff_within_at ℝ 1 f s x) (hs : convex s) :
+  {x : E} (hf : times_cont_diff_within_at ℝ 1 f s x) (hs : convex ℝ s) :
   ∃ (K : ℝ≥0) (t ∈ 𝓝[s] x), lipschitz_on_with K f t :=
 begin
   rcases hf 1 le_rfl with ⟨t, hst, p, hp⟩,