Commit 2021-09-11 15:52 62de5912

feat(interval_integral): generalize change of variables (#8869)

• Generalizes interval_integral.integral_comp_mul_deriv'. In this version: (1) f need not be differentiable at the endpoints of [a,b], only continuous, (2) I removed the measurable_at_filter assumption (3) I assumed that g was continuous on f '' [a,b], instead of continuous at every point of f '' [a,b] (which differs in the endpoints). This was possible after @sgouezel's PR #7978. The proof was a lot longer/messier than expected. Under these assumptions we have to be careful to sometimes take one-sided derivatives. For example, we cannot take the 2-sided derivative of λ u, ∫ x in f a..u, g x when u is the maximum/minimum of f on [a, b]. @urkud: I needed more FTC_filter classes, namely for closed intervals (to be precise: FTC_filter x (𝓝[[a, b]] x) (𝓝[[a, b]] x)). Was there a conscious reason to exclude these classes? (The documentation explicitly enumerates the existing instances.)