Structures · Analysis
MeasureTheory.IsProbabilityMeasure
A measure μ is called a probability measure if μ univ = 1.
- Shape
- One type argument · adds measure_univ
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Forgetful instances
Every MeasureTheory.IsProbabilityMeasure is also a
Concrete types that are instances8
- Nat
- Real
- SimpleGraph
- AddCircle
- Prod
- Set.Elem
- ULift
- Set
How is a type an instance?
Loading the hierarchy index…
Assumed by313
- MeasureTheory.IsProbabilityMeasure.measure_univ
- MeasureTheory.probReal_univ
- MeasureTheory.Measure.isProbabilityMeasure_map
- MeasureTheory.IsProbabilityMeasure.ne_zero
- MeasureTheory.average_eq_integral
- MeasureTheory.piContent
- MeasureTheory.Measure.infinitePi_pi
- MeasureTheory.Measure.toPMF
- MeasureTheory.laverage_eq_lintegral
- MeasureTheory.Measure.eq_infinitePi
- ProbabilityTheory.iIndepFun_iff_map_fun_eq_pi_map
- ProbabilityTheory.cdf_eq_real
- MeasureTheory.TendstoInDistribution.tendsto
- MeasureTheory.measurePreserving_eval
- MeasureTheory.TendstoInDistribution.aemeasurable_limit
- ProbabilityTheory.iIndepFun_iff_map_fun_eq_infinitePi_map
- MeasureTheory.TendstoInDistribution.forall_aemeasurable
- MeasureTheory.Measure.infinitePiNat
- MeasureTheory.piContent_cylinder
- MeasureTheory.Measure.infinitePi_map_restrict
- MeasureTheory.Measure.infinitePi_map_eval
- MeasureTheory.isProjectiveMeasureFamily_pi
- ProbabilityTheory.variance_eq_sub
- MeasureTheory.nonempty_of_isProbabilityMeasure
- MeasureTheory.prob_compl_eq_one_sub
- MeasureTheory.measurePreserving_fst
- ProbabilityTheory.iIndepFun_iff_map_fun_eq_infinitePi_map₀
- MeasureTheory.measurePreserving_snd
- indicator_indepFun_pi_of_prod_bcf
- MeasureTheory.Measure.fst_prod
- MeasureTheory.prob_compl_eq_zero_iff
- ProbabilityTheory.indepFun_prod
- Measurable.measure_of_isPiSystem_of_isProbabilityMeasure
- MeasureTheory.lintegral_eq_const
- ProbabilityTheory.mgf_pos
- ProbabilityTheory.covariance_add_const_left
- MeasureTheory.TendstoInDistribution.continuous_comp
- ProbabilityTheory.iIndepFun_infinitePi
- MeasureTheory.Measure.isProjectiveLimit_infinitePi
- MeasureTheory.le_measure_liminf_of_limsup_measure_compl_le
- MeasureTheory.ae_iff_prob_eq_one
- MeasureTheory.measureReal_abs_gt_le_integral_charFun
- MeasureTheory.prob_compl_eq_one_sub₀
- ProbabilityTheory.iIndepFun_pi
- ProbabilityTheory.variance_add_const
- ProbabilityTheory.indepFun_prod₀
- BoundedContinuousFunction.isBounded_range_integral
- MeasureTheory.Measure.infinitePiNat_map_restrict
- MeasureTheory.Measure.isProbabilityMeasure_of_map
- MeasureTheory.Measure.infinitePi_map_piCurry_symm