Importing ENNReal in normed groups

Stream: mathlib4

[Michael Rothgang]

In #21670, I'm adding a few new typeclasses, which generalise normed groups to include ENNReal: this need arose in the Carleson project.

(Some broader context: this change allows e.g. stating "the Hardy-Littlewood maximal function has weak type L^p", with that function being ENNReal-valued --- without duplicating this definition. The definition of e.g. HasFiniteIntegral was already changed some time ago to allow for enormed spaces, now I'd like to generalise many lemmas in mathlib.)

These typeclasses assume the space in question has an enorm, which is ENNReal-valued: to speak about continuity of that enorm, I need to import the topology on ENNReal, and know that the coercion to NNReal is continuous. Currently, this adds about 120 transitive imports to that file. The easy way of reducing imports does not help much. There are ideas for reducing the effect, but at some point there will be an increase.

In my opinion, this is the price to pay for this generalisation: having a more usable analysis library is worth it.
However, if you have major objections to this, please speak up and let's discuss!

[Xavier Roblot]

Note that, if #21995 gets merged, then Data.Complex.Abs will be replaced by Data.Complex.Norm which imports Analysis.Normed.Group.Basic. Thus, any changes to the imports of Analysis.Normed.Group.Basic could have a lot of impact. That was the reason for the split in #21554

[Anne Baanen]

(Reviving this topic since I want to rearrange the Instances.{ENN,NN,}Real file in the coming days.) In the end my stance is that import cleanup is all about unused imports. If you add a set of imports that are useful, then no harm has been done.