Automating proofs via indicator functions?

58 Views Asked by At

It is a common technique in measure theory to prove something for indicator functions / elementary functions, generalize it to positive-valued functions and to measurable functions via $X = X^+ - X^-$. It is used e. g. to prove multiple integral properties or "independent random variables are uncorrelated".

This technique is a bit boring to execute, if one has shown a question already for the indicator functions. Is it somehow possible to describe the set of all statements which are true for all measurable functions if the result is proven for only indicator functions / elementary functions? I'm in search of something like the Transfer Principle in nonstandard analysis.