Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-05 12:41 a17aefd3

View on Github →

feat(measure_theory/covering/density_theorem): add a version of Lebesgue's density theorem (#16762)

Estimated changes

Modified src/algebra/group_power/basic.lean

added theorem pow_three'

added theorem pow_three

Modified src/algebra/group_with_zero/basic.lean

added theorem mul_left_surjective₀

added theorem mul_right_surjective₀

Modified src/data/set/intervals/image_preimage.lean

added theorem set.image_const_mul_Ioi_zero

Modified src/measure_theory/covering/besicovitch.lean

Created src/measure_theory/covering/density_theorem.lean

added theorem is_doubling_measure.ae_tendsto_measure_inter_div

added def is_doubling_measure.doubling_constant

added theorem is_doubling_measure.eventually_scaling_constant_of

added theorem is_doubling_measure.exists_eventually_forall_measure_closed_ball_le_mul

added theorem is_doubling_measure.exists_measure_closed_ball_le_mul'

added def is_doubling_measure.scaling_constant_of

added def is_doubling_measure.vitali_family

Modified src/measure_theory/covering/vitali_family.lean

added theorem vitali_family.eventually_filter_at_subset_closed_ball

added theorem vitali_family.tendsto_filter_at_iff

Modified src/order/filter/basic.lean

added theorem filter.forall_eventually_of_eventually_forall

Modified src/topology/algebra/order/basic.lean

added theorem eventually_nhds_within_pos_mem_Ioc

added theorem eventually_nhds_within_pos_mem_Ioo

added theorem eventually_nhds_within_pos_mul_left

added theorem nhds_within_pos_comap_mul_left

Modified src/topology/continuous_on.lean

added theorem eventually_mem_of_tendsto_nhds_within

added theorem tendsto_nhds_of_tendsto_nhds_within