Documentation Verification Report

Unique

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

Statistics

Metric	Count
Definitions	0
Theorems `ae_eq_of_forall_setIntegral_eq'`, `ae_eq_zero_of_forall_setIntegral_eq_zero'`, `ae_eq_of_forall_setIntegral_eq_of_sigmaFinite'`, `integral_norm_le_of_forall_fin_meas_integral_eq`, `lintegral_enorm_le_of_forall_fin_meas_integral_eq`, `ae_eq_zero_of_forall_setIntegral_eq_zero`	6
Total	6

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ae_eq_of_forall_setIntegral_eq_of_sigmaFinite'` 📖	mathematical	`MeasurableSpace` `MeasurableSpace.instLE` `IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `integral` `Measure.restrict` `AEStronglyMeasurable`	`Filter.EventuallyEq` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass`	—	`Measure.instOuterMeasureClass` `ae_eq_trim_iff_of_aestronglyMeasurable` `EMetricSpace.metrizableSpace` `IntegrableOn.eq_1` `restrict_trim` `Integrable.trim` `Integrable.congr` `trim_measurableSet_eq` `ae_restrict_of_ae` `integral_trim` `integral_congr_ae` `Filter.EventuallyEq.symm` `ae_eq_of_forall_setIntegral_eq_of_sigmaFinite`
`integral_norm_le_of_forall_fin_meas_integral_eq` 📖	mathematical	`MeasurableSpace` `MeasurableSpace.instLE` `StronglyMeasurable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `IntegrableOn` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Measure.restrict` `MeasurableSet`	`Real.instLE` `Norm.norm` `Real.norm`	—	`integral_norm_eq_pos_sub_neg` `StronglyMeasurable.measurableSet_le` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `PseudoEMetricSpace.pseudoMetrizableSpace` `stronglyMeasurable_const` `sub_le_sub` `IsOrderedAddMonoid.toAddLeftMono` `Measure.restrict_restrict` `MeasurableSet.inter` `LE.le.trans_lt` `measure_mono` `Measure.instOuterMeasureClass` `Set.inter_subset_right` `lt_top_iff_ne_top` `setIntegral_le_nonneg` `setIntegral_nonpos_le`
`lintegral_enorm_le_of_forall_fin_meas_integral_eq` 📖	mathematical	`MeasurableSpace` `MeasurableSpace.instLE` `StronglyMeasurable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `IntegrableOn` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Measure.restrict` `MeasurableSet`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `lintegral` `ENorm.enorm` `ContinuousENorm.toENorm` `SeminormedAddGroup.toPseudoMetricSpace`	—	`ofReal_integral_norm_eq_lintegral_enorm` `ENNReal.ofReal_le_ofReal_iff` `integral_nonneg` `Real.instIsOrderedAddMonoid` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `Real.instIsStrictOrderedRing` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `norm_nonneg` `integral_norm_le_of_forall_fin_meas_integral_eq`

MeasureTheory.Lp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ae_eq_of_forall_setIntegral_eq'` 📖	mathematical	`MeasurableSpace` `MeasurableSpace.instLE` `MeasureTheory.IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `MeasureTheory.AEEqFun.cast` `MeasureTheory.AEEqFun` `AddSubgroup` `MeasureTheory.AEEqFun.instAddGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `MeasureTheory.Lp` `MeasureTheory.integral` `MeasureTheory.Measure.restrict` `MeasureTheory.AEStronglyMeasurable`	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.integral_congr_ae` `MeasureTheory.ae_restrict_of_ae` `coeFn_sub` `MeasureTheory.integral_sub'` `sub_eq_zero` `MeasureTheory.IntegrableOn.eq_1` `MeasureTheory.integrable_congr` `MeasureTheory.Integrable.sub` `ae_eq_zero_of_forall_setIntegral_eq_zero'` `MeasureTheory.AEStronglyMeasurable.congr` `MeasureTheory.AEStronglyMeasurable.sub` `Filter.EventuallyEq.symm` `MeasureTheory.sub_ae_eq_zero` `Filter.EventuallyEq.trans`
`ae_eq_zero_of_forall_setIntegral_eq_zero'` 📖	mathematical	`MeasurableSpace` `MeasurableSpace.instLE` `MeasureTheory.IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `MeasureTheory.AEEqFun.cast` `MeasureTheory.AEEqFun` `AddSubgroup` `MeasureTheory.AEEqFun.instAddGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `MeasureTheory.Lp` `MeasureTheory.integral` `MeasureTheory.Measure.restrict` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `MeasureTheory.AEStronglyMeasurable`	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `Pi.instZero`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `NormedSpace.toIsBoundedSMul` `MeasureTheory.Measure.instOuterMeasureClass` `Filter.EventuallyEq.trans` `MeasureTheory.lpMeas.ae_eq_zero_of_forall_setIntegral_eq_zero`

MeasureTheory.lpMeas

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ae_eq_zero_of_forall_setIntegral_eq_zero` 📖	mathematical	`MeasurableSpace` `MeasurableSpace.instLE` `MeasureTheory.IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `MeasureTheory.AEEqFun.cast` `MeasureTheory.AEEqFun` `AddSubgroup` `MeasureTheory.AEEqFun.instAddGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `MeasureTheory.Lp` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Submodule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `AddCommGroup.toAddCommMonoid` `AddSubgroup.toAddCommGroup` `MeasureTheory.AEEqFun.instAddCommGroup` `NormedAddCommGroup.toAddCommGroup` `MeasureTheory.Lp.instModule` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `NormedSpace.toIsBoundedSMul` `Submodule.setLike` `MeasureTheory.lpMeas` `MeasureTheory.integral` `MeasureTheory.Measure.restrict` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `Pi.instZero`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `NormedSpace.toIsBoundedSMul` `MeasureTheory.Measure.instOuterMeasureClass` `ae_fin_strongly_measurable'` `Filter.EventuallyEq.trans` `MeasureTheory.ae_eq_zero_of_forall_setIntegral_eq_of_finStronglyMeasurable_trim` `MeasureTheory.ae_restrict_of_ae` `MeasureTheory.IntegrableOn.eq_1` `MeasureTheory.integrable_congr` `Filter.EventuallyEq.symm` `MeasureTheory.integral_congr_ae`

---

← Back to Index