refactor(analysis/convex/basic): generalize segments to vector spaces (…

…#9094)

`segment` and `open_segment` 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.

src/analysis/calculus/local_extr.lean

@@ -84,14 +84,14 @@ begin
   exact ⟨c, d, mem_of_superset hd $ λ h hn, hst hn, hc, hcd⟩
 end
 
-lemma mem_pos_tangent_cone_at_of_segment_subset {s : set E} {x y : E} (h : segment x y ⊆ s) :
+lemma mem_pos_tangent_cone_at_of_segment_subset {s : set E} {x y : E} (h : segment ℝ x y ⊆ s) :
   y - x ∈ pos_tangent_cone_at s x :=
 begin
   let c := λn:ℕ, (2:ℝ)^n,
   let d := λn:ℕ, (c n)⁻¹ • (y-x),
   refine ⟨c, d, filter.univ_mem' (λn, h _),
     tendsto_pow_at_top_at_top_of_one_lt one_lt_two, _⟩,
-  show x + d n ∈ segment x y,
+  show x + d n ∈ segment ℝ x y,
   { rw segment_eq_image',
     refine ⟨(c n)⁻¹, ⟨_, _⟩, rfl⟩,
     exacts [inv_nonneg.2 (pow_nonneg zero_le_two _),
@@ -103,7 +103,8 @@ begin
     exact pow_ne_zero _ two_ne_zero }
 end
 
-lemma mem_pos_tangent_cone_at_of_segment_subset' {s : set E} {x y : E} (h : segment x (x + y) ⊆ s) :
+lemma mem_pos_tangent_cone_at_of_segment_subset' {s : set E} {x y : E}
+  (h : segment ℝ x (x + y) ⊆ s) :
   y ∈ pos_tangent_cone_at s x :=
 by simpa only [add_sub_cancel'] using mem_pos_tangent_cone_at_of_segment_subset h
 

src/analysis/calculus/mean_value.lean

@@ -1083,12 +1083,12 @@ concave_on_open_of_deriv2_nonpos convex_univ is_open_univ hf'.differentiable_on
 theorem domain_mvt
   {f : E → ℝ} {s : set E} {x y : E} {f' : E → (E →L[ℝ] ℝ)}
   (hf : ∀ x ∈ s, has_fderiv_within_at f (f' x) s x) (hs : convex s) (xs : x ∈ s) (ys : y ∈ s) :
-  ∃ z ∈ segment x y, f y - f x = f' z (y - x) :=
+  ∃ z ∈ segment ℝ x y, f y - f x = f' z (y - x) :=
 begin
   have hIccIoo := @Ioo_subset_Icc_self ℝ _ 0 1,
 -- parametrize segment
   set g : ℝ → E := λ t, x + t • (y - x),
-  have hseg : ∀ t ∈ Icc (0:ℝ) 1, g t ∈ segment x y,
+  have hseg : ∀ t ∈ Icc (0:ℝ) 1, g t ∈ segment ℝ x y,
   { rw segment_eq_image',
     simp only [mem_image, and_imp, add_right_inj],
     intros t ht, exact ⟨t, ht, rfl⟩ },

src/analysis/calculus/tangent_cone.lean

@@ -208,13 +208,13 @@ end
 
 /-- If a subset of a real vector space contains a segment, then the direction of this
 segment belongs to the tangent cone at its endpoints. -/
-lemma mem_tangent_cone_of_segment_subset {s : set G} {x y : G} (h : segment x y ⊆ s) :
+lemma mem_tangent_cone_of_segment_subset {s : set G} {x y : G} (h : segment ℝ x y ⊆ s) :
   y - x ∈ tangent_cone_at ℝ s x :=
 begin
   let c := λn:ℕ, (2:ℝ)^n,
   let d := λn:ℕ, (c n)⁻¹ • (y-x),
   refine ⟨c, d, filter.univ_mem' (λn, h _), _, _⟩,
-  show x + d n ∈ segment x y,
+  show x + d n ∈ segment ℝ x y,
   { rw segment_eq_image,
     refine ⟨(c n)⁻¹, ⟨_, _⟩, _⟩,
     { rw inv_nonneg, apply pow_nonneg, norm_num },