Commit 2022-10-10 13:36 09b58946

View on Github →

feat(measure_theory/measure/haar_lebesgue): the Lebesgue measure is doubling (#16885) Also split the file measure_theory/covering/density_theorem in two, to avoid importing all the differentiation theory into haar_lebesgue.lean.

Estimated changes

Modified src/analysis/special_functions/stirling.lean

modified theorem stirling.log_stirling_seq'_antitone

Modified src/data/real/nnreal.lean

added theorem real.to_nnreal_pow

Modified src/measure_theory/covering/density_theorem.lean

deleted def is_doubling_measure.doubling_constant

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 def is_doubling_measure.scaling_constant_of

deleted def is_doubling_measure.scaling_scale_of

deleted theorem is_doubling_measure.scaling_scale_of_pos

Created src/measure_theory/measure/doubling.lean

added def is_doubling_measure.doubling_constant

added theorem is_doubling_measure.eventually_measure_mul_le_scaling_constant_of_mul

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 theorem is_doubling_measure.measure_mul_le_scaling_constant_of_mul

added def is_doubling_measure.scaling_constant_of

added def is_doubling_measure.scaling_scale_of

added theorem is_doubling_measure.scaling_scale_of_pos

Modified src/measure_theory/measure/haar_lebesgue.lean