Lemma 10.2.2

Stream: Carleson

[James Sundstrom]

The comment on lebesgue_differentiation (Lemma 10.2.2) says that it should be an easy consequence of VitaliFamily.ae_tendsto_average, but it doesn't appear to be. That lemma applies to families of closed sets, but we need to prove a statement about averages over open balls. Obviously if we knew that ball x r and closedBall x r always had the same measure, this distinction wouldn't matter, but I don't think we can assume that's the case here.

For reference, here's my proof of a modified Lemma 10.2.2 using closed balls. This version is indeed an easy consequence of VitaliFamily.ae_tendsto_average, but I don't think it helps with its intended use (proving Lemma 10.2.5). A proof of Lemma 10.2.5 using the original version of Lemma 10.2.2 can be seen here.

[Sébastien Gouëzel]

I see two ways out here, if I'm not mistaken

• There are only countably many radii where the sphere S (x, r) has positive measure (as the overall measure of the ball is finite and the spheres are disjoint), so you can find a sequence of radii tending to zero where the closed ball and the open ball have the same measure. Since lebesgue_differentiation only asks for some sequence of radii, you're fine.
• But in fact, the Lebesgue differentiation theorem holds along all open balls. It can be deduced from the statement for closed ball: the open ball B = openBall x r is the increasing limit of B_n = closedBall x (r - 1/n). By the dominated convergence theorem, the integral of f on B_n converges to the integral on B, and same for the measure. So if you know that all the ∫ x in B_n, f x / measure (B_n) are close to a number, then so is the same quantity over B.

[Sébastien Gouëzel]

The second way out is better, because it's more general, but for Carleson I guess you can use whatever version looks easier to formalize to you.

[Sébastien Gouëzel]

Another argument for the first version is to say that r -> measure (closedBall x r) is monotone, so it is continuous at all but countably many points (see docs#Monotone.countable_not_continuousAt), and then at the continuity points the open ball and the closed ball have the same measure.