Banach fixed point theorem

[zstone1]

Motivation for this change

A generally useful result that doesn't require any machinery beyond geometric series. The proof is not too long, thankfully.

1. There is some nasty geometric series arithmetic. A large block of arithmetic rewrites appears in several proofs.
2. Lots of proofs of positivity are required. Having signed.v is a massive help, although it was a bit difficult to work with at first. I have a lot of terms like (1 - q) and (1-q^+n), and a q<1 in scope. But, by default, the canonical instance tried to prove 0 < 1-q via 0 < 1 + -q, which was bad news. I needed to refactor things so 1-q get rewritten as PosNum(... : 0 < 1-q). This seemed to do the trick. Once I figured this out things worked much better.
3. This should be possible to do on hausdorff pseudoMetric spaces. However, because we define things with ball, it's difficult to get a metric out. I have a suspicious it's not possible in general if the definition of ball is pathological. The proof doesn't use any interesting properties of norms, so will be easy to generalize if pseudoMetrics are ever fixed.
4. In order to make things work for subspaces, I need to introduce a set U as the domain of f. Our existing definition of subspace topology includes points outside the "good subset". This interferes with the definition of contraction.

Note that I'm taking a set U as an argument, so the indexing trick (that filter_from) uses could apply here. However, the type X appears in both covariant and contravariant positions. Is there some value in doing it that way?

There are probably some simplifications, and some cleanup. There's also some docs and changelogs to write.

• 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.

[zstone1]

On further reflection, something is wrong with the current previous formulation. Most applications of this theorem carve out a subset U of X, which is invariant under f, and where it's a contraction. This won't work work for us, (even if we used pseudoMetrc instead of normed) without making the domain a the dependent pair subtype. Using our definition of subspace won't work, because it includes all the extra points, and f won't be a contraction. We could introduce a set into the definition of contraction, but I wish there were a way to define things to make subspace work.

Edit: Thankfully functions.v lets me write f : {fun U >-> U}. Is this the cleanest way to get what I want? We will probably want a proof that if U is a subset of X, U is closed, and X is complete, then so is {subspace U} when working with subspaces anyway.

[affeldt-aist]

In another setting, we've been discussing with @proux01 a way to introduce a type for real numbers r between 0 and 1 so that 1 - r can be ruled out automatically as non-negative. It would help here too, wouldn't it?

[zstone1]

Yes, support for a "between 0 and 1" real would definitely simplify things for this proof. There are some details regarding strictness of the inequalities. I defined contractions here as 0 <= q < 1. But the 0 = q case is rather degenerate: it's a constant function (which of course has a unique fixed point). Redefining things to be 0 < q < 1 would lose almost nothing. However, the strictness of q < 1 is critical (translations have no fixed points in R, and have q=1). The machinery in signed.v is precise enough to handle the strictness, so as long as you're reusing that, it should work out well.

[affeldt-aist]

I think that in other situations similar needs to work with 1 - q and 1- q ^ n expressions will occur (we have been using such expressions a lot with probabilities and convexity) so I have been trying to come up with a way to make your mechanism to take advantage of signed.v available from outside of the section. What do you think about this commit affeldt-aist@3b08c0e ? It introduces a definition and a small theory for 1 - q expressions so that automation can be made available in (imho) a bit more principled way. (Though obviously this cannot be a definitive solution.)

[zstone1]

It's definitely an improvement. Factoring out the reusable bits from that giant algebra rewrite block is great. This look like a good halfway to building some canonical automation. I have a two thoughts:

1. Is onemN necessary? It seems to break the abstraction by producing an actually negative number. I also see you end up using it in the proofs. As far as submitting this improvement, it's not a blocker. But it does seem like a point where the automation is likely to hit a dead end.
2. The r.~ notation surprised me at first. It's not what I would have expected in this context. But the more I think about that's likely because I'm missing some deeper connection between this result and something in probability theory. I'm now quite curious to see where this line of inquiry will take us.

[affeldt-aist]

1. Is `onemN` necessary? It seems to break the abstraction by producing an actually negative number. I also see you end up using it in the proofs. As far as submitting this improvement, it's not a blocker. But it does seem like a point where the automation is likely to hit a dead end.

I tried to do without onemN: affeldt-aist@63f6eca

2. The `r.~` notation surprised me at first. It's not what I would have expected in this context. But the more I think about that's likely because I'm missing some deeper connection between this result and something in probability theory. I'm now quite curious to see where this line of inquiry will take us.

(I changed the notation to 1.-r.)
This comes from paper like e.g. https://arxiv.org/pdf/0903.5522.pdf where in section 2 the author use \bar{r} notations and a bit of theory that we found useful when doing formalization with no automation in other work.

[proux01]

I once took inspiration of signed.v to infer intervals: 3b2bcc1 This could probably extend signed.v to the use case needed here (without even needing any specific notation for 1 - x). This requires a bit more work (in particular to see whether it can replace signed.v or has to live beside it and how) that I probably won't be able to do before next month. Meanwhile the current situation here is probably fine and this shouldn't block merging this PR.

[zstone1]

Yeah, this looks good. That theory should probably move elsewhere, but otherwise I'm quite happy to see this improvement.

[affeldt-aist]

This looks ok to me in the current state of affairs.