Structures · Analysis
MeasureTheory.Measure.IsAddLeftInvariant
A measure μ on a measurable additive 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_add_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 by154
- MeasureTheory.Measure.addHaarScalarFactor
- MeasureTheory.measure_preimage_add
- MeasureTheory.Measure.addHaarMeasure_unique
- MeasureTheory.map_add_left_eq_self
- MeasureTheory.Measure.isAddLeftInvariant_eq_smul
- MeasureTheory.quasiMeasurePreserving_neg
- MeasureTheory.Measure.addHaarScalarFactor_eq_mul
- MeasureTheory.convolution_flip
- MeasureTheory.integral_add_left_eq_self
- MeasureTheory.measurePreserving_add_left
- MeasureTheory.absolutelyContinuous_neg
- Module.Basis.addHaar_eq_iff
- MeasureTheory.neg_absolutelyContinuous
- MeasureTheory.Measure.isAddLeftInvariant_eq_smul_of_regular
- MeasureTheory.Measure.measure_isAddInvariant_eq_smul_of_isCompact_closure
- MeasureTheory.Measure.exists_integral_isAddLeftInvariant_eq_smul_of_hasCompactSupport
- MeasureTheory.measure_add_right_null
- MeasureTheory.Measure.integral_isAddLeftInvariant_eq_smul_of_hasCompactSupport
- MeasureTheory.Measure.addHaarScalarFactor_eq_integral_div_of_continuous_nonneg_pos
- MeasureTheory.lintegral_add_left_eq_self
- MeasureTheory.Measure.IsAddLeftInvariant.map_add_left_eq_self
- MeasureTheory.Measure.addHaarScalarFactor_eq_integral_div
- MeasureTheory.convolution_eq_swap
- MeasureTheory.Measure.conv_absolutelyContinuous
- MeasureTheory.Measure.measurePreserving_sub_left
- MeasureTheory.aemeasurable_lconvolution
- MeasureTheory.quasiMeasurePreserving_add_right
- MeasureTheory.measure_add_lintegral_eq
- MeasureTheory.conv_eq_withDensity_lconvolution_rnDeriv
- MeasureTheory.measurePreserving_prod_add
- MeasureTheory.quasiMeasurePreserving_neg_add
- MeasureTheory.convolutionExistsAt_flip
- MeasureTheory.measure_univ_of_isAddLeftInvariant
- MeasureTheory.HaveLebesgueDecomposition.conv
- MeasureTheory.measure_eq_sub_vadd
- MeasureTheory.Measure.IsAddLeftInvariant.addQuotientMeasureEqMeasurePreimage_of_set
- MeasureTheory.measurePreserving_add_prod_neg
- MeasureTheory.Measure.measure_isAddLeftInvariant_eq_vadd_of_ne_top
- MeasureTheory.measurePreserving_prod_neg_add
- MeasureTheory.dist_convolution_le
- MeasureTheory.Measure.addHaarScalarFactor.congr_simp
- MeasureTheory.Integrable.comp_add_left
- MeasureTheory.measurePreserving_prod_neg_add_swap
- MeasureTheory.AddQuotientMeasureEqMeasurePreimage.addInvariantMeasure_quotient
- MeasureTheory.Measure.measure_preimage_isAddLeftInvariant_eq_smul_of_hasCompactSupport
- MeasureTheory.Integrable.comp_sub_left
- MeasureTheory.measure_neg_null
- MeasureTheory.isAddLeftInvariant_map
- MeasureTheory.contDiffOn_convolution_left_with_param
- MeasureTheory.Measure.isAddLeftInvariant_eq_smul_of_innerRegular
Ancestors0
No ancestors.