Commit 2022-10-12 23:21 f45d3379

feat(measure_theory/covering/differentiation): Lebesgue differentiation theorem (#16906) Given a doubling measure, then at almost every x the average of an integrable function on closed_ball x r converges to f x as r tends to zero (this is Lebesgue differentiation theorem). We give a version of this theorem for general Vitali families, and the concrete application to doubling measures.