Documentation Verification Report

AEEqOfIntegral

📁 Source: Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean

Statistics

Metric	Count
Definitions	0
Theorems `ae_eq_of_forall_setIntegral_eq`, `ae_eq_zero_of_forall_setIntegral_eq_zero`, `ae_nonneg_of_forall_setIntegral_nonneg`, `ae_eq_of_forall_setIntegral_eq`, `ae_eq_zero_of_forall_setIntegral_eq_zero`, `ae_eq_of_forall_setIntegral_eq`, `ae_eq_zero_of_forall_setIntegral_eq_zero`, `ae_eq_of_forall_setIntegral_eq_of_sigmaFinite`, `ae_eq_restrict_of_forall_setIntegral_eq`, `ae_eq_zero_of_forall_dual`, `ae_eq_zero_of_forall_dual_of_isSeparable`, `ae_eq_zero_of_forall_inner`, `ae_eq_zero_of_forall_setIntegral_eq_of_finStronglyMeasurable_trim`, `ae_eq_zero_of_forall_setIntegral_eq_of_sigmaFinite`, `ae_eq_zero_of_forall_setIntegral_isClosed_eq_zero`, `ae_eq_zero_of_forall_setIntegral_isCompact_eq_zero`, `ae_eq_zero_of_forall_setIntegral_isCompact_eq_zero'`, `ae_eq_zero_restrict_of_forall_setIntegral_eq_zero`, `ae_eq_zero_restrict_of_forall_setIntegral_eq_zero_real`, `ae_le_of_forall_setIntegral_le`, `ae_nonneg_of_forall_setIntegral_nonneg`, `ae_nonneg_of_forall_setIntegral_nonneg_of_sigmaFinite`, `ae_nonneg_restrict_of_forall_setIntegral_nonneg`, `ae_nonneg_restrict_of_forall_setIntegral_nonneg_inter`	24
Total	24

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ae_eq_of_forall_setIntegral_eq_of_sigmaFinite` 📖	mathematical	`IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `integral` `Measure.restrict`	`Filter.EventuallyEq` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass`	—	`Measure.instOuterMeasureClass` `sub_ae_eq_zero` `integral_sub'` `sub_eq_zero` `Integrable.sub` `ae_eq_zero_of_forall_setIntegral_eq_of_sigmaFinite`
`ae_eq_restrict_of_forall_setIntegral_eq` 📖	mathematical	`IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `integral` `Measure.restrict` `MeasurableSet`	`Filter.EventuallyEq` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass`	—	`Measure.instOuterMeasureClass` `sub_ae_eq_zero` `integral_sub'` `sub_eq_zero` `Integrable.sub` `ae_eq_zero_restrict_of_forall_setIntegral_eq_zero`
`ae_eq_zero_of_forall_dual` 📖	mathematical	`Filter.EventuallyEq` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `DFunLike.coe` `StrongDual` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousLinearMap.funLike` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `Pi.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing`	`NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`Measure.instOuterMeasureClass` `ae_eq_zero_of_forall_dual_of_isSeparable` `TopologicalSpace.IsSeparable.of_separableSpace` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `Filter.Eventually.of_forall` `Set.mem_univ`
`ae_eq_zero_of_forall_dual_of_isSeparable` 📖	mathematical	`TopologicalSpace.IsSeparable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Filter.EventuallyEq` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `DFunLike.coe` `StrongDual` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousLinearMap.funLike` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `Pi.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Filter.Eventually` `Set` `Set.instMembership`	`NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`Measure.instOuterMeasureClass` `exists_dual_vector''` `Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_forall_eq` `Nat.instAtLeastTwoHAddOfNat` `Metric.mem_closure_iff` `half_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `norm_le_insert'` `dist_eq_norm` `lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Nat.cast_one` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Mathlib.Tactic.Linarith.add_lt_of_le_of_neg` `Mathlib.Tactic.Linarith.mul_nonpos` `Real.instIsOrderedRing` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Mathlib.Meta.NormNum.isNat_lt_true` `RCLike.charZero_rclike` `CancelDenoms.sub_subst` `CancelDenoms.div_subst` `Mathlib.Meta.NormNum.isNat_eq_true` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Tactic.Linarith.mul_neg` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `lt_irrefl` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass` `sub_zero` `ContinuousLinearMap.le_of_opNorm_le` `RingHomIsometric.ids` `one_mul` `dist_eq_norm'` `norm_algebraMap'` `NormedDivisionRing.to_normOneClass` `norm_norm` `ae_all_iff` `Encodable.countable` `Filter.mp_mem` `Filter.univ_mem'`
`ae_eq_zero_of_forall_inner` 📖	mathematical	`Filter.EventuallyEq` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `Inner.inner` `InnerProductSpace.toInner` `NormedAddCommGroup.toSeminormedAddCommGroup` `Pi.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField`	`NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`Measure.instOuterMeasureClass` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `AddTorsor.nonempty` `TopologicalSpace.denseRange_denseSeq` `ae_all_iff` `instCountableNat` `Filter.Eventually.mono` `Pi.zero_apply` `inner_self_eq_zero` `isClosed_eq` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `Continuous.inner` `continuous_id'` `continuous_const` `isClosed_property`
`ae_eq_zero_of_forall_setIntegral_eq_of_finStronglyMeasurable_trim` 📖	mathematical	`MeasurableSpace` `MeasurableSpace.instLE` `IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `integral` `Measure.restrict` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `FinStronglyMeasurable` `Measure.trim`	`Filter.EventuallyEq` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `Pi.instZero`	—	`Measure.instOuterMeasureClass` `FinStronglyMeasurable.exists_set_sigmaFinite` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `Filter.EventuallyEq.eq_1` `ae_restrict_iff'` `MeasurableSet.compl` `Filter.Eventually.of_forall` `FinStronglyMeasurable.stronglyMeasurable` `measure_eq_zero_of_trim_eq_zero` `ae_eq_zero_of_forall_setIntegral_eq_of_sigmaFinite` `restrict_trim` `Measure.restrict_restrict` `Integrable.trim` `MeasurableSet.inter` `trim_measurableSet_eq` `Measure.restrict_apply` `integral_trim` `ae_of_ae_restrict_of_ae_restrict_compl`
`ae_eq_zero_of_forall_setIntegral_eq_of_sigmaFinite` 📖	mathematical	`IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `integral` `Measure.restrict` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	`Filter.EventuallyEq` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `Pi.instZero`	—	`Measure.instOuterMeasureClass` `Measure.restrict_univ` `iUnion_spanningSets` `Filter.EventuallyEq.eq_1` `ae_iff` `Measure.restrict_apply'` `MeasurableSet.iUnion` `instCountableNat` `measurableSet_spanningSets` `Set.inter_iUnion` `measure_iUnion_null_iff` `measure_spanningSets_lt_top` `ae_eq_zero_restrict_of_forall_setIntegral_eq_zero` `LT.lt.ne`
`ae_eq_zero_of_forall_setIntegral_isClosed_eq_zero` 📖	mathematical	`Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `integral` `Measure.restrict` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	`Filter.EventuallyEq` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `Pi.instZero`	—	`setIntegral_univ` `isClosed_univ` `zero_add` `integral_add_compl` `MeasurableSet.induction_on_open` `MeasurableSet.compl` `IsOpen.measurableSet` `BorelSpace.opensMeasurable` `IsOpen.isClosed_compl` `compl_compl` `integral_iUnion` `instCountableNat` `Integrable.integrableOn` `tsum_zero` `Integrable.ae_eq_zero_of_forall_setIntegral_eq_zero`
`ae_eq_zero_of_forall_setIntegral_isCompact_eq_zero` 📖	mathematical	`Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `integral` `Measure.restrict` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	`Filter.EventuallyEq` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `Pi.instZero`	—	`ae_eq_zero_of_forall_setIntegral_isClosed_eq_zero` `Set.iUnion_inter` `iUnion_closure_compactCovering` `Set.univ_inter` `tendsto_setIntegral_of_monotone` `instIsCountablyGenerated_atTop` `OrderTopology.of_linearLocallyFinite` `instDiscreteTopologyNat` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace` `Countable.LindelofSpace` `instCountableNat` `PseudoEMetricSpace.pseudoMetrizableSpace` `IsClosed.measurableSet` `BorelSpace.opensMeasurable` `IsClosed.inter` `isClosed_closure` `Set.inter_subset_inter` `closure_mono` `compactCovering_subset` `subset_refl` `Set.instReflSubset` `Integrable.integrableOn` `IsCompact.inter_right` `IsCompact.closure` `isCompact_compactCovering` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat`
`ae_eq_zero_of_forall_setIntegral_isCompact_eq_zero'` 📖	mathematical	`LocallyIntegrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `integral` `Measure.restrict` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	`Filter.EventuallyEq` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `Pi.instZero`	—	`Measure.instOuterMeasureClass` `Measure.restrict_univ` `iUnion_closure_compactCovering` `ae_restrict_iUnion_iff` `instCountableNat` `ae_eq_zero_of_forall_setIntegral_isCompact_eq_zero` `LocallyIntegrable.integrableOn_isCompact` `PseudoEMetricSpace.pseudoMetrizableSpace` `IsCompact.closure` `isCompact_compactCovering` `Measure.restrict_restrict'` `measurableSet_closure` `BorelSpace.opensMeasurable` `IsCompact.inter_right` `isClosed_closure`
`ae_eq_zero_restrict_of_forall_setIntegral_eq_zero` 📖	mathematical	`IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `integral` `Measure.restrict` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `MeasurableSet`	`Filter.EventuallyEq` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `Pi.instZero`	—	`Measure.instOuterMeasureClass` `AEStronglyMeasurable.isSeparable_ae_range` `Integrable.aestronglyMeasurable` `Ne.lt_top` `ae_eq_zero_of_forall_dual_of_isSeparable` `ae_eq_zero_restrict_of_forall_setIntegral_eq_zero_real` `ContinuousLinearMap.integrable_comp` `RingHomIsometric.ids` `ContinuousLinearMap.integral_comp_comm` `Real.instCompleteSpace` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass`
`ae_eq_zero_restrict_of_forall_setIntegral_eq_zero_real` 📖	mathematical	`IntegrableOn` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `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` `Real.instZero` `MeasurableSet`	`Filter.EventuallyEq` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `Pi.instZero`	—	`Measure.instOuterMeasureClass` `ae_nonneg_restrict_of_forall_setIntegral_nonneg` `Integrable.neg` `integral_neg` `neg_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Eq.le` `Filter.Eventually.mono` `Pi.neg_apply` `Filter.Eventually.mp` `le_antisymm`
`ae_le_of_forall_setIntegral_le` 📖	mathematical	`Integrable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `Real.instLE` `integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Measure.restrict`	`Filter.EventuallyLE` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass`	—	`Measure.instOuterMeasureClass` `Filter.eventually_sub_nonneg` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `ae_nonneg_of_forall_setIntegral_nonneg` `Integrable.sub` `integral_sub'` `Integrable.integrableOn` `sub_nonneg`
`ae_nonneg_of_forall_setIntegral_nonneg` 📖	mathematical	`Integrable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `Real.instLE` `Real.instZero` `integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Measure.restrict`	`Filter.EventuallyLE` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `Pi.instZero`	—	`Measure.instOuterMeasureClass` `ae_const_le_iff_forall_lt_measure_zero` `instOrderTopologyReal` `TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology` `PseudoEMetricSpace.pseudoMetrizableSpace` `nullMeasurableSet_le` `BorelSpace.opensMeasurable` `Real.borelSpace` `instSecondCountableTopologyReal` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `AEStronglyMeasurable.aemeasurable` `aemeasurable_const` `Integrable.measure_le_lt_top` `IsOrderedAddMonoid.toAddLeftMono` `setIntegral_mono_ae_restrict` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `Real.instIsStrictOrderedRing` `instClosedIciTopology` `Integrable.integrableOn` `integrableOn_const` `LT.lt.ne` `enorm_ne_top` `Filter.EventuallyLE.eq_1` `ae_restrict_iff₀` `NullMeasurableSet.mono` `Measure.restrict_le_self` `Filter.Eventually.of_forall` `mul_comm` `smul_eq_mul` `setIntegral_const` `Real.instCompleteSpace` `Mathlib.Tactic.Contrapose.contrapose₁` `mul_neg_of_neg_of_pos` `IsStrictOrderedRing.toMulPosStrictMono` `ENNReal.toReal_pos` `Measure.restrict_toMeasurable` `measurableSet_toMeasurable` `measure_toMeasurable`
`ae_nonneg_of_forall_setIntegral_nonneg_of_sigmaFinite` 📖	mathematical	`IntegrableOn` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `Real.instLE` `Real.instZero` `integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Measure.restrict`	`Filter.EventuallyLE` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `Pi.instZero`	—	`ae_of_forall_measure_lt_top_ae_restrict` `ae_nonneg_restrict_of_forall_setIntegral_nonneg_inter` `MeasurableSet.inter` `lt_of_le_of_lt` `measure_mono` `Measure.instOuterMeasureClass` `Set.inter_subset_right`
`ae_nonneg_restrict_of_forall_setIntegral_nonneg` 📖	mathematical	`IntegrableOn` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `Real.instLE` `Real.instZero` `integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Measure.restrict` `MeasurableSet`	`Filter.EventuallyLE` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `Pi.instZero`	—	`ae_nonneg_restrict_of_forall_setIntegral_nonneg_inter` `lt_top_iff_ne_top` `MeasurableSet.inter` `LE.le.trans_lt` `measure_mono` `Measure.instOuterMeasureClass` `Set.inter_subset_right`
`ae_nonneg_restrict_of_forall_setIntegral_nonneg_inter` 📖	mathematical	`IntegrableOn` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `Real.instLE` `Real.instZero` `integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Measure.restrict` `Set` `Set.instInter`	`Filter.EventuallyLE` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `Pi.instZero`	—	`ae_nonneg_of_forall_setIntegral_nonneg` `Measure.restrict_restrict` `Measure.restrict_apply`

MeasureTheory.AEFinStronglyMeasurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ae_eq_of_forall_setIntegral_eq` 📖	mathematical	`MeasureTheory.IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `MeasureTheory.integral` `MeasureTheory.Measure.restrict` `MeasureTheory.AEFinStronglyMeasurable` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.sub_ae_eq_zero` `MeasureTheory.integral_sub'` `sub_eq_zero` `MeasureTheory.Integrable.sub` `ae_eq_zero_of_forall_setIntegral_eq_zero` `sub` `IsTopologicalAddGroup.to_continuousSub` `SeminormedAddCommGroup.toIsTopologicalAddGroup`
`ae_eq_zero_of_forall_setIntegral_eq_zero` 📖	mathematical	`MeasureTheory.IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `MeasureTheory.integral` `MeasureTheory.Measure.restrict` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `MeasureTheory.AEFinStronglyMeasurable`	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `Pi.instZero`	—	`TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.ae_eq_zero_of_forall_setIntegral_eq_of_sigmaFinite` `sigmaFinite_restrict` `MeasureTheory.IntegrableOn.eq_1` `MeasureTheory.Measure.restrict_restrict` `MeasurableSet.inter` `measurableSet` `MeasureTheory.Measure.restrict_apply` `MeasureTheory.ae_of_ae_restrict_of_ae_restrict_compl` `ae_eq_zero_compl`
`ae_nonneg_of_forall_setIntegral_nonneg` 📖	mathematical	`MeasureTheory.AEFinStronglyMeasurable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instZero` `MeasureTheory.IntegrableOn` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `Real.instLE` `MeasureTheory.integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `MeasureTheory.Measure.restrict`	`Filter.EventuallyLE` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `Pi.instZero`	—	`TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.ae_nonneg_of_forall_setIntegral_nonneg_of_sigmaFinite` `sigmaFinite_restrict` `MeasureTheory.IntegrableOn.eq_1` `MeasureTheory.Measure.restrict_restrict` `MeasurableSet.inter` `measurableSet` `MeasureTheory.Measure.restrict_apply` `MeasureTheory.ae_of_ae_restrict_of_ae_restrict_compl` `Filter.EventuallyEq.le` `Filter.EventuallyEq.symm` `ae_eq_zero_compl`

