Lp for 0

Stream: Is there code for X?

---

[Vincent Beffara]

Do we have something about the Lp space for exponents between 0 and 1? It would not be a normed_space but could still be a metric_space and that might lift requirements for [fact (1 \le p)] in a few places. Is it possible to have an instance for p < 1 and another for 1 \le p, with very different definitions, or is that looking for trouble with decidability of 1 \le p?

[Filippo A. E. Nuccio]

This is something that shows up in LTE and I was planning to work on putting $\ell^p$ for $0<p<1$ in mathlib at a certain point.

[Sebastien Gouezel]

It wouldn't be a problem to have instances defined differently for p < 1 and 1 \le p. Right now, we have a has_dist instance for all p, and it does not satisfy the triangular inequality for p < 1, so one would have the change the definition. It would probably be a good thing to do, it's just that nobody has invested the time to do it properly for now.

[Yaël Dillies]

One possibility to avoid having an instance for 1 ≤ p and another one for p < 1 is to push the disjunction to the definition of dist. then you can probably prove a few things by casing within the theorems rather than having two separate versions.

[Yaël Dillies]

Surely you rarely unfold the definition anyway, right?

[Filippo A. E. Nuccio]

Well, but there are many theorems which are not true in case p<1, the theories are quite different.

[Filippo A. E. Nuccio]

Sure, the basic API looks similar, but they would rapidly diverge (Open Mapping thm fails in the non-locally convex setting, for instance, and many things depending on it).

[Yaël Dillies]

I'm not saying this buys us much. But it might be nice to have a single metric_space instance, for example.

[Sebastien Gouezel]

Yes, this should definitely be hidden in the definition of has_dist!

[Vincent Beffara]

Ah but if has_dist is non-trivial won't we fall back into the whole non-defeq problem of yesterday? I mean if p<1 then has_dist is a true definition while if 1 \le p it should still be obtained by typeclass inference from normed_group, or am I missing something?

[Filippo A. E. Nuccio]

Probably we should have pseudonormed_group (which are already there, I guess, but with a different meaning)

[Vincent Beffara]

prenormed_group?

[Filippo A. E. Nuccio]

Or quasinormed_group as here ?

[Johan Commelin]

Note that these spaces are p-Banach spaces. Which we have in LTE.

[Filippo A. E. Nuccio]

This is way I was planning to port them to mathlib once LTE will be more advanced.

[Sebastien Gouezel]

Vincent Beffara said:

Ah but if has_dist is non-trivial won't we fall back into the whole non-defeq problem of yesterday? I mean if p<1 then has_dist is a true definition while if 1 \le p it should still be obtained by typeclass inference from normed_group, or am I missing something?

No, in all cases has_dist will be a definition, and then when we define the normed_group structure we just have to make sure that the dist we define in there is definitionally the same as the one we had already defined. Which we can ensure.

[Vincent Beffara]

Oh, I thought naively (without looking at the definition of normde_group) that dist was defined in terms of the norm and that normed_group.dist_eq was a rfl lemma, I should have looked earlier. Nevertheless my fear is something like this:

variables (p : ℝ)

noncomputable def thenorm [fact (1 ≤ p)] (x : ℝ) : ℝ :=
abs x

noncomputable def thenorm' [fact (1 ≤ p)] (x : ℝ) : ℝ :=
ite (1 ≤ p) (abs x) (p * abs x)

noncomputable def thedist (x y : ℝ) : ℝ :=
ite (1 ≤ p) (abs (y - x)) (p * abs (y - x))

example [fact (1 ≤ p)] (x y : ℝ) :
thedist p x y = thenorm p (y - x) :=
begin
  have : 1 ≤ p := by apply fact.out,
  simp [thedist,thenorm,*]
end

example [fact (1 ≤ p)] (x y : ℝ) :
thedist p x y = thenorm' p (y - x) :=
rfl

where thenorm looks natural but is not defeq to thedist when both are defined, and where thenorm' is defeq to thedist whenever they are both defined but thenorm' just looks wrong.