Commit 2022-03-30 02:20 fc758559

feat(measure_theory/*): refactor integral to allow non second-countable target space (#12942) Currently, the Bochner integral in mathlib only allows second-countable target spaces. This is an issue, since many constructions in spectral theory require integrals, and spaces of operators are typically not second-countable. The most general definition of the Bochner integral requires functions that may take values in non second-countable spaces, but which are still pointwise limits of a sequence of simple functions (so-called strongly measurable functions) -- equivalently, they are measurable and with second-countable range. This PR refactors the Bochner integral, working with strongly measurable functions (or rather, almost everywhere strongly measurable functions, i.e., functions which coincide almost everywhere with a strongly measurable function). There are some prerequisistes (topological facts, and a good enough theory of almost everywhere strongly measurable functions) that have been PRed separately, but the remaining part of the change has to be done in one PR, as once one changes the basic definition of the integral one has to change all the files that depend on it. Once the change is done, in many files the fix is just to remove [measurable_space E] [borel_space E] [second_countable_topology E] to make the linter happy, and see that everything still compiles. (Well, sometimes it is also much more painful, of course :-). For end users using integrable, nothing has to be changed, but if you need to prove integrability by hand, instead of checking ae_measurable you need to check ae_strongly_measurable. In second-countable spaces, the two of them are equivalent (and you can use ae_strongly_measurable.ae_measurable and ae_measurable.ae_strongly_measurable to go between the two of them). The main changes are the following:

• change ae_eq_fun to base it on equivalence classes of ae strongly measurable functions
• fix everything that depends on this definition, including lp_space, set_to_L1, the Bochner integral and conditional expectation
• fix everything that depends on these, notably complex analysis (removing second-countability and measurability assumptions all over the place)
• A notion that involves a measurable function taking values in a normed space should probably better be rephrased in terms of strongly_measurable or ae_strongly_measurable. So, change a few definitions like measurable_at_filter (to strongly_measurable_at_filter) or martingale.