Documentation Verification Report

Indicator

📁 Source: Mathlib/MeasureTheory/Function/ConditionalExpectation/Indicator.lean

Statistics

Metric	Count
Definitions	0
Theorems `condExp_ae_eq_restrict_of_measurableSpace_eq_on`, `condExp_ae_eq_restrict_zero`, `condExp_indicator`, `condExp_indicator_aux`, `condExp_restrict_ae_eq_restrict`	5
Total	5

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`condExp_ae_eq_restrict_of_measurableSpace_eq_on` 📖	mathematical	`MeasurableSpace` `MeasurableSpace.instLE` `MeasurableSet` `Set` `Set.instInter`	`Filter.EventuallyEq` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `Measure.restrict` `condExp`	—	`Measure.instOuterMeasureClass` `ae_eq_restrict_iff_indicator_ae_eq` `Set.inter_univ` `Filter.EventuallyEq.trans` `Filter.EventuallyEq.symm` `condExp_indicator` `ae_eq_of_forall_setIntegral_eq_of_sigmaFinite'` `Integrable.integrableOn` `integrable_condExp` `integral_add_compl` `Measure.restrict_restrict` `MeasurableSet.compl` `condExp_ae_eq_restrict_zero` `indicator_ae_eq_restrict_compl` `Set.inter_comm` `setIntegral_congr_ae` `Filter.mp_mem` `Filter.univ_mem'` `integral_zero` `add_zero` `MeasurableSet.inter` `setIntegral_condExp` `Integrable.indicator` `integral_indicator` `Set.inter_self` `stronglyMeasurable_condExp` `AEStronglyMeasurable.of_measurableSpace_le_on` `StronglyMeasurable.aestronglyMeasurable` `condExp_of_not_integrable` `Filter.EventuallyEq.refl`
`condExp_ae_eq_restrict_zero` 📖	mathematical	`MeasurableSet` `Filter.EventuallyEq` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `Measure.restrict` `Pi.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	`condExp`	—	`Measure.instOuterMeasureClass` `restrict_trim` `Restrict.sigmaFinite` `ae_eq_of_forall_setIntegral_eq_of_sigmaFinite'` `Integrable.integrableOn` `integrable_condExp` `integrable_zero` `Measure.restrict_restrict` `setIntegral_condExp` `MeasurableSet.inter` `setIntegral_congr_ae` `Filter.mp_mem` `Filter.univ_mem'` `StronglyMeasurable.aestronglyMeasurable` `stronglyMeasurable_condExp` `stronglyMeasurable_zero` `condExp_of_not_integrable` `Filter.EventuallyEq.refl` `condExp_of_not_sigmaFinite` `condExp_of_not_le`
`condExp_indicator` 📖	mathematical	`Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `MeasurableSet`	`Filter.EventuallyEq` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `condExp` `Set.indicator` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`Measure.instOuterMeasureClass` `Set.indicator_self_add_compl` `Filter.EventuallyEq.refl` `Filter.EventuallyEq.symm` `Filter.EventuallyEq.trans` `Filter.mp_mem` `condExp_add` `Integrable.indicator` `MeasurableSet.compl` `Filter.univ_mem'` `Set.indicator_apply` `Set.indicator_add'` `Filter.EventuallyEq.add` `Filter.EventuallyEq.rfl` `condExp_indicator_aux` `indicator_ae_eq_restrict_compl` `Set.indicator_indicator` `Set.inter_self` `Set.indicator_of_mem` `Set.indicator_of_notMem` `Set.inter_compl_self` `Set.indicator_empty'` `add_zero` `condExp_of_not_sigmaFinite` `Set.indicator_zero'` `condExp_of_not_le`
`condExp_indicator_aux` 📖	mathematical	`MeasurableSet` `Filter.EventuallyEq` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `Measure.restrict` `Compl.compl` `Set` `Set.instCompl` `Pi.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	`condExp` `Set.indicator`	—	`Measure.instOuterMeasureClass` `indicator_ae_eq_of_restrict_compl_ae_eq_zero` `Filter.EventuallyEq.symm` `Filter.EventuallyEq.trans` `condExp_ae_eq_restrict_zero` `MeasurableSet.compl` `condExp_congr_ae` `condExp_of_not_le` `Set.indicator_zero'` `Filter.EventuallyEq.refl`
`condExp_restrict_ae_eq_restrict` 📖	mathematical	`MeasurableSpace` `MeasurableSpace.instLE` `MeasurableSet` `Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`Filter.EventuallyEq` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `Measure.restrict` `condExp`	—	`restrict_trim` `Restrict.sigmaFinite` `Measure.instOuterMeasureClass` `ae_eq_restrict_iff_indicator_ae_eq` `Filter.EventuallyEq.trans` `ae_eq_condExp_of_forall_setIntegral_eq` `Integrable.indicator` `integrable_indicator_iff` `Set.indicator_indicator` `Set.inter_comm` `integrable_condExp` `IntegrableOn.eq_1` `integral_indicator` `Measure.restrict_restrict` `setIntegral_condExp` `Integrable.integrableOn` `StronglyMeasurable.aestronglyMeasurable` `StronglyMeasurable.indicator` `stronglyMeasurable_condExp` `condExp_indicator`

---

← Back to Index