THE REVERSE MATHEMATICS OF THEOREMS OF JORDAN AND LEBESGUE

The Jordan decomposition theorem states that every function f : [0, 1] R of bounded variation can be written as the difference of two non-decreasing functions. Combining this fact with a result of Lebesgue, every function of bounded variation is differentiable almost everywhere in the sense of Lebesgue measure. We analyze the strength of these theorems in the setting of reverse mathematics. Over RCA, a stronger version of Jordan's result where all functions are continuous is equivalent to ACA0, while the version stated is equivalent to WKL0. The result that every function on [0, 1] of bounded variation is almost everywhere differentiable is equivalent to MANKL0. To state this equivalence in a meaningful way, we develop a theory of Martin Lof randomness over RCA.