eLpNorm junk value

Stream: mathlib4

[Floris van Doorn]

I think we should redefine docs#eLpNorm to be ∞ when the function is not docs#MeasureTheory.AEStronglyMeasurable.
Currently the value for non-measurable f is "the supremum of ‖g‖_{L^p} for measurable g that a.e. satisfy ‖g‖ ≤ ‖f‖".

The reason for this is twofold:

• I think it's a slightly better junk value. It means that some results can be stated without measurability assumption, e.g. docs#MeasureTheory.eLpNorm_add_le will be true unconditionally. Of course, there will be other results that need an additional assumption, e.g. docs#MeasureTheory.eLpNorm_mono_ae.
• I think it plays a lot better with docs#MeasureTheory.MemLp, which could be redefined as eLpNorm f p μ < ∞ in the new situation. I think it's much nicer if all non-L^p functions have infinite L^p norm.

One thing I'm not sure about is whether the L^0 norm should be constantly 0 or also ∞ for non-measurable functions.

Thoughts? (cc @Yury G. Kudryashov, @Sébastien Gouëzel, @Rémy Degenne)

[Jeremy Tan]

Very good idea

[Floris van Doorn]

To elaborate on the second point: this ensures that all the information is captured by the norm. I think this will be very useful if we want to consider operations on seminorms/quasinorms, such as abstract interpolation theory (a very preliminary experiment is here)

[Sébastien Gouëzel]

I agree it's probably a good idea.

[James E Hanson]

Floris van Doorn said:

One thing I'm not sure about is whether the L^0 norm should be constantly 0 or also ∞ for non-measurable functions.

Is the fact that the L^0 norm is 0 actually used anywhere?

[Floris van Doorn]

Not intentionally, but we should probably make a choice that results in the fewest p \ne 0 hypotheses.

[James E Hanson]

This isn't specifically about non-measurable functions, but would it make sense to actually define it in terms of the limiting behavior of L^p seminorms as p goes to 0?

[Yury G. Kudryashov]

Some time ago, I wanted to redefine the norm so that

• we drop the outer (_)^(1/p) for 0 < p < 1
• we use the measure of support f for p = 0
  but I failed to finish the refactor before it rot.

[Yury G. Kudryashov]

This :up: would allow us to drop Fact (1 ≤ p) here and there.

[Yury G. Kudryashov]

E.g., we get a SeminormedGroup for any p, but it's a p-norm.

[James E Hanson]

That would have the benefit of generalizing of the existing meanings of the 'L^0 norm' in the literature (i.e., the L^0 norm of of a vector in $\mathbb{R}^n$ being the number of non-zero entries).

[Sébastien Gouëzel]

James E Hanson said:

That would have the benefit of generalizing of the existing meanings of the 'L^0 norm' in the literature (i.e., the L^0 norm of of a vector in $\mathbb{R}^n$ being the number of non-zero entries).

This formula depends on the specific choice of coordinates you are using, while the other L^p norms are invariant under linear maps preserving the volume (and are in particular coordinate independent), so I don't see how they could play well together.

[James E Hanson]

Sébastien Gouëzel said:

James E Hanson said:

That would have the benefit of generalizing of the existing meanings of the 'L^0 norm' in the literature (i.e., the L^0 norm of of a vector in $\mathbb{R}^n$ being the number of non-zero entries).

This formula depends on the specific choice of coordinates you are using, while the other L^p norms are invariant under linear maps preserving the volume (and are in particular coordinate independent), so I don't see how they could play well together.

When I say the seminorm is 'on' $\mathbb{R}^n$, I mean that $\mathbb{R}^n$ is the corresponding vector space, not the corresponding measure space. In that example, the measure space in question is the measure space with $n$ elements and the counting measure.

[Sébastien Gouëzel]

Ah, thanks for clarifying!

[James E Hanson]

Although now I just realized that in Mathlib 0 ^ 0 = 1 in ℝ, so it wouldn't immediately match the definition I mentioned.

[James E Hanson]

Ah, but this is already covered by Yury's proposal.