L^p distance on finite products of metric spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 | x_i ≠ y_i}$. 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 pi_Lp p α. The assumpion [fact (1 ≤ p)] is required for the metric and normed space instances.

We ensure that the topology, bornology and uniform structure on pi_Lp 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 measure_theory.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 pi_Lp corresponds to the special case of measure_theory.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 pseudo_emetric_space and pseudo_metric_space.

Note that the unapplied versions of these lemmas are deliberately omitted, as they break the use of the type synonym.

Definition of edist, dist and norm on pi_Lp #

In this section we define the edist, dist and norm functions on pi_Lp p α without assuming [fact (1 ≤ p)] or metric properties of the spaces α i. This allows us to provide the rewrite lemmas for each of three cases p = 0, p = ∞ and 0 < p.to_real.

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

In this section, we put the L^p edistance on pi_Lp p α, and we check that the uniformity coming from this edistance coincides with the product uniformity, by showing that the canonical map to the Pi type (with the L^∞ distance) is a uniform embedding, as it is both Lipschitz and antiLipschitz.

We only register this emetric space structure as a temporary instance, as the true instance (to be registered later) will have as uniformity exactly the product uniformity, instead of the one coming from the edistance (which is equal to it, but not defeq). See Note [forgetful inheritance] explaining why having definitionally the right uniformity is often important.

Instances on finite L^p products #