MeasureTheory.Integrable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ae_eq_of_forall_setIntegral_eq` 📖	mathematical	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `MeasureTheory.integral` `MeasureTheory.Measure.restrict`	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.sub_ae_eq_zero` `MeasureTheory.integral_sub'` `integrableOn` `sub_eq_zero` `ae_eq_zero_of_forall_setIntegral_eq_zero` `sub`
`ae_eq_zero_of_forall_setIntegral_eq_zero` 📖	mathematical	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `MeasureTheory.integral` `MeasureTheory.Measure.restrict` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `Pi.instZero`	—	`MeasureTheory.memLp_one_iff_integrable` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `MeasureTheory.Measure.instOuterMeasureClass` `Filter.EventuallyEq.symm` `MeasureTheory.MemLp.coeFn_toLp` `Filter.EventuallyEq.trans` `MeasureTheory.Lp.ae_eq_zero_of_forall_setIntegral_eq_zero` `one_ne_zero` `NeZero.charZero_one` `ENNReal.instCharZero` `ENNReal.coe_ne_top` `integrableOn` `MeasureTheory.L1.integrable_coeFn` `MeasureTheory.integral_congr_ae` `MeasureTheory.ae_restrict_of_ae`

MeasureTheory.Lp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ae_eq_of_forall_setIntegral_eq` 📖	mathematical	`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`	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `MeasureTheory.AEFinStronglyMeasurable.ae_eq_of_forall_setIntegral_eq` `MeasureTheory.FinStronglyMeasurable.aefinStronglyMeasurable` `finStronglyMeasurable`
`ae_eq_zero_of_forall_setIntegral_eq_zero` 📖	mathematical	`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`	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `Pi.instZero`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `MeasureTheory.AEFinStronglyMeasurable.ae_eq_zero_of_forall_setIntegral_eq_zero` `MeasureTheory.FinStronglyMeasurable.aefinStronglyMeasurable` `finStronglyMeasurable`

---

← Back to Index