feat(analysis/convex/quasiconvex): A quasilinear function is either monotone or antitone (#17801)

Fulfill a todo I left a year ago. The proof is a big case bash on the relative positions of the four variables. I minimised it as much as I could.

The end result mentions convexity, but this is mostly order theory.

Author: YaelDillies

src/analysis/convex/quasiconvex.lean

@@ -21,11 +21,6 @@ quasiconcavity, and monotonicity implies quasilinearity.
 * `quasilinear_on 𝕜 s f`: Quasilinearity of the function `f` on the set `s` with scalars `𝕜`. This
   means that `f` is both quasiconvex and quasiconcave.
 
-## TODO
-
-Prove that a quasilinear function between two linear orders is either monotone or antitone. This is
-not hard but quite a pain to go about as there are many cases to consider.
-
 ## References
 
 * https://en.wikipedia.org/wiki/Quasiconvex_function
@@ -196,3 +191,21 @@ lemma antitone.quasilinear_on (hf : antitone f) : quasilinear_on 𝕜 univ f :=
 
 end linear_ordered_add_comm_monoid
 end ordered_semiring
+
+section linear_ordered_field
+variables [linear_ordered_field 𝕜] [linear_ordered_add_comm_monoid β] {s : set 𝕜} {f : 𝕜 → β}
+
+lemma quasilinear_on.monotone_on_or_antitone_on (hf : quasilinear_on 𝕜 s f) :
+  monotone_on f s ∨ antitone_on f s :=
+begin
+  simp_rw [monotone_on_or_antitone_on_iff_interval, ←segment_eq_interval],
+  rintro a ha b hb c hc h,
+  refine ⟨((hf.2 _).segment_subset _ _ h).2, ((hf.1 _).segment_subset _ _ h).2⟩; simp [*],
+end
+
+lemma quasilinear_on_iff_monotone_on_or_antitone_on (hs : convex 𝕜 s) :
+  quasilinear_on 𝕜 s f ↔ monotone_on f s ∨ antitone_on f s :=
+⟨λ h, h.monotone_on_or_antitone_on,
+  λ h, h.elim (λ h, h.quasilinear_on hs) (λ h, h.quasilinear_on hs)⟩
+
+end linear_ordered_field

src/data/set/basic.lean

@@ -2033,8 +2033,21 @@ theorem univ_eq_true_false : univ = ({true, false} : set Prop) :=
 eq.symm $ eq_univ_of_forall $ classical.cases (by simp) (by simp)
 
 section preorder
+variables [preorder α] [preorder β] {f : α → β}
 
-variables [preorder α] [preorder β] (f : α → β)
+lemma monotone_on_iff_monotone : monotone_on f s ↔ monotone (λ a : s, f a) :=
+by simp [monotone, monotone_on]
+
+lemma antitone_on_iff_antitone : antitone_on f s ↔ antitone (λ a : s, f a) :=
+by simp [antitone, antitone_on]
+
+lemma strict_mono_on_iff_strict_mono : strict_mono_on f s ↔ strict_mono (λ a : s, f a) :=
+by simp [strict_mono, strict_mono_on]
+
+lemma strict_anti_on_iff_strict_anti : strict_anti_on f s ↔ strict_anti (λ a : s, f a) :=
+by simp [strict_anti, strict_anti_on]
+
+variables (f)
 
 /-! ### Monotonicity on singletons -/
 
@@ -2068,6 +2081,27 @@ subsingleton_singleton.strict_anti_on f
 
 end preorder
 
+section linear_order
+variables [linear_order α] [linear_order β] {f : α → β}
+
+/-- A function between linear orders which is neither monotone nor antitone makes a dent upright or
+downright. -/
+lemma not_monotone_on_not_antitone_on_iff_exists_le_le :
+  ¬ monotone_on f s ∧ ¬ antitone_on f s ↔ ∃ a b c ∈ s, a ≤ b ∧ b ≤ c ∧
+    (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c) :=
+by simp [monotone_on_iff_monotone, antitone_on_iff_antitone, and_assoc, exists_and_distrib_left,
+  not_monotone_not_antitone_iff_exists_le_le, @and.left_comm (_ ∈ s)]
+
+/-- A function between linear orders which is neither monotone nor antitone makes a dent upright or
+downright. -/
+lemma not_monotone_on_not_antitone_on_iff_exists_lt_lt :
+  ¬ monotone_on f s ∧ ¬ antitone_on f s ↔ ∃ a b c ∈ s, a < b ∧ b < c ∧
+    (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c) :=
+by simp [monotone_on_iff_monotone, antitone_on_iff_antitone, and_assoc, exists_and_distrib_left,
+  not_monotone_not_antitone_iff_exists_lt_lt, @and.left_comm (_ ∈ s)]
+
+end linear_order
+
 /-! ### Lemmas about range of a function. -/
 section range
 variables {f : ι → α}

src/data/set/intervals/basic.lean

@@ -1219,7 +1219,7 @@ end both
 end lattice
 
 section linear_order
-variables [linear_order α] {a a₁ a₂ b b₁ b₂ c d : α}
+variables [linear_order α] [linear_order β] {f : α → β} {a a₁ a₂ b b₁ b₂ c d : α}
 
 @[simp] lemma Ioi_inter_Ioi : Ioi a ∩ Ioi b = Ioi (a ⊔ b) := ext $ λ _, sup_lt_iff.symm
 @[simp] lemma Iio_inter_Iio : Iio a ∩ Iio b = Iio (a ⊓ b) := ext $ λ _, lt_inf_iff.symm

src/data/set/intervals/unordered_interval.lean

@@ -25,15 +25,13 @@ make the notation available.
 
 -/
 
-universe u
-
 open function order_dual (to_dual of_dual)
 
 namespace set
 
 section linear_order
-
-variables {α : Type u} [linear_order α] {a a₁ a₂ b b₁ b₂ c x : α}
+variables {α β : Type*} [linear_order α] [linear_order β] {f : α → β} {s : set α}
+  {a a₁ a₂ b b₁ b₂ c x : α}
 
 /-- `interval a b` is the set of elements lying between `a` and `b`, with `a` and `b` included. -/
 def interval (a b : α) := Icc (min a b) (max a b)
@@ -140,6 +138,24 @@ begin
   { rintro ⟨a, b, h⟩, exact ⟨min a b, max a b, h⟩ }
 end
 
+lemma monotone_or_antitone_iff_interval :
+  monotone f ∨ antitone f ↔ ∀ a b c, c ∈ [a, b] → f c ∈ [f a, f b] :=
+begin
+  split,
+  { rintro (hf | hf) a b c; simp_rw [interval, ←hf.map_min, ←hf.map_max],
+    exacts [λ hc, ⟨hf hc.1, hf hc.2⟩, λ hc, ⟨hf hc.2, hf hc.1⟩] },
+  contrapose!,
+  rw not_monotone_not_antitone_iff_exists_le_le,
+  rintro ⟨a, b, c, hab, hbc, ⟨hfab, hfcb⟩ | ⟨hfba, hfbc⟩⟩,
+  { exact ⟨a, c, b, Icc_subset_interval ⟨hab, hbc⟩, λ h, h.2.not_lt $ max_lt hfab hfcb⟩ },
+  { exact ⟨a, c, b, Icc_subset_interval ⟨hab, hbc⟩, λ h, h.1.not_lt $ lt_min hfba hfbc⟩ }
+end
+
+lemma monotone_on_or_antitone_on_iff_interval :
+  monotone_on f s ∨ antitone_on f s ↔ ∀ a b c ∈ s, c ∈ [a, b] → f c ∈ [f a, f b] :=
+by simp [monotone_on_iff_monotone, antitone_on_iff_antitone, monotone_or_antitone_iff_interval,
+  mem_interval]
+
 /-- The open-closed interval with unordered bounds. -/
 def interval_oc : α → α → set α := λ a b, Ioc (min a b) (max a b)
 

src/order/monotone.lean

@@ -216,7 +216,7 @@ section preorder
 variables [preorder α]
 
 section preorder
-variables [preorder β] {f : α → β} {a b : α}
+variables [preorder β] {f : α → β} {s : set α} {a b : α}
 
 /-!
 These four lemmas are there to strip off the semi-implicit arguments `⦃a b : α⦄`. This is useful
@@ -235,10 +235,10 @@ protected lemma monotone.monotone_on (hf : monotone f) (s : set α) : monotone_o
 protected lemma antitone.antitone_on (hf : antitone f) (s : set α) : antitone_on f s :=
 λ a _ b _, hf.imp
 
-lemma monotone_on_univ : monotone_on f set.univ ↔ monotone f :=
+@[simp] lemma monotone_on_univ : monotone_on f set.univ ↔ monotone f :=
 ⟨λ h a b, h trivial trivial, λ h, h.monotone_on _⟩
 
-lemma antitone_on_univ : antitone_on f set.univ ↔ antitone f :=
+@[simp] lemma antitone_on_univ : antitone_on f set.univ ↔ antitone f :=
 ⟨λ h a b, h trivial trivial, λ h, h.antitone_on _⟩
 
 protected lemma strict_mono.strict_mono_on (hf : strict_mono f) (s : set α) : strict_mono_on f s :=
@@ -247,10 +247,10 @@ protected lemma strict_mono.strict_mono_on (hf : strict_mono f) (s : set α) : s
 protected lemma strict_anti.strict_anti_on (hf : strict_anti f) (s : set α) : strict_anti_on f s :=
 λ a _ b _, hf.imp
 
-lemma strict_mono_on_univ : strict_mono_on f set.univ ↔ strict_mono f :=
+@[simp] lemma strict_mono_on_univ : strict_mono_on f set.univ ↔ strict_mono f :=
 ⟨λ h a b, h trivial trivial, λ h, h.strict_mono_on _⟩
 
-lemma strict_anti_on_univ : strict_anti_on f set.univ ↔ strict_anti f :=
+@[simp] lemma strict_anti_on_univ : strict_anti_on f set.univ ↔ strict_anti f :=
 ⟨λ h a b, h trivial trivial, λ h, h.strict_anti_on _⟩
 
 end preorder
@@ -644,12 +644,55 @@ lemma antitone.strict_anti_iff_injective (hf : antitone f) :
 
 end partial_order
 
+variables [linear_order β] {f : α → β} {s : set α} {x y : α}
+
+/-- A function between linear orders which is neither monotone nor antitone makes a dent upright or
+downright. -/
+lemma not_monotone_not_antitone_iff_exists_le_le :
+  ¬ monotone f ∧ ¬ antitone f ↔ ∃ a b c, a ≤ b ∧ b ≤ c ∧
+    (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c) :=
+begin
+  simp_rw [monotone, antitone, not_forall, not_le],
+  refine iff.symm ⟨_, _⟩,
+  { rintro ⟨a, b, c, hab, hbc, ⟨hfab, hfcb⟩ | ⟨hfba, hfbc⟩⟩,
+    exacts [⟨⟨_, _, hbc, hfcb⟩, _, _, hab, hfab⟩, ⟨⟨_, _, hab, hfba⟩, _, _, hbc, hfbc⟩] },
+  rintro ⟨⟨a, b, hab, hfba⟩, c, d, hcd, hfcd⟩,
+  obtain hda | had := le_total d a,
+  { obtain hfad | hfda := le_total (f a) (f d),
+    { exact ⟨c, d, b, hcd, hda.trans hab, or.inl ⟨hfcd, hfba.trans_le hfad⟩⟩ },
+    { exact ⟨c, a, b, hcd.trans hda, hab, or.inl ⟨hfcd.trans_le hfda, hfba⟩⟩ } },
+  obtain hac | hca := le_total a c,
+  { obtain hfdb | hfbd := le_or_lt (f d) (f b),
+    { exact ⟨a, c, d, hac, hcd, or.inr ⟨hfcd.trans $ hfdb.trans_lt hfba, hfcd⟩⟩ },
+    obtain hfca | hfac := lt_or_le (f c) (f a),
+    { exact ⟨a, c, d, hac, hcd, or.inr ⟨hfca, hfcd⟩⟩ },
+    obtain hbd | hdb := le_total b d,
+    { exact ⟨a, b, d, hab, hbd, or.inr ⟨hfba, hfbd⟩⟩ },
+    { exact ⟨a, d, b, had, hdb, or.inl ⟨hfac.trans_lt hfcd, hfbd⟩⟩ } },
+  { obtain hfdb | hfbd := le_or_lt (f d) (f b),
+    { exact ⟨c, a, b, hca, hab, or.inl ⟨hfcd.trans $ hfdb.trans_lt hfba, hfba⟩⟩ },
+    obtain hfca | hfac := lt_or_le (f c) (f a),
+    { exact ⟨c, a, b, hca, hab, or.inl ⟨hfca, hfba⟩⟩ },
+    obtain hbd | hdb := le_total b d,
+    { exact ⟨a, b, d, hab, hbd, or.inr ⟨hfba, hfbd⟩⟩ },
+    { exact ⟨a, d, b, had, hdb, or.inl ⟨hfac.trans_lt hfcd, hfbd⟩⟩ } }
+end
+
+/-- A function between linear orders which is neither monotone nor antitone makes a dent upright or
+downright. -/
+lemma not_monotone_not_antitone_iff_exists_lt_lt :
+  ¬ monotone f ∧ ¬ antitone f ↔ ∃ a b c, a < b ∧ b < c ∧
+    (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c) :=
+begin
+  simp_rw [not_monotone_not_antitone_iff_exists_le_le, ←and_assoc],
+  refine exists₃_congr (λ a b c, and_congr_left $ λ h, (ne.le_iff_lt _).and $ ne.le_iff_lt _);
+    rintro rfl; simpa using h,
+end
+
 /-!
 ### Strictly monotone functions and `cmp`
 -/
 
-variables [linear_order β] {f : α → β} {s : set α} {x y : α}
-
 lemma strict_mono_on.cmp_map_eq (hf : strict_mono_on f s) (hx : x ∈ s) (hy : y ∈ s) :
   cmp (f x) (f y) = cmp x y :=
 ((hf.compares hx hy).2 (cmp_compares x y)).cmp_eq