feat(normed_space/lp_space): Lp space for Π i, E i (#11015)

For a family `Π i, E i` of normed spaces, define the subgroup with finite lp norm, and prove it is a `normed_group`.  Many parts adapted from the development of `measure_theory.Lp` by @RemyDegenne.

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Lp.20space