refactor(analysis): add nndist; add finite product of metric spaces; …

…prepare for normed spaces

analysis/complex.lean

@@ -18,7 +18,7 @@ instance : metric_space ℂ :=
 { dist               := λx y, (x - y).abs,
   dist_self          := by simp [abs_zero],
   eq_of_dist_eq_zero := by simp [add_neg_eq_zero],
-  dist_comm          := assume x y, by rw [complex.abs_sub],
+  dist_comm          := assume x y, complex.abs_sub _ _,
   dist_triangle      := assume x y z, complex.abs_sub_le _ _ _ }
 
 theorem dist_eq (x y : ℂ) : dist x y = (x - y).abs := rfl

analysis/ennreal.lean

@@ -13,29 +13,6 @@ variables {α : Type*} {β : Type*} {γ : Type*}
 
 local notation `∞` := ennreal.infinity
 
-namespace topological_space
-
-lemma tendsto_nhds_generate_from {m : α → β} {f : filter α} {g : set (set β)} {b : β}
-  (h : ∀s∈g, b ∈ s → m ⁻¹' s ∈ f.sets) : tendsto m f (@nhds β (generate_from g) b) :=
-by rw [nhds_generate_from]; exact
-  (tendsto_infi.2 $ assume s, tendsto_infi.2 $ assume ⟨hbs, hsg⟩, tendsto_principal.2 $ h s hsg hbs)
-
-lemma prod_mem_nhds_sets [topological_space α] [topological_space β]
-  {s : set α} {t : set β} {a : α} {b : β} (ha : s ∈ (nhds a).sets) (hb : t ∈ (nhds b).sets) :
-  set.prod s t ∈ (nhds (a, b)).sets :=
-by rw [nhds_prod_eq]; exact prod_mem_prod ha hb
-
-lemma nhds_swap [topological_space α] [topological_space β] (a : α) (b : β) :
-  nhds (a, b) = (nhds (b, a)).map prod.swap :=
-by rw [nhds_prod_eq, filter.prod_comm, nhds_prod_eq]; refl
-
-lemma tendsto_prod_mk_nhds [topological_space α] [topological_space β] {a : α} {b : β} {f : filter γ}
-  {ma : γ → α} {mb : γ → β} (ha : tendsto ma f (nhds a)) (hb : tendsto mb f (nhds b)) :
-  tendsto (λc, (ma c, mb c)) f (nhds (a, b)) :=
-by rw [nhds_prod_eq]; exact filter.tendsto.prod_mk ha hb
-
-end topological_space
-
 namespace ennreal
 variables {a b c d : ennreal} {r p q : nnreal}
 
@@ -106,7 +83,7 @@ by rw [embedding_coe.2, map_nhds_induced_eq coe_image_univ_mem_nhds]
 lemma nhds_coe_coe {r p : nnreal} : nhds ((r : ennreal), (p : ennreal)) =
   (nhds (r, p)).map (λp:nnreal×nnreal, (p.1, p.2)) :=
 begin
-  rw [(embedding_prod_mk embedding_coe embedding_coe).2, map_nhds_induced_eq],
+  rw [(embedding_prod_mk embedding_coe embedding_coe).map_nhds_eq],
   rw [← univ_prod_univ, ← prod_image_image_eq],
   exact prod_mem_nhds_sets coe_image_univ_mem_nhds coe_image_univ_mem_nhds
 end

analysis/metric_space.lean

@@ -9,7 +9,7 @@ Many definitions and theorems expected on metric spaces are already introduced o
 topological spaces. For example:
   open and closed sets, compactness, completeness, continuity and uniform continuity
 -/
-import data.real.basic analysis.topology.topological_structures
+import data.real.nnreal analysis.topology.topological_structures
 open lattice set filter classical
 noncomputable theory
 
@@ -37,14 +37,19 @@ uniform_space.of_core {
   symm       := tendsto_infi.2 $ assume ε, tendsto_infi.2 $ assume h,
     tendsto_infi' ε $ tendsto_infi' h $ tendsto_principal_principal.2 $ by simp [dist_comm] }
 
+/-- The distance function (given an ambient metric space on `α`), which returns
+  a nonnegative real number `dist x y` given `x y : α`. -/
+class has_dist (α : Type*) := (dist : α → α → ℝ)
+
+export has_dist (dist)
+
 /-- Metric space
 
 Each metric space induces a canonical `uniform_space` and hence a canonical `topological_space`.
 This is enforced in the type class definition, by extending the `uniform_space` structure. When
 instantiating a `metric_space` structure, the uniformity fields are not necessary, they will be
 filled in by default. -/
-class metric_space (α : Type u) : Type u :=
-(dist : α → α → ℝ)
+class metric_space (α : Type u) extends has_dist α : Type u :=
 (dist_self : ∀ x : α, dist x x = 0)
 (eq_of_dist_eq_zero : ∀ {x y : α}, dist x y = 0 → x = y)
 (dist_comm : ∀ x y : α, dist x y = dist y x)
@@ -65,10 +70,6 @@ variables [metric_space α]
 instance metric_space.to_uniform_space' : uniform_space α :=
 metric_space.to_uniform_space α
 
-/-- The distance function (given an ambient metric space on `α`), which returns
-  a nonnegative real number `dist x y` given `x y : α`. -/
-def dist : α → α → ℝ := metric_space.dist
-
 @[simp] theorem dist_self (x : α) : dist x x = 0 := metric_space.dist_self x
 
 theorem eq_of_dist_eq_zero {x y : α} : dist x y = 0 → x = y :=
@@ -111,6 +112,39 @@ by simpa [le_antisymm_iff, dist_nonneg] using @dist_eq_zero _ _ x y
 @[simp] theorem dist_pos {x y : α} : 0 < dist x y ↔ x ≠ y :=
 by simpa [-dist_le_zero] using not_congr (@dist_le_zero _ _ x y)
 
+
+section
+variables [metric_space α]
+
+def nndist (a b : α) : nnreal := ⟨dist a b, dist_nonneg⟩
+
+@[simp] lemma nndist_self (a : α) : nndist a a = 0 := (nnreal.coe_eq_zero _).1 (dist_self a)
+
+@[simp] lemma coe_dist (a b : α) : (nndist a b : ℝ) = dist a b := rfl
+
+theorem eq_of_nndist_eq_zero {x y : α} : nndist x y = 0 → x = y :=
+by simpa [nnreal.eq_iff.symm] using @eq_of_dist_eq_zero α _ x y
+
+theorem nndist_comm (x y : α) : nndist x y = nndist y x :=
+by simpa [nnreal.eq_iff.symm] using dist_comm x y
+
+@[simp] theorem nndist_eq_zero {x y : α} : nndist x y = 0 ↔ x = y :=
+by simpa [nnreal.eq_iff.symm]
+
+@[simp] theorem zero_eq_nndist {x y : α} : 0 = nndist x y ↔ x = y :=
+by simpa [nnreal.eq_iff.symm]
+
+theorem nndist_triangle (x y z : α) : nndist x z ≤ nndist x y + nndist y z :=
+by simpa [nnreal.coe_le] using dist_triangle x y z
+
+theorem nndist_triangle_left (x y z : α) : nndist x y ≤ nndist z x + nndist z y :=
+by simpa [nnreal.coe_le] using dist_triangle_left x y z
+
+theorem nndist_triangle_right (x y z : α) : nndist x y ≤ nndist x z + nndist y z :=
+by simpa [nnreal.coe_le] using dist_triangle_right x y z
+
+end
+
 /- instantiate metric space as a topology -/
 variables {x y z : α} {ε ε₁ ε₂ : ℝ} {s : set α}
 
@@ -270,7 +304,7 @@ instance : metric_space ℝ :=
 { dist               := λx y, abs (x - y),
   dist_self          := by simp [abs_zero],
   eq_of_dist_eq_zero := by simp [add_neg_eq_zero],
-  dist_comm          := assume x y, by rw [abs_sub],
+  dist_comm          := assume x y, abs_sub _ _,
   dist_triangle      := assume x y z, abs_sub_le _ _ _ }
 
 theorem real.dist_eq (x y : ℝ) : dist x y = abs (x - y) := rfl
@@ -296,7 +330,7 @@ end
 def metric_space.replace_uniformity {α} [U : uniform_space α] (m : metric_space α)
   (H : @uniformity _ U = @uniformity _ (metric_space.to_uniform_space α)) :
   metric_space α :=
-{ dist               := @dist _ m,
+{ dist               := @dist _ m.to_has_dist,
   dist_self          := dist_self,
   eq_of_dist_eq_zero := @eq_of_dist_eq_zero _ _,
   dist_comm          := dist_comm,
@@ -410,6 +444,36 @@ by rw [← nhds_vmap_dist a, tendsto_vmap_iff]
 theorem is_closed_ball : is_closed (closed_ball x ε) :=
 is_closed_le (continuous_dist continuous_id continuous_const) continuous_const
 
+section pi
+open finset lattice
+variables {π : β → Type*} [fintype β] [∀b, metric_space (π b)]
+
+instance has_dist_pi : has_dist (Πb, π b) :=
+⟨λf g, ((finset.sup univ (λb, nndist (f b) (g b)) : nnreal) : ℝ)⟩
+
+lemma dist_pi_def (f g : Πb, π b) :
+  dist f g = (finset.sup univ (λb, nndist (f b) (g b)) : nnreal) := rfl
+
+instance metric_space_pi : metric_space (Πb, π b) :=
+{ dist := dist,
+  dist_self := assume f, (nnreal.coe_eq_zero _).2 $ bot_unique $ finset.sup_le $ by simp,
+  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,
+        finset.sup_le_iff],
+      assume b hb,
+      exact le_trans (nndist_triangle _ (g b) _) (add_le_add (le_sup hb) (le_sup hb))
+    end,
+  eq_of_dist_eq_zero := assume f g eq0,
+    begin
+      simp only [dist_pi_def, nnreal.coe_eq_zero, nnreal.bot_eq_zero.symm, eq_bot_iff,
+        finset.sup_le_iff] at eq0,
+      exact (funext $ assume b, eq_of_nndist_eq_zero $ bot_unique $ eq0 b $ mem_univ b),
+    end }
+
+end pi
+
 lemma lebesgue_number_lemma_of_metric
   {s : set α} {ι} {c : ι → set α} (hs : compact s)
   (hc₁ : ∀ i, is_open (c i)) (hc₂ : s ⊆ ⋃ i, c i) :

analysis/nnreal.lean

@@ -12,7 +12,8 @@ open set topological_space
 namespace nnreal
 local notation ` ℝ≥0 ` := nnreal
 
-instance : topological_space ℝ≥0 := subtype.topological_space
+instance : metric_space ℝ≥0 := by unfold nnreal; apply_instance
+instance : topological_space ℝ≥0 := infer_instance
 
 instance : topological_semiring ℝ≥0 :=
 { continuous_mul :=

analysis/topology/continuity.lean

@@ -346,6 +346,10 @@ le_antisymm
         is_open_inter is_open_t is_open_s'',
         ⟨a_in_t, a_in_s'⟩⟩))
 
+lemma embedding.map_nhds_eq [topological_space α] [topological_space β] {f : α → β} (hf : embedding f) (a : α)
+  (h : f '' univ ∈ (nhds (f a)).sets) : (nhds a).map f = nhds (f a) :=
+by rw [hf.2]; exact map_nhds_induced_eq h
+
 lemma closure_induced [t : topological_space β] {f : α → β} {a : α} {s : set α}
   (hf : ∀x y, f x = f y → x = y) :
   a ∈ @closure α (topological_space.induced f t) s ↔ f a ∈ closure (f '' s) :=
@@ -392,6 +396,18 @@ is_open_inter (continuous_fst s hs) (continuous_snd t ht)
 lemma nhds_prod_eq {a : α} {b : β} : nhds (a, b) = filter.prod (nhds a) (nhds b) :=
 by rw [filter.prod, prod.topological_space, nhds_sup, nhds_induced_eq_vmap, nhds_induced_eq_vmap]
 
+lemma prod_mem_nhds_sets {s : set α} {t : set β} {a : α} {b : β}
+  (ha : s ∈ (nhds a).sets) (hb : t ∈ (nhds b).sets) : set.prod s t ∈ (nhds (a, b)).sets :=
+by rw [nhds_prod_eq]; exact prod_mem_prod ha hb
+
+lemma nhds_swap (a : α) (b : β) : nhds (a, b) = (nhds (b, a)).map prod.swap :=
+by rw [nhds_prod_eq, filter.prod_comm, nhds_prod_eq]; refl
+
+lemma tendsto_prod_mk_nhds {γ} {a : α} {b : β} {f : filter γ} {ma : γ → α} {mb : γ → β}
+  (ha : tendsto ma f (nhds a)) (hb : tendsto mb f (nhds b)) :
+  tendsto (λc, (ma c, mb c)) f (nhds (a, b)) :=
+by rw [nhds_prod_eq]; exact filter.tendsto.prod_mk ha hb
+
 lemma prod_generate_from_generate_from_eq {s : set (set α)} {t : set (set β)}
   (hs : ⋃₀ s = univ) (ht : ⋃₀ t = univ) :
   @prod.topological_space α β (generate_from s) (generate_from t) =

analysis/topology/topological_space.lean

@@ -739,6 +739,11 @@ le_antisymm
     end,
     this s hs as)
 
+lemma tendsto_nhds_generate_from {β : Type*} {m : α → β} {f : filter α} {g : set (set β)} {b : β}
+  (h : ∀s∈g, b ∈ s → m ⁻¹' s ∈ f.sets) : tendsto m f (@nhds β (generate_from g) b) :=
+by rw [nhds_generate_from]; exact
+  (tendsto_infi.2 $ assume s, tendsto_infi.2 $ assume ⟨hbs, hsg⟩, tendsto_principal.2 $ h s hsg hbs)
+
 end topological_space
 
 section lattice