From caeb3feabcf753bf36c06877c4988c6edda4bdf3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Fri, 6 Oct 2023 14:17:21 +0000 Subject: [PATCH] feat: Extending convex functions (#6339) Forward-ports https://github.com/leanprover-community/mathlib/pull/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 --- Mathlib/Algebra/Order/Module.lean | 15 ++++++++++++++- Mathlib/Algebra/Order/Monoid/Lemmas.lean | 23 ++++++++++++++++++++++- Mathlib/Algebra/Order/SMul.lean | 19 ++++++++++++++++--- Mathlib/Data/Set/Intervals/Basic.lean | 2 +- Mathlib/Data/Set/Intervals/Image.lean | 4 ++++ Mathlib/Order/Lattice.lean | 24 +++++++++++++++++++++++- 6 files changed, 80 insertions(+), 7 deletions(-) diff --git a/Mathlib/Algebra/Order/Module.lean b/Mathlib/Algebra/Order/Module.lean index 977d3036aa9a0..38413e037c287 100644 --- a/Mathlib/Algebra/Order/Module.lean +++ b/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} diff --git a/Mathlib/Algebra/Order/Monoid/Lemmas.lean b/Mathlib/Algebra/Order/Monoid/Lemmas.lean index 4908a3f927e69..7b1fa597fdda3 100644 --- a/Mathlib/Algebra/Order/Monoid/Lemmas.lean +++ b/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 diff --git a/Mathlib/Algebra/Order/SMul.lean b/Mathlib/Algebra/Order/SMul.lean index ef24103de5645..933dfff133ca6 100644 --- a/Mathlib/Algebra/Order/SMul.lean +++ b/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] diff --git a/Mathlib/Data/Set/Intervals/Basic.lean b/Mathlib/Data/Set/Intervals/Basic.lean index e93a47639df3e..d4af3dcc13876 100644 --- a/Mathlib/Data/Set/Intervals/Basic.lean +++ b/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 diff --git a/Mathlib/Data/Set/Intervals/Image.lean b/Mathlib/Data/Set/Intervals/Image.lean index 54820fd0fb753..1e1ca90b1cb4c 100644 --- a/Mathlib/Data/Set/Intervals/Image.lean +++ b/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 diff --git a/Mathlib/Order/Lattice.lean b/Mathlib/Order/Lattice.lean index 8f6c975f31fa1..4ff7c915a913e 100644 --- a/Mathlib/Order/Lattice.lean +++ b/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) :