Structures · Analysis
MeasureTheory.AddQuotientMeasureEqMeasurePreimage
A measure μ on the AddQuotient of α mod G satisfies
AddQuotientMeasureEqMeasurePreimage if: for any fundamental domain t, and any measurable
subset U of the quotient, μ U = volume ((π ⁻¹' U) ∩ t).
- Shape
- 2 explicit arguments · adds addProjection_respects_measure'
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- Subtype
How is a type an instance?
Loading the hierarchy index…
Assumed by13
- MeasureTheory.IsAddFundamentalDomain.addProjection_respects_measure_apply
- MeasureTheory.IsAddFundamentalDomain.addProjection_respects_measure
- MeasureTheory.AddQuotientMeasureEqMeasurePreimage.addInvariantMeasure_quotient
- MeasureTheory.AddQuotientMeasureEqMeasurePreimage.addProjection_respects_measure'
- MeasureTheory.AddQuotientMeasureEqMeasurePreimage.sigmaFiniteQuotient
- measurePreserving_quotientAddGroup_mk_of_AddQuotientMeasureEqMeasurePreimage
- MeasureTheory.IsAddFundamentalDomain.measurePreserving_add_quotient_mk
- MeasureTheory.AddQuotientMeasureEqMeasurePreimage.covolume_ne_top
- MeasureTheory.instSigmaFiniteAddQuotientOrbitRelInstMeasurableSpaceToMeasurableSpace
- MeasureTheory.AddQuotientMeasureEqMeasurePreimage.vaddInvariantMeasure_quotient
- MeasureTheory.AddQuotientMeasureEqMeasurePreimage.addHaarMeasure_quotient
- MeasureTheory.AddQuotientMeasureEqMeasurePreimage.isFiniteMeasure_quotient
- MeasureTheory.AddQuotientMeasureEqMeasurePreimage.unique
Ancestors0
No ancestors.