From c15e46e9bd6a62f3d9187d1b433ceefd9bea4749 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Tue, 24 Sep 2024 07:14:52 +0000 Subject: [PATCH] chore(Monoid/Unbundled/Pow): cleanup (#17013) --- .../Algebra/Order/Monoid/Unbundled/Pow.lean | 156 +++++++++--------- 1 file changed, 75 insertions(+), 81 deletions(-) diff --git a/Mathlib/Algebra/Order/Monoid/Unbundled/Pow.lean b/Mathlib/Algebra/Order/Monoid/Unbundled/Pow.lean index 877d5f5f47c07..11972efe4bd7d 100644 --- a/Mathlib/Algebra/Order/Monoid/Unbundled/Pow.lean +++ b/Mathlib/Algebra/Order/Monoid/Unbundled/Pow.lean @@ -24,96 +24,100 @@ section Preorder variable [Preorder M] -section Left +namespace Left -variable [CovariantClass M M (· * ·) (· ≤ ·)] {x : M} +variable [CovariantClass M M (· * ·) (· ≤ ·)] {a b : M} -@[to_additive (attr := mono, gcongr) nsmul_le_nsmul_right] -theorem pow_le_pow_left' [CovariantClass M M (swap (· * ·)) (· ≤ ·)] {a b : M} (hab : a ≤ b) : - ∀ i : ℕ, a ^ i ≤ b ^ i - | 0 => by simp - | k + 1 => by - rw [pow_succ, pow_succ] - exact mul_le_mul' (pow_le_pow_left' hab k) hab - -@[to_additive nsmul_nonneg] -theorem one_le_pow_of_one_le' {a : M} (H : 1 ≤ a) : ∀ n : ℕ, 1 ≤ a ^ n +@[to_additive Left.nsmul_nonneg] +theorem one_le_pow_of_le (ha : 1 ≤ a) : ∀ n : ℕ, 1 ≤ a ^ n | 0 => by simp | k + 1 => by rw [pow_succ] - exact one_le_mul (one_le_pow_of_one_le' H k) H + exact one_le_mul (one_le_pow_of_le ha k) ha + +@[deprecated (since := "2024-09-21")] alias pow_nonneg := nsmul_nonneg @[to_additive nsmul_nonpos] -theorem pow_le_one' {a : M} (H : a ≤ 1) (n : ℕ) : a ^ n ≤ 1 := - one_le_pow_of_one_le' (M := Mᵒᵈ) H n +theorem pow_le_one_of_le (ha : a ≤ 1) (n : ℕ) : a ^ n ≤ 1 := one_le_pow_of_le (M := Mᵒᵈ) ha n + +@[deprecated (since := "2024-09-21")] alias pow_nonpos := nsmul_nonpos + +@[to_additive nsmul_neg] +theorem pow_lt_one_of_lt {a : M} {n : ℕ} (h : a < 1) (hn : n ≠ 0) : a ^ n < 1 := by + rcases Nat.exists_eq_succ_of_ne_zero hn with ⟨k, rfl⟩ + rw [pow_succ'] + exact mul_lt_one_of_lt_of_le h (pow_le_one_of_le h.le _) + +@[deprecated (since := "2024-09-21")] alias pow_neg := nsmul_neg + +end Left + +@[to_additive nsmul_nonneg] alias one_le_pow_of_one_le' := Left.one_le_pow_of_le +@[to_additive nsmul_nonpos] alias pow_le_one' := Left.pow_le_one_of_le +@[to_additive nsmul_neg] alias pow_lt_one' := Left.pow_lt_one_of_lt + +section Left + +variable [CovariantClass M M (· * ·) (· ≤ ·)] {x : M} + +@[to_additive nsmul_left_monotone] +theorem pow_right_monotone {a : M} (ha : 1 ≤ a) : Monotone fun n : ℕ ↦ a ^ n := + monotone_nat_of_le_succ fun n ↦ by rw [pow_succ]; exact le_mul_of_one_le_right' ha @[to_additive (attr := gcongr) nsmul_le_nsmul_left] theorem pow_le_pow_right' {a : M} {n m : ℕ} (ha : 1 ≤ a) (h : n ≤ m) : a ^ n ≤ a ^ m := - let ⟨k, hk⟩ := Nat.le.dest h - calc - a ^ n ≤ a ^ n * a ^ k := le_mul_of_one_le_right' (one_le_pow_of_one_le' ha _) - _ = a ^ m := by rw [← hk, pow_add] + pow_right_monotone ha h @[to_additive nsmul_le_nsmul_left_of_nonpos] theorem pow_le_pow_right_of_le_one' {a : M} {n m : ℕ} (ha : a ≤ 1) (h : n ≤ m) : a ^ m ≤ a ^ n := pow_le_pow_right' (M := Mᵒᵈ) ha h @[to_additive nsmul_pos] -theorem one_lt_pow' {a : M} (ha : 1 < a) {k : ℕ} (hk : k ≠ 0) : 1 < a ^ k := by - rcases Nat.exists_eq_succ_of_ne_zero hk with ⟨l, rfl⟩ - clear hk - induction l with - | zero => rw [pow_succ]; simpa using ha - | succ l IH => rw [pow_succ]; exact one_lt_mul'' IH ha +theorem one_lt_pow' {a : M} (ha : 1 < a) {k : ℕ} (hk : k ≠ 0) : 1 < a ^ k := + pow_lt_one' (M := Mᵒᵈ) ha hk -@[to_additive nsmul_neg] -theorem pow_lt_one' {a : M} (ha : a < 1) {k : ℕ} (hk : k ≠ 0) : a ^ k < 1 := - one_lt_pow' (M := Mᵒᵈ) ha hk +end Left -@[to_additive (attr := gcongr) nsmul_lt_nsmul_left] -theorem pow_lt_pow_right' [CovariantClass M M (· * ·) (· < ·)] {a : M} {n m : ℕ} (ha : 1 < a) - (h : n < m) : a ^ n < a ^ m := by - rcases Nat.le.dest h with ⟨k, rfl⟩; clear h - rw [pow_add, pow_succ, mul_assoc, ← pow_succ'] - exact lt_mul_of_one_lt_right' _ (one_lt_pow' ha k.succ_ne_zero) +section LeftLt -@[to_additive nsmul_left_strictMono] -theorem pow_right_strictMono' [CovariantClass M M (· * ·) (· < ·)] {a : M} (ha : 1 < a) : - StrictMono ((a ^ ·) : ℕ → M) := fun _ _ => pow_lt_pow_right' ha +variable [CovariantClass M M (· * ·) (· < ·)] {a : M} {n m : ℕ} -@[to_additive Left.pow_nonneg] -theorem Left.one_le_pow_of_le (hx : 1 ≤ x) : ∀ {n : ℕ}, 1 ≤ x ^ n - | 0 => (pow_zero x).ge - | n + 1 => by - rw [pow_succ] - exact Left.one_le_mul (Left.one_le_pow_of_le hx) hx +@[to_additive nsmul_left_strictMono] +theorem pow_right_strictMono' (ha : 1 < a) : StrictMono ((a ^ ·) : ℕ → M) := + strictMono_nat_of_lt_succ fun n ↦ by rw [pow_succ]; exact lt_mul_of_one_lt_right' (a ^ n) ha -@[to_additive Left.pow_nonpos] -theorem Left.pow_le_one_of_le (hx : x ≤ 1) : ∀ {n : ℕ}, x ^ n ≤ 1 - | 0 => (pow_zero _).le - | n + 1 => by - rw [pow_succ] - exact Left.mul_le_one (Left.pow_le_one_of_le hx) hx +@[to_additive (attr := gcongr) nsmul_lt_nsmul_left] +theorem pow_lt_pow_right' (ha : 1 < a) (h : n < m) : a ^ n < a ^ m := + pow_right_strictMono' ha h -end Left +end LeftLt section Right variable [CovariantClass M M (swap (· * ·)) (· ≤ ·)] {x : M} -@[to_additive Right.pow_nonneg] +@[to_additive Right.nsmul_nonneg] theorem Right.one_le_pow_of_le (hx : 1 ≤ x) : ∀ {n : ℕ}, 1 ≤ x ^ n | 0 => (pow_zero _).ge | n + 1 => by rw [pow_succ] exact Right.one_le_mul (Right.one_le_pow_of_le hx) hx -@[to_additive Right.pow_nonpos] -theorem Right.pow_le_one_of_le (hx : x ≤ 1) : ∀ {n : ℕ}, x ^ n ≤ 1 - | 0 => (pow_zero _).le - | n + 1 => by - rw [pow_succ] - exact Right.mul_le_one (Right.pow_le_one_of_le hx) hx +@[deprecated (since := "2024-09-21")] alias Right.pow_nonneg := Right.nsmul_nonneg + +@[to_additive Right.nsmul_nonpos] +theorem Right.pow_le_one_of_le (hx : x ≤ 1) {n : ℕ} : x ^ n ≤ 1 := + Right.one_le_pow_of_le (M := Mᵒᵈ) hx + +@[deprecated (since := "2024-09-21")] alias Right.pow_nonpos := Right.nsmul_nonpos + +@[to_additive Right.nsmul_neg] +theorem Right.pow_lt_one_of_lt {n : ℕ} {x : M} (hn : 0 < n) (h : x < 1) : x ^ n < 1 := by + rcases Nat.exists_eq_succ_of_ne_zero hn.ne' with ⟨k, rfl⟩ + rw [pow_succ] + exact mul_lt_one_of_le_of_lt (pow_le_one_of_le h.le) h + +@[deprecated (since := "2024-09-21")] alias Right.pow_neg := Right.nsmul_neg end Right @@ -144,6 +148,13 @@ section CovariantLESwap variable [Preorder β] [CovariantClass M M (· * ·) (· ≤ ·)] [CovariantClass M M (swap (· * ·)) (· ≤ ·)] +@[to_additive (attr := mono, gcongr) nsmul_le_nsmul_right] +theorem pow_le_pow_left' {a b : M} (hab : a ≤ b) : ∀ i : ℕ, a ^ i ≤ b ^ i + | 0 => by simp + | k + 1 => by + rw [pow_succ, pow_succ] + exact mul_le_mul' (pow_le_pow_left' hab k) hab + @[to_additive Monotone.const_nsmul] theorem Monotone.pow_const {f : β → M} (hf : Monotone f) : ∀ n : ℕ, Monotone fun a => f a ^ n | 0 => by simpa using monotone_const @@ -156,24 +167,6 @@ theorem pow_left_mono (n : ℕ) : Monotone fun a : M => a ^ n := monotone_id.pow end CovariantLESwap -@[to_additive Left.pow_neg] -theorem Left.pow_lt_one_of_lt [CovariantClass M M (· * ·) (· < ·)] {n : ℕ} {x : M} (hn : 0 < n) - (h : x < 1) : x ^ n < 1 := - Nat.le_induction ((pow_one _).trans_lt h) - (fun n _ ih => by - rw [pow_succ] - exact mul_lt_one ih h) - _ (Nat.succ_le_iff.2 hn) - -@[to_additive Right.pow_neg] -theorem Right.pow_lt_one_of_lt [CovariantClass M M (swap (· * ·)) (· < ·)] {n : ℕ} {x : M} - (hn : 0 < n) (h : x < 1) : x ^ n < 1 := - Nat.le_induction ((pow_one _).trans_lt h) - (fun n _ ih => by - rw [pow_succ] - exact Right.mul_lt_one ih h) - _ (Nat.succ_le_iff.2 hn) - end Preorder section LinearOrder @@ -206,6 +199,10 @@ theorem pow_eq_one_iff {x : M} {n : ℕ} (hn : n ≠ 0) : x ^ n = 1 ↔ x = 1 := simp only [le_antisymm_iff] rw [pow_le_one_iff hn, one_le_pow_iff hn] +end CovariantLE + +section CovariantLT + variable [CovariantClass M M (· * ·) (· < ·)] {a : M} {m n : ℕ} @[to_additive nsmul_le_nsmul_iff_left] @@ -216,7 +213,7 @@ theorem pow_le_pow_iff_right' (ha : 1 < a) : a ^ m ≤ a ^ n ↔ m ≤ n := theorem pow_lt_pow_iff_right' (ha : 1 < a) : a ^ m < a ^ n ↔ m < n := (pow_right_strictMono' ha).lt_iff_lt -end CovariantLE +end CovariantLT section CovariantLESwap @@ -266,11 +263,8 @@ theorem Left.pow_lt_one_iff [CovariantClass M M (· * ·) (· < ·)] {n : ℕ} { @[to_additive] theorem Right.pow_lt_one_iff [CovariantClass M M (swap (· * ·)) (· < ·)] {n : ℕ} {x : M} (hn : 0 < n) : x ^ n < 1 ↔ x < 1 := - ⟨fun H => - not_le.mp fun k => - haveI := covariantClass_le_of_lt M M (swap (· * ·)) - H.not_le <| Right.one_le_pow_of_le k, - Right.pow_lt_one_of_lt hn⟩ + haveI := covariantClass_le_of_lt M M (swap (· * ·)) + ⟨fun H => not_le.mp fun k => H.not_le <| Right.one_le_pow_of_le k, Right.pow_lt_one_of_lt hn⟩ end LinearOrder