[Merged by Bors] - feat: Extending convex functions

Mathlib.lean

@@ -641,6 +641,7 @@ import Mathlib.Analysis.Convex.KreinMilman
 import Mathlib.Analysis.Convex.Measure
 import Mathlib.Analysis.Convex.Normed
 import Mathlib.Analysis.Convex.PartitionOfUnity
+import Mathlib.Analysis.Convex.ProjIcc
 import Mathlib.Analysis.Convex.Quasiconvex
 import Mathlib.Analysis.Convex.Segment
 import Mathlib.Analysis.Convex.Side

Mathlib/Algebra/Order/Module.lean

@@ -5,7 +5,7 @@
 -/
 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 @@
 
 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

@@ -8,7 +8,7 @@
 import Mathlib.Init.Data.Ordering.Basic
 import Mathlib.Order.MinMax
 
-#align_import algebra.order.monoid.lemmas from "leanprover-community/mathlib"@"2ed7e4aec72395b6a7c3ac4ac7873a7a43ead17c"
+#align_import algebra.order.monoid.lemmas from "leanprover-community/mathlib"@"3ba15165bd6927679be7c22d6091a87337e3cd0c"
 
 /-!
 # Ordered monoids
@@ -314,6 +314,27 @@
 #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.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,26 @@
     · 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/Analysis/Convex/ProjIcc.lean

