MetricCompatible

formal source

 171
 172/-- A comparative recognizer defines a "distance-like" function when it can
 173    distinguish "closer" from "farther" configurations. -/
 174structure MetricCompatible (R_cmp : ComparativeRecognizer C E) (gt_events : Set E)
 175    (d : C → C → ℝ) : Prop where
 176  /-- d(c,c) = 0 -/
 177  dist_self : ∀ c, d c c = 0
 178  /-- d(c₁,c₂) ≥ 0 -/
 179  dist_nonneg : ∀ c₁ c₂, 0 ≤ d c₁ c₂
 180  /-- d(c₁,c₂) = d(c₂,c₁) -/
 181  dist_symm : ∀ c₁ c₂, d c₁ c₂ = d c₂ c₁
 182  /-- If the recognizer *separates* `c₁,c₂`, then their distance is strictly positive. -/
 183  dist_pos_of_separated : ∀ {c₁ c₂ : C}, SeparatedBy R_cmp gt_events c₁ c₂ → 0 < d c₁ c₂
 184  /-- If c₁ ≤ c₂ (by comparison), then d(c₁, c₃) ≤ d(c₂, c₃) for all c₃ -/
 185  order_respects_dist : ∀ c₁ c₂ c₃, notGreaterThan R_cmp gt_events c₁ c₂ →
 186    d c₁ c₃ ≤ d c₂ c₃
 187
 188/-- **Key Theorem**: Many comparative recognizers can approximate a metric.
 189
 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