Commit 2023-06-06 17:47 27fd4aea

View on Github →

feat: port MeasureTheory.Group.FundamentalDomain (#4740)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Group/FundamentalDomain.lean

added structure MeasureTheory.IsAddFundamentalDomain

added theorem MeasureTheory.IsFundamentalDomain.essSup_measure_restrict

added theorem MeasureTheory.IsFundamentalDomain.exists_ne_one_smul_eq

added theorem MeasureTheory.IsFundamentalDomain.iUnion_smul_ae_eq

added theorem MeasureTheory.IsFundamentalDomain.image_of_equiv

added theorem MeasureTheory.IsFundamentalDomain.integral_eq_tsum'

added theorem MeasureTheory.IsFundamentalDomain.integral_eq_tsum

added theorem MeasureTheory.IsFundamentalDomain.integral_eq_tsum_of_ac

added theorem MeasureTheory.IsFundamentalDomain.lintegral_eq_tsum'

added theorem MeasureTheory.IsFundamentalDomain.lintegral_eq_tsum

added theorem MeasureTheory.IsFundamentalDomain.lintegral_eq_tsum_of_ac

added theorem MeasureTheory.IsFundamentalDomain.measure_eq_card_smul_of_smul_ae_eq_self

added theorem MeasureTheory.IsFundamentalDomain.measure_eq_tsum'

added theorem MeasureTheory.IsFundamentalDomain.measure_eq_tsum

added theorem MeasureTheory.IsFundamentalDomain.measure_eq_tsum_of_ac

added theorem MeasureTheory.IsFundamentalDomain.measure_fundamentalFrontier

added theorem MeasureTheory.IsFundamentalDomain.measure_fundamentalInterior

added theorem MeasureTheory.IsFundamentalDomain.measure_le_of_pairwise_disjoint

added theorem MeasureTheory.IsFundamentalDomain.measure_set_eq

added theorem MeasureTheory.IsFundamentalDomain.measure_zero_of_invariant

added theorem MeasureTheory.IsFundamentalDomain.mk''

added theorem MeasureTheory.IsFundamentalDomain.mk'

added theorem MeasureTheory.IsFundamentalDomain.mk_of_measure_univ_le

added theorem MeasureTheory.IsFundamentalDomain.mono

added theorem MeasureTheory.IsFundamentalDomain.nullMeasurableSet_smul

added theorem MeasureTheory.IsFundamentalDomain.pairwise_aEDisjoint_of_ac

added theorem MeasureTheory.IsFundamentalDomain.preimage_of_equiv

added theorem MeasureTheory.IsFundamentalDomain.restrict_restrict

added theorem MeasureTheory.IsFundamentalDomain.set_integral_eq_tsum'

added theorem MeasureTheory.IsFundamentalDomain.set_integral_eq_tsum

added theorem MeasureTheory.IsFundamentalDomain.set_lintegral_eq_tsum'

added theorem MeasureTheory.IsFundamentalDomain.set_lintegral_eq_tsum

added theorem MeasureTheory.IsFundamentalDomain.smul

added theorem MeasureTheory.IsFundamentalDomain.smul_of_comm

added theorem MeasureTheory.IsFundamentalDomain.sum_restrict

added theorem MeasureTheory.IsFundamentalDomain.sum_restrict_of_ac

added structure MeasureTheory.IsFundamentalDomain

added theorem MeasureTheory.disjoint_fundamentalInterior_fundamentalFrontier

added def MeasureTheory.fundamentalFrontier

added theorem MeasureTheory.fundamentalFrontier_smul

added theorem MeasureTheory.fundamentalFrontier_subset

added theorem MeasureTheory.fundamentalFrontier_union_fundamentalInterior

added def MeasureTheory.fundamentalInterior

added theorem MeasureTheory.fundamentalInterior_smul

added theorem MeasureTheory.fundamentalInterior_subset

added theorem MeasureTheory.fundamentalInterior_union_fundamentalFrontier

added theorem MeasureTheory.mem_fundamentalFrontier

added theorem MeasureTheory.mem_fundamentalInterior

added theorem MeasureTheory.pairwise_disjoint_fundamentalInterior

added theorem MeasureTheory.sdiff_fundamentalFrontier

added theorem MeasureTheory.sdiff_fundamentalInterior

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

added theorem MeasureTheory.AEDisjoint.preimage

deleted theorem MeasureTheory.AeDisjoint.preimage