ThmDex – An index of mathematical definitions, results, and conjectures.
Formulation 0
Let $M = (X, \mathcal{F}, \mu)$ be a D1158: Measure space such that
(i) $f : X \to [0, \infty]$ is an D5610: Unsigned basic Borel function on $M$
Let $\lambda \in [0, \infty]$ be an D5237: Unsigned basic number.
Then \begin{equation} \lambda \mu(f > \lambda) \leq \int_X f I_{\{ f > \lambda \}} \, d \mu \end{equation}
Formulation 1
Let $M = (X, \mathcal{F}, \mu)$ be a D1158: Measure space such that
(i) $f : X \to [0, \infty]$ is an D5610: Unsigned basic Borel function on $M$
Let $\lambda \in [0, \infty]$ be an D5237: Unsigned basic number.
Then \begin{equation} \lambda \mu \{ x \in X : f(x) > \lambda \} \leq \int_X f I_{\{ f > \lambda \}} \, d \mu \end{equation}