From 5e305ca9ad2491cec6431f7c4a374926fe302897 Mon Sep 17 00:00:00 2001 From: Siddhartha Gadgil Date: Thu, 15 Dec 2022 15:52:54 +0530 Subject: [PATCH 1/7] all but one error fixed --- Mathlib/Algebra/GroupPower/Order.lean | 681 ++++++++++++++++++++++++++ 1 file changed, 681 insertions(+) create mode 100644 Mathlib/Algebra/GroupPower/Order.lean diff --git a/Mathlib/Algebra/GroupPower/Order.lean b/Mathlib/Algebra/GroupPower/Order.lean new file mode 100644 index 0000000000000..df9c6e239da68 --- /dev/null +++ b/Mathlib/Algebra/GroupPower/Order.lean @@ -0,0 +1,681 @@ +/- +Copyright (c) 2015 Jeremy Avigad. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jeremy Avigad, Robert Y. Lewis +-/ +import Mathlib.Algebra.Order.Ring.Abs +import Mathlib.Algebra.Order.WithZero +import Mathlib.Algebra.GroupPower.Ring +import Mathlib.Data.Set.Intervals.Basic + +/-! +# Lemmas about the interaction of power operations with order + +Note that some lemmas are in `algebra/group_power/lemmas.lean` as they import files which +depend on this file. +-/ + + +open Function + +variable {A G M R : Type _} + +section Monoid + +variable [Monoid M] + +section Preorder + +variable [Preorder M] + +section Left + +variable [CovariantClass M M (· * ·) (· ≤ ·)] {x : M} + +-- `mono` attribute +@[to_additive nsmul_le_nsmul_of_le_right] +theorem pow_le_pow_of_le_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' hab (pow_le_pow_of_le_left' hab k) +#align pow_le_pow_of_le_left' pow_le_pow_of_le_left' + +-- attribute [mono] nsmul_le_nsmul_of_le_right + +@[to_additive nsmul_nonneg] +theorem one_le_pow_of_one_le' {a : M} (H : 1 ≤ a) : ∀ n : ℕ, 1 ≤ a ^ n + | 0 => by simp + | k + 1 => by + rw [pow_succ] + exact one_le_mul H (one_le_pow_of_one_le' H k) +#align one_le_pow_of_one_le' one_le_pow_of_one_le' + +@[to_additive nsmul_nonpos] +theorem pow_le_one' {a : M} (H : a ≤ 1) (n : ℕ) : a ^ n ≤ 1 := + @one_le_pow_of_one_le' Mᵒᵈ _ _ _ _ H n +#align pow_le_one' pow_le_one' + +@[to_additive nsmul_le_nsmul] +theorem pow_le_pow' {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] + +#align pow_le_pow' pow_le_pow' + +@[to_additive nsmul_le_nsmul_of_nonpos] +theorem pow_le_pow_of_le_one' {a : M} {n m : ℕ} (ha : a ≤ 1) (h : n ≤ m) : a ^ m ≤ a ^ n := + @pow_le_pow' Mᵒᵈ _ _ _ _ _ _ ha h +#align pow_le_pow_of_le_one' pow_le_pow_of_le_one' + +@[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 l IH + · rw [pow_succ]; simpa using ha + · rw [pow_succ] + exact one_lt_mul'' ha IH +#align one_lt_pow' one_lt_pow' + +@[to_additive nsmul_neg] +theorem pow_lt_one' {a : M} (ha : a < 1) {k : ℕ} (hk : k ≠ 0) : a ^ k < 1 := + @one_lt_pow' Mᵒᵈ _ _ _ _ ha k hk +#align pow_lt_one' pow_lt_one' + +@[to_additive nsmul_lt_nsmul] +theorem pow_lt_pow' [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) +#align pow_lt_pow' pow_lt_pow' + +@[to_additive nsmul_strict_mono_right] +theorem pow_strict_mono_left [CovariantClass M M (· * ·) (· < ·)] {a : M} (ha : 1 < a) : + StrictMono ((· ^ ·) a : ℕ → M) := fun _ _ => pow_lt_pow' ha +#align pow_strict_mono_left pow_strict_mono_left + +@[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 hx <| Left.one_le_pow_of_le hx +#align left.one_le_pow_of_le Left.one_le_pow_of_le + +@[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 hx <| Left.pow_le_one_of_le hx +#align left.pow_le_one_of_le Left.pow_le_one_of_le + +end Left + +section Right + +variable [CovariantClass M M (swap (· * ·)) (· ≤ ·)] {x : M} + +@[to_additive Right.pow_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 hx <| Right.one_le_pow_of_le hx +#align right.one_le_pow_of_le Right.one_le_pow_of_le + +@[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 hx <| Right.pow_le_one_of_le hx +#align right.pow_le_one_of_le Right.pow_le_one_of_le + +end Right + +@[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 h ih) + _ (Nat.succ_le_iff.2 hn) +#align left.pow_lt_one_of_lt Left.pow_lt_one_of_lt + +@[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 h ih) + _ (Nat.succ_le_iff.2 hn) +#align right.pow_lt_one_of_lt Right.pow_lt_one_of_lt + +end Preorder + +section LinearOrder + +variable [LinearOrder M] + +section CovariantLe + +variable [CovariantClass M M (· * ·) (· ≤ ·)] + +@[to_additive nsmul_nonneg_iff] +theorem one_le_pow_iff {x : M} {n : ℕ} (hn : n ≠ 0) : 1 ≤ x ^ n ↔ 1 ≤ x := + ⟨le_imp_le_of_lt_imp_lt fun h => pow_lt_one' h hn, fun h => one_le_pow_of_one_le' h n⟩ +#align one_le_pow_iff one_le_pow_iff + +@[to_additive] +theorem pow_le_one_iff {x : M} {n : ℕ} (hn : n ≠ 0) : x ^ n ≤ 1 ↔ x ≤ 1 := + @one_le_pow_iff Mᵒᵈ _ _ _ _ _ hn +#align pow_le_one_iff pow_le_one_iff + +@[to_additive nsmul_pos_iff] +theorem one_lt_pow_iff {x : M} {n : ℕ} (hn : n ≠ 0) : 1 < x ^ n ↔ 1 < x := + lt_iff_lt_of_le_iff_le (pow_le_one_iff hn) +#align one_lt_pow_iff one_lt_pow_iff + +@[to_additive] +theorem pow_lt_one_iff {x : M} {n : ℕ} (hn : n ≠ 0) : x ^ n < 1 ↔ x < 1 := + lt_iff_lt_of_le_iff_le (one_le_pow_iff hn) +#align pow_lt_one_iff pow_lt_one_iff + +@[to_additive] +theorem pow_eq_one_iff {x : M} {n : ℕ} (hn : n ≠ 0) : x ^ n = 1 ↔ x = 1 := by + simp only [le_antisymm_iff] + rw [pow_le_one_iff hn, one_le_pow_iff hn] + +#align pow_eq_one_iff pow_eq_one_iff + +variable [CovariantClass M M (· * ·) (· < ·)] {a : M} {m n : ℕ} + +@[to_additive nsmul_le_nsmul_iff] +theorem pow_le_pow_iff' (ha : 1 < a) : a ^ m ≤ a ^ n ↔ m ≤ n := + (pow_strict_mono_left ha).le_iff_le +#align pow_le_pow_iff' pow_le_pow_iff' + +@[to_additive nsmul_lt_nsmul_iff] +theorem pow_lt_pow_iff' (ha : 1 < a) : a ^ m < a ^ n ↔ m < n := + (pow_strict_mono_left ha).lt_iff_lt +#align pow_lt_pow_iff' pow_lt_pow_iff' + +end CovariantLe + +@[to_additive Left.nsmul_neg_iff] +theorem Left.pow_lt_one_iff' [CovariantClass M M (· * ·) (· < ·)] {n : ℕ} {x : M} (hn : 0 < n) : + x ^ n < 1 ↔ x < 1 := + haveI := Mul.to_CovariantClass_left M + pow_lt_one_iff hn.ne' + +theorem Left.pow_lt_one_iff [CovariantClass M M (· * ·) (· < ·)] {n : ℕ} {x : M} (hn : 0 < n) : + x ^ n < 1 ↔ x < 1 := Left.pow_lt_one_iff' hn +#align left.pow_lt_one_iff Left.pow_lt_one_iff + +@[to_additive Right.nsmul_neg_iff] +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 => + H.not_le <| + haveI := Mul.to_CovariantClass_right M + Right.one_le_pow_of_le k, + Right.pow_lt_one_of_lt hn⟩ +#align right.pow_lt_one_iff Right.pow_lt_one_iff + +end LinearOrder + +end Monoid + +section DivInvMonoid + +variable [DivInvMonoid G] [Preorder G] [CovariantClass G G (· * ·) (· ≤ ·)] + +-- porting note: expanded for missing lift +@[to_additive zsmul_nonneg] +theorem one_le_zpow {x : G} (H : 1 ≤ x) {n : ℤ} (hn : 0 ≤ n) : 1 ≤ x ^ n := by + let n' := n.natAbs + let pf : n' = n := Int.natAbs_of_nonneg hn + rw [← pf] + -- lift n to ℕ using hn + rw [zpow_ofNat] + apply one_le_pow_of_one_le' H +#align one_le_zpow one_le_zpow + +end DivInvMonoid + +namespace CanonicallyOrderedCommSemiring + +variable [CanonicallyOrderedCommSemiring R] + +theorem pow_pos {a : R} (H : 0 < a) (n : ℕ) : 0 < a ^ n := + pos_iff_ne_zero.2 <| pow_ne_zero _ H.ne' +#align canonically_ordered_comm_semiring.pow_pos CanonicallyOrderedCommSemiring.pow_pos + +end CanonicallyOrderedCommSemiring + +section OrderedSemiring + +variable [OrderedSemiring R] {a x y : R} {n m : ℕ} + +theorem zero_pow_le_one : ∀ n : ℕ, (0 : R) ^ n ≤ 1 + | 0 => (pow_zero _).le + | n + 1 => by + rw [zero_pow n.succ_pos] + exact zero_le_one +#align zero_pow_le_one zero_pow_le_one + +theorem pow_add_pow_le (hx : 0 ≤ x) (hy : 0 ≤ y) (hn : n ≠ 0) : x ^ n + y ^ n ≤ (x + y) ^ n := by + rcases Nat.exists_eq_succ_of_ne_zero hn with ⟨k, rfl⟩ + induction' k with k ih; + . have eqn : Nat.succ Nat.zero = 1 := rfl + rw [eqn] + simp only [pow_one, le_refl] + . let n := k.succ + have h1 := add_nonneg (mul_nonneg hx (pow_nonneg hy n)) (mul_nonneg hy (pow_nonneg hx n)) + have h2 := add_nonneg hx hy + calc + x ^ n.succ + y ^ n.succ ≤ x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n) := + by + rw [pow_succ _ n, pow_succ _ n] + exact le_add_of_nonneg_right h1 + _ = (x + y) * (x ^ n + y ^ n) := + by + rw [add_mul, mul_add, mul_add, add_comm (y * x ^ n), ← add_assoc, ← add_assoc, + add_assoc (x * x ^ n) (x * y ^ n), add_comm (x * y ^ n) (y * y ^ n), ← add_assoc] + _ ≤ (x + y) ^ n.succ := + by + rw [pow_succ _ n] + exact mul_le_mul_of_nonneg_left (ih (Nat.succ_ne_zero k)) h2 + +#align pow_add_pow_le pow_add_pow_le + +theorem pow_le_one : ∀ (n : ℕ) (_ : 0 ≤ a) (_ : a ≤ 1), a ^ n ≤ 1 + | 0, _, _ => (pow_zero a).le + | n + 1, h₀, h₁ => (pow_succ' a n).le.trans (mul_le_one (pow_le_one n h₀ h₁) h₀ h₁) +#align pow_le_one pow_le_one + +theorem pow_lt_one (h₀ : 0 ≤ a) (h₁ : a < 1) : ∀ {n : ℕ} (_ : n ≠ 0), a ^ n < 1 + | 0, h => (h rfl).elim + | n + 1, _ => by + rw [pow_succ] + exact mul_lt_one_of_nonneg_of_lt_one_left h₀ h₁ (pow_le_one _ h₀ h₁.le) +#align pow_lt_one pow_lt_one + +theorem one_le_pow_of_one_le (H : 1 ≤ a) : ∀ n : ℕ, 1 ≤ a ^ n + | 0 => by rw [pow_zero] + | n + 1 => by + rw [pow_succ] + simpa only [mul_one] using + mul_le_mul H (one_le_pow_of_one_le H n) zero_le_one (le_trans zero_le_one H) +#align one_le_pow_of_one_le one_le_pow_of_one_le + +theorem pow_mono (h : 1 ≤ a) : Monotone fun n : ℕ => a ^ n := + monotone_nat_of_le_succ fun n => by + rw [pow_succ] + exact le_mul_of_one_le_left (pow_nonneg (zero_le_one.trans h) _) h +#align pow_mono pow_mono + +theorem pow_le_pow (ha : 1 ≤ a) (h : n ≤ m) : a ^ n ≤ a ^ m := + pow_mono ha h +#align pow_le_pow pow_le_pow + +theorem le_self_pow (ha : 1 ≤ a) (h : m ≠ 0) : a ≤ a ^ m := + (pow_one a).symm.trans_le (pow_le_pow ha <| pos_iff_ne_zero.mpr h) +#align le_self_pow le_self_pow + +-- @[mono] +theorem pow_le_pow_of_le_left {a b : R} (ha : 0 ≤ a) (hab : a ≤ b) : ∀ i : ℕ, a ^ i ≤ b ^ i := by + intro i + induction i with + | zero => simp + | succ k ih => + rw [pow_succ, pow_succ] + apply mul_le_mul hab + apply ih + apply pow_nonneg ha + apply le_trans ha hab +#align pow_le_pow_of_le_left pow_le_pow_of_le_left + +theorem one_lt_pow (ha : 1 < a) : ∀ {n : ℕ} (hn : n ≠ 0), 1 < a ^ n + | 0, h => (h rfl).elim + | n + 1, h => by + rw [pow_succ] + exact one_lt_mul_of_lt_of_le ha (one_le_pow_of_one_le ha.le _) +#align one_lt_pow one_lt_pow + +end OrderedSemiring + +section StrictOrderedSemiring + +variable [StrictOrderedSemiring R] {a x y : R} {n m : ℕ} + +theorem pow_lt_pow_of_lt_left (h : x < y) (hx : 0 ≤ x) : ∀ {n : ℕ}, 0 < n → x ^ n < y ^ n + | 0, hn => by contradiction + | n + 1, _ => by + simpa only [pow_succ'] using + mul_lt_mul_of_le_of_le' (pow_le_pow_of_le_left hx h.le _) h (pow_pos (hx.trans_lt h) _) hx +#align pow_lt_pow_of_lt_left pow_lt_pow_of_lt_left + +theorem strict_mono_on_pow (hn : 0 < n) : StrictMonoOn (fun x : R => x ^ n) (Set.Ici 0) := + fun _ hx _ _ h => pow_lt_pow_of_lt_left h hx hn +#align strict_mono_on_pow strict_mono_on_pow + +theorem strict_mono_pow (h : 1 < a) : StrictMono fun n : ℕ => a ^ n := + have : 0 < a := zero_le_one.trans_lt h + strictMono_nat_of_lt_succ fun n => by + simpa only [one_mul, pow_succ] using mul_lt_mul h (le_refl (a ^ n)) (pow_pos this _) this.le +#align strict_mono_pow strict_mono_pow + +theorem pow_lt_pow (h : 1 < a) (h2 : n < m) : a ^ n < a ^ m := + strict_mono_pow h h2 +#align pow_lt_pow pow_lt_pow + +theorem pow_lt_pow_iff (h : 1 < a) : a ^ n < a ^ m ↔ n < m := + (strict_mono_pow h).lt_iff_lt +#align pow_lt_pow_iff pow_lt_pow_iff + +theorem pow_le_pow_iff (h : 1 < a) : a ^ n ≤ a ^ m ↔ n ≤ m := + (strict_mono_pow h).le_iff_le +#align pow_le_pow_iff pow_le_pow_iff + +theorem strict_anti_pow (h₀ : 0 < a) (h₁ : a < 1) : StrictAnti fun n : ℕ => a ^ n := + strictAnti_nat_of_succ_lt fun n => by + simpa only [pow_succ, one_mul] using mul_lt_mul h₁ le_rfl (pow_pos h₀ n) zero_le_one +#align strict_anti_pow strict_anti_pow + +theorem pow_lt_pow_iff_of_lt_one (h₀ : 0 < a) (h₁ : a < 1) : a ^ m < a ^ n ↔ n < m := + (strict_anti_pow h₀ h₁).lt_iff_lt +#align pow_lt_pow_iff_of_lt_one pow_lt_pow_iff_of_lt_one + +theorem pow_lt_pow_of_lt_one (h : 0 < a) (ha : a < 1) {i j : ℕ} (hij : i < j) : a ^ j < a ^ i := + (pow_lt_pow_iff_of_lt_one h ha).2 hij +#align pow_lt_pow_of_lt_one pow_lt_pow_of_lt_one + +theorem pow_lt_self_of_lt_one (h₀ : 0 < a) (h₁ : a < 1) (hn : 1 < n) : a ^ n < a := + calc + a ^ n < a ^ 1 := pow_lt_pow_of_lt_one h₀ h₁ hn + _ = a := pow_one _ + +#align pow_lt_self_of_lt_one pow_lt_self_of_lt_one + +theorem sq_pos_of_pos (ha : 0 < a) : 0 < a ^ 2 := by + rw [sq] + exact mul_pos ha ha +#align sq_pos_of_pos sq_pos_of_pos + +end StrictOrderedSemiring + +section StrictOrderedRing + +variable [StrictOrderedRing R] {a : R} + +theorem pow_bit0_pos_of_neg (ha : a < 0) (n : ℕ) : 0 < a ^ bit0 n := by + rw [pow_bit0'] + exact pow_pos (mul_pos_of_neg_of_neg ha ha) _ +#align pow_bit0_pos_of_neg pow_bit0_pos_of_neg + +theorem pow_bit1_neg (ha : a < 0) (n : ℕ) : a ^ bit1 n < 0 := by + rw [bit1, pow_succ] + exact mul_neg_of_neg_of_pos ha (pow_bit0_pos_of_neg ha n) +#align pow_bit1_neg pow_bit1_neg + +theorem sq_pos_of_neg (ha : a < 0) : 0 < a ^ 2 := + pow_bit0_pos_of_neg ha 1 +#align sq_pos_of_neg sq_pos_of_neg + +end StrictOrderedRing + +section LinearOrderedSemiring + +variable [LinearOrderedSemiring R] {a b : R} + +theorem pow_le_one_iff_of_nonneg {a : R} (ha : 0 ≤ a) {n : ℕ} (hn : n ≠ 0) : a ^ n ≤ 1 ↔ a ≤ 1 := by + refine' ⟨_, pow_le_one n ha⟩ + rw [← not_lt, ← not_lt] + exact mt fun h => one_lt_pow h hn +#align pow_le_one_iff_of_nonneg pow_le_one_iff_of_nonneg + +theorem one_le_pow_iff_of_nonneg {a : R} (ha : 0 ≤ a) {n : ℕ} (hn : n ≠ 0) : 1 ≤ a ^ n ↔ 1 ≤ a := by + refine' ⟨_, fun h => one_le_pow_of_one_le h n⟩ + rw [← not_lt, ← not_lt] + exact mt fun h => pow_lt_one ha h hn +#align one_le_pow_iff_of_nonneg one_le_pow_iff_of_nonneg + +theorem one_lt_pow_iff_of_nonneg {a : R} (ha : 0 ≤ a) {n : ℕ} (hn : n ≠ 0) : 1 < a ^ n ↔ 1 < a := + lt_iff_lt_of_le_iff_le (pow_le_one_iff_of_nonneg ha hn) +#align one_lt_pow_iff_of_nonneg one_lt_pow_iff_of_nonneg + +theorem pow_lt_one_iff_of_nonneg {a : R} (ha : 0 ≤ a) {n : ℕ} (hn : n ≠ 0) : a ^ n < 1 ↔ a < 1 := + lt_iff_lt_of_le_iff_le (one_le_pow_iff_of_nonneg ha hn) +#align pow_lt_one_iff_of_nonneg pow_lt_one_iff_of_nonneg + +theorem sq_le_one_iff {a : R} (ha : 0 ≤ a) : a ^ 2 ≤ 1 ↔ a ≤ 1 := + pow_le_one_iff_of_nonneg ha (Nat.succ_ne_zero _) +#align sq_le_one_iff sq_le_one_iff + +theorem sq_lt_one_iff {a : R} (ha : 0 ≤ a) : a ^ 2 < 1 ↔ a < 1 := + pow_lt_one_iff_of_nonneg ha (Nat.succ_ne_zero _) +#align sq_lt_one_iff sq_lt_one_iff + +theorem one_le_sq_iff {a : R} (ha : 0 ≤ a) : 1 ≤ a ^ 2 ↔ 1 ≤ a := + one_le_pow_iff_of_nonneg ha (Nat.succ_ne_zero _) +#align one_le_sq_iff one_le_sq_iff + +theorem one_lt_sq_iff {a : R} (ha : 0 ≤ a) : 1 < a ^ 2 ↔ 1 < a := + one_lt_pow_iff_of_nonneg ha (Nat.succ_ne_zero _) +#align one_lt_sq_iff one_lt_sq_iff + +@[simp] +theorem pow_left_inj {x y : R} {n : ℕ} (Hxpos : 0 ≤ x) (Hypos : 0 ≤ y) (Hnpos : 0 < n) : + x ^ n = y ^ n ↔ x = y := + (@strict_mono_on_pow R _ _ Hnpos).eq_iff_eq Hxpos Hypos +#align pow_left_inj pow_left_inj + +theorem lt_of_pow_lt_pow {a b : R} (n : ℕ) (hb : 0 ≤ b) (h : a ^ n < b ^ n) : a < b := + lt_of_not_ge fun hn => not_lt_of_ge (pow_le_pow_of_le_left hb hn _) h +#align lt_of_pow_lt_pow lt_of_pow_lt_pow + +theorem le_of_pow_le_pow {a b : R} (n : ℕ) (hb : 0 ≤ b) (hn : 0 < n) (h : a ^ n ≤ b ^ n) : a ≤ b := + le_of_not_lt fun h1 => not_le_of_lt (pow_lt_pow_of_lt_left h1 hb hn) h +#align le_of_pow_le_pow le_of_pow_le_pow + +@[simp] +theorem sq_eq_sq {a b : R} (ha : 0 ≤ a) (hb : 0 ≤ b) : a ^ 2 = b ^ 2 ↔ a = b := + pow_left_inj ha hb (by decide) +#align sq_eq_sq sq_eq_sq + +theorem lt_of_mul_self_lt_mul_self (hb : 0 ≤ b) : a * a < b * b → a < b := by + simp_rw [← sq] + exact lt_of_pow_lt_pow _ hb +#align lt_of_mul_self_lt_mul_self lt_of_mul_self_lt_mul_self + +end LinearOrderedSemiring + +section LinearOrderedRing + +variable [LinearOrderedRing R] + +theorem pow_abs (a : R) (n : ℕ) : |a| ^ n = |a ^ n| := + ((absHom.toMonoidHom : R →* R).map_pow a n).symm +#align pow_abs pow_abs + +theorem abs_neg_one_pow (n : ℕ) : |(-1 : R) ^ n| = 1 := by rw [← pow_abs, abs_neg, abs_one, one_pow] +#align abs_neg_one_pow abs_neg_one_pow + +/- warning: pow_bit0_nonneg -> pow_bit0_nonneg is a dubious translation: +lean 3 declaration is + forall {R : Type.{u_4}} [_inst_1 : LinearOrderedRing.{u_4} R] (a : R) (n : Nat), LE.le.{u_4} R (Preorder.toLE.{u_4} R (PartialOrder.toPreorder.{u_4} R (OrderedAddCommGroup.toPartialOrder.{u_4} R (StrictOrderedRing.toOrderedAddCommGroup.{u_4} R (LinearOrderedRing.toStrictOrderedRing.{u_4} R _inst_1))))) (OfNat.ofNat.{u_4} R 0 (OfNat.mk.{u_4} R 0 (Zero.zero.{u_4} R (MulZeroClass.toHasZero.{u_4} R (NonUnitalNonAssocSemiring.toMulZeroClass.{u_4} R (NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring.{u_4} R (NonAssocRing.toNonUnitalNonAssocRing.{u_4} R (Ring.toNonAssocRing.{u_4} R (StrictOrderedRing.toRing.{u_4} R (LinearOrderedRing.toStrictOrderedRing.{u_4} R _inst_1)))))))))) (HPow.hPow.{u_4, 0, u_4} R Nat R (instHPow.{u_4, 0} R Nat (Monoid.hasPow.{u_4} R (Ring.toMonoid.{u_4} R (StrictOrderedRing.toRing.{u_4} R (LinearOrderedRing.toStrictOrderedRing.{u_4} R _inst_1))))) a (bit0.{0} Nat Nat.hasAdd n)) +but is expected to have type + forall {α : Type.{u_1}} [inst._@.Mathlib.Tactic.Positivity.Basic._hyg.204 : LinearOrderedRing.{u_1} α] (a : α) (n : Nat), LE.le.{u_1} α (Preorder.toLE.{u_1} α (PartialOrder.toPreorder.{u_1} α (StrictOrderedRing.toPartialOrder.{u_1} α (LinearOrderedRing.toStrictOrderedRing.{u_1} α inst._@.Mathlib.Tactic.Positivity.Basic._hyg.204)))) (OfNat.ofNat.{u_1} α 0 (Zero.toOfNat0.{u_1} α (MonoidWithZero.toZero.{u_1} α (Semiring.toMonoidWithZero.{u_1} α (StrictOrderedSemiring.toSemiring.{u_1} α (StrictOrderedRing.toStrictOrderedSemiring.{u_1} α (LinearOrderedRing.toStrictOrderedRing.{u_1} α inst._@.Mathlib.Tactic.Positivity.Basic._hyg.204))))))) (HPow.hPow.{u_1, 0, u_1} α Nat α (instHPow.{u_1, 0} α Nat (Monoid.Pow.{u_1} α (MonoidWithZero.toMonoid.{u_1} α (Semiring.toMonoidWithZero.{u_1} α (StrictOrderedSemiring.toSemiring.{u_1} α (StrictOrderedRing.toStrictOrderedSemiring.{u_1} α (LinearOrderedRing.toStrictOrderedRing.{u_1} α inst._@.Mathlib.Tactic.Positivity.Basic._hyg.204))))))) a (HMul.hMul.{0, 0, 0} Nat Nat Nat (instHMul.{0} Nat instMulNat) (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)) n)) +Case conversion may be inaccurate. Consider using '#align pow_bit0_nonneg pow_bit0_nonnegₓ'. -/ +theorem pow_bit0_nonneg (a : R) (n : ℕ) : 0 ≤ a ^ bit0 n := by + rw [pow_bit0] + exact mul_self_nonneg _ +#align pow_bit0_nonneg pow_bit0_nonneg + +theorem sq_nonneg (a : R) : 0 ≤ a ^ 2 := + pow_bit0_nonneg a 1 +#align sq_nonneg sq_nonneg + +alias sq_nonneg ← pow_two_nonneg + +theorem pow_bit0_pos {a : R} (h : a ≠ 0) (n : ℕ) : 0 < a ^ bit0 n := + (pow_bit0_nonneg a n).lt_of_ne (pow_ne_zero _ h).symm +#align pow_bit0_pos pow_bit0_pos + +theorem sq_pos_of_ne_zero (a : R) (h : a ≠ 0) : 0 < a ^ 2 := + pow_bit0_pos h 1 +#align sq_pos_of_ne_zero sq_pos_of_ne_zero + +alias sq_pos_of_ne_zero ← pow_two_pos_of_ne_zero + +theorem pow_bit0_pos_iff (a : R) {n : ℕ} (hn : n ≠ 0) : 0 < a ^ bit0 n ↔ a ≠ 0 := by + refine' ⟨fun h => _, fun h => pow_bit0_pos h n⟩ + rintro rfl + rw [zero_pow (Nat.zero_lt_bit0 hn)] at h + exact lt_irrefl _ h +#align pow_bit0_pos_iff pow_bit0_pos_iff + +theorem sq_pos_iff (a : R) : 0 < a ^ 2 ↔ a ≠ 0 := + pow_bit0_pos_iff a one_ne_zero +#align sq_pos_iff sq_pos_iff + +variable {x y : R} + +theorem sq_abs (x : R) : |x| ^ 2 = x ^ 2 := by simpa only [sq] using abs_mul_abs_self x +#align sq_abs sq_abs + +theorem abs_sq (x : R) : |x ^ 2| = x ^ 2 := by simpa only [sq] using abs_mul_self x +#align abs_sq abs_sq + +theorem sq_lt_sq : x ^ 2 < y ^ 2 ↔ |x| < |y| := by + simpa only [sq_abs] using + (@strict_mono_on_pow R _ _ two_pos).lt_iff_lt (abs_nonneg x) (abs_nonneg y) +#align sq_lt_sq sq_lt_sq + +theorem sq_lt_sq' (h1 : -y < x) (h2 : x < y) : x ^ 2 < y ^ 2 := + sq_lt_sq.2 (lt_of_lt_of_le (abs_lt.2 ⟨h1, h2⟩) (le_abs_self _)) +#align sq_lt_sq' sq_lt_sq' + +theorem sq_le_sq : x ^ 2 ≤ y ^ 2 ↔ |x| ≤ |y| := by + simpa only [sq_abs] using + (@strict_mono_on_pow R _ _ two_pos).le_iff_le (abs_nonneg x) (abs_nonneg y) +#align sq_le_sq sq_le_sq + +theorem sq_le_sq' (h1 : -y ≤ x) (h2 : x ≤ y) : x ^ 2 ≤ y ^ 2 := + sq_le_sq.2 (le_trans (abs_le.mpr ⟨h1, h2⟩) (le_abs_self _)) +#align sq_le_sq' sq_le_sq' + +theorem abs_lt_of_sq_lt_sq (h : x ^ 2 < y ^ 2) (hy : 0 ≤ y) : |x| < y := by + rwa [← abs_of_nonneg hy, ← sq_lt_sq] +#align abs_lt_of_sq_lt_sq abs_lt_of_sq_lt_sq + +theorem abs_lt_of_sq_lt_sq' (h : x ^ 2 < y ^ 2) (hy : 0 ≤ y) : -y < x ∧ x < y := + abs_lt.mp <| abs_lt_of_sq_lt_sq h hy +#align abs_lt_of_sq_lt_sq' abs_lt_of_sq_lt_sq' + +theorem abs_le_of_sq_le_sq (h : x ^ 2 ≤ y ^ 2) (hy : 0 ≤ y) : |x| ≤ y := by + rwa [← abs_of_nonneg hy, ← sq_le_sq] +#align abs_le_of_sq_le_sq abs_le_of_sq_le_sq + +theorem abs_le_of_sq_le_sq' (h : x ^ 2 ≤ y ^ 2) (hy : 0 ≤ y) : -y ≤ x ∧ x ≤ y := + abs_le.mp <| abs_le_of_sq_le_sq h hy +#align abs_le_of_sq_le_sq' abs_le_of_sq_le_sq' + +theorem sq_eq_sq_iff_abs_eq_abs (x y : R) : x ^ 2 = y ^ 2 ↔ |x| = |y| := by + simp only [le_antisymm_iff, sq_le_sq] + apply Iff.refl +#align sq_eq_sq_iff_abs_eq_abs sq_eq_sq_iff_abs_eq_abs + +@[simp] +theorem sq_le_one_iff_abs_le_one (x : R) : x ^ 2 ≤ 1 ↔ |x| ≤ 1 := by + simpa only [one_pow, abs_one] using @sq_le_sq _ _ x 1 +#align sq_le_one_iff_abs_le_one sq_le_one_iff_abs_le_one + +@[simp] +theorem sq_lt_one_iff_abs_lt_one (x : R) : x ^ 2 < 1 ↔ |x| < 1 := by + simpa only [one_pow, abs_one] using @sq_lt_sq _ _ x 1 +#align sq_lt_one_iff_abs_lt_one sq_lt_one_iff_abs_lt_one + +@[simp] +theorem one_le_sq_iff_one_le_abs (x : R) : 1 ≤ x ^ 2 ↔ 1 ≤ |x| := by + simpa only [one_pow, abs_one] using @sq_le_sq _ _ 1 x +#align one_le_sq_iff_one_le_abs one_le_sq_iff_one_le_abs + +@[simp] +theorem one_lt_sq_iff_one_lt_abs (x : R) : 1 < x ^ 2 ↔ 1 < |x| := by + simpa only [one_pow, abs_one] using @sq_lt_sq _ _ 1 x +#align one_lt_sq_iff_one_lt_abs one_lt_sq_iff_one_lt_abs + +theorem pow_four_le_pow_two_of_pow_two_le {x y : R} (h : x ^ 2 ≤ y) : x ^ 4 ≤ y ^ 2 := + (pow_mul x 2 2).symm ▸ pow_le_pow_of_le_left (sq_nonneg x) h 2 +#align pow_four_le_pow_two_of_pow_two_le pow_four_le_pow_two_of_pow_two_le + +end LinearOrderedRing + +section LinearOrderedCommRing + +variable [LinearOrderedCommRing R] + +/-- Arithmetic mean-geometric mean (AM-GM) inequality for linearly ordered commutative rings. -/ +theorem two_mul_le_add_sq (a b : R) : 2 * a * b ≤ a ^ 2 + b ^ 2 := + sub_nonneg.mp ((sub_add_eq_add_sub _ _ _).subst ((sub_sq a b).subst (sq_nonneg _))) +#align two_mul_le_add_sq two_mul_le_add_sq + +alias two_mul_le_add_sq ← two_mul_le_add_pow_two + +end LinearOrderedCommRing + +section LinearOrderedCommMonoidWithZero + +variable [LinearOrderedCommMonoidWithZero M] [NoZeroDivisors M] {a : M} {n : ℕ} + +theorem pow_pos_iff (hn : 0 < n) : 0 < a ^ n ↔ 0 < a := by + simp_rw [zero_lt_iff, pow_ne_zero_iff hn] + rw [pow_ne_zero_iff] + assumption +#align pow_pos_iff pow_pos_iff + +end LinearOrderedCommMonoidWithZero + +section LinearOrderedCommGroupWithZero + +variable [LinearOrderedCommGroupWithZero M] {a : M} {m n : ℕ} + +theorem pow_lt_pow_succ (ha : 1 < a) : a ^ n < a ^ n.succ := by + rw [← one_mul (a ^ n), pow_succ] + exact mul_lt_right₀ _ ha (pow_ne_zero _ (zero_lt_one.trans ha).ne') +#align pow_lt_pow_succ pow_lt_pow_succ + +theorem pow_lt_pow₀ (ha : 1 < a) (hmn : m < n) : a ^ m < a ^ n := by + induction' hmn with n _ ih + exacts[pow_lt_pow_succ ha, lt_trans ih (pow_lt_pow_succ ha)] +#align pow_lt_pow₀ pow_lt_pow₀ + +end LinearOrderedCommGroupWithZero + +namespace MonoidHom + +variable [Ring R] [Monoid M] [LinearOrder M] [CovariantClass M M (· * ·) (· ≤ ·)] (f : R →* M) + +theorem map_neg_one : f (-1) = 1 := + (pow_eq_one_iff (Nat.succ_ne_zero 1)).1 <| by rw [← map_pow, neg_one_sq, map_one] +#align monoid_hom.map_neg_one MonoidHom.map_neg_one + +@[simp] +theorem map_neg (x : R) : f (-x) = f x := by rw [← neg_one_mul, map_mul, map_neg_one, one_mul] +#align monoid_hom.map_neg MonoidHom.map_neg + +theorem map_sub_swap (x y : R) : f (x - y) = f (y - x) := by rw [← map_neg, neg_sub] +#align monoid_hom.map_sub_swap MonoidHom.map_sub_swap + +end MonoidHom From 39fa0c6152121f04b12940f7a9f4448a91ae9c13 Mon Sep 17 00:00:00 2001 From: Siddhartha Gadgil Date: Thu, 15 Dec 2022 18:40:16 +0530 Subject: [PATCH 2/7] clean up, de-duplicate --- Mathlib.lean | 1 + Mathlib/Algebra/GroupPower/Order.lean | 18 +++++++------ Mathlib/Init/Data/Nat/Basic.lean | 37 ++++++++++++++++++++++++++- 3 files changed, 47 insertions(+), 9 deletions(-) diff --git a/Mathlib.lean b/Mathlib.lean index 9dbf747efdc3e..0e9c6c8b0dd34 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -26,6 +26,7 @@ import Mathlib.Algebra.Group.WithOne.Units import Mathlib.Algebra.GroupPower.Basic import Mathlib.Algebra.GroupPower.Identities import Mathlib.Algebra.GroupPower.Lemmas +import Mathlib.Algebra.GroupPower.Order import Mathlib.Algebra.GroupPower.Ring import Mathlib.Algebra.GroupWithZero.Basic import Mathlib.Algebra.GroupWithZero.Commute diff --git a/Mathlib/Algebra/GroupPower/Order.lean b/Mathlib/Algebra/GroupPower/Order.lean index df9c6e239da68..c46b5961505ce 100644 --- a/Mathlib/Algebra/GroupPower/Order.lean +++ b/Mathlib/Algebra/GroupPower/Order.lean @@ -7,6 +7,9 @@ import Mathlib.Algebra.Order.Ring.Abs import Mathlib.Algebra.Order.WithZero import Mathlib.Algebra.GroupPower.Ring import Mathlib.Data.Set.Intervals.Basic +import Mathlib.Data.Nat.Basic +import Mathlib.Tactic.Positivity.Basic +import Mathlib.Tactic.Linarith.Lemmas /-! # Lemmas about the interaction of power operations with order @@ -16,6 +19,8 @@ depend on this file. -/ +set_option linter.deprecated false + open Function variable {A G M R : Type _} @@ -345,9 +350,9 @@ theorem pow_le_pow_of_le_left {a b : R} (ha : 0 ≤ a) (hab : a ≤ b) : ∀ i : apply le_trans ha hab #align pow_le_pow_of_le_left pow_le_pow_of_le_left -theorem one_lt_pow (ha : 1 < a) : ∀ {n : ℕ} (hn : n ≠ 0), 1 < a ^ n +theorem one_lt_pow (ha : 1 < a) : ∀ {n : ℕ} (_ : n ≠ 0), 1 < a ^ n | 0, h => (h rfl).elim - | n + 1, h => by + | n + 1, _ => by rw [pow_succ] exact one_lt_mul_of_lt_of_le ha (one_le_pow_of_one_le ha.le _) #align one_lt_pow one_lt_pow @@ -517,19 +522,16 @@ lean 3 declaration is but is expected to have type forall {α : Type.{u_1}} [inst._@.Mathlib.Tactic.Positivity.Basic._hyg.204 : LinearOrderedRing.{u_1} α] (a : α) (n : Nat), LE.le.{u_1} α (Preorder.toLE.{u_1} α (PartialOrder.toPreorder.{u_1} α (StrictOrderedRing.toPartialOrder.{u_1} α (LinearOrderedRing.toStrictOrderedRing.{u_1} α inst._@.Mathlib.Tactic.Positivity.Basic._hyg.204)))) (OfNat.ofNat.{u_1} α 0 (Zero.toOfNat0.{u_1} α (MonoidWithZero.toZero.{u_1} α (Semiring.toMonoidWithZero.{u_1} α (StrictOrderedSemiring.toSemiring.{u_1} α (StrictOrderedRing.toStrictOrderedSemiring.{u_1} α (LinearOrderedRing.toStrictOrderedRing.{u_1} α inst._@.Mathlib.Tactic.Positivity.Basic._hyg.204))))))) (HPow.hPow.{u_1, 0, u_1} α Nat α (instHPow.{u_1, 0} α Nat (Monoid.Pow.{u_1} α (MonoidWithZero.toMonoid.{u_1} α (Semiring.toMonoidWithZero.{u_1} α (StrictOrderedSemiring.toSemiring.{u_1} α (StrictOrderedRing.toStrictOrderedSemiring.{u_1} α (LinearOrderedRing.toStrictOrderedRing.{u_1} α inst._@.Mathlib.Tactic.Positivity.Basic._hyg.204))))))) a (HMul.hMul.{0, 0, 0} Nat Nat Nat (instHMul.{0} Nat instMulNat) (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)) n)) Case conversion may be inaccurate. Consider using '#align pow_bit0_nonneg pow_bit0_nonnegₓ'. -/ -theorem pow_bit0_nonneg (a : R) (n : ℕ) : 0 ≤ a ^ bit0 n := by +-- Porting note: renamed to avoid collision with Mathlib.Tactic.Positivity.Basic +theorem pow_bit0_nonneg' (a : R) (n : ℕ) : 0 ≤ a ^ bit0 n := by rw [pow_bit0] exact mul_self_nonneg _ #align pow_bit0_nonneg pow_bit0_nonneg -theorem sq_nonneg (a : R) : 0 ≤ a ^ 2 := - pow_bit0_nonneg a 1 -#align sq_nonneg sq_nonneg - alias sq_nonneg ← pow_two_nonneg theorem pow_bit0_pos {a : R} (h : a ≠ 0) (n : ℕ) : 0 < a ^ bit0 n := - (pow_bit0_nonneg a n).lt_of_ne (pow_ne_zero _ h).symm + (pow_bit0_nonneg' a n).lt_of_ne (pow_ne_zero _ h).symm #align pow_bit0_pos pow_bit0_pos theorem sq_pos_of_ne_zero (a : R) (h : a ≠ 0) : 0 < a ^ 2 := diff --git a/Mathlib/Init/Data/Nat/Basic.lean b/Mathlib/Init/Data/Nat/Basic.lean index 8005d50fb8310..f412224c073c9 100644 --- a/Mathlib/Init/Data/Nat/Basic.lean +++ b/Mathlib/Init/Data/Nat/Basic.lean @@ -3,5 +3,40 @@ Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Floris van Doorn, Leonardo de Moura -/ - +import Mathlib.Init.ZeroOne notation "ℕ" => Nat + +namespace Nat + +set_option linter.deprecated false + +protected theorem bit0_succ_eq (n : ℕ) : bit0 (succ n) = succ (succ (bit0 n)) := + show succ (succ n + n) = succ (succ (n + n)) from congrArg succ (succ_add n n) +#align nat.bit0_succ_eq Nat.bit0_succ_eq + +protected theorem zero_lt_bit0 : ∀ {n : Nat}, n ≠ 0 → 0 < bit0 n + | 0, h => absurd rfl h + | succ n, _ => + calc + 0 < succ (succ (bit0 n)) := zero_lt_succ _ + _ = bit0 (succ n) := (Nat.bit0_succ_eq n).symm + +#align nat.zero_lt_bit0 Nat.zero_lt_bit0 + +protected theorem zero_lt_bit1 (n : Nat) : 0 < bit1 n := + zero_lt_succ _ +#align nat.zero_lt_bit1 Nat.zero_lt_bit1 + +protected theorem bit0_ne_zero : ∀ {n : ℕ}, n ≠ 0 → bit0 n ≠ 0 + | 0, h => absurd rfl h + | n + 1, _ => + suffices n + 1 + (n + 1) ≠ 0 from this + suffices succ (n + 1 + n) ≠ 0 from this + fun h => Nat.noConfusion h +#align nat.bit0_ne_zero Nat.bit0_ne_zero + +protected theorem bit1_ne_zero (n : ℕ) : bit1 n ≠ 0 := + show succ (n + n) ≠ 0 from fun h => Nat.noConfusion h +#align nat.bit1_ne_zero Nat.bit1_ne_zero + +end Nat From 6b2f26e7cb24748cba03f1fbed939f1f254cbcd5 Mon Sep 17 00:00:00 2001 From: Siddhartha Gadgil Date: Thu, 15 Dec 2022 18:45:43 +0530 Subject: [PATCH 3/7] breaking lines --- Mathlib/Algebra/GroupPower/Order.lean | 36 +++++++++++++++++++++++++-- 1 file changed, 34 insertions(+), 2 deletions(-) diff --git a/Mathlib/Algebra/GroupPower/Order.lean b/Mathlib/Algebra/GroupPower/Order.lean index c46b5961505ce..678bb5c49c4cf 100644 --- a/Mathlib/Algebra/GroupPower/Order.lean +++ b/Mathlib/Algebra/GroupPower/Order.lean @@ -518,9 +518,41 @@ theorem abs_neg_one_pow (n : ℕ) : |(-1 : R) ^ n| = 1 := by rw [← pow_abs, ab /- warning: pow_bit0_nonneg -> pow_bit0_nonneg is a dubious translation: lean 3 declaration is - forall {R : Type.{u_4}} [_inst_1 : LinearOrderedRing.{u_4} R] (a : R) (n : Nat), LE.le.{u_4} R (Preorder.toLE.{u_4} R (PartialOrder.toPreorder.{u_4} R (OrderedAddCommGroup.toPartialOrder.{u_4} R (StrictOrderedRing.toOrderedAddCommGroup.{u_4} R (LinearOrderedRing.toStrictOrderedRing.{u_4} R _inst_1))))) (OfNat.ofNat.{u_4} R 0 (OfNat.mk.{u_4} R 0 (Zero.zero.{u_4} R (MulZeroClass.toHasZero.{u_4} R (NonUnitalNonAssocSemiring.toMulZeroClass.{u_4} R (NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring.{u_4} R (NonAssocRing.toNonUnitalNonAssocRing.{u_4} R (Ring.toNonAssocRing.{u_4} R (StrictOrderedRing.toRing.{u_4} R (LinearOrderedRing.toStrictOrderedRing.{u_4} R _inst_1)))))))))) (HPow.hPow.{u_4, 0, u_4} R Nat R (instHPow.{u_4, 0} R Nat (Monoid.hasPow.{u_4} R (Ring.toMonoid.{u_4} R (StrictOrderedRing.toRing.{u_4} R (LinearOrderedRing.toStrictOrderedRing.{u_4} R _inst_1))))) a (bit0.{0} Nat Nat.hasAdd n)) + forall {R : Type.{u_4}} [_inst_1 : LinearOrderedRing.{u_4} R] (a : R) (n : Nat), LE.le.{u_4} R + (Preorder.toLE.{u_4} R + (PartialOrder.toPreorder.{u_4} R (OrderedAddCommGroup.toPartialOrder.{u_4} R + (StrictOrderedRing.toOrderedAddCommGroup.{u_4} R + (LinearOrderedRing.toStrictOrderedRing.{u_4} R _inst_1))))) (OfNat.ofNat.{u_4} R 0 + (OfNat.mk.{u_4} R 0 (Zero.zero.{u_4} R + (MulZeroClass.toHasZero.{u_4} R (NonUnitalNonAssocSemiring.toMulZeroClass.{u_4} R + (NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring.{u_4} R + (NonAssocRing.toNonUnitalNonAssocRing.{u_4} R (Ring.toNonAssocRing.{u_4} R + (StrictOrderedRing.toRing.{u_4} R (LinearOrderedRing.toStrictOrderedRing.{u_4} R _inst_1)))))))))) + (HPow.hPow.{u_4, 0, u_4} R Nat R (instHPow.{u_4, 0} R Nat + (Monoid.hasPow.{u_4} R (Ring.toMonoid.{u_4} R (StrictOrderedRing.toRing.{u_4} R + (LinearOrderedRing.toStrictOrderedRing.{u_4} R _inst_1))))) + a (bit0.{0} Nat Nat.hasAdd n)) but is expected to have type - forall {α : Type.{u_1}} [inst._@.Mathlib.Tactic.Positivity.Basic._hyg.204 : LinearOrderedRing.{u_1} α] (a : α) (n : Nat), LE.le.{u_1} α (Preorder.toLE.{u_1} α (PartialOrder.toPreorder.{u_1} α (StrictOrderedRing.toPartialOrder.{u_1} α (LinearOrderedRing.toStrictOrderedRing.{u_1} α inst._@.Mathlib.Tactic.Positivity.Basic._hyg.204)))) (OfNat.ofNat.{u_1} α 0 (Zero.toOfNat0.{u_1} α (MonoidWithZero.toZero.{u_1} α (Semiring.toMonoidWithZero.{u_1} α (StrictOrderedSemiring.toSemiring.{u_1} α (StrictOrderedRing.toStrictOrderedSemiring.{u_1} α (LinearOrderedRing.toStrictOrderedRing.{u_1} α inst._@.Mathlib.Tactic.Positivity.Basic._hyg.204))))))) (HPow.hPow.{u_1, 0, u_1} α Nat α (instHPow.{u_1, 0} α Nat (Monoid.Pow.{u_1} α (MonoidWithZero.toMonoid.{u_1} α (Semiring.toMonoidWithZero.{u_1} α (StrictOrderedSemiring.toSemiring.{u_1} α (StrictOrderedRing.toStrictOrderedSemiring.{u_1} α (LinearOrderedRing.toStrictOrderedRing.{u_1} α inst._@.Mathlib.Tactic.Positivity.Basic._hyg.204))))))) a (HMul.hMul.{0, 0, 0} Nat Nat Nat (instHMul.{0} Nat instMulNat) (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)) n)) + forall {α : Type.{u_1}} + [inst._@.Mathlib.Tactic.Positivity.Basic._hyg.204 : LinearOrderedRing.{u_1} α] + (a : α) (n : Nat), LE.le.{u_1} α (Preorder.toLE.{u_1} α + (PartialOrder.toPreorder.{u_1} α (StrictOrderedRing.toPartialOrder.{u_1} α + (LinearOrderedRing.toStrictOrderedRing.{u_1} + α inst._@.Mathlib.Tactic.Positivity.Basic._hyg.204)))) + (OfNat.ofNat.{u_1} α 0 (Zero.toOfNat0.{u_1} α + (MonoidWithZero.toZero.{u_1} α (Semiring.toMonoidWithZero.{u_1} α + (StrictOrderedSemiring.toSemiring.{u_1} α (StrictOrderedRing.toStrictOrderedSemiring.{u_1} α + (LinearOrderedRing.toStrictOrderedRing.{u_1} α + inst._@.Mathlib.Tactic.Positivity.Basic._hyg.204))))))) + (HPow.hPow.{u_1, 0, u_1} α Nat α (instHPow.{u_1, 0} α Nat (Monoid.Pow.{u_1} α + (MonoidWithZero.toMonoid.{u_1} α + (Semiring.toMonoidWithZero.{u_1} α (StrictOrderedSemiring.toSemiring.{u_1} α + (StrictOrderedRing.toStrictOrderedSemiring.{u_1} α + (LinearOrderedRing.toStrictOrderedRing.{u_1} α + inst._@.Mathlib.Tactic.Positivity.Basic._hyg.204))))))) a + (HMul.hMul.{0, 0, 0} Nat Nat Nat + (instHMul.{0} Nat instMulNat) + (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)) n)) Case conversion may be inaccurate. Consider using '#align pow_bit0_nonneg pow_bit0_nonnegₓ'. -/ -- Porting note: renamed to avoid collision with Mathlib.Tactic.Positivity.Basic theorem pow_bit0_nonneg' (a : R) (n : ℕ) : 0 ≤ a ^ bit0 n := by From a6660edb7a5891d35e592cd2820bbdc857dfb567 Mon Sep 17 00:00:00 2001 From: Riccardo Brasca Date: Thu, 15 Dec 2022 15:16:15 +0100 Subject: [PATCH 4/7] feat port Data.Nat.Pow --- Mathlib/Data/Nat/Pow.lean | 251 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 251 insertions(+) create mode 100644 Mathlib/Data/Nat/Pow.lean diff --git a/Mathlib/Data/Nat/Pow.lean b/Mathlib/Data/Nat/Pow.lean new file mode 100644 index 0000000000000..e6b0ffbafb1ef --- /dev/null +++ b/Mathlib/Data/Nat/Pow.lean @@ -0,0 +1,251 @@ +/- +Copyright (c) 2014 Floris van Doorn (c) 2016 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Floris van Doorn, Leonardo de Moura, Jeremy Avigad, Mario Carneiro + +! This file was ported from Lean 3 source module data.nat.pow +! leanprover-community/mathlib commit aba57d4d3dae35460225919dcd82fe91355162f9 +! Please do not edit these lines, except to modify the commit id +! if you have ported upstream changes. +-/ +import Mathbin.Algebra.GroupPower.Order + +/-! # `nat.pow` + +Results on the power operation on natural numbers. +-/ + + +namespace Nat + +/-! ### `pow` -/ + + +#print Nat.pow_le_pow_of_le_left /- +-- This is redundant with `pow_le_pow_of_le_left'`, +-- We leave a version in the `nat` namespace as well. +-- (The global `pow_le_pow_of_le_left` needs an extra hypothesis `0 ≤ x`.) +protected theorem pow_le_pow_of_le_left {x y : ℕ} (H : x ≤ y) : ∀ i : ℕ, x ^ i ≤ y ^ i := + pow_le_pow_of_le_left' H +#align nat.pow_le_pow_of_le_left Nat.pow_le_pow_of_le_left +-/ + +#print Nat.pow_le_pow_of_le_right /- +theorem pow_le_pow_of_le_right {x : ℕ} (H : 0 < x) {i j : ℕ} (h : i ≤ j) : x ^ i ≤ x ^ j := + pow_le_pow' H h +#align nat.pow_le_pow_of_le_right Nat.pow_le_pow_of_le_right +-/ + +theorem pow_lt_pow_of_lt_left {x y : ℕ} (H : x < y) {i} (h : 0 < i) : x ^ i < y ^ i := + pow_lt_pow_of_lt_left H (zero_le _) h +#align nat.pow_lt_pow_of_lt_left Nat.pow_lt_pow_of_lt_left + +theorem pow_lt_pow_of_lt_right {x : ℕ} (H : 1 < x) {i j : ℕ} (h : i < j) : x ^ i < x ^ j := + pow_lt_pow H h +#align nat.pow_lt_pow_of_lt_right Nat.pow_lt_pow_of_lt_right + +theorem pow_lt_pow_succ {p : ℕ} (h : 1 < p) (n : ℕ) : p ^ n < p ^ (n + 1) := + pow_lt_pow_of_lt_right h n.lt_succ_self +#align nat.pow_lt_pow_succ Nat.pow_lt_pow_succ + +theorem lt_pow_self {p : ℕ} (h : 1 < p) : ∀ n : ℕ, n < p ^ n + | 0 => by simp [zero_lt_one] + | n + 1 => + calc + n + 1 < p ^ n + 1 := Nat.add_lt_add_right (lt_pow_self _) _ + _ ≤ p ^ (n + 1) := pow_lt_pow_succ h _ + +#align nat.lt_pow_self Nat.lt_pow_self + +theorem lt_two_pow (n : ℕ) : n < 2 ^ n := + lt_pow_self (by decide) n +#align nat.lt_two_pow Nat.lt_two_pow + +theorem one_le_pow (n m : ℕ) (h : 0 < m) : 1 ≤ m ^ n := by + rw [← one_pow n] + exact Nat.pow_le_pow_of_le_left h n +#align nat.one_le_pow Nat.one_le_pow + +theorem one_le_pow' (n m : ℕ) : 1 ≤ (m + 1) ^ n := + one_le_pow n (m + 1) (succ_pos m) +#align nat.one_le_pow' Nat.one_le_pow' + +theorem one_le_two_pow (n : ℕ) : 1 ≤ 2 ^ n := + one_le_pow n 2 (by decide) +#align nat.one_le_two_pow Nat.one_le_two_pow + +theorem one_lt_pow (n m : ℕ) (h₀ : 0 < n) (h₁ : 1 < m) : 1 < m ^ n := by + rw [← one_pow n] + exact pow_lt_pow_of_lt_left h₁ h₀ +#align nat.one_lt_pow Nat.one_lt_pow + +theorem one_lt_pow' (n m : ℕ) : 1 < (m + 2) ^ (n + 1) := + one_lt_pow (n + 1) (m + 2) (succ_pos n) (Nat.lt_of_sub_eq_succ rfl) +#align nat.one_lt_pow' Nat.one_lt_pow' + +@[simp] +theorem one_lt_pow_iff {k n : ℕ} (h : 0 ≠ k) : 1 < n ^ k ↔ 1 < n := by + cases n + · cases k <;> simp [zero_pow_eq] + cases n + · rw [one_pow] + refine' ⟨fun _ => one_lt_succ_succ n, fun _ => _⟩ + induction' k with k hk + · exact absurd rfl h + cases k + · simp + exact one_lt_mul (one_lt_succ_succ _).le (hk (succ_ne_zero k).symm) +#align nat.one_lt_pow_iff Nat.one_lt_pow_iff + +theorem one_lt_two_pow (n : ℕ) (h₀ : 0 < n) : 1 < 2 ^ n := + one_lt_pow n 2 h₀ (by decide) +#align nat.one_lt_two_pow Nat.one_lt_two_pow + +theorem one_lt_two_pow' (n : ℕ) : 1 < 2 ^ (n + 1) := + one_lt_pow (n + 1) 2 (succ_pos n) (by decide) +#align nat.one_lt_two_pow' Nat.one_lt_two_pow' + +theorem pow_right_strict_mono {x : ℕ} (k : 2 ≤ x) : StrictMono fun n : ℕ => x ^ n := fun _ _ => + pow_lt_pow_of_lt_right k +#align nat.pow_right_strict_mono Nat.pow_right_strict_mono + +theorem pow_le_iff_le_right {x m n : ℕ} (k : 2 ≤ x) : x ^ m ≤ x ^ n ↔ m ≤ n := + StrictMono.le_iff_le (pow_right_strict_mono k) +#align nat.pow_le_iff_le_right Nat.pow_le_iff_le_right + +theorem pow_lt_iff_lt_right {x m n : ℕ} (k : 2 ≤ x) : x ^ m < x ^ n ↔ m < n := + StrictMono.lt_iff_lt (pow_right_strict_mono k) +#align nat.pow_lt_iff_lt_right Nat.pow_lt_iff_lt_right + +theorem pow_right_injective {x : ℕ} (k : 2 ≤ x) : Function.Injective fun n : ℕ => x ^ n := + StrictMono.injective (pow_right_strict_mono k) +#align nat.pow_right_injective Nat.pow_right_injective + +theorem pow_left_strict_mono {m : ℕ} (k : 1 ≤ m) : StrictMono fun x : ℕ => x ^ m := fun _ _ h => + pow_lt_pow_of_lt_left h k +#align nat.pow_left_strict_mono Nat.pow_left_strict_mono + +theorem mul_lt_mul_pow_succ {n a q : ℕ} (a0 : 0 < a) (q1 : 1 < q) : n * q < a * q ^ (n + 1) := by + rw [pow_succ', ← mul_assoc, mul_lt_mul_right (zero_lt_one.trans q1)] + exact lt_mul_of_one_le_of_lt (nat.succ_le_iff.mpr a0) (Nat.lt_pow_self q1 n) +#align nat.mul_lt_mul_pow_succ Nat.mul_lt_mul_pow_succ + +end Nat + +theorem StrictMono.nat_pow {n : ℕ} (hn : 1 ≤ n) {f : ℕ → ℕ} (hf : StrictMono f) : + StrictMono fun m => f m ^ n := + (Nat.pow_left_strict_mono hn).comp hf +#align strict_mono.nat_pow StrictMono.nat_pow + +namespace Nat + +theorem pow_le_iff_le_left {m x y : ℕ} (k : 1 ≤ m) : x ^ m ≤ y ^ m ↔ x ≤ y := + StrictMono.le_iff_le (pow_left_strict_mono k) +#align nat.pow_le_iff_le_left Nat.pow_le_iff_le_left + +theorem pow_lt_iff_lt_left {m x y : ℕ} (k : 1 ≤ m) : x ^ m < y ^ m ↔ x < y := + StrictMono.lt_iff_lt (pow_left_strict_mono k) +#align nat.pow_lt_iff_lt_left Nat.pow_lt_iff_lt_left + +theorem pow_left_injective {m : ℕ} (k : 1 ≤ m) : Function.Injective fun x : ℕ => x ^ m := + StrictMono.injective (pow_left_strict_mono k) +#align nat.pow_left_injective Nat.pow_left_injective + +theorem sq_sub_sq (a b : ℕ) : a ^ 2 - b ^ 2 = (a + b) * (a - b) := by + rw [sq, sq] + exact Nat.mul_self_sub_mul_self_eq a b +#align nat.sq_sub_sq Nat.sq_sub_sq + +alias sq_sub_sq ← pow_two_sub_pow_two + +/-! ### `pow` and `mod` / `dvd` -/ + + +theorem pow_mod (a b n : ℕ) : a ^ b % n = (a % n) ^ b % n := by + induction' b with b ih + rfl; simp [pow_succ, Nat.mul_mod, ih] +#align nat.pow_mod Nat.pow_mod + +theorem mod_pow_succ {b : ℕ} (w m : ℕ) : m % b ^ succ w = b * (m / b % b ^ w) + m % b := by + by_cases b_h : b = 0 + · simp [b_h, pow_succ] + have b_pos := Nat.pos_of_ne_zero b_h + apply Nat.strong_induction_on m + clear m + intro p IH + cases' lt_or_ge p (b ^ succ w) with h₁ h₁ + -- base case: p < b^succ w + · have h₂ : p / b < b ^ w := by + rw [div_lt_iff_lt_mul b_pos] + simpa [pow_succ'] using h₁ + rw [mod_eq_of_lt h₁, mod_eq_of_lt h₂] + simp [div_add_mod] + -- step: p ≥ b^succ w + · -- Generate condition for induction hypothesis + have h₂ : p - b ^ succ w < p := tsub_lt_self ((pow_pos b_pos _).trans_le h₁) (pow_pos b_pos _) + -- Apply induction + rw [mod_eq_sub_mod h₁, IH _ h₂] + -- Normalize goal and h1 + simp only [pow_succ] + simp only [GE.ge, pow_succ] at h₁ + -- Pull subtraction outside mod and div + rw [sub_mul_mod _ _ _ h₁, sub_mul_div _ _ _ h₁] + -- Cancel subtraction inside mod b^w + have p_b_ge : b ^ w ≤ p / b := by + rw [le_div_iff_mul_le b_pos, mul_comm] + exact h₁ + rw [Eq.symm (mod_eq_sub_mod p_b_ge)] +#align nat.mod_pow_succ Nat.mod_pow_succ + +theorem pow_dvd_pow_iff_pow_le_pow {k l : ℕ} : ∀ {x : ℕ} (w : 0 < x), x ^ k ∣ x ^ l ↔ x ^ k ≤ x ^ l + | x + 1, w => by + constructor + · intro a + exact le_of_dvd (pow_pos (succ_pos x) l) a + · intro a + cases' x with x + · simp only [one_pow] + · have le := (pow_le_iff_le_right (Nat.le_add_left _ _)).mp a + use (x + 2) ^ (l - k) + rw [← pow_add, add_comm k, tsub_add_cancel_of_le le] +#align nat.pow_dvd_pow_iff_pow_le_pow Nat.pow_dvd_pow_iff_pow_le_pow + +/-- If `1 < x`, then `x^k` divides `x^l` if and only if `k` is at most `l`. -/ +theorem pow_dvd_pow_iff_le_right {x k l : ℕ} (w : 1 < x) : x ^ k ∣ x ^ l ↔ k ≤ l := by + rw [pow_dvd_pow_iff_pow_le_pow (lt_of_succ_lt w), pow_le_iff_le_right w] +#align nat.pow_dvd_pow_iff_le_right Nat.pow_dvd_pow_iff_le_right + +theorem pow_dvd_pow_iff_le_right' {b k l : ℕ} : (b + 2) ^ k ∣ (b + 2) ^ l ↔ k ≤ l := + pow_dvd_pow_iff_le_right (Nat.lt_of_sub_eq_succ rfl) +#align nat.pow_dvd_pow_iff_le_right' Nat.pow_dvd_pow_iff_le_right' + +theorem not_pos_pow_dvd : ∀ {p k : ℕ} (hp : 1 < p) (hk : 1 < k), ¬p ^ k ∣ p + | succ p, succ k, hp, hk, h => + have : succ p * succ p ^ k ∣ succ p * 1 := by simpa [pow_succ] using h + have : succ p ^ k ∣ 1 := dvd_of_mul_dvd_mul_left (succ_pos _) this + have he : succ p ^ k = 1 := eq_one_of_dvd_one this + have : k < succ p ^ k := lt_pow_self hp k + have : k < 1 := by rwa [he] at this + have : k = 0 := Nat.eq_zero_of_le_zero <| le_of_lt_succ this + have : 1 < 1 := by rwa [this] at hk + absurd this (by decide) +#align nat.not_pos_pow_dvd Nat.not_pos_pow_dvd + +theorem pow_dvd_of_le_of_pow_dvd {p m n k : ℕ} (hmn : m ≤ n) (hdiv : p ^ n ∣ k) : p ^ m ∣ k := + (pow_dvd_pow _ hmn).trans hdiv +#align nat.pow_dvd_of_le_of_pow_dvd Nat.pow_dvd_of_le_of_pow_dvd + +theorem dvd_of_pow_dvd {p k m : ℕ} (hk : 1 ≤ k) (hpk : p ^ k ∣ m) : p ∣ m := by + rw [← pow_one p] <;> exact pow_dvd_of_le_of_pow_dvd hk hpk +#align nat.dvd_of_pow_dvd Nat.dvd_of_pow_dvd + +theorem pow_div {x m n : ℕ} (h : n ≤ m) (hx : 0 < x) : x ^ m / x ^ n = x ^ (m - n) := by + rw [Nat.div_eq_iff_eq_mul_left (pow_pos hx n) (pow_dvd_pow _ h), pow_sub_mul_pow _ h] +#align nat.pow_div Nat.pow_div + +theorem lt_of_pow_dvd_right {p i n : ℕ} (hn : n ≠ 0) (hp : 2 ≤ p) (h : p ^ i ∣ n) : i < n := by + rw [← pow_lt_iff_lt_right hp] + exact lt_of_le_of_lt (le_of_dvd hn.bot_lt h) (lt_pow_self (succ_le_iff.mp hp) n) +#align nat.lt_of_pow_dvd_right Nat.lt_of_pow_dvd_right + +end Nat From 2e911fa7e540b698e183cd7741529da841ae31b1 Mon Sep 17 00:00:00 2001 From: Riccardo Brasca Date: Thu, 15 Dec 2022 15:19:22 +0100 Subject: [PATCH 5/7] update mathlib.lean --- Mathlib.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib.lean b/Mathlib.lean index 0e9c6c8b0dd34..a9e23d9e78e27 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -196,6 +196,7 @@ import Mathlib.Data.Nat.Gcd.Basic import Mathlib.Data.Nat.Order.Basic import Mathlib.Data.Nat.Order.Lemmas import Mathlib.Data.Nat.PSub +import Mathlib.Data.Nat.Pow import Mathlib.Data.Nat.Set import Mathlib.Data.Nat.Units import Mathlib.Data.Nat.Upto From 67077a5991eeb3acc07478af4e662f370da28222 Mon Sep 17 00:00:00 2001 From: Riccardo Brasca Date: Thu, 15 Dec 2022 17:03:58 +0100 Subject: [PATCH 6/7] green --- Mathlib/Data/Nat/Pow.lean | 80 +++++++++++++++++++-------------------- 1 file changed, 40 insertions(+), 40 deletions(-) diff --git a/Mathlib/Data/Nat/Pow.lean b/Mathlib/Data/Nat/Pow.lean index e6b0ffbafb1ef..74b42d1ad60a5 100644 --- a/Mathlib/Data/Nat/Pow.lean +++ b/Mathlib/Data/Nat/Pow.lean @@ -8,7 +8,7 @@ Authors: Floris van Doorn, Leonardo de Moura, Jeremy Avigad, Mario Carneiro ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ -import Mathbin.Algebra.GroupPower.Order +import Mathlib.Algebra.GroupPower.Order /-! # `nat.pow` @@ -37,7 +37,7 @@ theorem pow_le_pow_of_le_right {x : ℕ} (H : 0 < x) {i j : ℕ} (h : i ≤ j) : -/ theorem pow_lt_pow_of_lt_left {x y : ℕ} (H : x < y) {i} (h : 0 < i) : x ^ i < y ^ i := - pow_lt_pow_of_lt_left H (zero_le _) h + _root_.pow_lt_pow_of_lt_left H (zero_le _) h #align nat.pow_lt_pow_of_lt_left Nat.pow_lt_pow_of_lt_left theorem pow_lt_pow_of_lt_right {x : ℕ} (H : 1 < x) {i j : ℕ} (h : i < j) : x ^ i < x ^ j := @@ -52,7 +52,7 @@ theorem lt_pow_self {p : ℕ} (h : 1 < p) : ∀ n : ℕ, n < p ^ n | 0 => by simp [zero_lt_one] | n + 1 => calc - n + 1 < p ^ n + 1 := Nat.add_lt_add_right (lt_pow_self _) _ + n + 1 < p ^ n + 1 := Nat.add_lt_add_right (lt_pow_self h _) _ _ ≤ p ^ (n + 1) := pow_lt_pow_succ h _ #align nat.lt_pow_self Nat.lt_pow_self @@ -85,15 +85,16 @@ theorem one_lt_pow' (n m : ℕ) : 1 < (m + 2) ^ (n + 1) := @[simp] theorem one_lt_pow_iff {k n : ℕ} (h : 0 ≠ k) : 1 < n ^ k ↔ 1 < n := by - cases n + rcases n with (rfl | n) · cases k <;> simp [zero_pow_eq] - cases n - · rw [one_pow] + rcases n with (rfl | n) + · rw [← Nat.one_eq_succ_zero, one_pow] refine' ⟨fun _ => one_lt_succ_succ n, fun _ => _⟩ induction' k with k hk · exact absurd rfl h - cases k - · simp + rcases k with (rfl | k) + · simp [← Nat.one_eq_succ_zero] + rw [pow_succ'] exact one_lt_mul (one_lt_succ_succ _).le (hk (succ_ne_zero k).symm) #align nat.one_lt_pow_iff Nat.one_lt_pow_iff @@ -126,8 +127,8 @@ theorem pow_left_strict_mono {m : ℕ} (k : 1 ≤ m) : StrictMono fun x : ℕ => #align nat.pow_left_strict_mono Nat.pow_left_strict_mono theorem mul_lt_mul_pow_succ {n a q : ℕ} (a0 : 0 < a) (q1 : 1 < q) : n * q < a * q ^ (n + 1) := by - rw [pow_succ', ← mul_assoc, mul_lt_mul_right (zero_lt_one.trans q1)] - exact lt_mul_of_one_le_of_lt (nat.succ_le_iff.mpr a0) (Nat.lt_pow_self q1 n) + rw [pow_succ, ← mul_assoc, mul_lt_mul_right (zero_lt_one.trans q1)] + exact lt_mul_of_one_le_of_lt (Nat.succ_le_iff.mpr a0) (Nat.lt_pow_self q1 n) #align nat.mul_lt_mul_pow_succ Nat.mul_lt_mul_pow_succ end Nat @@ -170,41 +171,40 @@ theorem mod_pow_succ {b : ℕ} (w m : ℕ) : m % b ^ succ w = b * (m / b % b ^ w by_cases b_h : b = 0 · simp [b_h, pow_succ] have b_pos := Nat.pos_of_ne_zero b_h - apply Nat.strong_induction_on m - clear m - intro p IH - cases' lt_or_ge p (b ^ succ w) with h₁ h₁ - -- base case: p < b^succ w - · have h₂ : p / b < b ^ w := by - rw [div_lt_iff_lt_mul b_pos] - simpa [pow_succ'] using h₁ - rw [mod_eq_of_lt h₁, mod_eq_of_lt h₂] - simp [div_add_mod] - -- step: p ≥ b^succ w - · -- Generate condition for induction hypothesis - have h₂ : p - b ^ succ w < p := tsub_lt_self ((pow_pos b_pos _).trans_le h₁) (pow_pos b_pos _) - -- Apply induction - rw [mod_eq_sub_mod h₁, IH _ h₂] + induction m using Nat.strong_induction_on with + | h p IH => + cases' lt_or_ge p (b ^ succ w) with h₁ h₁ + -- base case: p < b^succ w + · have h₂ : p / b < b ^ w := by + rw [div_lt_iff_lt_mul b_pos] + simpa [pow_succ] using h₁ + rw [mod_eq_of_lt h₁, mod_eq_of_lt h₂] + simp [div_add_mod] + -- step: p ≥ b^succ w + · -- Generate condition for induction hypothesis + have h₂ : p - b ^ succ w < p := tsub_lt_self ((pow_pos b_pos _).trans_le h₁) (pow_pos b_pos _) + -- Apply induction + rw [mod_eq_sub_mod h₁, IH _ h₂] -- Normalize goal and h1 - simp only [pow_succ] - simp only [GE.ge, pow_succ] at h₁ - -- Pull subtraction outside mod and div - rw [sub_mul_mod _ _ _ h₁, sub_mul_div _ _ _ h₁] - -- Cancel subtraction inside mod b^w - have p_b_ge : b ^ w ≤ p / b := by - rw [le_div_iff_mul_le b_pos, mul_comm] - exact h₁ - rw [Eq.symm (mod_eq_sub_mod p_b_ge)] + simp only [pow_succ'] + simp only [GE.ge, pow_succ'] at h₁ + -- Pull subtraction outside mod and div + rw [sub_mul_mod h₁, sub_mul_div _ _ _ h₁] + -- Cancel subtraction inside mod b^w + have p_b_ge : b ^ w ≤ p / b := by + rw [le_div_iff_mul_le b_pos, mul_comm] + exact h₁ + rw [Eq.symm (mod_eq_sub_mod p_b_ge)] #align nat.mod_pow_succ Nat.mod_pow_succ -theorem pow_dvd_pow_iff_pow_le_pow {k l : ℕ} : ∀ {x : ℕ} (w : 0 < x), x ^ k ∣ x ^ l ↔ x ^ k ≤ x ^ l +theorem pow_dvd_pow_iff_pow_le_pow {k l : ℕ} : ∀ {x : ℕ} (_ : 0 < x), x ^ k ∣ x ^ l ↔ x ^ k ≤ x ^ l | x + 1, w => by constructor · intro a exact le_of_dvd (pow_pos (succ_pos x) l) a · intro a cases' x with x - · simp only [one_pow] + · simp · have le := (pow_le_iff_le_right (Nat.le_add_left _ _)).mp a use (x + 2) ^ (l - k) rw [← pow_add, add_comm k, tsub_add_cancel_of_le le] @@ -219,10 +219,10 @@ theorem pow_dvd_pow_iff_le_right' {b k l : ℕ} : (b + 2) ^ k ∣ (b + 2) ^ l pow_dvd_pow_iff_le_right (Nat.lt_of_sub_eq_succ rfl) #align nat.pow_dvd_pow_iff_le_right' Nat.pow_dvd_pow_iff_le_right' -theorem not_pos_pow_dvd : ∀ {p k : ℕ} (hp : 1 < p) (hk : 1 < k), ¬p ^ k ∣ p +theorem not_pos_pow_dvd : ∀ {p k : ℕ} (_ : 1 < p) (_ : 1 < k), ¬p ^ k ∣ p | succ p, succ k, hp, hk, h => - have : succ p * succ p ^ k ∣ succ p * 1 := by simpa [pow_succ] using h - have : succ p ^ k ∣ 1 := dvd_of_mul_dvd_mul_left (succ_pos _) this + have : succ p * succ p ^ k ∣ succ p * 1 := by simpa [pow_succ'] using h + have : succ p ^ k ∣ 1 := Nat.dvd_of_mul_dvd_mul_left (succ_pos _) this have he : succ p ^ k = 1 := eq_one_of_dvd_one this have : k < succ p ^ k := lt_pow_self hp k have : k < 1 := by rwa [he] at this @@ -236,7 +236,7 @@ theorem pow_dvd_of_le_of_pow_dvd {p m n k : ℕ} (hmn : m ≤ n) (hdiv : p ^ n #align nat.pow_dvd_of_le_of_pow_dvd Nat.pow_dvd_of_le_of_pow_dvd theorem dvd_of_pow_dvd {p k m : ℕ} (hk : 1 ≤ k) (hpk : p ^ k ∣ m) : p ∣ m := by - rw [← pow_one p] <;> exact pow_dvd_of_le_of_pow_dvd hk hpk + rw [← pow_one p]; exact pow_dvd_of_le_of_pow_dvd hk hpk #align nat.dvd_of_pow_dvd Nat.dvd_of_pow_dvd theorem pow_div {x m n : ℕ} (h : n ≤ m) (hx : 0 < x) : x ^ m / x ^ n = x ^ (m - n) := by From 13e1d4bcab952d81885f333beb4467eed9ab7f49 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Fri, 16 Dec 2022 14:06:03 +1100 Subject: [PATCH 7/7] minor --- Mathlib/Data/Nat/Pow.lean | 25 ++++++++----------------- 1 file changed, 8 insertions(+), 17 deletions(-) diff --git a/Mathlib/Data/Nat/Pow.lean b/Mathlib/Data/Nat/Pow.lean index 74b42d1ad60a5..c26ea63cab518 100644 --- a/Mathlib/Data/Nat/Pow.lean +++ b/Mathlib/Data/Nat/Pow.lean @@ -20,21 +20,12 @@ namespace Nat /-! ### `pow` -/ +-- Porting note: the next two lemmas have moved into `Std`. -#print Nat.pow_le_pow_of_le_left /- --- This is redundant with `pow_le_pow_of_le_left'`, --- We leave a version in the `nat` namespace as well. --- (The global `pow_le_pow_of_le_left` needs an extra hypothesis `0 ≤ x`.) -protected theorem pow_le_pow_of_le_left {x y : ℕ} (H : x ≤ y) : ∀ i : ℕ, x ^ i ≤ y ^ i := - pow_le_pow_of_le_left' H +-- The global `pow_le_pow_of_le_left` needs an extra hypothesis `0 ≤ x`. #align nat.pow_le_pow_of_le_left Nat.pow_le_pow_of_le_left --/ - -#print Nat.pow_le_pow_of_le_right /- -theorem pow_le_pow_of_le_right {x : ℕ} (H : 0 < x) {i j : ℕ} (h : i ≤ j) : x ^ i ≤ x ^ j := - pow_le_pow' H h #align nat.pow_le_pow_of_le_right Nat.pow_le_pow_of_le_right --/ + theorem pow_lt_pow_of_lt_left {x y : ℕ} (H : x < y) {i} (h : 0 < i) : x ^ i < y ^ i := _root_.pow_lt_pow_of_lt_left H (zero_le _) h @@ -174,18 +165,18 @@ theorem mod_pow_succ {b : ℕ} (w m : ℕ) : m % b ^ succ w = b * (m / b % b ^ w induction m using Nat.strong_induction_on with | h p IH => cases' lt_or_ge p (b ^ succ w) with h₁ h₁ - -- base case: p < b^succ w - · have h₂ : p / b < b ^ w := by + · -- base case: p < b^succ w + have h₂ : p / b < b ^ w := by rw [div_lt_iff_lt_mul b_pos] simpa [pow_succ] using h₁ rw [mod_eq_of_lt h₁, mod_eq_of_lt h₂] simp [div_add_mod] - -- step: p ≥ b^succ w - · -- Generate condition for induction hypothesis + · -- step: p ≥ b^succ w + -- Generate condition for induction hypothesis have h₂ : p - b ^ succ w < p := tsub_lt_self ((pow_pos b_pos _).trans_le h₁) (pow_pos b_pos _) -- Apply induction rw [mod_eq_sub_mod h₁, IH _ h₂] - -- Normalize goal and h1 + -- Normalize goal and h1 simp only [pow_succ'] simp only [GE.ge, pow_succ'] at h₁ -- Pull subtraction outside mod and div