Commit 2025-04-29 16:34 587458d2

chore(L1Space/HasFiniteIntegral): generalise a few lemmas to enorm (#24343) These are necessary to speak about IntegrableOn well. Similarly to previous PRs, when a statement needs more than trivial changes, this PR just adds enorm analogues (without deprecating existing lemmas) and tries to golf the existing version in terms of the enorm result. (In this PR, I chose to not always golf one-line proofs. For multi-line proofs, this PR shows that work can really be re-used.)