A computable approach to measure and integration theory

We introduce a computable framework for Lebesgue's measure and integration theory in the spirit of domain theory. For an effectively given locally compact second countable Hausdorff space and an effectively given locally finite Borel measure on the space, we define the notion of a computable measurable set with respect to the given measure, which is stronger than Sanin's recursive measurable set. The set of computable measurable subsets is closed under complementation, finite unions and finite intersections. We then introduce interval-valued measurable functions and develop the notion of computable measurable functions using interval-valued simple functions. This leads us to the interval versions of the main results of the theory of Lebesgue integration which provide a computable framework for measure and integration theory. The Lebesgue integral of a computable integrable function with respect to an effectively given (sigma-)finite Borel measure on an effectively given (locally) compact second countable Hausdorff space can be computed up to any required accuracy. We show that, with respect to the metric induced from the L1norm, the set of Scott continuous interval-valued functions is dense in the set of interval-valued integrable functions.