Status of the Central limit theorem

Stream: mathlib4

[Josha Dekker]

I couldn’t find a thread on this, but I’m on mobile, so I might’ve missed this. What is the current status on the central limit theorem in Mathlib?

Is this work in progress or is this wide open?
In any case, are there important components (likely) missing?

[Yaël Dillies]

This is a question for @Jason KY.

[Rémy Degenne]

The main missing piece for the usual proof of that theorem is the definition of the characteristic function, and proofs of its properties.
I wrote a definition (and basically nothing else) a while ago here: https://github.com/leanprover-community/mathlib4/compare/RD_char_fun .
I you want to work on it, feel free to take this definition (or discard it).

[Josha Dekker]

Okay, I’ll see if I can get around to that at some stage. I haven’t yet invested too much time into the measure theory parts of Mathlib, I’ll probably turn my attention there once I finish working on Lindelöf spaces.

[Josha Dekker]

I think that a feasible approach would be adapting some of the first chapter of Applebaum’s Lévy Processes and Stochastic Calculus. This provides the basic tools to work with characteristic functions (incl eg Lévy’s continuity theorem) and would also lay some more foundations for Lévy process theory at some point. If you’re aware of a better source, please let me know! I’ll try to adapt everything to more general measurable spaces where possible, of course! I’ll work on this somewhere in the new year, can’t say for certain yet when!

[Josha Dekker]

@Rémy Degenne your file looks very good, I'll add some more basic API and make a PR (linearity, Lévy's continuity theorem etc.). Shall I include you in the copyright statement? You provided all the essential pieces!

[Rémy Degenne]

@Josha Dekker I wanted to try setting up a blueprint to learn how it works, and your question about the CLT gave me a good reason: over the last two days I created a project with a blueprint for a proof of CLT using characteristic functions. See https://remydegenne.github.io/CLT/index.html for the blueprint, https://github.com/RemyDegenne/CLT for the github repository and https://remydegenne.github.io/CLT/dep_graph_document.html for the dependency graph. I have added my characteristic function code to that repository.

If anyone wants to contribute to the CLT proof, feel free to fork the repository and then open a PR!
The blueprint is very much WIP: it is not yet very detailed and many proofs are missing in the latex. I'll continue working on it, and PRs for that aspect of the project are also welcome. The home page of the blueprint lists a few helpful books.

The proof goes through Prokhorov's theorem, and I think that Kalle Kytölä is working on that. @Kalle Kytölä perhaps you'd like to expand the blueprint with details about your preferred way of proving that theorem?

The central limit theorem is one of the most embarrassing gaps in our probability library: let's close it!

[Josha Dekker]

Thanks, I’ll take a look later! I’ll probably try to work on building some more API for characteristic functions, something like Lévy’s continuity criterion is useful in multiple results!

[Josha Dekker]

We might consider a more general CLT like the Lindeberg-Feller CLT as a follow up, which also is proven through characteristic functions and doesn’t require the observations to be iid (which probably makes the approach a bit longer).

[Josha Dekker]

I'll take a shot at lemma 4.6!

[Josha Dekker]

