Commit 2023-06-08 03:38 d2179494

View on Github →

feat: port MeasureTheory.Covering.BesicovitchVectorSpace (#4832)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Covering/BesicovitchVectorSpace.lean

added def Besicovitch.SatelliteConfig.centerAndRescale

added theorem Besicovitch.SatelliteConfig.centerAndRescale_center

added theorem Besicovitch.SatelliteConfig.centerAndRescale_radius

added theorem Besicovitch.SatelliteConfig.exists_normalized

added theorem Besicovitch.SatelliteConfig.exists_normalized_aux1

added theorem Besicovitch.SatelliteConfig.exists_normalized_aux2

added theorem Besicovitch.SatelliteConfig.exists_normalized_aux3

added theorem Besicovitch.card_le_multiplicity

added theorem Besicovitch.card_le_multiplicity_of_δ

added theorem Besicovitch.card_le_of_separated

added theorem Besicovitch.exists_goodδ

added def Besicovitch.goodδ

added theorem Besicovitch.goodδ_lt_one

added def Besicovitch.goodτ

added theorem Besicovitch.isEmpty_satelliteConfig_multiplicity

added theorem Besicovitch.le_multiplicity_of_δ_of_fin

added def Besicovitch.multiplicity

added theorem Besicovitch.multiplicity_le

added theorem Besicovitch.one_lt_goodτ