[Merged by Bors] - feat(analysis/normed_space/enorm): define extended norm

[urkud]

No description provided.

[sgouezel]

I have a design question here. When one does analysis with, say, L^p functions, then one wants to work with functions (to be able to speak of the value of a function at a point), and not equivalence classes of functions, most of the time, and only switch to equivalence classes when applying some results of functional analysis. On the other hand, with your definition of enorm, where you require that only the zero function can have zero enorm, you can only put it on equivalence classes of functions.

Think for instance of the case where you speak of continuous functions on [0,1], and you want to say that the L^1 norm of your function is bounded by the C^0 norm. Since the C^0 norm works on genuine functions, not on equivalence classes, then the statement will become awkward to state and to use.

So, I am wondering if in the definition of enorm you should not also allow the enorm to vanish on more vectors than just 0. And then to e : enorm you could associate its kernel (the vector with 0 norm), and put an emetric space structure on V / e.ker, and a metric space structure on e.finite_subspace / e.ker.

Both options have pros and cons, so I just want to be sure that you have considered both of them before opting for one. (Avoiding quotients as you do is probably a good idea, in fact). It would be worth mentioning this in the docstring, too.

[urkud]

Both options have pros and cons, so I just want to be sure that you have considered both of them before opting for one.

No, I missed this point.

(Avoiding quotients as you do is probably a good idea, in fact).

Another approach: define eseminorm, then eseminorm.to_enorm (on the quotient space`). What do you think about this?

[sgouezel]

I would say: for now, let's only define enorms as in your file. Maybe this will be sufficient, together with a coercion from functions to almost everywhere defined functions, and otherwise we will see what we need when we need it.

[sgouezel]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Run tests and docs