(I'm not working on that at this point. I was first trying to work on convolution of measures for this, but hit a bump as my proficiency with integrals in Mathlib is too lacking)

[Kalle Kytölä]

Sorry for the very late reply!

Rémy Degenne said:

The proof goes through Prokhorov's theorem, and I think that Kalle Kytölä is working on that. Kalle Kytölä perhaps you'd like to expand the blueprint with details about your preferred way of proving that theorem?

Yes, I indeed have a preferred way to do the Prokhorov's theorem :grinning_face_with_smiling_eyes: :innocent:. I checked your blueprint, and it matches my preferred way --- I want to do it via Riesz-Markov-Kakutani. Is there a way I can contribute to the blueprint? [EDIT: I see now you said how to do that.] I don't have an awful lot to add, though... The plan is to use Riesz-Markov-Kakutani on compact spaces $X$ to identify the space of probability measures on $X$ with a closed subset of the unit ball of the weak dual of continuous functions, and get its compactness from Banach-Alaoglu. This gives Prokhorov's theorem on compact spaces $X$. Then on general Polish spaces Prokhorov's theorem reduces to the case of compact spaces by omitting an $\varepsilon>0$ of total mass of tight families.

(I'd also want metrizability of the convergence in distribution, which is what I am doing in #10406 etc. This gets rid of any barriers between compactness and sequential compactness, for example.)

(Riesz-Markov-Kakutani on compact spaces has been proved by Jesse Reimann some years ago, but it is not in Mathlib. The PRs of the main content have essentially not been started because of stupid issues regarding the handling subtractions of bounded continuous NNReal-valued functions etc. The plan forward involved a bit of a refactor, but I have not had time to get started with it...)

Rémy Degenne said:

The central limit theorem is one of the most embarrassing gaps in our probability library: let's close it!

Yes!

If the bottleneck is Prokhorov, then there is, of course, a much simpler way for $\R$ via cumulative distribution functions ("Helly's selection theorem"). I have been intending to PR the cdf characterization of convergence in distribution for some time... I will try to do that soon (it is almost trivial with the portmanteau theorem, which exists in a sufficient form in Mathlib already), so that if someone wants to take the route of Helly's selection, that should not hold back the Central Limit Theorem.

(I suppose indeed the other needed component for CLT is inversion of characteristic functions, i.e., suitable Fourier theory. In my mind there might be one tricky lemma that is often proven by complex contour integrals, although ways around that seem to exist. Anyway, someone else knows about the status of that better than I do.)

[Rémy Degenne]

Central limit theorem update

There has been some work happening over at https://github.com/RemyDegenne/CLT and we now have a proof of the central limit theorem for real random variables, if we assume Prokhorov's theorem.

Jakob Stiefel has recently added to Mathlib a proof that characteristic functions separate measures, which is a key ingredient.
Using that, we were able to prove the Lévy convergence theorem (weak convergence of measures equivalent to convergence of characteristic functions), assuming Prokhorov's theorem.

@Thomas Zhu then proved the CLT from there, which needed facts about characteristic functions, independence and Gaussian random variables.

Prokhorov's theorem is being worked on by Arav Bhattacharyya , and once that's done our proof will be complete.
You might spot another blue node in the graph leading to the CLT corresponding to a version of Taylor's theorem, but there is an open Mathlib PR for that.

We are making PRs to Mathlib with the material that does not depend on Prokhorov.

[Sébastien Gouëzel]

Regarding Prokhorov, I've just sent the Riesz-Markov-Kakutani theorem of #12290 to bors. This should be an important ingredient for Prokhorov.

[Rémy Degenne]

Yes, if I recall correctly Arav is assuming RMK and going from there.

[Sébastien Gouëzel]

Could you add a link to the blueprint on the readme of the project? Otherwise, there is no direct way to find the blueprint when one is on the github page.

[Rémy Degenne]

There is a link in the "About" section on the right of the github page, but I'll add it to the readme as well.

[Sébastien Gouëzel]

Ah yes, thanks!

[Rémy Degenne]

And I need to restore the docs too. For now the "LEAN" links in the blueprint point nowhere, so it's a bit hard to find the results in the code.

[Rémy Degenne]

In the dependency graph I used a purple border color to denote things that are already in Mathlib, but I don't know how to add an entry in the legend for that color. Does anyone know?

[Patrick Massot]

It looks like I forgot that case in the function that creates the legend.

[Patrick Massot]

I just pushed a fix. Is your blueprint generated using the master branch of leanblueprint or do you take it from pypi (hence need a release)?

[Yaël Dillies]

Rémy Degenne said:

In the dependency graph I used a purple border color to denote things that are already in Mathlib

:idea: New blueprint color discovered

[Rémy Degenne]

Patrick Massot said:

I just pushed a fix. Is your blueprint generated using the master branch of leanblueprint or do you take it from pypi (hence need a release)?

My CI gets leanblueprint with pip install leanblueprint, so I guess I will have to wait for a release. That's not a big issue anyway. It can wait.

[Rémy Degenne]

Yaël Dillies said:

:idea: New blueprint color discovered

The default color for \mathlibok is a slightly darker green than the \leanok color. I can't easily tell them apart, so I replaced it with purple.

[Thomas Zhu]

You can use pip install git+https://github.com/PatrickMassot/leanblueprint.git@master for installing from the newest github version (or pip install --upgrade --force-reinstall --no-deps git+https://github.com/PatrickMassot/leanblueprint.git@master to force override an existing install)

[Arav Bhattacharyya]

Regarding Prokhorov- the easy direction is pretty much done. The other direction (requiring RMK) I will start soon. I’m having to take a little break from working properly on this right now as I have exams over May, but intend to get it done over June. I don’t want to hold up the CLT going in mathlib so if anyone wants to get it done sooner I don’t mind!

[Patrick Massot]

Rémy Degenne said:

My CI gets leanblueprint with pip install leanblueprint, so I guess I will have to wait for a release. That's not a big issue anyway. It can wait.

Releases are cheap. Could you try it locally using master? I didn’t test my fix at all…

[Rémy Degenne]

I tested in local: I have a new legend, but it says

The statement of this result is in Mathlib border
    this is in Mathlib

So there is "The statement of this result is in Mathlib" where I would expect the color. But I suspect it's my fault. I changed the color with

\graphcolor{mathlib}{purple}{The statement of this result is in Mathlib}

[Patrick Massot]

Ah yes, the laster argument is meant to be a description of the border.

[Patrick Massot]

So Purple would be fine.

[Patrick Massot]

It looks redundant with the previous argument, but the previous argument could a html color description such as #ff10aa

[Rémy Degenne]

Thanks! It works perfectly in local now.

[Rémy Degenne]

Arav Bhattacharyya said:

Regarding Prokhorov- the easy direction is pretty much done. The other direction (requiring RMK) I will start soon. I’m having to take a little break from working properly on this right now as I have exams over May, but intend to get it done over June. I don’t want to hold up the CLT going in mathlib so if anyone wants to get it done sooner I don’t mind!

I am not aware of any formalization project that desperately needs the CLT right now, so take all the time you need!
If at some point your university project is done but there is still something left to do and you want help, ping me.

[Yaël Dillies]

Rémy Degenne said:

Yaël Dillies said:

:idea: New blueprint color discovered

The default color for \mathlibok is a slightly darker green than the \leanok color. I can't easily tell them apart, so I replaced it with purple.

:light_bulb: New blueprint macro discovered

[Patrick Massot]

Note this macro is documented in the leanblueprint repo README. So maybe you could discover more things by reading that file.

[Patrick Massot]

I just released a new version on pypi with the fix.

[Miyahara Kō]

Hi, since there hasn’t been much activity in this thread and in the CLT repository recently, I’ve gone ahead and almost fully formalized the proof of Prokhorov’s theorem.
https://github.com/RemyDegenne/CLT/pull/56
The remained parts are these two lemmas:

In pseudo metrizable space, if any sequence on the Set $S$ has a subsequence converges, then the closure of $S$ is compact.

In pseudo metrizable space, any separable set $M$, there are the countable open sets family $\mathcal{A}$ has the following property: for any open set $G$ and $x \in M \cap G$, there exists $A \in \mathcal{A}$ such that $x \in A \subseteq \mathrm{cl}A \subseteq G$.

[Aaron Liu]

Miyahara Kō said:

In pseudo metrizable space, if any sequence on the Set $S$ has a subsequence converges, then the closure of $S$ is compact.

I think you can probably use docs#IsSeqCompact.isCompact

[Aaron Liu]

Miyahara Kō said:

In pseudo metrizable space, any separable set $M$, there are the countable open sets family $\mathcal{A}$ has the following property: for any open set $G$ and $x \in M \cap G$, there exists $A \in \mathcal{A}$ such that $x \in A \subseteq \mathrm{cl}A \subseteq G$.

I think this can be done with a combination of docs#TopologicalSpace.IsSeparable.secondCountableTopology and docs#closed_nhds_basis (choose a countable basis and for each element $O$ of the basis choose an open set inside a closed set inside an open set whose intersection with $M$ is $O$)

[Aaron Liu]

now that I've written this out I realize it doesn't work like that

[Aaron Liu]

I guess you can simultaneously do the open-closed-open thing for each point in $M$ and use lindelöf to extract a countable subcover

[Aaron Liu]

if you write the statements in Lean I can prove them for you

[Miyahara Kō]

Thank you! These statements are written as sorry in isCompact_closure_of_isTightMeasureSet in Clt/Prokhorov of my PR. (Add SecoundCountableTopology to isCompact_closure_of_isTightMeasureSet, or the space of probability measure can't be metrizable.)

[Aaron Liu]

@Miyahara Kō You seems to have a lot going on in that PR so I will simplify a bit is it okay if I just do these

import Mathlib

open Filter TopologicalSpace Topology

variable {X : Type*} [TopologicalSpace X] [PseudoMetrizableSpace X]

example {S : Set X} (hS : ∀ (P : ℕ → X), (∀ n, P n ∈ S) → ∃ P', ∃ N : ℕ → ℕ, StrictMono N ∧
    Tendsto (P ∘ N) atTop (𝓝 P')) : IsCompact (closure S) := by
  sorry

example {M : Set X} (hM : IsSeparable M) :
    ∃ (𝓐 : Set (Set X)), 𝓐.Countable ∧ (∀ A ∈ 𝓐, IsOpen A) ∧
      ∀ (G : Set X), IsOpen G → ∀ x ∈ M ∩ G,
      ∃ A ∈ 𝓐, x ∈ A ∧ closure A ⊆ G := by
  sorry

[Miyahara Kō]

Yes.

[Aaron Liu]

one done

import Mathlib

open Filter TopologicalSpace Topology

variable {X : Type*} [TopologicalSpace X] [PseudoMetrizableSpace X]

example {S : Set X} (hS : ∀ (P : ℕ → X), (∀ n, P n ∈ S) → ∃ P', ∃ N : ℕ → ℕ, StrictMono N ∧
    Tendsto (P ∘ N) atTop (𝓝 P')) : IsCompact (closure S) := by
  let := pseudoMetrizableSpacePseudoMetric
  apply IsSeqCompact.isCompact
  intro P hP
  simp_rw [Metric.mem_closure_iff] at hP
  choose b hb hbd using hP
  obtain ⟨us, hus, tus⟩ : ∃ us : ℕ → ℝ, (∀ n, 0 < us n) ∧ Tendsto us atTop (𝓝 0) :=
    ⟨fun n => 1 / (n + 1), fun _ => by positivity, tendsto_one_div_add_atTop_nhds_zero_nat⟩
  obtain ⟨P', N, hN, hP'⟩ := hS (fun n => b n (us n) (hus n)) (fun _ => hb ..)
  refine ⟨P', mem_closure_of_tendsto hP' (.of_forall fun _ => hb ..), N, hN, ?_⟩
  rw [Metric.tendsto_nhds] at tus hP' ⊢
  intro ε hε
  have h : ∀ᶠ (x : Nat) in map N atTop, dist (P x) (b x (us x) (hus x)) < ε / 2 := by
    apply Filter.Eventually.filter_mono hN.tendsto_atTop
    filter_upwards [tus (ε / 2) (by positivity)] with x hx
    apply (hbd ..).trans
    rwa [Real.dist_0_eq_abs, abs_of_pos (hus x)] at hx
  rw [Filter.eventually_map] at h
  apply (hP' (ε / 2) (by positivity)).mp
  apply h.mono
  intro x h₁ h₂
  exact (dist_triangle _ _ _).trans_lt ((add_lt_add h₁ h₂).trans_eq (add_halves ε))

[Aaron Liu]

unexpectedly had to manipulate epsilons but I figured it out

[Yongxi Lin (Aaron)]

So it seems like that we actually don't need the Riesz Representation theorem and the sequential Banach Alaoglu theorem to prove the Prokhorov’s theorem? The formalization for the Prokhorov’s theorem was stuck mainly because we are missing these two theorems right now in the Mathlib.

[Lawrence Wu (llllvvuu)]

AI proof of the first lemma (from Harmonic's forthcoming release):

theorem problem1 {X : Type*} [TopologicalSpace X] [TopologicalSpace.PseudoMetrizableSpace X] {S : Set X} (hS : ∀ (P : ℕ → X), (∀ n, P n ∈ S) → ∃ P', ∃ N : ℕ → ℕ, StrictMono N ∧
    Filter.Tendsto (P ∘ N) Filter.atTop (nhds P')) : IsCompact (closure S) := by
  have h : TopologicalSpace.PseudoMetrizableSpace X := by infer_instance;
  obtain ⟨ d, hd ⟩ := h;
  -- Since S is relatively sequentially compact, its closure is sequentially compact.
  have h_seq_compact : IsSeqCompact (closure S) := by
    intro x hx;
    -- For each $n$, since $x_n \in \overline{S}$, there exists $y_n \in S$ such that $d(x_n, y_n) < \frac{1}{n}$.
    have hy : ∀ n, ∃ y ∈ S, dist (x n) y < 1 / (n + 1) := by
      intro n;
      have := hx n;
      -- By definition of closure, every neighborhood of $x_n$ intersects $S$.
      have h_neighborhood : ∀ ε > 0, ∃ y ∈ S, dist (x n) y < ε := by
        bound;
        rw [ Metric.mem_closure_iff ] at this;
        exact this ε a;
      exact h_neighborhood _ <| by positivity;
    choose y hyS hyx using hy;
    obtain ⟨ P', N, hN, hPN ⟩ := hS y hyS;
    bound;
    refine' ⟨ P', _, N, hN, _ ⟩;
    · exact mem_closure_of_tendsto hPN ( by aesop );
    · rw [ tendsto_iff_dist_tendsto_zero ] at *;
      exact squeeze_zero ( fun _ => dist_nonneg ) ( fun n => dist_triangle _ _ _ ) ( by simpa using Filter.Tendsto.add ( squeeze_zero ( fun _ => dist_nonneg ) ( fun n => le_of_lt ( hyx ( N n ) ) ) ( tendsto_one_div_add_atTop_nhds_zero_nat.comp hN.tendsto_atTop ) ) hPN );
  bound;
  convert h_seq_compact.isCompact using 1

some small cleanup yields

import Mathlib

open Filter TopologicalSpace Topology

variable {X : Type*} [TopologicalSpace X] [PseudoMetrizableSpace X]

example {S : Set X} (hS : ∀ (P : ℕ → X), (∀ n, P n ∈ S) → ∃ P', ∃ N : ℕ → ℕ, StrictMono N ∧
    Tendsto (P ∘ N) atTop (𝓝 P')) : IsCompact (closure S) := by
  let := pseudoMetrizableSpacePseudoMetric X
  apply IsSeqCompact.isCompact
  intro x hx
  have hy (n : ℕ) : ∃ y ∈ S, dist (x n) y < 1 / (n + 1) :=
    Metric.mem_closure_iff.mp (hx n) _ (by positivity)
  choose y hyS hyx using hy
  obtain ⟨P', N, hN, hPN⟩ := hS y hyS
  refine ⟨P', mem_closure_of_tendsto hPN (by simp_all), N, hN, ?_⟩
  rw [tendsto_iff_dist_tendsto_zero] at *
  apply squeeze_zero (fun _ => dist_nonneg) (fun n => dist_triangle _ _ _)
  simpa using (squeeze_zero (fun _ => dist_nonneg) (fun n => le_of_lt (hyx (N n)))
    (tendsto_one_div_add_atTop_nhds_zero_nat.comp hN.tendsto_atTop)).add hPN

[Yaël Dillies]

Miyahara Kō said:

Hi, since there hasn’t been much activity in this thread and in the CLT repository recently, I’ve gone ahead and almost fully formalized the proof of Prokhorov’s theorem.

Do you know that this is already being done outside the CLT repo by @Arav Bhattacharyya ?

[Arav Bhattacharyya]

I have almost finished the proof too and can probably PR in the next couple of weeks - sorry progress has been slow due to exams and holidays. I’ll have a look at this when I’m back too

[Lawrence Wu (llllvvuu)]

AI proof of the second lemma (from Harmonic's forthcoming release):

theorem problem {X : Type*} [TopologicalSpace X] [TopologicalSpace.PseudoMetrizableSpace X] {M : Set X} (hM : TopologicalSpace.IsSeparable M) :
    ∃ (𝓐 : Set (Set X)), 𝓐.Countable ∧ (∀ A ∈ 𝓐, IsOpen A) ∧
      ∀ (G : Set X), IsOpen G → ∀ x ∈ M ∩ G,
      ∃ A ∈ 𝓐, x ∈ A ∧ closure A ⊆ G := by
  obtain ⟨D, hD1, hD2⟩ : ∃ D, D.Countable ∧ M ⊆ closure D := by
    bound;
  -- Let $d$ be a pseudometric on $X$ that induces the topology $\tau$.
  obtain ⟨d, hd⟩ : ∃ d : PseudoMetricSpace X, UniformSpace.toTopologicalSpace = ‹TopologicalSpace X› := by
    exact?;
  use { U | ∃ x ∈ D, ∃ q : ℚ, 0 < q ∧ U = Metric.ball x q };
  aesop;
  · -- The set of pairs (x, q) where x ∈ D and q ∈ ℚ is countable because D and ℚ are countable.
    have h_pairs_countable : Set.Countable (Set.image (fun p : X × ℚ => Metric.ball p.1 p.2) (D ×ˢ {q : ℚ | 0 < q})) := by
      exact Set.Countable.image ( hD1.prod ( Set.to_countable _ ) ) _;
    exact h_pairs_countable.mono fun U => by aesop;
  · -- Since $G$ is open and $x \in G$, there exists an $\epsilon > 0$ such that $B(x, \epsilon) \subseteq G$.
    obtain ⟨ε, hε⟩ : ∃ ε > 0, Metric.ball x ε ⊆ G := by
      exact Metric.isOpen_iff.1 a x a_2;
    -- Choose a positive rational number $q \in \mathbb{Q}^+$ such that $0 < q < \frac{\epsilon}{2}$.
    obtain ⟨q, hq_pos, hq_lt⟩ : ∃ q : ℚ, 0 < q ∧ q < ε / 2 := by
      exact mod_cast exists_rat_btwn ( half_pos hε.1 ) |> fun ⟨ q, hq₁, hq₂ ⟩ => ⟨ q, by exact_mod_cast hq₁, hq₂ ⟩;
    -- Since $D$ is dense in $M$, there exists a point $c \in D$ such that $c \in B(x, q)$.
    obtain ⟨c, hc⟩ : ∃ c ∈ D, c ∈ Metric.ball x q := by
      have := hD2 a_1;
      rw [ Metric.mem_closure_iff ] at this ; aesop;
      simpa only [ dist_comm ] using this q ( mod_cast hq_pos );
    refine' ⟨ _, ⟨ c, hc.1, q, hq_pos, rfl ⟩, _, _ ⟩ <;> aesop;
    · rwa [ dist_comm ];
    · -- Let $y$ be an arbitrary point in $\text{closure}(B(c, q))$. Then $d(y, c) \le q$.
      intro y hy
      have h_dist : dist y c ≤ q := by
        rw [ Metric.mem_closure_iff ] at hy;
        exact le_of_forall_pos_le_add fun δ δ_pos => by rcases hy δ δ_pos with ⟨ b, hb, hb' ⟩ ; linarith [ dist_triangle y b c, Metric.mem_ball.mp hb ] ;
      exact right ( Metric.mem_ball.2 <| by linarith [ dist_triangle y c x ] )

bit of cleanup (can surely clean up more):

import Mathlib

open Filter TopologicalSpace Topology

variable {X : Type*} [TopologicalSpace X] [PseudoMetrizableSpace X]

example {M : Set X} (hM : IsSeparable M) :
    ∃ (𝓐 : Set (Set X)), 𝓐.Countable ∧ (∀ A ∈ 𝓐, IsOpen A) ∧
      ∀ (G : Set X), IsOpen G → ∀ x ∈ M ∩ G,
      ∃ A ∈ 𝓐, x ∈ A ∧ closure A ⊆ G := by
  obtain ⟨D, hD1, hD2⟩ := hM
  let := pseudoMetrizableSpacePseudoMetric X
  let 𝓐 := (fun p : X × ℚ ↦ Metric.ball p.1 p.2) '' D ×ˢ {q | 0 < q}
  refine ⟨𝓐, (hD1.prod (Set.to_countable _)).image _, ⟨by rintro _ ⟨_, _, rfl⟩; simp, ?_⟩⟩
  intro G hG x ⟨hxM, hxG⟩
  obtain ⟨ε, hε0, hεG⟩ : ∃ ε > 0, Metric.ball x ε ⊆ G := Metric.isOpen_iff.1 hG x hxG
  obtain ⟨q, hq_pos, hq_lt⟩ : ∃ q : ℚ, 0 < q ∧ q < ε / 2 := mod_cast exists_rat_btwn (half_pos hε0)
  obtain ⟨c, hcD, hcb⟩ : ∃ c ∈ D, dist x c < q := by
    simp [Metric.mem_closure_iff.mp (hD2 hxM) q (mod_cast hq_pos)]
  refine ⟨_, ⟨⟨c, q⟩, ⟨hcD, hq_pos⟩, rfl⟩, by simpa, ?_⟩
  intro y hy
  have h_dist : dist y c ≤ q := by
    rw [Metric.mem_closure_iff] at hy
    refine le_of_forall_pos_le_add fun δ δ_pos => ?_
    obtain ⟨b, hb, hb'⟩ := hy δ δ_pos
    linarith [dist_triangle y b c, Metric.mem_ball.mp hb]
  exact hεG (Metric.mem_ball.mpr <| by linarith [dist_triangle_right y x c])

[Rémy Degenne]

For Prokhorov's theorem we were indeed waiting for Arav, who was doing it as a university project (as written higher in this thread; this is the reason the code contained sorry -- do not work on this. Somebody claimed it).
But it's better to have two proofs than none, and I guess that you did not prove it exactly in the same way, so there will be different auxiliary lemmas you can PR to Mathlib.

But actually I see that you did not prove that sorry but the next one in the file, about getting one of the two directions of Prokhorov's theorem with weaker hypothesis? Did you use the first theorem to then relax the assumptions (as I thought we would do), or did you prove it from scratch?

[Rémy Degenne]

I got to a computer and checked: @Miyahara Kō doesn't apparently use isTightMeasureSet_iff_isCompact_closure in the proof of the implication with relaxed hypotheses isCompact_closure_of_isTightMeasureSet. So that's a full proof for one of the implications of Prokhorov's theorem.

[Lawrence Wu (llllvvuu)]

Aaron Liu said:

I guess you can simultaneously do the open-closed-open thing for each point in $M$ and use lindelöf to extract a countable subcover

could be annoying to work in the subspace topology on $M$ (consider closed $M$ with $x$ on the boundary, then you need $A \in \mathcal{A}$ with $A \not\subseteq M$, so you have to enlarge everything correctly)

[Aaron Liu]

Lawrence Wu (llllvvuu) said:

Aaron Liu said:

I guess you can simultaneously do the open-closed-open thing for each point in $M$ and use lindelöf to extract a countable subcover

could be annoying to work in the subspace topology on $M$ (consider closed $M$ with $x$ on the boundary, then you need $A \in \mathcal{A}$ with $A \not\subseteq M$, so you have to enlarge everything correctly)

This was indeed weirdly annoying (and my proof was wrong, thanks Lean for helping me figure that out) so I resorted to using epsilons again

[Aaron Liu]

here it is

import Mathlib

open Filter TopologicalSpace Topology

variable {X : Type*} [TopologicalSpace X] [PseudoMetrizableSpace X]

example {M : Set X} (hM : IsSeparable M) :
    ∃ (𝓐 : Set (Set X)), 𝓐.Countable ∧ (∀ A ∈ 𝓐, IsOpen A) ∧
      ∀ (G : Set X), IsOpen G → ∀ x ∈ M ∩ G,
      ∃ A ∈ 𝓐, x ∈ A ∧ closure A ⊆ G := by
  let := pseudoMetrizableSpacePseudoMetric X
  obtain ⟨t, ht, sc⟩ := hM
  rw [← Set.countable_coe_iff] at ht
  obtain ⟨us, hus, tus⟩ : ∃ us : ℕ → ℝ, (∀ n, 0 < us n) ∧ Tendsto us atTop (𝓝 0) :=
    ⟨fun n => 1 / (n + 1), fun _ => by positivity, tendsto_one_div_add_atTop_nhds_zero_nat⟩
  let k (n : t × ℕ) : Set X := Metric.ball n.1.1 (us n.2)
  refine ⟨Set.range k, Set.countable_range k,
    Set.forall_mem_range.2 fun _ => Metric.isOpen_ball, ?_⟩
  intro G hG x ⟨hxM, hxG⟩
  obtain ⟨ε, hε, hεG⟩ := Metric.mem_nhds_iff.1 (hG.mem_nhds hxG)
  obtain ⟨c, hc⟩ := (Metric.tendsto_nhds.1 tus (ε / 2) (by positivity)).exists
  rw [Real.dist_0_eq_abs, abs_of_pos (hus c)] at hc
  obtain ⟨ut, hut, hεut⟩ := Metric.mem_closure_iff.1 (sc hxM) (us c / 2) (half_pos (hus c))
  refine ⟨k (⟨ut, hut⟩, c), Set.mem_range_self _, ?_, ?_⟩
  · apply Metric.mem_ball.2
    apply hεut.trans
    linarith [hus c]
  · apply Metric.closure_ball_subset_closedBall.trans
    exact (Metric.closedBall_subset_ball' (by linarith [dist_comm x ut])).trans hεG

[Miyahara Kō]

@Lawrence Wu (llllvvuu) @Aaron Liu Thank you!
I pushed @Lawrence Wu (llllvvuu)'s proofs, and CLT is now sorry-free!!!

import Clt.CLT

/--
info: 'ProbabilityTheory.central_limit' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms ProbabilityTheory.central_limit

[Miyahara Kō]

https://github.com/RemyDegenne/CLT/pull/56

[Miyahara Kō]

@Rémy Degenne
Unfortunately, my proof of Prokhorov's theorem requires second countable topology because deducing relatively compactness from relatively sequentially compactness requires the space of probability measure is pseudometrizable, and metrizability of the space of probability measure requires the space is second countable.

[Miyahara Kō]

If @Arav Bhattacharyya's proof doesn't requires second countable topology, that's awesome.

[Rémy Degenne]

I'll summarize what we have about Prokhorov's theorem and what else could be done, based on theorem 23.2 in Kallenberg's Foundations of Modern Probability (3rd ed).
The general setting is this:

variable {E : Type*} {mE : MeasurableSpace E} [MetricSpace E] [BorelSpace E]
  {S : Set (ProbabilityMeasure E)}

Then we consider two properties:

1. IsTightMeasureSet {((μ : ProbabilityMeasure E) : Measure E) | μ ∈ S}
2. IsCompact (closure S)

Theorem 23.2 states that

• (1) implies (2), without additional hypotheses
• If [CompleteSpace E] [SecondCountableTopology E] then (2) implies (1)

In the PR, @Miyahara Kō proved that (1) imples (2) under the additional assumption [SecondCountableTopology E].
If you look at the proof in Kallenberg's book, page 508, you'll see that the fact that (1) implies (2) is also first proved for separable spaces, and then at the end the general case is reduced to the separable case (see the paragraph "Now turn to the general case" at the bottom of page 508). So it would be nice to prove that extension.

And we are missing the other direction, that (2) implies (1). But perhaps @Arav Bhattacharyya proved that one?

None of this is required for the CLT, which is sorry free on the branch of the PR. But it would be nice to have it.

[Miyahara Kō]

In Kallenberg's book, "relatevely compact" means relatively sequentially compact: every sequence in the set has converging subsequence, but the limit point is not necessarily in the set.
This is not the same to relatively compactness in isCompact_closure_of_isTightMeasureSet: the closure of the set is compact.
So, if you want to drop second countability, the conclusion of isCompact_closure_of_isTightMeasureSet should be changed to relatively sequentially compactness.

[Rémy Degenne]

Oh right, I did not see that.

[Sébastien Gouëzel]

Isn't it true that the closure is compact in the usual sense?

[Arav Bhattacharyya]

Miyahara Kō said:

If Arav Bhattacharyya's proof doesn't requires second countable topology, that's awesome.

Sorry for the slow reply - my proof also uses a sequential compactness argument so it will require the second countable assumption too.

[Arav Bhattacharyya]

Rémy Degenne said:

And we are missing the other direction, that (2) implies (1). But perhaps Arav Bhattacharyya proved that one?

Yes this is complete. I started PRing it a while back but closed it to break it into smaller chunks. I will open a PR when I get back to my computer in a couple of days

[Arav Bhattacharyya]

The majority of my proof is complete and will be useful for other parts of the library I think, so I will open PRs for those too.

[Yongxi Lin (Aaron)]

Rémy Degenne said:

I'll summarize what we have about Prokhorov's theorem and what else could be done, based on theorem 23.2 in Kallenberg's Foundations of Modern Probability (3rd ed).
The general setting is this:

variable {E : Type*} {mE : MeasurableSpace E} [MetricSpace E] [BorelSpace E]
  {S : Set (ProbabilityMeasure E)}

Then we consider two properties:

1. IsTightMeasureSet {((μ : ProbabilityMeasure E) : Measure E) | μ ∈ S}
2. IsCompact (closure S)

Theorem 23.2 states that

• (1) implies (2), without additional hypotheses
• If [CompleteSpace E] [SecondCountableTopology E] then (2) implies (1)

In the PR, Miyahara Kō proved that (1) imples (2) under the additional assumption [SecondCountableTopology E].
If you look at the proof in Kallenberg's book, page 508, you'll see that the fact that (1) implies (2) is also first proved for separable spaces, and then at the end the general case is reduced to the separable case (see the paragraph "Now turn to the general case" at the bottom of page 508). So it would be nice to prove that extension.

And we are missing the other direction, that (2) implies (1). But perhaps Arav Bhattacharyya proved that one?

None of this is required for the CLT, which is sorry free on the branch of the PR. But it would be nice to have it.

I do think that (1) implies (2) without additional assumptions. I am using Bogachev's Measure Theory as my reference. Let me first list some related definitions and theorems in this book. Assume $\mu$ is a finite Borel measure.

1. Definition 7.1.1: $\mu$ is a Radon measure if for any Borel set $B$ and $\varepsilon>0$, there exists a compact set $K_\varepsilon\subset B$ such that $\mu(B\setminus K_\varepsilon)<\varepsilon$.
2. Definition 7.1.5: $\mu$ is regular if for any Borel set $B$ and $\varepsilon>0$, there exists a closed set $F_\varepsilon\subset B$ such that $\mu(B\setminus F_\varepsilon)<\varepsilon$.
3. From the definitions above, it is easy to see that if $\mu$ is regular and tight, then it is Radon.
4. Theorem 7.1.7: Every Borel measure defined on a metric space is regular.
5. Theorem 8.6.7: Let $\mathcal{K}$ be a subset of Radon measures that is both tight and bounded (in the variation norm) defined on a completely regular space $E$. Then $\mathcal{K}$ has compact closure in the weak topology.

Now we are ready to prove (1) implies (2) without any additional assumptions. Let $S$ be a tight set of probability measures defined on a metric space $E$. Every element of $S$ is regular and tight and hence Radon. $S$ is clearly bounded in the variation norm. $E$ is completely regular. Therefore, we can use Theorem 8.6.7 to deduce that $S$ has compact closure in the weak topology.

Bogachev actually proves 8.6.7 for complex measures. The definitions above still make sense for complex measure if we use the total variation.