Bochner integral

Stream: new members

[Pietro Lavino]

is the Bochner integral of a function f: \alpha to \R allowed to be equal to infinity?

[Sébastien Gouëzel]

No, the Bochner integral is real-valued (or vector-space valued) by definition. There is in mathlib a version of the integral that can take value infinity, but it's for functions taking values in ENNReal (and it's called the Lebesgue integral).