feat(topology/urysohns_lemma): Urysohn's lemma (#6967)

Author: urkud

src/algebra/ordered_ring.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro
 -/
 import algebra.ordered_group
+import algebra.invertible
 import data.set.intervals.basic
 
 set_option old_structure_cmd true
@@ -322,12 +323,33 @@ lemma pos_of_mul_pos_left (h : 0 < a * b) (ha : 0 ≤ a) : 0 < b :=
 lemma pos_of_mul_pos_right (h : 0 < a * b) (hb : 0 ≤ b) : 0 < a :=
 ((pos_and_pos_or_neg_and_neg_of_mul_pos h).resolve_right $ λ h, h.2.not_le hb).1
 
+@[simp] lemma inv_of_pos [invertible a] : 0 < ⅟a ↔ 0 < a :=
+begin
+  have : 0 < a * ⅟a, by simp only [mul_inv_of_self, zero_lt_one],
+  exact ⟨λ h, pos_of_mul_pos_right this h.le, λ h, pos_of_mul_pos_left this h.le⟩
+end
+
+@[simp] lemma inv_of_nonpos [invertible a] : ⅟a ≤ 0 ↔ a ≤ 0 :=
+by simp only [← not_lt, inv_of_pos]
+
 lemma nonneg_of_mul_nonneg_left (h : 0 ≤ a * b) (h1 : 0 < a) : 0 ≤ b :=
 le_of_not_gt (assume h2 : b < 0, (mul_neg_of_pos_of_neg h1 h2).not_le h)
 
 lemma nonneg_of_mul_nonneg_right (h : 0 ≤ a * b) (h1 : 0 < b) : 0 ≤ a :=
 le_of_not_gt (assume h2 : a < 0, (mul_neg_of_neg_of_pos h2 h1).not_le h)
 
+@[simp] lemma inv_of_nonneg [invertible a] : 0 ≤ ⅟a ↔ 0 ≤ a :=
+begin
+  have : 0 < a * ⅟a, by simp only [mul_inv_of_self, zero_lt_one],
+  exact ⟨λ h, (pos_of_mul_pos_right this h).le, λ h, (pos_of_mul_pos_left this h).le⟩
+end
+
+@[simp] lemma inv_of_lt_zero [invertible a] : ⅟a < 0 ↔ a < 0 :=
+by simp only [← not_le, inv_of_nonneg]
+
+@[simp] lemma inv_of_le_one [invertible a] (h : 1 ≤ a) : ⅟a ≤ 1 :=
+mul_inv_of_self a ▸ le_mul_of_one_le_left (inv_of_nonneg.2 $ zero_le_one.trans h) h
+
 lemma neg_of_mul_neg_left (h : a * b < 0) (h1 : 0 ≤ a) : b < 0 :=
 lt_of_not_ge (assume h2 : b ≥ 0, (mul_nonneg h1 h2).not_lt h)
 

src/analysis/normed_space/add_torsor.lean

@@ -280,6 +280,22 @@ hf.vsub hg
 
 end
 
+section
+
+variables {R : Type*} [ring R] [topological_space R] [semimodule R V] [has_continuous_smul R V]
+
+lemma filter.tendsto.line_map {l : filter α} {f₁ f₂ : α → P} {g : α → R} {p₁ p₂ : P} {c : R}
+  (h₁ : tendsto f₁ l (𝓝 p₁)) (h₂ : tendsto f₂ l (𝓝 p₂)) (hg : tendsto g l (𝓝 c)) :
+  tendsto (λ x, affine_map.line_map (f₁ x) (f₂ x) (g x)) l (𝓝 $ affine_map.line_map p₁ p₂ c) :=
+(hg.smul (h₂.vsub h₁)).vadd h₁
+
+lemma filter.tendsto.midpoint [invertible (2:R)] {l : filter α} {f₁ f₂ : α → P} {p₁ p₂ : P}
+  (h₁ : tendsto f₁ l (𝓝 p₁)) (h₂ : tendsto f₂ l (𝓝 p₂)) :
+  tendsto (λ x, midpoint R (f₁ x) (f₂ x)) l (𝓝 $ midpoint R p₁ p₂) :=
+h₁.line_map h₂ tendsto_const_nhds
+
+end
+
 variables {V' : Type*} {P' : Type*} [normed_group V'] [metric_space P'] [normed_add_torsor V' P']
 
 /-- The map `g` from `V1` to `V2` corresponding to a map `f` from `P1`
