English
The Hausdorff distance between the two optimal image ranges is bounded by the bound HD of f.
Русский
Расстояние Хаусдорфа между диапазонами изображений двух оптимальных инъекций ограничено величиной HD(f).
LaTeX
$$hausdorffDist( range(optimalGHInjl X Y), range(optimalGHInjr X Y) ) \le HD f$$
Lean4
/-- For any candidate `f`, `HD(f)` is larger than or equal to the Hausdorff distance in the
optimal coupling. This follows from the fact that `HD` of the optimal candidate is exactly
the Hausdorff distance in the optimal coupling, although we only prove here the inequality
we need. -/
theorem hausdorffDist_optimal_le_HD {f} (h : f ∈ candidatesB X Y) :
hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ HD f :=
by
refine le_trans (le_of_forall_gt_imp_ge_of_dense fun r hr => ?_) (HD_optimalGHDist_le X Y f h)
have A : ∀ x ∈ range (optimalGHInjl X Y), ∃ y ∈ range (optimalGHInjr X Y), dist x y ≤ r :=
by
rintro _ ⟨z, rfl⟩
have I1 : (⨆ x, ⨅ y, optimalGHDist X Y (inl x, inr y)) < r := lt_of_le_of_lt (le_max_left _ _) hr
have I2 : ⨅ y, optimalGHDist X Y (inl z, inr y) ≤ ⨆ x, ⨅ y, optimalGHDist X Y (inl x, inr y) :=
le_csSup (by simpa using HD_bound_aux1 _ 0) (mem_range_self _)
have I : ⨅ y, optimalGHDist X Y (inl z, inr y) < r := lt_of_le_of_lt I2 I1
rcases exists_lt_of_csInf_lt (range_nonempty _) I with ⟨r', ⟨z', rfl⟩, hr'⟩
exact ⟨optimalGHInjr X Y z', mem_range_self _, le_of_lt hr'⟩
refine hausdorffDist_le_of_mem_dist ?_ A ?_
· inhabit X
rcases A _ (mem_range_self default) with ⟨y, -, hy⟩
exact le_trans dist_nonneg hy
· rintro _ ⟨z, rfl⟩
have I1 : (⨆ y, ⨅ x, optimalGHDist X Y (inl x, inr y)) < r := lt_of_le_of_lt (le_max_right _ _) hr
have I2 : ⨅ x, optimalGHDist X Y (inl x, inr z) ≤ ⨆ y, ⨅ x, optimalGHDist X Y (inl x, inr y) :=
le_csSup (by simpa using HD_bound_aux2 _ 0) (mem_range_self _)
have I : ⨅ x, optimalGHDist X Y (inl x, inr z) < r := lt_of_le_of_lt I2 I1
rcases exists_lt_of_csInf_lt (range_nonempty _) I with ⟨r', ⟨z', rfl⟩, hr'⟩
refine ⟨optimalGHInjl X Y z', mem_range_self _, le_of_lt ?_⟩
rwa [dist_comm]
