Commit 2024-06-16 12:04 950e3d06

View on Github →

feat (MeasureTheory/Function): trivial cases of integrability / summability (#13872) Any function on a finite type is multipliable / summable; a function on a discrete measurable space is integrable iff its norm is summable.

Estimated changes