@@ -0,0 +1,99 @@
+/-
+Copyright (c) 2023 Yaël Dillies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies
+-/
+import Mathlib.Analysis.Convex.Function
+import Mathlib.Data.Set.Intervals.ProjIcc
+
+#align_import analysis.convex.proj_Icc from "leanprover-community/mathlib"@"3ba15165bd6927679be7c22d6091a87337e3cd0c"
+
+/-!
+# Convexity of extension from intervals
+
+This file proves that constantly extending monotone/antitone functions preserves their convexity.
+
+## TODO
+
+We could deduplicate the proofs if we had a typeclass stating that `segment 𝕜 x y = [x -[𝕜] y]` as
+`𝕜ᵒᵈ` respects it if `𝕜` does, while `𝕜ᵒᵈ` isn't a `LinearOrderedField` if `𝕜` is.
+-/
+
+open Set
+
+variable {𝕜 β : Type _} [LinearOrderedField 𝕜] [LinearOrderedAddCommMonoid β] [SMul 𝕜 β] {s : Set 𝕜}
+  {f : 𝕜 → β} {z : 𝕜}
+
+/-- A convex set extended towards minus infinity is convex. -/
+protected theorem Convex.IciExtend (hf : Convex 𝕜 s) :
+    Convex 𝕜 {x | IciExtend (restrict (Ici z) (· ∈ s)) x} := by
+  rw [convex_iff_ordConnected] at hf ⊢; exact hf.restrict.IciExtend
+#align convex.Ici_extend Convex.IciExtend
+
+/-- A convex set extended towards infinity is convex. -/
+protected theorem Convex.IicExtend (hf : Convex 𝕜 s) :
+    Convex 𝕜 {x | IicExtend (restrict (Iic z) (· ∈ s)) x} := by
+  rw [convex_iff_ordConnected] at hf ⊢; exact hf.restrict.IicExtend
+#align convex.Iic_extend Convex.IicExtend
+
+/-- A convex monotone function extended constantly towards minus infinity is convex. -/
+protected theorem ConvexOn.IciExtend (hf : ConvexOn 𝕜 s f) (hf' : MonotoneOn f s) :
+    ConvexOn 𝕜 {x | IciExtend (restrict (Ici z) (· ∈ s)) x} (IciExtend $ restrict (Ici z) f) := by
+  refine' ⟨hf.1.IciExtend, λ x hx y hy a b ha hb hab ↦ _⟩
+  dsimp [IciExtend_apply] at hx hy ⊢
+  refine' (hf' (hf.1.ordConnected.uIcc_subset hx hy $ (Monotone.image_uIcc_subset λ _ _ ↦
+    max_le_max le_rfl) $ mem_image_of_mem _ $ convex_uIcc _ _
+    left_mem_uIcc right_mem_uIcc ha hb hab) (hf.1 hx hy ha hb hab) _).trans (hf.2 hx hy ha hb hab)
+  rw [smul_max ha z, smul_max hb z]
+  refine' le_trans _ max_add_add_le_max_add_max
+  rw [Convex.combo_self hab, smul_eq_mul, smul_eq_mul]
+#align convex_on.Ici_extend ConvexOn.IciExtend
+
+/-- A convex antitone function extended constantly towards infinity is convex. -/
+protected theorem ConvexOn.IicExtend (hf : ConvexOn 𝕜 s f) (hf' : AntitoneOn f s) :
+    ConvexOn 𝕜 {x | IicExtend (restrict (Iic z) (· ∈ s)) x} (IicExtend $ restrict (Iic z) f) := by
+  refine' ⟨hf.1.IicExtend, λ x hx y hy a b ha hb hab ↦ _⟩
+  dsimp [IicExtend_apply] at hx hy ⊢
+  refine' (hf' (hf.1 hx hy ha hb hab) (hf.1.ordConnected.uIcc_subset hx hy $
+    (Monotone.image_uIcc_subset λ _ _ ↦ min_le_min le_rfl) $ mem_image_of_mem _ $ convex_uIcc _ _
+    left_mem_uIcc right_mem_uIcc ha hb hab) _).trans (hf.2 hx hy ha hb hab)
+  rw [smul_min ha z, smul_min hb z]
+  refine' min_add_min_le_min_add_add.trans _
+  rw [Convex.combo_self hab, smul_eq_mul, smul_eq_mul]
+#align convex_on.Iic_extend ConvexOn.IicExtend
+
+/-- A concave antitone function extended constantly minus towards infinity is concave. -/
+protected theorem ConcaveOn.IciExtend (hf : ConcaveOn 𝕜 s f) (hf' : AntitoneOn f s) :
+    ConcaveOn 𝕜 {x | IciExtend (restrict (Ici z) (· ∈ s)) x} (IciExtend $ restrict (Ici z) f) :=
+  hf.dual.IciExtend hf'.dual_right
+#align concave_on.Ici_extend ConcaveOn.IciExtend
+
+/-- A concave monotone function extended constantly towards infinity is concave. -/
+protected theorem ConcaveOn.IicExtend (hf : ConcaveOn 𝕜 s f) (hf' : MonotoneOn f s) :
+    ConcaveOn 𝕜 {x | IicExtend (restrict (Iic z) (· ∈ s)) x} (IicExtend $ restrict (Iic z) f) :=
+  hf.dual.IicExtend hf'.dual_right
+#align concave_on.Iic_extend ConcaveOn.IicExtend
+
+/-- A convex monotone function extended constantly towards minus infinity is convex. -/
+protected theorem ConvexOn.IciExtend_of_monotone (hf : ConvexOn 𝕜 univ f) (hf' : Monotone f) :
+    ConvexOn 𝕜 univ (IciExtend $ restrict (Ici z) f) :=
+  hf.IciExtend $ hf'.monotoneOn _
+#align convex_on.Ici_extend_of_monotone ConvexOn.IciExtend_of_monotone
+
+/-- A convex antitone function extended constantly towards infinity is convex. -/
+protected theorem ConvexOn.IicExtend_of_antitone (hf : ConvexOn 𝕜 univ f) (hf' : Antitone f) :
+    ConvexOn 𝕜 univ (IicExtend $ restrict (Iic z) f) :=
+  hf.IicExtend $ hf'.antitoneOn _
+#align convex_on.Iic_extend_of_antitone ConvexOn.IicExtend_of_antitone
+
+/-- A concave antitone function extended constantly minus towards infinity is concave. -/
+protected theorem ConcaveOn.IciExtend_of_antitone (hf : ConcaveOn 𝕜 univ f) (hf' : Antitone f) :
+    ConcaveOn 𝕜 univ (IciExtend $ restrict (Ici z) f) :=
+  hf.IciExtend $ hf'.antitoneOn _
+#align concave_on.Ici_extend_of_antitone ConcaveOn.IciExtend_of_antitone
+
+/-- A concave monotone function extended constantly towards infinity is concave. -/
+protected theorem ConcaveOn.IicExtend_of_monotone (hf : ConcaveOn 𝕜 univ f) (hf' : Monotone f) :
+    ConcaveOn 𝕜 univ (IicExtend $ restrict (Iic z) f) :=
+  hf.IicExtend $ hf'.monotoneOn _
+#align concave_on.Iic_extend_of_monotone ConcaveOn.IicExtend_of_monotone

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
@@ -38,7 +38,7 @@ namespace Set
 
 section Preorder
 
-variable [Preorder α] {a a₁ a₂ b b₁ b₂ c x : α}
+variable [Preorder α] [Preorder β] {f : α → β} {a a₁ a₂ b b₁ b₂ c x : α}
 
 /-- Left-open right-open interval -/
 def Ioo (a b : α) :=