[Merged by Bors] - feat(measure_theory/interval_integral): more versions of FTC-1

[urkud]

Left/right derivative, strict derivative, differentiability in both endpoints.

Other changes:

• rename filter.tendsto_le_left and filter.tendsto_le_right to filter.tendsto.mono_left and filter.tendsto.mono_right, swap arguments;
• rename order_top.tendsto_at_top to order_top.tendsto_at_top_nhds;
• introduce tendsto_Ixx_class instead of is_interval_generated.

---

Some lemmas assume (l : filter α) [is_interval_generated l] (_ : pure b ≤ l) (l ≤ 𝓝 b).
This is a fancy way to say “l is one of pure b, 𝓝[Iic b] b, 𝓝[Ici b] b, 𝓝 b”
in order to prove a lemma for the three non-trivial cases simultaneously.

[urkud]

While adding docs I found some holes in API. I'll work on this tonight or tomorrow.

[bryangingechen]

Some lemmas assume (l : filter α) [is_interval_generated l] (_ : pure b ≤ l) (l ≤ 𝓝 b).
This is a fancy way to say “l is one of pure b, 𝓝[Iic b] b, 𝓝[Ici b] b, 𝓝 b”
in order to prove a lemma for the three non-trivial cases simultaneously.

Should this be mentioned in a module doc string?

[sgouezel]

This is very nice: the formulations of the different versions of the FTC are really neat, and you have been able to factor out the proof part very efficiently. Thanks!

[sgouezel]

Could you add comments on the different versions of the FTC you prove, in the file-level docstring?

[urkud]

While working on the docs I've realized that I have no has_strict_fderiv_at for ∫ x in a..b, f x ∂μ as a function of both a and b. tl;dr: I refactored FTC again (almost done, will finish tomorrow).

[urkud]

I rewrote large parts of this PR to add differentiability in both endpoints.

[sgouezel]

Thanks! In addition to minor comments, my main concern is that the file-level docstring could (should?) be exanded a lot, both in the statements section (can you explain what you prove, maybe not all versions but at least one or two relevant versions), and also in the implementation section (comment on the specific type classes you introduce, and how they are used and how they make it possible to avoid proof duplication).

[urkud]

@sgouezel I tried to address all your comments.

[sgouezel]

bors r+

Thanks!

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Run tests