-
Notifications
You must be signed in to change notification settings - Fork 82
Description
Addition of Cauchy sequences in the reals is cool and all, but we can be more general. There's nothing special about addition as an operation that takes two Cauchy sequences to a Cauchy sequence; any continuous function on the product of two metric spaces to another metric space will do; the continuity of addition suffices.
But to define that, we need the product of two metric spaces to be another metric space, and that brings us to https://en.wikipedia.org/wiki/Lp_space , which Wikipedia also calls Lebesgue spaces. Any of the Lp norms would do here, I think?
How to approach it is a little ambiguous, which is why I'm bothering to file an issue at all. First, we're defining metric spaces in terms of rational bounds, not real number distances. Second, the L_\infty norm is popular and straightforward to use, but infinity is of course not a rational or real number. Third, the L_p norm is defined for any rational or even real number, but we don't have fractional powers yet.
So there's a lot of ambiguity there. I might start off with the L_\infty norm just because it's one that won't generalize in the same way as any of the others later, so we don't have to worry about generalizing it immediately. But it seems worth thinking about.