Commit 2021-11-21 21:47 8f07d75b

feat(measure_theory/covering/differentiation): differentiation of measures (#10101) If ρ and μ are two Radon measures on a finite-dimensional normed real vector space, then for μ-almost every x, the ratio ρ (B (x, r)) / μ (B(x,r)) converges when r tends to 0, towards the Radon-Nikodym derivative of ρ with respect to μ. This is the main theorem on differentiation of measures. The convergence in fact holds for more general families of sets than balls, called Vitali families (the fact that balls form a Vitali family is a restatement of the Besicovitch covering theorem). The general version of the differentation of measures theorem is proved in this PR, following [Federer, geometric measure theory].