`L^p` distance on finite products of metric spaces #

Given finitely many metric spaces, one can put the max distance on their product, but there is also a whole family of natural distances, indexed by a parameter p : ℝ≥0∞, that also induce the product topology. We define them in this file. For 0 < p < ∞, the distance on Π i, α i is given by $$ d(x, y) = \left(\sum d(x_i, y_i)^p\right)^{1/p}. $$, whereas for p = 0 it is the cardinality of the set ${i | d (x_i, y_i) ≠ 0}$. For p = ∞ the distance is the supremum of the distances.

We give instances of this construction for emetric spaces, metric spaces, normed groups and normed spaces.

To avoid conflicting instances, all these are defined on a copy of the original Π-type, named PiLp p α. The assumption [Fact (1 ≤ p)] is required for the metric and normed space instances.

We ensure that the topology, bornology and uniform structure on PiLp p α are (defeq to) the product topology, product bornology and product uniformity, to be able to use freely continuity statements for the coordinate functions, for instance.

Implementation notes #

We only deal with the L^p distance on a product of finitely many metric spaces, which may be distinct. A closely related construction is lp, the L^p norm on a product of (possibly infinitely many) normed spaces, where the norm is $$ \left(\sum ‖f (x)‖^p \right)^{1/p}. $$ However, the topology induced by this construction is not the product topology, and some functions have infinite L^p norm. These subtleties are not present in the case of finitely many metric spaces, hence it is worth devoting a file to this specific case which is particularly well behaved.

Another related construction is MeasureTheory.Lp, the L^p norm on the space of functions from a measure space to a normed space, where the norm is $$ \left(\int ‖f (x)‖^p dμ\right)^{1/p}. $$ This has all the same subtleties as lp, and the further subtlety that this only defines a seminorm (as almost everywhere zero functions have zero L^p norm). The construction PiLp corresponds to the special case of MeasureTheory.Lp in which the basis is a finite space equipped with the counting measure.

To prove that the topology (and the uniform structure) on a finite product with the L^p distance are the same as those coming from the L^∞ distance, we could argue that the L^p and L^∞ norms are equivalent on ℝ^n for abstract (norm equivalence) reasons. Instead, we give a more explicit (easy) proof which provides a comparison between these two norms with explicit constants.

We also set up the theory for PseudoEMetricSpace and PseudoMetricSpace.

L^p distance on finite products of metric spaces #

Implementation notes #

Definition of edist, dist and norm on PiLp #

The uniformity on finite L^p products is the product uniformity #

Instances on finite L^p products #

`L^p` distance on finite products of metric spaces #

Definition of `edist`, `dist` and `norm` on `PiLp` #

The uniformity on finite `L^p` products is the product uniformity #

Instances on finite `L^p` products #