A Computable Version of the Daniell-Stone Theorem on Integration and Linear Functionals
Yongcheng Wu, Klaus Weihrauch · Electronic Notes in Theoretical Computer Science · 2005
For every measure μ, the integral I:f↦∫fdμ is a linear functional on the set of real measurable functions. By the Daniell-Stone theorem, for every abstract integral Λ:F→R on a stone vector lattice F of real functions f:Ω→R there is a measure μ such that ∫fdμ=Λ(f) for all f∈F. In this paper we prove a computable version of this theorem.