A nonstandard proof of a lemma from constructive measure theory

Suppose that f(n) is a sequence of nonnegative functions with compact support on a locally compact metric space, that T is a nonnegative linear functional, and that Sigma(infinity)(n=1), T f(n) < T(f0). A result of Bishop, foundational to a constructive theory of functional analysis, asserts the existence of a point x such that Sigma(infinity)(n=1), f(n)(x) < f(0)(x). This paper extends this result to arbitrary Hausdorff spaces, and gives short proofs using nonstandard analysis. While such arguments used are not themselves constructive, they can illuminate where the difficulty lies in finding the point x. An algorithm for constructing x is then given, with a nonstandard proof that the algorithm converges to a correct value. (c) 2006 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim.