Lebesgue Differentiation and Weak Weak König's Lemma

Definitions and mathematical statement

Shared notation.

$\mathbb N=\{1,2,\ldots\}$, and $\mathbb Z,\mathbb Q,\mathbb R,\mathbb C$ denote the integers, rationals, reals and complex numbers. Any other conventions are specified locally.

Work in second-order arithmetic over $\mathsf{RCA}_0$, the base theory with $\Delta^0_1$ comprehension and $\Sigma^0_1$ induction. The strength of a principle means which subsystems prove it and which subsystems it implies over that base; equivalence requires both implications. An $L^1$ function on $[0,1]^d$, $d\geq1$, is represented as a Cauchy limit of polynomials in the $L^1$ norm. The Lebesgue differentiation theorem says that for almost every $x$, $f(x)=\lim_{Q\ni x,\,\operatorname{diam}Q\to0}\mu(Q)^{-1}\int_Qf\,d\mu$, where $Q$ ranges over open cubes containing $x$ and $\mu$ is Lebesgue measure. The principle $\mathsf{WWKL}_0$ asserts that every binary tree $T\subseteq\{0,1\}^{<\omega}$ of positive measure has an infinite path; positive measure means $\inf_n |T\cap\{0,1\}^n|/2^n>0$.

Statement recorded in the supplied source.

Does the Lebesgue differentiation theorem imply $\mathsf{WWKL}_0$ over $\mathsf{RCA}_0$? [S2]

Short English statement

Does proving almost-everywhere differentiation for all integrable functions require the positive-measure binary-tree path principle?

Sources

• S1 ULAM.AI and the UnsolvedMath Contributors, UnsolvedMath: A Curated Collection of Open Mathematics Problems, record 7500117 (AMR-074-0117). CC BY 4.0. https://huggingface.co/datasets/ulamai/UnsolvedMath.
• S2 Antonio Montalbán, Open Questions in Reverse Mathematics, author preprint dated 17 August 2010, Question 17, printed p. 7. https://math.berkeley.edu/~antonio/papers/questionsRM.pdf.