From e7ea02fd0f23b434824935267721a2833b293f13 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Tue, 5 Oct 2021 10:10:29 +0000
Subject: [PATCH] feat(analysis/convex/basic): Levels of a monotone/antitone
 function (#9547)

The set of points whose image under a monotone function is less than a fixed value is convex, when the space is linear.
---
 src/analysis/convex/basic.lean | 96 ++++++++++++++++++++++++++++++++++
 1 file changed, 96 insertions(+)

diff --git a/src/analysis/convex/basic.lean b/src/analysis/convex/basic.lean
index 6d320eb69ff14..cf53da6024070 100644
--- a/src/analysis/convex/basic.lean
+++ b/src/analysis/convex/basic.lean
@@ -289,6 +289,28 @@ begin
 end
 
 end ordered_cancel_add_comm_monoid
+
+section linear_ordered_add_comm_monoid
+variables [linear_ordered_add_comm_monoid E] [module 𝕜 E] [ordered_smul 𝕜 E] {𝕜}
+
+lemma segment_subset_interval (x y : E) : [x -[𝕜] y] ⊆ interval x y :=
+begin
+  cases le_total x y,
+  { rw interval_of_le h,
+    exact segment_subset_Icc h },
+  { rw [interval_of_ge h, segment_symm],
+    exact segment_subset_Icc h }
+end
+
+lemma convex.min_le_combo (x y : E) {a b : 𝕜} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) :
+  min x y ≤ a • x + b • y :=
+(segment_subset_interval x y ⟨_, _, ha, hb, hab, rfl⟩).1
+
+lemma convex.combo_le_max (x y : E) {a b : 𝕜} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) :
+  a • x + b • y ≤ max x y :=
+(segment_subset_interval x y ⟨_, _, ha, hb, hab, rfl⟩).2
+
+end linear_ordered_add_comm_monoid
 end ordered_semiring
 
 section linear_ordered_field
@@ -667,6 +689,80 @@ end linear_ordered_add_comm_monoid
 end module
 end add_comm_monoid
 
+section linear_ordered_add_comm_monoid
+variables [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E]
+  [ordered_smul 𝕜 E] {s : set E} {f : E → β}
+
+lemma monotone_on.convex_le (hf : monotone_on f s) (hs : convex 𝕜 s) (r : β) :
+  convex 𝕜 {x ∈ s | f x ≤ r} :=
+λ x y hx hy a b ha hb hab, ⟨hs hx.1 hy.1 ha hb hab,
+  (hf (hs hx.1 hy.1 ha hb hab) (max_rec' s hx.1 hy.1) (convex.combo_le_max x y ha hb hab)).trans
+    (max_rec' _ hx.2 hy.2)⟩
+
+lemma monotone_on.convex_lt (hf : monotone_on f s) (hs : convex 𝕜 s) (r : β) :
+  convex 𝕜 {x ∈ s | f x < r} :=
+λ x y hx hy a b ha hb hab, ⟨hs hx.1 hy.1 ha hb hab,
+  (hf (hs hx.1 hy.1 ha hb hab) (max_rec' s hx.1 hy.1) (convex.combo_le_max x y ha hb hab)).trans_lt
+    (max_rec' _ hx.2 hy.2)⟩
+
+lemma monotone_on.convex_ge (hf : monotone_on f s) (hs : convex 𝕜 s) (r : β) :
+  convex 𝕜 {x ∈ s | r ≤ f x} :=
+@monotone_on.convex_le 𝕜 (order_dual E) (order_dual β) _ _ _ _ _ _ _ hf.dual hs r
+
+lemma monotone_on.convex_gt (hf : monotone_on f s) (hs : convex 𝕜 s) (r : β) :
+  convex 𝕜 {x ∈ s | r < f x} :=
+@monotone_on.convex_lt 𝕜 (order_dual E) (order_dual β) _ _ _ _ _ _ _ hf.dual hs r
+
+lemma antitone_on.convex_le (hf : antitone_on f s) (hs : convex 𝕜 s) (r : β) :
+  convex 𝕜 {x ∈ s | f x ≤ r} :=
+@monotone_on.convex_ge 𝕜 E (order_dual β) _ _ _ _ _ _ _ hf hs r
+
+lemma antitone_on.convex_lt (hf : antitone_on f s) (hs : convex 𝕜 s) (r : β) :
+  convex 𝕜 {x ∈ s | f x < r} :=
+@monotone_on.convex_gt 𝕜 E (order_dual β) _ _ _ _ _ _ _ hf hs r
+
+lemma antitone_on.convex_ge (hf : antitone_on f s) (hs : convex 𝕜 s) (r : β) :
+  convex 𝕜 {x ∈ s | r ≤ f x} :=
+@monotone_on.convex_le 𝕜 E (order_dual β) _ _ _ _ _ _ _ hf hs r
+
+lemma antitone_on.convex_gt (hf : antitone_on f s) (hs : convex 𝕜 s) (r : β) :
+  convex 𝕜 {x ∈ s | r < f x} :=
+@monotone_on.convex_lt 𝕜 E (order_dual β) _ _ _ _ _ _ _ hf hs r
+
+lemma monotone.convex_le (hf : monotone f) (r : β) :
+  convex 𝕜 {x | f x ≤ r} :=
+set.sep_univ.subst ((hf.monotone_on univ).convex_le convex_univ r)
+
+lemma monotone.convex_lt (hf : monotone f) (r : β) :
+  convex 𝕜 {x | f x ≤ r} :=
+set.sep_univ.subst ((hf.monotone_on univ).convex_le convex_univ r)
+
+lemma monotone.convex_ge (hf : monotone f ) (r : β) :
+  convex 𝕜 {x | r ≤ f x} :=
+set.sep_univ.subst ((hf.monotone_on univ).convex_ge convex_univ r)
+
+lemma monotone.convex_gt (hf : monotone f) (r : β) :
+  convex 𝕜 {x | f x ≤ r} :=
+set.sep_univ.subst ((hf.monotone_on univ).convex_le convex_univ r)
+
+lemma antitone.convex_le (hf : antitone f) (r : β) :
+  convex 𝕜 {x | f x ≤ r} :=
+set.sep_univ.subst ((hf.antitone_on univ).convex_le convex_univ r)
+
+lemma antitone.convex_lt (hf : antitone f) (r : β) :
+  convex 𝕜 {x | f x < r} :=
+set.sep_univ.subst ((hf.antitone_on univ).convex_lt convex_univ r)
+
+lemma antitone.convex_ge (hf : antitone f) (r : β) :
+  convex 𝕜 {x | r ≤ f x} :=
+set.sep_univ.subst ((hf.antitone_on univ).convex_ge convex_univ r)
+
+lemma antitone.convex_gt (hf : antitone f) (r : β) :
+  convex 𝕜 {x | r < f x} :=
+set.sep_univ.subst ((hf.antitone_on univ).convex_gt convex_univ r)
+
+end linear_ordered_add_comm_monoid
+
 section add_comm_group
 variables [add_comm_group E] [module 𝕜 E] {s t : set E}