English
Same idea as above: a setoid on NonemptyCompacts ℓ_∞(ℝ) identifying isometric nonempty compact subspaces, used to form the Gromov–Hausdorff framework.
Русский
Та же идея: сетойд на не пустых компактных подпространствах ℓ∞(ℝ), идентифицирующий изометричные подмножества, используемый в рамках Громова–Хаусдорфа.
LaTeX
$$Setoid (NonemptyCompacts ℓ_infty_ℝ) := IsometryRel equivalence_isometryRel$$
Lean4
/-- The Gromov-Hausdorff space is complete. -/
instance : CompleteSpace GHSpace := by
set d := fun n : ℕ ↦ ((1 : ℝ) / 2) ^ n
have : ∀ n : ℕ, 0 < d n := fun _ ↦ by
positivity
-- start from a sequence of nonempty compact metric spaces within distance `1/2^n` of each other
refine
Metric.complete_of_convergent_controlled_sequences d this fun u hu =>
?_
-- `X n` is a representative of `u n`
let X n := (u n).Rep
let Y := auxGluing X
have E : ∀ n : ℕ, GlueSpace (Y n).isom (isometry_optimalGHInjl (X n) (X (n + 1))) = (Y (n + 1)).Space := fun n => by
dsimp only [Y, auxGluing]
let c n := cast (E n)
have ic : ∀ n, Isometry (c n) := fun n x y => by dsimp only [Y, auxGluing]; exact rfl
let f : ∀ n, (Y n).Space → (Y (n + 1)).Space := fun n =>
c n ∘ toGlueL (Y n).isom (isometry_optimalGHInjl (X n) (X n.succ))
have I : ∀ n, Isometry (f n) := fun n =>
(ic n).comp
(toGlueL_isometry _ _)
-- consider the inductive limit `Z0` of the `Y n`, and then its completion `Z`
let Z0 := Metric.InductiveLimit I
let Z := UniformSpace.Completion Z0
let Φ := toInductiveLimit I
let coeZ :=
((↑) : Z0 → Z)
-- let `X2 n` be the image of `X n` in the space `Z`
let X2 n := range (coeZ ∘ Φ n ∘ (Y n).embed)
have isom : ∀ n, Isometry (coeZ ∘ Φ n ∘ (Y n).embed) :=
by
intro n
refine UniformSpace.Completion.coe_isometry.comp ?_
exact (toInductiveLimit_isometry _ _).comp (Y n).isom
have X2n :
∀ n,
X2 n =
range
((coeZ ∘ Φ n.succ ∘ c n ∘ toGlueR (Y n).isom (isometry_optimalGHInjl (X n) (X n.succ))) ∘
optimalGHInjl (X n) (X n.succ)) :=
by
intro n
change
X2 n =
range
(coeZ ∘
Φ n.succ ∘
c n ∘ toGlueR (Y n).isom (isometry_optimalGHInjl (X n) (X n.succ)) ∘ optimalGHInjl (X n) (X n.succ))
simp only [X2, Φ]
rw [← toInductiveLimit_commute I]
simp only [f, ← toGlue_commute, Function.comp_assoc]
have X2nsucc :
∀ n,
X2 n.succ =
range
((coeZ ∘ Φ n.succ ∘ c n ∘ toGlueR (Y n).isom (isometry_optimalGHInjl (X n) (X n.succ))) ∘
optimalGHInjr (X n) (X n.succ)) :=
by
intro n
rfl
have D2 : ∀ n, hausdorffDist (X2 n) (X2 n.succ) < d n := fun n ↦
by
rw [X2n n, X2nsucc n, range_comp, range_comp, hausdorffDist_image, hausdorffDist_optimal, ← dist_ghDist]
· exact hu n n n.succ (le_refl n) (le_succ n)
· apply UniformSpace.Completion.coe_isometry.comp _
exact
(toInductiveLimit_isometry _ _).comp
((ic n).comp (toGlueR_isometry _ _))
-- consider `X2 n` as a member `X3 n` of the type of nonempty compact subsets of `Z`, which
-- is a metric space
let X3 : ℕ → NonemptyCompacts Z := fun n =>
⟨⟨X2 n, isCompact_range (isom n).continuous⟩, range_nonempty _⟩
-- `X3 n` is a Cauchy sequence by construction, as the successive distances are
-- bounded by `(1/2)^n`
have : CauchySeq X3 := by
refine cauchySeq_of_le_geometric (1 / 2) 1 (by norm_num) fun n => ?_
rw [one_mul]
exact
le_of_lt
(D2 n)
-- therefore, it converges to a limit `L`
rcases cauchySeq_tendsto_of_complete this with
⟨L, hL⟩
-- By construction, the image of `X3 n` in the Gromov-Hausdorff space is `u n`.
have : ∀ n, (NonemptyCompacts.toGHSpace ∘ X3) n = u n :=
by
intro n
rw [Function.comp_apply, NonemptyCompacts.toGHSpace, ← (u n).toGHSpace_rep,
toGHSpace_eq_toGHSpace_iff_isometryEquiv]
constructor
convert (isom n).isometryEquivOnRange.symm
use L.toGHSpace
apply Filter.Tendsto.congr this
refine Tendsto.comp ?_ hL
apply toGHSpace_continuous.tendsto
