[Merged by Bors] - feat(measure_theory/interval_integral): FTC-2

[benjamindavidson]

The second fundamental theorem of calculus and supporting lemmas

[urkud]

@benjamindavidson I've merged master and fixed some statements. I didn't touch the proofs.

[sgouezel]

The measurability assumptions on f' when you assume that it is continuous on the relevant interval feel really strange. Of course, I understand that it comes from the current implementation in terms of the restricted measure, but it hints that a refactor might be a good idea. Still, this should wait in any case for another PR.

[sgouezel]

Why of_le in the name?

[urkud]

Because this form assumes a ≤ b. Should we move le somewhere else?

[hrmacbeth]

The measurability assumptions on f' when you assume that it is continuous on the relevant interval feel really strange. Of course, I understand that it comes from the current implementation in terms of the restricted measure, but it hints that a refactor might be a good idea.

Yes, I was surprised by this too recently (had to do something similar in #5288).

(EDIT: I see it's for a variant of the lemmas from #5288, so not surprising.)

[benjamindavidson]

@sgouezel Yury will have to answer the other questions/concerns you raised, I'm not sure about them myself.

[urkud]

The measurability assumptions on f' when you assume that it is continuous on the relevant interval feel really strange. Of course, I understand that it comes from the current implementation in terms of the restricted measure, but it hints that a refactor might be a good idea. Still, this should wait in any case for another PR.

This is a side-effect of my choice to use measure.restrict instead of indicator and someone else's choice to use measurable f instead of ∀ s, measurable s → is_null_measurable (f ⁻¹' s). There are a few possible refactors of different scale that would allow us to drop this assumption:

1. Introduce null_measurable_fun and replace most of measurable f with null_measurable_fun f.
2. Use the definition of Bochner integral from Wikipedia. In particular, this definition does not assume that the whole space is separable, and uses weaker measurability assumptions than our definition.
3. Go back to the approach "integral over a set is defined as the integral of the indicator" instead of "integral w.r.t. the restriction of the measure".

[sgouezel]

Does it seem reasonable to try to replace the measurable f assumption in integrable f with the existence of a measurable g which coincides almost everywhere with f? I may give it a try if you think it might be a good move. (This is a version of null_measurable_fun f, but for which the refactor doesn't seem to be too big).

[sgouezel]

Let's merge this. I'll adjust #5510 accordingly afterwards.
bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

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