Structures · Analysis
MeasureTheory.Measure.IsMulLeftInvariant
A measure μ on a measurable group is left invariant
if the measure of left translations of a set are equal to the measure of the set itself.
- Defined in
- Mathlib.MeasureTheory.Group.Defs
- Shape
- One type argument · adds map_mul_left_eq_self
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances1
- Prod
How is a type an instance?
Loading the hierarchy index…
Assumed by130
- MeasureTheory.Measure.haarScalarFactor
- MeasureTheory.map_mul_left_eq_self
- MeasureTheory.quasiMeasurePreserving_inv
- MeasureTheory.absolutelyContinuous_inv
- MeasureTheory.Measure.haarScalarFactor.congr_simp
- MeasureTheory.measure_preimage_mul
- MeasureTheory.lintegral_mul_left_eq_self
- MeasureTheory.Measure.haarMeasure_unique
- MeasureTheory.Measure.integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport
- MeasureTheory.Measure.measure_isMulInvariant_eq_smul_of_isCompact_closure
- MeasureTheory.measure_mul_right_null
- MeasureTheory.Measure.IsMulLeftInvariant.map_mul_left_eq_self
- MeasureTheory.integral_mul_left_eq_self
- MeasureTheory.Measure.haarScalarFactor_eq_integral_div_of_continuous_nonneg_pos
- MeasureTheory.inv_absolutelyContinuous
- MeasureTheory.Measure.exists_integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport
- MeasureTheory.measurePreserving_mul_left
- MeasureTheory.measurePreserving_prod_mul
- MeasureTheory.Measure.mconv_absolutelyContinuous
- MeasureTheory.Measure.haarScalarFactor_eq_integral_div
- MeasureTheory.quasiMeasurePreserving_inv_mul
- MeasureTheory.measure_mul_lintegral_eq
- MeasureTheory.mconv_eq_withDensity_mlconvolution_rnDeriv
- MeasureTheory.Measure.haarScalarFactor_eq_mul
- MeasureTheory.quasiMeasurePreserving_mul_right
- MeasureTheory.aemeasurable_mlconvolution
- MeasureTheory.Measure.isMulLeftInvariant_eq_smul_of_regular
- MeasureTheory.Measure.measure_preimage_isMulLeftInvariant_eq_smul_of_hasCompactSupport
- MeasureTheory.Measure.measure_isMulLeftInvariant_eq_smul_of_ne_top
- MeasureTheory.Measure.IsMulLeftInvariant.quotientMeasureEqMeasurePreimage_of_set
- MeasureTheory.Measure.isMulLeftInvariant_eq_smul_of_innerRegular
- MeasureTheory.isMulLeftInvariant_map
- MeasureTheory.QuotientMeasureEqMeasurePreimage.mulInvariantMeasure_quotient
- MeasureTheory.HaveLebesgueDecomposition.mconv
- MeasureTheory.measurePreserving_prod_mul_swap
- MeasureTheory.Measure.measurePreserving_div_left
- MeasureTheory.measurePreserving_prod_inv_mul
- MeasureTheory.measure_eq_div_smul
- MeasureTheory.measurePreserving_mul_prod_inv
- MeasureTheory.measurePreserving_prod_inv_mul_swap
- MeasureTheory.mlconvolution_assoc₀
- MeasureTheory.measure_univ_of_isMulLeftInvariant
- MeasureTheory.Measure.map_div_left_eq_self
- MeasureTheory.measure_lintegral_div_measure
- MeasureTheory.mconv_withDensity_eq_mlconvolution
- MeasureTheory.Measure.innerRegularWRT_preimage_one_hasCompactSupport_measure_ne_top_of_group
- MeasureTheory.Measure.haarScalarFactor_smul_smul
- MeasureTheory.Measure.measure_isMulInvariant_eq_smul_of_isCompact_closure_of_innerRegularCompactLTTop
- MeasureTheory.Measure.integral_isMulLeftInvariant_isMulRightInvariant_combo
- MeasureTheory.measure_ne_zero_iff_nonempty_of_isMulLeftInvariant
Ancestors0
No ancestors.