Topology on Lp

Stream: mathlib4

[Yury G. Kudryashov]

In #6839, I define a UniformSpace structure on docs#MeasureTheory.Lp for all p. The goal is to port lemmas from ∀ ε > 0, ∃ f, P f ∧ snorm (f - g) < ε to Dense {f : Lp E p μ | P f}, though I postpone this to a later PR.

[Yury G. Kudryashov]

Since Lp does not satisfy the triangle inequality for 0 < p < 1, I had to repeat some lemmas for Lp.

[Yury G. Kudryashov]

I didn't add more typeclasses because we don't have more examples.

[Antoine Chambert-Loir]

Mathlib doesn't know about this weaker version of metric spaces where d(x,y) <= c (d(x,z)+ d(y,z)) for some constant c ?

[Jireh Loreaux]

Correct. We don't currently have a type class for that. However, in various places, including Lp, we have designed things in such a way that it should be possible to easily make instances of this type class once it's defined.

[Filippo A. E. Nuccio]

With @Heather Macbeth we made some progress in that direction in https://github.com/leanprover-community/mathlib/tree/lp_p_le_one but this has never been pushed to mathlib (and never translated into Lean4).

[Yury G. Kudryashov]

I'm going to add typeclasses for that. How should I call it?

[Jireh Loreaux]

The terminology I'm familiar with is quasi-metric and quasi-norm. I think the latter is unambiguous, but the former I think may have other meanings.

[Jireh Loreaux]

Indeed, Wikipedia seems to agree with my assessment. I would vote for "quasi" in both settings for consistency.

[Yury G. Kudryashov]

Should it be PseudoQuasiEMetricSpace or QuasiPseudoEMetricSpace?

[Anatole Dedecker]

Wouldn't it be more useful to give up on homogeneity but keep subadditivity? If we use $\Vert f\Vert_p = \int \vert f\vert^p$ for $p < 1$ we still have a metric structure right?

[Yury G. Kudryashov]

Either way works for me...

[Yury G. Kudryashov]

@Sebastien Gouezel @Jireh Loreaux What do you think?

[Sebastien Gouezel]

I don't have a well-informed opinion here. The book on F-spaces that Filippo pointed to uses the homogeneous norm, but also the distance which satisfies the triangular inequality (which is not given directly by the norm, but rather a power of it). It proves that given any quasi-distance, there exists a true distance defining the same topology.

[Yury G. Kudryashov]

My only goal is to reformulate our "dense" lemmas in terms of docs#Dense in Lp.

[Kevin Buzzard]

p-Banach spaces (usual axioms for Banach space except for $||\lambda v||=|\lambda|^p||v||$ ) are all over the liquid Tensor experiment.

[Yury G. Kudryashov]

So, should I change the definition of snorm?

[Jireh Loreaux]

Yeah, I'm not sure which is preferable.

[Yury G. Kudryashov]

For me, it's easier to change snorm and reuse NormedAddCommGroup than to add QuasiMetricSpaces etc. So, unless someone tells me that QuasiMetricSpaces are a much better approach to $L^p$, $0<p<1$, then I'll change snorm.

[Adam Topaz]

FWIW, here's LTE's $\ell^p$ as a $p$-Banach space:
https://github.com/leanprover-community/lean-liquid/blob/master/src/pBanach/lp.lean

I haven't followed the discussion above, but just wanted to mention it, in case it's helpful at all.

[Yury G. Kudryashov]

But it's a p-Banach space for all p.

[Yury G. Kudryashov]

Not only for p < 1.

[Yury G. Kudryashov]

I mean, in that file.

[Yury G. Kudryashov]

BTW, is it a metric for p > 1?

[Adam Topaz]

https://github.com/leanprover-community/lean-liquid/blob/92f188bd17f34dbfefc92a83069577f708851aec/src/pBanach/lp.lean#L39

[Adam Topaz]

Looks like we used docs3#nnreal.rpow_add_le_add_rpow for the triangle inequality

[Yury G. Kudryashov]

So, I'll use that formula for 0 < p < 1 and the usual formula for 1 ≤ p.

[Antoine Chambert-Loir]

I am not sure all the intermediate categories (where various restrictions are made regarding the “distance”) are really worthy of introduction. However, a general lemma which can be found in Bourbaki (General Topology, chapter 9, §1) describes the functions $d \colon X \times X \to [0;+\infty]$ such that the preimages of the intervals $[0;a]$, for $a >0$, generate a fundamental systems of entourages of a uniform structure. My feeling is that this lemma could be introduced, together with a name for these functions as well as a process of creation of the according uniform structure.

[Antoine Chambert-Loir]

image.png
(The exercise, in French… )

[Antoine Chambert-Loir]

and in English
image.png

[Anatole Dedecker]

We have docs#UniformSpace.ofFun, but not much API for it

[Anatole Dedecker]

Oh and it’s still too strong

[Filippo A. E. Nuccio]

Yury G. Kudryashov said:

So, I'll use that formula for 0 < p < 1 and the usual formula for 1 ≤ p.

This was the approach that we took with Heather.

[Filippo A. E. Nuccio]

Yury G. Kudryashov said:

Should it be PseudoQuasiEMetricSpace or QuasiPseudoEMetricSpace?

I have also seen the comment

Registering this separately allows for a future emetric-like structure on `PiLp p β` for `p < 1`
satisfying a relaxed triangle inequality. The terminology for this varies throughout the
literature, but it is sometimes called a *quasi-metric* or *semi-metric*. -/

on line 127 of Mathlib/Analysis/NormedSpace/PiLp.lean

[Yury G. Kudryashov]

I'm going to finally implement this change (redefine norm on Lp for p < 1). I have one last question: for p = 0, the formula for p < 1 gives the measure of the indicator. Does it make sense to redefine Lp 0 norm this way (currently it's just zero)?

[Yury G. Kudryashov]

I mean, it gives more information about f than just constant zero, so unless it breaks some useful statement, I'm going to do it.

[Jireh Loreaux]

Yes, I would do that. It would match PiLp and lp that way.

[Yury G. Kudryashov]

UPD: no, the formula gives μ univ. I'll need to override for p = 0.