[Merged by Bors] - feat(MeasureTheory/Function): ae convergence implies convergence in distribution

[jvanwinden]

This PR introduces a theorem which concludes convergence in distribution from almost everywhere convergence.

Previously, this could be done by chaining tendstoInMeasure_of_tendsto_ae and TendstoInMeasure.tendstoInDistribution.
However, this is not a good way to to it since the second lemma requires a SeminormedAddCommGroup E instance (which is not needed for the statement to hold). Thus, we instead give a direct short proof which relies on dominated convergence.

As a consequence, we also obtain a new proof of TendstoInMeasure.tendstoInDistribution which does not pass through tendstoInDistribution_of_tendstoInMeasure_sub and therefore does not require SeminormedAddCommGroup and SecondCountableTopology anymore. I expect this will enable significant golfing (or maybe even removal) of tendstoInDistribution_of_tendstoInMeasure_sub in the future.

In order to allow for ae measurability as an assumption, it was necessary to add tendsto_lintegral_filter_of_dominated_convergence', which gives dominated convergence along a countable filter for AEMeasurable functions.

Sidenote: I believe TendstoInMeasure.tendstoInDistribution should be rewritten at some point to require only a metric space (or maybe only uniform space) structure. However, even if this was done, the theorem of this PR provides the value of relying only on TopologicalSpace E.

---

• depends on: [Merged by Bors] - feat: another version of dominated convergence for AEMeasurable functions #39768

[github-actions]

PR summary b838ba2ec6

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ apply_le_edist_zero
+ tendstoInDistribution_of_ae_tendsto

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

---

No changes to strong technical debt.

No changes to weak technical debt.

[CoolRmal]

You need a notion of distance for TendstoInMeasure, so what you said about uniform space is not correct.

[CoolRmal]

And actually I think the proof of TendstoInMeasure.tendstoInDistribution for a (pseudo)(e)metric space (not sure whether you can do it for pseudo/extended metric) follows from the lemma you proved in this PR by using MeasureTheory.TendstoInMeasure.exists_seq_tendsto_ae' and Filter.tendsto_iff_seq_tendsto. Do you want to formalize this? If so, I think you can create a new PR dependent on this one.

[jvanwinden]

You need a notion of distance for TendstoInMeasure, so what you said about uniform space is not correct.

I am aware of this, but what I meant here was that the definition of TendstoInMeasure itself could perhaps be generalized to uniform spaces. Although I am not familiar enough with uniform spaces to way whether the proofs would carry over.

[jvanwinden]

And actually I think the proof of TendstoInMeasure.tendstoInDistribution for a (pseudo)(e)metric space (not sure whether you can do it for pseudo/extended metric) follows from the lemma you proved in this PR by using MeasureTheory.TendstoInMeasure.exists_seq_tendsto_ae' and Filter.tendsto_iff_seq_tendsto. Do you want to formalize this? If so, I think you can create a new PR dependent on this one.

I had also been thinking about this route, and I think it would be a good idea. In the coming week I can check if a nice proof indeed falls out.

[CoolRmal]

You need a notion of distance for TendstoInMeasure, so what you said about uniform space is not correct.

I am aware of this, but what I meant here was that the definition of TendstoInMeasure itself could perhaps be generalized to uniform spaces. Although I am not familiar enough with uniform spaces to way whether the proofs would carry over.

Oh I think I see what you mean. This is interesting! Maybe I'll do an experiment with the definition of TendstoInMeasure recently.

[jvanwinden]

And actually I think the proof of TendstoInMeasure.tendstoInDistribution for a (pseudo)(e)metric space (not sure whether you can do it for pseudo/extended metric) follows from the lemma you proved in this PR by using MeasureTheory.TendstoInMeasure.exists_seq_tendsto_ae' and Filter.tendsto_iff_seq_tendsto. Do you want to formalize this? If so, I think you can create a new PR dependent on this one.

I had also been thinking about this route, and I think it would be a good idea. In the coming week I can check if a nice proof indeed falls out.

