Commit 2023-05-31 10:33 422af61d

View on Github →

feat: port MeasureTheory.Measure.Haar.Basic (#4517) This PR also rename locallyCompactSpace_of_Group to locallyCompactSpace_of_group, and add a reference to the issue in MeasureTheory.Group.Measure.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/MeasureTheory/Group/Measure.lean

Created Mathlib/MeasureTheory/Measure/Haar/Basic.lean

added theorem MeasureTheory.Measure.MeasurePreserving.zpow

added theorem MeasureTheory.Measure.div_mem_nhds_one_of_haar_pos

added theorem MeasureTheory.Measure.haar.chaar_empty

added theorem MeasureTheory.Measure.haar.chaar_mem_clPrehaar

added theorem MeasureTheory.Measure.haar.chaar_mem_haarProduct

added theorem MeasureTheory.Measure.haar.chaar_mono

added theorem MeasureTheory.Measure.haar.chaar_nonneg

added theorem MeasureTheory.Measure.haar.chaar_self

added theorem MeasureTheory.Measure.haar.chaar_sup_eq

added theorem MeasureTheory.Measure.haar.chaar_sup_le

added def MeasureTheory.Measure.haar.clPrehaar

added theorem MeasureTheory.Measure.haar.haarContent_apply

added theorem MeasureTheory.Measure.haar.haarContent_outerMeasure_self_pos

added theorem MeasureTheory.Measure.haar.haarContent_self

added def MeasureTheory.Measure.haar.haarProduct

added theorem MeasureTheory.Measure.haar.index_defined

added theorem MeasureTheory.Measure.haar.index_elim

added theorem MeasureTheory.Measure.haar.index_empty

added theorem MeasureTheory.Measure.haar.index_mono

added theorem MeasureTheory.Measure.haar.index_pos

added theorem MeasureTheory.Measure.haar.index_union_eq

added theorem MeasureTheory.Measure.haar.index_union_le

added theorem MeasureTheory.Measure.haar.is_left_invariant_chaar

added theorem MeasureTheory.Measure.haar.is_left_invariant_haarContent

added theorem MeasureTheory.Measure.haar.is_left_invariant_index

added theorem MeasureTheory.Measure.haar.is_left_invariant_prehaar

added theorem MeasureTheory.Measure.haar.le_index_mul

added theorem MeasureTheory.Measure.haar.mem_prehaar_empty

added theorem MeasureTheory.Measure.haar.mul_left_index_le

added theorem MeasureTheory.Measure.haar.nonempty_iInter_clPrehaar

added theorem MeasureTheory.Measure.haar.prehaar_empty

added theorem MeasureTheory.Measure.haar.prehaar_le_index

added theorem MeasureTheory.Measure.haar.prehaar_mem_haarProduct

added theorem MeasureTheory.Measure.haar.prehaar_mono

added theorem MeasureTheory.Measure.haar.prehaar_nonneg

added theorem MeasureTheory.Measure.haar.prehaar_pos

added theorem MeasureTheory.Measure.haar.prehaar_self

added theorem MeasureTheory.Measure.haar.prehaar_sup_eq

added theorem MeasureTheory.Measure.haar.prehaar_sup_le

added theorem MeasureTheory.Measure.haarMeasure_apply

added theorem MeasureTheory.Measure.haarMeasure_eq_smul_haarMeasure

added theorem MeasureTheory.Measure.haarMeasure_self

added theorem MeasureTheory.Measure.haarMeasure_unique

added theorem MeasureTheory.Measure.measurePreserving_zpow

added theorem MeasureTheory.Measure.regular_of_mulLeftInvariant

Modified Mathlib/Topology/Algebra/Group/Compact.lean

deleted theorem TopologicalSpace.PositiveCompacts.locallyCompactSpace_of_Group

added theorem TopologicalSpace.PositiveCompacts.locallyCompactSpace_of_group