Structures · Analysis
MeasurableConstSMul
We say that the action of M on α has MeasurableConstSMul if for each c the map
x ↦ c • x is a measurable function.
- Defined in
- Mathlib.MeasureTheory.Group.Arithmetic
- Shape
- 2 explicit arguments · adds measurable_const_smul
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances3
- Units
- Subtype
- MulOpposite
How is a type an instance?
Loading the hierarchy index…
Assumed by121
- MeasureTheory.measurePreserving_smul
- MeasurableConstSMul.measurable_const_smul
- AEMeasurable.const_smul
- MeasurableEquiv.smul
- measurableEmbedding_const_smul
- Measurable.const_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.IsFundamentalDomain.lintegral_eq_tsum_of_ac
- MeasureTheory.IsFundamentalDomain.nullMeasurableSet_smul
- MeasureTheory.IsFundamentalDomain.setLIntegral_eq
- MeasurableEquiv.smul₀
- MeasureTheory.IsFundamentalDomain.restrict_restrict
- MeasureTheory.IsFundamentalDomain.integral_eq_tsum_of_ac
- MeasureTheory.IsFundamentalDomain.quotientMeasureEqMeasurePreimage_quotientMeasure
- MeasurableSet.const_smul
- AEMeasurable.fun_const_smul
- MeasureTheory.IsFundamentalDomain.quotientMeasureEqMeasurePreimage
- MeasureTheory.IsFundamentalDomain.setIntegral_eq_tsum
- MeasureTheory.IsFundamentalDomain.setLIntegral_eq_tsum'
- MeasureTheory.IsFundamentalDomain.setLIntegral_eq_tsum
- MeasurableSet.const_smul_of_ne_zero
- IsUnit.aemeasurable_const_smul_iff
- MeasureTheory.QuotientMeasureEqMeasurePreimage.covolume_ne_top
- MeasureTheory.IsFundamentalDomain.integral_eq_tsum''
- aemeasurable_const_smul_iff
- IsUnit.measurable_const_smul_iff
- MeasureTheory.IsFundamentalDomain.lintegral_eq_tsum'
- measurable_const_smul_iff
- 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.IsFundamentalDomain.smul_of_comm
- MeasureTheory.Measure.domSMul_apply
- MeasureTheory.IsFundamentalDomain.measure_eq_tsum_of_ac
- MeasureTheory.IsFundamentalDomain.hasFiniteIntegral_on_iff
- MeasureTheory.integral_domSMul
- MeasureTheory.IsFundamentalDomain.integrableOn_iff
- MeasureTheory.NullMeasurableSet.fundamentalInterior
- MeasurableSet.const_smul₀
- DomMulAct.dist_smul_Lp
- MeasureTheory.IsFundamentalDomain.measure_set_eq
- MeasureTheory.QuotientMeasureEqMeasurePreimage.sigmaFiniteQuotient
- MeasureTheory.IsFundamentalDomain.lintegral_eq_tsum
- MeasureTheory.IsFundamentalDomain.quotientMeasure_eq
Ancestors0
No ancestors.