feat(topology/instances/ennreal): continuity of subtraction on ennreal (

#11527)

src/data/real/ennreal.lean

@@ -999,6 +999,24 @@ inv_top ▸ inv_eq_inv
 
 lemma inv_ne_zero : a⁻¹ ≠ 0 ↔ a ≠ ∞ := by simp
 
+lemma mul_inv {a b : ℝ≥0∞} (ha : a ≠ 0 ∨ b ≠ ∞) (hb : a ≠ ∞ ∨ b ≠ 0) :
+  (a * b)⁻¹ = a⁻¹ * b⁻¹ :=
+begin
+  induction b using with_top.rec_top_coe,
+  { simp at ha, simp [ha], },
+  induction a using with_top.rec_top_coe,
+  { simp at hb, simp [hb] },
+  by_cases h'a : a = 0,
+  { simp only [h'a, with_top.top_mul, ennreal.inv_zero, ennreal.coe_ne_top, zero_mul, ne.def,
+               not_false_iff, ennreal.coe_zero, ennreal.inv_eq_zero] },
+  by_cases h'b : b = 0,
+  { simp only [h'b, ennreal.inv_zero, ennreal.coe_ne_top, with_top.mul_top, ne.def, not_false_iff,
+               mul_zero, ennreal.coe_zero, ennreal.inv_eq_zero] },
+  rw [← ennreal.coe_mul, ← ennreal.coe_inv, ← ennreal.coe_inv h'a, ← ennreal.coe_inv h'b,
+      ← ennreal.coe_mul, nnreal.mul_inv, mul_comm],
+  simp [h'a, h'b],
+end
+
 @[simp] lemma inv_pos : 0 < a⁻¹ ↔ a ≠ ∞ :=
 pos_iff_ne_zero.trans inv_ne_zero
 

src/data/real/nnreal.lean

@@ -697,6 +697,13 @@ begin
   { simp [pow_pos hx.bot_lt _] }
 end
 
+lemma inv_lt_inv_iff {x y : ℝ≥0} (hx : x ≠ 0) (hy : y ≠ 0) :
+  y⁻¹ < x⁻¹ ↔ x < y :=
+by rw [← one_div, div_lt_iff hy, ← div_eq_inv_mul, lt_div_iff hx, one_mul]
+
+lemma inv_lt_inv {x y : ℝ≥0} (hx : x ≠ 0) (h : x < y) : y⁻¹ < x⁻¹ :=
+(inv_lt_inv_iff hx ((bot_le.trans_lt h).ne')).2 h
+
 end inv
 
 @[simp] lemma abs_eq (x : ℝ≥0) : |(x : ℝ)| = x :=

src/topology/instances/ennreal.lean

@@ -257,6 +257,45 @@ begin
   { exact hβ, },
 end
 
+lemma tendsto_sub {a b : ℝ≥0∞} (h : a ≠ ∞ ∨ b ≠ ∞) :
+  tendsto (λ p : ℝ≥0∞ × ℝ≥0∞, p.1 - p.2) (𝓝 (a, b)) (𝓝 (a - b)) :=
+begin
+  cases a; cases b,
+  { simp only [eq_self_iff_true, not_true, ne.def, none_eq_top, or_self] at h, contradiction },
+  { simp only [some_eq_coe, with_top.top_sub_coe, none_eq_top],
+    apply tendsto_nhds_top_iff_nnreal.2 (λ n, _),
+    rw [nhds_prod_eq, eventually_prod_iff],
+    refine ⟨λ z, ((n + (b + 1)) : ℝ≥0∞) < z,
+            Ioi_mem_nhds (by simp only [one_lt_top, add_lt_top, coe_lt_top, and_self]),
+            λ z, z < b + 1, Iio_mem_nhds ((ennreal.lt_add_right coe_ne_top one_ne_zero)),
+            λ x hx y hy, _⟩,
+    dsimp,
+    rw lt_tsub_iff_right,
+    have : ((n : ℝ≥0∞) + y) + (b + 1) < x + (b + 1) := calc
+      ((n : ℝ≥0∞) + y) + (b + 1) = ((n : ℝ≥0∞) + (b + 1)) + y : by abel
+      ... < x + (b + 1) : ennreal.add_lt_add hx hy,
+    exact lt_of_add_lt_add_right this },
+  { simp only [some_eq_coe, with_top.sub_top, none_eq_top],
+    suffices H : ∀ᶠ (p : ℝ≥0∞ × ℝ≥0∞) in 𝓝 (a, ∞), 0 = p.1 - p.2,
+      from tendsto_const_nhds.congr' H,
+    rw [nhds_prod_eq, eventually_prod_iff],
+    refine ⟨λ z, z < a + 1, Iio_mem_nhds (ennreal.lt_add_right coe_ne_top one_ne_zero),
+            λ z, (a : ℝ≥0∞) + 1 < z,
+            Ioi_mem_nhds (by simp only [one_lt_top, add_lt_top, coe_lt_top, and_self]),
+            λ x hx y hy, _⟩,
+    rw eq_comm,
+    simp only [tsub_eq_zero_iff_le, (has_lt.lt.trans hx hy).le], },
+  { simp only [some_eq_coe, nhds_coe_coe, tendsto_map'_iff, function.comp, ← ennreal.coe_sub,
+               tendsto_coe],
+    exact continuous.tendsto (by continuity) _ }
+end
+
+protected lemma tendsto.sub {f : filter α} {ma : α → ℝ≥0∞} {mb : α → ℝ≥0∞} {a b : ℝ≥0∞}
+  (hma : tendsto ma f (𝓝 a)) (hmb : tendsto mb f (𝓝 b)) (h : a ≠ ∞ ∨ b ≠ ∞) :
+  tendsto (λ a, ma a - mb a) f (𝓝 (a - b)) :=
+show tendsto ((λ p : ℝ≥0∞ × ℝ≥0∞, p.1 - p.2) ∘ (λa, (ma a, mb a))) f (𝓝 (a - b)), from
+tendsto.comp (ennreal.tendsto_sub h) (hma.prod_mk_nhds hmb)
+
 protected lemma tendsto_mul (ha : a ≠ 0 ∨ b ≠ ⊤) (hb : b ≠ 0 ∨ a ≠ ⊤) :
   tendsto (λp:ℝ≥0∞×ℝ≥0∞, p.1 * p.2) (𝓝 (a, b)) (𝓝 (a * b)) :=
 have ht : ∀b:ℝ≥0∞, b ≠ 0 → tendsto (λp:ℝ≥0∞×ℝ≥0∞, p.1 * p.2) (𝓝 ((⊤:ℝ≥0∞), b)) (𝓝 ⊤),