change of variables by nondecreasing/nonincreasing function

[IshiguroYoshihiro]

Motivation for this change

add lemmas for integration by substitution with increasing/decreasing function.

some intermediate lemmas are admitted but proved in #1327

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Reference: How to document

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[zstone1]

The joy of boundary condition never ceases. The term F^`() is defined as

Definition derive1 V (f : R -> V) (a : R) := lim ((fun h => h^-1 *: (f (h + a) - f a)) @ 0^').

which is taking the limit near 0 in R. Which means F^`() depends on values outside of [a,b]. That's bad news if you want to consider F\_[a,b]. which will not have a (full) derivative at a.

Several ways to fix this

• The "right" way to fix this is have derive1 consider a under different topologies. Shouldn't be too hard, but it's still kinda invasive. Maybe a ticket for this?
• For a less invasive way, you can introduce another helper function

{within `[a, b], continuous F1} ->
{in `]a.b[, F1 = F^`()}

This forces F^`() to have limits at its endpoints. That is F1 a = lim_(x -->a^+) F`^() x which is what we want.

• We can also do {within ]a.b[, continuous F^()} + cvg (F`^() @ a^+)

I don't have a strong preference on which approach you take. It's not clear to me how much harder this will make the proof...

[IshiguroYoshihiro]

I had thought that {within `[a, b], continuous F^`()} as `` {within [a, b], continuous F1} /\ {in ]a, b[, F1 = F^`()}`, but I hesitate to add a new function in the statement and make less convenient.
So, I think the first solution looks better.
I will try to define right/left derivation

Definition right_derive1 V (f : R -> V) (a : R) :=
   lim ((fun h => h^-1 *: (f (h + a) - f a)) @ 0^'+).
Definition left_derive1 V (f : R -> V) (a : R) :=
   lim ((fun h => h^-1 *: (f (h + a) - f a)) @ 0^'-).

and to change {within `[a, b], continuous F^`()} to
{in `]a, b[, continuous F^`()} and right_derive1 F is right continuous at a and left_derive1 F is left continuous at b.
Thank you for advice!

[zstone1]

Theory wise, I think you'll end up needing to prove something along the lines of F^`() @a^+ --> L -> right_derive1 F a /\ F^`+() a = L anyway (see https://math.stackexchange.com/questions/3301610/proving-differentiability-at-a-point-if-limit-of-derivative-exists-at-that-point). But engineering-wise I'm happy with whatever will lead you to the nicest theorem statement. Good luck!

[IshiguroYoshihiro]

I noticed that the necessary parts of boundary condition of F^`() is that this converged, so I have changed hypothesis to cvg (F^`() @ a^'+/@ b^'-).
This seems easier to use as we don't necessarily have to consider one-sided derivatives.

[zstone1]

Looks much better with the fixed boundary conditions. A couple thoughts on potential improvements to the proofs, but nothing serious. Qed is Qed, after all. So I'm happy with it

[affeldt-aist]

A couple of lemmas to move to more appropriate locations and we should be done.

[affeldt-aist]

Still feels a bit long but at least all comments should be addressed.