Commit 2023-11-11 06:37 e052b5ef

View on Github →

feat: more facts on measures in topological groups (#8286) Prerequisites for #8198

Estimated changes

Modified Mathlib/MeasureTheory/Group/LIntegral.lean

modified theorem MeasureTheory.lintegral_eq_zero_of_isMulLeftInvariant

Modified Mathlib/MeasureTheory/Group/Measure.lean

added theorem IsCompact.closure_subset_of_measurableSet_of_group

added theorem IsCompact.measure_closure_eq_of_group

added theorem MeasurableSet.mul_closure_one_eq

added theorem MeasureTheory.Measure.inv_def

added theorem MeasureTheory.Measure.isHaarMeasure_map_of_isFiniteMeasure

added theorem MeasureTheory.innerRegular_inv_iff

deleted theorem MeasureTheory.isOpenPosMeasure_of_mulLeftInvariant_of_regular

added theorem MeasureTheory.measure_mul_closure_one

modified theorem MeasureTheory.regular_inv_iff