Structures · Analysis
MeasureTheory.QuotientMeasureEqMeasurePreimage
Measures ν on α and μ on the Quotient of α mod G satisfy
QuotientMeasureEqMeasurePreimage if: for any fundamental domain t, and any measurable subset
U of the quotient, μ U = ν ((π ⁻¹' U) ∩ t).
- Shape
- 2 explicit arguments · adds projection_respects_measure'
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by13
- MeasureTheory.IsFundamentalDomain.projection_respects_measure
- MeasureTheory.IsFundamentalDomain.projection_respects_measure_apply
- MeasureTheory.QuotientMeasureEqMeasurePreimage.mulInvariantMeasure_quotient
- MeasureTheory.QuotientMeasureEqMeasurePreimage.covolume_ne_top
- MeasureTheory.QuotientMeasureEqMeasurePreimage.projection_respects_measure'
- MeasureTheory.QuotientMeasureEqMeasurePreimage.sigmaFiniteQuotient
- MeasureTheory.IsFundamentalDomain.measurePreserving_quotient_mk
- measurePreserving_quotientGroup_mk_of_QuotientMeasureEqMeasurePreimage
- MeasureTheory.QuotientMeasureEqMeasurePreimage.unique
- MeasureTheory.instSigmaFiniteQuotientOrbitRelOfHasFundamentalDomainOfQuotientMeasureEqMeasurePreimageVolume
- MeasureTheory.QuotientMeasureEqMeasurePreimage.isFiniteMeasure_quotient
- MeasureTheory.QuotientMeasureEqMeasurePreimage.haarMeasure_quotient
- MeasureTheory.QuotientMeasureEqMeasurePreimage.smulInvariantMeasure_quotient
Ancestors0
No ancestors.