chore(data/*): flipping inequalities (#1436)

* chore(data/*): flipping inequalities

* some more

* Update src/algebra/order_functions.lean

* fixing some names

* fix

* fixes

* fixes

* making names/comments uniform

* fixes

* fixes

* fix

* rename

* fixes

* fixes

* fix

* renames

* I'm so bad at this

* ...

* fixes

Author: kim-em

src/algebra/archimedean.lean

@@ -24,17 +24,17 @@ let ⟨n, h⟩ := archimedean.arch x zero_lt_one in
 section linear_ordered_ring
 variables [linear_ordered_ring α] [archimedean α]
 
-lemma pow_unbounded_of_gt_one (x : α) {y : α}
+lemma pow_unbounded_of_one_lt (x : α) {y : α}
     (hy1 : 1 < y) : ∃ n : ℕ, x < y ^ n :=
 have hy0 : 0 <  y - 1 := sub_pos_of_lt hy1,
 let ⟨n, h⟩ := archimedean.arch x hy0 in
 ⟨n, calc x ≤ n • (y - 1)     : h
        ... < 1 + n • (y - 1) : by rw add_comm; exact lt_add_one _
-       ... ≤ y ^ n           : pow_ge_one_add_sub_mul (le_of_lt hy1) _⟩
+       ... ≤ y ^ n           : one_add_sub_mul_le_pow (le_of_lt hy1) _⟩
 
 lemma exists_nat_pow_near {x : α} {y : α} (hx : 1 < x) (hy : 1 < y) :
   ∃ n : ℕ, y ^ n ≤ x ∧ x < y ^ (n + 1) :=
-have h : ∃ n : ℕ, x < y ^ n, from pow_unbounded_of_gt_one _ hy,
+have h : ∃ n : ℕ, x < y ^ n, from pow_unbounded_of_one_lt _ hy,
 by classical; exact let n := nat.find h in
   have hn  : x < y ^ n, from nat.find_spec h,
   have hnp : 0 < n,     from nat.pos_iff_ne_zero.2 (λ hn0,
@@ -71,11 +71,11 @@ lemma exists_int_pow_near [discrete_linear_ordered_field α] [archimedean α]
   {x : α} {y : α} (hx : 0 < x) (hy : 1 < y) :
   ∃ n : ℤ, y ^ n ≤ x ∧ x < y ^ (n + 1) :=
 by classical; exact
-let ⟨N, hN⟩ := pow_unbounded_of_gt_one x⁻¹ hy in
+let ⟨N, hN⟩ := pow_unbounded_of_one_lt x⁻¹ hy in
   have he: ∃ m : ℤ, y ^ m ≤ x, from
     ⟨-N, le_of_lt (by rw [(fpow_neg y (↑N)), one_div_eq_inv];
     exact (inv_lt hx (lt_trans (inv_pos hx) hN)).1 hN)⟩,
-let ⟨M, hM⟩ := pow_unbounded_of_gt_one x hy in
+let ⟨M, hM⟩ := pow_unbounded_of_one_lt x hy in
   have hb: ∃ b : ℤ, ∀ m, y ^ m ≤ x → m ≤ b, from
     ⟨M, λ m hm, le_of_not_lt (λ hlt, not_lt_of_ge
   (fpow_le_of_le (le_of_lt hy) (le_of_lt hlt)) (lt_of_le_of_lt hm hM))⟩,

src/algebra/field_power.lean

@@ -108,11 +108,11 @@ open int
 
 variables {α : Type u} [discrete_linear_ordered_field α]
 
-lemma fpow_nonneg_of_nonneg {a : α} (ha : a ≥ 0) : ∀ (z : ℤ), a ^ z ≥ 0
+lemma fpow_nonneg_of_nonneg {a : α} (ha : 0 ≤ a) : ∀ (z : ℤ), 0 ≤ a ^ z
 | (of_nat n) := pow_nonneg ha _
 | -[1+n] := div_nonneg' zero_le_one $ pow_nonneg ha _
 
-lemma fpow_pos_of_pos {a : α} (ha : a > 0) : ∀ (z : ℤ), a ^ z > 0
+lemma fpow_pos_of_pos {a : α} (ha : 0 < a) : ∀ (z : ℤ), 0 < a ^ z
 | (of_nat n) := pow_pos ha _
 | -[1+n] := div_pos zero_lt_one $ pow_pos ha _
 
@@ -136,7 +136,7 @@ begin
     repeat { apply pow_pos (lt_of_lt_of_le zero_lt_one hx) } }
 end
 
-lemma pow_le_max_of_min_le {x : α} (hx : x ≥ 1) {a b c : ℤ} (h : min a b ≤ c) :
+lemma pow_le_max_of_min_le {x : α} (hx : 1 ≤ x) {a b c : ℤ} (h : min a b ≤ c) :
       x ^ (-c) ≤ max (x ^ (-a)) (x ^ (-b)) :=
 begin
   wlog hle : a ≤ b,
@@ -148,17 +148,17 @@ begin
   simpa only [max_eq_left hfle]
 end
 
-lemma fpow_le_one_of_nonpos {p : α} (hp : p ≥ 1) {z : ℤ} (hz : z ≤ 0) : p ^ z ≤ 1 :=
+lemma fpow_le_one_of_nonpos {p : α} (hp : 1 ≤ p) {z : ℤ} (hz : z ≤ 0) : p ^ z ≤ 1 :=
 calc p ^ z ≤ p ^ 0 : fpow_le_of_le hp hz
           ... = 1        : by simp
 
-lemma fpow_ge_one_of_nonneg {p : α} (hp : p ≥ 1) {z : ℤ} (hz : z ≥ 0) : p ^ z ≥ 1 :=
+lemma one_le_fpow_of_nonneg {p : α} (hp : 1 ≤ p) {z : ℤ} (hz : 0 ≤ z) : 1 ≤ p ^ z :=
 calc p ^ z ≥ p ^ 0 : fpow_le_of_le hp hz
           ... = 1        : by simp
 
 end ordered_field_power
 
-lemma one_lt_pow {α} [linear_ordered_semiring α] {p : α} (hp : p > 1) : ∀ {n : ℕ}, 1 ≤ n → 1 < p ^ n
+lemma one_lt_pow {α} [linear_ordered_semiring α] {p : α} (hp : 1 < p) : ∀ {n : ℕ}, 1 ≤ n → 1 < p ^ n
 | 1 h := by simp; assumption
 | (k+2) h :=
   begin
@@ -170,6 +170,6 @@ lemma one_lt_pow {α} [linear_ordered_semiring α] {p : α} (hp : p > 1) : ∀ {
     { apply le_of_lt (lt_trans zero_lt_one hp) }
   end
 
-lemma one_lt_fpow {α}  [discrete_linear_ordered_field α] {p : α} (hp : p > 1) :
-  ∀ z : ℤ, z > 0 → 1 < p ^ z
+lemma one_lt_fpow {α}  [discrete_linear_ordered_field α] {p : α} (hp : 1 < p) :
+  ∀ z : ℤ, 0 < z → 1 < p ^ z
 | (int.of_nat n) h := one_lt_pow hp (nat.succ_le_of_lt (int.lt_of_coe_nat_lt_coe_nat h))

src/algebra/floor.lean

@@ -218,7 +218,7 @@ lemma ceil_pos {a : α} : 0 < ⌈a⌉ ↔ 0 < a :=
 
 @[simp] theorem ceil_zero : ⌈(0 : α)⌉ = 0 := by simp [ceil]
 
-lemma ceil_nonneg [decidable_rel ((<) : α → α → Prop)] {q : α} (hq : q ≥ 0) : ⌈q⌉ ≥ 0 :=
+lemma ceil_nonneg [decidable_rel ((<) : α → α → Prop)] {q : α} (hq : 0 ≤ q) : 0 ≤ ⌈q⌉ :=
 if h : q > 0 then le_of_lt $ ceil_pos.2 h
 else by rw [le_antisymm (le_of_not_lt h) hq, ceil_zero]; trivial
 

src/algebra/gcd_domain.lean

@@ -465,10 +465,10 @@ by simp [(int.coe_nat_eq_coe_nat_iff _ _).symm, coe_gcd, coe_nat_abs_eq_normaliz
 theorem gcd_mul_right (i j k : ℤ) : gcd (i * j) (k * j) = gcd i k * nat_abs j :=
 by simp [(int.coe_nat_eq_coe_nat_iff _ _).symm, coe_gcd, coe_nat_abs_eq_normalize]
 
-theorem gcd_pos_of_non_zero_left {i : ℤ} (j : ℤ) (i_non_zero : i ≠ 0) : gcd i j > 0 :=
+theorem gcd_pos_of_non_zero_left {i : ℤ} (j : ℤ) (i_non_zero : i ≠ 0) : 0 < gcd i j :=
 nat.gcd_pos_of_pos_left (nat_abs j) (nat_abs_pos_of_ne_zero i_non_zero)
 
-theorem gcd_pos_of_non_zero_right (i : ℤ) {j : ℤ} (j_non_zero : j ≠ 0) : gcd i j > 0 :=
+theorem gcd_pos_of_non_zero_right (i : ℤ) {j : ℤ} (j_non_zero : j ≠ 0) : 0 < gcd i j :=
 nat.gcd_pos_of_pos_right (nat_abs i) (nat_abs_pos_of_ne_zero j_non_zero)
 
 theorem gcd_eq_zero_iff {i j : ℤ} : gcd i j = 0 ↔ i = 0 ∧ j = 0 :=

src/algebra/group_power.lean

@@ -167,11 +167,11 @@ by induction n with n ih; [exact one_inv.symm,
 @[simp] theorem add_monoid.neg_smul : ∀ (a : β) (n : ℕ), n•(-a) = -(n•a) :=
 @inv_pow (multiplicative β) _
 
-theorem pow_sub (a : α) {m n : ℕ} (h : m ≥ n) : a^(m - n) = a^m * (a^n)⁻¹ :=
+theorem pow_sub (a : α) {m n : ℕ} (h : n ≤ m) : a^(m - n) = a^m * (a^n)⁻¹ :=
 have h1 : m - n + n = m, from nat.sub_add_cancel h,
 have h2 : a^(m - n) * a^n = a^m, by rw [←pow_add, h1],
 eq_mul_inv_of_mul_eq h2
-theorem add_monoid.smul_sub : ∀ (a : β) {m n : ℕ}, m ≥ n → (m - n)•a = m•a - n•a :=
+theorem add_monoid.smul_sub : ∀ (a : β) {m n : ℕ}, n ≤ m → (m - n)•a = m•a - n•a :=
 @pow_sub (multiplicative β) _
 
 theorem pow_inv_comm (a : α) (m n : ℕ) : (a⁻¹)^m * a^n = a^n * (a⁻¹)^m :=
@@ -524,13 +524,13 @@ theorem one_le_pow_of_one_le {a : α} (H : 1 ≤ a) : ∀ (n : ℕ), 1 ≤ a ^ n
 | (n+1) := by simpa only [mul_one] using mul_le_mul H (one_le_pow_of_one_le n)
     zero_le_one (le_trans zero_le_one H)
 
-theorem pow_ge_one_add_mul {a : α} (H : a ≥ 0) :
+theorem one_add_mul_le_pow {a : α} (H : 0 ≤ a) :
   ∀ (n : ℕ), 1 + n • a ≤ (1 + a) ^ n
 | 0     := le_of_eq $ add_zero _
 | (n+1) := begin
   rw [pow_succ', succ_smul'],
   refine le_trans _ (mul_le_mul_of_nonneg_right
-    (pow_ge_one_add_mul n) (add_nonneg zero_le_one H)),
+    (one_add_mul_le_pow n) (add_nonneg zero_le_one H)),
   rw [mul_add, mul_one, ← add_assoc, add_le_add_iff_left],
   simpa only [one_mul] using mul_le_mul_of_nonneg_right
     ((le_add_iff_nonneg_right 1).2 (add_monoid.smul_nonneg H n)) H
@@ -595,9 +595,9 @@ end linear_ordered_semiring
 theorem pow_two_nonneg [linear_ordered_ring α] (a : α) : 0 ≤ a ^ 2 :=
 by rw pow_two; exact mul_self_nonneg _
 
-theorem pow_ge_one_add_sub_mul [linear_ordered_ring α]
-  {a : α} (H : a ≥ 1) (n : ℕ) : 1 + n • (a - 1) ≤ a ^ n :=
-by simpa only [add_sub_cancel'_right] using pow_ge_one_add_mul (sub_nonneg.2 H) n
+theorem one_add_sub_mul_le_pow [linear_ordered_ring α]
+  {a : α} (H : 1 ≤ a) (n : ℕ) : 1 + n • (a - 1) ≤ a ^ n :=
+by simpa only [add_sub_cancel'_right] using one_add_mul_le_pow (sub_nonneg.2 H) n
 
 namespace int
 

src/algebra/order.lean

@@ -152,7 +152,7 @@ begin
   apply h₂, apply le_antisymm; apply le_of_not_gt; assumption
 end
 
-lemma ne_iff_lt_or_gt [decidable_linear_order α] {a b : α} : a ≠ b ↔ a < b ∨ a > b :=
+lemma ne_iff_lt_or_gt [decidable_linear_order α] {a b : α} : a ≠ b ↔ a < b ∨ b < a :=
 ⟨lt_or_gt_of_ne, λo, o.elim ne_of_lt ne_of_gt⟩
 
 lemma le_imp_le_of_lt_imp_lt {β} [preorder α] [decidable_linear_order β]

src/algebra/order_functions.lean

@@ -208,7 +208,7 @@ def sub_abs_le_abs_sub := @abs_sub_abs_le_abs_sub
 lemma abs_abs_sub_le_abs_sub (a b : α) : abs (abs a - abs b) ≤ abs (a - b) :=
 abs_sub_le_iff.2 ⟨sub_abs_le_abs_sub _ _, by rw abs_sub; apply sub_abs_le_abs_sub⟩
 
-lemma abs_eq (hb : b ≥ 0) : abs a = b ↔ a = b ∨ a = -b :=
+lemma abs_eq (hb : 0 ≤ b) : abs a = b ↔ a = b ∨ a = -b :=
 iff.intro
   begin
     cases le_total a 0 with a_nonpos a_nonneg,

src/algebra/ordered_group.lean

@@ -46,11 +46,11 @@ ordered_comm_monoid.lt_of_add_lt_add_left a b c
 lemma add_le_add' (h₁ : a ≤ b) (h₂ : c ≤ d) : a + c ≤ b + d :=
 le_trans (add_le_add_right' h₁) (add_le_add_left' h₂)
 
-lemma le_add_of_nonneg_right' (h : b ≥ 0) : a ≤ a + b :=
+lemma le_add_of_nonneg_right' (h : 0 ≤ b) : a ≤ a + b :=
 have a + b ≥ a + 0, from add_le_add_left' h,
 by rwa add_zero at this
 
-lemma le_add_of_nonneg_left' (h : b ≥ 0) : a ≤ b + a :=
+lemma le_add_of_nonneg_left' (h : 0 ≤ b) : a ≤ b + a :=
 have 0 + a ≤ b + a, from add_le_add_right' h,
 by rwa zero_add at this
 

src/algebra/ordered_ring.lean

@@ -8,10 +8,14 @@ import tactic.split_ifs order.basic algebra.order algebra.ordered_group algebra.
 universe u
 variable {α : Type u}
 
--- TODO: this is necessary additionally to mul_nonneg otherwise the simplifier can not match
-lemma zero_le_mul [ordered_semiring α] {a b : α} : 0 ≤ a → 0 ≤ b → 0 ≤ a * b :=
+-- `mul_nonneg` and `mul_pos` in core are stated in terms of `≥` and `>`, so we restate them here
+-- for use in syntactic tactics (e.g. `simp` and `rw`).
+lemma mul_nonneg' [ordered_semiring α] {a b : α} : 0 ≤ a → 0 ≤ b → 0 ≤ a * b :=
 mul_nonneg
 
+lemma mul_pos' [ordered_semiring α] {a b : α} (ha : 0 < a) (hb : 0 < b) : 0 < a * b :=
+mul_pos ha hb
+
 section linear_ordered_semiring
 variable [linear_ordered_semiring α]
 
@@ -36,30 +40,30 @@ lemma mul_lt_mul'' {a b c d : α} (h1 : a < c) (h2 : b < d) (h3 : 0 ≤ a) (h4 :
   (λ b0, by rw [← b0, mul_zero]; exact
     mul_pos (lt_of_le_of_lt h3 h1) (lt_of_le_of_lt h4 h2))
 
-lemma le_mul_iff_one_le_left {a b : α} (hb : b > 0) : b ≤ a * b ↔ 1 ≤ a :=
+lemma le_mul_iff_one_le_left {a b : α} (hb : 0 < b) : b ≤ a * b ↔ 1 ≤ a :=
 suffices 1 * b ≤ a * b ↔ 1 ≤ a, by rwa one_mul at this,
 mul_le_mul_right hb
 
-lemma lt_mul_iff_one_lt_left {a b : α} (hb : b > 0) : b < a * b ↔ 1 < a :=
+lemma lt_mul_iff_one_lt_left {a b : α} (hb : 0 < b) : b < a * b ↔ 1 < a :=
 suffices 1 * b < a * b ↔ 1 < a, by rwa one_mul at this,
 mul_lt_mul_right hb
 
-lemma le_mul_iff_one_le_right {a b : α} (hb : b > 0) : b ≤ b * a ↔ 1 ≤ a :=
+lemma le_mul_iff_one_le_right {a b : α} (hb : 0 < b) : b ≤ b * a ↔ 1 ≤ a :=
 suffices b * 1 ≤ b * a ↔ 1 ≤ a, by rwa mul_one at this,
 mul_le_mul_left hb
 
-lemma lt_mul_iff_one_lt_right {a b : α} (hb : b > 0) : b < b * a ↔ 1 < a :=
+lemma lt_mul_iff_one_lt_right {a b : α} (hb : 0 < b) : b < b * a ↔ 1 < a :=
 suffices b * 1 < b * a ↔ 1 < a, by rwa mul_one at this,
 mul_lt_mul_left hb
 
-lemma lt_mul_of_gt_one_right' {a b : α} (hb : b > 0) : a > 1 → b < b * a :=
+lemma lt_mul_of_one_lt_right' {a b : α} (hb : 0 < b) : 1 < a → b < b * a :=
 (lt_mul_iff_one_lt_right hb).2
 
-lemma le_mul_of_ge_one_right' {a b : α} (hb : b ≥ 0) (h : a ≥ 1) : b ≤ b * a :=
+lemma le_mul_of_one_le_right' {a b : α} (hb : 0 ≤ b) (h : 1 ≤ a) : b ≤ b * a :=
 suffices b * 1 ≤ b * a, by rwa mul_one at this,
 mul_le_mul_of_nonneg_left h hb
 
-lemma le_mul_of_ge_one_left' {a b : α} (hb : b ≥ 0) (h : a ≥ 1) : b ≤ a * b :=
+lemma le_mul_of_one_le_left' {a b : α} (hb : 0 ≤ b) (h : 1 ≤ a) : b ≤ a * b :=
 suffices 1 * b ≤ a * b, by rwa one_mul at this,
 mul_le_mul_of_nonneg_right h hb
 
@@ -109,19 +113,19 @@ lemma mul_lt_one_of_nonneg_of_lt_one_right {a b : α}
 calc a * b ≤ b : mul_le_of_le_one_left hb0 ha
 ... < 1 : hb
 
-lemma mul_le_iff_le_one_left {a b : α} (hb : b > 0) : a * b ≤ b ↔ a ≤ 1 :=
+lemma mul_le_iff_le_one_left {a b : α} (hb : 0 < b) : a * b ≤ b ↔ a ≤ 1 :=
 ⟨ λ h, le_of_not_lt (mt (lt_mul_iff_one_lt_left hb).2 (not_lt_of_ge h)),
   λ h, le_of_not_lt (mt (lt_mul_iff_one_lt_left hb).1 (not_lt_of_ge h)) ⟩
 
-lemma mul_lt_iff_lt_one_left {a b : α} (hb : b > 0) : a * b < b ↔ a < 1 :=
+lemma mul_lt_iff_lt_one_left {a b : α} (hb : 0 < b) : a * b < b ↔ a < 1 :=
 ⟨ λ h, lt_of_not_ge (mt (le_mul_iff_one_le_left hb).2 (not_le_of_gt h)),
   λ h, lt_of_not_ge (mt (le_mul_iff_one_le_left hb).1 (not_le_of_gt h)) ⟩
 
-lemma mul_le_iff_le_one_right {a b : α} (hb : b > 0) : b * a ≤ b ↔ a ≤ 1 :=
+lemma mul_le_iff_le_one_right {a b : α} (hb : 0 < b) : b * a ≤ b ↔ a ≤ 1 :=
 ⟨ λ h, le_of_not_lt (mt (lt_mul_iff_one_lt_right hb).2 (not_lt_of_ge h)),
   λ h, le_of_not_lt (mt (lt_mul_iff_one_lt_right hb).1 (not_lt_of_ge h)) ⟩
 
-lemma mul_lt_iff_lt_one_right {a b : α} (hb : b > 0) : b * a < b ↔ a < 1 :=
+lemma mul_lt_iff_lt_one_right {a b : α} (hb : 0 < b) : b * a < b ↔ a < 1 :=
 ⟨ λ h, lt_of_not_ge (mt (le_mul_iff_one_le_right hb).2 (not_le_of_gt h)),
   λ h, lt_of_not_ge (mt (le_mul_iff_one_le_right hb).1 (not_le_of_gt h)) ⟩
 

src/analysis/convex.lean

@@ -474,7 +474,7 @@ begin
         { rw finset.mul_sum.symm,
           exact division_ring.inv_mul_cancel h_cases },
         { intros i hi,
-          exact zero_le_mul (inv_nonneg.2 h_sum_nonneg) (ha i (finset.mem_insert_of_mem hi))},
+          exact mul_nonneg (inv_nonneg.2 h_sum_nonneg) (ha i (finset.mem_insert_of_mem hi))},
         { intros i hi,
           exact hz i (finset.mem_insert_of_mem hi) } },
       have h_sum_in_A: a k • z k
@@ -621,7 +621,7 @@ begin
                   ≤ s.sum (λ (i : γ), ((s.sum a)⁻¹ * a i) • f (z i)),
     { apply ih _ hf,
       { intros i hi,
-        exact zero_le_mul (inv_nonneg.2 h_sum_nonneg) (ha i (finset.mem_insert_of_mem hi))},
+        exact mul_nonneg (inv_nonneg.2 h_sum_nonneg) (ha i (finset.mem_insert_of_mem hi))},
       { intros i hi,
         exact hz i (finset.mem_insert_of_mem hi) },
       { rw finset.mul_sum.symm,
@@ -631,7 +631,7 @@ begin
       { rw finset.mul_sum.symm,
         exact division_ring.inv_mul_cancel h_cases },
       { intros i hi,
-        exact zero_le_mul (inv_nonneg.2 h_sum_nonneg) (ha i (finset.mem_insert_of_mem hi))},
+        exact mul_nonneg (inv_nonneg.2 h_sum_nonneg) (ha i (finset.mem_insert_of_mem hi))},
       { intros i hi,
         exact hz i (finset.mem_insert_of_mem hi) } },
     have hf': f (a k • z k     + s.sum a •    s.sum (λ (i : γ), ((finset.sum s a)⁻¹ * a i) • z i))