feat: f a ≤ f (succ a) → Monotone f (#18008)

From GrowthInGroups

Mathlib/Algebra/Order/SuccPred.lean

@@ -6,7 +6,7 @@ Authors: Violeta Hernández Palacios, Yaël Dillies
 import Mathlib.Algebra.Group.Basic
 import Mathlib.Algebra.Order.ZeroLEOne
 import Mathlib.Data.Int.Cast.Defs
-import Mathlib.Order.SuccPred.Basic
+import Mathlib.Order.SuccPred.Archimedean
 
 /-!
 # Interaction between successors and arithmetic
@@ -183,3 +183,73 @@ theorem lt_one_iff_nonpos [AddMonoidWithOne α] [ZeroLEOneClass α] [NeZero (1 :
 end LinearOrder
 
 end Order
+
+section Monotone
+variable {α β : Type*} [PartialOrder α] [Preorder β]
+
+section SuccAddOrder
+variable [Add α] [One α] [SuccAddOrder α] [IsSuccArchimedean α] {s : Set α} {f : α → β}
+
+lemma monotoneOn_of_le_add_one (hs : s.OrdConnected) :
+    (∀ a, ¬ IsMax a → a ∈ s → a + 1 ∈ s → f a ≤ f (a + 1)) → MonotoneOn f s := by
+  simpa [Order.succ_eq_add_one] using monotoneOn_of_le_succ hs (f := f)
+
+lemma antitoneOn_of_add_one_le (hs : s.OrdConnected) :
+    (∀ a, ¬ IsMax a → a ∈ s → a + 1 ∈ s → f (a + 1) ≤ f a) → AntitoneOn f s := by
+  simpa [Order.succ_eq_add_one] using antitoneOn_of_succ_le hs (f := f)
+
+lemma strictMonoOn_of_lt_add_one (hs : s.OrdConnected) :
+    (∀ a, ¬ IsMax a → a ∈ s → a + 1 ∈ s → f a < f (a + 1)) → StrictMonoOn f s := by
+  simpa [Order.succ_eq_add_one] using strictMonoOn_of_lt_succ hs (f := f)
+
+lemma strictAntiOn_of_add_one_lt (hs : s.OrdConnected) :
+    (∀ a, ¬ IsMax a → a ∈ s → a + 1 ∈ s → f (a + 1) < f a) → StrictAntiOn f s := by
+  simpa [Order.succ_eq_add_one] using strictAntiOn_of_succ_lt hs (f := f)
+
+lemma monotone_of_le_add_one : (∀ a, ¬ IsMax a → f a ≤ f (a + 1)) → Monotone f := by
+  simpa [Order.succ_eq_add_one] using monotone_of_le_succ (f := f)
+
+lemma antitone_of_add_one_le : (∀ a, ¬ IsMax a → f (a + 1) ≤ f a) → Antitone f := by
+  simpa [Order.succ_eq_add_one] using antitone_of_succ_le (f := f)
+
+lemma strictMono_of_lt_add_one : (∀ a, ¬ IsMax a → f a < f (a + 1)) → StrictMono f := by
+  simpa [Order.succ_eq_add_one] using strictMono_of_lt_succ (f := f)
+
+lemma strictAnti_of_add_one_lt : (∀ a, ¬ IsMax a → f (a + 1) < f a) → StrictAnti f := by
+  simpa [Order.succ_eq_add_one] using strictAnti_of_succ_lt (f := f)
+
+end SuccAddOrder
+
+section PredSubOrder
+variable [Sub α] [One α] [PredSubOrder α] [IsPredArchimedean α] {s : Set α} {f : α → β}
+
+lemma monotoneOn_of_sub_one_le (hs : s.OrdConnected) :
+    (∀ a, ¬ IsMin a → a ∈ s → a - 1 ∈ s → f (a - 1) ≤ f a) → MonotoneOn f s := by
+  simpa [Order.pred_eq_sub_one] using monotoneOn_of_pred_le hs (f := f)
+
+lemma antitoneOn_of_le_sub_one (hs : s.OrdConnected) :
+    (∀ a, ¬ IsMin a → a ∈ s → a - 1 ∈ s → f a ≤ f (a - 1)) → AntitoneOn f s := by
+  simpa [Order.pred_eq_sub_one] using antitoneOn_of_le_pred hs (f := f)
+
+lemma strictMonoOn_of_sub_one_lt (hs : s.OrdConnected) :
+    (∀ a, ¬ IsMin a → a ∈ s → a - 1 ∈ s → f (a - 1) < f a) → StrictMonoOn f s := by
+  simpa [Order.pred_eq_sub_one] using strictMonoOn_of_pred_lt hs (f := f)
+
+lemma strictAntiOn_of_lt_sub_one (hs : s.OrdConnected) :
+    (∀ a, ¬ IsMin a → a ∈ s → a - 1 ∈ s → f a < f (a - 1)) → StrictAntiOn f s := by
+  simpa [Order.pred_eq_sub_one] using strictAntiOn_of_lt_pred hs (f := f)
+
+lemma monotone_of_sub_one_le : (∀ a, ¬ IsMin a → f (a - 1) ≤ f a) → Monotone f := by
+  simpa [Order.pred_eq_sub_one] using monotone_of_pred_le (f := f)
+
+lemma antitone_of_le_sub_one : (∀ a, ¬ IsMin a → f a ≤ f (a - 1)) → Antitone f := by
+  simpa [Order.pred_eq_sub_one] using antitone_of_le_pred (f := f)
+
+lemma strictMono_of_sub_one_lt : (∀ a, ¬ IsMin a → f (a - 1) < f a) → StrictMono f := by
+  simpa [Order.pred_eq_sub_one] using strictMono_of_pred_lt (f := f)
+
+lemma strictAnti_of_lt_sub_one : (∀ a, ¬ IsMin a → f a < f (a - 1)) → StrictAnti f := by
+  simpa [Order.pred_eq_sub_one] using strictAnti_of_lt_pred (f := f)
+
+end PredSubOrder
+end Monotone

Mathlib/Order/Interval/Set/Monotone.lean

@@ -164,58 +164,22 @@ variable {α β : Type*} [PartialOrder α] [Preorder β] {ψ : α → β}
 /-- A function `ψ` on a `SuccOrder` is strictly monotone before some `n` if for all `m` such that
 `m < n`, we have `ψ m < ψ (succ m)`. -/
 theorem strictMonoOn_Iic_of_lt_succ [SuccOrder α] [IsSuccArchimedean α] {n : α}
-    (hψ : ∀ m, m < n → ψ m < ψ (succ m)) : StrictMonoOn ψ (Set.Iic n) := by
-  intro x hx y hy hxy
-  obtain ⟨i, rfl⟩ := hxy.le.exists_succ_iterate
-  induction' i with k ih
-  · simp at hxy
-  cases' k with k
-  · exact hψ _ (lt_of_lt_of_le hxy hy)
-  rw [Set.mem_Iic] at *
-  simp only [Function.iterate_succ', Function.comp_apply] at ih hxy hy ⊢
-  by_cases hmax : IsMax (succ^[k] x)
-  · rw [succ_eq_iff_isMax.2 hmax] at hxy ⊢
-    exact ih (le_trans (le_succ _) hy) hxy
-  by_cases hmax' : IsMax (succ (succ^[k] x))
-  · rw [succ_eq_iff_isMax.2 hmax'] at hxy ⊢
-    exact ih (le_trans (le_succ _) hy) hxy
-  refine
-    lt_trans
-      (ih (le_trans (le_succ _) hy)
-        (lt_of_le_of_lt (le_succ_iterate k _) (lt_succ_iff_not_isMax.2 hmax)))
-      ?_
-  rw [← Function.comp_apply (f := succ), ← Function.iterate_succ']
-  refine hψ _ (lt_of_lt_of_le ?_ hy)
-  rwa [Function.iterate_succ', Function.comp_apply, lt_succ_iff_not_isMax]
-
-theorem strictMono_of_lt_succ [SuccOrder α] [IsSuccArchimedean α]
-    (hψ : ∀ m, ψ m < ψ (succ m)) : StrictMono ψ := fun _ _ h ↦
-  (strictMonoOn_Iic_of_lt_succ fun m _ ↦ hψ m) h.le le_rfl h
+    (hψ : ∀ m, m < n → ψ m < ψ (succ m)) : StrictMonoOn ψ (Set.Iic n) :=
+  strictMonoOn_of_lt_succ ordConnected_Iic fun _a ha' _ ha ↦
+    hψ _ <| (succ_le_iff_of_not_isMax ha').1 ha
 
 theorem strictAntiOn_Iic_of_succ_lt [SuccOrder α] [IsSuccArchimedean α] {n : α}
     (hψ : ∀ m, m < n → ψ (succ m) < ψ m) : StrictAntiOn ψ (Set.Iic n) := fun i hi j hj hij =>
   @strictMonoOn_Iic_of_lt_succ α βᵒᵈ _ _ ψ _ _ n hψ i hi j hj hij
 
-theorem strictAnti_of_succ_lt [SuccOrder α] [IsSuccArchimedean α]
-    (hψ : ∀ m, ψ (succ m) < ψ m) : StrictAnti ψ := fun _ _ h ↦
-  (strictAntiOn_Iic_of_succ_lt fun m _ ↦ hψ m) h.le le_rfl h
-
 theorem strictMonoOn_Ici_of_pred_lt [PredOrder α] [IsPredArchimedean α] {n : α}
     (hψ : ∀ m, n < m → ψ (pred m) < ψ m) : StrictMonoOn ψ (Set.Ici n) := fun i hi j hj hij =>
   @strictMonoOn_Iic_of_lt_succ αᵒᵈ βᵒᵈ _ _ ψ _ _ n hψ j hj i hi hij
 
-theorem strictMono_of_pred_lt [PredOrder α] [IsPredArchimedean α]
-    (hψ : ∀ m, ψ (pred m) < ψ m) : StrictMono ψ := fun _ _ h ↦
-  (strictMonoOn_Ici_of_pred_lt fun m _ ↦ hψ m) le_rfl h.le h
-
 theorem strictAntiOn_Ici_of_lt_pred [PredOrder α] [IsPredArchimedean α] {n : α}
     (hψ : ∀ m, n < m → ψ m < ψ (pred m)) : StrictAntiOn ψ (Set.Ici n) := fun i hi j hj hij =>
   @strictAntiOn_Iic_of_succ_lt αᵒᵈ βᵒᵈ _ _ ψ _ _ n hψ j hj i hi hij
 
-theorem strictAnti_of_lt_pred [PredOrder α] [IsPredArchimedean α]
-    (hψ : ∀ m, ψ m < ψ (pred m)) : StrictAnti ψ := fun _ _ h ↦
-  (strictAntiOn_Ici_of_lt_pred fun m _ ↦ hψ m) le_rfl h.le h
-
 end SuccOrder
 
 section LinearOrder

Mathlib/Order/SuccPred/Archimedean.lean

@@ -396,3 +396,117 @@ instance Set.OrdConnected.isSuccArchimedean [SuccOrder α] [IsSuccArchimedean α
   inferInstanceAs (IsSuccArchimedean sᵒᵈᵒᵈ)
 
 end OrdConnected
+
+section Monotone
+variable {α β : Type*} [PartialOrder α] [Preorder β]
+
+section SuccOrder
+variable [SuccOrder α] [IsSuccArchimedean α] {s : Set α} {f : α → β}
+
+lemma monotoneOn_of_le_succ (hs : s.OrdConnected)
+    (hf : ∀ a, ¬ IsMax a → a ∈ s → succ a ∈ s → f a ≤ f (succ a)) : MonotoneOn f s := by
+  rintro a ha b hb hab
+  obtain ⟨n, rfl⟩ := exists_succ_iterate_of_le hab
+  clear hab
+  induction' n with n hn
+  · simp
+  rw [Function.iterate_succ_apply'] at hb ⊢
+  have : succ^[n] a ∈ s := hs.1 ha hb ⟨le_succ_iterate .., le_succ _⟩
+  by_cases hb' : IsMax (succ^[n] a)
+  · rw [succ_eq_iff_isMax.2 hb']
+    exact hn this
+  · exact (hn this).trans (hf _ hb' this hb)
+
+lemma antitoneOn_of_succ_le (hs : s.OrdConnected)
+    (hf : ∀ a, ¬ IsMax a → a ∈ s → succ a ∈ s → f (succ a) ≤ f a) : AntitoneOn f s :=
+  monotoneOn_of_le_succ (β := βᵒᵈ) hs hf
+
+lemma strictMonoOn_of_lt_succ (hs : s.OrdConnected)
+    (hf : ∀ a, ¬ IsMax a → a ∈ s → succ a ∈ s → f a < f (succ a)) : StrictMonoOn f s := by
+  rintro a ha b hb hab
+  obtain ⟨n, rfl⟩ := exists_succ_iterate_of_le hab.le
+  obtain _ | n := n
+  · simp at hab
+  apply not_isMax_of_lt at hab
+  induction' n with n hn
+  · simpa using hf _ hab ha hb
+  rw [Function.iterate_succ_apply'] at hb ⊢
+  have : succ^[n + 1] a ∈ s := hs.1 ha hb ⟨le_succ_iterate .., le_succ _⟩
+  by_cases hb' : IsMax (succ^[n + 1] a)
+  · rw [succ_eq_iff_isMax.2 hb']
+    exact hn this
+  · exact (hn this).trans (hf _ hb' this hb)
+
+lemma strictAntiOn_of_succ_lt (hs : s.OrdConnected)
+    (hf : ∀ a, ¬ IsMax a → a ∈ s → succ a ∈ s → f (succ a) < f a) : StrictAntiOn f s :=
+  strictMonoOn_of_lt_succ (β := βᵒᵈ) hs hf
+
+lemma monotone_of_le_succ (hf : ∀ a, ¬ IsMax a → f a ≤ f (succ a)) : Monotone f := by
+  simpa using monotoneOn_of_le_succ Set.ordConnected_univ (by simpa using hf)
+
+lemma antitone_of_succ_le (hf : ∀ a, ¬ IsMax a → f (succ a) ≤ f a) : Antitone f := by
+  simpa using antitoneOn_of_succ_le Set.ordConnected_univ (by simpa using hf)
+
+lemma strictMono_of_lt_succ (hf : ∀ a, ¬ IsMax a → f a < f (succ a)) : StrictMono f := by
+  simpa using strictMonoOn_of_lt_succ Set.ordConnected_univ (by simpa using hf)
+
+lemma strictAnti_of_succ_lt (hf : ∀ a, ¬ IsMax a → f (succ a) < f a) : StrictAnti f := by
+  simpa using strictAntiOn_of_succ_lt Set.ordConnected_univ (by simpa using hf)
+
+end SuccOrder
+
+section PredOrder
+variable [PredOrder α] [IsPredArchimedean α] {s : Set α} {f : α → β}
+
+lemma monotoneOn_of_pred_le (hs : s.OrdConnected)
+    (hf : ∀ a, ¬ IsMin a → a ∈ s → pred a ∈ s → f (pred a) ≤ f a) : MonotoneOn f s := by
+  rintro a ha b hb hab
+  obtain ⟨n, rfl⟩ := exists_pred_iterate_of_le hab
+  clear hab
+  induction' n with n hn
+  · simp
+  rw [Function.iterate_succ_apply'] at ha ⊢
+  have : pred^[n] b ∈ s := hs.1 ha hb ⟨pred_le _, pred_iterate_le ..⟩
+  by_cases ha' : IsMin (pred^[n] b)
+  · rw [pred_eq_iff_isMin.2 ha']
+    exact hn this
+  · exact (hn this).trans' (hf _ ha' this ha)
+
+lemma antitoneOn_of_le_pred (hs : s.OrdConnected)
+    (hf : ∀ a, ¬ IsMin a → a ∈ s → pred a ∈ s → f a ≤ f (pred a)) : AntitoneOn f s :=
+  monotoneOn_of_pred_le (β := βᵒᵈ) hs hf
+
+lemma strictMonoOn_of_pred_lt (hs : s.OrdConnected)
+    (hf : ∀ a, ¬ IsMin a → a ∈ s → pred a ∈ s → f (pred a) < f a) : StrictMonoOn f s := by
+  rintro a ha b hb hab
+  obtain ⟨n, rfl⟩ := exists_pred_iterate_of_le hab.le
+  obtain _ | n := n
+  · simp at hab
+  apply not_isMin_of_lt at hab
+  induction' n with n hn
+  · simpa using hf _ hab hb ha
+  rw [Function.iterate_succ_apply'] at ha ⊢
+  have : pred^[n + 1] b ∈ s := hs.1 ha hb ⟨pred_le _, pred_iterate_le ..⟩
+  by_cases ha' : IsMin (pred^[n + 1] b)
+  · rw [pred_eq_iff_isMin.2 ha']
+    exact hn this
+  · exact (hn this).trans' (hf _ ha' this ha)
+
+lemma strictAntiOn_of_lt_pred (hs : s.OrdConnected)
+    (hf : ∀ a, ¬ IsMin a → a ∈ s → pred a ∈ s → f a < f (pred a)) : StrictAntiOn f s :=
+  strictMonoOn_of_pred_lt (β := βᵒᵈ) hs hf
+
+lemma monotone_of_pred_le (hf : ∀ a, ¬ IsMin a → f (pred a) ≤ f a) : Monotone f := by
+  simpa using monotoneOn_of_pred_le Set.ordConnected_univ (by simpa using hf)
+
+lemma antitone_of_le_pred (hf : ∀ a, ¬ IsMin a → f a ≤ f (pred a)) : Antitone f := by
+  simpa using antitoneOn_of_le_pred Set.ordConnected_univ (by simpa using hf)
+
+lemma strictMono_of_pred_lt (hf : ∀ a, ¬ IsMin a → f (pred a) < f a) : StrictMono f := by
+  simpa using strictMonoOn_of_pred_lt Set.ordConnected_univ (by simpa using hf)
+
+lemma strictAnti_of_lt_pred (hf : ∀ a, ¬ IsMin a → f a < f (pred a)) : StrictAnti f := by
+  simpa using strictAntiOn_of_lt_pred Set.ordConnected_univ (by simpa using hf)
+
+end PredOrder
+end Monotone