feat: Levy-Prokhorov distance pseudometrizes convergence in distribution (#11549)

Add the more interesting direction of topology comparison for the Lévy-Prokhorov distance. Conclude that if the underlying space is separable, then the topology of convergence in distribution coincides with the one obtained from the Lévy-Prokhorov (pseudo)metric. In particular the topology of convergence in distribution is (pseudo)metrizable, and so first countable.



Co-authored-by: kkytola <39528102+kkytola@users.noreply.github.com>
Co-authored-by: kkytola <“kalle.kytola@aalto.fi”>

Author: kkytola

Mathlib/Data/Set/Lattice.lean

@@ -2092,6 +2092,22 @@ theorem disjoint_sUnion_right {s : Set α} {S : Set (Set α)} :
   disjoint_sSup_iff
 #align set.disjoint_sUnion_right Set.disjoint_sUnion_right
 
+lemma biUnion_compl_eq_of_pairwise_disjoint_of_iUnion_eq_univ {ι : Type*} {Es : ι → Set α}
+    (Es_union : ⋃ i, Es i = univ) (Es_disj : Pairwise fun i j ↦ Disjoint (Es i) (Es j))
+    (I : Set ι) :
+    (⋃ i ∈ I, Es i)ᶜ = ⋃ i ∈ Iᶜ, Es i := by
+  ext x
+  obtain ⟨i, hix⟩ : ∃ i, x ∈ Es i := by simp [← mem_iUnion, Es_union]
+  have obs : ∀ (J : Set ι), x ∈ ⋃ j ∈ J, Es j ↔ i ∈ J := by
+    refine fun J ↦ ⟨?_, fun i_in_J ↦ by simpa only [mem_iUnion, exists_prop] using ⟨i, i_in_J, hix⟩⟩
+    intro x_in_U
+    simp only [mem_iUnion, exists_prop] at x_in_U
+    obtain ⟨j, j_in_J, hjx⟩ := x_in_U
+    rwa [show i = j by by_contra i_ne_j; exact Disjoint.ne_of_mem (Es_disj i_ne_j) hix hjx rfl]
+  have obs' : ∀ (J : Set ι), x ∈ (⋃ j ∈ J, Es j)ᶜ ↔ i ∉ J :=
+    fun J ↦ by simpa only [mem_compl_iff, not_iff_not] using obs J
+  rw [obs, obs', mem_compl_iff]
+
 end Set
 
 end Disjoint