Lebesgue differentiation theorem for $L^1$ functions

Let $f\in L^1({\mathbb{R}}^n)$. Then for almost every $x\in {\mathbb{R}}^n$,

${\lim }_{r\to 0^{+}}\frac{1}{{\lambda }_n(B(x,r))}{\int }_{B(x,r)}fd{\lambda }_n=f(x),$

and indeed almost every $x$ is a Lebesgue point, meaning

${\lim }_{r\to 0^{+}}\frac{1}{{\lambda }_n(B(x,r))}{\int }_{B(x,r)}\mathrm{\mid }f(y)-f(x)\mathrm{\mid }d{\lambda }_n(y)=0.$

In dimension one this says that for $f\in L^1[a,b]$ the indefinite integral $F(x)={\int }_a^{x}fd\lambda$ satisfies $F^{\mathrm{\prime }}=f$ almost everywhere, which is the Lebesgue form of the first fundamental theorem of calculus. A special case is the Lebesgue density theorem: a measurable set $E$ has density $1$ at almost every point of $E$ and density $0$ at almost every point of its complement.

Not proved in this library. It is recorded with citations and used in no proof here.

What would prove it. The Hardy-Littlewood maximal inequality, itself proved from the $5r$ covering lemma inside Vitali covering theorem ‡, plus density of the continuous functions in $L^1$, plus the dominated convergence theorem (Dominated convergence theorem ‡). Every ingredient is measure-theoretic.

Which page it serves. The fundamental theorems of calculus page. That page proves that $F(x)={\int }_a^{x}f$ is differentiable with $F^{\mathrm{\prime }}=f$ at every point where $f$ is continuous, which is as far as the Riemann theory reaches. The theorem above removes continuity entirely and replaces "at every point of continuity" by "at almost every point", and together with The sharp fundamental theorem of calculus (absolute continuity) ‡ it closes the subject.

Why it is stated separately from the monotone case. See the naming warning in Lebesgue's differentiation theorem for monotone functions ‡. The two results are close relatives, each provable from Vitali-type covering arguments, but they are different statements about different objects, and conflating them is a common source of confusion about what the fundamental theorem of calculus actually says.