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 real parameter p ∈ [1, ∞), that also induce
the product topology. We define them in this file. The distance on Π i, α i is given by
$$
d(x, y) = \left(\sum d(x_i, y_i)^p\right)^{1/p}.
$$
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 Pi type, named
pi_Lp p hp α, where hp : 1 ≤ p. This assumption is included in the definition of the type
to make sure that it is always available to typeclass inference to construct the instances.
We ensure that the topology and uniform structure on pi_Lp p hp α are (defeq to) the product
topology 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 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}.
$$
However, the topology induced by this construction is not the product topology, this only
defines a seminorm (as almost everywhere zero functions have zero L^p norm), and some functions
have infinite L^p norm. All these subtleties are not present in the case of finitely many
metric spaces (which corresponds to the basis which is a finite space with the counting measure),
hence it is worth devoting a file to this specific case which is particularly well behaved.
The general case is not yet formalized in mathlib.
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.
A copy of a Pi type, on which we will put the L^p distance. Since the Pi type itself is
already endowed with the L^∞ distance, we need the type synonym to avoid confusing typeclass
resolution. Also, we let it depend on p, to get a whole family of type on which we can put
different distances, and we provide the assumption hp in the definition, to make it available
to typeclass resolution when it looks for a distance on pi_Lp p hp α.
Equations
- pi_Lp.inhabited p hp α = {default := λ (i : ι), inhabited.default (α i)}
Canonical bijection between pi_Lp p hp α and the original Pi type. We introduce it to be able
to compare the L^p and L^∞ distances through it.
Equations
- pi_Lp.equiv p hp α = equiv.refl (pi_Lp p hp α)
The uniformity on finite L^p products is the product uniformity
In this section, we put the L^p edistance on pi_Lp p hp α, 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.
Endowing the space pi_Lp p hp α with the L^p edistance. This definition is not satisfactory,
as it does not register the fact that the topology and the uniform structure coincide with the
product one. Therefore, we do not register it as an instance. Using this as a temporary emetric
space instance, we will show that the uniform structure is equal (but not defeq) to the product one,
and then register an instance in which we replace the uniform structure by the product one using
this emetric space and emetric_space.replace_uniformity.
Equations
- pi_Lp.emetric_aux p hp α = have pos : 0 < p, from _, {to_has_edist := {edist := λ (f g : pi_Lp p hp α), finset.univ.sum (λ (i : ι), has_edist.edist (f i) (g i) ^ p) ^ (1 / p)}, edist_self := _, eq_of_edist_eq_zero := _, edist_comm := _, edist_triangle := _, to_uniform_space := uniform_space_of_edist (λ (f g : pi_Lp p hp α), finset.univ.sum (λ (i : ι), has_edist.edist (f i) (g i) ^ p) ^ (1 / p)) _ _ _, uniformity_edist := _}
Instances on finite L^p products
Equations
- pi_Lp.uniform_space p hp α = Pi.uniform_space (λ (i : ι), α i)
emetric space instance on the product of finitely many emetric spaces, using the L^p
edistance, and having as uniformity the product uniformity.
Equations
- pi_Lp.emetric_space p hp α = (pi_Lp.emetric_aux p hp α).replace_uniformity _
metric space instance on the product of finitely many metric spaces, using the L^p distance,
and having as uniformity the product uniformity.
Equations
- pi_Lp.metric_space p hp α = emetric_space.to_metric_space_of_dist (λ (f g : pi_Lp p hp α), finset.univ.sum (λ (i : ι), has_dist.dist (f i) (g i) ^ p) ^ (1 / p)) _ _
normed group instance on the product of finitely many normed groups, using the L^p norm.
Equations
- pi_Lp.normed_group p hp α = {to_has_norm := {norm := λ (f : pi_Lp p hp α), finset.univ.sum (λ (i : ι), ∥f i∥ ^ p) ^ (1 / p)}, to_add_comm_group := {add := add_comm_group.add pi.add_comm_group, add_assoc := _, zero := add_comm_group.zero pi.add_comm_group, zero_add := _, add_zero := _, neg := add_comm_group.neg pi.add_comm_group, add_left_neg := _, add_comm := _}, to_metric_space := pi_Lp.metric_space p hp α (λ (i : ι), normed_group.to_metric_space), dist_eq := _}
The product of finitely many normed spaces is a normed space, with the L^p norm.
Equations
- pi_Lp.normed_space p hp α 𝕜 = {to_semimodule := {to_distrib_mul_action := semimodule.to_distrib_mul_action (pi.semimodule ι α 𝕜), add_smul := _, zero_smul := _}, norm_smul_le := _}