feat(algebra/ordered_*): arithmetic operations on monotone functions (#2634)

Also move `strict_mono` to `order/basic` and add a module docstring.

Author: urkud

src/algebra/order_functions.lean

@@ -3,7 +3,7 @@ Copyright (c) 2017 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import algebra.ordered_group
+import algebra.ordered_ring
 
 /-!
 # strictly monotone functions, max, min and abs
@@ -12,81 +12,16 @@ This file proves basic properties about strictly monotone functions,
 maxima and minima on a `decidable_linear_order`, and the absolute value
 function on linearly ordered add_comm_groups, semirings and rings.
 
-One useful result proved here is that if `f : ℕ → α` and `f n < f (n + 1)` for all `n`
-then f is strictly monotone (see `strict_mono.nat`).
-
-## Definition
-
-`strict_mono f` : a function between two types equipped with `<` is strictly monotone
-  if `a < b` implies `f a < f b`.
-
 ## Tags
 
-monotone, strictly monotone, min, max, abs
+min, max, abs
 -/
 
 universes u v
 variables {α : Type u} {β : Type v}
 
 attribute [simp] max_eq_left max_eq_right min_eq_left min_eq_right
 
-/-- A function `f` is strictly monotone if `a < b` implies `f a < f b`. -/
-def strict_mono [has_lt α] [has_lt β] (f : α → β) : Prop :=
-∀ ⦃a b⦄, a < b → f a < f b
-
-namespace strict_mono
-open ordering function
-
-section
-variables [linear_order α] [preorder β] {f : α → β}
-
-lemma lt_iff_lt (H : strict_mono f) {a b} :
-  f a < f b ↔ a < b :=
-⟨λ h, ((lt_trichotomy b a)
-  .resolve_left $ λ h', lt_asymm h $ H h')
-  .resolve_left $ λ e, ne_of_gt h $ congr_arg _ e, @H _ _⟩
-
-lemma injective (H : strict_mono f) : injective f
-| a b e := ((lt_trichotomy a b)
-  .resolve_left $ λ h, ne_of_lt (H h) e)
-  .resolve_right $ λ h, ne_of_gt (H h) e
-
-theorem compares (H : strict_mono f) {a b} :
-  ∀ {o}, compares o (f a) (f b) ↔ compares o a b
-| lt := H.lt_iff_lt
-| eq := ⟨λ h, H.injective h, congr_arg _⟩
-| gt := H.lt_iff_lt
-
-lemma le_iff_le (H : strict_mono f) {a b} :
-  f a ≤ f b ↔ a ≤ b :=
-⟨λ h, le_of_not_gt $ λ h', not_le_of_lt (H h') h,
- λ h, (lt_or_eq_of_le h).elim (λ h', le_of_lt (H h')) (λ h', h' ▸ le_refl _)⟩
-end
-
-protected lemma nat {β} [preorder β] {f : ℕ → β} (h : ∀n, f n < f (n+1)) : strict_mono f :=
-by { intros n m hnm, induction hnm with m' hnm' ih, apply h, exact lt.trans ih (h _) }
-
--- `preorder α` isn't strong enough: if the preorder on α is an equivalence relation,
--- then `strict_mono f` is vacuously true.
-lemma monotone [partial_order α] [preorder β] {f : α → β} (H : strict_mono f) : monotone f :=
-λ a b h, (lt_or_eq_of_le h).rec (le_of_lt ∘ (@H _ _)) (by rintro rfl; refl)
-
-end strict_mono
-
-section
-open function
-variables [partial_order α] [partial_order β] {f : α → β}
-
-lemma strict_mono_of_monotone_of_injective (h₁ : monotone f) (h₂ : injective f) :
-  strict_mono f :=
-λ a b h,
-begin
-  rw lt_iff_le_and_ne at ⊢ h,
-  exact ⟨h₁ h.1, λ e, h.2 (h₂ e)⟩
-end
-
-end
-
 section
 variables [decidable_linear_order α] [decidable_linear_order β] {f : α → β} {a b c d : α}
 
