feat(measurable_space): is_measurable_supr lemma

[semorrison]

(Builds on #2091)

Three lemmas describing is_measurable on various suprema of measurable spaces. All are written in terms of the inductive predicate generate_measurable, which may be morally wrong.

If someone who loves galois connections more than I do wants to tell me that wanting these lemmas is surely a sign that I'm doing it wrong, I'm happy to learn. :-)

But for now it's hard to get access to this information.

[sgouezel]

I don't know really well this part of the library (in general, I use a fixed measurable structure). These lemmas seem perfectly reasonable and useful, but I am not convinced they should be simp lemmas. Do you have a specific application in mind?

[semorrison]

I wanted these because I was thinking about proving a theorem of Kolmogorov on the way to constructing the Wiener process.

If you have a measure on a function space X -> Y, you can look at its "finite dimensional distributions", i.e. the induced measures on F -> Y for each F : finset X. The theorem I have in mind says that a set of "consistent finite dimensional distributions" (i.e. a measure for every such F, appropriately compatible with inclusions of finsets) always comes from an actual measure on the function space.

A key step of the proof is that the measurable structure on a function space is the one generated by the evaluation maps at points of x, and so in particular the cylinder sets generate the measurable sets. So I needed to be able to describe that generated measurable structure, and this is what these lemmas do.

[semorrison]

I agree, nevertheless, that they needn't be simp lemmas, at least for now. I'll fix that.

[sgouezel]

The Kolmogorov extension theorem is definitely a worthy goal. I am not sure it is the best way to construct the Wiener measure, though, as it gives a measure which is not supported on continuous functions while there is a version of the Wiener measure which is (and for which one can use the sigma-algebra coming from the topology of locally uniform convergence).