Commit 2026-09-11 14:45 8319c83a

refactor(MeasureTheory): define eLpNorm f to be infinite when not AEStronglyMeasurable (#42406) This PR redefines eLpNorm f p μ to be infinite when f is not AEStronglyMeasurable. This has been discussed fairly thoroughly on Zulip here https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/eLpNorm.20junk.20value This simplifies some things, but complicates others. In particular, in some cases we need to require a topology now (though not very often) and in many lemmas we need a measurability requirement now. Some things can now be simplified; I changed the definition of MemLp from AEStronglyMeasurable f + eLpNorm f p μ < ∞ to eLpNorm f p \mu < ∞ since the measurability is now implied. I tried to minimise the measurability conditions throughout the library.