Structures · Analysis
MeasureTheory.IsZeroOrProbabilityMeasure
A measure μ is zero or a probability measure if μ univ = 0 or μ univ = 1. This class
of measures appears naturally when conditioning on events, and many results which are true for
probability measures hold more generally over this class.
- Shape
- One type argument · adds measure_univ
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by2
Forgetful instances
Every MeasureTheory.IsZeroOrProbabilityMeasure is also a
Provided automatically by
Concrete types that are instances1
- Prod
How is a type an instance?
Loading the hierarchy index…
Assumed by53
- MeasureTheory.prob_le_one
- MeasureTheory.eq_zero_or_isProbabilityMeasure
- MeasureTheory.IsZeroOrProbabilityMeasure.measure_univ
- ProbabilityTheory.IndepFun.indepFun_process₀
- ProbabilityTheory.IndepFun.process_indepFun_process₀
- ProbabilityTheory.IndepFun.process_indepFun₀
- ProbabilityTheory.HasSubgaussianMGF.sum_of_hasCondSubgaussianMGF
- ProbabilityTheory.cgf_zero
- ProbabilityTheory.exists_cgf_eq_iteratedDeriv_two_cgf_mul
- ProbabilityTheory.measure_sum_ge_le_of_hasCondSubgaussianMGF
- MeasureTheory.one_le_prob_iff
- MeasureTheory.measureReal_le_one
- ProbabilityTheory.HasSubgaussianMGF.fun_zero
- ProbabilityTheory.indep_bot_right
- ProbabilityTheory.indepSet_iff_indepSets_singleton
- ProbabilityTheory.HasSubgaussianMGF.zero
- MeasureTheory.instIsZeroOrProbabilityMeasureMap
- MeasureTheory.Measure.instIsZeroOrProbabilityMeasureBindCoeKernelOfIsZeroOrMarkovKernel
- ProbabilityTheory.indep_iSup_of_monotone
- MeasureTheory.Measure.snd.instIsZeroOrProbabilityMeasure
- ProbabilityTheory.IndepFun.process_indepFun_process
- process_indepFun_process_of_bcf
- ProbabilityTheory.indepSet_empty_left
- ProbabilityTheory.measure_sum_ge_le_of_HasCondSubgaussianMGF
- MeasureTheory.prob_compl_lt_one_sub_of_lt_prob
- ProbabilityTheory.indep_iSup_of_directed_le
- ProbabilityTheory.indepFun_iff_indepSet_preimage
- MeasureTheory.inv_measure_univ_smul_eq_self
- ProbabilityTheory.indepFun_const_right
- indepFun_process_of_prod_bcf
- ProbabilityTheory.IndepFun.process_indepFun
- ProbabilityTheory.HasSubgaussianMGF_sum_of_HasCondSubgaussianMGF
- MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure
- MeasureTheory.Measure.instIsZeroOrProbabilityMeasureProdCompProdOfIsZeroOrMarkovKernel
- ProbabilityTheory.indep_bot_left
- ProbabilityTheory.Kernel.const.instIsZeroOrMarkovKernel
- ProbabilityTheory.indepSet_iff_measure_inter_eq_mul
- ProbabilityTheory.IndepFun.indepFun_process
- process_indepFun_of_bcf
- ProbabilityTheory.IndepSets.indep'
- ProbabilityTheory.IndepSets.indepSet_of_mem
- process_indepFun_of_prod_bcf
- ProbabilityTheory.indep_iSup_of_antitone
- ProbabilityTheory.centralMoment_one
- process_indepFun_process_of_prod_bcf
- ProbabilityTheory.indepSet_empty_right
- MeasureTheory.Measure.fst.instIsZeroOrProbabilityMeasure
- ProbabilityTheory.variance_of_ae_eq_zero_or_one
- indepFun_process_of_bcf
- ProbabilityTheory.IndepSets.indep