Commit 2023-04-02 14:57 5f6e827d

View on Github →

chore(measure_theory/measure/doubling): rename is_doubling_measure to is_unif_loc_doubling_measure (#18709) With thanks to Jireh for highlighting our non-standard terminology. See also Zulip conversation.

Estimated changes

Modified src/analysis/calculus/monotone.lean

Modified src/dynamics/ergodic/add_circle.lean

Modified src/measure_theory/covering/besicovitch.lean

Modified src/measure_theory/covering/density_theorem.lean

deleted theorem is_doubling_measure.ae_tendsto_average

deleted theorem is_doubling_measure.ae_tendsto_average_norm_sub

deleted theorem is_doubling_measure.ae_tendsto_measure_inter_div

deleted theorem is_doubling_measure.closed_ball_mem_vitali_family_of_dist_le_mul

deleted theorem is_doubling_measure.tendsto_closed_ball_filter_at

deleted def is_doubling_measure.vitali_family

added theorem is_unif_loc_doubling_measure.ae_tendsto_average

added theorem is_unif_loc_doubling_measure.ae_tendsto_average_norm_sub

added theorem is_unif_loc_doubling_measure.ae_tendsto_measure_inter_div

added theorem is_unif_loc_doubling_measure.closed_ball_mem_vitali_family_of_dist_le_mul

added theorem is_unif_loc_doubling_measure.tendsto_closed_ball_filter_at

added def is_unif_loc_doubling_measure.vitali_family

Modified src/measure_theory/covering/liminf_limsup.lean

Modified src/measure_theory/covering/one_dim.lean

Modified src/measure_theory/integral/periodic.lean

Modified src/measure_theory/measure/doubling.lean

deleted def is_doubling_measure.doubling_constant

deleted theorem is_doubling_measure.eventually_measure_le_scaling_constant_mul'

deleted theorem is_doubling_measure.eventually_measure_le_scaling_constant_mul

deleted theorem is_doubling_measure.eventually_measure_mul_le_scaling_constant_of_mul

deleted theorem is_doubling_measure.exists_eventually_forall_measure_closed_ball_le_mul

deleted theorem is_doubling_measure.exists_measure_closed_ball_le_mul'

deleted theorem is_doubling_measure.measure_mul_le_scaling_constant_of_mul

deleted theorem is_doubling_measure.one_le_scaling_constant_of

deleted def is_doubling_measure.scaling_constant_of

deleted def is_doubling_measure.scaling_scale_of

deleted theorem is_doubling_measure.scaling_scale_of_pos

added def is_unif_loc_doubling_measure.doubling_constant

added theorem is_unif_loc_doubling_measure.eventually_measure_le_scaling_constant_mul'

added theorem is_unif_loc_doubling_measure.eventually_measure_le_scaling_constant_mul

added theorem is_unif_loc_doubling_measure.eventually_measure_mul_le_scaling_constant_of_mul

added theorem is_unif_loc_doubling_measure.exists_eventually_forall_measure_closed_ball_le_mul

added theorem is_unif_loc_doubling_measure.exists_measure_closed_ball_le_mul'

added theorem is_unif_loc_doubling_measure.measure_mul_le_scaling_constant_of_mul

added theorem is_unif_loc_doubling_measure.one_le_scaling_constant_of

added def is_unif_loc_doubling_measure.scaling_constant_of

added def is_unif_loc_doubling_measure.scaling_scale_of

added theorem is_unif_loc_doubling_measure.scaling_scale_of_pos

Modified src/measure_theory/measure/haar_lebesgue.lean