Documentation Verification Report

TwoValued

📁 Source: Mathlib/Probability/Distributions/TwoValued.lean

Statistics

Metric	Count
Definitions	0
Theorems `integral_of_ae_eq_zero_or_one`, `integral_one_sub_of_ae_eq_zero_or_one`, `condVar_of_ae_eq_zero_or_one`, `variance_of_ae_eq_zero_or_one`	4
Total	4

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`integral_of_ae_eq_zero_or_one` 📖	mathematical	`AEMeasurable` `Real` `Real.measurableSpace` `Filter.Eventually` `Real.instZero` `Real.instOne` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass`	`integral` `Real` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Measure.real` `setOf` `Real.instOne`	—	`Measure.instOuterMeasureClass` `integral_map` `aestronglyMeasurable_id` `PseudoEMetricSpace.pseudoMetrizableSpace` `BorelSpace.opensMeasurable` `Real.borelSpace` `instSecondCountableTopologyReal` `IsScalarTower.right` `Measure.ae_eq_or_eq_iff_map_eq_dirac_add_dirac` `instMeasurableSingletonClassOfMeasurableEq` `instMeasurableEqOfSecondCountableTopologyOfT2Space` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `zero_ne_one` `NeZero.charZero_one` `RCLike.charZero_rclike` `integral_undef` `lintegral_add_measure` `lintegral_smul_measure` `lintegral_dirac` `enorm_zero` `MulZeroClass.mul_zero` `enorm_one` `NormedDivisionRing.to_normOneClass` `mul_one` `add_top` `integral_add_measure` `Integrable.smul_measure` `integral_smul_measure` `integral_dirac` `Real.instCompleteSpace` `zero_add`
`integral_one_sub_of_ae_eq_zero_or_one` 📖	mathematical	`AEMeasurable` `Real` `Real.measurableSpace` `Filter.Eventually` `Real.instZero` `Real.instOne` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass`	`integral` `Real` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Real.instSub` `Real.instOne` `Measure.real` `setOf` `Real.instZero`	—	`Measure.instOuterMeasureClass` `integral_of_ae_eq_zero_or_one` `AEMeasurable.sub` `ContinuousSub.measurableSub₂` `Real.borelSpace` `instSecondCountableTopologyReal` `IsTopologicalAddGroup.to_continuousSub` `instIsTopologicalAddGroupReal` `aemeasurable_const`

ProbabilityTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`condVar_of_ae_eq_zero_or_one` 📖	mathematical	`MeasurableSpace` `MeasurableSpace.instLE` `AEMeasurable` `Real` `Real.measurableSpace` `Filter.Eventually` `Real.instZero` `Real.instOne` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	`Filter.EventuallyEq` `Real` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `condVar` `Pi.instMul` `Real.instMul` `MeasureTheory.condExp` `Real.normedAddCommGroup` `Real.instCompleteSpace` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Pi.instSub` `Real.instSub` `Pi.instOne` `Real.instOne`	—	`MeasureTheory.Measure.instOuterMeasureClass` `Real.instCompleteSpace` `condVar_ae_eq_condExp_sq_sub_sq_condExp` `MeasureTheory.MemLp.of_bound` `Nat.instAtLeastTwoHAddOfNat` `Measurable.aestronglyMeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `instSecondCountableTopologyReal` `BorelSpace.opensMeasurable` `Real.borelSpace` `Filter.mp_mem` `Filter.univ_mem'` `norm_zero` `Real.instZeroLEOneClass` `CStarRing.norm_of_mem_unitary` `instCStarRingReal` `Real.instNontrivial` `SubmonoidClass.toOneMemClass` `Submonoid.instSubmonoidClass` `instReflLe` `Filter.EventuallyEq.sub` `MeasureTheory.condExp_congr_ae` `zero_pow` `Nat.instCharZero` `one_pow` `MeasureTheory.ae_eq_rfl` `sq` `one_sub_mul` `mul_comm` `Filter.EventuallyEq.mul` `MeasureTheory.condExp_const` `Filter.EventuallyEq.symm` `MeasureTheory.condExp_sub` `MeasureTheory.integrable_const` `MeasureTheory.Integrable.of_bound` `condVar_congr_ae` `Measurable.aemeasurable`
`variance_of_ae_eq_zero_or_one` 📖	mathematical	`AEMeasurable` `Real` `Real.measurableSpace` `Filter.Eventually` `Real.instZero` `Real.instOne` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	`variance` `Real` `Real.instMul` `MeasureTheory.Measure.real` `setOf` `Real.instZero` `Real.instOne`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.eq_zero_or_isProbabilityMeasure` `variance_zero_measure` `MulZeroClass.mul_zero` `Real.instCompleteSpace` `condVar_bot` `MeasureTheory.condExp_bot` `MeasureTheory.integral_of_ae_eq_zero_or_one` `MeasureTheory.integral_one_sub_of_ae_eq_zero_or_one` `mul_comm` `MeasureTheory.Measure.ae.neBot` `MeasureTheory.IsProbabilityMeasure.neZero` `condVar_of_ae_eq_zero_or_one` `bot_le` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure`

---

← Back to Index