A nice proof did indeed fall out (currently 6 lines, plus it generalizes SeminormedAddCommGroup to PseudoEMetricSpace and removes SecondCountableTopology. I will clean it up and add it to this PR.

[jvanwinden]

awaiting-author

[jvanwinden]

You need a notion of distance for TendstoInMeasure, so what you said about uniform space is not correct.

I am aware of this, but what I meant here was that the definition of TendstoInMeasure itself could perhaps be generalized to uniform spaces. Although I am not familiar enough with uniform spaces to way whether the proofs would carry over.

Oh I think I see what you mean. This is interesting! Maybe I'll do an experiment with the definition of TendstoInMeasure recently.

Funnily enough, the characterization of convergence in measure in terms of a.e. convergent subsequences does not even require a uniformity! Thus it would even be possible to write a definition of TendstoInMeasure which only requires a topology.

I am not sure if I would advocate for this, since it is not the standard definition and the equivalence only holds for countably generated filters, but I do think this is something worth thinking about.

[CoolRmal]

May you be more specific about how you would like to define TendstoInMeasure by using only topology? Here's a list of definitions that I am thinking about.

import Mathlib.MeasureTheory.Measure.MeasureSpaceDef

open scoped Topology

open Filter

def MeasureTheory.TendstoInMeasure {ι α E : Type*} [EDist E] {m : MeasurableSpace α} 
    (μ : Measure α) (f : ι → α → E) (l : Filter ι) (g : α → E) : Prop := 
  ∀ ε, 0 < ε → Tendsto (fun i => μ { x | ε ≤ edist (f i x) (g x) }) l (𝓝 0)

def MeasureTheory.TendstoInMeasure' {ι α E : Type*} [UniformSpace E] {m : MeasurableSpace α} 
    (μ : Measure α) (f : ι → α → E) (l : Filter ι) (g : α → E) : Prop := 
  ∀ s ∈ uniformity E, Tendsto (fun i => μ { x | ⟨f i x, g x⟩ ∉ s }) l (𝓝 0)

def MeasureTheory.TendstoInMeasure'' {ι α E : Type*} [TopologicalSpace E] {m : MeasurableSpace α} 
    (μ : Measure α) (f : ι → α → E) (l : Filter ι) (g : α → E) : Prop := 
  ∀ s : α → Set E, (∀ x, s x ∈ 𝓝 (g x)) → Tendsto (fun i => μ { x | f i x ∉ s x }) l (𝓝 0)

def MeasureTheory.TendstoInMeasure''' {ι α E : Type*} [TopologicalSpace E] {m : MeasurableSpace α} 
    (μ : Measure α) (f : ι → α → E) (l : Filter ι) (g : α → E) : Prop := 
  ∀ s ∈ 𝓝 g, Tendsto (fun i => μ { x | f i x ∉ (Function.eval x '' s) }) l (𝓝 0)

The first one is just the classical definition used in Mathlib right now. It naturally leads to the second definition (as a uniform space structure can be constructed from a pseudoEMetricSpace by uniformSpaceOfEDist). The second definition is not really more general than the first one, as an EDist does not always induces a uniform strucutre, but I believe both definitions are equivalent with MeasureTheory.tendstoInMeasure_iff_dist in the case that E is a pseudometric space.

The third and the fourth definitions are my guesses of how we should define it in a general topological space, but I don't think they give an equivalent definition with the classical one when E is a pseduometric space.

Maybe we should create a Zulip thread for this.

[jvanwinden]

I have added the new proof of TendstoInMeasure.tendstoInDistribution. I expect that this will enable us to significantly golf (or perhaps even remove?) tendstoInDistribution_of_tendstoInMeasure_sub. But this PR is already experiencing some scope creep.

[jvanwinden]

-awaiting-author

[jvanwinden]

May you be more specific about how you would like to define TendstoInMeasure by using only topology? Here's a list of definitions that I am thinking about.

import Mathlib.MeasureTheory.Measure.MeasureSpaceDef

open scoped Topology

open Filter

def MeasureTheory.TendstoInMeasure {ι α E : Type*} [EDist E] {m : MeasurableSpace α} 
    (μ : Measure α) (f : ι → α → E) (l : Filter ι) (g : α → E) : Prop := 
  ∀ ε, 0 < ε → Tendsto (fun i => μ { x | ε ≤ edist (f i x) (g x) }) l (𝓝 0)

def MeasureTheory.TendstoInMeasure' {ι α E : Type*} [UniformSpace E] {m : MeasurableSpace α} 
    (μ : Measure α) (f : ι → α → E) (l : Filter ι) (g : α → E) : Prop := 
  ∀ s ∈ uniformity E, Tendsto (fun i => μ { x | ⟨f i x, g x⟩ ∉ s }) l (𝓝 0)

def MeasureTheory.TendstoInMeasure'' {ι α E : Type*} [TopologicalSpace E] {m : MeasurableSpace α} 
    (μ : Measure α) (f : ι → α → E) (l : Filter ι) (g : α → E) : Prop := 
  ∀ s : α → Set E, (∀ x, s x ∈ 𝓝 (g x)) → Tendsto (fun i => μ { x | f i x ∉ s x }) l (𝓝 0)

def MeasureTheory.TendstoInMeasure''' {ι α E : Type*} [TopologicalSpace E] {m : MeasurableSpace α} 
    (μ : Measure α) (f : ι → α → E) (l : Filter ι) (g : α → E) : Prop := 
  ∀ s ∈ 𝓝 g, Tendsto (fun i => μ { x | f i x ∉ (Function.eval x '' s) }) l (𝓝 0)

The first one is just the classical definition used in Mathlib right now. It naturally leads to the second definition (as a uniform space structure can be constructed from a pseudoEMetricSpace by uniformSpaceOfEDist). The second definition is not really more general than the first one, as an EDist does not always induces a uniform strucutre, but I believe both definitions are equivalent with MeasureTheory.tendstoInMeasure_iff_dist in the case that E is a pseudometric space.

The third and the fourth definitions are my guesses of how we should define it in a general topological space, but I don't think they give an equivalent definition with the classical one when E is a pseduometric space.

Maybe we should create a Zulip thread for this.

What I meant with TopologicalSpace was the following: for sequences of (finite) measures, convergence in probability is equivalent to the statement that every subsequence has a further subsequence which converges almost surely. But this subsequence property only requires a TopologicalSpace instance. Thus we could use this as a definition instead.

However, there is the issue that this characterization only holds true for finite measures and countably generated filters. And I would expect that these drawbacks weigh more heavily than the benefit of generalizing from UniformSpace to TopologicalSpace.

[jvanwinden]

-awaiting-author

[jvanwinden]

-awaiting-author

[github-actions]

🚀 Pull request has been placed on the maintainer queue by EtienneC30.

[RemyDegenne]

Thanks!
bors r+

[jvanwinden]

Thanks for the thorough reviews! I learned some new tricks.

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Post-Build Step
• ci (staging) / Lint style
• ci (staging) / Build
• ci (staging) / Post-CI job