Structures · Analysis
MeasureTheory.VAddInvariantMeasure
A measure μ : Measure α is invariant under an additive action of M on α if for any
measurable set s : Set α and c : M, the measure of its preimage under fun x => c +ᵥ x is equal
to the measure of s.
- Defined in
- Mathlib.MeasureTheory.Group.Defs
- Shape
- 3 explicit arguments · adds measure_preimage_vadd
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances2
- Subtype
- AddOpposite
How is a type an instance?
Loading the hierarchy index…
Assumed by120
- MeasureTheory.measurePreserving_vadd
- MeasureTheory.measure_vadd
- AddAction.aestabilizer
- MeasureTheory.VAddInvariantMeasure.measure_preimage_vadd
- AddAction.mem_aestabilizer
- 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.measure_preimage_vadd
- MeasureTheory.measure_vadd_eq_zero_iff
- MeasureTheory.IsAddFundamentalDomain.setLIntegral_eq
- MeasureTheory.measure_preimage_vadd_le
- MeasureTheory.IsAddFundamentalDomain.restrict_restrict
- MeasureTheory.IsAddFundamentalDomain.nullMeasurableSet_vadd
- MeasureTheory.IsAddFundamentalDomain.lintegral_eq_tsum_of_ac
- MeasureTheory.IsAddFundamentalDomain.setLIntegral_eq_tsum'
- MeasureTheory.IsAddFundamentalDomain.addQuotientMeasureEqMeasurePreimage_addQuotientMeasure
- MeasureTheory.IsAddFundamentalDomain.setIntegral_eq_tsum
- MeasureTheory.IsAddFundamentalDomain.measure_ne_zero
- MeasureTheory.IsAddFundamentalDomain.setLIntegral_eq_tsum
- MeasureTheory.IsAddFundamentalDomain.addQuotientMeasureEqMeasurePreimage
- MeasureTheory.tendsto_vadd_ae
- MeasureTheory.measure_inter_neg_vadd
- MeasureTheory.IsAddFundamentalDomain.integral_eq_tsum_of_ac
- MeasureTheory.vadd_set_ae_eq
- MeasureTheory.measure_sdiff_neg_vadd
- MeasureTheory.measure_isOpen_pos_of_vaddInvariant_of_compact_ne_zero
- 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
- MeasureTheory.exists_pair_mem_lattice_not_disjoint_vadd
- MeasureTheory.IsAddFundamentalDomain.setIntegral_eq
- MeasureTheory.IsAddFundamentalDomain.measure_eq
- MeasureTheory.IsAddFundamentalDomain.vadd_of_comm
- IsAddFoelner.tendsto_meas_vadd_symmDiff_vadd
- MeasureTheory.IsAddFundamentalDomain.lintegral_eq_tsum'
- MeasureTheory.AddQuotientMeasureEqMeasurePreimage.sigmaFiniteQuotient
- DomAddAct.vadd_Lp_add
- MeasureTheory.measure_union_neg_vadd
- MeasureTheory.IsAddFundamentalDomain.lintegral_eq_tsum
- MeasureTheory.IsAddFundamentalDomain.integral_eq_tsum
- DomAddAct.norm_vadd_Lp
- MeasureTheory.IsAddFundamentalDomain.addQuotientMeasureEqMeasurePreimage_of_zero
- IsAddFoelner.mean_vadd_eq_mean_vadd
- MeasureTheory.IsAddFundamentalDomain.measure_le_of_pairwise_disjoint
- MeasureTheory.IsAddFundamentalDomain.integral_eq_tsum'
- IsAddFoelner.mean_vadd_eq_mean
Ancestors0
No ancestors.