[Merged by Bors] - feat(measure_theory/*): refactor integral to allow non second-countable target space

[sgouezel]

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.

---

• depends on: [Merged by Bors] - feat(topology/metric_space/metrizable): define and use a metrizable typeclass #12934
• depends on: [Merged by Bors] - feat(topology/constructions): continuity of uncurried functions when the first factor is discrete #12935
• depends on: [Merged by Bors] - feat(topology/bases): separable subsets of topological spaces #12936
• depends on: [Merged by Bors] - chore(nnreal): rename lemmas based on real.to_nnreal when they mention of_real #12937
• depends on: [Merged by Bors] - chore(measure_theory/measure/lebesgue): delete leftovers #12951
• depends on: [Merged by Bors] - chore(order/filter/basic): rename using the zero subscript convention for groups with zero #12952
• depends on: [Merged by Bors] - chore(measure_theory/integral/lebesgue): extend to ae_measurable #12953
• depends on: [Merged by Bors] - feat(measure_theory/constructions/borel_space): drop a countability assumption #12954
• depends on: [Merged by Bors] - feat(measure_theory/functions/strongly_measurable): almost everywhere strongly measurable functions #12985

[leanprover-community-bot-assistant]

This PR/issue depends on:

• [Merged by Bors] - feat(topology/metric_space/metrizable): define and use a metrizable typeclass #12934
• [Merged by Bors] - feat(topology/constructions): continuity of uncurried functions when the first factor is discrete #12935
• [Merged by Bors] - feat(topology/bases): separable subsets of topological spaces #12936
• [Merged by Bors] - chore(nnreal): rename lemmas based on real.to_nnreal when they mention of_real #12937
• [Merged by Bors] - chore(measure_theory/measure/lebesgue): delete leftovers #12951
• [Merged by Bors] - chore(order/filter/basic): rename using the zero subscript convention for groups with zero #12952
• [Merged by Bors] - chore(measure_theory/integral/lebesgue): extend to ae_measurable #12953
• [Merged by Bors] - feat(measure_theory/constructions/borel_space): drop a countability assumption #12954
• [Merged by Bors] - feat(measure_theory/functions/strongly_measurable): almost everywhere strongly measurable functions #12985
  By Dependent Issues (🤖). Happy coding!

[urkud]

Thanks!!
bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests