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

Commit 57ac39b

Browse files
urkudurkud
committed
chore(data/real/ennreal): drop some lemmas (#18501)
Drop lemmas that are in fact more general lemmas applied to `ennreal`. For now, these lemmas are marked as `@[deprecated]` in leanprover-community/mathlib4#2388.
1 parent 03994e0 commit 57ac39b

39 files changed

Lines changed: 145 additions & 189 deletions

‎archive/100-theorems-list/30_ballot_problem.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -425,9 +425,9 @@ begin
425425
{ rw ballot_problem' q p qp,
426426
rw [ennreal.to_real_div, ← nat.cast_add, ← nat.cast_add, ennreal.to_real_nat,
427427
ennreal.to_real_sub_of_le, ennreal.to_real_nat, ennreal.to_real_nat],
428-
exacts [ennreal.coe_nat_le_coe_nat.2 qp.le, ennreal.nat_ne_top _] },
428+
exacts [nat.cast_le.2 qp.le, ennreal.nat_ne_top _] },
429429
rwa ennreal.to_real_eq_to_real (measure_lt_top _ _).ne at this,
430-
{ simp only [ne.def, ennreal.div_eq_top, tsub_eq_zero_iff_le, ennreal.coe_nat_le_coe_nat,
430+
{ simp only [ne.def, ennreal.div_eq_top, tsub_eq_zero_iff_le, nat.cast_le,
431431
not_le, add_eq_zero_iff, nat.cast_eq_zero, ennreal.add_eq_top, ennreal.nat_ne_top,
432432
or_self, not_false_iff, and_true],
433433
push_neg,

‎src/analysis/analytic/composition.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -444,8 +444,8 @@ begin
444444
/- This follows from the fact that the growth rate of `‖qₙ‖` and `‖pₙ‖` is at most geometric,
445445
giving a geometric bound on each `‖q.comp_along_composition p op‖`, together with the
446446
fact that there are `2^(n-1)` compositions of `n`, giving at most a geometric loss. -/
447-
rcases ennreal.lt_iff_exists_nnreal_btwn.1 (lt_min ennreal.zero_lt_one hq) with ⟨rq, rq_pos, hrq⟩,
448-
rcases ennreal.lt_iff_exists_nnreal_btwn.1 (lt_min ennreal.zero_lt_one hp) with ⟨rp, rp_pos, hrp⟩,
447+
rcases ennreal.lt_iff_exists_nnreal_btwn.1 (lt_min zero_lt_one hq) with ⟨rq, rq_pos, hrq⟩,
448+
rcases ennreal.lt_iff_exists_nnreal_btwn.1 (lt_min zero_lt_one hp) with ⟨rp, rp_pos, hrp⟩,
449449
simp only [lt_min_iff, ennreal.coe_lt_one_iff, ennreal.coe_pos] at hrp hrq rp_pos rq_pos,
450450
obtain ⟨Cq, hCq0, hCq⟩ : ∃ Cq > 0, ∀ n, ‖q n‖₊ * rq^n ≤ Cq :=
451451
q.nnnorm_mul_pow_le_of_lt_radius hrq.2,

‎src/analysis/normed_space/enorm.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -68,7 +68,7 @@ begin
6868
calc (‖c‖₊ : ℝ≥0∞) * e x = ‖c‖₊ * e (c⁻¹ • c • x) : by rw [inv_smul_smul₀ hc]
6969
... ≤ ‖c‖₊ * (‖c⁻¹‖₊ * e (c • x)) : _
7070
... = e (c • x) : _,
71-
{ exact ennreal.mul_le_mul le_rfl (e.map_smul_le' _ _) },
71+
{ exact mul_le_mul_left' (e.map_smul_le' _ _) _ },
7272
{ rw [← mul_assoc, nnnorm_inv, ennreal.coe_inv,
7373
ennreal.mul_inv_cancel _ ennreal.coe_ne_top, one_mul]; simp [hc] }
7474
end

‎src/analysis/normed_space/lp_space.lean‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -610,7 +610,7 @@ end
610610

611611
instance [fact (1 ≤ p)] : normed_space 𝕜 (lp E p) :=
612612
{ norm_smul_le := λ c f, begin
613-
have hp : 0 < p := ennreal.zero_lt_one.trans_le (fact.out _),
613+
have hp : 0 < p := zero_lt_one.trans_le (fact.out _),
614614
simp [norm_const_smul hp.ne']
615615
end }
616616

@@ -944,7 +944,7 @@ by linarith [lp.norm_sub_norm_compl_sub_single hp f s]
944944
protected lemma has_sum_single [fact (1 ≤ p)] (hp : p ≠ ⊤) (f : lp E p) :
945945
has_sum (λ i : α, lp.single p i (f i : E i)) f :=
946946
begin
947-
have hp₀ : 0 < p := ennreal.zero_lt_one.trans_le (fact.out _),
947+
have hp₀ : 0 < p := zero_lt_one.trans_le (fact.out _),
948948
have hp' : 0 < p.to_real := ennreal.to_real_pos hp₀.ne' hp,
949949
have := lp.has_sum_norm hp' f,
950950
rw [has_sum, metric.tendsto_nhds] at this ⊢,
@@ -975,7 +975,7 @@ open_locale topology uniformity
975975
/-- The coercion from `lp E p` to `Π i, E i` is uniformly continuous. -/
976976
lemma uniform_continuous_coe [_i : fact (1 ≤ p)] : uniform_continuous (coe : lp E p → Π i, E i) :=
977977
begin
978-
have hp : p ≠ 0 := (ennreal.zero_lt_one.trans_le _i.elim).ne',
978+
have hp : p ≠ 0 := (zero_lt_one.trans_le _i.elim).ne',
979979
rw uniform_continuous_pi,
980980
intros i,
981981
rw normed_add_comm_group.uniformity_basis_dist.uniform_continuous_iff
@@ -1008,7 +1008,7 @@ lemma sum_rpow_le_of_tendsto (hp : p ≠ ∞) {C : ℝ} {F : ι → lp E p} (hCF
10081008
{f : Π a, E a} (hf : tendsto (id (λ i, F i) : ι → Π a, E a) l (𝓝 f)) (s : finset α) :
10091009
∑ (i : α) in s, ‖f i‖ ^ p.to_real ≤ C ^ p.to_real :=
10101010
begin
1011-
have hp' : p ≠ 0 := (ennreal.zero_lt_one.trans_le _i.elim).ne',
1011+
have hp' : p ≠ 0 := (zero_lt_one.trans_le _i.elim).ne',
10121012
have hp'' : 0 < p.to_real := ennreal.to_real_pos hp' hp,
10131013
let G : (Π a, E a) → ℝ := λ f, ∑ a in s, ‖f a‖ ^ p.to_real,
10141014
have hG : continuous G,
@@ -1034,7 +1034,7 @@ begin
10341034
unfreezingI { rcases eq_top_or_lt_top p with rfl | hp },
10351035
{ apply norm_le_of_forall_le hC,
10361036
exact norm_apply_le_of_tendsto hCF hf, },
1037-
{ have : 0 < p := ennreal.zero_lt_one.trans_le _i.elim,
1037+
{ have : 0 < p := zero_lt_one.trans_le _i.elim,
10381038
have hp' : 0 < p.to_real := ennreal.to_real_pos this.ne' hp.ne,
10391039
apply norm_le_of_forall_sum_le hp' hC,
10401040
exact sum_rpow_le_of_tendsto hp.ne hCF hf, }

‎src/analysis/special_functions/pow.lean‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1941,7 +1941,7 @@ end
19411941
lemma rpow_pos_of_nonneg {p : ℝ} {x : ℝ≥0∞} (hx_pos : 0 < x) (hp_nonneg : 0 ≤ p) : 0 < x^p :=
19421942
begin
19431943
by_cases hp_zero : p = 0,
1944-
{ simp [hp_zero, ennreal.zero_lt_one], },
1944+
{ simp [hp_zero, zero_lt_one], },
19451945
{ rw ←ne.def at hp_zero,
19461946
have hp_pos := lt_of_le_of_ne hp_nonneg hp_zero.symm,
19471947
rw ←zero_rpow_of_pos hp_pos, exact rpow_lt_rpow hx_pos hp_pos, },
@@ -1972,7 +1972,7 @@ end
19721972
lemma rpow_lt_one_of_one_lt_of_neg {x : ℝ≥0∞} {z : ℝ} (hx : 1 < x) (hz : z < 0) : x^z < 1 :=
19731973
begin
19741974
cases x,
1975-
{ simp [top_rpow_of_neg hz, ennreal.zero_lt_one] },
1975+
{ simp [top_rpow_of_neg hz, zero_lt_one] },
19761976
{ simp only [some_eq_coe, one_lt_coe_iff] at hx,
19771977
simp [coe_rpow_of_ne_zero (ne_of_gt (lt_trans zero_lt_one hx)),
19781978
nnreal.rpow_lt_one_of_one_lt_of_neg hx hz] },
@@ -1981,7 +1981,7 @@ end
19811981
lemma rpow_le_one_of_one_le_of_neg {x : ℝ≥0∞} {z : ℝ} (hx : 1 ≤ x) (hz : z < 0) : x^z ≤ 1 :=
19821982
begin
19831983
cases x,
1984-
{ simp [top_rpow_of_neg hz, ennreal.zero_lt_one] },
1984+
{ simp [top_rpow_of_neg hz, zero_lt_one] },
19851985
{ simp only [one_le_coe_iff, some_eq_coe] at hx,
19861986
simp [coe_rpow_of_ne_zero (ne_of_gt (lt_of_lt_of_le zero_lt_one hx)),
19871987
nnreal.rpow_le_one_of_one_le_of_nonpos hx (le_of_lt hz)] },

‎src/analysis/specific_limits/basic.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -506,7 +506,7 @@ begin
506506
refine ⟨λ i, δ' i / max 1 (w i), λ i, div_pos (Hpos _) (this i), _⟩,
507507
refine lt_of_le_of_lt (ennreal.tsum_le_tsum $ λ i, _) Hsum,
508508
rw [coe_div (this i).ne'],
509-
refine mul_le_of_le_div' (ennreal.mul_le_mul le_rfl $ ennreal.inv_le_inv.2 _),
509+
refine mul_le_of_le_div' (mul_le_mul_left' (ennreal.inv_le_inv.2 _) _),
510510
exact coe_le_coe.2 (le_max_right _ _)
511511
end
512512

‎src/data/real/ennreal.lean‎

Lines changed: 18 additions & 54 deletions
Original file line numberDiff line numberDiff line change
@@ -80,7 +80,7 @@ variables {α : Type*} {β : Type*}
8080
semilattice_sup, distrib_lattice, order_bot, bounded_order,
8181
canonically_ordered_comm_semiring, complete_linear_order, densely_ordered, nontrivial,
8282
canonically_linear_ordered_add_monoid, has_sub, has_ordered_sub,
83-
linear_ordered_add_comm_monoid_with_top]]
83+
linear_ordered_add_comm_monoid_with_top, char_zero]]
8484
def ennreal := with_top ℝ≥0
8585

8686
localized "notation (name := ennreal) `ℝ≥0∞` := ennreal" in ennreal
@@ -222,7 +222,6 @@ lemma coe_mono : monotone (coe : ℝ≥0 → ℝ≥0∞) := λ _ _, coe_le_coe.2
222222
@[simp, norm_cast] lemma zero_eq_coe : 0 = (↑r : ℝ≥0∞) ↔ 0 = r := coe_eq_coe
223223
@[simp, norm_cast] lemma coe_eq_one : (↑r : ℝ≥0∞) = 1 ↔ r = 1 := coe_eq_coe
224224
@[simp, norm_cast] lemma one_eq_coe : 1 = (↑r : ℝ≥0∞) ↔ 1 = r := coe_eq_coe
225-
@[simp] lemma coe_nonneg : 0 ≤ (↑r : ℝ≥0∞) := coe_le_coe.2 $ zero_le _
226225
@[simp, norm_cast] lemma coe_pos : 0 < (↑r : ℝ≥0∞) ↔ 0 < r := coe_lt_coe
227226
lemma coe_ne_zero : (r : ℝ≥0∞) ≠ 0 ↔ r ≠ 0 := not_congr coe_eq_coe
228227

@@ -255,12 +254,9 @@ lemma to_real_eq_to_real_iff' {x y : ℝ≥0∞} (hx : x ≠ ⊤) (hy : y ≠
255254
x.to_real = y.to_real ↔ x = y :=
256255
by simp only [ennreal.to_real, nnreal.coe_eq, to_nnreal_eq_to_nnreal_iff' hx hy]
257256

258-
protected lemma zero_lt_one : 0 < (1 : ℝ≥0∞) := zero_lt_one
259-
260257
@[simp] lemma one_lt_two : (1 : ℝ≥0∞) < 2 :=
261258
coe_one ▸ coe_two ▸ by exact_mod_cast (one_lt_two : 1 < 2)
262-
@[simp] lemma zero_lt_two : (0 : ℝ≥0∞) < 2 := lt_trans zero_lt_one one_lt_two
263-
lemma two_ne_zero : (2 : ℝ≥0∞) ≠ 0 := (ne_of_lt zero_lt_two).symm
259+
264260
lemma two_ne_top : (2 : ℝ≥0∞) ≠ ∞ := coe_two ▸ coe_ne_top
265261

266262
/-- `(1 : ℝ≥0∞) ≤ 1`, recorded as a `fact` for use with `Lp` spaces. -/
@@ -301,9 +297,6 @@ lemma supr_ennreal {α : Type*} [complete_lattice α] {f : ℝ≥0∞ → α} :
301297
(⨆ n, f n) = (⨆ n : ℝ≥0, f n) ⊔ f ∞ :=
302298
@infi_ennreal αᵒᵈ _ _
303299

304-
@[simp] lemma add_top : a + ∞ = ∞ := add_top _
305-
@[simp] lemma top_add : ∞ + a = ∞ := top_add _
306-
307300
/-- Coercion `ℝ≥0 → ℝ≥0∞` as a `ring_hom`. -/
308301
def of_nnreal_hom : ℝ≥0 →+* ℝ≥0∞ :=
309302
⟨coe, coe_one, λ _ _, coe_mul, coe_zero, λ _ _, coe_add⟩
@@ -486,21 +479,6 @@ end
486479
↑(s.sup f) = s.sup (λ x, (f x : ℝ≥0∞)) :=
487480
finset.comp_sup_eq_sup_comp_of_is_total _ coe_mono rfl
488481

489-
lemma pow_le_pow {n m : ℕ} (ha : 1 ≤ a) (h : n ≤ m) : a ^ n ≤ a ^ m :=
490-
begin
491-
cases a,
492-
{ cases m,
493-
{ rw eq_bot_iff.mpr h,
494-
exact le_rfl },
495-
{ rw [none_eq_top, top_pow (nat.succ_pos m)],
496-
exact le_top } },
497-
{ rw [some_eq_coe, ← coe_pow, ← coe_pow, coe_le_coe],
498-
exact pow_le_pow (by simpa using ha) h }
499-
end
500-
501-
lemma one_le_pow_of_one_le (ha : 1 ≤ a) (n : ℕ) : 1 ≤ a ^ n :=
502-
by simpa using pow_le_pow ha (zero_le n)
503-
504482
@[simp] lemma max_eq_zero_iff : max a b = 0 ↔ a = 0 ∧ b = 0 :=
505483
by simp only [nonpos_iff_eq_zero.symm, max_le_iff]
506484

@@ -592,15 +570,11 @@ begin
592570
exact tsub_add_cancel_of_le ad.le
593571
end
594572

595-
lemma coe_nat_lt_coe {n : ℕ} : (n : ℝ≥0∞) < r ↔ ↑n < r := ennreal.coe_nat n ▸ coe_lt_coe
596-
lemma coe_lt_coe_nat {n : ℕ} : (r : ℝ≥0∞) < n ↔ r < n := ennreal.coe_nat n ▸ coe_lt_coe
597-
@[simp, norm_cast] lemma coe_nat_lt_coe_nat {m n : ℕ} : (m : ℝ≥0∞) < n ↔ m < n :=
598-
ennreal.coe_nat n ▸ coe_nat_lt_coe.trans nat.cast_lt
599-
lemma coe_nat_mono : strict_mono (coe : ℕ → ℝ≥0∞) := λ _ _, coe_nat_lt_coe_nat.2
600-
@[simp, norm_cast] lemma coe_nat_le_coe_nat {m n : ℕ} : (m : ℝ≥0∞) ≤ n ↔ m ≤ n :=
601-
coe_nat_mono.le_iff_le
573+
@[simp, norm_cast] lemma coe_nat_lt_coe {n : ℕ} : (n : ℝ≥0∞) < r ↔ ↑n < r :=
574+
ennreal.coe_nat n ▸ coe_lt_coe
602575

603-
instance : char_zero ℝ≥0∞ := ⟨coe_nat_mono.injective⟩
576+
@[simp, norm_cast] lemma coe_lt_coe_nat {n : ℕ} : (r : ℝ≥0∞) < n ↔ r < n :=
577+
ennreal.coe_nat n ▸ coe_lt_coe
604578

605579
protected lemma exists_nat_gt {r : ℝ≥0∞} (h : r ≠ ∞) : ∃n:ℕ, r < n :=
606580
begin
@@ -674,9 +648,6 @@ section complete_lattice
674648
lemma coe_Sup {s : set ℝ≥0} : bdd_above s → (↑(Sup s) : ℝ≥0∞) = (⨆a∈s, ↑a) := with_top.coe_Sup
675649
lemma coe_Inf {s : set ℝ≥0} : s.nonempty → (↑(Inf s) : ℝ≥0∞) = (⨅a∈s, ↑a) := with_top.coe_Inf
676650

677-
@[simp] lemma top_mem_upper_bounds {s : set ℝ≥0∞} : ∞ ∈ upper_bounds s :=
678-
assume x hx, le_top
679-
680651
lemma coe_mem_upper_bounds {s : set ℝ≥0} :
681652
↑r ∈ upper_bounds ((coe : ℝ≥0 → ℝ≥0∞) '' s) ↔ r ∈ upper_bounds s :=
682653
by simp [upper_bounds, ball_image_iff, -mem_image, *] {contextual := tt}
@@ -685,9 +656,6 @@ end complete_lattice
685656

686657
section mul
687658

688-
@[mono] lemma mul_le_mul : a ≤ b → c ≤ d → a * c ≤ b * d :=
689-
mul_le_mul'
690-
691659
@[mono] lemma mul_lt_mul (ac : a < c) (bd : b < d) : a * b < c * d :=
692660
begin
693661
rcases lt_iff_exists_nnreal_btwn.1 ac with ⟨a', aa', a'c⟩,
@@ -698,12 +666,14 @@ begin
698666
calc ↑(a * b) < ↑(a' * b') :
699667
coe_lt_coe.2 (mul_lt_mul' aa'.le bb' (zero_le _) ((zero_le a).trans_lt aa'))
700668
... = ↑a' * ↑b' : coe_mul
701-
... ≤ c * d : mul_le_mul a'c.le b'd.le
669+
... ≤ c * d : mul_le_mul' a'c.le b'd.le
702670
end
703671

704-
lemma mul_left_mono : monotone ((*) a) := λ b c, mul_le_mul le_rfl
672+
-- TODO: generalize to `covariant_class α α (*) (≤)`
673+
lemma mul_left_mono : monotone ((*) a) := λ b c, mul_le_mul' le_rfl
705674

706-
lemma mul_right_mono : monotone (λ x, x * a) := λ b c h, mul_le_mul h le_rfl
675+
-- TODO: generalize to `covariant_class α α (swap (*)) (≤)`
676+
lemma mul_right_mono : monotone (λ x, x * a) := λ b c h, mul_le_mul' h le_rfl
707677

708678
lemma pow_strict_mono {n : ℕ} (hn : n ≠ 0) : strict_mono (λ (x : ℝ≥0∞), x^n) :=
709679
begin
@@ -727,7 +697,7 @@ begin
727697
intros x y h,
728698
contrapose! h,
729699
simpa only [← mul_assoc, ← coe_mul, inv_mul_cancel h0, coe_one, one_mul]
730-
using mul_le_mul' (le_refl ↑a⁻¹) h
700+
using mul_le_mul_left' h (↑a⁻¹)
731701
end
732702

733703
lemma mul_eq_mul_left (h₀ : a ≠ 0) (hinf : a ≠ ∞) : a * b = a * c ↔ b = c :=
@@ -974,7 +944,7 @@ lemma bit0_injective : function.injective (bit0 : ℝ≥0∞ → ℝ≥0∞) :=
974944
@[simp] lemma bit0_inj : bit0 a = bit0 b ↔ a = b := bit0_injective.eq_iff
975945

976946
@[simp] lemma bit0_eq_zero_iff : bit0 a = 0 ↔ a = 0 := bit0_injective.eq_iff' bit0_zero
977-
@[simp] lemma bit0_top : bit0 ∞ = ∞ := add_top
947+
@[simp] lemma bit0_top : bit0 ∞ = ∞ := add_top _
978948
@[simp] lemma bit0_eq_top_iff : bit0 a = ∞ ↔ a = ∞ := bit0_injective.eq_iff' bit0_top
979949

980950
@[mono] lemma bit1_strict_mono : strict_mono (bit1 : ℝ≥0∞ → ℝ≥0∞) :=
@@ -1151,12 +1121,6 @@ def _root_.order_iso.inv_ennreal : ℝ≥0∞ ≃o ℝ≥0∞ᵒᵈ :=
11511121
lemma _root_.order_iso.inv_ennreal_symm_apply :
11521122
order_iso.inv_ennreal.symm a = (order_dual.of_dual a)⁻¹ := rfl
11531123

1154-
protected lemma pow_le_pow_of_le_one {n m : ℕ} (ha : a ≤ 1) (h : n ≤ m) : a ^ m ≤ a ^ n :=
1155-
begin
1156-
rw [←inv_inv a, ← ennreal.inv_pow, ← @ennreal.inv_pow a⁻¹, ennreal.inv_le_inv],
1157-
exact pow_le_pow (ennreal.one_le_inv.2 ha) h
1158-
end
1159-
11601124
@[simp] lemma div_top : a / ∞ = 0 := by rw [div_eq_mul_inv, inv_top, mul_zero]
11611125

11621126
@[simp] lemma top_div_coe : ∞ / p = ∞ := by simp [div_eq_mul_inv, top_mul]
@@ -1176,7 +1140,7 @@ lemma div_eq_top : a / b = ∞ ↔ (a ≠ 0 ∧ b = 0) ∨ (a = ∞ ∧ b ≠
11761140
by simp [div_eq_mul_inv, ennreal.mul_eq_top]
11771141

11781142
protected lemma le_div_iff_mul_le (h0 : b ≠ 0 ∨ c ≠ 0) (ht : b ≠ ∞ ∨ c ≠ ∞) :
1179-
a ≤ c / b ↔ a * b ≤ c :=
1143+
a ≤ c / b ↔ a * b ≤ c :=
11801144
begin
11811145
induction b using with_top.rec_top_coe,
11821146
{ lift c to ℝ≥0 using ht.neg_resolve_left rfl,
@@ -1239,7 +1203,7 @@ end
12391203
by rw [← one_div, ennreal.le_div_iff_mul_le]; { right, simp }
12401204

12411205
protected lemma div_le_div (hab : a ≤ b) (hdc : d ≤ c) : a / c ≤ b / d :=
1242-
div_eq_mul_inv b d ▸ div_eq_mul_inv a c ▸ ennreal.mul_le_mul hab (ennreal.inv_le_inv.mpr hdc)
1206+
div_eq_mul_inv b d ▸ div_eq_mul_inv a c ▸ mul_le_mul' hab (ennreal.inv_le_inv.mpr hdc)
12431207

12441208
protected lemma div_le_div_left (h : a ≤ b) (c : ℝ≥0∞) : c / b ≤ c / a :=
12451209
ennreal.div_le_div le_rfl h
@@ -1389,8 +1353,8 @@ lemma exists_nat_pos_mul_gt (ha : a ≠ 0) (hb : b ≠ ∞) :
13891353
begin
13901354
have : b / a ≠ ∞, from mul_ne_top hb (inv_ne_top.2 ha),
13911355
refine (ennreal.exists_nat_gt this).imp (λ n hn, _),
1392-
have : ↑0 < (n : ℝ≥0∞), from lt_of_le_of_lt (by simp) hn,
1393-
refine ⟨coe_nat_lt_coe_nat.1 this, _⟩,
1356+
have : 0 < (n : ℝ≥0∞), from lt_of_le_of_lt (zero_le _) hn,
1357+
refine ⟨nat.cast_pos.1 this, _⟩,
13941358
rwa [← ennreal.div_lt_iff (or.inl ha) (or.inr hb)]
13951359
end
13961360

@@ -1504,7 +1468,7 @@ begin
15041468
exact lt_of_lt_of_le (int.neg_succ_lt_zero _) (int.of_nat_nonneg _) },
15051469
{ simp only [zpow_neg_succ_of_nat, int.of_nat_eq_coe, zpow_coe_nat],
15061470
refine (ennreal.inv_le_one.2 _).trans _;
1507-
exact ennreal.one_le_pow_of_one_le hx _, },
1471+
exact one_le_pow_of_one_le' hx _, },
15081472
{ simp only [zpow_neg_succ_of_nat, ennreal.inv_le_inv],
15091473
apply pow_le_pow hx,
15101474
simpa only [←int.coe_nat_le_coe_nat_iff, neg_le_neg_iff, int.coe_nat_add, int.coe_nat_one,

‎src/measure_theory/covering/besicovitch.lean‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -565,7 +565,7 @@ begin
565565
apply (ennreal.mul_lt_mul_left hμs.ne' (measure_lt_top μ s).ne).2,
566566
rw ennreal.inv_lt_inv,
567567
conv_lhs {rw ← add_zero (N : ℝ≥0∞) },
568-
exact ennreal.add_lt_add_left (ennreal.nat_ne_top N) ennreal.zero_lt_one },
568+
exact ennreal.add_lt_add_left (ennreal.nat_ne_top N) zero_lt_one },
569569
have B : μ (o ∩ v i) = ∑' (x : u i), μ (o ∩ closed_ball x (r x)),
570570
{ have : o ∩ v i = ⋃ (x : s) (hx : x ∈ u i), o ∩ closed_ball x (r x), by simp only [inter_Union],
571571
rw [this, measure_bUnion (u_count i)],
@@ -750,13 +750,13 @@ begin
750750
≤ (N/(N+1)) * μ (s \ ⋃ (p : α × ℝ) (hp : p ∈ u n), closed_ball p.fst p.snd) :
751751
by { rw u_succ, exact (hF (u n) (Pu n)).2.2 }
752752
... ≤ (N/(N+1))^n.succ * μ s :
753-
by { rw [pow_succ, mul_assoc], exact ennreal.mul_le_mul le_rfl IH } },
753+
by { rw [pow_succ, mul_assoc], exact mul_le_mul_left' IH _ } },
754754
have C : tendsto (λ (n : ℕ), ((N : ℝ≥0∞)/(N+1))^n * μ s) at_top (𝓝 (0 * μ s)),
755755
{ apply ennreal.tendsto.mul_const _ (or.inr (measure_lt_top μ s).ne),
756756
apply ennreal.tendsto_pow_at_top_nhds_0_of_lt_1,
757757
rw [ennreal.div_lt_iff, one_mul],
758758
{ conv_lhs {rw ← add_zero (N : ℝ≥0∞) },
759-
exact ennreal.add_lt_add_left (ennreal.nat_ne_top N) ennreal.zero_lt_one },
759+
exact ennreal.add_lt_add_left (ennreal.nat_ne_top N) zero_lt_one },
760760
{ simp only [true_or, add_eq_zero_iff, ne.def, not_false_iff, one_ne_zero, and_false] },
761761
{ simp only [ennreal.nat_ne_top, ne.def, not_false_iff, or_true] } },
762762
rw zero_mul at C,

‎src/measure_theory/covering/differentiation.lean‎

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -178,14 +178,14 @@ begin
178178
rw [ennreal.mul_inv_cancel (ennreal.coe_pos.2 εpos).ne' ennreal.coe_ne_top, one_mul],
179179
end
180180
... ≤ ε⁻¹ * ρ (s ∩ o) : begin
181-
apply ennreal.mul_le_mul le_rfl,
181+
refine mul_le_mul_left' _ _,
182182
refine v.measure_le_of_frequently_le ρ ((measure.absolutely_continuous.refl μ).smul ε) _ _,
183183
assume x hx,
184184
rw hs at hx,
185185
simp only [mem_inter_iff, not_lt, not_eventually, mem_set_of_eq] at hx,
186186
exact hx.1
187187
end
188-
... ≤ ε⁻¹ * ρ o : ennreal.mul_le_mul le_rfl (measure_mono (inter_subset_right _ _))
188+
... ≤ ε⁻¹ * ρ o : mul_le_mul_left' (measure_mono (inter_subset_right _ _)) _
189189
... = 0 : by rw [ρo, mul_zero] },
190190
obtain ⟨u, u_anti, u_pos, u_lim⟩ :
191191
∃ (u : ℕ → ℝ≥0), strict_anti u ∧ (∀ (n : ℕ), 0 < u n) ∧ tendsto u at_top (𝓝 0) :=
@@ -202,7 +202,7 @@ begin
202202
filter_upwards [hx n, h'x, v.eventually_measure_lt_top x],
203203
assume a ha μa_pos μa_lt_top,
204204
rw ennreal.div_lt_iff (or.inl μa_pos.ne') (or.inl μa_lt_top.ne),
205-
exact ha.trans_le (ennreal.mul_le_mul ((ennreal.coe_le_coe.2 hn.le).trans w_lt.le) le_rfl)
205+
exact ha.trans_le (mul_le_mul_right' ((ennreal.coe_le_coe.2 hn.le).trans w_lt.le) _)
206206
end
207207

208208
section absolutely_continuous
@@ -453,7 +453,7 @@ begin
453453
... ≤ p * μ (s ∩ t) + 0 :
454454
add_le_add H ((measure_mono (inter_subset_right _ _)).trans (hρ A).le)
455455
... ≤ p * μ s :
456-
by { rw add_zero, exact ennreal.mul_le_mul le_rfl (measure_mono (inter_subset_left _ _)) },
456+
by { rw add_zero, exact mul_le_mul_left' (measure_mono (inter_subset_left _ _)) _ },
457457
refine v.measure_le_of_frequently_le _ hρ _ (λ x hx, _),
458458
have I : ∀ᶠ (b : set α) in v.filter_at x, ρ b / μ b < p := (tendsto_order.1 hx.2).2 _ (h hx.1),
459459
apply I.frequently.mono (λ a ha, _),
@@ -477,7 +477,7 @@ begin
477477
... ≤ ρ (s ∩ t) + q * μ tᶜ : begin
478478
apply add_le_add H,
479479
rw [coe_nnreal_smul_apply],
480-
exact ennreal.mul_le_mul le_rfl (measure_mono (inter_subset_right _ _)),
480+
exact mul_le_mul_left' (measure_mono (inter_subset_right _ _)) _,
481481
end
482482
... ≤ ρ s :
483483
by { rw [A, mul_zero, add_zero], exact measure_mono (inter_subset_left _ _) },
@@ -584,7 +584,7 @@ begin
584584
abel,
585585
end
586586
... ≤ t^2 * ρ (s ∩ f ⁻¹' I) : begin
587-
apply ennreal.mul_le_mul le_rfl _,
587+
refine mul_le_mul_left' _ _,
588588
rw ← ennreal.coe_zpow (zero_lt_one.trans ht).ne',
589589
apply v.mul_measure_le_of_subset_lt_lim_ratio_meas hρ,
590590
assume x hx,
@@ -646,7 +646,7 @@ begin
646646
... ≤ ∫⁻ x in s ∩ f⁻¹' I, t * f x ∂μ : begin
647647
apply lintegral_mono_ae ((ae_restrict_iff' M).2 (eventually_of_forall (λ x hx, _))),
648648
rw [add_comm, ennreal.zpow_add t_ne_zero ennreal.coe_ne_top, zpow_one],
649-
exact ennreal.mul_le_mul le_rfl hx.2.1,
649+
exact mul_le_mul_left' hx.2.1 _,
650650
end
651651
... = t * ∫⁻ x in s ∩ f⁻¹' I, f x ∂μ : lintegral_const_mul _ f_meas },
652652
calc ρ s = ρ (s ∩ f⁻¹' {0}) + ρ (s ∩ f⁻¹' {∞}) + ∑' (n : ℤ), ρ (s ∩ f⁻¹' (Ico (t^n) (t^(n+1)))) :

‎src/measure_theory/covering/vitali.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -388,7 +388,7 @@ begin
388388
measure_Union_le _
389389
... ≤ ∑' (a : {a // a ∉ w}), C * μ (B a) : ennreal.tsum_le_tsum (λ a, μB a (ut (vu a.1.2)))
390390
... = C * ∑' (a : {a // a ∉ w}), μ (B a) : ennreal.tsum_mul_left
391-
... ≤ C * (ε / C) : ennreal.mul_le_mul le_rfl hw.le
391+
... ≤ C * (ε / C) : mul_le_mul_left' hw.le _
392392
... ≤ ε : ennreal.mul_div_le
393393
end
394394

0 commit comments

Comments
 (0)