Commit 2025-04-15 12:02 091be7a8

feat(LpSeminorm/Basic): generalise monotonicity section to enorm (#23707) For every lemma about normed spaces, we add an enorm variant. These have virtually identical proofs, sometimes even slightly shorter. Since the new lemmas have slightly different hypotheses (involving enorms, not (nn)norms), I have left the original lemmas untouched for now. I'm happy to investigate their removal, but would like such a conversation to not delay merging this PR. Prepared for the Carleson project: these lemmas are necessary for generalising basic lemmas about operators of weak/strong type to ENorm. In passing, this PR corrects a few related shortcomings which were noticed during development:

• weaken a hypothesis of a lemma tweaked in #22798: the hypothesis was already unnecessarily strong; this PR changes it to ContinuousENorm, which suffices.
• document that eLpNorm' is a purely auxiliary quantity
• mention a counterexample why lintegral_eq_zero_iff' requires measurability hypotheses