Structures · Analysis
MeasureTheory.Measure.IsAddRightInvariant
A measure μ on a measurable additive group is right invariant
if the measure of right 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_right_eq_self
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- Prod
How is a type an instance?
Loading the hierarchy index…
Assumed by65
- MeasureTheory.map_add_right_eq_self
- MeasureTheory.integral_add_right_eq_self
- MeasureTheory.quasiMeasurePreserving_sub_left_of_right_invariant
- MeasureTheory.integral_sub_right_eq_self
- MeasureTheory.Integrable.convolution_integrand
- MeasureTheory.Integrable.comp_sub_right
- MeasureTheory.measure_preimage_add_right
- MeasureTheory.Measure.IsAddRightInvariant.map_add_right_eq_self
- MeasureTheory.Measure.IsAddLeftInvariant.addQuotientMeasureEqMeasurePreimage_of_set
- MeasureTheory.measurePreserving_add_right
- MeasureTheory.measurePreserving_prod_add_right
- MeasureTheory.Integrable.comp_add_right
- MeasureTheory.measurePreserving_prod_sub_swap
- MeasureTheory.lintegral_add_right_eq_self
- MeasureTheory.measurePreserving_prod_add_swap_right
- MeasureTheory.AEStronglyMeasurable.convolution_integrand
- MeasureTheory.quasiMeasurePreserving_sub_of_right_invariant
- IsFundamentalDomain.AddQuotientMeasureEqMeasurePreimage_AddHaarMeasure
- MeasureTheory.map_add_right_ae
- MeasureTheory.integral_posConvolution
- MeasureTheory.map_sub_right_ae
- essSup_comp_quotientAddGroup_mk
- MeasureTheory.IsAddFundamentalDomain.absolutelyContinuous_map
- MeasureTheory.Integrable.integrable_convolution
- MeasureTheory.integral_eq_zero_of_add_right_eq_neg
- MeasureTheory.measurePreserving_sub_prod
- MeasureTheory.measurePreserving_prod_sub
- MeasureTheory.Measure.integral_isAddLeftInvariant_isAddRightInvariant_combo
- MeasureTheory.quasiMeasurePreserving_add_left
- VectorFourier.fourierIntegral_comp_add_right
- MeasureTheory.ConvolutionExistsAt.of_norm
- QuotientAddGroup.integral_eq_integral_automorphize
- MeasureTheory.quasiMeasurePreserving_neg_of_right_invariant
- MeasureTheory.measurePreserving_sub_right
- MeasureTheory.convolution_assoc'
- MeasureTheory.AEStronglyMeasurable.convolution_integrand_snd
- MeasureTheory.integral_convolution
- MeasureTheory.map_sub_right_eq_self
- MeasureTheory.eventually_add_right_iff
- QuotientAddGroup.integral_mul_eq_integral_automorphize_mul
- MeasureTheory.integrable_posConvolution
- instErgodicVAddAddOppositeOfIsAddRightInvariant
- MeasureTheory.AddQuotientMeasureEqMeasurePreimage.addHaarMeasure_quotient
- MeasureTheory.Measure.IsAddRightInvariant.toVAddInvariantMeasure_op
- MeasureTheory.AEStronglyMeasurable.convolution_integrand_swap_snd
- MeasureTheory.measurePreserving_add_prod
- MeasureTheory.lintegral_sub_right_eq_self
- MeasureTheory.convolution_congr
- Fourier.fourierIntegral_comp_add_right
- MeasureTheory.Measure.instIsAddRightInvariantForallVolumeOfMeasurableAddOfSigmaFinite
Ancestors0
No ancestors.