English
Simplification lemmas about ghDist_le_hausdorffDist and allied relations. (Abstract reductions between equivalent forms.)
Русский
Леммы упрощения о ghDist_le_hausdorffDist и их близких отношениях. (Обобщённые сокращения между эквивалентными формами.)
LaTeX
$$$$\text{[Simplicial lemmas ensuring equivalences of helper forms].$$$$
Lean4
/-- The optimal coupling constructed above realizes exactly the Gromov-Hausdorff distance,
essentially by design. -/
theorem hausdorffDist_optimal {X : Type u} [MetricSpace X] [CompactSpace X] [Nonempty X] {Y : Type v} [MetricSpace Y]
[CompactSpace Y] [Nonempty Y] :
hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) = ghDist X Y :=
by
inhabit X; inhabit Y
have A :
∀ p q : NonemptyCompacts ℓ_infty_ℝ,
⟦p⟧ = toGHSpace X →
⟦q⟧ = toGHSpace Y →
hausdorffDist (p : Set ℓ_infty_ℝ) q < diam (univ : Set X) + 1 + diam (univ : Set Y) →
hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤
hausdorffDist (p : Set ℓ_infty_ℝ) q :=
by
intro p q hp hq bound
rcases eq_toGHSpace_iff.1 hp with ⟨Φ, ⟨Φisom, Φrange⟩⟩
rcases eq_toGHSpace_iff.1 hq with ⟨Ψ, ⟨Ψisom, Ψrange⟩⟩
have I : diam (range Φ ∪ range Ψ) ≤ 2 * diam (univ : Set X) + 1 + 2 * diam (univ : Set Y) :=
by
rcases exists_mem_of_nonempty X with ⟨xX, _⟩
have : ∃ y ∈ range Ψ, dist (Φ xX) y < diam (univ : Set X) + 1 + diam (univ : Set Y) :=
by
rw [Ψrange]
have : Φ xX ∈ (p : Set _) := Φrange ▸ (mem_range_self _)
exact
exists_dist_lt_of_hausdorffDist_lt this bound
(hausdorffEdist_ne_top_of_nonempty_of_bounded p.nonempty q.nonempty p.isCompact.isBounded
q.isCompact.isBounded)
rcases this with ⟨y, hy, dy⟩
rcases mem_range.1 hy with ⟨z, hzy⟩
rw [← hzy] at dy
have DΦ : diam (range Φ) = diam (univ : Set X) := Φisom.diam_range
have DΨ : diam (range Ψ) = diam (univ : Set Y) := Ψisom.diam_range
calc
diam (range Φ ∪ range Ψ) ≤ diam (range Φ) + dist (Φ xX) (Ψ z) + diam (range Ψ) :=
diam_union (mem_range_self _) (mem_range_self _)
_ ≤ diam (univ : Set X) + (diam (univ : Set X) + 1 + diam (univ : Set Y)) + diam (univ : Set Y) :=
by
rw [DΦ, DΨ]
gcongr
_ = 2 * diam (univ : Set X) + 1 + 2 * diam (univ : Set Y) := by ring
let f : X ⊕ Y → ℓ_infty_ℝ := fun x =>
match x with
| inl y => Φ y
| inr z => Ψ z
let F : (X ⊕ Y) × (X ⊕ Y) → ℝ := fun p =>
dist (f p.1)
(f p.2)
-- check that the induced "distance" is a candidate
have Fgood : F ∈ candidates X Y :=
by
simp only [F, candidates, forall_const, dist_eq_zero, Set.mem_setOf_eq]
repeat' constructor
·
exact fun x y =>
calc
F (inl x, inl y) = dist (Φ x) (Φ y) := rfl
_ = dist x y := Φisom.dist_eq x y
·
exact fun x y =>
calc
F (inr x, inr y) = dist (Ψ x) (Ψ y) := rfl
_ = dist x y := Ψisom.dist_eq x y
· exact fun x y => dist_comm _ _
· exact fun x y z => dist_triangle _ _ _
·
exact fun x y =>
calc
F (x, y) ≤ diam (range Φ ∪ range Ψ) :=
by
have A : ∀ z : X ⊕ Y, f z ∈ range Φ ∪ range Ψ := by
intro z
cases z
· apply mem_union_left; apply mem_range_self
· apply mem_union_right; apply mem_range_self
refine dist_le_diam_of_mem ?_ (A _) (A _)
rw [Φrange, Ψrange]
exact (p ⊔ q).isCompact.isBounded
_ ≤ 2 * diam (univ : Set X) + 1 + 2 * diam (univ : Set Y) := I
let Fb := candidatesBOfCandidates F Fgood
have : hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ HD Fb :=
hausdorffDist_optimal_le_HD _ _ (candidatesBOfCandidates_mem F Fgood)
refine le_trans this (le_of_forall_gt_imp_ge_of_dense fun r hr => ?_)
have I1 : ∀ x : X, (⨅ y, Fb (inl x, inr y)) ≤ r := by
intro x
have : f (inl x) ∈ (p : Set _) := Φrange ▸ (mem_range_self _)
rcases
exists_dist_lt_of_hausdorffDist_lt this hr
(hausdorffEdist_ne_top_of_nonempty_of_bounded p.nonempty q.nonempty p.isCompact.isBounded
q.isCompact.isBounded) with
⟨z, zq, hz⟩
have : z ∈ range Ψ := by rwa [← Ψrange] at zq
rcases mem_range.1 this with ⟨y, hy⟩
calc
(⨅ y, Fb (inl x, inr y)) ≤ Fb (inl x, inr y) := ciInf_le (by simpa only [add_zero] using HD_below_aux1 0) y
_ = dist (Φ x) (Ψ y) := rfl
_ = dist (f (inl x)) z := by rw [hy]
_ ≤ r := le_of_lt hz
have I2 : ∀ y : Y, (⨅ x, Fb (inl x, inr y)) ≤ r := by
intro y
have : f (inr y) ∈ (q : Set _) := Ψrange ▸ (mem_range_self _)
rcases
exists_dist_lt_of_hausdorffDist_lt' this hr
(hausdorffEdist_ne_top_of_nonempty_of_bounded p.nonempty q.nonempty p.isCompact.isBounded
q.isCompact.isBounded) with
⟨z, zq, hz⟩
have : z ∈ range Φ := by rwa [← Φrange] at zq
rcases mem_range.1 this with ⟨x, hx⟩
calc
(⨅ x, Fb (inl x, inr y)) ≤ Fb (inl x, inr y) := ciInf_le (by simpa only [add_zero] using HD_below_aux2 0) x
_ = dist (Φ x) (Ψ y) := rfl
_ = dist z (f (inr y)) := by rw [hx]
_ ≤ r := le_of_lt hz
simp only [HD, ciSup_le I1, ciSup_le I2, max_le_iff, and_self_iff]
/- Get the same inequality for any coupling. If the coupling is quite good, the desired
inequality has been proved above. If it is bad, then the inequality is obvious. -/
have B :
∀ p q : NonemptyCompacts ℓ_infty_ℝ,
⟦p⟧ = toGHSpace X →
⟦q⟧ = toGHSpace Y →
hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ hausdorffDist (p : Set ℓ_infty_ℝ) q :=
by
intro p q hp hq
by_cases h : hausdorffDist (p : Set ℓ_infty_ℝ) q < diam (univ : Set X) + 1 + diam (univ : Set Y)
· exact A p q hp hq h
·
calc
hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ HD (candidatesBDist X Y) :=
hausdorffDist_optimal_le_HD _ _ candidatesBDist_mem_candidatesB
_ ≤ diam (univ : Set X) + 1 + diam (univ : Set Y) := HD_candidatesBDist_le
_ ≤ hausdorffDist (p : Set ℓ_infty_ℝ) q := not_lt.1 h
refine le_antisymm ?_ ?_
· apply le_csInf
· refine (Set.Nonempty.prod ?_ ?_).image _ <;> exact ⟨_, rfl⟩
· rintro b ⟨⟨p, q⟩, ⟨hp, hq⟩, rfl⟩
exact B p q hp hq
· exact ghDist_le_hausdorffDist (isometry_optimalGHInjl X Y) (isometry_optimalGHInjr X Y)
