agda-unimath
agda-unimath copied to clipboard
UniMath
Lebesgue spaces
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.
Sorry, stupid question, but won't it suffice to define binary continuous maps on metric spaces instead of product metrics? Also, we already have dependent product metrics, of which binary products is a special case.
I think the dependent product metric is equivalent to the L^infinity metric, which will probably be good enough for now.
won't it suffice to define binary continuous maps on metric spaces instead of product metrics?
It seems to me the most reasonable, general definition of a binary continuous map is in terms of the product metric?
It seems to me the most reasonable, general definition of a binary continuous map is in terms of the product metric?
It is often practical to consider binary maps of type A -> B -> C, but this sort of depends on whether the category of metric spaces and continuous maps satisfies good categorical properties. As demonstrated, there is not a unique/canonical metric on the product of two metric spaces, so you might be right.