Standard Machinery

Theorem

Let $\struct {X, \Sigma, \mu}$ be a measure space.

Let $\map {\LL^1_{\overline \R} } \mu$ be the space of $\mu$-integrable functions.

Let $\map P {f_1, \ldots, f_n}$ be a proposition, where the variables $f_i$ denote $\mu$-measurable functions $f_i: X \to \overline \R$.

Let every occurrence of an $f_i$ be of the form:

$\ds \int \map \Phi {f_i} \rd \mu$

for a suitable index set $I$ and multilinear mapping $\Phi: \map {\LL^1_{\overline \R} } \mu^I \to \map {\LL^1_{\overline \R} } \mu$.

Denote with $\map \chi \Sigma$ the set of characteristic functions of elements of $\Sigma$, that is:

$\map \chi \Sigma := \set {\chi_E: X \to \R: E \in \Sigma}$

Then the following are equivalent:

$(A): \quad \forall f_1, \ldots, f_n \in \map \chi \Sigma: \map P {f_1, \ldots, f_n}$

$(B): \quad \forall f_1, \ldots, f_n \in \map {\LL^1_{\overline \R} } \mu: \map P {f_1, \ldots, f_n}$

that is, it suffices to verify $P$ holds for characteristic functions.

Work In Progress In particular: Not completely valid as stated; need to restrict to $E$ with $\map \mu E < +\infty$ and impose more conditions on $P$ You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by completing it. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{WIP}} from the code.

Proof

This theorem requires a proof. You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by crafting such a proof. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{ProofWanted}} from the code. If you would welcome a second opinion as to whether your work is correct, add a call to {{Proofread}} the page.