chore(data/real/{e,}nnreal): a few lemmas (#5530)

* Rename `nnreal.le_of_forall_lt_one_mul_lt` to
  `nnreal.le_of_forall_lt_one_mul_le`, and similarly for `ennreal`.
* Move the proof of the latter lemma to `topology/instances/ennreal`,
  prove it using continuity of multiplication.
* Add `ennreal.le_of_forall_nnreal_lt`, `nnreal.lt_div_iff`, and
  `nnreal.mul_lt_of_lt_div`.

Author: urkud

src/data/real/ennreal.lean

@@ -1039,23 +1039,12 @@ mul_comm a a⁻¹ ▸ mul_inv_cancel h0 ht
 lemma mul_le_iff_le_inv {a b r : ennreal} (hr₀ : r ≠ 0) (hr₁ : r ≠ ∞) : (r * a ≤ b ↔ a ≤ r⁻¹ * b) :=
 by rw [← @ennreal.mul_le_mul_left _ a _ hr₀ hr₁, ← mul_assoc, mul_inv_cancel hr₀ hr₁, one_mul]
 
-lemma le_of_forall_lt_one_mul_lt : ∀{x y : ennreal}, (∀a<1, a * x ≤ y) → x ≤ y :=
-forall_ennreal.2 $ and.intro
-  (assume r, forall_ennreal.2 $ and.intro
-    (assume q h, coe_le_coe.2 $ nnreal.le_of_forall_lt_one_mul_lt $ assume a ha,
-      begin rw [← coe_le_coe, coe_mul], exact h _ (coe_lt_coe.2 ha) end)
-    (assume h, le_top))
-  (assume r hr,
-    have ((1 / 2 : ℝ≥0) : ennreal) * ∞ ≤ r :=
-      hr _ (coe_lt_coe.2 ((@nnreal.coe_lt_coe (1/2) 1).1 one_half_lt_one)),
-    have ne : ((1 / 2 : ℝ≥0) : ennreal) ≠ 0,
-    begin
-      rw [(≠), coe_eq_zero],
-      refine zero_lt_iff_ne_zero.1 _,
-      show 0 < (1 / 2 : ℝ),
-      linarith,
-    end,
-    by rwa [mul_top, if_neg ne] at this)
+lemma le_of_forall_nnreal_lt {x y : ennreal} (h : ∀ r : ℝ≥0, ↑r < x → ↑r ≤ y) : x ≤ y :=
+begin
+  refine le_of_forall_ge_of_dense (λ r hr, _),
+  lift r to ℝ≥0 using ne_top_of_lt hr,
+  exact h r hr
+end
 
 lemma div_add_div_same {a b c : ennreal} : a / c + b / c = (a + b) / c :=
 eq.symm $ right_distrib a b (c⁻¹)

src/data/real/nnreal.lean

@@ -572,7 +572,17 @@ by rw [div_def, mul_comm, ← mul_le_iff_le_inv hr, mul_comm]
 lemma div_le_iff {a b r : ℝ≥0} (hr : r ≠ 0) : a / r ≤ b ↔ a ≤ b * r :=
 @div_le_iff ℝ _ a r b $ zero_lt_iff_ne_zero.2 hr
 
-lemma le_of_forall_lt_one_mul_lt {x y : ℝ≥0} (h : ∀a<1, a * x ≤ y) : x ≤ y :=
+lemma lt_div_iff {a b r : ℝ≥0} (hr : r ≠ 0) : a < b / r ↔ a * r < b :=
+lt_iff_lt_of_le_iff_le (div_le_iff hr)
+
+lemma mul_lt_of_lt_div {a b r : ℝ≥0} (h : a < b / r) : a * r < b :=
+begin
+  refine (lt_div_iff $ λ hr, false.elim _).1 h,
+  subst r,
+  simpa using h
+end
+
+lemma le_of_forall_lt_one_mul_le {x y : ℝ≥0} (h : ∀a<1, a * x ≤ y) : x ≤ y :=
 le_of_forall_ge_of_dense $ assume a ha,
   have hx : x ≠ 0 := zero_lt_iff_ne_zero.1 (lt_of_le_of_lt (zero_le _) ha),
   have hx' : x⁻¹ ≠ 0, by rwa [(≠), inv_eq_zero],

src/measure_theory/integration.lean

@@ -938,7 +938,7 @@ begin
   refine le_antisymm _ (supr_lintegral_le _),
   rw [lintegral_eq_nnreal],
   refine supr_le (assume s, supr_le (assume hsf, _)),
-  refine ennreal.le_of_forall_lt_one_mul_lt (assume a ha, _),
+  refine ennreal.le_of_forall_lt_one_mul_le (assume a ha, _),
   rcases ennreal.lt_iff_exists_coe.1 ha with ⟨r, rfl, ha⟩,
   have ha : r < 1 := ennreal.coe_lt_coe.1 ha,
   let rs := s.map (λa, r * a),

src/topology/instances/ennreal.lean

@@ -286,6 +286,15 @@ continuous_iff_continuous_at.2 $ λ x, ennreal.continuous_at_const_mul (or.inl h
 protected lemma continuous_mul_const {a : ennreal} (ha : a ≠ ⊤) : continuous (λ x, x * a) :=
 continuous_iff_continuous_at.2 $ λ x, ennreal.continuous_at_mul_const (or.inl ha)
 
+lemma le_of_forall_lt_one_mul_le {x y : ennreal} (h : ∀ a < 1, a * x ≤ y) : x ≤ y :=
+begin
+  have : tendsto (* x) (𝓝[Iio 1] 1) (𝓝 (1 * x)) :=
+    (ennreal.continuous_at_mul_const (or.inr one_ne_zero)).mono_left inf_le_left,
+  rw one_mul at this,
+  haveI : (𝓝[Iio 1] (1 : ennreal)).ne_bot := nhds_within_Iio_self_ne_bot' ennreal.zero_lt_one,
+  exact le_of_tendsto this (eventually_nhds_within_iff.2 $ eventually_of_forall h)
+end
+
 lemma infi_mul_left {ι} [nonempty ι] {f : ι → ennreal} {a : ennreal}
   (h : a = ⊤ → (⨅ i, f i) = 0 → ∃ i, f i = 0) :
   (⨅ i, a * f i) = a * ⨅ i, f i :=