refactor(data/set/intervals/monotone): split (#17893)

Also generalize&golf `monotone_on.exists_monotone_extension` and rename `order.monotone` to `order.monotone.basic`.

Lean 4 version is leanprover-community/mathlib4#947

scripts/modules_used.lean

@@ -14,7 +14,7 @@ returns
 ```
 order.synonym
 order.rel_classes
-order.monotone
+order.monotone.basic
 order.lattice
 order.heyting.basic
 order.bounded_order

src/algebra/covariant_and_contravariant.lean

@@ -6,7 +6,7 @@ Authors: Damiano Testa
 
 import algebra.group.defs
 import order.basic
-import order.monotone
+import order.monotone.basic
 
 /-!
 

src/analysis/calculus/monotone.lean

@@ -6,6 +6,7 @@ Authors: Sébastien Gouëzel
 import measure_theory.measure.lebesgue
 import analysis.calculus.deriv
 import measure_theory.covering.one_dim
+import order.monotone.extension
 
 /-!
 # Differentiability of monotone functions
@@ -232,8 +233,9 @@ begin
   apply ae_of_mem_of_ae_of_mem_inter_Ioo,
   assume a b as bs hab,
   obtain ⟨g, hg, gf⟩ : ∃ (g : ℝ → ℝ), monotone g ∧ eq_on f g (s ∩ Icc a b) :=
-    monotone_on.exists_monotone_extension (hf.mono (inter_subset_left s (Icc a b)))
-      ⟨⟨as, ⟨le_rfl, hab.le⟩⟩, λ x hx, hx.2.1⟩ ⟨⟨bs, ⟨hab.le, le_rfl⟩⟩, λ x hx, hx.2.2⟩,
+    (hf.mono (inter_subset_left s (Icc a b))).exists_monotone_extension
+      (hf.map_bdd_below (inter_subset_left _ _) ⟨a, λ x hx, hx.2.1, as⟩)
+      (hf.map_bdd_above (inter_subset_left _ _) ⟨b, λ x hx, hx.2.2, bs⟩),
   filter_upwards [hg.ae_differentiable_at] with x hx,
   assume h'x,
   apply hx.differentiable_within_at.congr_of_eventually_eq _ (gf ⟨h'x.1, h'x.2.1.le, h'x.2.2.le⟩),

src/analysis/special_functions/trigonometric/deriv.lean

@@ -3,6 +3,7 @@ Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Abhimanyu Pallavi Sudhir, Jean Lo, Calle Sönne, Benjamin Davidson
 -/
+import order.monotone.odd
 import analysis.special_functions.exp_deriv
 import analysis.special_functions.trigonometric.basic
 import data.set.intervals.monotone

src/data/int/basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad
 -/
 import data.nat.basic
-import order.monotone
+import order.monotone.basic
 
 /-!
 # Basic instances on the integers

src/data/set/intervals/iso_Ioo.lean

@@ -0,0 +1,37 @@
+/-
+Copyright (c) 2022 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
+import order.monotone.odd
+import tactic.field_simp
+
+/-!
+# Order isomorphism between a linear ordered field and `(-1, 1)`
+
+In this file we provide an order isomorphism `order_iso_Ioo_neg_one_one` between the open interval
+`(-1, 1)` in a linear ordered field and the whole field.
+-/
+
+open set
+
+/-- In a linear ordered field, the whole field is order isomorphic to the open interval `(-1, 1)`.
+We consider the actual implementation to be a "black box", so it is irreducible.
+-/
+@[irreducible] def order_iso_Ioo_neg_one_one (k : Type*) [linear_ordered_field k] :
+  k ≃o Ioo (-1 : k) 1 :=
+begin
+  refine strict_mono.order_iso_of_right_inverse _ _ (λ x, x / (1 - |x|)) _,
+  { refine cod_restrict (λ x, x / (1 + |x|)) _ (λ x, abs_lt.1 _),
+    have H : 0 < 1 + |x|, from (abs_nonneg x).trans_lt (lt_one_add _),
+    calc |x / (1 + |x|)| = |x| / (1 + |x|) : by rw [abs_div, abs_of_pos H]
+                     ... < 1               : (div_lt_one H).2 (lt_one_add _) },
+  { refine (strict_mono_of_odd_strict_mono_on_nonneg _ _).cod_restrict _,
+    { intro x, simp only [abs_neg, neg_div] },
+    { rintros x (hx : 0 ≤ x) y (hy : 0 ≤ y) hxy,
+      simp [abs_of_nonneg, mul_add, mul_comm x y, div_lt_div_iff,
+        hx.trans_lt (lt_one_add _), hy.trans_lt (lt_one_add _), *] } },
+  { refine λ x, subtype.ext _,
+    have : 0 < 1 - |(x : k)|, from sub_pos.2 (abs_lt.2 x.2),
+    field_simp [abs_div, this.ne', abs_of_pos this] }
+end

src/data/set/intervals/monotone.lean

@@ -4,235 +4,17 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
 import data.set.intervals.disjoint
-import order.conditionally_complete_lattice.basic
 import order.succ_pred.basic
-import algebra.order.field.basic
-import tactic.field_simp
 
 /-!
 # Monotonicity on intervals
 
-In this file we prove that a function is (strictly) monotone (or antitone) on a linear order `α`
-provided that it is (strictly) monotone on `(-∞, a]` and on `[a, +∞)`. This is a special case
-of a more general statement where one deduces monotonicity on a union from monotonicity on each
-set.
-
-We deduce in `monotone_on.exists_monotone_extension` that a function which is monotone on a set
-with a smallest and a largest element admits a monotone extension to the whole space.
-
-We also provide an order isomorphism `order_iso_Ioo_neg_one_one` between the open
-interval `(-1, 1)` in a linear ordered field and the whole field.
+In this file we prove that `set.Ici` etc are monotone/antitone functions. We also prove some lemmas
+about functions monotone on intervals in `succ_order`s.
 -/
 
 open set
 
-section
-
-variables {α β : Type*} [linear_order α] [preorder β] {a : α} {f : α → β}
-
-/-- If `f` is strictly monotone both on `s` and `t`, with `s` to the left of `t` and the center
-point belonging to both `s` and `t`, then `f` is strictly monotone on `s ∪ t` -/
-protected lemma strict_mono_on.union {s t : set α} {c : α} (h₁ : strict_mono_on f s)
-  (h₂ : strict_mono_on f t) (hs : is_greatest s c) (ht : is_least t c) :
-  strict_mono_on f (s ∪ t) :=
-begin
-  have A : ∀ x, x ∈ s ∪ t → x ≤ c → x ∈ s,
-  { assume x hx hxc,
-    cases hx, { exact hx },
-    rcases eq_or_lt_of_le hxc with rfl|h'x, { exact hs.1 },
-    exact (lt_irrefl _ (h'x.trans_le (ht.2 hx))).elim },
-  have B : ∀ x, x ∈ s ∪ t → c ≤ x → x ∈ t,
-  { assume x hx hxc,
-    cases hx, swap, { exact hx },
-    rcases eq_or_lt_of_le hxc with rfl|h'x, { exact ht.1 },
-    exact (lt_irrefl _ (h'x.trans_le (hs.2 hx))).elim },
-  assume x hx y hy hxy,
-  rcases lt_or_le x c with hxc|hcx,
-  { have xs : x ∈ s, from A _ hx hxc.le,
-    rcases lt_or_le y c with hyc|hcy,
-    { exact h₁ xs (A _ hy hyc.le) hxy },
-    { exact (h₁ xs hs.1 hxc).trans_le (h₂.monotone_on ht.1 (B _ hy hcy) hcy) } },
-  { have xt : x ∈ t, from B _ hx hcx,
-    have yt : y ∈ t, from B _ hy (hcx.trans hxy.le),
-    exact h₂ xt yt hxy }
-end
-
-/-- If `f` is strictly monotone both on `(-∞, a]` and `[a, ∞)`, then it is strictly monotone on the
-whole line. -/
-protected lemma strict_mono_on.Iic_union_Ici (h₁ : strict_mono_on f (Iic a))
-  (h₂ : strict_mono_on f (Ici a)) : strict_mono f :=
-begin
-  rw [← strict_mono_on_univ, ← @Iic_union_Ici _ _ a],
-  exact strict_mono_on.union h₁ h₂ is_greatest_Iic is_least_Ici,
-end
-
-/-- If `f` is strictly antitone both on `s` and `t`, with `s` to the left of `t` and the center
-point belonging to both `s` and `t`, then `f` is strictly antitone on `s ∪ t` -/
-protected lemma strict_anti_on.union {s t : set α} {c : α} (h₁ : strict_anti_on f s)
-  (h₂ : strict_anti_on f t) (hs : is_greatest s c) (ht : is_least t c) :
-  strict_anti_on f (s ∪ t) :=
-(h₁.dual_right.union h₂.dual_right hs ht).dual_right
-
-/-- If `f` is strictly antitone both on `(-∞, a]` and `[a, ∞)`, then it is strictly antitone on the
-whole line. -/
-protected lemma strict_anti_on.Iic_union_Ici (h₁ : strict_anti_on f (Iic a))
-  (h₂ : strict_anti_on f (Ici a)) : strict_anti f :=
-(h₁.dual_right.Iic_union_Ici h₂.dual_right).dual_right
-
-/-- If `f` is monotone both on `s` and `t`, with `s` to the left of `t` and the center
-point belonging to both `s` and `t`, then `f` is monotone on `s ∪ t` -/
-protected lemma monotone_on.union_right {s t : set α} {c : α} (h₁ : monotone_on f s)
-  (h₂ : monotone_on f t) (hs : is_greatest s c) (ht : is_least t c) :
-  monotone_on f (s ∪ t) :=
-begin
-  have A : ∀ x, x ∈ s ∪ t → x ≤ c → x ∈ s,
-  { assume x hx hxc,
-    cases hx, { exact hx },
-    rcases eq_or_lt_of_le hxc with rfl|h'x, { exact hs.1 },
-    exact (lt_irrefl _ (h'x.trans_le (ht.2 hx))).elim },
-  have B : ∀ x, x ∈ s ∪ t → c ≤ x → x ∈ t,
-  { assume x hx hxc,
-    cases hx, swap, { exact hx },
-    rcases eq_or_lt_of_le hxc with rfl|h'x, { exact ht.1 },
-    exact (lt_irrefl _ (h'x.trans_le (hs.2 hx))).elim },
-  assume x hx y hy hxy,
-  rcases lt_or_le x c with hxc|hcx,
-  { have xs : x ∈ s, from A _ hx hxc.le,
-    rcases lt_or_le y c with hyc|hcy,
-    { exact h₁ xs (A _ hy hyc.le) hxy },
-    { exact (h₁ xs hs.1 hxc.le).trans (h₂ ht.1 (B _ hy hcy) hcy) } },
-  { have xt : x ∈ t, from B _ hx hcx,
-    have yt : y ∈ t, from B _ hy (hcx.trans hxy),
-    exact h₂ xt yt hxy }
-end
-
-/-- If `f` is monotone both on `(-∞, a]` and `[a, ∞)`, then it is monotone on the whole line. -/
-protected lemma monotone_on.Iic_union_Ici (h₁ : monotone_on f (Iic a))
-  (h₂ : monotone_on f (Ici a)) : monotone f :=
-begin
-  rw [← monotone_on_univ, ← @Iic_union_Ici _ _ a],
-  exact monotone_on.union_right h₁ h₂ is_greatest_Iic is_least_Ici
-end
-
-/-- If `f` is antitone both on `s` and `t`, with `s` to the left of `t` and the center
-point belonging to both `s` and `t`, then `f` is antitone on `s ∪ t` -/
-protected lemma antitone_on.union_right {s t : set α} {c : α} (h₁ : antitone_on f s)
-  (h₂ : antitone_on f t) (hs : is_greatest s c) (ht : is_least t c) :
-  antitone_on f (s ∪ t) :=
-(h₁.dual_right.union_right h₂.dual_right hs ht).dual_right
-
-/-- If `f` is antitone both on `(-∞, a]` and `[a, ∞)`, then it is antitone on the whole line. -/
-protected lemma antitone_on.Iic_union_Ici (h₁ : antitone_on f (Iic a))
-  (h₂ : antitone_on f (Ici a)) : antitone f :=
-(h₁.dual_right.Iic_union_Ici h₂.dual_right).dual_right
-
-/-- If a function is monotone on a set `s`, then it admits a monotone extension to the whole space
-provided `s` has a least element `a` and a greatest element `b`. -/
-lemma monotone_on.exists_monotone_extension {β : Type*} [conditionally_complete_linear_order β]
-  {f : α → β} {s : set α} (h : monotone_on f s) {a b : α}
-  (ha : is_least s a) (hb : is_greatest s b) :
-  ∃ g : α → β, monotone g ∧ eq_on f g s :=
-begin
-  /- The extension is defined by `f x = f a` for `x ≤ a`, and `f x` is the supremum of the values
-  of `f`  to the left of `x` for `x ≥ a`. -/
-  have aleb : a ≤ b := hb.2 ha.1,
-  have H : ∀ x ∈ s, f x = Sup (f '' (Icc a x ∩ s)),
-  { assume x xs,
-    have xmem : x ∈ Icc a x ∩ s := ⟨⟨ha.2 xs, le_rfl⟩, xs⟩,
-    have H : ∀ z, z ∈ f '' (Icc a x ∩ s) → z ≤ f x,
-    { rintros _ ⟨z, ⟨⟨az, zx⟩, zs⟩, rfl⟩,
-      exact h zs xs zx },
-    apply le_antisymm,
-    { exact le_cSup ⟨f x, H⟩ (mem_image_of_mem _ xmem) },
-    { exact cSup_le (nonempty_image_iff.2 ⟨x, xmem⟩) H } },
-  let g := λ x, if x ≤ a then f a else Sup (f '' (Icc a x ∩ s)),
-  have hfg : eq_on f g s,
-  { assume x xs,
-    dsimp only [g],
-    by_cases hxa : x ≤ a,
-    { have : x = a, from le_antisymm hxa (ha.2 xs),
-      simp only [if_true, this, le_refl] },
-    rw [if_neg hxa],
-    exact H x xs },
-  have M1 : monotone_on g (Iic a),
-  { rintros x (hx : x ≤ a) y (hy : y ≤ a) hxy,
-    dsimp only [g],
-    simp only [hx, hy, if_true] },
-  have g_eq : ∀ x ∈ Ici a, g x = Sup (f '' (Icc a x ∩ s)),
-  { rintros x ax,
-    dsimp only [g],
-    by_cases hxa : x ≤ a,
-    { have : x = a := le_antisymm hxa ax,
-      simp_rw [hxa, if_true, H a ha.1, this] },
-    simp only [hxa, if_false], },
-  have M2 : monotone_on g (Ici a),
-  { rintros x ax y ay hxy,
-    rw [g_eq x ax, g_eq y ay],
-    apply cSup_le_cSup,
-    { refine ⟨f b, _⟩,
-      rintros _ ⟨z, ⟨⟨az, zy⟩, zs⟩, rfl⟩,
-      exact h zs hb.1 (hb.2 zs) },
-    { exact ⟨f a, mem_image_of_mem _ ⟨⟨le_rfl, ax⟩, ha.1⟩⟩ },
-    { apply image_subset,
-      apply inter_subset_inter_left,
-      exact Icc_subset_Icc le_rfl hxy } },
-  exact ⟨g, M1.Iic_union_Ici M2, hfg⟩,
-end
-
-/-- If a function is antitone on a set `s`, then it admits an antitone extension to the whole space
-provided `s` has a least element `a` and a greatest element `b`. -/
-lemma antitone_on.exists_antitone_extension {β : Type*} [conditionally_complete_linear_order β]
-  {f : α → β} {s : set α} (h : antitone_on f s) {a b : α}
-  (ha : is_least s a) (hb : is_greatest s b) :
-  ∃ g : α → β, antitone g ∧ eq_on f g s :=
-h.dual_right.exists_monotone_extension ha hb
-
-end
-
-section ordered_group
-
-variables {G H : Type*} [linear_ordered_add_comm_group G] [ordered_add_comm_group H]
-
-lemma strict_mono_of_odd_strict_mono_on_nonneg {f : G → H} (h₁ : ∀ x, f (-x) = -f x)
-  (h₂ : strict_mono_on f (Ici 0)) :
-  strict_mono f :=
-begin
-  refine strict_mono_on.Iic_union_Ici (λ x hx y hy hxy, neg_lt_neg_iff.1 _) h₂,
-  rw [← h₁, ← h₁],
-  exact h₂ (neg_nonneg.2 hy) (neg_nonneg.2 hx) (neg_lt_neg hxy)
-end
-
-lemma monotone_of_odd_of_monotone_on_nonneg {f : G → H} (h₁ : ∀ x, f (-x) = -f x)
-  (h₂ : monotone_on f (Ici 0)) : monotone f :=
-begin
-  refine monotone_on.Iic_union_Ici (λ x hx y hy hxy, neg_le_neg_iff.1 _) h₂,
-  rw [← h₁, ← h₁],
-  exact h₂ (neg_nonneg.2 hy) (neg_nonneg.2 hx) (neg_le_neg hxy)
-end
-
-end ordered_group
-
-/-- In a linear ordered field, the whole field is order isomorphic to the open interval `(-1, 1)`.
-We consider the actual implementation to be a "black box", so it is irreducible.
--/
-@[irreducible] def order_iso_Ioo_neg_one_one (k : Type*) [linear_ordered_field k] :
-  k ≃o Ioo (-1 : k) 1 :=
-begin
-  refine strict_mono.order_iso_of_right_inverse _ _ (λ x, x / (1 - |x|)) _,
-  { refine cod_restrict (λ x, x / (1 + |x|)) _ (λ x, abs_lt.1 _),
-    have H : 0 < 1 + |x|, from (abs_nonneg x).trans_lt (lt_one_add _),
-    calc |x / (1 + |x|)| = |x| / (1 + |x|) : by rw [abs_div, abs_of_pos H]
-                     ... < 1               : (div_lt_one H).2 (lt_one_add _) },
-  { refine (strict_mono_of_odd_strict_mono_on_nonneg _ _).cod_restrict _,
-    { intro x, simp only [abs_neg, neg_div] },
-    { rintros x (hx : 0 ≤ x) y (hy : 0 ≤ y) hxy,
-      simp [abs_of_nonneg, mul_add, mul_comm x y, div_lt_div_iff,
-        hx.trans_lt (lt_one_add _), hy.trans_lt (lt_one_add _), *] } },
-  { refine λ x, subtype.ext _,
-    have : 0 < 1 - |(x : k)|, from sub_pos.2 (abs_lt.2 x.2),
-    field_simp [abs_div, this.ne', abs_of_pos this] }
-end
-
 section Ixx
 
 variables {α β : Type*} [preorder α] [preorder β] {f g : α → β} {s : set α}

src/order/iterate.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury G. Kudryashov
 -/
 import logic.function.iterate
-import order.monotone
+import order.monotone.basic
 
 /-!
 # Inequalities on iterates

src/order/lattice.lean

@@ -3,7 +3,7 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 -/
-import order.monotone
+import order.monotone.basic
 import tactic.simps
 import tactic.pi_instances