Commit 2025-05-21 11:47 674e9c00

feat(L1Space/IntegrableOn): generalise more lemmas to enorm (#24352)

• integrableOn_const now includes a side condition that the constant is finite: use by finiteness as default argument, and teach finiteness about enorm_lt_top to make this possible.
• Further, rename integrableOn_const to integrableOn_const_iff (it was always an iff statement), and
• introduce integrableOn_const for just the backwards direction (which is the lemma's most common use).
• similarly, introduce integrableOn_singleton for the backwards direction of integrableOn_singleton_iff, which is its most common use Future possibilities include generalising norm_le_pi_norm to enorm, and generalising HasFiniteIntegral.of_finite.