Commit 2025-11-26 16:01 cb55ab33
View on Github →feat: many lemmas on integrability of a bounded linear map composed with two functions (#31661) Specialize ContinuousLinearMap.memLp_of_bilin to the case where one of the argument is bounded and the other is integrable. Add a version of MeasureTheory.Integrable.bdd_mul' for scalar multiplication. This is needed for #31666.