Tight measures

Stream: Is there code for X?

[Josha Dekker]

Hi, I've noticed that tight measures are missing from mathlib, is anyone working on these? Otherwise I'd be happy to develop some API!

[Kexing Ying]

iirc @Kalle Kytölä was working on Prokhorov's theorem.

[Kalle Kytölä]

I haven't really started working on tightness per se! It would be great to see these developed!

[Kalle Kytölä]

The main thing that I planned was Prokhorov's theorem via Riesz-Markov-Kakutani on compact spaces plus Banach-Alaoglu. But I have not done it (one significant reason is that I had not yet gotten to PRing the Riesz-Markov-Kakutani). And even excluding Prokhorov's theorem, there would be a fair amount of API about tight measures that should be added.

(I do have a personal preference for the Prokhorov proof along the above mentioned route, but if you end up doing that via another route, then it is still better to have in Mathlib than not have it at all! :smile:)

[Kalle Kytölä]

So @Josha Dekker, please go ahead if you want to develop tightness!

We should just slightly coordinate regarding the remaining parts of weak convergence theory. The Lévy-Prokhorov metric is still in an open PR #11549. There are some other parts of the weak convergence API that I plan to fill in as soon as I have time (next week when I'm back from a conference should be my semester's almost last two exam gradings so I expect to have more time in relatively near future). Also one portmanteau implication is sequential in its current formulation, and I intend to fix this. It doesn't really matter when one has metrizability, but it is not mathlib-stylish as it is. I had something on cdf's, but I might have to rewrite to connect better to what exists... Also if that overlaps with your tightness plans, you can do the relevant cdf API, too.

[Kalle Kytölä]

...and once we have Measure.real (from the PFR project) I would like to clean up some of docs#MeasureTheory.ProbabilityMeasure and docs#MeasureTheory.FiniteMeasure with it.

[Josha Dekker]

Kalle Kytölä said:

So Josha Dekker, please go ahead if you want to develop tightness!

We should just slightly coordinate regarding the remaining parts of weak convergence theory. The Lévy-Prokhorov metric is still in an open PR #11549. There are some other parts of the weak convergence API that I plan to fill in as soon as I have time (next week when I'm back from a conference should be my semester's almost last two exam gradings so I expect to have more time in relatively near future). Also one portmanteau implication is sequential in its current formulation, and I intend to fix this. It doesn't really matter when one has metrizability, but it is not mathlib-stylish as it is. I had something on cdf's, but I might have to rewrite to connect better to what exists... Also if that overlaps with your tightness plans, you can do the relevant cdf API, too.

No worries, I'm not necessarily planning to tackle Prokhorov at this point. I just noted tightness was missing, and thought it would be a nice opportunity to familiarise myself more with this region of Mathlib

[Josha Dekker]

I will just write up some general tightness API, but if you have special orders, let me know and I'll see what I can do (assuming my own research permits me the time...)

[Ruben Van de Velde]

Sounds like the two of you should be reviewing each other's PRs, so we can get them in quicker :)

[Josha Dekker]

Ruben Van de Velde said:

Sounds like the two of you should be reviewing each other's PRs, so we can get them in quicker :)

Sure, feel free to tag me, @Kalle Kytölä! I'm not a very experienced reviewer at this point, but I'm happy to chip in!

[Kalle Kytölä]

Ruben Van de Velde said:

Sounds like the two of you should be reviewing each other's PRs, so we can get them in quicker :)

:sweat_smile: I agree! (...but for a week or so still, I doubt I would get any reviewing done. Hopefully better in near future!)

[Jireh Loreaux]

@Kalle Kytölä and @Josha Dekker, have you seen #12290 about RMK? It's not complete yet, and there's still some work to be done to get it into a good form, but it's a start on getting a more general version.

[Josha Dekker]

yes, it would certainly be good to have this. I think this is going to depend on having a type class for compactly supported continuous functions, judging from the conversations, so I’ll keep an eye out for this work!

[Josha Dekker]

