Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-16 19:59 59cda6d0

View on Github →

feat(measure_theory/group/basic): introduce a class is_haar_measure, and its basic properties (#9142) We have in mathlib a construction of Haar measures. But there are many measures which do not come from this construction, and are still Haar measures (Lebesgue measure on a vector space, Hausdorff measure of the right dimension, for instance). We introduce a new class is_haar_measure (and its additive analogue) to be able to express facts simultaneously for all these measures, and prove their basic properties.

Estimated changes

Modified src/measure_theory/group/basic.lean

added theorem is_compact.haar_lt_top

added theorem is_open.haar_pos

added theorem measure_theory.is_mul_left_invariant.measure_lt_top_of_is_compact'

added theorem measure_theory.is_mul_left_invariant.measure_lt_top_of_is_compact

added theorem measure_theory.is_mul_left_invariant.measure_pos_of_is_open

added theorem measure_theory.is_mul_left_invariant.measure_preimage_mul

modified theorem measure_theory.is_mul_left_invariant.null_iff_empty

added theorem measure_theory.is_mul_left_invariant.smul

added theorem measure_theory.is_mul_right_invariant.smul

added theorem measure_theory.measure.haar_pos_of_nonempty_interior

added theorem measure_theory.measure.haar_preimage_mul

added theorem measure_theory.measure.haar_preimage_mul_right

added theorem measure_theory.measure.haar_singleton

added theorem measure_theory.measure.is_haar_measure.smul

added theorem measure_theory.measure.is_haar_measure_map

added theorem measure_theory.measure.is_haar_measure_of_is_compact_nonempty_interior

added theorem measure_theory.measure.is_mul_left_invariant_haar

Modified src/topology/separation.lean

added theorem finite.is_closed

added theorem infinite_of_mem_nhds