|
| 1 | +/- |
| 2 | +Copyright (c) 2015, 2017 Jeremy Avigad. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Jeremy Avigad, Robert Y. Lewis, Johannes Hölzl, Mario Carneiro, Sébastien Gouëzel |
| 5 | +-/ |
| 6 | +import Mathlib.Topology.EMetricSpace.Basic |
| 7 | +import Mathlib.Data.ENNReal.Real |
| 8 | + |
| 9 | +/-! |
| 10 | +# Diameters of sets in extended metric spaces |
| 11 | +
|
| 12 | +-/ |
| 13 | + |
| 14 | + |
| 15 | +open Set Filter Classical |
| 16 | + |
| 17 | +open scoped Uniformity Topology Filter NNReal ENNReal Pointwise |
| 18 | + |
| 19 | +universe u v w |
| 20 | + |
| 21 | +variable {α β : Type*} {s : Set α} {x y z : α} |
| 22 | + |
| 23 | +namespace EMetric |
| 24 | + |
| 25 | +section |
| 26 | +variable [PseudoEMetricSpace α] |
| 27 | + |
| 28 | +/-- The diameter of a set in a pseudoemetric space, named `EMetric.diam` -/ |
| 29 | +noncomputable def diam (s : Set α) := |
| 30 | + ⨆ (x ∈ s) (y ∈ s), edist x y |
| 31 | + |
| 32 | +theorem diam_eq_sSup (s : Set α) : diam s = sSup (image2 edist s s) := sSup_image2.symm |
| 33 | + |
| 34 | +theorem diam_le_iff {d : ℝ≥0∞} : diam s ≤ d ↔ ∀ x ∈ s, ∀ y ∈ s, edist x y ≤ d := by |
| 35 | + simp only [diam, iSup_le_iff] |
| 36 | + |
| 37 | +theorem diam_image_le_iff {d : ℝ≥0∞} {f : β → α} {s : Set β} : |
| 38 | + diam (f '' s) ≤ d ↔ ∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) ≤ d := by |
| 39 | + simp only [diam_le_iff, forall_mem_image] |
| 40 | + |
| 41 | +theorem edist_le_of_diam_le {d} (hx : x ∈ s) (hy : y ∈ s) (hd : diam s ≤ d) : edist x y ≤ d := |
| 42 | + diam_le_iff.1 hd x hx y hy |
| 43 | + |
| 44 | +/-- If two points belong to some set, their edistance is bounded by the diameter of the set -/ |
| 45 | +theorem edist_le_diam_of_mem (hx : x ∈ s) (hy : y ∈ s) : edist x y ≤ diam s := |
| 46 | + edist_le_of_diam_le hx hy le_rfl |
| 47 | + |
| 48 | +/-- If the distance between any two points in a set is bounded by some constant, this constant |
| 49 | +bounds the diameter. -/ |
| 50 | +theorem diam_le {d : ℝ≥0∞} (h : ∀ x ∈ s, ∀ y ∈ s, edist x y ≤ d) : diam s ≤ d := |
| 51 | + diam_le_iff.2 h |
| 52 | + |
| 53 | +/-- The diameter of a subsingleton vanishes. -/ |
| 54 | +theorem diam_subsingleton (hs : s.Subsingleton) : diam s = 0 := |
| 55 | + nonpos_iff_eq_zero.1 <| diam_le fun _x hx y hy => (hs hx hy).symm ▸ edist_self y ▸ le_rfl |
| 56 | + |
| 57 | +/-- The diameter of the empty set vanishes -/ |
| 58 | +@[simp] |
| 59 | +theorem diam_empty : diam (∅ : Set α) = 0 := |
| 60 | + diam_subsingleton subsingleton_empty |
| 61 | + |
| 62 | +/-- The diameter of a singleton vanishes -/ |
| 63 | +@[simp] |
| 64 | +theorem diam_singleton : diam ({x} : Set α) = 0 := |
| 65 | + diam_subsingleton subsingleton_singleton |
| 66 | + |
| 67 | +@[to_additive (attr := simp)] |
| 68 | +theorem diam_one [One α] : diam (1 : Set α) = 0 := |
| 69 | + diam_singleton |
| 70 | + |
| 71 | +theorem diam_iUnion_mem_option {ι : Type*} (o : Option ι) (s : ι → Set α) : |
| 72 | + diam (⋃ i ∈ o, s i) = ⨆ i ∈ o, diam (s i) := by cases o <;> simp |
| 73 | + |
| 74 | +theorem diam_insert : diam (insert x s) = max (⨆ y ∈ s, edist x y) (diam s) := |
| 75 | + eq_of_forall_ge_iff fun d => by |
| 76 | + simp only [diam_le_iff, forall_mem_insert, edist_self, edist_comm x, max_le_iff, iSup_le_iff, |
| 77 | + zero_le, true_and_iff, forall_and, and_self_iff, ← and_assoc] |
| 78 | + |
| 79 | +theorem diam_pair : diam ({x, y} : Set α) = edist x y := by |
| 80 | + simp only [iSup_singleton, diam_insert, diam_singleton, ENNReal.max_zero_right] |
| 81 | + |
| 82 | +theorem diam_triple : diam ({x, y, z} : Set α) = max (max (edist x y) (edist x z)) (edist y z) := by |
| 83 | + simp only [diam_insert, iSup_insert, iSup_singleton, diam_singleton, ENNReal.max_zero_right, |
| 84 | + ENNReal.sup_eq_max] |
| 85 | + |
| 86 | +/-- The diameter is monotonous with respect to inclusion -/ |
| 87 | +@[gcongr] |
| 88 | +theorem diam_mono {s t : Set α} (h : s ⊆ t) : diam s ≤ diam t := |
| 89 | + diam_le fun _x hx _y hy => edist_le_diam_of_mem (h hx) (h hy) |
| 90 | + |
| 91 | +/-- The diameter of a union is controlled by the diameter of the sets, and the edistance |
| 92 | +between two points in the sets. -/ |
| 93 | +theorem diam_union {t : Set α} (xs : x ∈ s) (yt : y ∈ t) : |
| 94 | + diam (s ∪ t) ≤ diam s + edist x y + diam t := by |
| 95 | + have A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ diam s + edist x y + diam t := fun a ha b hb => |
| 96 | + calc |
| 97 | + edist a b ≤ edist a x + edist x y + edist y b := edist_triangle4 _ _ _ _ |
| 98 | + _ ≤ diam s + edist x y + diam t := |
| 99 | + add_le_add (add_le_add (edist_le_diam_of_mem ha xs) le_rfl) (edist_le_diam_of_mem yt hb) |
| 100 | + refine diam_le fun a ha b hb => ?_ |
| 101 | + cases' (mem_union _ _ _).1 ha with h'a h'a <;> cases' (mem_union _ _ _).1 hb with h'b h'b |
| 102 | + · calc |
| 103 | + edist a b ≤ diam s := edist_le_diam_of_mem h'a h'b |
| 104 | + _ ≤ diam s + (edist x y + diam t) := le_self_add |
| 105 | + _ = diam s + edist x y + diam t := (add_assoc _ _ _).symm |
| 106 | + · exact A a h'a b h'b |
| 107 | + · have Z := A b h'b a h'a |
| 108 | + rwa [edist_comm] at Z |
| 109 | + · calc |
| 110 | + edist a b ≤ diam t := edist_le_diam_of_mem h'a h'b |
| 111 | + _ ≤ diam s + edist x y + diam t := le_add_self |
| 112 | + |
| 113 | +theorem diam_union' {t : Set α} (h : (s ∩ t).Nonempty) : diam (s ∪ t) ≤ diam s + diam t := by |
| 114 | + let ⟨x, ⟨xs, xt⟩⟩ := h |
| 115 | + simpa using diam_union xs xt |
| 116 | + |
| 117 | +theorem diam_closedBall {r : ℝ≥0∞} : diam (closedBall x r) ≤ 2 * r := |
| 118 | + diam_le fun a ha b hb => |
| 119 | + calc |
| 120 | + edist a b ≤ edist a x + edist b x := edist_triangle_right _ _ _ |
| 121 | + _ ≤ r + r := add_le_add ha hb |
| 122 | + _ = 2 * r := (two_mul r).symm |
| 123 | + |
| 124 | +theorem diam_ball {r : ℝ≥0∞} : diam (ball x r) ≤ 2 * r := |
| 125 | + le_trans (diam_mono ball_subset_closedBall) diam_closedBall |
| 126 | + |
| 127 | +theorem diam_pi_le_of_le {π : β → Type*} [Fintype β] [∀ b, PseudoEMetricSpace (π b)] |
| 128 | + {s : ∀ b : β, Set (π b)} {c : ℝ≥0∞} (h : ∀ b, diam (s b) ≤ c) : diam (Set.pi univ s) ≤ c := by |
| 129 | + refine diam_le fun x hx y hy => edist_pi_le_iff.mpr ?_ |
| 130 | + rw [mem_univ_pi] at hx hy |
| 131 | + exact fun b => diam_le_iff.1 (h b) (x b) (hx b) (y b) (hy b) |
| 132 | + |
| 133 | +end |
| 134 | + |
| 135 | +section |
| 136 | +variable [EMetricSpace β] {s : Set β} |
| 137 | + |
| 138 | +theorem diam_eq_zero_iff : diam s = 0 ↔ s.Subsingleton := |
| 139 | + ⟨fun h _x hx _y hy => edist_le_zero.1 <| h ▸ edist_le_diam_of_mem hx hy, diam_subsingleton⟩ |
| 140 | + |
| 141 | +theorem diam_pos_iff : 0 < diam s ↔ s.Nontrivial := by |
| 142 | + simp only [pos_iff_ne_zero, Ne, diam_eq_zero_iff, Set.not_subsingleton_iff] |
| 143 | + |
| 144 | +theorem diam_pos_iff' : 0 < diam s ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y := by |
| 145 | + simp only [diam_pos_iff, Set.Nontrivial, exists_prop] |
| 146 | + |
| 147 | +end |
| 148 | + |
| 149 | +end EMetric |
0 commit comments