From 233efbb56d8ebde1c8af3f029feeb40592895530 Mon Sep 17 00:00:00 2001 From: negiizhao Date: Thu, 15 Sep 2022 22:13:26 +0800 Subject: [PATCH 1/3] chore(algebra/order/monoid_lemmas_zero_lt): remove useless lemmas, use namespace `without_zero_le_one` The fourth part of #16449 There are still some useless lemmas which were simply ported from `algebra/order/monoid_lemmas`, this PR removes them. Also some lemmas have both assumptions like `1 < a` `0 < a`, this is because the file does not use type classes like `zero_le_one_class` currently. So I put these lemmas in the namespace `without_zero_le_one`. --- src/algebra/order/monoid_lemmas_zero_lt.lean | 278 ++++++------------- 1 file changed, 88 insertions(+), 190 deletions(-) diff --git a/src/algebra/order/monoid_lemmas_zero_lt.lean b/src/algebra/order/monoid_lemmas_zero_lt.lean index f0d03dda5612d..dc94d09f3239e 100644 --- a/src/algebra/order/monoid_lemmas_zero_lt.lean +++ b/src/algebra/order/monoid_lemmas_zero_lt.lean @@ -547,263 +547,161 @@ lemma mul_lt_iff_lt_one_left a * b < b ↔ a < 1 := iff.trans (by rw [one_mul]) (mul_lt_mul_right b0) -/-! Lemmas of the form `1 ≤ b → a ≤ a * b`. -/ +/-! Lemmas of the form `b ≤ 1` → `a * b ≤ a`. -/ -lemma mul_le_of_le_one_left [mul_pos_mono α] (hb : 0 ≤ b) (h : a ≤ 1) : a * b ≤ b := -by simpa only [one_mul] using mul_le_mul_of_nonneg_right h hb +lemma mul_le_of_le_one_right [pos_mul_mono α] (a0 : 0 ≤ a) (h : b ≤ 1) : a * b ≤ a := +by simpa only [mul_one] using mul_le_mul_of_nonneg_left h a0 -lemma le_mul_of_one_le_left [mul_pos_mono α] (hb : 0 ≤ b) (h : 1 ≤ a) : b ≤ a * b := -by simpa only [one_mul] using mul_le_mul_of_nonneg_right h hb +lemma le_mul_of_one_le_right [pos_mul_mono α] (a0 : 0 ≤ a) (h : 1 ≤ b) : a ≤ a * b := +by simpa only [mul_one] using mul_le_mul_of_nonneg_left h a0 -lemma mul_le_of_le_one_right [pos_mul_mono α] (ha : 0 ≤ a) (h : b ≤ 1) : a * b ≤ a := -by simpa only [mul_one] using mul_le_mul_of_nonneg_left h ha +lemma mul_le_of_le_one_left [mul_pos_mono α] (b0 : 0 ≤ b) (h : a ≤ 1) : a * b ≤ b := +by simpa only [one_mul] using mul_le_mul_of_nonneg_right h b0 -lemma le_mul_of_one_le_right [pos_mul_mono α] (ha : 0 ≤ a) (h : 1 ≤ b) : a ≤ a * b := -by simpa only [mul_one] using mul_le_mul_of_nonneg_left h ha +lemma le_mul_of_one_le_left [mul_pos_mono α] (b0 : 0 ≤ b) (h : 1 ≤ a) : b ≤ a * b := +by simpa only [one_mul] using mul_le_mul_of_nonneg_right h b0 -lemma mul_lt_of_lt_one_left [mul_pos_strict_mono α] (hb : 0 < b) (h : a < 1) : a * b < b := -by simpa only [one_mul] using mul_lt_mul_of_pos_right h hb +lemma mul_lt_of_lt_one_right [pos_mul_strict_mono α] (a0 : 0 < a) (h : b < 1) : a * b < a := +by simpa only [mul_one] using mul_lt_mul_of_pos_left h a0 -lemma lt_mul_of_one_lt_left [mul_pos_strict_mono α] (hb : 0 < b) (h : 1 < a) : b < a * b := -by simpa only [one_mul] using mul_lt_mul_of_pos_right h hb +lemma lt_mul_of_one_lt_right [pos_mul_strict_mono α] (a0 : 0 < a) (h : 1 < b) : a < a * b := +by simpa only [mul_one] using mul_lt_mul_of_pos_left h a0 -lemma mul_lt_of_lt_one_right [pos_mul_strict_mono α] (ha : 0 < a) (h : b < 1) : a * b < a := -by simpa only [mul_one] using mul_lt_mul_of_pos_left h ha +lemma mul_lt_of_lt_one_left [mul_pos_strict_mono α] (b0 : 0 < b) (h : a < 1) : a * b < b := +by simpa only [one_mul] using mul_lt_mul_of_pos_right h b0 -lemma lt_mul_of_one_lt_right [pos_mul_strict_mono α] (ha : 0 < a) (h : 1 < b) : a < a * b := -by simpa only [mul_one] using mul_lt_mul_of_pos_left h ha +lemma lt_mul_of_one_lt_left [mul_pos_strict_mono α] (b0 : 0 < b) (h : 1 < a) : b < a * b := +by simpa only [one_mul] using mul_lt_mul_of_pos_right h b0 /-! Lemmas of the form `b ≤ c → a ≤ 1 → b * a ≤ c`. -/ -/- Yaël: What's the point of these lemmas? They just chain an existing lemma with an assumption in -all possible ways, thereby artificially inflating the API and making the truly relevant lemmas hard -to find -/ - -lemma mul_le_of_le_of_le_one_of_nonneg [pos_mul_mono α] (h : b ≤ c) (ha : a ≤ 1) (hb : 0 ≤ b) : - b * a ≤ c := -(mul_le_of_le_one_right hb ha).trans h - -lemma mul_lt_of_le_of_lt_one_of_pos [pos_mul_strict_mono α] (bc : b ≤ c) (ha : a < 1) (b0 : 0 < b) : - b * a < c := -(mul_lt_of_lt_one_right b0 ha).trans_le bc - -lemma mul_lt_of_lt_of_le_one_of_nonneg [pos_mul_mono α] (h : b < c) (ha : a ≤ 1) (hb : 0 ≤ b) : - b * a < c := -(mul_le_of_le_one_right hb ha).trans_lt h /-- Assumes left covariance. -/ -lemma left.mul_le_one_of_le_of_le [pos_mul_mono α] (ha : a ≤ 1) (hb : b ≤ 1) (a0 : 0 ≤ a) : - a * b ≤ 1 := -mul_le_of_le_of_le_one_of_nonneg ha hb a0 +lemma mul_le_one_of_le_of_le_left [pos_mul_mono α] + (ha : a ≤ 1) (hb : b ≤ 1) (a0 : 0 ≤ a) : a * b ≤ 1 := +(mul_le_of_le_one_right a0 hb).trans ha /-- Assumes left covariance. -/ -lemma left.mul_lt_of_le_of_lt_one_of_pos [pos_mul_strict_mono α] +lemma mul_lt_one_of_le_of_lt_left [pos_mul_strict_mono α] (ha : a ≤ 1) (hb : b < 1) (a0 : 0 < a) : a * b < 1 := -mul_lt_of_le_of_lt_one_of_pos ha hb a0 +(mul_lt_of_lt_one_right a0 hb).trans_le ha /-- Assumes left covariance. -/ -lemma left.mul_lt_of_lt_of_le_one_of_nonneg [pos_mul_mono α] +lemma mul_lt_one_of_lt_of_le_left [pos_mul_mono α] (ha : a < 1) (hb : b ≤ 1) (a0 : 0 ≤ a) : a * b < 1 := -mul_lt_of_lt_of_le_one_of_nonneg ha hb a0 - -lemma mul_le_of_le_of_le_one' [pos_mul_mono α] [mul_pos_mono α] - (bc : b ≤ c) (ha : a ≤ 1) (a0 : 0 ≤ a) (c0 : 0 ≤ c) : b * a ≤ c := -(mul_le_mul_of_nonneg_right bc a0).trans $ mul_le_of_le_one_right c0 ha - -lemma mul_lt_of_lt_of_le_one' [pos_mul_mono α] [mul_pos_strict_mono α] - (bc : b < c) (ha : a ≤ 1) (a0 : 0 < a) (c0 : 0 ≤ c) : b * a < c := -(mul_lt_mul_of_pos_right bc a0).trans_le $ mul_le_of_le_one_right c0 ha - -lemma mul_lt_of_le_of_lt_one' [pos_mul_strict_mono α] [mul_pos_mono α] - (bc : b ≤ c) (ha : a < 1) (a0 : 0 ≤ a) (c0 : 0 < c) : b * a < c := -(mul_le_mul_of_nonneg_right bc a0).trans_lt $ mul_lt_of_lt_one_right c0 ha - -lemma mul_lt_of_lt_of_lt_one_of_pos [pos_mul_mono α] [mul_pos_strict_mono α] - (bc : b < c) (ha : a ≤ 1) (a0 : 0 < a) (c0 : 0 ≤ c) : b * a < c := -(mul_lt_mul_of_pos_right bc a0).trans_le $ mul_le_of_le_one_right c0 ha - -/-! Lemmas of the form `b ≤ c → 1 ≤ a → b ≤ c * a`. -/ - -lemma le_mul_of_le_of_one_le_of_nonneg [pos_mul_mono α] (h : b ≤ c) (ha : 1 ≤ a) (hc : 0 ≤ c) : - b ≤ c * a := -h.trans $ le_mul_of_one_le_right hc ha - -lemma lt_mul_of_le_of_one_lt_of_pos [pos_mul_strict_mono α] (bc : b ≤ c) (ha : 1 < a) (c0 : 0 < c) : - b < c * a := -bc.trans_lt $ lt_mul_of_one_lt_right c0 ha - -lemma lt_mul_of_lt_of_one_le_of_nonneg [pos_mul_mono α] (h : b < c) (ha : 1 ≤ a) (hc : 0 ≤ c) : - b < c * a := -h.trans_le $ le_mul_of_one_le_right hc ha +(mul_le_of_le_one_right a0 hb).trans_lt ha /-- Assumes left covariance. -/ -lemma left.one_le_mul_of_le_of_le [pos_mul_mono α] (ha : 1 ≤ a) (hb : 1 ≤ b) (a0 : 0 ≤ a) : - 1 ≤ a * b := -le_mul_of_le_of_one_le_of_nonneg ha hb a0 - -/-- Assumes left covariance. -/ -lemma left.one_lt_mul_of_le_of_lt_of_pos [pos_mul_strict_mono α] - (ha : 1 ≤ a) (hb : 1 < b) (a0 : 0 < a) : 1 < a * b := -lt_mul_of_le_of_one_lt_of_pos ha hb a0 - -/-- Assumes left covariance. -/ -lemma left.lt_mul_of_lt_of_one_le_of_nonneg [pos_mul_mono α] - (ha : 1 < a) (hb : 1 ≤ b) (a0 : 0 ≤ a) : 1 < a * b := -lt_mul_of_lt_of_one_le_of_nonneg ha hb a0 - -lemma le_mul_of_le_of_one_le' [pos_mul_mono α] [mul_pos_mono α] - (bc : b ≤ c) (ha : 1 ≤ a) (a0 : 0 ≤ a) (b0 : 0 ≤ b) : b ≤ c * a := -(le_mul_of_one_le_right b0 ha).trans $ mul_le_mul_of_nonneg_right bc a0 - -lemma lt_mul_of_le_of_one_lt' [pos_mul_strict_mono α] [mul_pos_mono α] - (bc : b ≤ c) (ha : 1 < a) (a0 : 0 ≤ a) (b0 : 0 < b) : b < c * a := -(lt_mul_of_one_lt_right b0 ha).trans_le $ mul_le_mul_of_nonneg_right bc a0 - -lemma lt_mul_of_lt_of_one_le' [pos_mul_mono α] [mul_pos_strict_mono α] - (bc : b < c) (ha : 1 ≤ a) (a0 : 0 < a) (b0 : 0 ≤ b) : b < c * a := -(le_mul_of_one_le_right b0 ha).trans_lt $ mul_lt_mul_of_pos_right bc a0 - -lemma lt_mul_of_lt_of_one_lt_of_pos [pos_mul_strict_mono α] [mul_pos_strict_mono α] - (bc : b < c) (ha : 1 < a) (a0 : 0 < a) (b0 : 0 < b) : b < c * a := -(lt_mul_of_one_lt_right b0 ha).trans $ mul_lt_mul_of_pos_right bc a0 +lemma mul_lt_one_of_lt_of_lt_left [pos_mul_strict_mono α] + (ha : a < 1) (hb : b < 1) (a0 : 0 < a) : a * b < 1 := +(mul_lt_of_lt_one_right a0 hb).trans ha /-! Lemmas of the form `a ≤ 1 → b ≤ c → a * b ≤ c`. -/ -lemma mul_le_of_le_one_of_le_of_nonneg [mul_pos_mono α] (ha : a ≤ 1) (h : b ≤ c) (hb : 0 ≤ b) : - a * b ≤ c := -(mul_le_of_le_one_left hb ha).trans h - -lemma mul_lt_of_lt_one_of_le_of_pos [mul_pos_strict_mono α] (ha : a < 1) (h : b ≤ c) (hb : 0 < b) : - a * b < c := -(mul_lt_of_lt_one_left hb ha).trans_le h - -lemma mul_lt_of_le_one_of_lt_of_nonneg [mul_pos_mono α] (ha : a ≤ 1) (h : b < c) (hb : 0 ≤ b) : - a * b < c := -(mul_le_of_le_one_left hb ha).trans_lt h +/-- Assumes right covariance. -/ +lemma mul_le_one_of_le_of_le_right [mul_pos_mono α] + (ha : a ≤ 1) (hb : b ≤ 1) (b0 : 0 ≤ b) : a * b ≤ 1 := +(mul_le_of_le_one_left b0 ha).trans hb /-- Assumes right covariance. -/ -lemma right.mul_lt_one_of_lt_of_le_of_pos [mul_pos_strict_mono α] +lemma mul_lt_one_of_lt_of_le_right [mul_pos_strict_mono α] (ha : a < 1) (hb : b ≤ 1) (b0 : 0 < b) : a * b < 1 := -mul_lt_of_lt_one_of_le_of_pos ha hb b0 +(mul_lt_of_lt_one_left b0 ha).trans_le hb /-- Assumes right covariance. -/ -lemma right.mul_lt_one_of_le_of_lt_of_nonneg [mul_pos_mono α] +lemma mul_lt_one_of_le_of_lt_right [mul_pos_mono α] (ha : a ≤ 1) (hb : b < 1) (b0 : 0 ≤ b) : a * b < 1 := -mul_lt_of_le_one_of_lt_of_nonneg ha hb b0 - -lemma mul_lt_of_lt_one_of_lt_of_pos [pos_mul_strict_mono α] [mul_pos_strict_mono α] - (ha : a < 1) (bc : b < c) (a0 : 0 < a) (c0 : 0 < c) : a * b < c := -(mul_lt_mul_of_pos_left bc a0).trans $ mul_lt_of_lt_one_left c0 ha +(mul_le_of_le_one_left b0 ha).trans_lt hb /-- Assumes right covariance. -/ -lemma right.mul_le_one_of_le_of_le [mul_pos_mono α] - (ha : a ≤ 1) (hb : b ≤ 1) (b0 : 0 ≤ b) : a * b ≤ 1 := -mul_le_of_le_one_of_le_of_nonneg ha hb b0 +lemma mul_lt_one_of_lt_of_lt_right [mul_pos_strict_mono α] + (ha : a < 1) (hb : b < 1) (b0 : 0 < b) : a * b < 1 := +(mul_lt_of_lt_one_left b0 ha).trans hb + +namespace without_zero_le_one -lemma mul_le_of_le_one_of_le' [pos_mul_mono α] [mul_pos_mono α] - (ha : a ≤ 1) (bc : b ≤ c) (a0 : 0 ≤ a) (c0 : 0 ≤ c) : a * b ≤ c := -(mul_le_mul_of_nonneg_left bc a0).trans $ mul_le_of_le_one_left c0 ha +/-! Lemmas of the form `b ≤ c → 1 ≤ a → b ≤ c * a`. -/ -lemma mul_lt_of_lt_one_of_le' [pos_mul_mono α] [mul_pos_strict_mono α] - (ha : a < 1) (bc : b ≤ c) (a0 : 0 ≤ a) (c0 : 0 < c) : a * b < c := -(mul_le_mul_of_nonneg_left bc a0).trans_lt $ mul_lt_of_lt_one_left c0 ha +/-- Assumes left covariance. -/ +lemma one_le_mul_of_le_of_le_left [pos_mul_mono α] + (ha : 1 ≤ a) (hb : 1 ≤ b) (a0 : 0 ≤ a) : 1 ≤ a * b := +ha.trans (le_mul_of_one_le_right a0 hb) -lemma mul_lt_of_le_one_of_lt' [pos_mul_strict_mono α] [mul_pos_mono α] - (ha : a ≤ 1) (bc : b < c) (a0 : 0 < a) (c0 : 0 ≤ c) : a * b < c := -(mul_lt_mul_of_pos_left bc a0).trans_le $ mul_le_of_le_one_left c0 ha +/-- Assumes left covariance. -/ +lemma one_lt_mul_of_le_of_lt_left [pos_mul_strict_mono α] + (ha : 1 ≤ a) (hb : 1 < b) (a0 : 0 < a) : 1 < a * b := +ha.trans_lt (lt_mul_of_one_lt_right a0 hb) -/-! Lemmas of the form `1 ≤ a → b ≤ c → b ≤ a * c`. -/ +/-- Assumes left covariance. -/ +lemma one_lt_mul_of_lt_of_le_left [pos_mul_mono α] + (ha : 1 < a) (hb : 1 ≤ b) (a0 : 0 ≤ a) : 1 < a * b := +ha.trans_le (le_mul_of_one_le_right a0 hb) -lemma lt_mul_of_one_lt_of_le_of_pos [mul_pos_strict_mono α] (ha : 1 < a) (h : b ≤ c) (hc : 0 < c) : - b < a * c := -h.trans_lt $ lt_mul_of_one_lt_left hc ha +/-- Assumes left covariance. -/ +lemma one_lt_mul_of_lt_of_lt_left [pos_mul_strict_mono α] + (ha : 1 < a) (hb : 1 < b) (a0 : 0 < a) : 1 < a * b := +ha.trans (lt_mul_of_one_lt_right a0 hb) -lemma lt_mul_of_one_le_of_lt_of_nonneg [mul_pos_mono α] (ha : 1 ≤ a) (h : b < c) (hc : 0 ≤ c) : - b < a * c := -h.trans_le $ le_mul_of_one_le_left hc ha +/-! Lemmas of the form `1 ≤ a → b ≤ c → b ≤ a * c`. -/ -lemma lt_mul_of_one_lt_of_lt_of_pos [mul_pos_strict_mono α] (ha : 1 < a) (h : b < c) (hc : 0 < c) : - b < a * c := -h.trans $ lt_mul_of_one_lt_left hc ha +/-- Assumes right covariance. -/ +lemma one_le_mul_of_le_of_le_right [mul_pos_mono α] + (ha : 1 ≤ a) (hb : 1 ≤ b) (b0 : 0 ≤ b) : 1 ≤ a * b := +hb.trans (le_mul_of_one_le_left b0 ha) /-- Assumes right covariance. -/ -lemma right.one_lt_mul_of_lt_of_le_of_pos [mul_pos_strict_mono α] +lemma one_lt_mul_of_lt_of_le_right [mul_pos_strict_mono α] (ha : 1 < a) (hb : 1 ≤ b) (b0 : 0 < b) : 1 < a * b := -lt_mul_of_one_lt_of_le_of_pos ha hb b0 +hb.trans_lt (lt_mul_of_one_lt_left b0 ha) /-- Assumes right covariance. -/ -lemma right.one_lt_mul_of_le_of_lt_of_nonneg [mul_pos_mono α] +lemma one_lt_mul_of_le_of_lt_right [mul_pos_mono α] (ha : 1 ≤ a) (hb : 1 < b) (b0 : 0 ≤ b) : 1 < a * b := -lt_mul_of_one_le_of_lt_of_nonneg ha hb b0 +hb.trans_le (le_mul_of_one_le_left b0 ha) /-- Assumes right covariance. -/ -lemma right.one_lt_mul_of_lt_of_lt [mul_pos_strict_mono α] +lemma one_lt_mul_of_lt_of_lt_right [mul_pos_strict_mono α] (ha : 1 < a) (hb : 1 < b) (b0 : 0 < b) : 1 < a * b := -lt_mul_of_one_lt_of_lt_of_pos ha hb b0 +hb.trans (lt_mul_of_one_lt_left b0 ha) -lemma lt_mul_of_one_lt_of_lt_of_nonneg [mul_pos_mono α] (ha : 1 ≤ a) (h : b < c) (hc : 0 ≤ c) : - b < a * c := -h.trans_le $ le_mul_of_one_le_left hc ha +end without_zero_le_one -lemma lt_of_mul_lt_of_one_le_of_nonneg_left [pos_mul_mono α] (h : a * b < c) (hle : 1 ≤ b) - (ha : 0 ≤ a) : - a < c := -(le_mul_of_one_le_right ha hle).trans_lt h +end preorder + +end mul_one_class -lemma lt_of_lt_mul_of_le_one_of_nonneg_left [pos_mul_mono α] (h : a < b * c) (hc : c ≤ 1) - (hb : 0 ≤ b) : - a < b := -h.trans_le $ mul_le_of_le_one_right hb hc +section mul_zero_one_class +variables [mul_zero_one_class α] -lemma lt_of_lt_mul_of_le_one_of_nonneg_right [mul_pos_mono α] (h : a < b * c) (hb : b ≤ 1) - (hc : 0 ≤ c) : - a < c := -h.trans_le $ mul_le_of_le_one_left hc hb +section preorder +variables [preorder α] -lemma le_mul_of_one_le_of_le_of_nonneg [mul_pos_mono α] (ha : 1 ≤ a) (bc : b ≤ c) (c0 : 0 ≤ c) : - b ≤ a * c := -bc.trans $ le_mul_of_one_le_left c0 ha +lemma left.zero_lt_one_of_pos [pos_mul_reflect_lt α] + (a0 : 0 < a) : (0 : α) < 1 := +lt_of_mul_lt_mul_left ((mul_zero _).le.trans_lt (a0.trans_le (mul_one _).ge)) a0.le -/-- Assumes right covariance. -/ -lemma right.one_le_mul_of_le_of_le [mul_pos_mono α] (ha : 1 ≤ a) (hb : 1 ≤ b) (b0 : 0 ≤ b) : - 1 ≤ a * b := -le_mul_of_one_le_of_le_of_nonneg ha hb b0 - -lemma le_of_mul_le_of_one_le_of_nonneg_left [pos_mul_mono α] (h : a * b ≤ c) (hb : 1 ≤ b) - (ha : 0 ≤ a) : - a ≤ c := -(le_mul_of_one_le_right ha hb).trans h - -lemma le_of_le_mul_of_le_one_of_nonneg_left [pos_mul_mono α] (h : a ≤ b * c) (hc : c ≤ 1) - (hb : 0 ≤ b) : - a ≤ b := -h.trans $ mul_le_of_le_one_right hb hc - -lemma le_of_mul_le_of_one_le_nonneg_right [mul_pos_mono α] (h : a * b ≤ c) (ha : 1 ≤ a) - (hb : 0 ≤ b) : - b ≤ c := -(le_mul_of_one_le_left hb ha).trans h +lemma right.zero_lt_one_of_pos [mul_pos_reflect_lt α] + (a0 : 0 < a) : (0 : α) < 1 := +lt_of_mul_lt_mul_right ((zero_mul _).le.trans_lt (a0.trans_le (one_mul _).ge)) a0.le -lemma le_of_le_mul_of_le_one_of_nonneg_right [mul_pos_mono α] (h : a ≤ b * c) (hb : b ≤ 1) - (hc : 0 ≤ c) : - a ≤ c := -h.trans $ mul_le_of_le_one_left hc hb +alias left.zero_lt_one_of_pos ← zero_lt_one_of_pos end preorder section linear_order variables [linear_order α] --- Yaël: What's the point of this lemma? If we have `0 * 0 = 0`, then we can just take `b = 0`. --- proven with `a0 : 0 ≤ a` as `exists_square_le` -lemma exists_square_le' [pos_mul_strict_mono α] (a0 : 0 < a) : ∃ (b : α), b * b ≤ a := +lemma exists_square_leₚ [pos_mul_strict_mono α] + (a0 : 0 ≤ a) : ∃ (b : α), b * b ≤ a := begin + rcases a0.eq_or_lt with rfl | a0, { exact ⟨0, by simp⟩, }, obtain ha | ha := lt_or_le a 1, { exact ⟨a, (mul_lt_of_lt_one_right a0 ha).le⟩ }, { exact ⟨1, by rwa mul_one⟩ } end end linear_order -end mul_one_class + +end mul_zero_one_class section cancel_monoid_with_zero From 0ba9c6c9730d491d69313c7c81226f3b86deee5f Mon Sep 17 00:00:00 2001 From: negiizhao Date: Fri, 16 Sep 2022 20:01:14 +0800 Subject: [PATCH 2/3] Update bernstein.lean --- src/analysis/special_functions/bernstein.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/analysis/special_functions/bernstein.lean b/src/analysis/special_functions/bernstein.lean index f7532b07c6960..4c8424fe410fe 100644 --- a/src/analysis/special_functions/bernstein.lean +++ b/src/analysis/special_functions/bernstein.lean @@ -296,10 +296,10 @@ begin : by conv_rhs { rw [mul_assoc, finset.mul_sum], simp only [←mul_assoc], } -- `bernstein.variance` and `x ∈ [0,1]` gives the uniform bound - ... = (2 * ∥f∥) * δ^(-2 : ℤ) * x * (1-x) / n + ... = (2 * ∥f∥) * δ^(-2 : ℤ) * (x * (1-x)) / n : by { rw variance npos, ring, } ... ≤ (2 * ∥f∥) * δ^(-2 : ℤ) / n - : (div_le_div_right npos).mpr $ - by refine mul_le_of_le_of_le_one' (mul_le_of_le_one_right w₂ _) _ _ w₂; unit_interval + : (div_le_div_right npos).mpr $ mul_le_of_le_one_right w₂ $ + by refine mul_le_one _ _ _; unit_interval ... < ε/2 : nh, } end From 5090a16a0608c8d30c7da846a67d17c93d4acb03 Mon Sep 17 00:00:00 2001 From: negiizhao Date: Mon, 10 Oct 2022 10:39:30 +0800 Subject: [PATCH 3/3] fix --- src/algebra/order/ring.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/algebra/order/ring.lean b/src/algebra/order/ring.lean index 5fb15cbba7f82..cf72fc294ab95 100644 --- a/src/algebra/order/ring.lean +++ b/src/algebra/order/ring.lean @@ -230,7 +230,7 @@ calc a + (2 + b) ≤ a + (a + a * b) : ... ≤ a * (2 + b) : by rw [mul_add, mul_two, add_assoc] lemma one_le_mul_of_one_le_of_one_le (ha : 1 ≤ a) (hb : 1 ≤ b) : (1 : α) ≤ a * b := -left.one_le_mul_of_le_of_le ha hb $ zero_le_one.trans ha +ha.trans (le_mul_of_one_le_right (zero_le_one.trans ha) hb) section monotone variables [preorder β] {f g : β → α}