Structures · Analysis
MeasurableConstVAdd
We say that the action of M on α has MeasurableConstVAdd 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_vadd
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances3
- AddUnits
- Subtype
- AddOpposite
How is a type an instance?
Loading the hierarchy index…
Assumed by95
- MeasureTheory.measurePreserving_vadd
- MeasurableConstVAdd.measurable_const_vadd
- measurableEmbedding_const_vadd
- MeasurableEquiv.vadd
- MeasureTheory.NullMeasurableSet.vadd
- MeasureTheory.IsAddFundamentalDomain.covolume_eq_volume
- MeasureTheory.IsAddFundamentalDomain.measure_eq_tsum
- MeasureTheory.IsAddFundamentalDomain.sum_restrict_of_ac
- MeasureTheory.IsAddFundamentalDomain.measure_zero_of_invariant
- MeasureTheory.IsAddFundamentalDomain.setLIntegral_eq
- MeasureTheory.IsAddFundamentalDomain.restrict_restrict
- MeasureTheory.IsAddFundamentalDomain.nullMeasurableSet_vadd
- MeasureTheory.IsAddFundamentalDomain.lintegral_eq_tsum_of_ac
- MeasurableSet.const_vadd
- MeasureTheory.IsAddFundamentalDomain.setLIntegral_eq_tsum'
- MeasureTheory.IsAddFundamentalDomain.addQuotientMeasureEqMeasurePreimage_addQuotientMeasure
- AEMeasurable.const_vadd
- MeasureTheory.IsAddFundamentalDomain.setIntegral_eq_tsum
- MeasureTheory.IsAddFundamentalDomain.setLIntegral_eq_tsum
- MeasureTheory.IsAddFundamentalDomain.addQuotientMeasureEqMeasurePreimage
- Measurable.const_vadd
- MeasureTheory.IsAddFundamentalDomain.integral_eq_tsum_of_ac
- MeasureTheory.IsAddFundamentalDomain.measure_eq_tsum_of_ac
- MeasureTheory.IsAddFundamentalDomain.measure_eq_card_smul_of_vadd_ae_eq_self
- MeasureTheory.IsAddFundamentalDomain.measure_set_eq
- MeasureTheory.IsAddFundamentalDomain.hasFiniteIntegral_on_iff
- aemeasurable_const_vadd_iff
- MeasureTheory.IsAddFundamentalDomain.setIntegral_eq
- MeasureTheory.IsAddFundamentalDomain.measure_eq
- MeasureTheory.IsAddFundamentalDomain.vadd_of_comm
- MeasureTheory.IsAddFundamentalDomain.lintegral_eq_tsum'
- MeasureTheory.AddQuotientMeasureEqMeasurePreimage.sigmaFiniteQuotient
- DomAddAct.vadd_Lp_add
- MeasureTheory.IsAddFundamentalDomain.lintegral_eq_tsum
- MeasureTheory.IsAddFundamentalDomain.integral_eq_tsum
- DomAddAct.norm_vadd_Lp
- MeasureTheory.IsAddFundamentalDomain.addQuotientMeasureEqMeasurePreimage_of_zero
- MeasureTheory.IsAddFundamentalDomain.measure_le_of_pairwise_disjoint
- MeasureTheory.IsAddFundamentalDomain.integral_eq_tsum'
- measurable_const_vadd_iff
- MeasureTheory.IsAddFundamentalDomain.lintegral_eq_tsum''
- MeasureTheory.IsAddFundamentalDomain.essSup_measure_restrict
- MeasureTheory.IsAddFundamentalDomain.aestronglyMeasurable_on_iff
- MeasureTheory.map_vadd
- MeasureTheory.IsAddFundamentalDomain.addQuotientMeasure_eq
- DomAddAct.dist_vadd_Lp
- MeasureTheory.IsAddFundamentalDomain.integrableOn_iff
- DomAddAct.vadd_Lp_neg
- MeasureTheory.IsAddFundamentalDomain.integral_eq_tsum''
- MeasureTheory.IsAddFundamentalDomain.setIntegral_eq_tsum'
Ancestors0
No ancestors.