Structures · Analysis
MeasureTheory.SMulInvariantMeasure
A measure μ : Measure α is invariant under a multiplicative action of M on α if for any
measurable set s : Set α and c : M, the measure of its preimage under fun x => c • x is equal
to the measure of s.
- Defined in
- Mathlib.MeasureTheory.Group.Defs
- Shape
- 3 explicit arguments · adds measure_preimage_smul
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances3
- Matrix.GeneralLinearGroup
- Subtype
- MulOpposite
How is a type an instance?
Loading the hierarchy index…
Assumed by134
- MeasureTheory.measurePreserving_smul
- MulAction.aestabilizer
- MeasureTheory.measure_smul
- MeasureTheory.SMulInvariantMeasure.measure_preimage_smul
- MeasureTheory.IsFundamentalDomain.sum_restrict_of_ac
- MeasureTheory.IsFundamentalDomain.covolume_eq_volume
- MeasureTheory.IsFundamentalDomain.measure_eq_tsum
- MeasureTheory.IsFundamentalDomain.measure_zero_of_invariant
- MeasureTheory.NullMeasurableSet.smul
- MeasureTheory.measure_preimage_smul
- MeasureTheory.IsFundamentalDomain.lintegral_eq_tsum_of_ac
- MeasureTheory.IsFundamentalDomain.nullMeasurableSet_smul
- MeasureTheory.measure_preimage_smul_le
- MulAction.mem_aestabilizer
- MeasureTheory.IsFundamentalDomain.setLIntegral_eq
- MeasureTheory.IsFundamentalDomain.restrict_restrict
- MeasureTheory.IsFundamentalDomain.integral_eq_tsum_of_ac
- MeasureTheory.IsFundamentalDomain.quotientMeasureEqMeasurePreimage_quotientMeasure
- MeasureTheory.tendsto_smul_ae
- MeasureTheory.IsFundamentalDomain.quotientMeasureEqMeasurePreimage
- MeasureTheory.IsFundamentalDomain.setIntegral_eq_tsum
- MeasureTheory.IsFundamentalDomain.setLIntegral_eq_tsum'
- MeasureTheory.IsFundamentalDomain.setLIntegral_eq_tsum
- MulAction.aestabilizer_univ
- MulAction.aestabilizer_empty
- MeasureTheory.QuotientMeasureEqMeasurePreimage.covolume_ne_top
- IsFoelner.mean_smul_eq_mean
- MeasureTheory.IsFundamentalDomain.integral_eq_tsum''
- MeasureTheory.IsFundamentalDomain.lintegral_eq_tsum'
- IsFoelner.mean_smul_eq_mean_smul
- MeasureTheory.measure_sdiff_inv_smul
- MeasureTheory.IsFundamentalDomain.setIntegral_eq_tsum'
- MeasureTheory.IsFundamentalDomain.integral_eq_tsum'
- MeasureTheory.IsFundamentalDomain.measure_eq
- MeasureTheory.IsFundamentalDomain.lintegral_eq_tsum''
- MeasureTheory.IsFundamentalDomain.aestronglyMeasurable_on_iff
- MeasureTheory.measure_inv_smul_symmDiff
- MeasureTheory.IsFundamentalDomain.smul_of_comm
- MeasureTheory.IsFundamentalDomain.measure_eq_tsum_of_ac
- MeasureTheory.measure_isOpen_pos_of_smulInvariant_of_compact_ne_zero
- MeasureTheory.IsFundamentalDomain.hasFiniteIntegral_on_iff
- MeasureTheory.IsFundamentalDomain.integrableOn_iff
- MeasureTheory.NullMeasurableSet.fundamentalInterior
- MeasureTheory.measure_smul_eq_zero_iff
- DomMulAct.dist_smul_Lp
- MeasureTheory.measure_symmDiff_inv_smul
- MeasureTheory.IsFundamentalDomain.measure_set_eq
- IsFoelner.amenable
- MeasureTheory.QuotientMeasureEqMeasurePreimage.sigmaFiniteQuotient
- MeasureTheory.IsFundamentalDomain.lintegral_eq_tsum
Ancestors0
No ancestors.