Outer/inner probability and integrals

Stream: Is there code for X?

[Josha Dekker]

I'm soon starting a reading group on the book "Weak Convergence and Empirical Processes" and I'm curious, do we have the concepts of outer/inner integrals and probability? These are the extensions of the usual notions to the case where the involved function $T$ fails to be measurable. These are defined by taking infs (resp. sups) over functions $U\geq T$ (resp. $U\leq T$). I'm not asking for outer measure here, a quick Moogle search suggested not, but I've missed obvious stuff there before...

[Josha Dekker]

If we do not have them yet, would we like to have outer/inner integrals defined in full generality, or only with respect to probability measures (I guess in the latter case a more suitable name would then be outer/inner expectations perhaps)? Outer/inner probability is of course just the outer/inner measure corresponding to a probability measure, so we effectively have that. I'm happy to code up some basic API if there is interest in this, although I could probably use a second pair of eyes to ensure that I get the definitions right before I start!

[Josha Dekker]

Screenshot-2024-02-04-at-14.54.28.png
To be specific, I would like to extend this to a general setting: we can probably work on any (sigma-finite?) measure space and with maps $T$ into some space that generalises $\bar{\mathbb{R}}$ and that has a definition for inf and sup? From what I've understood, EReal is not the nicest thing to work on, so any guidance/a definition that I can start from would be greatly appreciated!

[Josha Dekker]

From this, we could define weak convergence of a sequence of arbitrary (= not necessarily measurable) maps and set up e.g. a portmanteau theorem for weak convergence.

[Josha Dekker]

(E = integral wrt P in the picture by the way)

[Sébastien Gouëzel]

The question you are asking only makes sense for real or ereal or ennreal-valued functions, say. The very definition of the Lebesgue integral for ennreal-valued functions f is the supremum of the integral of simple functions bounded above by f, so this is one of the integrals you are mentioning (the inner one, probably). We haven't the other one, as far as I can tell, because the important thing is to make a coherent choice once and for all in the library -- anyway, integrals of non-measurable functions are bad enough that they're not really useful for serious applications as far as I can tell. I would only advise you to formalize this if you have an application in mind where this is important, as a definition like that comes with a heavy API cost: you would need to formalize a big bunch of properties to make it useful in general.

[Josha Dekker]

I see, thank you. In e.g. empirical process theory, you sometimes work with sequences of non-measurable functions where the limit of the functions is measurable. By working with outer integrals, you can actually still get a meaningful theory of stochastic convergence when the functions fail to be measurable. Do you think this would be something worth formalizing? I would essentially try to formalise some aspects of chapter 1 of Van der Vaart and Wellner - Weak Convergence and Empirical Processes. Let me know!

[Sébastien Gouëzel]

I'm not used to this point of view (to me the usual thing to do is to use one of the Skohorod metrics), but I don't think you need to add any definition to mathlib to formalize it: since this notion of convergence uses continuous bounded functions, it's not really important to use the extended real line, you could as well use the real line, or the nonnegative reals. And since the definition given in the book is invariant by replacing f with -f, you could use the inner integral instead of the outer one, it would give you the same notion of convergence. To summarize, the notion of weak convergence defined in the book is equivalent to convergence of inner integrals of bounded continuous functions valued in ennreal. All the words in the latter sentence are already defined in mathlib, and ready to be used!

[Sébastien Gouëzel]

(And many results about the Lebesgue integral in mathlib are already formulated minimizing the measurability assumptions.)

[Josha Dekker]

Thank you, that is a very insightful observation and using the inner integrals should certainly reduce the number of definitions. What isn’t clear to me yet is why it would suffice to work with ENNReal, I would think that the definition of weak convergence in the book considers all bounded continuous functions, right? So these might be negative?

[Josha Dekker]

I'll need to think if this is something I should pursue at this point though, I think that studying the material AND putting it in Mathlib in a rather different way might become a bit confusing to me; perhaps it is better that I revisit formalising it in lean after I've worked through the book.

[Sébastien Gouëzel]

It's probably a good idea to wait until you're very familiar with the material, to be able to weigh the different design choices knowing how they could interfere with applications. In general, I agree that learning and formalizing at the same time is a little bit dangerous.

[Josha Dekker]

Yes, I agree! I'll stick to formalising more familiar stuff for a while then. Thank you for your support!