mathlib documentation

topology.metric_space.pi_Lp

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.

@[nolint]
def pi_Lp {ι : Type u_1} (p : ) :
1 p(ι → Type u_2)Type (max u_1 u_2)

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 p hp α = Π (i : ι), α i
@[instance]
def pi_Lp.inhabited {ι : Type u_1} (p : ) (hp : 1 p) (α : ι → Type u_2) [Π (i : ι), inhabited (α i)] :
inhabited (pi_Lp p hp α)

Equations
def pi_Lp.equiv {ι : Type u_1} (p : ) (hp : 1 p) (α : ι → Type u_2) :
pi_Lp p hp α Π (i : ι), α 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

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.

def pi_Lp.emetric_aux {ι : Type u_1} (p : ) (hp : 1 p) (α : ι → Type u_2) [Π (i : ι), emetric_space (α i)] [fintype ι] :

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
theorem pi_Lp.lipschitz_with_equiv {ι : Type u_1} (p : ) (hp : 1 p) (α : ι → Type u_2) [Π (i : ι), emetric_space (α i)] [fintype ι] :

theorem pi_Lp.antilipschitz_with_equiv {ι : Type u_1} (p : ) (hp : 1 p) (α : ι → Type u_2) [Π (i : ι), emetric_space (α i)] [fintype ι] :

theorem pi_Lp.aux_uniformity_eq {ι : Type u_1} (p : ) (hp : 1 p) (α : ι → Type u_2) [Π (i : ι), emetric_space (α i)] [fintype ι] :
𝓤 (pi_Lp p hp α) = 𝓤 (Π (i : ι), α i)

Instances on finite L^p products

@[instance]
def pi_Lp.uniform_space {ι : Type u_1} (p : ) (hp : 1 p) (α : ι → Type u_2) [Π (i : ι), uniform_space (α i)] :

Equations
@[instance]
def pi_Lp.emetric_space {ι : Type u_1} (p : ) (hp : 1 p) (α : ι → Type u_2) [fintype ι] [Π (i : ι), emetric_space (α 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
theorem pi_Lp.edist {ι : Type u_1} [fintype ι] {p : } {hp : 1 p} {α : ι → Type u_2} [Π (i : ι), emetric_space (α i)] (x y : pi_Lp p hp α) :
edist x y = (∑ (i : ι), edist (x i) (y i) ^ p) ^ (1 / p)

@[instance]
def pi_Lp.metric_space {ι : Type u_1} (p : ) (hp : 1 p) (α : ι → Type u_2) [fintype ι] [Π (i : ι), metric_space (α i)] :

metric space instance on the product of finitely many metric spaces, using the L^p distance, and having as uniformity the product uniformity.

Equations
theorem pi_Lp.dist {ι : Type u_1} [fintype ι] {p : } {hp : 1 p} {α : ι → Type u_2} [Π (i : ι), metric_space (α i)] (x y : pi_Lp p hp α) :
dist x y = (∑ (i : ι), dist (x i) (y i) ^ p) ^ (1 / p)

@[instance]
def pi_Lp.normed_group {ι : Type u_1} (p : ) (hp : 1 p) (α : ι → Type u_2) [fintype ι] [Π (i : ι), normed_group (α i)] :

normed group instance on the product of finitely many normed groups, using the L^p norm.

Equations
theorem pi_Lp.norm_eq {ι : Type u_1} [fintype ι] {p : } {hp : 1 p} {α : ι → Type u_2} [Π (i : ι), normed_group (α i)] (f : pi_Lp p hp α) :
f = (∑ (i : ι), f i ^ p) ^ (1 / p)

@[instance]
def pi_Lp.normed_space {ι : Type u_1} (p : ) (hp : 1 p) (α : ι → Type u_2) [fintype ι] (𝕜 : Type u_3) [normed_field 𝕜] [Π (i : ι), normed_group (α i)] [Π (i : ι), normed_space 𝕜 (α i)] :
normed_space 𝕜 (pi_Lp p hp α)

The product of finitely many normed spaces is a normed space, with the L^p norm.

Equations
@[simp]
theorem pi_Lp.add_apply {ι : Type u_1} {p : } {hp : 1 p} {α : ι → Type u_2} [fintype ι] [Π (i : ι), normed_group (α i)] (x y : pi_Lp p hp α) (i : ι) :
(x + y) i = x i + y i

@[simp]
theorem pi_Lp.sub_apply {ι : Type u_1} {p : } {hp : 1 p} {α : ι → Type u_2} [fintype ι] [Π (i : ι), normed_group (α i)] (x y : pi_Lp p hp α) (i : ι) :
(x - y) i = x i - y i

@[simp]
theorem pi_Lp.smul_apply {ι : Type u_1} {p : } {hp : 1 p} {α : ι → Type u_2} [fintype ι] {𝕜 : Type u_3} [normed_field 𝕜] [Π (i : ι), normed_group (α i)] [Π (i : ι), normed_space 𝕜 (α i)] (c : 𝕜) (x : pi_Lp p hp α) (i : ι) :
(c x) i = c x i

@[simp]
theorem pi_Lp.neg_apply {ι : Type u_1} {p : } {hp : 1 p} {α : ι → Type u_2} [fintype ι] [Π (i : ι), normed_group (α i)] (x : pi_Lp p hp α) (i : ι) :
(-x) i = -x i