fine lemmas

[zstone1]

Motivation for this change

A super useful lemma is that integrals and derivatives exchange. That is,

d (int (f x y) dx) / dy = int (d (f x y) /dy) dx)

This comes up in applications like

1. Partials derivatives commute
2. Homotopy invariance of path integrals
3. Computing derivatives of certain integral operators, E.G. fourier transform

However, the derive infrastructure works on T -> R but integration works on T -> \bar R. We need to do a lot of work to make them compatible without duplicating the whole theory. To that end, I'm adding a bunch of helper lemmas about fine and integrable that'll help smooth out the process.

Things done/to do

• added corresponding entries in CHANGELOG_UNRELEASED.md
  (do not edit former entries, only append new ones, be careful:
  merge and rebase have a tendency to mess up CHANGELOG_UNRELEASED.md)
• added corresponding documentation in the headers

Automatic note to reviewers

Read this Checklist and put a milestone if possible.

[affeldt-aist]

I shortened using the lemma lte_oppl.

[affeldt-aist]

Maybe squash before merge.