Lean4
theorem continuous_equiv_symm_probabilityMeasure : Continuous (LevyProkhorov.equiv (α := ProbabilityMeasure Ω)).symm :=
by
-- We check continuity of `id : ProbabilityMeasure Ω → LevyProkhorov (ProbabilityMeasure Ω)` at
-- each point `P : ProbabilityMeasure Ω`.
rw [continuous_iff_continuousAt]
intro P
rw [continuousAt_iff']
intro ε ε_pos
have third_ε_pos : 0 < ε / 3 := by linarith
have third_ε_pos' : 0 < ENNReal.ofReal (ε / 3) := ofReal_pos.mpr third_ε_pos
obtain ⟨Es, Es_mble, Es_bdd, Es_diam, Es_cover, Es_disjoint⟩ :=
SeparableSpace.exists_measurable_partition_diam_le Ω third_ε_pos
obtain ⟨N, hN⟩ : ∃ N, P.toMeasure (⋃ j ∈ Iio N, Es j)ᶜ < ENNReal.ofReal (ε / 3) :=
by
have exhaust :=
@tendsto_measure_biUnion_Ici_zero_of_pairwise_disjoint Ω _ P.toMeasure _ Es
(fun n ↦ (Es_mble n).nullMeasurableSet) Es_disjoint
simp only [tendsto_atTop_nhds, Function.comp_apply] at exhaust
obtain ⟨N, hN⟩ := exhaust (Iio (ENNReal.ofReal (ε / 3))) third_ε_pos' isOpen_Iio
refine ⟨N, ?_⟩
have rewr : ⋃ i, ⋃ (_ : N ≤ i), Es i = (⋃ i, ⋃ (_ : i < N), Es i)ᶜ := by
simpa only [mem_Iio, compl_Iio, mem_Ici] using
(biUnion_compl_eq_of_pairwise_disjoint_of_iUnion_eq_univ Es_cover Es_disjoint (Iio N)).symm
simpa only [mem_Iio, ← rewr, gt_iff_lt] using hN N le_rfl
have Js_finite : Set.Finite {J | J ⊆ Iio N} := Finite.finite_subsets <| finite_Iio N
set Gs := (fun (J : Set ℕ) ↦ thickening (ε / 3) (⋃ j ∈ J, Es j)) '' {J | J ⊆ Iio N}
have Gs_open : ∀ (J : Set ℕ), IsOpen (thickening (ε / 3) (⋃ j ∈ J, Es j)) := fun J ↦ isOpen_thickening
have mem_nhds_P (G : Set Ω) (G_open : IsOpen G) :
{Q | P.toMeasure G < Q.toMeasure G + ENNReal.ofReal (ε / 3)} ∈ 𝓝 P :=
P.toMeasure_add_pos_gt_mem_nhds G_open third_ε_pos'
filter_upwards [(Finset.iInter_mem_sets Js_finite.toFinset).mpr <| fun J _ ↦ mem_nhds_P _ (Gs_open J)] with Q hQ
simp only [Finite.mem_toFinset, mem_setOf_eq, thickening_iUnion, mem_iInter] at hQ
apply lt_of_le_of_lt ?_ (show 2 * (ε / 3) < ε by linarith)
rw [dist_comm]
-- Fix an arbitrary set `B ⊆ Ω`, and an arbitrary `δ > 2*ε/3` to gain some room for error
-- and for thickening.
apply
levyProkhorovDist_le_of_forall_le _ _ (by linarith)
(fun δ B δ_gt _ ↦ ?_)
-- Let `JB ⊆ {0, 1, ..., N-1}` consist of those indices `j` such that `B` intersects `Es j`.
-- Then the open set `Gs JB` approximates `B` rather well:
-- except for what happens in the small complement `(⋃ n < N, Es n)ᶜ`, the set `B` is
-- contained in `Gs JB`, and conversely `Gs JB` only contains points within `δ` from `B`.
set JB := {i | B ∩ Es i ≠ ∅ ∧ i ∈ Iio N}
have B_subset : B ⊆ (⋃ i ∈ JB, thickening (ε / 3) (Es i)) ∪ (⋃ j ∈ Iio N, Es j)ᶜ :=
by
suffices B ⊆ (⋃ i ∈ JB, thickening (ε / 3) (Es i)) ∪ (⋃ j ∈ Ici N, Es j)
by
refine this.trans <| union_subset_union le_rfl ?_
intro ω hω
simp only [mem_Ici, mem_iUnion, exists_prop] at hω
obtain ⟨i, i_large, ω_in_Esi⟩ := hω
by_contra con
simp only [mem_Iio, compl_iUnion, mem_iInter, mem_compl_iff, not_forall, not_not, exists_prop] at con
obtain ⟨j, j_small, ω_in_Esj⟩ := con
exact disjoint_left.mp (Es_disjoint (show j ≠ i by cutsat)) ω_in_Esj ω_in_Esi
intro ω ω_in_B
obtain ⟨i, hi⟩ := show ∃ n, ω ∈ Es n by simp only [← mem_iUnion, Es_cover, mem_univ]
simp only [mem_Ici, mem_union, mem_iUnion, exists_prop]
by_cases i_small : i ∈ Iio N
· refine Or.inl ⟨i, ?_, self_subset_thickening third_ε_pos _ hi⟩
simp only [mem_Iio, mem_setOf_eq, JB]
push_neg
exact ⟨Set.nonempty_of_mem <| mem_inter ω_in_B hi, i_small⟩
· exact Or.inr ⟨i, by simpa only [mem_Iio, not_lt] using i_small, hi⟩
have subset_thickB : ⋃ i ∈ JB, thickening (ε / 3) (Es i) ⊆ thickening δ B :=
by
intro ω ω_in_U
simp only [mem_iUnion, exists_prop] at ω_in_U
obtain ⟨k, ⟨B_intersects, _⟩, ω_in_thEk⟩ := ω_in_U
rw [mem_thickening_iff] at ω_in_thEk ⊢
obtain ⟨w, w_in_Ek, w_near⟩ := ω_in_thEk
obtain ⟨z, ⟨z_in_B, z_in_Ek⟩⟩ := nonempty_iff_ne_empty.mpr B_intersects
refine ⟨z, z_in_B, lt_of_le_of_lt (dist_triangle ω w z) ?_⟩
apply lt_of_le_of_lt (add_le_add w_near.le <| (dist_le_diam_of_mem (Es_bdd k) w_in_Ek z_in_Ek).trans <| Es_diam k)
linarith
-- We use the resulting upper bound `P B ≤ P (Gs JB) + P (small complement)`.
apply
(measure_mono B_subset).trans
((measure_union_le _ _).trans ?_)
-- From the choice of `Q` in a suitable neighborhood, we have `P (Gs JB) < Q (Gs JB) + ε/3`.
specialize
hQ _
(show JB ⊆ Iio N from fun _ h ↦ h.2)
-- Now it remains to add the pieces and use the above estimates.
apply (add_le_add hQ.le hN.le).trans
rw [add_assoc, ← ENNReal.ofReal_add third_ε_pos.le third_ε_pos.le, ← two_mul]
apply add_le_add (measure_mono subset_thickB) (ofReal_le_ofReal _)
exact δ_gt.le
