[Merged by Bors] - refactor(analysis/convex/function): generalize lemmas about convexity/concavity of functions, prove concave Jensen

src/analysis/calculus/mean_value.lean

@@ -974,7 +974,7 @@ 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
+convex_on_of_slope_mono_adjacent hD
 begin
   intros x y z hx hz hxy hyz,
   -- First we prove some trivial inclusions
@@ -1005,8 +1005,7 @@ begin
   { intros x y hx hy hxy,
     convert neg_le_neg (hf'_mono x y hx hy hxy);
     convert deriv.neg },
-  exact (neg_convex_on_iff D f).mp (convex_on_of_deriv_mono hD
-    hf.neg hf'.neg this),
+  exact neg_convex_on_iff.mp (convex_on_of_deriv_mono hD hf.neg hf'.neg this),
 end
 
 /-- If a function `f` is differentiable and `f'` is monotone on `ℝ` then `f` is convex. -/

src/analysis/convex/basic.lean

@@ -18,7 +18,7 @@ In a 𝕜-vector space, we define the following objects and properties.
 * `convex_hull 𝕜 s`: The minimal convex set that includes `s`. In order theory speak, this is a
   closure operator.
 * Standard simplex `std_simplex ι [fintype ι]` is the intersection of the positive quadrant with
-  the hyperplane `s.sum = 1` in the space `ι → ℝ`.
+  the hyperplane `s.sum = 1` in the space `ι → 𝕜`.
 
 We also provide various equivalent versions of the definitions above, prove that some specific sets
 are convex.
@@ -119,7 +119,7 @@ begin
   exact h (mem_open_segment_of_ne_left_right 𝕜 hxz hyz hz),
 end
 
-lemma convex.combo_self {x y : 𝕜} (h : x + y = 1) (a : 𝕜) : x • a + y • a = a :=
+lemma convex.combo_self {x y : 𝕜} (h : x + y = 1) (a : E) : x • a + y • a = a :=
 by rw [←add_smul, h, one_smul]
 
 end ordered_semiring

src/analysis/convex/combination.lean

@@ -26,9 +26,7 @@ open set
 open_locale big_operators classical
 
 universes u u'
-variables {R E F ι ι' : Type*}
-  [linear_ordered_field R] [add_comm_group E] [module R E] [add_comm_group F] [module R F]
-  {s : set E}
+variables {R E ι ι' : Type*} [linear_ordered_field R] [add_comm_monoid E] [module R E] {s : set E}
 
 /-- Center of mass of a finite collection of points with prescribed weights.
 Note that we require neither `0 ≤ w i` nor `∑ w = 1`. -/

src/analysis/convex/exposed.lean

@@ -164,12 +164,12 @@ begin
   exact hC.inter_left hCA,
 end
 
-protected lemma is_extreme [normed_space ℝ E]  (hAB : is_exposed ℝ A B) :
-  is_extreme ℝ A B :=
+protected lemma is_extreme (hAB : is_exposed 𝕜 A B) :
+  is_extreme 𝕜 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, _⟩⟩,
@@ -179,14 +179,14 @@ begin
     exact hxB.2 y hy }
 end
 
-protected lemma convex [normed_space ℝ E] (hAB : is_exposed ℝ A B) (hA : convex ℝ A) :
-  convex ℝ B :=
+protected lemma convex (hAB : is_exposed 𝕜 A B) (hA : convex 𝕜 A) :
+  convex 𝕜 B :=
 begin
   obtain rfl | hB := B.eq_empty_or_nonempty,
   { exact convex_empty },
   obtain ⟨l, rfl⟩ := hAB hB,
   exact λ x₁ x₂ hx₁ hx₂ a b ha hb hab, ⟨hA hx₁.1 hx₂.1 ha hb hab, λ y hy,
-    ((l.to_linear_map.concave_on convex_univ).concave_le _
+    ((l.to_linear_map.concave_on convex_univ).concave_ge _
     ⟨mem_univ _, hx₁.2 y hy⟩ ⟨mem_univ _, hx₂.2 y hy⟩ ha hb hab).2⟩,
 end