feat(topology): prove continuity of nndist and edist; ball a r is a…

… metric space

src/analysis/normed_space/basic.lean

@@ -161,6 +161,9 @@ begin
   exact squeeze_zero (λ t, abs_nonneg _) (λ t, abs_norm_sub_norm_le _ _) (lim_norm x)
 end
 
+lemma continuous_nnnorm : continuous (nnnorm : α → nnreal) :=
+continuous_subtype_mk _ continuous_norm
+
 instance normed_top_monoid : topological_add_monoid α :=
 ⟨continuous_iff_tendsto.2 $ λ ⟨x₁, x₂⟩,
   tendsto_iff_norm_tendsto_zero.2
@@ -342,6 +345,11 @@ begin
     exact tendsto_add lim1 lim2  }
 end
 
+lemma continuous_smul [topological_space γ] {f : γ → α} {g : γ → E}
+  (hf : continuous f) (hg : continuous g) : continuous (λc, f c • g c) :=
+continuous_iff_tendsto.2 $ assume c,
+  tendsto_smul (continuous_iff_tendsto.1 hf _) (continuous_iff_tendsto.1 hg _)
+
 instance : normed_space α (E × F) :=
 { norm_smul :=
   begin

src/data/real/ennreal.lean

@@ -125,6 +125,12 @@ begin split_ifs, { simp [h] }, { exact with_top.top_mul h } end
 
 @[simp] lemma top_mul_top : ∞ * ∞ = ∞ := with_top.top_mul_top
 
+lemma mul_eq_top {a b : ennreal} : a * b = ⊤ ↔ (a ≠ 0 ∧ b = ⊤) ∨ (a = ⊤ ∧ b ≠ 0) :=
+with_top.mul_eq_top_iff
+
+lemma mul_lt_top {a b : ennreal}  : a < ⊤ → b < ⊤ → a * b < ⊤ :=
+by simp [ennreal.lt_top_iff_ne_top, (≠), mul_eq_top] {contextual := tt}
+
 @[simp] lemma coe_finset_sum {s : finset α} {f : α → nnreal} : ↑(s.sum f) = (s.sum (λa, f a) : ennreal) :=
 (finset.sum_hom coe).symm
 
@@ -230,6 +236,12 @@ lemma coe_mem_upper_bounds {s : set nnreal} :
   ↑r ∈ upper_bounds ((coe : nnreal → ennreal) '' s) ↔ r ∈ upper_bounds s :=
 by simp [upper_bounds, ball_image_iff, -mem_image, *] {contextual := tt}
 
+lemma infi_ennreal {α : Type*} [complete_lattice α] {f : ennreal → α} :
+  (⨅n, f n) = (⨅n:nnreal, f n) ⊓ f ⊤ :=
+le_antisymm
+  (le_inf (le_infi $ assume i, infi_le _ _) (infi_le _ _))
+  (le_infi $ forall_ennreal.2 ⟨assume r, inf_le_left_of_le $ infi_le _ _, inf_le_right⟩)
+
 end complete_lattice
 
 section mul
@@ -248,9 +260,6 @@ 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 _ _
 

src/topology/instances/ennreal.lean

@@ -410,3 +410,94 @@ 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,
 show has_sum (λb, g' b : β → ℝ), from nnreal.has_sum_coe.2 this
+
+lemma infi_real_pos_eq_infi_nnreal_pos {α : Type*} [complete_lattice α] {f : ℝ → α} :
+  (⨅(n:ℝ) (h : n > 0), f n) = (⨅(n:nnreal) (h : n > 0), f n) :=
+le_antisymm
+  (le_infi $ assume n, le_infi $ assume hn, infi_le_of_le n $ infi_le _ (nnreal.coe_pos.2 hn))
+  (le_infi $ assume r, le_infi $ assume hr, infi_le_of_le ⟨r, le_of_lt hr⟩ $ infi_le _ hr)
+
+namespace emetric
+variables [emetric_space β]
+open lattice ennreal filter
+
+lemma edist_ne_top_of_mem_ball {a : β} {r : ennreal} (x y : ball a r) : edist x.1 y.1 ≠ ⊤ :=
+lt_top_iff_ne_top.1 $
+calc edist x y ≤ edist a x + edist a y : edist_triangle_left x.1 y.1 a
+  ... < r + r : by rw [edist_comm a x, edist_comm a y]; exact add_lt_add x.2 y.2
+  ... ≤ ⊤ : le_top
+
+/-- Each ball in an extended metric space gives us a metric space.
+
+The topology is fixed to be the subtype topology. -/
+def metric_space_emetric_ball (a : β) (r : ennreal) : metric_space (ball a r) :=
+{ dist               := λx y, (edist x.1 y.1).to_nnreal,
+  edist              := λx y, edist x.1 y.1,
+  to_uniform_space   := subtype.uniform_space,
+  dist_self          := assume ⟨x, hx⟩, by simp,
+  dist_comm          := assume ⟨x, hx⟩ ⟨y, hy⟩, by simp [edist_comm],
+  dist_triangle      := assume x y z,
+  begin
+    simp only [coe_to_nnreal (edist_ne_top_of_mem_ball _ _),
+      (nnreal.coe_add _ _).symm, ennreal.coe_le_coe.symm, nnreal.coe_le.symm, ennreal.coe_add],
+    exact edist_triangle _ _ _
+  end,
+  eq_of_dist_eq_zero := assume x y h, subtype.eq $
+    by simp [to_nnreal_eq_zero_iff, edist_ne_top_of_mem_ball] at h; assumption,
+  edist_dist         := assume x y,
+    have h : _ := edist_ne_top_of_mem_ball x y,
+    by cases eq : edist x.1 y.1; simp [none_eq_top, some_eq_coe, *] at *,
+  uniformity_dist    :=
+  begin
+    have : ∀(p : ↥(ball a r) × ↥(ball a r)) (n : nnreal),
+      ((edist p.1.1 p.2.1).to_nnreal : ℝ) < n ↔ edist p.1.1 p.2.1 < n,
+    { assume p n,
+      rw [← nnreal.coe_lt, ← ennreal.coe_lt_coe, coe_to_nnreal (edist_ne_top_of_mem_ball _ _)] },
+    simp only [uniformity_subtype, uniformity_edist_nnreal, comap_infi, comap_principal,
+      infi_real_pos_eq_infi_nnreal_pos, this],
+    refl
+  end }
+
+section
+local attribute [instance] metric_space_emetric_ball
+
+lemma nhds_eq_nhds_emetric_ball (a x : β) (r : ennreal) (h : x ∈ ball a r) :
+  nhds x = map (coe : ball a r → β) (nhds ⟨x, h⟩) :=
+(map_nhds_subtype_val_eq _ $ mem_nhds_sets is_open_ball h).symm
+
+lemma continuous_edist : continuous (λp:β×β, edist p.1 p.2) :=
+continuous_iff_tendsto.2
+begin
+  rintros ⟨p₁, p₂⟩,
+  cases h : edist p₁ p₂; simp [none_eq_top, some_eq_coe, nhds_prod_eq] at ⊢ h,
+  { refine tendsto_nhds_top (assume n, _),
+    rw [filter.mem_prod_iff],
+    refine ⟨_, ball_mem_nhds p₁ ennreal.zero_lt_one, _, ball_mem_nhds p₂ ennreal.zero_lt_one, _⟩,
+    rintros ⟨q₁, q₂⟩ ⟨h₁, h₂⟩,
+    change edist q₁ p₁ < 1 at h₁,
+    change edist q₂ p₂ < 1 at h₂,
+    rw [edist_comm] at h₁,
+    have : ⊤ ≤ edist q₁ q₂ + 2,
+    exact calc ⊤ = edist p₁ p₂ : h.symm
+      ... ≤ edist p₁ q₁ + edist q₁ q₂ + edist q₂ p₂ : edist_triangle4 _ _ _ _
+      ... ≤ 1 + edist q₁ q₂ + 1 : add_le_add' (add_le_add' (le_of_lt h₁) $ le_refl _) (le_of_lt h₂)
+      ... = edist q₁ q₂ + 2 : by rw [← one_add_one_eq_two]; simp,
+    rw [top_le_iff, add_eq_top] at this,
+    simp at this,
+    simp [this, lt_top_iff_ne_top] },
+  { have h₁ : p₁ ∈ ball p₁ ⊤, { simp, exact with_top.zero_lt_top },
+    let p'₁ : ↥(ball p₁ ⊤) := ⟨p₁, h₁⟩,
+    have h₂ : p₂ ∈ ball p₁ ⊤, { dsimp [ball], rw [edist_comm, h], exact coe_lt_top },
+    let p'₂ : ↥(ball p₁ ⊤) := ⟨p₂, h₂⟩,
+    rw [nhds_eq_nhds_emetric_ball p₁ p₁ ⊤ h₁, nhds_eq_nhds_emetric_ball p₁ p₂ ⊤ h₂,
+      prod_map_map_eq, tendsto_map'_iff, ← h],
+    change tendsto (λp : ↥(ball p₁ ⊤) × ↥(ball p₁ ⊤), edist p.1 p.2)
+      (filter.prod (nhds ⟨p₁, h₁⟩) (nhds ⟨p₂, h₂⟩))
+      (nhds (edist p'₁ p'₂)),
+    simp only [(nndist_eq_edist _ _).symm],
+    exact ennreal.tendsto_coe.2 (tendsto_nndist' _ _) }
+end
+
+end
+
+end emetric

src/topology/instances/nnreal.lean

@@ -12,7 +12,6 @@ open set topological_space metric
 namespace nnreal
 local notation ` ℝ≥0 ` := nnreal
 
-instance : metric_space ℝ≥0 := by unfold nnreal; apply_instance
 instance : topological_space ℝ≥0 := infer_instance
 
 instance : topological_semiring ℝ≥0 :=
@@ -98,4 +97,4 @@ tsum_eq_is_sum $ is_sum_coe.2 $ is_sum_tsum $ hf
 
 end coe
 
-end nnreal
+end nnreal

src/topology/metric_space/basic.lean

@@ -646,6 +646,12 @@ metric_space.induced subtype.val (λ x y, subtype.eq) t
 theorem subtype.dist_eq {p : α → Prop} [t : metric_space α] (x y : subtype p) :
   dist x y = dist x.1 y.1 := rfl
 
+section nnreal
+
+instance : metric_space nnreal := by unfold nnreal; apply_instance
+
+end nnreal
+
 section prod
 
 instance prod.metric_space_max [metric_space β] : metric_space (α × β) :=
@@ -820,6 +826,16 @@ lemma tendsto_iff_dist_tendsto_zero {f : β → α} {x : filter β} {a : α} :
   (tendsto f x (nhds a)) ↔ (tendsto (λb, dist (f b) a) x (nhds 0)) :=
 by rw [← nhds_comap_dist a, tendsto_comap_iff]
 
+lemma uniform_continuous_nndist' : uniform_continuous (λp:α×α, nndist p.1 p.2) :=
+uniform_continuous_subtype_mk uniform_continuous_dist' _
+
+lemma continuous_nndist' : continuous (λp:α×α, nndist p.1 p.2) :=
+uniform_continuous_nndist'.continuous
+
+lemma tendsto_nndist' (a b :α) :
+  tendsto (λp:α×α, nndist p.1 p.2) (filter.prod (nhds a) (nhds b)) (nhds (nndist a b)) :=
+by rw [← nhds_prod_eq]; exact continuous_iff_tendsto.1 continuous_nndist' _
+
 namespace metric
 variables {x y z : α} {ε ε₁ ε₂ : ℝ} {s : set α}
 

src/topology/metric_space/emetric_space.lean

@@ -89,7 +89,10 @@ This is enforced in the type class definition, by extending the `uniform_space`
 instantiating an `emetric_space` structure, the uniformity fields are not necessary, they will be
 filled in by default. There is a default value for the uniformity, that can be substituted
 in cases of interest, for instance when instantiating an `emetric_space` structure
-on a product. -/
+on a product.
+
+Continuity of `edist` is finally proving in `topology.instances.ennreal`
+-/
 class emetric_space (α : Type u) extends has_edist α : Type u :=
 (edist_self : ∀ x : α, edist x x = 0)
 (eq_of_edist_eq_zero : ∀ {x y : α}, edist x y = 0 → x = y)
@@ -142,6 +145,15 @@ emetric_space.uniformity_edist _
 theorem uniformity_edist'' : uniformity = (⨅ε:{ε:ennreal // ε>0}, principal {p:α×α | edist p.1 p.2 < ε.val}) :=
 by simp [infi_subtype]; exact uniformity_edist'
 
+theorem uniformity_edist_nnreal :
+  uniformity = (⨅(ε:nnreal) (h : ε > 0), principal {p:α×α | edist p.1 p.2 < ε}) :=
+begin
+  rw [uniformity_edist', ennreal.infi_ennreal, inf_of_le_left],
+  { congr, funext ε, refine infi_congr_Prop ennreal.coe_pos _, assume h, refl },
+  refine le_infi (assume h, infi_le_of_le 1 $ infi_le_of_le ennreal.zero_lt_one $ _),
+  exact principal_mono.2 (assume p h, lt_of_lt_of_le h le_top)
+end
+
 /-- Characterization of the elements of the uniformity in terms of the extended distance -/
 theorem mem_uniformity_edist {s : set (α×α)} :
   s ∈ (@uniformity α _).sets ↔ (∃ε>0, ∀{a b:α}, edist a b < ε → (a, b) ∈ s) :=