feat(analysis/convex/function): helper lemmas and general cleanup (#9438

)

This adds
* `convex_iff_pairwise_on_pos`
* `convex_on_iff_forall_pos`, `concave_on_iff_forall_pos`,
* `convex_on_iff_forall_pos_ne`, `concave_on_iff_forall_pos_ne`
* `convex_on.convex_strict_epigraph`, `concave_on.convex_strict_hypograph`

generalizes some instance assumptions:
* `convex_on.translate_` didn't need `module 𝕜 β` but `has_scalar 𝕜 β`.
* some proofs in `analysis.convex.exposed` were vestigially using `ℝ`.
 
and golfs proofs.

src/analysis/convex/basic.lean

@@ -507,6 +507,20 @@ begin
   exact h hx hy ha hb hab
 end
 
+lemma convex_iff_pairwise_on_pos :
+  convex 𝕜 s ↔ s.pairwise_on (λ x y, ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s) :=
+begin
+  refine ⟨λ h x hx y hy _ a b ha hb hab, h hx hy ha.le hb.le hab, _⟩,
+  intros h x y hx hy a b ha hb hab,
+  obtain rfl | ha' := ha.eq_or_lt,
+  { rw [zero_add] at hab, rwa [hab, zero_smul, one_smul, zero_add] },
+  obtain rfl | hb' := hb.eq_or_lt,
+  { rw [add_zero] at hab, rwa [hab, zero_smul, one_smul, add_zero] },
+  obtain rfl | hxy := eq_or_ne x y,
+  { rwa convex.combo_self hab },
+  exact h _ hx _ hy hxy ha' hb' hab,
+end
+
 lemma convex_iff_open_segment_subset :
   convex 𝕜 s ↔ ∀ ⦃x y⦄, x ∈ s → y ∈ s → open_segment 𝕜 x y ⊆ s :=
 begin

src/analysis/convex/exposed.lean

@@ -74,10 +74,10 @@ begin
   exact hx.1,
 end
 
-@[refl] lemma refl (A : set E) : is_exposed 𝕜 A A :=
+@[refl] protected lemma refl (A : set E) : is_exposed 𝕜 A A :=
 λ ⟨w, hw⟩, ⟨0, subset.antisymm (λ x hx, ⟨hx, λ y hy, by exact le_refl 0⟩) (λ x hx, hx.1)⟩
 
-lemma antisymm (hB : is_exposed 𝕜 A B) (hA : is_exposed 𝕜 B A) :
+protected lemma antisymm (hB : is_exposed 𝕜 A B) (hA : is_exposed 𝕜 B A) :
   A = B :=
 hA.subset.antisymm hB.subset
 
@@ -113,7 +113,7 @@ begin
     (λ x hx, ⟨hx.1, λ y hy, (hw.2 y hy).trans hx.2⟩)⟩,
 end
 
-lemma inter (hB : is_exposed 𝕜 A B) (hC : is_exposed 𝕜 A C) :
+protected lemma inter (hB : is_exposed 𝕜 A B) (hC : is_exposed 𝕜 A C) :
   is_exposed 𝕜 A (B ∩ C) :=
 begin
   rintro ⟨w, hwB, hwC⟩,
@@ -186,18 +186,18 @@ begin
   { 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_ge _
+    ((l.to_linear_map.concave_on convex_univ).convex_ge _
     ⟨mem_univ _, hx₁.2 y hy⟩ ⟨mem_univ _, hx₂.2 y hy⟩ ha hb hab).2⟩,
 end
 
-lemma is_closed [normed_space ℝ E] (hAB : is_exposed ℝ A B) (hA : is_closed A) :
+protected lemma is_closed [order_closed_topology 𝕜] (hAB : is_exposed 𝕜 A B) (hA : is_closed A) :
   is_closed B :=
 begin
   obtain ⟨l, a, rfl⟩ := hAB.eq_inter_halfspace,
   exact hA.is_closed_le continuous_on_const l.continuous.continuous_on,
 end
 
-lemma is_compact [normed_space ℝ E] (hAB : is_exposed ℝ A B) (hA : is_compact A) :
+protected lemma is_compact [order_closed_topology 𝕜] (hAB : is_exposed 𝕜 A B) (hA : is_compact A) :
   is_compact B :=
 compact_of_is_closed_subset hA (hAB.is_closed hA.is_closed) hAB.subset
 
@@ -237,7 +237,7 @@ begin
   exact ⟨hl.1.1, l, λ y hy, ⟨hl.1.2 y hy, λ hxy, hl.2 y ⟨hy, λ z hz, (hl.1.2 z hz).trans hxy⟩⟩⟩,
 end
 
-lemma exposed_points_subset_extreme_points [normed_space ℝ E] :
-  A.exposed_points ℝ ⊆ A.extreme_points ℝ :=
+lemma exposed_points_subset_extreme_points :
+  A.exposed_points 𝕜 ⊆ A.extreme_points 𝕜 :=
 λ x hx, mem_extreme_points_iff_extreme_singleton.2
   (mem_exposed_points_iff_exposed_singleton.1 hx).is_extreme