[WIP] feat(analysis/topology/banach_contraction) #428
Conversation
|
That PR needs to be reworked to use 4a013fb Compare https://github.com/leanprover/mathlib/pull/428/files#diff-6f3fee1c28d757f0199c3512ffc8e5e9R83 and 4a013fb#diff-5edb379056f11c116887dcff6e8bed0dR366 for instance |
|
I have forked rmitta:Banach with an eye to updating this PR to reflect recent changes in mathlib. But now of course it doesn't compile. I think we want to rebase the branch? https://git-scm.com/book/en/v2/Git-Branching-Rebasing |
|
Indeed this needs rebasing first |
|
Thanks for the feedback both, I've not had time for Lean for a while but I'm back on it now, should have an updated version of this in the next few days. |
|
That's great 😄. Looking back at my contribution I should mention I am using Lipschitz continuous in the Wikipedia sense rather than in the Sutherland sense (which appears to correspond to Hölder continuous on Wikipedia). |
|
I've pushed a new version of this that should compile with the latest version of mathlib and keeps the contribution by agjftucker. I had to unfortunately do some of this (the bit that I think was equivalent to rebasing) manually, but it should all work now, so I think we are good to go! @agjftucker I didn't quite see what you were trying to say about |
| open nat | ||
| def iteration_map {α : Type*} (f : α → α) (start : α) : ℕ → α | ||
| | zero := start | ||
| | (succ x) := f (iteration_map x) |
|
|
||
| --Definition 17.24 | ||
| def is_contraction {α : Type*} [metric_space α] (f : α → α) := | ||
| ∃ (k : ℝ) (H1 : k < 1) (H2 : 0 < k), ∀ (x y : α), dist (f x) (f y) ≤ k* (dist x y) |
There was a problem hiding this comment.
maybe put some more space in, I was wondering what the k* function is
There was a problem hiding this comment.
I'm not sure this is yet ready to review. Between Rohan Mitta and myself we have a lot of redundancy. There is a completely parallel proof of the main theorem here https://github.com/agjftucker/mathlib/blob/Banach/analysis/topology/banach_contraction.lean
There was a problem hiding this comment.
I should have said: it would be great to have your feedback :)
There was a problem hiding this comment.
ok, remove the [WIP] when ready
digama0
changed the title
|
closed with #553 |
I think I've done all of this, the one thing I'm not sure about is whether the lemma complete_iff_seq_complete in metric_sequences is redundant.
TO CONTRIBUTORS:
Make sure you have:
For reviewers: code review check list