monotonous and derivative

[affeldt-aist]

Motivation for this change

This PR contains a proof that "decreasing implies non-positive derivative".
@t6s If I remember correctly, you proved similar lemmas somewhere.
Are they in some pending PRs or do you have them elsewhere?
(By the way, the lemmas in this PR are used to prove integration-by-substitution like lemmas.)

@IshiguroYoshihiro you may want to amend this PR.

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

[t6s]

Yes, I have a local branch for a similar PR, though not ready yet.

I'm happy to have this PR going first, so that I can generalize the lemmas as needed.

[affeldt-aist]

Ah, I remember now. We were actually discussing generalizations of the lemmas that establish monotonicity from the sign of the derivative, as the two lemmas in this commit 2b63e89
(the lemmas in the previous commit are doing the contrary).
I think that you had other variants of the lemmas in the second commit.

Ideally, we want to factorize all of the them as a few generic lemmas exploiting the Interval type.

[affeldt-aist]

@t6s : @IshiguroYoshihiro has added variants so that this PR might actually cover what you were working on afaiu

[t6s]

Looks good. Could you quickly add closureT and closure0?

Future TODOs:

• generalize interior_set1 (to metric spaces (=pseudometric + hausdorff)?)
• split normedtype.v into generic and real-specific files
• add closure_itv_{bnd, bndy, Nybnd, Nyy}

[t6s]

affeldt-aist#24
added closureT

[affeldt-aist]

I'll merge when the CI is green, since these lemmas are much needed in other PRs and in infotheo.