ThmDex – An index of mathematical definitions, results, and conjectures.
Result R3863 on D1748: Signed basic integral
Signed basic integral with respect to a point measure
Formulation 0
Let $M = (X, \mathcal{F}, \delta_{x_0})$ be a D5671: Point measure space such that
(i) $f : X \to [-\infty, \infty]$ is an D1921: Absolutely integrable function on $M$
Then \begin{equation} \int_X f \, d \delta_{x_0} = f(x_0) \end{equation}
Subresults
▶ R4662: Signed basic expectation with respect to a point probability measure
Proofs
Proof 0
Let $M = (X, \mathcal{F}, \delta_{x_0})$ be a D5671: Point measure space such that
(i) $f : X \to [-\infty, \infty]$ is an D1921: Absolutely integrable function on $M$
By definition \begin{equation} \int_X f \, d \delta_{x_0} = \int_X f^+ \, d \delta_{x_0} - \int_X f^- \, d \delta_{x_0} \end{equation} We may thus use results
(i) R4698: Unsigned basic integral with respect to a point measure
(ii) R1022: Partition of basic function into positive and negative parts

to conclude \begin{equation} \int_X f \, d \delta_{x_0} = \int_X f^+ \, d \delta_{x_0} - \int_X f^- \, d \delta_{x_0} = f^+(x_0) - f^-(x_0) = f(x_0) \end{equation} $\square$