Structures · Analysis
MeasureTheory.MeasureSpace
A measure space is a measurable space equipped with a
measure, referred to as volume.
- Shape
- One type argument · adds volume
Extends1
Extended by0
Nothing extends this class yet.
Concrete types that are instances6
- Real
- AddCircle
- UpperHalfPlane
- Prod
- Set.Elem
- PUnit
How is a type an instance?
Loading the hierarchy index…
Assumed by81
- MeasureTheory.MeasureSpace.volume
- MeasureTheory.Measure.volume_eq_prod
- MeasureTheory.Measure.Subtype.measureSpace
- MeasureTheory.volume_pi
- MeasureTheory.volume_pi_pi
- MeasureTheory.volume_preserving_pi
- MeasureTheory.volume_preserving_funUnique
- MeasureTheory.integral_fintype_prod_volume_eq_pow
- volume_set_coe_def
- MeasureTheory.integral_fintype_prod_volume_eq_prod
- MeasureTheory.volume_preserving_finTwoArrow
- MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable_of_equiv
- ProbabilityTheory.strong_law_aux2
- MeasureTheory.volume_preserving_arrowCongr'
- MeasureTheory.integral_subtype
- MeasureTheory.volume_preserving_piEquivPiSubtypeProd
- MeasureTheory.volume_preserving_piFinTwo
- ProbabilityTheory.sum_prob_mem_Ioc_le
- MeasureTheory.volume_preserving_piFinSuccAbove
- volume_image_subtype_coe
- MeasureTheory.volume_measurePreserving_arrowProdEquivProdArrow
- ProbabilityTheory.strong_law_aux7
- ProbabilityTheory.strong_law_aux5
- MeasureTheory.Measure.volume_pi_eq_dirac
- MeasureTheory.volume_pi_closedBall
- ProbabilityTheory.strong_law_aux3
- MeasureTheory.volume_preserving_prodAssoc
- ProbabilityTheory.tsum_prob_mem_Ioi_lt_top
- ProbabilityTheory.strong_law_aux4
- MeasureTheory.volume_pi_ball
- ProbabilityTheory.sum_variance_truncation_le
- MeasureTheory.Measure.Subtype.volume_def
- ProbabilityTheory.strong_law_aux1
- ProbabilityTheory.strong_law_aux6
- MeasureTheory.Measure.IsUnifLocDoublingMeasure.volume_pi
- MeasureTheory.instSigmaFiniteAddQuotientOrbitRelInstMeasurableSpaceToMeasurableSpace
- MeasureTheory.Measure.instSigmaFiniteProdVolume
- MeasureTheory.Measure.Subtype.volume_univ
- MeasureTheory.Measure.instIsOpenPosMeasureForallVolumeOfSigmaFinite
- MeasureTheory.Measure.volume_subtype_coe_eq_zero_of_volume_eq_zero
- MeasureTheory.Pi.isNegInvariant_volume
- MeasureTheory.Measure.instNullSingletonClassForallVolumeOfNonemptyOfSigmaFinite
- MeasureTheory.instSigmaFiniteQuotientOrbitRelOfHasFundamentalDomainOfQuotientMeasureEqMeasurePreimageVolume
- MeasureTheory.Measure.instSFiniteProdVolume
- MeasureTheory.integral_fin_nat_prod_volume_eq_prod
- MeasureTheory.MeasureSpace.toMeasurableSpace
- MeasureTheory.Measure.IsUnifLocDoublingMeasure.volume_prod
- MeasureTheory.Pi.isAddLeftInvariant_volume
- MeasureTheory.Pi.isMulLeftInvariant_volume
- MeasureTheory.Measure.instIsAddRightInvariantForallVolumeOfMeasurableAddOfSigmaFinite