Abstract. Expectation (average) properties of continuous random variables are widely used to judge performance characteristics in engineering and physical sciences. This paper presents an infrastructure that can be used to formally reason about expectation properties of most of the continuous random variables in a theorem prover. Starting from the relatively complex higher-order-logic definition of expectation, based on Lebesgue integration, we formally verify key expectation properties that allow us to reason about expectation of a continuous random variable in terms of simple arithmetic operations. In order to illustrate the practical effectiveness and utilization of our approach, we also present the formal verification of expectation properties of the commonly used continuous random variables: Uniform, Triangular and Exponential.
Statistical properties of continuous random variables have been also verified in REF .
Formal Reasoning about Expectation Properties for Continuous Random Variables
FM
Computer Science