Folders in `MeasureTheory/`

Stream: mathlib4

[Yury G. Kudryashov]

Motivated by @Rémy Degenne 's comment in #16205. How do folders in MeasureTheory/ work? Should MeasurableSpace/ contain everything about σ-algebras? If yes, then we should move more stuff (e.g., parts of Constructions/Borel) there. If no, then where's the line between "goes to MeasurableSpace/" and "goes to Constructions/, Function/ etc"?

[Yaël Dillies]

I personally don't understand the current folder system at all. Eg we have MeasurableSpace.Defs but also MeasureSpaceDef, and the latter contains very little about MeasureSpace as it's instead about Measure

[Rémy Degenne]

MeasureSpaceDef is the result of an old split (before we decided to have .Defs or .Basic files) of MeasureSpace (which has always been more about Measure) into two files: one that contained only basic facts and was imported by the measurability tactic, and another one that could use that tactic.
The tactic changed a lot and that split might not even be useful anymore. I agree that the file name is strange in any case.

[Rémy Degenne]

My understanding of the MeasurableSpace folder was that it was supposed to contain only properties of the spaces, not of functions defined on them (those go to the folder Function). The scope of Constructions is a bit unclear to me as well.

[Yury G. Kudryashov]

I suggest that we clearly split theory about σ-algebras from theory about measures.

[Yury G. Kudryashov]

Rémy Degenne said:

MeasureSpace (which has always been more about Measure)

Before !3#3373 many parts of the library (e.g., integrals) assumed [measure_space _] instead of [measurable_space α] (μ : measure α) and assumed that the only interesting measure is volume.

[Yury G. Kudryashov]

Rémy Degenne said:

My understanding of the MeasurableSpace folder was that it was supposed to contain only properties of the spaces, not of functions defined on them (those go to the folder Function). The scope of Constructions is a bit unclear to me as well.

docs#Measurable is defined in MeasurableSpace/Defs and measurability of functions like Prod.fst is proved in MeasurableSpace/Basic.

[Rémy Degenne]

Well yes, those lemmas are in there, but I'd say more for historical reasons than anything else. When someone (Floris?) changed MeasureTheory from one folder with many files and zero sub-folders to something more organized, the MeasurableSpace folder did not exist and the reorganization left the file MeasurableSpace.lean (or perhaps it was already two files) outside of any sub-folder, with many basic definitions for measure theory. Then more recently someone created a MeasurableSpace folder and the content of the MeasurableSpace file(s) ended up in there.

Anyway, my point is that the different folders we have are not the result of one phase of design with clear specification for the contents of each folder, but the result of several successive moves as the library grew, each of which mostly kept together the lemmas that happened to be in the same file. Thus I also don't want to claim that I know clearly what should go where. That's why my comment on your PR was that ultimately you could choose what you thought was best.

If someone wants to spend time reorganizing everything in MeasureTheory with a clear scope for each sub-folder, that would be nice (but that's a lot of work).

[Yury G. Kudryashov]

I can start reorganizing, but we need to agree on the goal first. I suggest that we separate theory about [MeasurableSpace α] from theory about [MeasurableSpace α] {μ : Meausre α}, because the latter usually needs more dependencies.

[Rémy Degenne]

That sounds like a good first split.

[Yury G. Kudryashov]

Then I'll merge the PR as is, then start moving stuff that doesn't depend on Measure to MeasurableSpace/.