Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit f5a600f

Browse files
YaelDilliesYaelDillies
committed
feat(algebra/order/ring): Non-cancellative ordered semirings (#16172)
## Historical background This tackles a problem that we have had for six years (#2697 for its move to mathlib, before it was in core): `ordered_semiring` assumes that addition and multiplication are strictly monotone. This led to weirdness within the algebraic order hierarchy: * `ennreal`/`ereal`/`enat` needed custom lemmas (`∞ + 0 = ∞ = ∞ + 1`, `1 * ∞ = ∞ = 2 * ∞`). * A `canonically_ordered_comm_semiring` was not an `ordered_comm_semiring`! ## What this PR does This PR solves the problem minimally by renaming `ordered_(comm_)semiring` to `strict_ordered_(comm_)semiring` and adding a new class `ordered_(comm_)semiring` that doesn't assume strict monotonicity of addition and multiplication but only monotonicity: ``` class ordered_semiring (α : Type*) extends semiring α, ordered_add_comm_monoid α := (zero_le_one : (0 : α) ≤ 1) (mul_le_mul_of_nonneg_left : ∀ a b c : α, a ≤ b → 0 ≤ c → c * a ≤ c * b) (mul_le_mul_of_nonneg_right : ∀ a b c : α, a ≤ b → 0 ≤ c → a * c ≤ b * c) class ordered_comm_semiring (α : Type*) extends ordered_semiring α, comm_semiring α class ordered_ring (α : Type u) extends ring α, ordered_add_comm_group α := (zero_le_one : 0 ≤ (1 : α)) (mul_nonneg : ∀ a b : α, 0 ≤ a → 0 ≤ b → 0 ≤ a * b) class ordered_comm_ring (α : Type u) extends ordered_ring α, comm_ring α class strict_ordered_semiring (α : Type*) extends semiring α, ordered_cancel_add_comm_monoid α := (zero_le_one : (0 : α) ≤ 1) (mul_lt_mul_of_pos_left : ∀ a b c : α, a < b → 0 < c → c * a < c * b) (mul_lt_mul_of_pos_right : ∀ a b c : α, a < b → 0 < c → a * c < b * c) class strict_ordered_comm_semiring (α : Type*) extends strict_ordered_semiring α, comm_semiring α class strict_ordered_ring (α : Type u) extends ring α, ordered_add_comm_group α := (zero_le_one : 0 ≤ (1 : α)) (mul_pos : ∀ a b : α, 0 < a → 0 < b → 0 < a * b) class strict_ordered_comm_ring (α : Type*) extends strict_ordered_ring α, comm_ring α ``` ## Whatever happened to the `decidable` lemmas? Scrolling through the diff, you will see that only one lemma in the `decidable` namespace out of many survives this PR. Those lemmas were originally meant to avoid using choice in the proof of `nat` and `int` lemmas. The need for decidability originated from the proofs of `mul_le_mul_of_nonneg_left`/`mul_le_mul_of_nonneg_right`. ``` protected lemma decidable.mul_le_mul_of_nonneg_left [@decidable_rel α (≤)] (h₁ : a ≤ b) (h₂ : 0 ≤ c) : c * a ≤ c * b := begin by_cases ba : b ≤ a, { simp [ba.antisymm h₁] }, by_cases c0 : c ≤ 0, { simp [c0.antisymm h₂] }, exact (mul_lt_mul_of_pos_left (h₁.lt_of_not_le ba) (h₂.lt_of_not_le c0)).le, end ``` Now that these are fields to `ordered_semiring`, they are already choice-free. Instead, choice is now used in showing that an `ordered_cancel_semiring` is an `ordered_semiring`. ``` @[priority 100] -- see Note [lower instance priority] instance ordered_cancel_semiring.to_ordered_semiring : ordered_semiring α := { mul_le_mul_of_nonneg_left := λ a b c hab hc, begin obtain rfl | hab := hab.eq_or_lt, { refl }, obtain rfl | hc := hc.eq_or_lt, { simp }, { exact (mul_lt_mul_of_pos_left hab hc).le } end, mul_le_mul_of_nonneg_right := λ a b c hab hc, begin obtain rfl | hab := hab.eq_or_lt, { refl }, obtain rfl | hc := hc.eq_or_lt, { simp }, { exact (mul_lt_mul_of_pos_right hab hc).le } end, ..‹ordered_cancel_semiring α› } ``` It seems unreasonable to make that instance depend on `@decidable_rel α (≤)` even though it's only needed for the proofs. ## Other changes To have some lemmas in the generality of the new `ordered_semiring`, I needed a few new lemmas: * `bit0_mono` * `bit0_strict_mono` It was also simpler to golf `analysis.special_functions.stirling` using `positivity` rather than fixing it so I introduce the following (simple) `positivity` extensions: * `positivity_succ` * `positivity_factorial` * `positivity_asc_factorial`
1 parent fdb930f commit f5a600f

57 files changed

Lines changed: 1237 additions & 1177 deletions

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎archive/imo/imo2008_q3.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -66,11 +66,11 @@ begin
6666
have hreal₃ : (k:ℝ) ^ 2 + 4 ≥ p, { assumption_mod_cast },
6767

6868
have hreal₅ : (k:ℝ) > 4,
69-
{ apply lt_of_pow_lt_pow 2 k.cast_nonneg,
69+
{ refine lt_of_pow_lt_pow 2 k.cast_nonneg _,
7070
linarith only [hreal₂, hreal₃] },
7171

7272
have hreal₆ : (k:ℝ) > sqrt (2 * n),
73-
{ apply lt_of_pow_lt_pow 2 k.cast_nonneg,
73+
{ refine lt_of_pow_lt_pow 2 k.cast_nonneg _,
7474
rw sq_sqrt (mul_nonneg zero_le_two n.cast_nonneg),
7575
linarith only [hreal₁, hreal₃, hreal₅] },
7676

‎counterexamples/canonically_ordered_comm_semiring_two_mul.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -132,7 +132,7 @@ lemma mul_lt_mul_of_pos_left : ∀ (a b c : ℕ × zmod 2), a < b → 0 < c →
132132
lemma mul_lt_mul_of_pos_right : ∀ (a b c : ℕ × zmod 2), a < b → 0 < c → a * c < b * c :=
133133
λ a b c ab c0, lt_def.mpr ((mul_lt_mul_right (lt_def.mp c0)).mpr (lt_def.mp ab))
134134

135-
instance ocsN2 : ordered_comm_semiring (ℕ × zmod 2) :=
135+
instance socsN2 : strict_ordered_comm_semiring (ℕ × zmod 2) :=
136136
{ add_le_add_left := add_le_add_left,
137137
le_of_add_le_add_left := le_of_add_le_add_left,
138138
zero_le_one := zero_le_one,

‎src/algebra/algebra/subalgebra/basic.lean‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -188,9 +188,15 @@ instance to_comm_ring {R A}
188188
instance to_ordered_semiring {R A}
189189
[comm_semiring R] [ordered_semiring A] [algebra R A] (S : subalgebra R A) :
190190
ordered_semiring S := S.to_subsemiring.to_ordered_semiring
191+
instance to_strict_ordered_semiring {R A}
192+
[comm_semiring R] [strict_ordered_semiring A] [algebra R A] (S : subalgebra R A) :
193+
strict_ordered_semiring S := S.to_subsemiring.to_strict_ordered_semiring
191194
instance to_ordered_comm_semiring {R A}
192195
[comm_semiring R] [ordered_comm_semiring A] [algebra R A] (S : subalgebra R A) :
193196
ordered_comm_semiring S := S.to_subsemiring.to_ordered_comm_semiring
197+
instance to_strict_ordered_comm_semiring {R A}
198+
[comm_semiring R] [strict_ordered_comm_semiring A] [algebra R A] (S : subalgebra R A) :
199+
strict_ordered_comm_semiring S := S.to_subsemiring.to_strict_ordered_comm_semiring
194200
instance to_ordered_ring {R A}
195201
[comm_ring R] [ordered_ring A] [algebra R A] (S : subalgebra R A) :
196202
ordered_ring S := S.to_subring.to_ordered_ring

‎src/algebra/big_operators/order.lean‎

Lines changed: 18 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -411,6 +411,14 @@ lt_of_le_of_lt (by rw prod_const_one) $ prod_lt_prod_of_nonempty' hs h
411411
(∏ i in s, f i) < 1 :=
412412
(prod_lt_prod_of_nonempty' hs h).trans_le (by rw prod_const_one)
413413

414+
@[to_additive sum_pos'] lemma one_lt_prod' (h : ∀ i ∈ s, 1 ≤ f i) (hs : ∃ i ∈ s, 1 < f i) :
415+
1 < (∏ i in s, f i) :=
416+
prod_const_one.symm.trans_lt $ prod_lt_prod' h hs
417+
418+
@[to_additive] lemma prod_lt_one' (h : ∀ i ∈ s, f i ≤ 1) (hs : ∃ i ∈ s, f i < 1) :
419+
∏ i in s, f i < 1 :=
420+
prod_const_one.le.trans_lt' $ prod_lt_prod' h hs
421+
414422
@[to_additive] lemma prod_eq_prod_iff_of_le {f g : ι → M} (h : ∀ i ∈ s, f i ≤ g i) :
415423
∏ i in s, f i = ∏ i in s, g i ↔ ∀ i ∈ s, f i = g i :=
416424
begin
@@ -464,15 +472,10 @@ section ordered_comm_semiring
464472
variables [ordered_comm_semiring R] {f g : ι → R} {s t : finset ι}
465473
open_locale classical
466474

467-
/- this is also true for a ordered commutative multiplicative monoid -/
475+
/- this is also true for a ordered commutative multiplicative monoid with zero -/
468476
lemma prod_nonneg (h0 : ∀ i ∈ s, 0 ≤ f i) : 0 ≤ ∏ i in s, f i :=
469477
prod_induction f (λ i, 0 ≤ i) (λ _ _ ha hb, mul_nonneg ha hb) zero_le_one h0
470478

471-
/- this is also true for a ordered commutative multiplicative monoid -/
472-
lemma prod_pos [nontrivial R] (h0 : ∀ i ∈ s, 0 < f i) :
473-
0 < ∏ i in s, f i :=
474-
prod_induction f (λ x, 0 < x) (λ _ _ ha hb, mul_pos ha hb) zero_lt_one h0
475-
476479
/-- If all `f i`, `i ∈ s`, are nonnegative and each `f i` is less than or equal to `g i`, then the
477480
product of `f i` is less than or equal to the product of `g i`. See also `finset.prod_le_prod''` for
478481
the case of an ordered commutative multiplicative monoid. -/
@@ -515,6 +518,15 @@ end
515518

516519
end ordered_comm_semiring
517520

521+
section strict_ordered_comm_semiring
522+
variables [strict_ordered_comm_semiring R] [nontrivial R] {f : ι → R} {s : finset ι}
523+
524+
/- This is also true for a ordered commutative multiplicative monoid with zero -/
525+
lemma prod_pos (h0 : ∀ i ∈ s, 0 < f i) : 0 < ∏ i in s, f i :=
526+
prod_induction f (λ x, 0 < x) (λ _ _ ha hb, mul_pos ha hb) zero_lt_one h0
527+
528+
end strict_ordered_comm_semiring
529+
518530
section canonically_ordered_comm_semiring
519531

520532
variables [canonically_ordered_comm_semiring R] {f g h : ι → R} {s : finset ι} {i : ι}

‎src/algebra/geom_sum.lean‎

Lines changed: 56 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -409,10 +409,11 @@ section order
409409

410410
variables {n : ℕ} {x : α}
411411

412-
lemma geom_sum_pos [ordered_semiring α] (hx : 0 < x) (hn : n ≠ 0) : 0 < ∑ i in range n, x ^ i :=
413-
sum_pos (λ k hk, pow_pos hx _) $ nonempty_range_iff.2 hn
412+
lemma geom_sum_pos [strict_ordered_semiring α] [nontrivial α] (hx : 0 ≤ x) (hn : n ≠ 0) :
413+
0 < ∑ i in range n, x ^ i :=
414+
sum_pos' (λ k hk, pow_nonneg hx _) ⟨0, mem_range.2 hn.bot_lt, by simp⟩
414415

415-
lemma geom_sum_pos_and_lt_one [ordered_ring α] (hx : x < 0) (hx' : 0 < x + 1) (hn : 1 < n) :
416+
lemma geom_sum_pos_and_lt_one [strict_ordered_ring α] (hx : x < 0) (hx' : 0 < x + 1) (hn : 1 < n) :
416417
0 < ∑ i in range n, x ^ i ∧ ∑ i in range n, x ^ i < 1 :=
417418
begin
418419
refine nat.le_induction _ _ n (show 2 ≤ n, from hn),
@@ -425,7 +426,22 @@ begin
425426
(neg_lt_iff_pos_add'.2 hx') ihn.2.le, mul_neg_of_neg_of_pos hx ihn.1⟩
426427
end
427428

428-
lemma geom_sum_alternating_of_lt_neg_one [ordered_ring α] (hx : x + 1 < 0) (hn : 1 < n) :
429+
lemma geom_sum_alternating_of_le_neg_one [strict_ordered_ring α] (hx : x + 1 ≤ 0) (n : ℕ) :
430+
if even n then ∑ i in range n, x ^ i ≤ 0 else 1 ≤ ∑ i in range n, x ^ i :=
431+
begin
432+
have hx0 : x ≤ 0 := (le_add_of_nonneg_right zero_le_one).trans hx,
433+
induction n with n ih,
434+
{ simp only [even_zero, geom_sum_zero, le_refl] },
435+
simp only [nat.even_add_one, geom_sum_succ],
436+
split_ifs at ih,
437+
{ rw [if_neg (not_not_intro h), le_add_iff_nonneg_left],
438+
exact mul_nonneg_of_nonpos_of_nonpos hx0 ih },
439+
{ rw if_pos h,
440+
refine (add_le_add_right _ _).trans hx,
441+
simpa only [mul_one] using mul_le_mul_of_nonpos_left ih hx0 }
442+
end
443+
444+
lemma geom_sum_alternating_of_lt_neg_one [strict_ordered_ring α] (hx : x + 1 < 0) (hn : 1 < n) :
429445
if even n then ∑ i in range n, x ^ i < 0 else 1 < ∑ i in range n, x ^ i :=
430446
begin
431447
have hx0 : x < 0, from ((le_add_iff_nonneg_right _).2 zero_le_one).trans_lt hx,
@@ -443,6 +459,17 @@ begin
443459
exact this.trans hx }
444460
end
445461

462+
lemma geom_sum_pos' [linear_ordered_ring α] (hx : 0 < x + 1) (hn : n ≠ 0) :
463+
0 < ∑ i in range n, x ^ i :=
464+
begin
465+
obtain _ | _ | n := n,
466+
{ cases hn rfl },
467+
{ simp },
468+
obtain hx' | hx' := lt_or_le x 0,
469+
{ exact (geom_sum_pos_and_lt_one hx' hx n.one_lt_succ_succ).1 },
470+
{ exact geom_sum_pos hx' (by simp only [nat.succ_ne_zero, ne.def, not_false_iff]) }
471+
end
472+
446473
lemma odd.geom_sum_pos [linear_ordered_ring α] (h : odd n) :
447474
0 < ∑ i in range n, x ^ i :=
448475
begin
@@ -455,55 +482,47 @@ begin
455482
simp only [h, if_false] at this,
456483
exact zero_lt_one.trans this },
457484
{ simp only [eq_neg_of_add_eq_zero_left hx, h, neg_one_geom_sum, if_false, zero_lt_one] },
458-
rcases lt_trichotomy x 0 with hx' | rfl | hx',
459-
{ exact (geom_sum_pos_and_lt_one hx' hx k.one_lt_succ_succ).1 },
460-
{ simp only [zero_geom_sum, nat.succ_ne_zero, if_false, zero_lt_one] },
461-
{ exact geom_sum_pos hx' (by simp only [nat.succ_ne_zero, ne.def, not_false_iff]) }
485+
{ exact geom_sum_pos' hx k.succ.succ_ne_zero }
462486
end
463487

464-
lemma geom_sum_pos_iff [linear_ordered_ring α] (hn : 1 < n) :
488+
lemma geom_sum_pos_iff [linear_ordered_ring α] (hn : n ≠ 0) :
465489
0 < ∑ i in range n, x ^ i ↔ odd n ∨ 0 < x + 1 :=
466490
begin
467491
refine ⟨λ h, _, _⟩,
468-
{ suffices : ¬ 0 < x + 1 → odd n, by tauto,
469-
intro hx,
470-
rw not_lt at hx,
471-
contrapose! h,
472-
rw [←nat.even_iff_not_odd] at h,
473-
rcases hx.eq_or_lt with hx | hx,
474-
{ rw [←neg_neg (1 : α), add_neg_eq_iff_eq_add, zero_add] at hx,
475-
simp only [hx, neg_one_geom_sum, h, if_true] },
476-
apply le_of_lt,
477-
simpa [h] using geom_sum_alternating_of_lt_neg_one hx hn },
492+
{ rw [or_iff_not_imp_left, ←not_le, ←nat.even_iff_not_odd],
493+
refine λ hn hx, h.not_le _,
494+
simpa [if_pos hn] using geom_sum_alternating_of_le_neg_one hx n },
478495
{ rintro (hn | hx'),
479496
{ exact hn.geom_sum_pos },
480-
rcases lt_trichotomy x 0 with hx | rfl | hx,
481-
{ exact (geom_sum_pos_and_lt_one hx hx' hn).1 },
482-
{ simp only [(zero_lt_one.trans hn).ne', zero_geom_sum, if_false, zero_lt_one] },
483-
{ exact geom_sum_pos hx (zero_lt_one.trans hn).ne' } }
497+
{ exact geom_sum_pos' hx' hn } }
484498
end
485499

486-
lemma geom_sum_eq_zero_iff_neg_one [linear_ordered_ring α] (hn : 1 < n) :
500+
lemma geom_sum_ne_zero [linear_ordered_ring α] (hx : x ≠ -1) (hn : n ≠ 0) :
501+
∑ i in range n, x ^ i ≠ 0 :=
502+
begin
503+
obtain _ | _ | n := n,
504+
{ cases hn rfl },
505+
{ simp },
506+
rw [ne.def, eq_neg_iff_add_eq_zero, ←ne.def] at hx,
507+
obtain h | h := hx.lt_or_lt,
508+
{ have := geom_sum_alternating_of_lt_neg_one h n.one_lt_succ_succ,
509+
split_ifs at this,
510+
{ exact this.ne },
511+
{ exact (zero_lt_one.trans this).ne' } },
512+
{ exact (geom_sum_pos' h n.succ.succ_ne_zero).ne' }
513+
end
514+
515+
lemma geom_sum_eq_zero_iff_neg_one [linear_ordered_ring α] (hn : n ≠ 0) :
487516
∑ i in range n, x ^ i = 0 ↔ x = -1 ∧ even n :=
488517
begin
489518
refine ⟨λ h, _, λ ⟨h, hn⟩, by simp only [h, hn, neg_one_geom_sum, if_true]⟩,
490519
contrapose! h,
491-
rcases eq_or_ne x (-1) with rfl | h,
520+
obtain rfl | hx := eq_or_ne x (-1),
492521
{ simp only [h rfl, neg_one_geom_sum, if_false, ne.def, not_false_iff, one_ne_zero] },
493-
rw [ne.def, eq_neg_iff_add_eq_zero, ←ne.def] at h,
494-
rcases h.lt_or_lt with h | h,
495-
{ have := geom_sum_alternating_of_lt_neg_one h hn,
496-
split_ifs at this,
497-
{ exact this.ne },
498-
{ exact (zero_lt_one.trans this).ne' } },
499-
apply ne_of_gt,
500-
rcases lt_trichotomy x 0 with h' | rfl | h',
501-
{ exact (geom_sum_pos_and_lt_one h' h hn).1 },
502-
{ simp only [(pos_of_gt hn).ne', zero_geom_sum, if_false, zero_lt_one] },
503-
{ exact geom_sum_pos h' (pos_of_gt hn).ne' }
522+
{ exact geom_sum_ne_zero hx hn }
504523
end
505524

506-
lemma geom_sum_neg_iff [linear_ordered_ring α] (hn : 1 < n) :
525+
lemma geom_sum_neg_iff [linear_ordered_ring α] (hn : n ≠ 0) :
507526
∑ i in range n, x ^ i < 0 ↔ even n ∧ x + 1 < 0 :=
508527
by rw [← not_iff_not, not_lt, le_iff_lt_or_eq, eq_comm,
509528
or_congr (geom_sum_pos_iff hn) (geom_sum_eq_zero_iff_neg_one hn), nat.odd_iff_not_even,

‎src/algebra/group_power/lemmas.lean‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -423,8 +423,8 @@ end
423423
lemma neg_one_pow_eq_pow_mod_two [ring R] {n : ℕ} : (-1 : R) ^ n = (-1) ^ (n % 2) :=
424424
by rw [← nat.mod_add_div n 2, pow_add, pow_mul]; simp [sq]
425425

426-
section ordered_semiring
427-
variables [ordered_semiring R] {a : R}
426+
section strict_ordered_semiring
427+
variables [strict_ordered_semiring R] {a : R}
428428

429429
/-- Bernoulli's inequality. This version works for semirings but requires
430430
additional hypotheses `0 ≤ a * a` and `0 ≤ (1 + a) * (1 + a)`. -/
@@ -461,7 +461,7 @@ lemma pow_le_of_le_one (h₀ : 0 ≤ a) (h₁ : a ≤ 1) {n : ℕ} (hn : n ≠ 0
461461

462462
lemma sq_le (h₀ : 0 ≤ a) (h₁ : a ≤ 1) : a ^ 2 ≤ a := pow_le_of_le_one h₀ h₁ two_ne_zero
463463

464-
end ordered_semiring
464+
end strict_ordered_semiring
465465

466466
section linear_ordered_semiring
467467

‎src/algebra/group_power/order.lean‎

Lines changed: 38 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -222,6 +222,15 @@ begin
222222
by { rw [pow_succ _ n], exact mul_le_mul_of_nonneg_left (ih (nat.succ_ne_zero k)) h2 }
223223
end
224224

225+
lemma pow_le_one : ∀ (n : ℕ) (h₀ : 0 ≤ a) (h₁ : a ≤ 1), a ^ n ≤ 1
226+
| 0 h₀ h₁ := (pow_zero a).le
227+
| (n + 1) h₀ h₁ := (pow_succ' a n).le.trans (mul_le_one (pow_le_one n h₀ h₁) h₀ h₁)
228+
229+
lemma pow_lt_one (h₀ : 0 ≤ a) (h₁ : a < 1) : ∀ {n : ℕ} (hn : n ≠ 0), a ^ n < 1
230+
| 0 h := (h rfl).elim
231+
| (n + 1) h :=
232+
by { rw pow_succ, exact mul_lt_one_of_nonneg_of_lt_one_left h₀ h₁ (pow_le_one _ h₀ h₁.le) }
233+
225234
theorem one_le_pow_of_one_le (H : 1 ≤ a) : ∀ (n : ℕ), 1 ≤ a ^ n
226235
| 0 := by rw [pow_zero]
227236
| (n+1) := by { rw pow_succ, simpa only [mul_one] using mul_le_mul H (one_le_pow_of_one_le n)
@@ -237,6 +246,29 @@ pow_mono ha h
237246
theorem le_self_pow (ha : 1 ≤ a) (h : m ≠ 0) : a ≤ a ^ m :=
238247
(pow_one a).symm.trans_le (pow_le_pow ha $ pos_iff_ne_zero.mpr h)
239248

249+
@[mono] lemma pow_le_pow_of_le_left {a b : R} (ha : 0 ≤ a) (hab : a ≤ b) : ∀ i : ℕ, a^i ≤ b^i
250+
| 0 := by simp
251+
| (k+1) := by { rw [pow_succ, pow_succ],
252+
exact mul_le_mul hab (pow_le_pow_of_le_left _) (pow_nonneg ha _) (le_trans ha hab) }
253+
254+
lemma one_lt_pow (ha : 1 < a) : ∀ {n : ℕ} (hn : n ≠ 0), 1 < a ^ n
255+
| 0 h := (h rfl).elim
256+
| (n + 1) h :=
257+
by { rw pow_succ, exact one_lt_mul_of_lt_of_le ha (one_le_pow_of_one_le ha.le _) }
258+
259+
end ordered_semiring
260+
261+
section strict_ordered_semiring
262+
variables [strict_ordered_semiring R] {a x y : R} {n m : ℕ}
263+
264+
lemma pow_lt_pow_of_lt_left (h : x < y) (hx : 0 ≤ x) : ∀ {n : ℕ}, 0 < n → x ^ n < y ^ n
265+
| 0 hn := hn.false.elim
266+
| (n + 1) _ := by simpa only [pow_succ'] using
267+
mul_lt_mul_of_le_of_le' (pow_le_pow_of_le_left hx h.le _) h (pow_pos (hx.trans_lt h) _) hx
268+
269+
lemma strict_mono_on_pow (hn : 0 < n) : strict_mono_on (λ x : R, x ^ n) (set.Ici 0) :=
270+
λ x hx y hy h, pow_lt_pow_of_lt_left h hx hn
271+
240272
lemma strict_mono_pow (h : 1 < a) : strict_mono (λ n : ℕ, a ^ n) :=
241273
have 0 < a := zero_le_one.trans_lt h,
242274
strict_mono_nat_of_lt_succ $ λ n, by simpa only [one_mul, pow_succ]
@@ -261,37 +293,12 @@ lemma pow_lt_pow_iff_of_lt_one (h₀ : 0 < a) (h₁ : a < 1) : a ^ m < a ^ n ↔
261293
lemma pow_lt_pow_of_lt_one (h : 0 < a) (ha : a < 1) {i j : ℕ} (hij : i < j) : a ^ j < a ^ i :=
262294
(pow_lt_pow_iff_of_lt_one h ha).2 hij
263295

264-
@[mono] lemma pow_le_pow_of_le_left {a b : R} (ha : 0 ≤ a) (hab : a ≤ b) : ∀ i : ℕ, a^i ≤ b^i
265-
| 0 := by simp
266-
| (k+1) := by { rw [pow_succ, pow_succ],
267-
exact mul_le_mul hab (pow_le_pow_of_le_left _) (pow_nonneg ha _) (le_trans ha hab) }
268-
269-
lemma pow_lt_pow_of_lt_left (h : x < y) (hx : 0 ≤ x) : ∀ {n : ℕ}, 0 < n → x ^ n < y ^ n
270-
| 0 hn := hn.false.elim
271-
| (n + 1) _ := by simpa only [pow_succ'] using
272-
mul_lt_mul' (pow_le_pow_of_le_left hx h.le _) h hx (pow_pos (hx.trans_lt h) _)
273-
274-
lemma pow_lt_one (h₀ : 0 ≤ a) (h₁ : a < 1) {n : ℕ} (hn : n ≠ 0) : a ^ n < 1 :=
275-
(one_pow n).subst (pow_lt_pow_of_lt_left h₁ h₀ (nat.pos_of_ne_zero hn))
276-
277-
lemma one_lt_pow (ha : 1 < a) {n : ℕ} (hn : n ≠ 0) : 1 < a ^ n :=
278-
pow_zero a ▸ pow_lt_pow ha (pos_iff_ne_zero.2 hn)
279-
280-
lemma pow_le_one : ∀ (n : ℕ) (h₀ : 0 ≤ a) (h₁ : a ≤ 1), a ^ n ≤ 1
281-
| 0 h₀ h₁ := (pow_zero a).le
282-
| (n + 1) h₀ h₁ := (pow_succ' a n).le.trans (mul_le_one (pow_le_one n h₀ h₁) h₀ h₁)
283-
284-
lemma strict_mono_on_pow (hn : 0 < n) : strict_mono_on (λ x : R, x ^ n) (set.Ici 0) :=
285-
λ x hx y hy h, pow_lt_pow_of_lt_left h hx hn
286-
287296
lemma sq_pos_of_pos (ha : 0 < a) : 0 < a ^ 2 := by { rw sq, exact mul_pos ha ha }
288297

289-
end ordered_semiring
298+
end strict_ordered_semiring
290299

291-
section ordered_ring
292-
variables [ordered_ring R] {a : R}
293-
294-
lemma sq_pos_of_neg (ha : a < 0) : 0 < a ^ 2 := by { rw sq, exact mul_pos_of_neg_of_neg ha ha }
300+
section strict_ordered_ring
301+
variables [strict_ordered_ring R] {a : R}
295302

296303
lemma pow_bit0_pos_of_neg (ha : a < 0) (n : ℕ) : 0 < a ^ bit0 n :=
297304
begin
@@ -305,7 +312,9 @@ begin
305312
exact mul_neg_of_neg_of_pos ha (pow_bit0_pos_of_neg ha n),
306313
end
307314

308-
end ordered_ring
315+
lemma sq_pos_of_neg (ha : a < 0) : 0 < a ^ 2 := pow_bit0_pos_of_neg ha _
316+
317+
end strict_ordered_ring
309318

310319
section linear_ordered_semiring
311320
variables [linear_ordered_semiring R] {a b : R}

‎src/algebra/ne_zero.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -62,7 +62,7 @@ instance bit0 [canonically_ordered_add_monoid M] [ne_zero x] : ne_zero (bit0 x)
6262
of_pos $ bit0_pos $ ne_zero.pos x
6363

6464
instance bit1 [canonically_ordered_comm_semiring M] [nontrivial M] : ne_zero (bit1 x) :=
65-
⟨mt (λ h, le_iff_exists_add'.2 ⟨_, h.symm⟩) canonically_ordered_comm_semiring.zero_lt_one.not_le⟩
65+
⟨mt (λ h, le_iff_exists_add'.2 ⟨_, h.symm⟩) zero_lt_one.not_le⟩
6666

6767
instance pow [monoid_with_zero M] [no_zero_divisors M] [ne_zero x] : ne_zero (x ^ n) :=
6868
⟨pow_ne_zero n out⟩

‎src/algebra/order/algebra.lean‎

Lines changed: 0 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -45,13 +45,3 @@ begin
4545
end
4646

4747
end ordered_algebra
48-
49-
section instances
50-
51-
variables {R : Type*} [linear_ordered_comm_ring R]
52-
53-
instance linear_ordered_comm_ring.to_ordered_smul : ordered_smul R R :=
54-
{ smul_lt_smul_of_pos := ordered_semiring.mul_lt_mul_of_pos_left,
55-
lt_of_smul_lt_smul_of_pos := λ a b c w₁ w₂, (mul_lt_mul_left w₂).mp w₁ }
56-
57-
end instances

0 commit comments

Comments
 (0)