(Pre-)Tight measures are defined in  #12394. This is very much WIP. I'm sharing as I welcome suggestions on missing parts of the API. Currently it is very bare-bones. Also, if anyone has a good suggestion where my lemma's aux1 and aux2 should go/are in Mathlib, I'm happy to hear this!

[Josha Dekker]

I don't think we have the notion of Separable Measures yet, right? (These are measures that assign full measure to a separable set). I'll make a separate PR for these, along with some very small API. This property is weaker than tightness on metric spaces but equivalent on complete metric spaces (which is occasionally useful).

[Josha Dekker]

Separable measures are in #12396, but I'm a bit short on inspiration about what API I can write for them that isn't "infer IsSeparable from IsTight" (all of which need to be in #12394, as I think the file on tightness should import the file on separable, not vice versa)

[Rémy Degenne]

I guess that you don't know what API you should prove for separable measures because you don't have any use for those measures (yet?). If you don't need them, the best course of action might simply be to not add them, and wait until you need them for something. A definition without API is useless, and a definition that is not tested in an application might be a "wrong" definition, in the sense that the way it is formalized is unusable. Of course I am not saying that those separable measures are useless in general (I don't know about that): I am only remarking that they seem useless to you for now.

In contrast, you have apparently no trouble finding stuff to add about tight measures because there is a clear use case discussed in this thread. This is in my opinion a much better way to develop the library: pick a goal and then add the missing definitions and theorems that are useful towards that goal, rather than add something just because it's a definition that exists in some book and that is not in mathlib yet.

[Josha Dekker]

Yes, in a sense that is correct, although tight measures and separable measures have some interplay: on complete metric spaces, Borel measures are pretight iff tight iff separable. It is furthermore consistent with ZF that all Borel measures on metric spaces are separable.

Along this, we have the advantage that separable measures also have nice characterisations for weak convergence (where we only have to consider fewer test functions). Also, if I recall correctly, general versions of convergence results like Slutsky require the limiting distribution to be separable.

[Josha Dekker]

But I agree that building API purely for the sake of building API is not the way to go. I'm putting my definition of Separable measures in  #12396 for now, as it sometimes is convenient to move from tightness to separability of a measure.

[Sébastien Gouëzel]

Josha Dekker said:

Yes, in a sense that is correct, although tight measures and separable measures have some interplay: on complete metric spaces, Borel measures are pretight iff tight iff separable. It is furthermore consistent with ZF that all Borel measures on metric spaces are separable.

I don't know anything about separable measures, but I don't see how this statement could be true. Take a very big Hilbert space, and define a measure mu by mu s = 0 is s is contained in a countable union of balls of radius 1, and mu s = \infty otherwise. This is a Borel measure on a metric space, but it is not separable if I understand your definition correctly.

[Josha Dekker]

Sébastien Gouëzel said:

Josha Dekker said:

Yes, in a sense that is correct, although tight measures and separable measures have some interplay: on complete metric spaces, Borel measures are pretight iff tight iff separable. It is furthermore consistent with ZF that all Borel measures on metric spaces are separable.

I don't know anything about separable measures, but I don't see how this statement could be true. Take a very big Hilbert space, and define a measure mu by mu s = 0 is s is contained in a countable union of balls of radius 1, and mu s = \infty otherwise. This is a Borel measure on a metric space, but it is not separable if I understand your definition correctly.

You are absolutely right, I should've specified that I'm assuming here that we are looking at finite measures (typically, probability measures even)

[Josha Dekker]

just a very brief update: I’ve defined separable measures, pretight measures and tight measures so far, and I’m proving the necessary relationships between them while I go to make sure the definitions are sensible. I’m literally an epsilon away from the Ulam tightness theorem, which is the last ingredient I need for showing that under some niceness conditions, separable measures are in fact right. I didn’t commit this yet, but I’m hoping to finish that tomorrow/friday, so that the PR can be up for review! Uniform tightness/asymptotic tightness are deferred for now, as we had some discussions in a different thread about how best to formalize them in terms of filters!

[Vincent Beffara]

