-
Notifications
You must be signed in to change notification settings - Fork 298
/
order.lean
297 lines (219 loc) · 10.4 KB
/
order.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
/-
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 algebra.ordered_ring
import algebra.group_power.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.
-/
variables {A G M R : Type*}
section preorder
variables [monoid M] [preorder M] [covariant_class M M (*) (≤)]
@[mono, to_additive nsmul_le_nsmul_of_le_right]
lemma pow_le_pow_of_le_left' [covariant_class M M (function.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' k) }
@[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' k) }
@[to_additive nsmul_nonpos]
theorem pow_le_one' {a : M} (H : a ≤ 1) (n : ℕ) : a ^ n ≤ 1 :=
@one_le_pow_of_one_le' (order_dual M) _ _ _ _ H n
@[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 in
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]
@[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' (order_dual M) _ _ _ _ _ _ ha h
@[to_additive nsmul_pos]
theorem one_lt_pow' {a : M} (ha : 1 < a) {k : ℕ} (hk : k ≠ 0) : 1 < a ^ k :=
begin
rcases nat.exists_eq_succ_of_ne_zero hk with ⟨l, rfl⟩,
clear hk,
induction l with l IH,
{ simpa using ha },
{ rw pow_succ,
exact one_lt_mul' ha IH }
end
@[to_additive nsmul_neg]
theorem pow_lt_one' {a : M} (ha : a < 1) {k : ℕ} (hk : k ≠ 0) : a ^ k < 1 :=
@one_lt_pow' (order_dual M) _ _ _ _ ha k hk
@[to_additive nsmul_lt_nsmul]
theorem pow_lt_pow'' [covariant_class M M (*) (<)] {a : M} {n m : ℕ} (ha : 1 < a) (h : n < m) :
a ^ n < a ^ m :=
begin
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)
end
end preorder
section linear_order
variables [monoid M] [linear_order M] [covariant_class M M (*) (≤)]
@[to_additive nsmul_nonneg_iff]
lemma one_le_pow_iff {x : M} {n : ℕ} (hn : n ≠ 0) : 1 ≤ x ^ n ↔ 1 ≤ x :=
⟨le_imp_le_of_lt_imp_lt $ λ h, pow_lt_one' h hn, λ h, one_le_pow_of_one_le' h n⟩
@[to_additive nsmul_nonpos_iff]
lemma pow_le_one_iff {x : M} {n : ℕ} (hn : n ≠ 0) : x ^ n ≤ 1 ↔ x ≤ 1 :=
@one_le_pow_iff (order_dual M) _ _ _ _ _ hn
@[to_additive nsmul_pos_iff]
lemma 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)
@[to_additive nsmul_neg_iff]
lemma 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)
@[to_additive nsmul_eq_zero_iff]
lemma pow_eq_one_iff {x : M} {n : ℕ} (hn : n ≠ 0) : x ^ n = 1 ↔ x = 1 :=
by simp only [le_antisymm_iff, pow_le_one_iff hn, one_le_pow_iff hn]
end linear_order
section group
variables [group G] [preorder G] [covariant_class G G (*) (≤)]
@[to_additive gsmul_nonneg]
theorem one_le_gpow {x : G} (H : 1 ≤ x) {n : ℤ} (hn : 0 ≤ n) :
1 ≤ x ^ n :=
begin
lift n to ℕ using hn,
rw gpow_coe_nat,
apply one_le_pow_of_one_le' H,
end
end group
namespace canonically_ordered_comm_semiring
variables [canonically_ordered_comm_semiring R]
theorem pow_pos {a : R} (H : 0 < a) (n : ℕ) : 0 < a ^ n :=
pos_iff_ne_zero.2 $ pow_ne_zero _ H.ne'
end canonically_ordered_comm_semiring
section ordered_semiring
variable [ordered_semiring R]
@[simp] theorem pow_pos {a : R} (H : 0 < a) : ∀ (n : ℕ), 0 < a ^ n
| 0 := by { nontriviality, rw pow_zero, exact zero_lt_one }
| (n+1) := by { rw pow_succ, exact mul_pos H (pow_pos _) }
@[simp] theorem pow_nonneg {a : R} (H : 0 ≤ a) : ∀ (n : ℕ), 0 ≤ a ^ n
| 0 := by { rw pow_zero, exact zero_le_one}
| (n+1) := by { rw pow_succ, exact mul_nonneg H (pow_nonneg _) }
theorem pow_add_pow_le {x y : R} {n : ℕ} (hx : 0 ≤ x) (hy : 0 ≤ y) (hn : n ≠ 0) :
x ^ n + y ^ n ≤ (x + y) ^ n :=
begin
rcases nat.exists_eq_succ_of_ne_zero hn with ⟨k, rfl⟩,
induction k with k ih, { simp only [pow_one] },
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 }
end
theorem pow_lt_pow_of_lt_left {x y : R} {n : ℕ} (Hxy : x < y) (Hxpos : 0 ≤ x) (Hnpos : 0 < n) :
x ^ n < y ^ n :=
begin
cases lt_or_eq_of_le Hxpos,
{ rw ←nat.sub_add_cancel Hnpos,
induction (n - 1), { simpa only [pow_one] },
rw [pow_add, pow_add, nat.succ_eq_add_one, pow_one, pow_one],
apply mul_lt_mul ih (le_of_lt Hxy) h (le_of_lt (pow_pos (lt_trans h Hxy) _)) },
{ rw [←h, zero_pow Hnpos], apply pow_pos (by rwa ←h at Hxy : 0 < y),}
end
theorem strict_mono_incr_on_pow {n : ℕ} (hn : 0 < n) :
strict_mono_incr_on (λ x : R, x ^ n) (set.Ici 0) :=
λ x hx y hy h, pow_lt_pow_of_lt_left h hx hn
theorem one_le_pow_of_one_le {a : R} (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 n)
zero_le_one (le_trans zero_le_one H) }
lemma pow_mono {a : R} (h : 1 ≤ a) : monotone (λ n : ℕ, a ^ n) :=
monotone_nat_of_le_succ $ λ n,
by { rw pow_succ, exact le_mul_of_one_le_left (pow_nonneg (zero_le_one.trans h) _) h }
theorem pow_le_pow {a : R} {n m : ℕ} (ha : 1 ≤ a) (h : n ≤ m) : a ^ n ≤ a ^ m :=
pow_mono ha h
lemma strict_mono_pow {a : R} (h : 1 < a) : strict_mono (λ n : ℕ, a ^ n) :=
have 0 < a := zero_le_one.trans_lt h,
strict_mono_nat_of_lt_succ $ λ n, by simpa only [one_mul, pow_succ]
using mul_lt_mul h (le_refl (a ^ n)) (pow_pos this _) this.le
lemma pow_lt_pow {a : R} {n m : ℕ} (h : 1 < a) (h2 : n < m) : a ^ n < a ^ m :=
strict_mono_pow h h2
lemma pow_lt_pow_iff {a : R} {n m : ℕ} (h : 1 < a) : a ^ n < a ^ m ↔ n < m :=
(strict_mono_pow h).lt_iff_lt
@[mono] lemma pow_le_pow_of_le_left {a b : R} (ha : 0 ≤ a) (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 _) (pow_nonneg ha _) (le_trans ha hab) }
end ordered_semiring
section linear_ordered_semiring
variable [linear_ordered_semiring R]
@[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_incr_on_pow R _ _ Hnpos).inj_on.eq_iff Hxpos Hypos
lemma lt_of_pow_lt_pow {a b : R} (n : ℕ) (hb : 0 ≤ b) (h : a ^ n < b ^ n) : a < b :=
lt_of_not_ge $ λ hn, not_lt_of_ge (pow_le_pow_of_le_left hb hn _) h
lemma 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 $ λ h1, not_le_of_lt (pow_lt_pow_of_lt_left h1 hb hn) h
@[simp] lemma sq_eq_sq {a b : R} (ha : 0 ≤ a) (hb : 0 ≤ b) : a ^ 2 = b ^ 2 ↔ a = b :=
pow_left_inj ha hb dec_trivial
end linear_ordered_semiring
section linear_ordered_ring
variable [linear_ordered_ring R]
lemma pow_abs (a : R) (n : ℕ) : (abs a) ^ n = abs (a ^ n) :=
((abs_hom.to_monoid_hom : R →* R).map_pow a n).symm
lemma abs_neg_one_pow (n : ℕ) : abs ((-1 : R) ^ n) = 1 :=
by rw [←pow_abs, abs_neg, abs_one, one_pow]
theorem pow_bit0_nonneg (a : R) (n : ℕ) : 0 ≤ a ^ bit0 n :=
by { rw pow_bit0, exact mul_self_nonneg _ }
theorem sq_nonneg (a : R) : 0 ≤ a ^ 2 :=
pow_bit0_nonneg a 1
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
theorem sq_pos_of_ne_zero (a : R) (h : a ≠ 0) : 0 < a ^ 2 :=
pow_bit0_pos h 1
alias sq_pos_of_ne_zero ← pow_two_pos_of_ne_zero
variables {x y : R}
theorem sq_abs (x : R) : abs x ^ 2 = x ^ 2 :=
by simpa only [sq] using abs_mul_abs_self x
theorem abs_sq (x : R) : abs (x ^ 2) = x ^ 2 :=
by simpa only [sq] using abs_mul_self x
theorem sq_lt_sq (h : abs x < y) : x ^ 2 < y ^ 2 :=
by simpa only [sq_abs] using pow_lt_pow_of_lt_left h (abs_nonneg x) (1:ℕ).succ_pos
theorem sq_lt_sq' (h1 : -y < x) (h2 : x < y) : x ^ 2 < y ^ 2 :=
sq_lt_sq (abs_lt.mpr ⟨h1, h2⟩)
theorem sq_le_sq (h : abs x ≤ abs y) : x ^ 2 ≤ y ^ 2 :=
by simpa only [sq_abs] using pow_le_pow_of_le_left (abs_nonneg x) h 2
theorem sq_le_sq' (h1 : -y ≤ x) (h2 : x ≤ y) : x ^ 2 ≤ y ^ 2 :=
sq_le_sq (le_trans (abs_le.mpr ⟨h1, h2⟩) (le_abs_self _))
theorem abs_lt_abs_of_sq_lt_sq (h : x^2 < y^2) : abs x < abs y :=
lt_of_pow_lt_pow 2 (abs_nonneg y) $ by rwa [← sq_abs x, ← sq_abs y] at h
theorem abs_lt_of_sq_lt_sq (h : x^2 < y^2) (hy : 0 ≤ y) : abs x < y :=
begin
rw [← abs_of_nonneg hy],
exact abs_lt_abs_of_sq_lt_sq h,
end
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
theorem abs_le_abs_of_sq_le_sq (h : x^2 ≤ y^2) : abs x ≤ abs y :=
le_of_pow_le_pow 2 (abs_nonneg y) (1:ℕ).succ_pos $ by rwa [← sq_abs x, ← sq_abs y] at h
theorem abs_le_of_sq_le_sq (h : x^2 ≤ y^2) (hy : 0 ≤ y) : abs x ≤ y :=
begin
rw [← abs_of_nonneg hy],
exact abs_le_abs_of_sq_le_sq h,
end
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
end linear_ordered_ring
section linear_ordered_comm_ring
variables [linear_ordered_comm_ring R]
/-- Arithmetic mean-geometric mean (AM-GM) inequality for linearly ordered commutative rings. -/
lemma 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 _)))
alias two_mul_le_add_sq ← two_mul_le_add_pow_two
end linear_ordered_comm_ring