feat(analysis/convex/proj_Icc): Extending convex functions (#18797)

Constantly extending monotone/antitone functions preserves their convexity.

src/algebra/order/module.lean

@@ -209,6 +209,18 @@ lemma bdd_above.smul_of_nonpos (hc : c ≤ 0) (hs : bdd_above s) : bdd_below (c
 
 end ordered_ring
 
+section linear_ordered_ring
+variables [linear_ordered_ring k] [linear_ordered_add_comm_group M] [module k M] [ordered_smul k M]
+  {a : k}
+
+lemma 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
+
+lemma 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
+
+end linear_ordered_ring
+
 section linear_ordered_field
 variables [linear_ordered_field k] [ordered_add_comm_group M] [module k M] [ordered_smul k M]
   {s : set M} {c : k}

src/algebra/order/monoid/lemmas.lean

@@ -244,6 +244,23 @@ variables [linear_order α] {a b c d : α} [covariant_class α α (*) (<)]
 @[to_additive] lemma min_le_max_of_mul_le_mul (h : a * b ≤ c * d) : min a b ≤ max c d :=
 by { simp_rw [min_le_iff, le_max_iff], contrapose! h, exact mul_lt_mul_of_lt_of_lt h.1.1 h.2.2 }
 
+end linear_order
+
+section linear_order
+variables [linear_order α] [covariant_class α α (*) (≤)] [covariant_class α α (swap (*)) (≤)]
+  {a b c d : α}
+
+@[to_additive max_add_add_le_max_add_max] lemma 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 _ _
+
+--TODO: Also missing `min_mul_min_le_min_mul_mul`
+@[to_additive min_add_min_le_min_add_add] lemma 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 _ _
+
 end linear_order
 end has_mul
 

src/algebra/order/smul.lean

@@ -170,12 +170,23 @@ ordered_smul.mk'' $ λ n hn, begin
   { cases (int.neg_succ_not_pos _).1 hn }
 end
 
+section linear_ordered_semiring
+variables [linear_ordered_semiring R] [linear_ordered_add_comm_monoid M] [smul_with_zero R M]
+  [ordered_smul R M] {a : R}
+
 -- TODO: `linear_ordered_field M → ordered_smul ℚ M`
 
-instance linear_ordered_semiring.to_ordered_smul {R : Type*} [linear_ordered_semiring R] :
-  ordered_smul R R :=
+instance linear_ordered_semiring.to_ordered_smul : ordered_smul R R :=
 ordered_smul.mk'' $ λ c, strict_mono_mul_left_of_pos
 
+lemma 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
+
+lemma 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
+
+end linear_ordered_semiring
+
 section linear_ordered_semifield
 variables [linear_ordered_semifield 𝕜] [ordered_add_comm_monoid M] [ordered_add_comm_monoid N]
   [mul_action_with_zero 𝕜 M] [mul_action_with_zero 𝕜 N]

src/analysis/convex/proj_Icc.lean

@@ -0,0 +1,91 @@
+/-
+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 analysis.convex.function
+import data.set.intervals.proj_Icc
+
+/-!
+# 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 `linear_ordered_field` if `𝕜` is.
+-/
+
+open set
+
+variables {𝕜 β : Type*} [linear_ordered_field 𝕜] [linear_ordered_add_comm_monoid β] [has_smul 𝕜 β]
+  {s : set 𝕜} {f : 𝕜 → β} {z : 𝕜}
+
+/-- A convex set extended towards minus infinity is convex. -/
+protected lemma convex.Ici_extend (hf : convex 𝕜 s) :
+  convex 𝕜 {x | Ici_extend (restrict (Ici z) (∈ s)) x} :=
+by { rw convex_iff_ord_connected at ⊢ hf, exact hf.restrict.Ici_extend }
+
+/-- A convex set extended towards infinity is convex. -/
+protected lemma convex.Iic_extend (hf : convex 𝕜 s) :
+  convex 𝕜 {x | Iic_extend (restrict (Iic z) (∈ s)) x} :=
+by { rw convex_iff_ord_connected at ⊢ hf, exact hf.restrict.Iic_extend }
+
+/-- A convex monotone function extended constantly towards minus infinity is convex. -/
+protected lemma convex_on.Ici_extend (hf : convex_on 𝕜 s f) (hf' : monotone_on f s) :
+  convex_on 𝕜 {x | Ici_extend (restrict (Ici z) (∈ s)) x} (Ici_extend $ restrict (Ici z) f) :=
+begin
+  refine ⟨hf.1.Ici_extend, λ x hx y hy a b ha hb hab, _⟩,
+  dsimp [Ici_extend_apply] at ⊢ hx hy,
+  refine (hf' (hf.1.ord_connected.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],
+end
+
+/-- A convex antitone function extended constantly towards infinity is convex. -/
+protected lemma convex_on.Iic_extend (hf : convex_on 𝕜 s f) (hf' : antitone_on f s) :
+  convex_on 𝕜 {x | Iic_extend (restrict (Iic z) (∈ s)) x} (Iic_extend $ restrict (Iic z) f) :=
+begin
+  refine ⟨hf.1.Iic_extend, λ x hx y hy a b ha hb hab, _⟩,
+  dsimp [Iic_extend_apply] at ⊢ hx hy,
+  refine (hf' (hf.1 hx hy ha hb hab) (hf.1.ord_connected.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],
+end
+
+/-- A concave antitone function extended constantly minus towards infinity is concave. -/
+protected lemma concave_on.Ici_extend (hf : concave_on 𝕜 s f) (hf' : antitone_on f s) :
+  concave_on 𝕜 {x | Ici_extend (restrict (Ici z) (∈ s)) x} (Ici_extend $ restrict (Ici z) f) :=
+hf.dual.Ici_extend hf'.dual_right
+
+/-- A concave monotone function extended constantly towards infinity is concave. -/
+protected lemma concave_on.Iic_extend (hf : concave_on 𝕜 s f) (hf' : monotone_on f s) :
+  concave_on 𝕜 {x | Iic_extend (restrict (Iic z) (∈ s)) x} (Iic_extend $ restrict (Iic z) f) :=
+hf.dual.Iic_extend hf'.dual_right
+
+/-- A convex monotone function extended constantly towards minus infinity is convex. -/
+protected lemma convex_on.Ici_extend_of_monotone (hf : convex_on 𝕜 univ f) (hf' : monotone f) :
+  convex_on 𝕜 univ (Ici_extend $ restrict (Ici z) f) :=
+hf.Ici_extend $ hf'.monotone_on _
+
+/-- A convex antitone function extended constantly towards infinity is convex. -/
+protected lemma convex_on.Iic_extend_of_antitone (hf : convex_on 𝕜 univ f) (hf' : antitone f) :
+  convex_on 𝕜 univ (Iic_extend $ restrict (Iic z) f) :=
+hf.Iic_extend $ hf'.antitone_on _
+
+/-- A concave antitone function extended constantly minus towards infinity is concave. -/
+protected lemma concave_on.Ici_extend_of_antitone (hf : concave_on 𝕜 univ f) (hf' : antitone f) :
+  concave_on 𝕜 univ (Ici_extend $ restrict (Ici z) f) :=
+hf.Ici_extend $ hf'.antitone_on _
+
+/-- A concave monotone function extended constantly towards infinity is concave. -/
+protected lemma concave_on.Iic_extend_of_monotone (hf : concave_on 𝕜 univ f) (hf' : monotone f) :
+  concave_on 𝕜 univ (Iic_extend $ restrict (Iic z) f) :=
+hf.Iic_extend $ hf'.monotone_on _

src/data/set/intervals/basic.lean

@@ -1164,6 +1164,26 @@ begin
       le_of_lt h₂, le_of_lt h₁] },
 end
 
+section lattice
+variables [lattice β] {f : α → β}
+
+lemma _root_.monotone_on.image_Icc_subset (hf : monotone_on f (Icc a b)) :
+  f '' Icc a b ⊆ Icc (f a) (f b) :=
+image_subset_iff.2 $ λ c hc,
+  ⟨hf (left_mem_Icc.2 $ hc.1.trans hc.2) hc hc.1, hf hc (right_mem_Icc.2 $ hc.1.trans hc.2) hc.2⟩
+
+lemma _root_.antitone_on.image_Icc_subset (hf : antitone_on f (Icc a b)) :
+  f '' Icc a b ⊆ Icc (f b) (f a) :=
+image_subset_iff.2 $ λ c hc,
+  ⟨hf hc (right_mem_Icc.2 $ hc.1.trans hc.2) hc.2, hf (left_mem_Icc.2 $ hc.1.trans hc.2) hc hc.1⟩
+
+lemma _root_.monotone.image_Icc_subset (hf : monotone f) : f '' Icc a b ⊆ Icc (f a) (f b) :=
+(hf.monotone_on _).image_Icc_subset
+
+lemma _root_.antitone.image_Icc_subset (hf : antitone f) : f '' Icc a b ⊆ Icc (f b) (f a) :=
+(hf.antitone_on _).image_Icc_subset
+
+end lattice
 end linear_order
 
 section lattice

src/data/set/intervals/unordered_interval.lean

@@ -129,7 +129,30 @@ by simpa only [uIcc_comm] using uIcc_injective_right a
 end distrib_lattice
 
 section linear_order
-variables [linear_order α] [linear_order β] {f : α → β} {s : set α} {a a₁ a₂ b b₁ b₂ c d x : α}
+variables [linear_order α]
+
+section lattice
+variables [lattice β] {f : α → β} {s : set α} {a b : α}
+
+lemma _root_.monotone_on.image_uIcc_subset (hf : monotone_on f (uIcc a b)) :
+  f '' uIcc a b ⊆ uIcc (f a) (f b) :=
+hf.image_Icc_subset.trans $
+  by rw [hf.map_sup left_mem_uIcc right_mem_uIcc, hf.map_inf left_mem_uIcc right_mem_uIcc, uIcc]
+
+lemma _root_.antitone_on.image_uIcc_subset (hf : antitone_on f (uIcc a b)) :
+  f '' uIcc a b ⊆ uIcc (f a) (f b) :=
+hf.image_Icc_subset.trans $
+  by rw [hf.map_sup left_mem_uIcc right_mem_uIcc, hf.map_inf left_mem_uIcc right_mem_uIcc, uIcc]
+
+lemma _root_.monotone.image_uIcc_subset (hf : monotone f) : f '' uIcc a b ⊆ uIcc (f a) (f b) :=
+(hf.monotone_on _).image_uIcc_subset
+
+lemma _root_.antitone.image_uIcc_subset (hf : antitone f) : f '' uIcc a b ⊆ uIcc (f a) (f b) :=
+(hf.antitone_on _).image_uIcc_subset
+
+end lattice
+
+variables [linear_order β] {f : α → β} {s : set α} {a a₁ a₂ b b₁ b₂ c d x : α}
 
 lemma Icc_min_max : Icc (min a b) (max a b) = [a, b] := rfl
 

src/order/lattice.lean

@@ -846,6 +846,7 @@ hf.dual.map_sup _ _
 end monotone
 
 namespace monotone_on
+variables {f : α → β} {s : set α} {x y : α}
 
 /-- Pointwise supremum of two monotone functions is a monotone function. -/
 protected lemma sup [preorder α] [semilattice_sup β] {f g : α → β} {s : set α}
@@ -867,6 +868,25 @@ protected lemma min [preorder α] [linear_order β] {f g : α → β} {s : set 
   (hf : monotone_on f s) (hg : monotone_on g s) : monotone_on (λ x, min (f x) (g x)) s :=
 hf.inf hg
 
+lemma of_map_inf [semilattice_inf α] [semilattice_inf β]
+  (h : ∀ (x ∈ s) (y ∈ s), f (x ⊓ y) = f x ⊓ f y) : monotone_on f s :=
+λ x hx y hy hxy, inf_eq_left.1 $ by rw [←h _ hx _ hy, inf_eq_left.2 hxy]
+
+lemma of_map_sup [semilattice_sup α] [semilattice_sup β]
+  (h : ∀ (x ∈ s) (y ∈ s), f (x ⊔ y) = f x ⊔ f y) : monotone_on f s :=
+(@of_map_inf αᵒᵈ βᵒᵈ _ _ _ _ h).dual
+
+variables [linear_order α]
+
+lemma map_sup [semilattice_sup β] (hf : monotone_on f s) (hx : x ∈ s) (hy : y ∈ s) :
+  f (x ⊔ y) = f x ⊔ f y :=
+by cases le_total x y; have := hf _ _ h;
+  assumption <|> simp only [h, this, sup_of_le_left, sup_of_le_right]
+
+lemma map_inf [semilattice_inf β] (hf : monotone_on f s) (hx : x ∈ s) (hy : y ∈ s) :
+  f (x ⊓ y) = f x ⊓ f y :=
+hf.dual.map_sup hx hy
+
 end monotone_on
 
 namespace antitone
@@ -912,6 +932,7 @@ hf.dual_right.map_inf x y
 end antitone
 
 namespace antitone_on
+variables {f : α → β} {s : set α} {x y : α}
 
 /-- Pointwise supremum of two antitone functions is a antitone function. -/
 protected lemma sup [preorder α] [semilattice_sup β] {f g : α → β} {s : set α}
@@ -933,6 +954,25 @@ protected lemma min [preorder α] [linear_order β] {f g : α → β} {s : set 
   (hf : antitone_on f s) (hg : antitone_on g s) : antitone_on (λ x, min (f x) (g x)) s :=
 hf.inf hg
 
+lemma of_map_inf [semilattice_inf α] [semilattice_sup β]
+  (h : ∀ (x ∈ s) (y ∈ s), f (x ⊓ y) = f x ⊔ f y) : antitone_on f s :=
+λ x hx y hy hxy, sup_eq_left.1 $ by rw [←h _ hx _ hy, inf_eq_left.2 hxy]
+
+lemma of_map_sup [semilattice_sup α] [semilattice_inf β]
+  (h : ∀ (x ∈ s) (y ∈ s), f (x ⊔ y) = f x ⊓ f y) : antitone_on f s :=
+(@of_map_inf αᵒᵈ βᵒᵈ _ _ _ _ h).dual
+
+variables [linear_order α]
+
+lemma map_sup [semilattice_inf β] (hf : antitone_on f s) (hx : x ∈ s) (hy : y ∈ s) :
+  f (x ⊔ y) = f x ⊓ f y :=
+by cases le_total x y; have := hf _ _ h; assumption <|>
+  simp only [h, this, sup_of_le_left, sup_of_le_right, inf_of_le_left, inf_of_le_right]
+
+lemma map_inf [semilattice_sup β] (hf : antitone_on f s) (hx : x ∈ s) (hy : y ∈ s) :
+  f (x ⊓ y) = f x ⊔ f y :=
+hf.dual.map_sup hx hy
+
 end antitone_on
 
 /-!