The set of functions on α ⊕ β that are candidates distances to realize the minimum of the Hausdorff distances between α and β in a coupling

Version of the set of candidates in bounded_continuous_functions, to apply Arzela-Ascoli

candidates are bounded by max_var α β

Technical lemma to prove that candidates are Lipschitz

Candidates are Lipschitz

candidates give rise to elements of bounded_continuous_functions

The distance on α ⊕ β is a candidate

To apply Arzela-Ascoli, we need to check that the set of candidates is closed and equicontinuous. Equicontinuity follows from the Lipschitz control, we check closedness

Compactness of candidates (in bounded_continuous_functions) follows

We will then choose the candidate minimizing the Hausdorff distance. Except that we are not in a metric space setting, so we need to define our custom version of Hausdorff distance, called HD, and prove its basic properties.

Explicit bound on HD (dist). This means that when looking for minimizers it will be sufficient to look for functions with HD(f) bounded by this bound.

Conclude that HD, being Lipschitz, is continuous

With the optimal candidate, construct a premetric space structure on α ⊕ β, on which the predistance is given by the candidate. Then, we will identify points at 0 predistance to obtain a genuine metric space

A metric space which realizes the optimal coupling between α and β

Injection of α in the optimal coupling between α and β

The injection of α in the optimal coupling between α and β is an isometry.

Injection of β in the optimal coupling between α and β

The injection of β in the optimal coupling between α and β is an isometry.

The optimal coupling between two compact spaces α and β is still a compact space

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.