feat(Analysis/Convex/Function): composition of strictly and non-strictly convex functions (leanprover-community#40830)

We currently have composition lemmas for `StrictCon{vex/cave}On` of the form:
```lean
theorem StrictConvexOn.comp :
  StrictConvexOn 𝕜 (f '' s) g → StrictMonoOn g (f '' s) →
  StrictConvexOn 𝕜 s f → s.InjOn f →
  StrictConvexOn 𝕜 s (g ∘ f)
```
If we let either function be convex instead of strictly convex we get:
```lean
theorem ConvexOn.comp_strictConvexOn :
  ConvexOn 𝕜 (f '' s) g → StrictMonoOn g (f '' s) →
  StrictConvexOn 𝕜 s f →
  StrictConvexOn 𝕜 s (g ∘ f)

theorem StrictConvexOn.comp_convexOn :
  StrictConvexOn 𝕜 (f '' s) g → MonotoneOn g (f '' s) →
  ConvexOn 𝕜 s f → s.InjOn f →
  StrictConvexOn 𝕜 s (g ∘ f)
```
In a `Module` these are both stronger than the original version (since `StrictConvexOn` implies `ConvexOn`), but they work over any `SMul`.

Author: SnirBroshi

Mathlib/Analysis/Convex/Function.lean

@@ -166,23 +166,58 @@ theorem StrictConvexOn.comp (hg : StrictConvexOn 𝕜 (f '' s) g) (hf : StrictCo
           hf.2 hx hy hxy ha hb hab).trans <|
       hg.2 (mem_image_of_mem f hx) (mem_image_of_mem f hy) (mt (hf' hx hy) hxy) ha hb hab⟩
 
+theorem StrictConcaveOn.comp_strictConvexOn (hg : StrictConcaveOn 𝕜 (f '' s) g)
+    (hf : StrictConvexOn 𝕜 s f) (hg' : StrictAntiOn g (f '' s)) (hf' : s.InjOn f) :
+    StrictConcaveOn 𝕜 s (g ∘ f) :=
+  hg.dual.comp hf hg' hf'
+
 theorem StrictConcaveOn.comp (hg : StrictConcaveOn 𝕜 (f '' s) g) (hf : StrictConcaveOn 𝕜 s f)
     (hg' : StrictMonoOn g (f '' s)) (hf' : s.InjOn f) : StrictConcaveOn 𝕜 s (g ∘ f) :=
-  ⟨hf.1, fun _ hx _ hy hxy _ _ ha hb hab =>
-    (hg.2 (mem_image_of_mem f hx) (mem_image_of_mem f hy) (mt (hf' hx hy) hxy) ha hb hab).trans <|
-      hg' (hg.1 (mem_image_of_mem f hx) (mem_image_of_mem f hy) ha.le hb.le hab)
-          (mem_image_of_mem f <| hf.1 hx hy ha.le hb.le hab) <|
-        hf.2 hx hy hxy ha hb hab⟩
+  hg.comp_strictConvexOn (β := βᵒᵈ) hf hg'.dual hf'
 
 theorem StrictConvexOn.comp_strictConcaveOn (hg : StrictConvexOn 𝕜 (f '' s) g)
     (hf : StrictConcaveOn 𝕜 s f) (hg' : StrictAntiOn g (f '' s)) (hf' : s.InjOn f) :
     StrictConvexOn 𝕜 s (g ∘ f) :=
   hg.dual.comp hf hg' hf'
 
-theorem StrictConcaveOn.comp_strictConvexOn (hg : StrictConcaveOn 𝕜 (f '' s) g)
-    (hf : StrictConvexOn 𝕜 s f) (hg' : StrictAntiOn g (f '' s)) (hf' : s.InjOn f) :
-    StrictConcaveOn 𝕜 s (g ∘ f) :=
-  hg.dual.comp hf hg' hf'
+theorem ConvexOn.comp_strictConvexOn (hg : ConvexOn 𝕜 (f '' s) g) (hf : StrictConvexOn 𝕜 s f)
+    (hg' : StrictMonoOn g (f '' s)) : StrictConvexOn 𝕜 s (g ∘ f) := by
+  refine ⟨hf.left, fun x hx y hy hxy a b ha hb hab ↦ .trans_le (b := g (a • f x + b • f y)) ?_ ?_⟩
+  · refine hg' (mem_image_of_mem f <| hf.1 hx hy ha.le hb.le hab) ?_ <| hf.2 hx hy hxy ha hb hab
+    exact hg.left (mem_image_of_mem f hx) (mem_image_of_mem f hy) ha.le hb.le hab
+  · exact hg.right (mem_image_of_mem f hx) (mem_image_of_mem f hy) ha.le hb.le hab
+
+theorem ConcaveOn.comp_strictConvexOn (hg : ConcaveOn 𝕜 (f '' s) g) (hf : StrictConvexOn 𝕜 s f)
+    (hg' : StrictAntiOn g (f '' s)) : StrictConcaveOn 𝕜 s (g ∘ f) :=
+  hg.dual.comp_strictConvexOn hf hg'
+
+theorem ConcaveOn.comp_strictConcaveOn (hg : ConcaveOn 𝕜 (f '' s) g) (hf : StrictConcaveOn 𝕜 s f)
+    (hg' : StrictMonoOn g (f '' s)) : StrictConcaveOn 𝕜 s (g ∘ f) :=
+  hg.comp_strictConvexOn (β := βᵒᵈ) hf hg'.dual
+
+theorem ConvexOn.comp_strictConcaveOn (hg : ConvexOn 𝕜 (f '' s) g) (hf : StrictConcaveOn 𝕜 s f)
+    (hg' : StrictAntiOn g (f '' s)) : StrictConvexOn 𝕜 s (g ∘ f) :=
+  hg.dual.comp_strictConcaveOn hf hg'
+
+theorem StrictConvexOn.comp_convexOn (hg : StrictConvexOn 𝕜 (f '' s) g) (hf : ConvexOn 𝕜 s f)
+    (hg' : MonotoneOn g (f '' s)) (hf' : s.InjOn f) : StrictConvexOn 𝕜 s (g ∘ f) := by
+  refine ⟨hf.left, fun x hx y hy hxy a b ha hb hab ↦ .trans_le' (b := g (a • f x + b • f y)) ?_ ?_⟩
+  · exact hg.right (mem_image_of_mem f hx) (mem_image_of_mem f hy) (hf'.ne hx hy hxy) ha hb hab
+  · refine hg' ?_ ?_ <| hf.right hx hy ha.le hb.le hab
+    · exact mem_image_of_mem f <| hf.left hx hy ha.le hb.le hab
+    · exact hg.left (mem_image_of_mem f hx) (mem_image_of_mem f hy) ha.le hb.le hab
+
+theorem StrictConcaveOn.comp_convexOn (hg : StrictConcaveOn 𝕜 (f '' s) g) (hf : ConvexOn 𝕜 s f)
+    (hg' : AntitoneOn g (f '' s)) (hf' : s.InjOn f) : StrictConcaveOn 𝕜 s (g ∘ f) :=
+  hg.dual.comp_convexOn hf hg' hf'
+
+theorem StrictConvexOn.comp_concaveOn (hg : StrictConvexOn 𝕜 (f '' s) g) (hf : ConcaveOn 𝕜 s f)
+    (hg' : AntitoneOn g (f '' s)) (hf' : s.InjOn f) : StrictConvexOn 𝕜 s (g ∘ f) :=
+  hg.comp_convexOn (β := βᵒᵈ) hf hg'.dual hf'
+
+theorem StrictConcaveOn.comp_concaveOn (hg : StrictConcaveOn 𝕜 (f '' s) g) (hf : ConcaveOn 𝕜 s f)
+    (hg' : MonotoneOn g (f '' s)) (hf' : s.InjOn f) : StrictConcaveOn 𝕜 s (g ∘ f) :=
+  hg.dual.comp_concaveOn hf hg' hf'
 
 end SMul