Commit 2023-06-07 15:05 e7155768

View on Github →

feat: port MeasureTheory.Covering.Besicovitch (#4794)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Covering/Besicovitch.lean

added structure Besicovitch.BallPackage

added theorem Besicovitch.SatelliteConfig.hlast'

added theorem Besicovitch.SatelliteConfig.inter'

added structure Besicovitch.SatelliteConfig

added def Besicovitch.TauPackage.R

added theorem Besicovitch.TauPackage.color_lt

added def Besicovitch.TauPackage.iUnionUpTo

added def Besicovitch.TauPackage.lastStep

added theorem Besicovitch.TauPackage.lastStep_nonempty

added theorem Besicovitch.TauPackage.mem_iUnionUpTo_lastStep

added theorem Besicovitch.TauPackage.monotone_iUnionUpTo

added structure Besicovitch.TauPackage

added theorem Besicovitch.ae_tendsto_measure_inter_div

added theorem Besicovitch.ae_tendsto_measure_inter_div_of_measurableSet

added theorem Besicovitch.ae_tendsto_rnDeriv

added theorem Besicovitch.exist_disjoint_covering_families

added theorem Besicovitch.exist_finset_disjoint_balls_large_measure

added theorem Besicovitch.exists_closedBall_covering_tsum_measure_le

added theorem Besicovitch.exists_disjoint_closedBall_covering_ae

added theorem Besicovitch.exists_disjoint_closedBall_covering_ae_aux

added theorem Besicovitch.exists_disjoint_closedBall_covering_ae_of_finiteMeasure_aux

added theorem Besicovitch.tendsto_filterAt

added def Besicovitch.unitBallPackage