mathlib

f45d3379 - feat(measure_theory/covering/differentiation): Lebesgue differentiation theorem (#16906)

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.