Commit 2021-10-02 09:30 e26a9e56

View on Github →

feat(measure_theory/covering/besicovitch): the Besicovitch covering theorem (#9462) The Besicovitch covering theorem: in a nice metric space (e.g. real vector spaces), from any family of balls one can extract N subfamilies made of disjoint balls, covering all the centers of the balls in the family. The number N only depends on the metric space.

Estimated changes

Modified docs/references.bib

Created src/measure_theory/covering/besicovitch.lean

added structure besicovitch.ball_package

added theorem besicovitch.exist_disjoint_covering_families

added theorem besicovitch.satellite_config.hlast'

added theorem besicovitch.satellite_config.inter'

added structure besicovitch.satellite_config

added def besicovitch.tau_package.R

added def besicovitch.tau_package.Union_up_to

added theorem besicovitch.tau_package.color_lt

added def besicovitch.tau_package.last_step

added theorem besicovitch.tau_package.last_step_nonempty

added theorem besicovitch.tau_package.mem_Union_up_to_last_step

added theorem besicovitch.tau_package.monotone_Union_up_to

added structure besicovitch.tau_package

added def besicovitch.unit_ball_package