feat(data/real/ennreal): minor additions to ennreal (#558)

analysis/ennreal.lean

@@ -133,7 +133,7 @@ instance : topological_add_monoid ennreal :=
     simp only [coe_add.symm, tendsto_coe, tendsto_add']
   end ⟩
 
-protected lemma tendsto_mul' (ha : a ≠ 0) (hb : b ≠ 0) :
+protected lemma tendsto_mul' (ha : a ≠ 0 ∨ b ≠ ⊤) (hb : b ≠ 0 ∨ a ≠ ⊤) :
   tendsto (λp:ennreal×ennreal, p.1 * p.2) (nhds (a, b)) (nhds (a * b)) :=
 have ht : ∀b:ennreal, b ≠ 0 → tendsto (λp:ennreal×ennreal, p.1 * p.2) (nhds ((⊤:ennreal), b)) (nhds ⊤),
 begin
@@ -157,25 +157,26 @@ begin
       (le_of_lt h₂)
 end,
 begin
-  cases a, { simp [none_eq_top, ht b hb, top_mul, hb] },
+  cases a, {simp [none_eq_top] at hb, simp [none_eq_top, ht b hb, top_mul, hb] },
   cases b, {
+    simp [none_eq_top] at ha,
     have ha' : a ≠ 0, from mt coe_eq_coe.2 ha,
     simp [*, nhds_swap (a : ennreal) ⊤, none_eq_top, some_eq_coe, top_mul, tendsto_map'_iff, (∘), mul_comm] },
   simp [some_eq_coe, nhds_coe_coe, tendsto_map'_iff, (∘)],
   simp only [coe_mul.symm, tendsto_coe, tendsto_mul']
 end
 
 protected lemma tendsto_mul {f : filter α} {ma : α → ennreal} {mb : α → ennreal} {a b : ennreal}
-  (hma : tendsto ma f (nhds a)) (ha : a ≠ 0) (hmb : tendsto mb f (nhds b)) (hb : b ≠ 0) :
+  (hma : tendsto ma f (nhds a)) (ha : a ≠ 0 ∨ b ≠ ⊤) (hmb : tendsto mb f (nhds b)) (hb : b ≠ 0 ∨ a ≠ ⊤) :
   tendsto (λa, ma a * mb a) f (nhds (a * b)) :=
 show tendsto ((λp:ennreal×ennreal, p.1 * p.2) ∘ (λa, (ma a, mb a))) f (nhds (a * b)), from
 tendsto.comp (tendsto_prod_mk_nhds hma hmb) (ennreal.tendsto_mul' ha hb)
 
 protected lemma tendsto_mul_right {f : filter α} {m : α → ennreal} {a b : ennreal}
-  (hm : tendsto m f (nhds b)) (hb : b ≠ 0) : tendsto (λb, a * m b) f (nhds (a * b)) :=
+  (hm : tendsto m f (nhds b)) (hb : b ≠ 0 ∨ a ≠ ⊤) : tendsto (λb, a * m b) f (nhds (a * b)) :=
 by_cases
   (assume : a = 0, by simp [this, tendsto_const_nhds])
-  (assume ha : a ≠ 0, ennreal.tendsto_mul tendsto_const_nhds ha hm hb)
+  (assume ha : a ≠ 0, ennreal.tendsto_mul tendsto_const_nhds (or.inl ha) hm hb)
 
 lemma Sup_add {s : set ennreal} (hs : s ≠ ∅) : Sup s + a = ⨆b∈s, b + a :=
 have Sup ((λb, b + a) '' s) = Sup s + a,
@@ -244,7 +245,7 @@ begin
         (assume x _ y _ h, canonically_ordered_semiring.mul_le_mul (le_refl _) h)
         is_lub_Sup
         s₀
-        (ennreal.tendsto_mul_right (tendsto_id' inf_le_left) s₁)),
+        (ennreal.tendsto_mul_right (tendsto_id' inf_le_left) (or.inl s₁))),
     rw [this.symm, Sup_image] }
 end
 
@@ -358,7 +359,7 @@ have sum_ne_0 : (∑i, f i) ≠ 0, from ne_of_gt $
 have tendsto (λs:finset α, s.sum ((*) a ∘ f)) at_top (nhds (a * (∑i, f i))),
   by rw [← show (*) a ∘ (λs:finset α, s.sum f) = λs, s.sum ((*) a ∘ f),
          from funext $ λ s, finset.mul_sum];
-  exact ennreal.tendsto_mul_right (is_sum_tsum ennreal.has_sum) sum_ne_0,
+  exact ennreal.tendsto_mul_right (is_sum_tsum ennreal.has_sum) (or.inl sum_ne_0),
 tsum_eq_is_sum this
 
 protected lemma tsum_mul : (∑i, f i * a) = (∑i, f i) * a :=
@@ -403,5 +404,5 @@ lemma has_sum_of_nonneg_of_le {f g : β → ℝ} (hg : ∀b, 0 ≤ g b) (hgf : 
 let f' (b : β) : nnreal := ⟨f b, le_trans (hg b) (hgf b)⟩ in
 let g' (b : β) : nnreal := ⟨g b, hg b⟩ in
 have has_sum f', from nnreal.has_sum_coe.1 hf,
-have has_sum g', from nnreal.has_sum_of_le (assume b, (nnreal.coe_le (g' b) (f' b)).2 $ hgf b) this,
+have has_sum g', from nnreal.has_sum_of_le (assume b, (@nnreal.coe_le (g' b) (f' b)).2 $ hgf b) this,
 show has_sum (λb, g' b : β → ℝ), from nnreal.has_sum_coe.2 this

analysis/metric_space.lean

@@ -449,7 +449,7 @@ begin
     by rwa [← nndist_eq_edist, ennreal.coe_lt_coe] at Dab,
     have J : dist a b < ε := begin
       rw [← nndist_eq_dist],
-      have K := (nnreal.coe_lt _ _).1 I,
+      have K := nnreal.coe_lt.1 I,
       rwa [nnreal.coe_of_real _ (le_of_lt εpos)] at K
     end,
     exact Hε a b J
@@ -482,7 +482,7 @@ instance emetric_space_of_metric_space [a : metric_space α] : emetric_space α
   begin
     rw [edist_dist, edist_dist, edist_dist, ← ennreal.coe_add, ennreal.coe_le_coe,
         nnreal.of_real_add_of_real (@dist_nonneg _ _ x y) (@dist_nonneg _ _ y z),
-        nnreal.of_real_le_of_real_iff (@dist_nonneg _ _ x z) $
+        nnreal.of_real_le_of_real_iff $
           add_nonneg (@dist_nonneg _ _ x y) (@dist_nonneg _ _ y z)],
     apply dist_triangle x y z
   end,
@@ -778,7 +778,7 @@ instance metric_space_pi : metric_space (Πb, π b) :=
   dist_comm := assume f g, nnreal.eq_iff.2 $ by congr; ext a; exact nndist_comm _ _,
   dist_triangle := assume f g h, show dist f h ≤ (dist f g) + (dist g h), from
     begin
-      simp only [dist_pi_def, (nnreal.coe_add _ _).symm, (nnreal.coe_le _ _).symm,
+      simp only [dist_pi_def, (nnreal.coe_add _ _).symm, nnreal.coe_le.symm,
         finset.sup_le_iff],
       assume b hb,
       exact le_trans (nndist_triangle _ (g b) _) (add_le_add (le_sup hb) (le_sup hb))

data/real/ennreal.lean

@@ -65,7 +65,7 @@ lemma to_nnreal_eq_zero_iff (x : ennreal) : x.to_nnreal = 0 ↔ x = 0 ∨ x = 
   { have A : some (0:nnreal) = (0:ennreal) := rfl,
     simp [ennreal.to_nnreal, A] {contextual := tt} }
 end,
-by intro h; cases h; [simp [h], simp[h]]⟩
+by intro h; cases h; simp [h]⟩
 
 @[simp] lemma coe_ne_top : (r : ennreal) ≠ ∞ := with_top.coe_ne_top
 @[simp] lemma top_ne_coe : ∞ ≠ (r : ennreal) := with_top.top_ne_coe
@@ -88,13 +88,22 @@ by intro h; cases h; [simp [h], simp[h]]⟩
 @[simp] lemma coe_add : ↑(r + p) = (r + p : ennreal) := with_top.coe_add
 @[simp] lemma coe_mul : ↑(r * p) = (r * p : ennreal) := with_top.coe_mul
 
+@[simp] lemma coe_bit0 : (↑(bit0 r) : ennreal) = bit0 r := coe_add
+@[simp] lemma coe_bit1 : (↑(bit1 r) : ennreal) = bit1 r := by simp [bit1]
+
 @[simp] lemma add_top : a + ∞ = ∞ := with_top.add_top
 @[simp] lemma top_add : ∞ + a = ∞ := with_top.top_add
 
 instance : is_semiring_hom (coe : nnreal → ennreal) :=
 by refine_struct {..}; simp
 
 lemma add_eq_top : a + b = ∞ ↔ a = ∞ ∨ b = ∞ := with_top.add_eq_top _ _
+lemma add_lt_top : a + b < ∞ ↔ a < ∞ ∧ b < ∞ := with_top.add_lt_top _ _
+
+/- rw has trouble with the generic lt_top_iff_ne_top and bot_lt_iff_ne_bot
+(contrary to erw). This is solved with the next lemmas -/
+protected lemma lt_top_iff_ne_top : a < ∞ ↔ a ≠ ∞ := lt_top_iff_ne_top
+protected lemma bot_lt_iff_ne_bot : 0 < a ↔ a ≠ 0 := bot_lt_iff_ne_bot
 
 lemma mul_top : a * ∞ = (if a = 0 then 0 else ∞) :=
 begin split_ifs, { simp [h] }, { exact with_top.mul_top h } end
@@ -137,6 +146,9 @@ protected lemma zero_lt_one : 0 < (1 : ennreal) := zero_lt_coe_iff.mpr zero_lt_o
 lemma add_lt_add_iff_left : a < ⊤ → (a + c < a + b ↔ c < b) :=
 with_top.add_lt_add_iff_left
 
+lemma add_lt_add_iff_right : a < ⊤ → (c + a < b + a ↔ c < b) :=
+with_top.add_lt_add_iff_right
+
 lemma lt_add_right (ha : a < ⊤) (hb : 0 < b) : a < a + b :=
 by rwa [← add_lt_add_iff_left ha, add_zero] at hb
 
@@ -161,6 +173,14 @@ protected lemma lt_iff_exists_rat_btwn :
   end,
 λ ⟨q, q0, qa, qb⟩, lt_trans qa qb⟩
 
+protected lemma exists_nat_gt {r : ennreal} (h : r ≠ ⊤) : ∃n:ℕ, r < n :=
+begin
+  rcases lt_iff_exists_coe.1 (lt_top_iff_ne_top.2 h) with ⟨r, rfl, hb⟩,
+  rcases exists_nat_gt r with ⟨n, hn⟩,
+  refine ⟨n, _⟩,
+  rwa [← ennreal.coe_nat, ennreal.coe_lt_coe],
+end
+
 lemma add_lt_add (ac : a < c) (bd : b < d) : a + b < c + d :=
 begin
   rcases dense ac with ⟨a', aa', a'c⟩,
@@ -210,6 +230,12 @@ begin
   assume h, exact mul_le_mul_left (zero_lt_iff_ne_zero.2 h)
 end
 
+lemma mul_eq_top {a b : ennreal} : a * b = ⊤ ↔ (a ≠ 0 ∧ b = ⊤) ∨ (a = ⊤ ∧ b ≠ 0) :=
+with_top.mul_eq_top_iff
+
+lemma mul_eq_zero {a b : ennreal} : a * b = 0 ↔ a = 0 ∨ b = 0 :=
+canonically_ordered_comm_semiring.mul_eq_zero_iff _ _
+
 end mul
 
 section sub
@@ -280,6 +306,12 @@ iff.intro
     calc a - b ≤ (c + b) - b : sub_le_sub h (le_refl _)
       ... ≤ c : Inf_le (le_refl (c + b)))
 
+@[simp] lemma sub_eq_zero_iff_le : a - b = 0 ↔ a ≤ b :=
+by simpa [-ennreal.sub_le_iff_le_add] using @ennreal.sub_le_iff_le_add a b 0
+
+@[simp] lemma zero_lt_sub_iff_lt : 0 < a - b ↔ b < a :=
+by simpa [ennreal.bot_lt_iff_ne_bot, -sub_eq_zero_iff_le] using not_iff_not.2 (@sub_eq_zero_iff_le a b)
+
 lemma sub_le_self (a b : ennreal) : a - b ≤ a :=
 ennreal.sub_le_iff_le_add.2 $ le_add_of_nonneg_right' $ zero_le _
 
@@ -292,6 +324,42 @@ by rw [← add_right_inj (lt_of_le_of_lt (sub_le_self _ _) h),
 
 end sub
 
+section bit
+
+@[simp] lemma bit0_inj : bit0 a = bit0 b ↔ a = b :=
+⟨λh, begin
+  rcases (lt_trichotomy a b) with h₁| h₂| h₃,
+  { exact (absurd h (ne_of_lt (add_lt_add h₁ h₁))) },
+  { exact h₂ },
+  { exact (absurd h.symm (ne_of_lt (add_lt_add h₃ h₃))) }
+end,
+λh, congr_arg _ h⟩
+
+@[simp] lemma bit0_eq_zero_iff : bit0 a = 0 ↔ a = 0 :=
+by simpa only [bit0_zero] using @bit0_inj a 0
+
+@[simp] lemma bit0_eq_top_iff : bit0 a = ∞ ↔ a = ∞ :=
+by rw [bit0, add_eq_top, or_self]
+
+@[simp] lemma bit1_inj : bit1 a = bit1 b ↔ a = b :=
+⟨λh, begin
+  unfold bit1 at h,
+  rwa [add_right_inj, bit0_inj] at h,
+  simp [lt_top_iff_ne_top]
+end,
+λh, congr_arg _ h⟩
+
+@[simp] lemma bit1_ne_zero : bit1 a ≠ 0 :=
+by unfold bit1; simp
+
+@[simp] lemma bit1_eq_one_iff : bit1 a = 1 ↔ a = 0 :=
+by simpa only [bit1_zero] using @bit1_inj a 0
+
+@[simp] lemma bit1_eq_top_iff : bit1 a = ∞ ↔ a = ∞ :=
+by unfold bit1; rw add_eq_top; simp
+
+end bit
+
 section inv
 instance : has_inv ennreal := ⟨λa, Inf {b | 1 ≤ a * b}⟩
 instance : has_div ennreal := ⟨λa b, a * b⁻¹⟩
@@ -304,27 +372,29 @@ show Inf {b : ennreal | 1 ≤ 0 * b} = ∞, by simp; refl
 @[simp] lemma inv_top : (∞ : ennreal)⁻¹ = 0 :=
 bot_unique $ le_of_forall_le_of_dense $ λ a (h : a > 0), Inf_le $ by simp [*, ne_of_gt h, top_mul]
 
-@[simp] lemma inv_coe (hr : r ≠ 0) : (r : ennreal)⁻¹ = ↑(r⁻¹ : nnreal) :=
+@[simp] lemma coe_inv (hr : r ≠ 0) : (↑r⁻¹ : ennreal) = (↑r)⁻¹ :=
 le_antisymm
-  (Inf_le $ by simp; rw [← coe_mul, nnreal.mul_inv_cancel hr]; exact le_refl 1)
   (le_Inf $ assume b (hb : 1 ≤ ↑r * b), coe_le_iff.2 $
     by rintros b rfl; rwa [← coe_mul, ← coe_one, coe_le_coe, ← nnreal.inv_le hr] at hb)
+  (Inf_le $ by simp; rw [← coe_mul, nnreal.mul_inv_cancel hr]; exact le_refl 1)
 
-@[simp] lemma coe_div (hr : r ≠ 0) : (p : ennreal) / (r : ennreal) = ↑(p / r) :=
-show (↑p * (↑r)⁻¹) = ↑(p * r⁻¹), by rw [inv_coe hr, coe_mul]
+@[simp] lemma coe_div (hr : r ≠ 0) : (↑(p / r) : ennreal) = p / r :=
+show ↑(p * r⁻¹) = ↑p * (↑r)⁻¹, by rw [coe_mul, coe_inv hr]
 
-@[simp] lemma inv_eq_top : (a)⁻¹ = ∞ ↔ a = 0 :=
-by by_cases a = 0; cases a; simp [*, none_eq_top, some_eq_coe] at *
+@[simp] lemma inv_inv : (a⁻¹)⁻¹ = a :=
+by by_cases a = 0; cases a; simp [*, none_eq_top, some_eq_coe,
+  -coe_inv, (coe_inv _).symm] at *
 
-lemma inv_ne_top : (a)⁻¹ ≠ ∞ ↔ a ≠ 0 := by simp
+@[simp] lemma inv_eq_top : a⁻¹ = ∞ ↔ a = 0 :=
+by by_cases a = 0; cases a; simp [*, none_eq_top, some_eq_coe,
+  -coe_inv, (coe_inv _).symm] at *
 
-@[simp] lemma inv_eq_zero : (a)⁻¹ = 0 ↔ a = ∞ :=
-by by_cases a = 0; cases a; simp [*, none_eq_top, some_eq_coe] at *
+lemma inv_ne_top : a⁻¹ ≠ ∞ ↔ a ≠ 0 := by simp
 
-lemma inv_ne_zero : (a)⁻¹ ≠ 0 ↔ a ≠ ∞ := by simp
+@[simp] lemma inv_eq_zero : a⁻¹ = 0 ↔ a = ∞ :=
+by rw [← inv_eq_top, inv_inv]
 
-@[simp] lemma inv_inv : ∀{a:ennreal}, (a⁻¹)⁻¹ = a :=
-forall_ennreal.mpr $ and.intro (assume r, by by_cases r = 0; simp [*, inv_pos]) (by simp)
+lemma inv_ne_zero : a⁻¹ ≠ 0 ↔ a ≠ ∞ := by simp
 
 lemma le_div_iff_mul_le : ∀{b}, b ≠ 0 → b ≠ ⊤ → (a ≤ c / b ↔ a * b ≤ c)
 | none     h0 ht := (ht rfl).elim
@@ -337,14 +407,14 @@ lemma le_div_iff_mul_le : ∀{b}, b ≠ 0 → b ≠ ⊤ → (a ≤ c / b ↔ a *
     rw [← coe_mul, nnreal.mul_inv_cancel hr, coe_one, one_mul, mul_comm]
   end
 
-lemma div_le_iff_le_mul (hb0 : b ≠ 0) (hbt : b ≠ ⊤) : (a / b ≤ c ↔ a ≤ c * b) :=
+lemma div_le_iff_le_mul (hb0 : b ≠ 0) (hbt : b ≠ ⊤) : a / b ≤ c ↔ a ≤ c * b :=
 suffices a * b⁻¹ ≤ c ↔ a ≤ c / b⁻¹, by simpa [div_def],
 (le_div_iff_mul_le (inv_ne_zero.2 hbt) (inv_ne_top.2 hb0)).symm
 
 lemma inv_le_iff_le_mul : (b = ⊤ → a ≠ 0) → (a = ⊤ → b ≠ 0) → (a⁻¹ ≤ b ↔ 1 ≤ a * b) :=
 begin
   cases a; cases b; simp [none_eq_top, some_eq_coe, mul_top, top_mul] {contextual := tt},
-  by_cases a = 0; simp [*, -coe_mul, coe_mul.symm, nnreal.inv_le]
+  by_cases a = 0; simp [*, -coe_mul, coe_mul.symm, -coe_inv, (coe_inv _).symm, nnreal.inv_le]
 end
 
 @[simp] lemma le_inv_iff_mul_le : a ≤ b⁻¹ ↔ a * b ≤ 1 :=
@@ -357,7 +427,7 @@ end
 
 lemma mul_inv_cancel : ∀{r : ennreal}, r ≠ 0 → r ≠ ⊤ → r * r⁻¹ = 1 :=
 begin
-  refine forall_ennreal.2 (and.intro (assume r, _) _); simp { contextual := tt},
+  refine forall_ennreal.2 ⟨λ r, _, _⟩; simp [-coe_inv, (coe_inv _).symm] {contextual := tt},
   assume h, rw [← ennreal.coe_mul, nnreal.mul_inv_cancel h, coe_one]
 end
 
@@ -372,7 +442,7 @@ forall_ennreal.2 $ and.intro
     (assume h, le_top))
   (assume r hr,
     have ((1 / 2 : nnreal) : ennreal) * ⊤ ≤ r :=
-      hr _ (coe_lt_coe.2 ((nnreal.coe_lt (1/2) 1).2 one_half_lt_one)),
+      hr _ (coe_lt_coe.2 ((@nnreal.coe_lt (1/2) 1).2 one_half_lt_one)),
     have ne : ((1 / 2 : nnreal) : ennreal) ≠ 0,
     begin
       rw [(≠), coe_eq_zero],
@@ -403,9 +473,41 @@ calc
     ... = a * 1                : by rw A
     ... = a                    : by rw mul_one
 
-@[simp] lemma div_pos_iff {a b : ennreal}: 0 < a / b ↔ a ≠ 0 ∧ b ≠ ⊤ :=
-by simp [zero_lt_iff_ne_zero, div_def, canonically_ordered_comm_semiring.mul_eq_zero_iff, not_or_distrib]
+@[simp] lemma div_zero_iff {a b : ennreal} : a / b = 0 ↔ a = 0 ∨ b = ⊤ :=
+by simp [div_def, mul_eq_zero]
+
+@[simp] lemma div_pos_iff {a b : ennreal} : 0 < a / b ↔ a ≠ 0 ∧ b ≠ ⊤ :=
+by simp [zero_lt_iff_ne_zero, not_or_distrib]
+
+lemma half_pos {a : ennreal} (h : 0 < a) : 0 < a / 2 :=
+by simp [ne_of_gt h]
 
+lemma half_lt_self {a : ennreal} (hz : a ≠ 0) (ht : a ≠ ⊤) : a / 2 < a :=
+begin
+  cases a,
+  { cases ht none_eq_top },
+  { simp [some_eq_coe] at hz,
+    simpa [-coe_lt_coe, coe_div two_ne_zero'] using
+      coe_lt_coe.2 (nnreal.half_lt_self hz) }
+end
+
+lemma exists_inv_nat_lt {a : ennreal} (h : a ≠ 0) :
+  ∃n:ℕ, (n:ennreal)⁻¹ < a :=
+begin
+  rcases dense (bot_lt_iff_ne_bot.2 h) with ⟨b, bz, ba⟩,
+  have bz' : b ≠ 0 := bot_lt_iff_ne_bot.1 bz,
+  have : b⁻¹ ≠ ⊤ := by simp [bz'],
+  rcases ennreal.exists_nat_gt this with ⟨n, bn⟩,
+  have I : ((n : ℕ) : ennreal)⁻¹ ≤ b := begin
+    rw [ennreal.inv_le_iff_le_mul, mul_comm, ← ennreal.inv_le_iff_le_mul],
+    exact le_of_lt bn,
+    simp only [h, ennreal.nat_ne_top, forall_prop_of_false, ne.def, not_false_iff],
+    exact λ_, ne_bot_of_gt bn,
+    exact λ_, ne_bot_of_gt bn,
+    exact λ_, bz'
+  end,
+  exact ⟨n, lt_of_le_of_lt I ba⟩
+end
 end inv
 
 section infi
@@ -459,13 +561,7 @@ end infi
 section supr
 
 lemma supr_coe_nat : (⨆n:ℕ, (n : ennreal)) = ⊤ :=
-(lattice.supr_eq_top _).2 $ assume b hb,
-begin
-  rcases lt_iff_exists_coe.1 hb with ⟨r, rfl, hb⟩,
-  rcases exists_nat_gt r with ⟨n, hn⟩,
-  refine ⟨n, _⟩,
-  rwa [← ennreal.coe_nat, ennreal.coe_lt_coe],
-end
+(lattice.supr_eq_top _).2 $ assume b hb, ennreal.exists_nat_gt (lt_top_iff_ne_top.1 hb)
 
 end supr