For uniform and asymptotic tightness (and for tightness of a single measure as well), a filtery definition (from that other thread) could be like this:

def IsTight (μ : Measure α) : Prop := Tendsto μ (cocompact α).smallSets (𝓝 0)

def IsUniformlyTight (μ : ι → Measure α) : Prop :=
    TendstoUniformly (fun A i => μ i A) 0 (cocompact α).smallSets

def IsTightAtFilter (μ : ι → Measure α) (F : Filter ι) : Prop :=
    TendstoUniformlyOnFilter (fun A i => μ i A) 0 (cocompact α).smallSets F

except the last two don't work now because of a missing UniformSpace instance on ENNReal (and the last one might not be what you want).

[Josha Dekker]

Vincent Beffara said:

For uniform and asymptotic tightness (and for tightness of a single measure as well), a filtery definition (from that other thread) could be like this:

def IsTight (μ : Measure α) : Prop := Tendsto μ (cocompact α).smallSets (𝓝 0)

def IsUniformlyTight (μ : ι → Measure α) : Prop :=
    TendstoUniformly (fun A i => μ i A) 0 (cocompact α).smallSets

def IsTightAtFilter (μ : ι → Measure α) (F : Filter ι) : Prop :=
    TendstoUniformlyOnFilter (fun A i => μ i A) 0 (cocompact α).smallSets F

except the last two don't work now because of a missing UniformSpace instance on ENNReal (and the last one might not be what you want).

Thanks! I’ll wait for that instance to land then, then I’ll start playing around with these definitions!

[Josha Dekker]

Hi, #12394 is up for review and defines IsSeparable, IsPretight and IsTight and shows some relationships between them. Main result is Ulam's tightness theorem (and a strengthened version that only requires IsSeparable rather than SeparableSpace. It is still building, but I don't expect any problems there! I think most results are straightforward, although some proofs are a bit longish: I've used 4 private lemma's to break up the work a bit, but still Ulam's tightness theorem and its strengthened form require some legwork.

[Vincent Beffara]

Still pushing for the use of filters: e.g.

lemma of_compactSpace {μ : Measure α} [TopologicalSpace α] [CompactSpace α] : IsTight μ := by
  simpa [IsTight, Tendsto] using pure_le_nhds 0

[Josha Dekker]

Vincent Beffara said:

Still pushing for the use of filters: e.g.

lemma of_compactSpace {μ : Measure α} [TopologicalSpace α] [CompactSpace α] : IsTight μ := by
  simpa [IsTight, Tendsto] using pure_le_nhds 0

Thanks, I’ll try and see soon if I can refactor some of them in terms of filters!

[Josha Dekker]

Do you think (almost) all proofs should be based on filters if (reasonably) possible? Or do you think that it is okay to just use the epsilon-based definition if it is more convenient?

[Vincent Beffara]

I guess whatever is more convenient works in proofs, but using filters tends to make proofs easier. Typically,

lemma add [TopologicalSpace α] {μ ν : Measure α} (hμ : IsTight μ) (hν : IsTight ν) :
    IsTight (μ + ν) := by
  simpa only [add_zero] using hμ.add hν

(which is essentially your version) is much easier than slicing epsilons and taking unions :-)

[Peter Pfaffelhuber]

Is there any news on this PR? We are in the process of proving that algebras which separate points are separating (in a complete and separable metric space). One step requires to use that single finite measures are tight.

[Josha Dekker]

I’m a bit swamped by work for the next few weeks (research, thesis supervision, etc), so I won’t be able to properly integrate the final remarks before late July, I think. It shouldn’t be too hard, but I can’t afford to make the headspace for Lean right now. Please feel free to pick what you want from the PR/incorporate the remaining comments there! I’m happy to advise!

[Josha Dekker]

@Peter Pfaffelhuber if I do manage to find a good opportunity anyway I'll make sure to post here first, but I don't expect that to be the case in the next two weeks for sure... I think the details that are still open are not too tricky. Perhaps you find Ulam's tightness theorem useful as well, that one is in there as well!