Commit 2025-04-29 15:12 6943d23d

feat(LpSeminorm/Basic): generalise a few more lemmas to enorms (#24355)

• For some lemmas, this was as easy as changing the co-domain.
• Weaken a few enorm typeclasses: make shadowing explicit by using named sections.
• For other lemmas, the enorm version requires a new explicit hypothesis (typically, around some constant being non-zero). For those, we add a new enorm version, and golf the existing result in terms of that. For the Carleson project.