mathlib
mathlib copied to clipboard
leanprover-community
feat(topology,analysis): add the discrete metric and normed spaces
These are provided as definitions for now, but in future might be reasonable to associate with a type synonym.
- [x] depends on: #13927
- [x] depends on: #14638
This PR/issue depends on:
- ~~leanprover-community/mathlib#13927~~
- ~~leanprover-community/mathlib#14638~~ By Dependent Issues (🤖). Happy coding!
I will freely admit I don't entirely understand the bornology stuff or why it's necessary.
Bearing that in mind:
This is good I think, but ultimately I do not think this definition of a constant metric is a good definition of the discrete metric. It's very usual to define d(x, y) = 1 when x /= y, and this is I think the approach we should take. In some sense, it might be worth mirroring what I've done over at https://github.com/leanprover-community/mathlib/pull/14739 (or I adopt something like your approach), because the Hamming metric and the discrete metric are obviously related.
Having a type synonym would make this a lot more usable in practice.
Thanks for the reminder about this PR, I've resolved the conflicts.
I will freely admit I don't entirely understand the bornology stuff or why it's necessary.
It's there just so that the implied bornology is defeq to the discrete bornology, I don't understand the mathematics either, but it looks like how the API was intended to be used
This is good I think, but ultimately I do not think this definition of a constant metric is a good definition of the discrete metric. It's very usual to define d(x, y) = 1 when x /= y, and this is I think the approach we should take.
My thinking was that d(x,y) = 1 falls out as a special case of d(x, y) = c. Since all the proofs still work, I figured I may as well prove the more general case.
Would you be happier if I renamed discrete to const?
In some sense, it might be worth mirroring what I've done over at #14739 (or I adopt something like your approach), because the Hamming metric and the discrete metric are obviously related.
I assume this is regarding the use of a synonym?
Having a type synonym would make this a lot more usable in practice.
I agree, but I didn't want to let this PR get too big. As it currently is, a user can put these instances on their own type manually using the definitions that are present. Replacing the metric space of an existing type feels like a job for a follow-up.
I'd be happy if you renamed discrete to const. It's also probably true that there is more to be said about discreteness - for instance, a metric can be discrete without being uniformly discrete (and your const is a special case of uniform discreteness). "The discrete metric" is different from "a discrete metric" in common parlance, I think.
I believe often you can just ignore the bornology stuff and it Just Works (TM)? That's certainly what I did in my Hamming work.
With regards to "what I did there" - I was actually thinking that once again with the particular case of the discrete metric you have an integer-valued metric. Though in this case it doesn't really count anything so it's probably fine to leave it directly as a real.
The significant thing about the value 1 is that it lets you define a normed_field instance, which I note you don't seem to here. For a normed field, you need ∥a * b∥ = ∥a∥ * ∥b∥, and the constant metric doesn't obey this. This is different than normed_ring, where ∥a * b∥ ≤ ∥a∥ * ∥b∥ is all that is required, and thus (as you have) you just need 1 ≤ c.
Someone explained to me why normed_field works differently but I can't remember what their reasoning was and I don't think I was really convinced. This is an illustration of why the difference matters. (Some literature distinguishes between normed fields, where ≤ is what you need, and valued fields, with =. For 1 < c, const c gives a normed field but not a valued field, in this language.)
While I agree we should avoid the PR getting too big, I think it would be good to plan for the future. I've expressed before that I'm not sure something is quite right about the norm-valuation-algebrahierarchy picture, and this touches on that. We should be careful of adding more stuff that a future refactor would have to do busywork to fix.
Why do you want normed_field anyway? Well, it's all in aid of trying to reach normed_space, which currently (for, again, mysterious reasons) requires it. The particular kind of normed_space where the field norm is discrete corresponds to "scalar multiplication can only decrease the norm".
What I'm trying to say I think is that it feels like there's sticky jam everywhere and we should avoid rolling in it lest the wasps descend. Proceed with caution. Good job on the conflict fixing though!
I'd be happy if you renamed discrete to const.
Done
I believe often you can just ignore the bornology stuff and it Just Works (TM)? That's certainly what I did in my Hamming work.
Think of it as dotting the i's and crossing the t's. It probably doesn't make much difference, but it's more thorough to do it anyway.
The significant thing about the value 1 is that it lets you define a
normed_fieldinstance, which I note you don't seem to here.
This was an unintentional omission, I've just added it
