A computable version of the Daniell-Stone theorem on integration and linear functionals (Q2503282)

For every measure \(\nu\), the integral \(I: f\to \int f d\mu\) is a linear functional on the set of real measurable functions. By the Daniell-Stone theorem, for every abstract intergral \(\Lambda: F \to \mathbb{R}\) on a Stone vector lattice \(F\) of real functions \(f:\Omega \to \mathbb{R}\) there is a measure \(\mu\) such that \(\int f d \mu = \Lambda(f)\) for all \(f \in F\). In this paper a computable version of this theorem is proven.