The Lebesgue Differentiation Theorem over RCA0: On Question 17 of Montalbán's Open Questions in Reverse Mathematics

Question 17 of Montalbán's survey of open questions in reverse mathematics (Bull. Symbolic Logic 17 (2011)) asks whether the Lebesgue differentiation theorem (LDT) implies \(\mathsf{WWKL}_0\) over \(\mathsf{RCA}_0\); Simpson had observed, using Pathak's work, that LDT is provable in \(\mathsf{WWKL}_0\). The question does not fix how “for almost every \(x\)” and the measure of an open set are formalised, and the answer depends on this. We prove in \(\mathsf{RCA}_0\): for every \(L^1\) function \(f=(p_n)\) on \([0,1]^d\), given by rational polynomials with \(\|p_n-p_{n+1}\|_1\le2^{-n}\), there are open sets \(U_N\), uniformly \(\Delta^0_1\) in \(f\), of measure at most \(\varepsilon_N\to0\) (for the extensional measure of Brown, Giusto and Simpson and for the measure \(\bar\mu\) of Nies, Triplett and Yokoyama), such that every point outside some \(U_N\) is a Lebesgue point of \(f\) with \(f(x)=\lim p_n(x)\), and every box of measure \(>\varepsilon_N\) meets the complement of \(U_N\). Hence \(\mathsf{RCA}_0\) proves LDT under the null-cover reading of Yu and of Brown, Giusto and Simpson, under the reading that Lebesgue points exist and are dense, and under the randomness reading; under these readings LDT does not imply \(\mathsf{WWKL}_0\). Under the outer reading of Nies, Triplett and Yokoyama, LDT is equivalent to \(\mathsf{WWKL}_0\); the reversal uses their open set of measure \(<1\) whose complement consists of dyadic rationals, and it reflects the behaviour of measure in \(\mathsf{RCA}_0\), not differentiation. We judge the null-cover reading to be the intended one, so that the answer is no. The method makes the maximal-function estimates of Pathak, Rojas and Simpson finite. Yu proved in \(\mathsf{RCA}_0\) that the values \(p_n(x)\) converge outside a Martin-Löf null set; our results are close to known techniques and may be known to experts, but we found no printed answer to the question. This is an unrefereed note.