From 8572c6b07d85af3e6134aa7a286714a1052dd37d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Johannes=20H=C3=B6lzl?= Date: Mon, 28 Jan 2019 14:18:30 +0100 Subject: [PATCH] feat(topology): prove continuity of nndist and edist; `ball a r` is a metric space --- src/analysis/normed_space/basic.lean | 8 ++ src/data/real/ennreal.lean | 15 +++- src/topology/instances/ennreal.lean | 91 ++++++++++++++++++++ src/topology/instances/nnreal.lean | 3 +- src/topology/metric_space/basic.lean | 16 ++++ src/topology/metric_space/emetric_space.lean | 14 ++- 6 files changed, 141 insertions(+), 6 deletions(-) diff --git a/src/analysis/normed_space/basic.lean b/src/analysis/normed_space/basic.lean index 7ce5cde0c25af..127beced156af 100644 --- a/src/analysis/normed_space/basic.lean +++ b/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 diff --git a/src/data/real/ennreal.lean b/src/data/real/ennreal.lean index 8357f9260a83f..f26abe08449f8 100644 --- a/src/data/real/ennreal.lean +++ b/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 _ _ diff --git a/src/topology/instances/ennreal.lean b/src/topology/instances/ennreal.lean index 9af51cf74f88c..552bf85336181 100644 --- a/src/topology/instances/ennreal.lean +++ b/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 diff --git a/src/topology/instances/nnreal.lean b/src/topology/instances/nnreal.lean index babf565845443..3272ac2f11d3f 100644 --- a/src/topology/instances/nnreal.lean +++ b/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 \ No newline at end of file +end nnreal diff --git a/src/topology/metric_space/basic.lean b/src/topology/metric_space/basic.lean index 9df229432e94b..bc5908935018f 100644 --- a/src/topology/metric_space/basic.lean +++ b/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 α} diff --git a/src/topology/metric_space/emetric_space.lean b/src/topology/metric_space/emetric_space.lean index f6ac36042483b..47419aa03d8e0 100644 --- a/src/topology/metric_space/emetric_space.lean +++ b/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) :=