feat: Extending convex functions (#6339)

Forward-ports leanprover-community/mathlib3#18797

The changes to `Mathlib.Data.Set.Intervals.Basic` were independently added to mathlib4 in `Mathlib.Data.Set.Intervals.Image`, so the `#align`s have been added there instead of the original file.



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Mathlib/Algebra/Order/Module.lean

@@ -5,7 +5,7 @@ Authors: Frédéric Dupuis, Yaël Dillies
 -/
 import Mathlib.Algebra.Order.SMul
 
-#align_import algebra.order.module from "leanprover-community/mathlib"@"9003f28797c0664a49e4179487267c494477d853"
+#align_import algebra.order.module from "leanprover-community/mathlib"@"3ba15165bd6927679be7c22d6091a87337e3cd0c"
 
 /-!
 # Ordered module
@@ -217,6 +217,19 @@ theorem BddAbove.smul_of_nonpos (hc : c ≤ 0) (hs : BddAbove s) : BddBelow (c 
 
 end OrderedRing
 
+section LinearOrderedRing
+variable [LinearOrderedRing k] [LinearOrderedAddCommGroup M] [Module k M] [OrderedSMul k M] {a : k}
+
+theorem smul_max_of_nonpos (ha : a ≤ 0) (b₁ b₂ : M) : a • max b₁ b₂ = min (a • b₁) (a • b₂) :=
+  (antitone_smul_left ha : Antitone (_ : M → M)).map_max
+#align smul_max_of_nonpos smul_max_of_nonpos
+
+theorem smul_min_of_nonpos (ha : a ≤ 0) (b₁ b₂ : M) : a • min b₁ b₂ = max (a • b₁) (a • b₂) :=
+  (antitone_smul_left ha : Antitone (_ : M → M)).map_min
+#align smul_min_of_nonpos smul_min_of_nonpos
+
+end LinearOrderedRing
+
 section LinearOrderedField
 
 variable [LinearOrderedField k] [OrderedAddCommGroup M] [Module k M] [OrderedSMul k M] {s : Set M}

Mathlib/Algebra/Order/Monoid/Lemmas.lean

@@ -9,7 +9,7 @@ import Mathlib.Init.Data.Ordering.Basic
 import Mathlib.Order.MinMax
 import Mathlib.Tactic.Contrapose
 
-#align_import algebra.order.monoid.lemmas from "leanprover-community/mathlib"@"2ed7e4aec72395b6a7c3ac4ac7873a7a43ead17c"
+#align_import algebra.order.monoid.lemmas from "leanprover-community/mathlib"@"3ba15165bd6927679be7c22d6091a87337e3cd0c"
 
 /-!
 # Ordered monoids
@@ -355,6 +355,27 @@ variable [LinearOrder α] {a b c d : α}
 #align min_le_max_of_add_le_add min_le_max_of_add_le_add
 #align min_le_max_of_mul_le_mul min_le_max_of_mul_le_mul
 
+end LinearOrder
+
+section LinearOrder
+variable [LinearOrder α] [CovariantClass α α (· * ·) (· ≤ ·)]
+  [CovariantClass α α (swap (· * ·)) (· ≤ ·)] {a b c d : α}
+
+@[to_additive max_add_add_le_max_add_max]
+theorem max_mul_mul_le_max_mul_max' : max (a * b) (c * d) ≤ max a c * max b d :=
+  max_le (mul_le_mul' (le_max_left _ _) <| le_max_left _ _) <|
+    mul_le_mul' (le_max_right _ _) <| le_max_right _ _
+#align max_mul_mul_le_max_mul_max' max_mul_mul_le_max_mul_max'
+#align max_add_add_le_max_add_max max_add_add_le_max_add_max
+
+--TODO: Also missing `min_mul_min_le_min_mul_mul`
+@[to_additive min_add_min_le_min_add_add]
+theorem min_mul_min_le_min_mul_mul' : min a c * min b d ≤ min (a * b) (c * d) :=
+  le_min (mul_le_mul' (min_le_left _ _) <| min_le_left _ _) <|
+    mul_le_mul' (min_le_right _ _) <| min_le_right _ _
+#align min_mul_min_le_min_mul_mul' min_mul_min_le_min_mul_mul'
+#align min_add_min_le_min_add_add min_add_min_le_min_add_add
+
 end LinearOrder
 end Mul
 

Mathlib/Algebra/Order/SMul.lean

@@ -11,7 +11,7 @@ import Mathlib.Data.Set.Pointwise.SMul
 import Mathlib.Tactic.GCongr.Core
 import Mathlib.Tactic.Positivity
 
-#align_import algebra.order.smul from "leanprover-community/mathlib"@"9003f28797c0664a49e4179487267c494477d853"
+#align_import algebra.order.smul from "leanprover-community/mathlib"@"3ba15165bd6927679be7c22d6091a87337e3cd0c"
 
 /-!
 # Ordered scalar product
@@ -186,12 +186,25 @@ instance Int.orderedSMul [LinearOrderedAddCommGroup M] : OrderedSMul ℤ M :=
     · cases (Int.negSucc_not_pos _).1 hn
 #align int.ordered_smul Int.orderedSMul
 
+section LinearOrderedSemiring
+variable [LinearOrderedSemiring R] [LinearOrderedAddCommMonoid M] [SMulWithZero R M]
+  [OrderedSMul R M] {a : R}
+
 -- TODO: `LinearOrderedField M → OrderedSMul ℚ M`
-instance LinearOrderedSemiring.toOrderedSMul {R : Type*} [LinearOrderedSemiring R] :
-    OrderedSMul R R :=
+instance LinearOrderedSemiring.toOrderedSMul : OrderedSMul R R :=
   OrderedSMul.mk'' fun _ => strictMono_mul_left_of_pos
 #align linear_ordered_semiring.to_ordered_smul LinearOrderedSemiring.toOrderedSMul
 
+theorem smul_max (ha : 0 ≤ a) (b₁ b₂ : M) : a • max b₁ b₂ = max (a • b₁) (a • b₂) :=
+  (monotone_smul_left ha : Monotone (_ : M → M)).map_max
+#align smul_max smul_max
+
+theorem smul_min (ha : 0 ≤ a) (b₁ b₂ : M) : a • min b₁ b₂ = min (a • b₁) (a • b₂) :=
+  (monotone_smul_left ha : Monotone (_ : M → M)).map_min
+#align smul_min smul_min
+
+end LinearOrderedSemiring
+
 section LinearOrderedSemifield
 
 variable [LinearOrderedSemifield 𝕜] [OrderedAddCommMonoid M] [OrderedAddCommMonoid N]

Mathlib/Data/Set/Intervals/Basic.lean

@@ -6,7 +6,7 @@ Authors: Johannes Hölzl, Mario Carneiro, Patrick Massot, Yury Kudryashov, Rémy
 import Mathlib.Order.MinMax
 import Mathlib.Data.Set.Prod
 
-#align_import data.set.intervals.basic from "leanprover-community/mathlib"@"4367b192b58a665b6f18773f73eb492eb4df7990"
+#align_import data.set.intervals.basic from "leanprover-community/mathlib"@"3ba15165bd6927679be7c22d6091a87337e3cd0c"
 
 /-!
 # Intervals

Mathlib/Data/Set/Intervals/Image.lean

@@ -110,6 +110,7 @@ lemma MonotoneOn.image_Iic_subset (h : MonotoneOn f (Iic b)) : f '' Iic b ⊆ Ii
 
 lemma MonotoneOn.image_Icc_subset (h : MonotoneOn f (Icc a b)) : f '' Icc a b ⊆ Icc (f a) (f b) :=
   h.mapsTo_Icc.image_subset
+#align monotone_on.image_Icc_subset MonotoneOn.image_Icc_subset
 
 lemma AntitoneOn.image_Ici_subset (h : AntitoneOn f (Ici a)) : f '' Ici a ⊆ Iic (f a) :=
   h.mapsTo_Ici.image_subset
@@ -119,6 +120,7 @@ lemma AntitoneOn.image_Iic_subset (h : AntitoneOn f (Iic b)) : f '' Iic b ⊆ Ic
 
 lemma AntitoneOn.image_Icc_subset (h : AntitoneOn f (Icc a b)) : f '' Icc a b ⊆ Icc (f b) (f a) :=
   h.mapsTo_Icc.image_subset
+#align antitone_on.image_Icc_subset AntitoneOn.image_Icc_subset
 
 lemma StrictMonoOn.image_Ioi_subset (h : StrictMonoOn f (Ici a)) : f '' Ioi a ⊆ Ioi (f a) :=
   h.mapsTo_Ioi.image_subset
@@ -146,6 +148,7 @@ lemma Monotone.image_Iic_subset (h : Monotone f) : f '' Iic b ⊆ Iic (f b) :=
 
 lemma Monotone.image_Icc_subset (h : Monotone f) : f '' Icc a b ⊆ Icc (f a) (f b) :=
   (h.monotoneOn _).image_Icc_subset
+#align monotone.image_Icc_subset Monotone.image_Icc_subset
 
 lemma Antitone.image_Ici_subset (h : Antitone f) : f '' Ici a ⊆ Iic (f a) :=
   (h.antitoneOn _).image_Ici_subset
@@ -155,6 +158,7 @@ lemma Antitone.image_Iic_subset (h : Antitone f) : f '' Iic b ⊆ Ici (f b) :=
 
 lemma Antitone.image_Icc_subset (h : Antitone f) : f '' Icc a b ⊆ Icc (f b) (f a) :=
   (h.antitoneOn _).image_Icc_subset
+#align antitone.image_Icc_subset Antitone.image_Icc_subset
 
 lemma StrictMono.image_Ioi_subset (h : StrictMono f) : f '' Ioi a ⊆ Ioi (f a) :=
   (h.strictMonoOn _).image_Ioi_subset

Mathlib/Order/Lattice.lean

@@ -9,7 +9,7 @@ import Mathlib.Order.Monotone.Basic
 import Mathlib.Order.ULift
 import Mathlib.Tactic.GCongr.Core
 
-#align_import order.lattice from "leanprover-community/mathlib"@"e4bc74cbaf429d706cb9140902f7ca6c431e75a4"
+#align_import order.lattice from "leanprover-community/mathlib"@"3ba15165bd6927679be7c22d6091a87337e3cd0c"
 
 /-!
 # (Semi-)lattices
@@ -1161,6 +1161,16 @@ protected theorem min [Preorder α] [LinearOrder β] {f g : α → β} {s : Set
   hf.inf hg
 #align monotone_on.min MonotoneOn.min
 
+theorem of_map_inf [SemilatticeInf α] [SemilatticeInf β]
+    (h : ∀ x ∈ s, ∀ y ∈ s, f (x ⊓ y) = f x ⊓ f y) : MonotoneOn f s := fun x hx y hy hxy =>
+  inf_eq_left.1 <| by rw [← h _ hx _ hy, inf_eq_left.2 hxy]
+#align monotone_on.of_map_inf MonotoneOn.of_map_inf
+
+theorem of_map_sup [SemilatticeSup α] [SemilatticeSup β]
+    (h : ∀ x ∈ s, ∀ y ∈ s, f (x ⊔ y) = f x ⊔ f y) : MonotoneOn f s :=
+  (@of_map_inf αᵒᵈ βᵒᵈ _ _ _ _ h).dual
+#align monotone_on.of_map_sup MonotoneOn.of_map_sup
+
 variable [LinearOrder α]
 
 theorem map_sup [SemilatticeSup β] (hf : MonotoneOn f s) (hx : x ∈ s) (hy : y ∈ s) :
@@ -1169,10 +1179,12 @@ theorem map_sup [SemilatticeSup β] (hf : MonotoneOn f s) (hx : x ∈ s) (hy : y
     first
     | assumption
     | simp only [*, sup_of_le_left, sup_of_le_right]
+#align monotone_on.map_sup MonotoneOn.map_sup
 
 theorem map_inf [SemilatticeInf β] (hf : MonotoneOn f s) (hx : x ∈ s) (hy : y ∈ s) :
     f (x ⊓ y) = f x ⊓ f y :=
   hf.dual.map_sup hx hy
+#align monotone_on.map_inf MonotoneOn.map_inf
 
 end MonotoneOn
 
@@ -1255,6 +1267,16 @@ protected theorem min [Preorder α] [LinearOrder β] {f g : α → β} {s : Set
   hf.inf hg
 #align antitone_on.min AntitoneOn.min
 
+theorem of_map_inf [SemilatticeInf α] [SemilatticeSup β]
+    (h : ∀ x ∈ s, ∀ y ∈ s, f (x ⊓ y) = f x ⊔ f y) : AntitoneOn f s := fun x hx y hy hxy =>
+  sup_eq_left.1 <| by rw [← h _ hx _ hy, inf_eq_left.2 hxy]
+#align antitone_on.of_map_inf AntitoneOn.of_map_inf
+
+theorem of_map_sup [SemilatticeSup α] [SemilatticeInf β]
+    (h : ∀ x ∈ s, ∀ y ∈ s, f (x ⊔ y) = f x ⊓ f y) : AntitoneOn f s :=
+  (@of_map_inf αᵒᵈ βᵒᵈ _ _ _ _ h).dual
+#align antitone_on.of_map_sup AntitoneOn.of_map_sup
+
 variable [LinearOrder α]
 
 theorem map_sup [SemilatticeInf β] (hf : AntitoneOn f s) (hx : x ∈ s) (hy : y ∈ s) :