Contraction Definitions

[zstone1]

Motivation for this change

Splitting out another piece of the Banach Fixed Point PR, this just defines contractions and proves a simple fact about them. Note that this places them in normedtype.v next to the lipschitz, which is a much more sensible place to define things.

Things done/to do

• [x] 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)
• [x] added corresponding documentation in the headers

Automatic note to reviewers

Read this Checklist and put a milestone if possible.

[affeldt-aist]

I would be tempted to write:

Definition contraction (q : {nonneg R}) (f : {fun U >-> V}) :=
  ((q%:num < 1) * q%:num.-lipschitz_U f)%type.

so that at least one can rewrite with an hypothesis h : contraction q f to prove q%:num < 1 (i.e., without needing to do a case analysis on h), but I am not sure.

[zstone1]

Interesting. I have not seen this trick before. Although, I can't find an example of it elsewhere in mathcomp analysis. For what it's worth, in the proof I have I need to case on the hypothesis to grab the lipschitz clause anyway.

[affeldt-aist]

For what it's worth, in the proof I have I need to case on the hypothesis to grab the lipschitz clause anyway.

Yes, of course. I believe that there is a better definition but I do not see how to improve it in the current state of affairs. Sorry for delaying merging with unfruitful thinking.