The reverse mathematics of theorems of Jordan and Lebesgue
The Jordan decomposition theorem states that every function $f \colon [0,1] \to \mathbb{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 $\mathsf{RCA}_0$, a stronger version of Jordan's result where all functions are continuous is equivalent to $\mathsf{ACA}_0$, while the version stated is equivalent to $\mathsf{WKL}_0$. The result that every function on $[0,1]$ of bounded variation is almost everywhere differentiable is equivalent to $\mathsf{WWKL}_0$. To state this equivalence in a meaningful way, we develop a theory of Martin-Löf randomness over $\mathsf{RCA}_0$.