Lean4
/-- In a complete space, the type of closed subsets is complete for the
Hausdorff edistance. -/
instance completeSpace [CompleteSpace α] : CompleteSpace (Closeds α) := by
/- We will show that, if a sequence of sets `s n` satisfies
`edist (s n) (s (n+1)) < 2^{-n}`, then it converges. This is enough to guarantee
completeness, by a standard completeness criterion.
We use the shorthand `B n = 2^{-n}` in ennreal. -/
let B : ℕ → ℝ≥0∞ := fun n => 2⁻¹ ^ n
have B_pos : ∀ n, (0 : ℝ≥0∞) < B n := by simp [B, ENNReal.pow_pos]
have B_ne_top : ∀ n, B n ≠ ⊤ := by
finiteness
/- Consider a sequence of closed sets `s n` with `edist (s n) (s (n+1)) < B n`.
We will show that it converges. The limit set is `t0 = ⋂n, closure (⋃m≥n, s m)`.
We will have to show that a point in `s n` is close to a point in `t0`, and a point
in `t0` is close to a point in `s n`. The completeness then follows from a
standard criterion. -/
refine complete_of_convergent_controlled_sequences B B_pos fun s hs => ?_
let t0 := ⋂ n, closure (⋃ m ≥ n, s m : Set α)
let t : Closeds α := ⟨t0, isClosed_iInter fun _ => isClosed_closure⟩
use t
have I1 : ∀ n, ∀ x ∈ s n, ∃ y ∈ t0, edist x y ≤ 2 * B n := by
/- This is the main difficulty of the proof. Starting from `x ∈ s n`, we want
to find a point in `t0` which is close to `x`. Define inductively a sequence of
points `z m` with `z n = x` and `z m ∈ s m` and `edist (z m) (z (m+1)) ≤ B m`. This is
possible since the Hausdorff distance between `s m` and `s (m+1)` is at most `B m`.
This sequence is a Cauchy sequence, therefore converging as the space is complete, to
a limit which satisfies the required properties. -/
intro n x hx
obtain ⟨z, hz₀, hz⟩ : ∃ z : ∀ l, s (n + l), (z 0 : α) = x ∧ ∀ k, edist (z k : α) (z (k + 1) : α) ≤ B n / 2 ^ k := by
-- We prove existence of the sequence by induction.
have : ∀ (l) (z : s (n + l)), ∃ z' : s (n + l + 1), edist (z : α) z' ≤ B n / 2 ^ l :=
by
intro l z
obtain ⟨z', z'_mem, hz'⟩ : ∃ z' ∈ s (n + l + 1), edist (z : α) z' < B n / 2 ^ l :=
by
refine exists_edist_lt_of_hausdorffEdist_lt (s := s (n + l)) z.2 ?_
simp only [ENNReal.inv_pow, div_eq_mul_inv]
rw [← pow_add]
apply hs <;> simp
exact ⟨⟨z', z'_mem⟩, le_of_lt hz'⟩
use fun k => Nat.recOn k ⟨x, hx⟩ fun l z => (this l z).choose
simp only [Nat.add_zero, Nat.rec_zero, true_and]
exact fun k => (this k _).choose_spec
have : CauchySeq fun k => (z k : α) := cauchySeq_of_edist_le_geometric_two (B n) (B_ne_top n) hz
rcases cauchySeq_tendsto_of_complete this with ⟨y, y_lim⟩
use y
have : y ∈ t0 :=
mem_iInter.2 fun k =>
mem_closure_of_tendsto y_lim
(by
simp only [exists_prop, Set.mem_iUnion, Filter.eventually_atTop]
exact ⟨k, fun m hm => ⟨n + m, by cutsat, (z m).2⟩⟩)
use this
rw [← hz₀]
exact edist_le_of_edist_le_geometric_two_of_tendsto₀ (B n) hz y_lim
have I2 : ∀ n, ∀ x ∈ t0, ∃ y ∈ s n, edist x y ≤ 2 * B n := by
/- For the (much easier) reverse inequality, we start from a point `x ∈ t0` and we want
to find a point `y ∈ s n` which is close to `x`.
`x` belongs to `t0`, the intersection of the closures. In particular, it is well
approximated by a point `z` in `⋃m≥n, s m`, say in `s m`. Since `s m` and
`s n` are close, this point is itself well approximated by a point `y` in `s n`,
as required. -/
intro n x xt0
have : x ∈ closure (⋃ m ≥ n, s m : Set α) := by apply mem_iInter.1 xt0 n
obtain ⟨z : α, hz, Dxz : edist x z < B n⟩ := mem_closure_iff.1 this (B n) (B_pos n)
simp only [exists_prop, Set.mem_iUnion] at hz
obtain ⟨m : ℕ, m_ge_n : m ≥ n, hm : z ∈ (s m : Set α)⟩ := hz
have : hausdorffEdist (s m : Set α) (s n) < B n := hs n m n m_ge_n (le_refl n)
obtain ⟨y : α, hy : y ∈ (s n : Set α), Dzy : edist z y < B n⟩ := exists_edist_lt_of_hausdorffEdist_lt hm this
exact
⟨y, hy,
calc
edist x y ≤ edist x z + edist z y := edist_triangle _ _ _
_ ≤ B n + B n := by gcongr
_ = 2 * B n := (two_mul _).symm⟩
-- Deduce from the above inequalities that the distance between `s n` and `t0` is at most `2 B n`.
have main : ∀ n : ℕ, edist (s n) t ≤ 2 * B n := fun n =>
hausdorffEdist_le_of_mem_edist (I1 n)
(I2 n)
-- from this, the convergence of `s n` to `t0` follows.
refine tendsto_atTop.2 fun ε εpos => ?_
have : Tendsto (fun n => 2 * B n) atTop (𝓝 (2 * 0)) :=
ENNReal.Tendsto.const_mul (ENNReal.tendsto_pow_atTop_nhds_zero_of_lt_one <| by simp) (Or.inr <| by simp)
rw [mul_zero] at this
obtain ⟨N, hN⟩ : ∃ N, ∀ b ≥ N, ε > 2 * B b := ((tendsto_order.1 this).2 ε εpos).exists_forall_of_atTop
exact ⟨N, fun n hn => lt_of_le_of_lt (main n) (hN n hn)⟩
