ENorm for measure theory

Stream: mathlib4

[Floris van Doorn]

In analysis, one often works with functions that are well-defined only almost everywhere. On a set of measure 0 we might take integrals of non-integrable functions, supremums over values that are not bounded and things like that.
For example in the Carleson project we define the Hardy-Littlewood maximal function (carleson#maximalFunction). This takes functions into ENNReal, because ENNReal-valued suprema are nicer to work with, and on a set of measure 0 the maximal function can be infinite.
For the functions we are considering, we do want to prove that being infinite only happens on a set of measure 0. The typical proof goes as follows:
(1) We prove that if the input function is L^1 (docs#MeasureTheory.Memℒp) then the output function is weak-L^1 (link).
(2) If a function is weak-L^1, then it is almost everywhere not equal to infinity.

Now even stating step 2 requires some care: the linked version of weak-L^p above follows Mathlib's examples of docs#MeasureTheory.eLpNorm and many similar definitions to consider maps from a measurable space to a normed space. Using such a codomain, we already have to turn our map into a map into Real by using ENNReal.toReal (see e.g. carleson#HasWeakType.MB_one), and then we have lost information about where this map is infinity.

To fix this, @Pietro Monticone and I have defined a slightly more general version of definitions like L^p-norm, being L^p, weak-L^p, etc. in this file. For these definitions, the only thing we need is a map from the codomain to ENNReal, so we define a class doing exactly that:

class ENorm (E : Type*) where
  enorm : E → ℝ≥0∞

Compare docs#Norm and docs#NNNorm.
We have two natural instances: the identity function on ENNReal and

instance [NNNorm E] : ENorm E where
  enorm := (‖·‖₊ : E → ℝ≥0∞)

My concrete suggestion is to add the ENorm class to Mathlib, and generalize definitions like Integrable/Memℒp/eLpNorm/... to use this definition. I think the fallout of this will be minimal, except that we will replace some uses of a lemma about coe_nnnorm with the corresponding lemma about enorm.

Two remarks:

• An alternative approach is to duplicate the definitions: have one version of Banach-space-valued functions and one for ENNReal-valued functions (which we do for e.g. integration). I don't like this duplication, and this problem might get worse when we consider a predicate on an operator stating that it sends L^p maps to L^p maps. Then we might potentially need 4 versions of such a predicate.
• In this proposal I am suggesting to not suggesting to generalize many lemmas: anything that mentions addition on the Banach space will still be stated using Banach spaces for a while. We can consider later to also generalize some lemmas, but that would require classes that state the relation between enorm and algebraic operations, the topology, etc. I'm not sure what these classes should be precisely (e.g.: the topology on ENNReal is not given by the standard metric on ENNReal). I added something (ENormedAddMonoid) in the linked file above, but the intention is not to port that to Mathlib at first.

Thoughts?

[Edward van de Meent]

i guess you can compare mathlibs docs#EDist / docs#NNDist / docs#Dist design to decide how this might fit in with the rest. See also docs#EMetricSpace / docs#MetricSpace for how this example uses forgetful inheritance.

[Floris van Doorn]

@Yury G. Kudryashov I just saw that docs#ENorm exists in Mathlib. It was apparently defined in 2020, but still a leaf file of Mathlib.
Can we rename it to ENormedSpace so that ENorm becomes available for just the class defining the notation?
Or maybe more radically: should this be removed?

[Yury G. Kudryashov]

I thought that it will be useful to define Lp spaces, but it was never used there.

[Yury G. Kudryashov]

You may deprecate the whole file and/or rename any parts of it.

[Yury G. Kudryashov]

I have no other plans for this structure.