metric_from_comparisons

formal source

 190    The idea: if we have enough comparative recognizers that collectively
 191    separate all points and respect a common distance function, then
 192    that distance function is "visible" through the comparisons. -/
 193theorem metric_from_comparisons {ι : Type*} [Nonempty ι]
 194    (R_family : ι → ComparativeRecognizer C E)
 195    (gt_events : ι → Set E)
 196    (d : C → C → ℝ)
 197    (hsep : SeparatesPoints R_family gt_events)
 198    (hcompat : ∀ i, MetricCompatible (R_family i) (gt_events i) d) :
 199    -- If c₁ ≠ c₂, then d(c₁, c₂) > 0
 200    ∀ c₁ c₂, c₁ ≠ c₂ → 0 < d c₁ c₂ := by
 201  intro c₁ c₂ hne
 202  obtain ⟨i, hsep_i⟩ := hsep c₁ c₂ hne
 203  exact (hcompat i).dist_pos_of_separated hsep_i
 204
 205/-! ## The Recognition Distance -/
 206
 207/-- A recognition distance is a pseudometric derived from a family of
 208    comparative recognizers. -/
 209structure RecognitionDistance (C : Type*) where
 210  /-- The distance function -/
 211  dist : C → C → ℝ
 212  /-- Non-negativity -/
 213  dist_nonneg : ∀ c₁ c₂, 0 ≤ dist c₁ c₂
 214  /-- Self-distance is zero -/
 215  dist_self : ∀ c, dist c c = 0
 216  /-- Symmetry -/
 217  dist_symm : ∀ c₁ c₂, dist c₁ c₂ = dist c₂ c₁
 218  /-- Triangle inequality -/
 219  dist_triangle : ∀ c₁ c₂ c₃, dist c₁ c₃ ≤ dist c₁ c₂ + dist c₂ c₃
 220
 221/-- A recognition distance is a metric (not just pseudometric) when
 222    d(c₁, c₂) = 0 implies c₁ = c₂ -/
 223def RecognitionDistance.IsMetric (d : RecognitionDistance C) : Prop :=