@@ -347,9 +363,23 @@ by rw [midpoint_comm, dist_midpoint_left, dist_comm]
   dist p₂ (midpoint 𝕜 p₁ p₂) = ∥(2:𝕜)∥⁻¹ * dist p₁ p₂ :=
 by rw [dist_comm, dist_midpoint_right]
 
+lemma dist_midpoint_midpoint_le' (p₁ p₂ p₃ p₄ : P) :
+  dist (midpoint 𝕜 p₁ p₂) (midpoint 𝕜 p₃ p₄) ≤ (dist p₁ p₃ + dist p₂ p₄) / ∥(2 : 𝕜)∥ :=
+begin
+  rw [dist_eq_norm_vsub V, dist_eq_norm_vsub V, dist_eq_norm_vsub V, midpoint_vsub_midpoint];
+    try { apply_instance },
+  rw [midpoint_eq_smul_add, norm_smul, inv_of_eq_inv, normed_field.norm_inv, ← div_eq_inv_mul],
+  exact div_le_div_of_le_of_nonneg (norm_add_le _ _) (norm_nonneg _),
+end
+
 end normed_space
 
 variables [normed_space ℝ V] [normed_space ℝ V']
+
+lemma dist_midpoint_midpoint_le (p₁ p₂ p₃ p₄ : V) :
+  dist (midpoint ℝ p₁ p₂) (midpoint ℝ p₃ p₄) ≤ (dist p₁ p₃ + dist p₂ p₄) / 2 :=
+by simpa using dist_midpoint_midpoint_le' p₁ p₂ p₃ p₄
+
 include V'
 
 /-- A continuous map between two normed affine spaces is an affine map provided that

src/data/indicator_function.lean

@@ -265,13 +265,22 @@ lemma indicator_sub {G} [add_group G] (s : set α) (f g : α → G) :
   indicator s (λa, f a - g a) = λa, indicator s f a - indicator s g a :=
 (indicator_hom G s).map_sub f g
 
-@[to_additive indicator_compl''] lemma mul_indicator_compl (s : set α) (f : α → G) :
+@[to_additive indicator_compl'] lemma mul_indicator_compl (s : set α) (f : α → G) :
   mul_indicator sᶜ f = f * (mul_indicator s f)⁻¹ :=
 eq_mul_inv_of_mul_eq $ s.mul_indicator_compl_mul_self f
 
 lemma indicator_compl {G} [add_group G] (s : set α) (f : α → G) :
   indicator sᶜ f = f - indicator s f :=
-by rw [sub_eq_add_neg, indicator_compl'']
+by rw [sub_eq_add_neg, indicator_compl']
+
+@[to_additive indicator_diff'] lemma mul_indicator_diff (h : s ⊆ t) (f : α → G) :
+  mul_indicator (t \ s) f = mul_indicator t f * (mul_indicator s f)⁻¹ :=
+eq_mul_inv_of_mul_eq $ by rw [pi.mul_def, ← mul_indicator_union_of_disjoint disjoint_diff.symm f,
+  diff_union_self, union_eq_self_of_subset_right h]
+
+lemma indicator_diff {G : Type*} [add_group G] {s t : set α} (h : s ⊆ t) (f : α → G) :
+  indicator (t \ s) f = indicator t f - indicator s f :=
+by rw [indicator_diff' h, sub_eq_add_neg]
 
 end group
 
@@ -373,19 +382,19 @@ by simp [indicator, ← ite_and]
 end monoid_with_zero
 
 section order
-variables [has_one M] [preorder M] {s t : set α} {f g : α → M} {a : α}
+variables [has_one M] [preorder M] {s t : set α} {f g : α → M} {a : α} {y : M}
 
-@[to_additive] lemma mul_indicator_apply_le' (hfg : a ∈ s → f a ≤ g a) (hg : a ∉ s → 1 ≤ g a) :
-  mul_indicator s f a ≤ g a :=
+@[to_additive] lemma mul_indicator_apply_le' (hfg : a ∈ s → f a ≤ y) (hg : a ∉ s → 1 ≤ y) :
+  mul_indicator s f a ≤ y :=
 if ha : a ∈ s then by simpa [ha] using hfg ha else by simpa [ha] using hg ha
 
 @[to_additive] lemma mul_indicator_le' (hfg : ∀ a ∈ s, f a ≤ g a) (hg : ∀ a ∉ s, 1 ≤ g a) :
   mul_indicator s f ≤ g :=
 λ a, mul_indicator_apply_le' (hfg _) (hg _)
 
-@[to_additive] lemma le_mul_indicator_apply (hfg : a ∈ s → f a ≤ g a) (hf : a ∉ s → f a ≤ 1) :
-  f a ≤ mul_indicator s g a :=
-if ha : a ∈ s then by simpa [ha] using hfg ha else by simpa [ha] using hf ha
+@[to_additive] lemma le_mul_indicator_apply {y} (hfg : a ∈ s → y ≤ g a) (hf : a ∉ s → y ≤ 1) :
+  y ≤ mul_indicator s g a :=
+@mul_indicator_apply_le' α (order_dual M) ‹_› _ _ _ _ _ hfg hf
 
 @[to_additive] lemma le_mul_indicator (hfg : ∀ a ∈ s, f a ≤ g a) (hf : ∀ a ∉ s, f a ≤ 1) :
   f ≤ mul_indicator s g :=

src/linear_algebra/affine_space/midpoint.lean

@@ -130,6 +130,10 @@ calc midpoint R x y +ᵥ midpoint R x y = midpoint R x y +ᵥ midpoint R y x : b
 lemma midpoint_zero_add (x y : V) : midpoint R 0 (x + y) = midpoint R x y :=
 (midpoint_eq_midpoint_iff_vsub_eq_vsub R).2 $ by simp [sub_add_eq_sub_sub_swap]
 
+lemma midpoint_eq_smul_add (x y : V) : midpoint R x y = (⅟2 : R) • (x + y) :=
+by rw [midpoint_eq_iff, point_reflection_apply, vsub_eq_sub, vadd_eq_add, sub_add_eq_add_sub,
+  ← two_smul R, smul_smul, mul_inv_of_self, one_smul, add_sub_cancel']
+
 end
 
 lemma line_map_inv_two {R : Type*} {V P : Type*} [division_ring R] [char_zero R]

src/linear_algebra/affine_space/ordered.lean

@@ -182,6 +182,18 @@ lemma right_lt_line_map_iff_lt (h : r < 1) : b < line_map a b r ↔ b < a :=
 
 end ordered_ring
 
+section linear_ordered_ring
+
+variables [linear_ordered_ring k] [ordered_add_comm_group E] [semimodule k E]
+  [ordered_semimodule k E] [invertible (2:k)] {a a' b b' : E} {r r' : k}
+
+lemma midpoint_le_midpoint (ha : a ≤ a') (hb : b ≤ b') :
+  midpoint k a b ≤ midpoint k a' b' :=
+line_map_mono_endpoints ha hb (inv_of_nonneg.2 zero_le_two) $
+  inv_of_le_one one_le_two
+
+end linear_ordered_ring
+
 section linear_ordered_field
 
 variables [linear_ordered_field k] [ordered_add_comm_group E]

src/topology/metric_space/basic.lean

@@ -381,6 +381,11 @@ theorem uniformity_basis_dist_inv_nat_pos :
 metric.mk_uniformity_basis (λ n hn, div_pos zero_lt_one $ nat.cast_pos.2 hn)
   (λ ε ε0, let ⟨n, hn⟩ := exists_nat_one_div_lt ε0 in ⟨n+1, nat.succ_pos n, hn.le⟩)
 
+theorem uniformity_basis_dist_pow {r : ℝ} (h0 : 0 < r) (h1 : r < 1) :
+  (𝓤 α).has_basis (λ n:ℕ, true) (λ n:ℕ, {p:α×α | dist p.1 p.2 < r ^ n }) :=
+metric.mk_uniformity_basis (λ n hn, pow_pos h0 _)
+  (λ ε ε0, let ⟨n, hn⟩ := exists_pow_lt_of_lt_one ε0 h1 in ⟨n, trivial, hn.le⟩)
+
 theorem uniformity_basis_dist_lt {R : ℝ} (hR : 0 < R) :
   (𝓤 α).has_basis (λ r : ℝ, 0 < r ∧ r < R) (λ r, {p : α × α | dist p.1 p.2 < r}) :=
 metric.mk_uniformity_basis (λ r, and.left) $ λ r hr,
@@ -412,6 +417,11 @@ theorem uniformity_basis_dist_le :
   (𝓤 α).has_basis (λ ε : ℝ, 0 < ε) (λ ε, {p:α×α | dist p.1 p.2 ≤ ε}) :=
 metric.mk_uniformity_basis_le (λ _, id) (λ ε ε₀, ⟨ε, ε₀, le_refl ε⟩)
 
+theorem uniformity_basis_dist_le_pow {r : ℝ} (h0 : 0 < r) (h1 : r < 1) :
+  (𝓤 α).has_basis (λ n:ℕ, true) (λ n:ℕ, {p:α×α | dist p.1 p.2 ≤ r ^ n }) :=
+metric.mk_uniformity_basis_le (λ n hn, pow_pos h0 _)
+  (λ ε ε0, let ⟨n, hn⟩ := exists_pow_lt_of_lt_one ε0 h1 in ⟨n, trivial, hn.le⟩)
+
 theorem mem_uniformity_dist {s : set (α×α)} :
   s ∈ 𝓤 α ↔ (∃ε>0, ∀{a b:α}, dist a b < ε → (a, b) ∈ s) :=
 uniformity_basis_dist.mem_uniformity_iff
@@ -559,6 +569,14 @@ theorem nhds_basis_ball_inv_nat_pos :
   (𝓝 x).has_basis (λ n, 0<n) (λ n:ℕ, ball x (1 / ↑n)) :=
 nhds_basis_uniformity uniformity_basis_dist_inv_nat_pos
 
+theorem nhds_basis_ball_pow {r : ℝ} (h0 : 0 < r) (h1 : r < 1) :
+  (𝓝 x).has_basis (λ n, true) (λ n:ℕ, ball x (r ^ n)) :=
+nhds_basis_uniformity (uniformity_basis_dist_pow h0 h1)
+
+theorem nhds_basis_closed_ball_pow {r : ℝ} (h0 : 0 < r) (h1 : r < 1) :
+  (𝓝 x).has_basis (λ n, true) (λ n:ℕ, closed_ball x (r ^ n)) :=
+nhds_basis_uniformity (uniformity_basis_dist_le_pow h0 h1)
+
 theorem is_open_iff : is_open s ↔ ∀x∈s, ∃ε>0, ball x ε ⊆ s :=
 by simp only [is_open_iff_mem_nhds, mem_nhds_iff]
 
@@ -820,6 +838,26 @@ theorem real.dist_eq (x y : ℝ) : dist x y = abs (x - y) := rfl
 theorem real.dist_0_eq_abs (x : ℝ) : dist x 0 = abs x :=
 by simp [real.dist_eq]
 
+theorem real.dist_left_le_of_mem_interval {x y z : ℝ} (h : y ∈ interval x z) :
+  dist x y ≤ dist x z :=
+by simpa only [dist_comm x] using abs_sub_left_of_mem_interval h
+
+theorem real.dist_right_le_of_mem_interval {x y z : ℝ} (h : y ∈ interval x z) :
+  dist y z ≤ dist x z :=
+by simpa only [dist_comm _ z] using abs_sub_right_of_mem_interval h
+
+theorem real.dist_le_of_mem_interval {x y x' y' : ℝ} (hx : x ∈ interval x' y')
+  (hy : y ∈ interval x' y') : dist x y ≤ dist x' y' :=
+abs_sub_le_of_subinterval $ interval_subset_interval (by rwa interval_swap) (by rwa interval_swap)
+
+theorem real.dist_le_of_mem_Icc {x y x' y' : ℝ} (hx : x ∈ Icc x' y') (hy : y ∈ Icc x' y') :
+  dist x y ≤ dist x' y' :=
+real.dist_le_of_mem_interval (Icc_subset_interval hx) (Icc_subset_interval hy)
+
+theorem real.dist_le_of_mem_Icc_01 {x y : ℝ} (hx : x ∈ Icc (0:ℝ) 1) (hy : y ∈ Icc (0:ℝ) 1) :
+  dist x y ≤ 1 :=
+by simpa [real.dist_eq] using real.dist_le_of_mem_Icc hx hy
+
 instance : order_topology ℝ :=
 order_topology_of_nhds_abs $ λ x,
   by simp only [nhds_basis_ball.eq_binfi, ball, real.dist_eq, abs_sub]