@@ -313,12 +248,6 @@ end decidable_linear_ordered_add_comm_group
 section decidable_linear_ordered_semiring
 variables [decidable_linear_ordered_semiring α] {a b c d : α}
 
-lemma monotone_mul_left_of_nonneg (ha : 0 ≤ a) : monotone (λ x, a*x) :=
-assume b c b_le_c, mul_le_mul_of_nonneg_left b_le_c ha
-
-lemma monotone_mul_right_of_nonneg (ha : 0 ≤ a) : monotone (λ x, x*a) :=
-assume b c b_le_c, mul_le_mul_of_nonneg_right b_le_c ha
-
 lemma mul_max_of_nonneg (b c : α) (ha : 0 ≤ a) : a * max b c = max (a * b) (a * c) :=
 (monotone_mul_left_of_nonneg ha).map_max
 

src/algebra/ordered_field.lean

@@ -138,6 +138,16 @@ lemma div_lt_div' (hac : a ≤ c) (hbd : d < b) (c0 : 0 < c) (d0 : 0 < d) :
   a / b < c / d :=
 (div_lt_div_iff (lt_trans d0 hbd) d0).2 (mul_lt_mul' hac hbd (le_of_lt d0) c0)
 
+lemma monotone.div_const {β : Type*} [preorder β] {f : β → α} (hf : monotone f)
+  {c : α} (hc : 0 ≤ c) :
+  monotone (λ x, (f x) / c) :=
+hf.mul_const (inv_nonneg.2 hc)
+
+lemma strict_mono.div_const {β : Type*} [preorder β] {f : β → α} (hf : strict_mono f)
+  {c : α} (hc : 0 < c) :
+  strict_mono (λ x, (f x) / c) :=
+hf.mul_const (inv_pos.2 hc)
+
 lemma half_pos {a : α} (h : 0 < a) : 0 < a / 2 := div_pos h two_pos
 
 lemma one_half_pos : (0:α) < 1 / 2 := half_pos zero_lt_one

src/algebra/ordered_group.lean

@@ -2,14 +2,16 @@
 Copyright (c) 2017 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Johannes Hölzl
-
-Ordered monoids and groups.
 -/
 import algebra.group.units
 import algebra.group.with_one
 import algebra.group.type_tags
 import order.bounded_lattice
 
+/-!
+# Ordered monoids and groups
+-/
+
 universe u
 variable {α : Type u}
 
@@ -135,6 +137,21 @@ iff.intro
 lemma bit0_pos {a : α} (h : 0 < a) : 0 < bit0 a :=
 add_pos' h h
 
+section mono
+
+variables {β : Type*} [preorder β] {f g : β → α}
+
+lemma monotone.add (hf : monotone f) (hg : monotone g) : monotone (λ x, f x + g x) :=
+λ x y h, add_le_add' (hf h) (hg h)
+
+lemma monotone.add_const (hf : monotone f) (a : α) : monotone (λ x, f x + a) :=
+hf.add monotone_const
+
+lemma monotone.const_add (hf : monotone f) (a : α) : monotone (λ x, a + f x) :=
+monotone_const.add hf
+
+end mono
+
 end ordered_add_comm_monoid
 
 namespace units
@@ -471,6 +488,20 @@ lemma with_top.add_lt_add_iff_right
   {a b c : with_top α} : a < ⊤ → (c + a < b + a ↔ c < b) :=
 by simpa [add_comm] using @with_top.add_lt_add_iff_left _ _ a b c
 
+section mono
+
+variables {β : Type*} [preorder β] {f g : β → α}
+
+lemma monotone.add_strict_mono (hf : monotone f) (hg : strict_mono g) :
+  strict_mono (λ x, f x + g x) :=
+λ x y h, add_lt_add_of_le_of_lt (hf $ le_of_lt h) (hg h)
+
+lemma strict_mono.add_monotone (hf : strict_mono f) (hg : monotone g) :
+  strict_mono (λ x, f x + g x) :=
+λ x y h, add_lt_add_of_lt_of_le (hf h) (hg $ le_of_lt h)
+
+end mono
+
 end ordered_cancel_comm_monoid
 
 section ordered_add_comm_group

src/algebra/ordered_ring.lean

@@ -184,6 +184,59 @@ lt_of_not_ge (λ ha, absurd h (not_lt_of_ge (mul_nonpos_of_nonneg_of_nonpos ha h
 lemma neg_of_mul_pos_right {a b : α} (h : 0 < a * b) (ha : a ≤ 0) : b < 0 :=
 lt_of_not_ge (λ hb, absurd h (not_lt_of_ge (mul_nonpos_of_nonpos_of_nonneg ha hb)))
 
+section mono
+
+variables {β : Type*} [preorder β] {f g : β → α} {a : α}
+
+lemma monotone_mul_left_of_nonneg (ha : 0 ≤ a) : monotone (λ x, a*x) :=
+assume b c b_le_c, mul_le_mul_of_nonneg_left b_le_c ha
+
+lemma monotone_mul_right_of_nonneg (ha : 0 ≤ a) : monotone (λ x, x*a) :=
+assume b c b_le_c, mul_le_mul_of_nonneg_right b_le_c ha
+
+lemma monotone.mul_const (hf : monotone f) (ha : 0 ≤ a) :
+  monotone (λ x, (f x) * a) :=
+(monotone_mul_right_of_nonneg ha).comp hf
+
+lemma monotone.const_mul (hf : monotone f) (ha : 0 ≤ a) :
+  monotone (λ x, a * (f x)) :=
+(monotone_mul_left_of_nonneg ha).comp hf
+
+lemma monotone.mul (hf : monotone f) (hg : monotone g) (hf0 : ∀ x, 0 ≤ f x) (hg0 : ∀ x, 0 ≤ g x) :
+  monotone (λ x, f x * g x) :=
+λ x y h, mul_le_mul (hf h) (hg h) (hg0 x) (hf0 y)
+
+lemma strict_mono_mul_left_of_pos (ha : 0 < a) : strict_mono (λ x, a * x) :=
+assume b c b_lt_c, (mul_lt_mul_left ha).2 b_lt_c
+
+lemma strict_mono_mul_right_of_pos (ha : 0 < a) : strict_mono (λ x, x * a) :=
+assume b c b_lt_c, (mul_lt_mul_right ha).2 b_lt_c
+
+lemma strict_mono.mul_const (hf : strict_mono f) (ha : 0 < a) :
+  strict_mono (λ x, (f x) * a) :=
+(strict_mono_mul_right_of_pos ha).comp hf
+
+lemma strict_mono.const_mul (hf : strict_mono f) (ha : 0 < a) :
+  strict_mono (λ x, a * (f x)) :=
+(strict_mono_mul_left_of_pos ha).comp hf
+
+lemma strict_mono.mul_monotone (hf : strict_mono f) (hg : monotone g) (hf0 : ∀ x, 0 ≤ f x)
+  (hg0 : ∀ x, 0 < g x) :
+  strict_mono (λ x, f x * g x) :=
+λ x y h, mul_lt_mul (hf h) (hg $ le_of_lt h) (hg0 x) (hf0 y)
+
+lemma monotone.mul_strict_mono (hf : monotone f) (hg : strict_mono g) (hf0 : ∀ x, 0 < f x)
+  (hg0 : ∀ x, 0 ≤ g x) :
+  strict_mono (λ x, f x * g x) :=
+λ x y h, mul_lt_mul' (hf $ le_of_lt h) (hg h) (hg0 x) (hf0 y)
+
+lemma strict_mono.mul (hf : strict_mono f) (hg : strict_mono g) (hf0 : ∀ x, 0 ≤ f x)
+  (hg0 : ∀ x, 0 ≤ g x) :
+  strict_mono (λ x, f x * g x) :=
+λ x y h, mul_lt_mul'' (hf h) (hg h) (hf0 x) (hg0 x)
+
+end mono
+
 end linear_ordered_semiring
 
 section decidable_linear_ordered_semiring