Lean4
/-- The hard part of the Lusin separation theorem saying that two disjoint analytic sets are
contained in disjoint Borel sets (see the full statement in `AnalyticSet.measurablySeparable`).
Here, we prove this when our analytic sets are the ranges of functions from `ℕ → ℕ`.
-/
theorem measurablySeparable_range_of_disjoint [T2Space α] [MeasurableSpace α] [OpensMeasurableSpace α]
{f g : (ℕ → ℕ) → α} (hf : Continuous f) (hg : Continuous g) (h : Disjoint (range f) (range g)) :
MeasurablySeparable (range f) (range g) := by
/- We follow [Kechris, *Classical Descriptive Set Theory* (Theorem 14.7)][kechris1995].
If the ranges are not Borel-separated, then one can find two cylinders of length one whose
images are not Borel-separated, and then two smaller cylinders of length two whose images are
not Borel-separated, and so on. One thus gets two sequences of cylinders, that decrease to two
points `x` and `y`. Their images are different by the disjointness assumption, hence contained
in two disjoint open sets by the T2 property. By continuity, long enough cylinders around `x`
and `y` have images which are separated by these two disjoint open sets, a contradiction.
-/
by_contra hfg
have I :
∀ n x y,
¬MeasurablySeparable (f '' cylinder x n) (g '' cylinder y n) →
∃ x' y',
x' ∈ cylinder x n ∧
y' ∈ cylinder y n ∧ ¬MeasurablySeparable (f '' cylinder x' (n + 1)) (g '' cylinder y' (n + 1)) :=
by
intro n x y
contrapose!
intro H
rw [← iUnion_cylinder_update x n, ← iUnion_cylinder_update y n, image_iUnion, image_iUnion]
refine MeasurablySeparable.iUnion fun i j => ?_
exact
H _ _ (update_mem_cylinder _ _ _)
(update_mem_cylinder _ _ _)
-- consider the set of pairs of cylinders of some length whose images are not Borel-separated
let A :=
{ p : ℕ × (ℕ → ℕ) × (ℕ → ℕ) // ¬MeasurablySeparable (f '' cylinder p.2.1 p.1) (g '' cylinder p.2.2 p.1) }
-- for each such pair, one can find longer cylinders whose images are not Borel-separated either
have : ∀ p : A, ∃ q : A, q.1.1 = p.1.1 + 1 ∧ q.1.2.1 ∈ cylinder p.1.2.1 p.1.1 ∧ q.1.2.2 ∈ cylinder p.1.2.2 p.1.1 :=
by
rintro ⟨⟨n, x, y⟩, hp⟩
rcases I n x y hp with ⟨x', y', hx', hy', h'⟩
exact ⟨⟨⟨n + 1, x', y'⟩, h'⟩, rfl, hx', hy'⟩
choose F hFn hFx hFy using this
let p0 : A :=
⟨⟨0, fun _ => 0, fun _ => 0⟩, by simp [hfg]⟩
-- construct inductively decreasing sequences of cylinders whose images are not separated
let p : ℕ → A := fun n => F^[n] p0
have prec : ∀ n, p (n + 1) = F (p n) := fun n => by
simp only [p, iterate_succ', Function.comp]
-- check that at the `n`-th step we deal with cylinders of length `n`
have pn_fst : ∀ n, (p n).1.1 = n := fun n ↦ by
induction n with
| zero => rfl
| succ n IH =>
simp only [prec, hFn, IH]
-- check that the cylinders we construct are indeed decreasing, by checking that the coordinates
-- are stationary.
have Ix : ∀ m n, m + 1 ≤ n → (p n).1.2.1 m = (p (m + 1)).1.2.1 m :=
by
intro m
apply Nat.le_induction
· rfl
intro n hmn IH
have I : (F (p n)).val.snd.fst m = (p n).val.snd.fst m :=
by
apply hFx (p n) m
rw [pn_fst]
exact hmn
rw [prec, I, IH]
have Iy : ∀ m n, m + 1 ≤ n → (p n).1.2.2 m = (p (m + 1)).1.2.2 m :=
by
intro m
apply Nat.le_induction
· rfl
intro n hmn IH
have I : (F (p n)).val.snd.snd m = (p n).val.snd.snd m :=
by
apply hFy (p n) m
rw [pn_fst]
exact hmn
rw [prec, I, IH]
-- denote by `x` and `y` the limit points of these two sequences of cylinders.
set x : ℕ → ℕ := fun n => (p (n + 1)).1.2.1 n with hx
set y : ℕ → ℕ := fun n => (p (n + 1)).1.2.2 n with hy
have M : ∀ n, ¬MeasurablySeparable (f '' cylinder x n) (g '' cylinder y n) :=
by
intro n
convert (p n).2 using 3
· rw [pn_fst, ← mem_cylinder_iff_eq, mem_cylinder_iff]
intro i hi
rw [hx]
exact (Ix i n hi).symm
· rw [pn_fst, ← mem_cylinder_iff_eq, mem_cylinder_iff]
intro i hi
rw [hy]
exact (Iy i n hi).symm
obtain ⟨u, v, u_open, v_open, xu, yv, huv⟩ : ∃ u v : Set α, IsOpen u ∧ IsOpen v ∧ f x ∈ u ∧ g y ∈ v ∧ Disjoint u v :=
by
apply t2_separation
exact disjoint_iff_forall_ne.1 h (mem_range_self _) (mem_range_self _)
letI : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
obtain ⟨εx, εxpos, hεx⟩ : ∃ (εx : ℝ), εx > 0 ∧ Metric.ball x εx ⊆ f ⁻¹' u :=
by
apply Metric.mem_nhds_iff.1
exact hf.continuousAt.preimage_mem_nhds (u_open.mem_nhds xu)
obtain ⟨εy, εypos, hεy⟩ : ∃ (εy : ℝ), εy > 0 ∧ Metric.ball y εy ⊆ g ⁻¹' v :=
by
apply Metric.mem_nhds_iff.1
exact hg.continuousAt.preimage_mem_nhds (v_open.mem_nhds yv)
obtain ⟨n, hn⟩ : ∃ n : ℕ, (1 / 2 : ℝ) ^ n < min εx εy :=
exists_pow_lt_of_lt_one (lt_min εxpos εypos)
(by norm_num)
-- for large enough `n`, these open sets separate the images of long cylinders around `x` and `y`
have B : MeasurablySeparable (f '' cylinder x n) (g '' cylinder y n) :=
by
refine ⟨u, ?_, ?_, u_open.measurableSet⟩
· rw [image_subset_iff]
apply Subset.trans _ hεx
intro z hz
rw [mem_cylinder_iff_dist_le] at hz
exact hz.trans_lt (hn.trans_le (min_le_left _ _))
· refine Disjoint.mono_left ?_ huv.symm
change g '' cylinder y n ⊆ v
rw [image_subset_iff]
apply Subset.trans _ hεy
intro z hz
rw [mem_cylinder_iff_dist_le] at hz
exact
hz.trans_lt
(hn.trans_le (min_le_right _ _))
-- this is a contradiction.
exact M n B
