Documentation Verification Report

Integral

📁 Source: Mathlib/MeasureTheory/Measure/Lebesgue/Integral.lean

Statistics

Metric	Count
Definitions	0
Theorems `integrable_of_summable_norm_Icc`, `integral_comp_abs`, `integral_comp_neg_Iic`, `integral_comp_neg_Ioi`, `volume_regionBetween_eq_integral`, `volume_regionBetween_eq_integral'`	6
Total	6

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`integrable_of_summable_norm_Icc` 📖	mathematical	`Summable` `Real` `instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `Norm.norm` `ContinuousMap` `Set.Elem` `Set.Icc` `instPreorder` `instZero` `instOne` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ContinuousMap.instNorm` `compactSpace_Icc` `ConditionallyCompleteLinearOrder.toCompactIccSpace` `instConditionallyCompleteLinearOrder` `instOrderTopologyReal` `ContinuousMap.restrict` `ContinuousMap.comp` `ContinuousMap.addRight` `instAdd` `IsTopologicalSemiring.toContinuousAdd` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `normedCommRing` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instIntCast` `SummationFilter.unconditional`	`MeasureTheory.Integrable` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpace` `DFunLike.coe` `ContinuousMap.instFunLike` `MeasureTheory.MeasureSpace.volume`	—	`compactSpace_Icc` `ConditionallyCompleteLinearOrder.toCompactIccSpace` `instOrderTopologyReal` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `MeasureTheory.integrable_of_summable_norm_restrict` `instCountableInt` `borelSpace` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `locallyFinite_volume` `CompactIccSpace.isCompact_Icc` `Summable.of_nonneg_of_le` `ContinuousMap.instCompactSpaceElemCoeCompacts` `mul_nonneg` `IsOrderedRing.toPosMulMono` `instIsOrderedRing` `norm_nonneg` `ENNReal.toReal_nonneg` `volume_real_Icc_of_le` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `instZeroLEOneClass` `add_sub_cancel_left` `mul_one` `ContinuousMap.norm_le` `sub_nonneg` `covariant_swap_add_of_covariant_add` `sub_le_iff_le_add'` `ContinuousMap.norm_coe_le_norm` `sub_add_cancel` `iUnion_Icc_intCast` `instIsStrictOrderedRing` `instArchimedean`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`integral_comp_abs` 📖	mathematical	—	`MeasureTheory.integral` `Real` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `MeasureTheory.MeasureSpace.volume` `abs` `Real.lattice` `Real.instAddGroup` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `MeasureTheory.Measure.restrict` `Set.Ioi` `Real.instPreorder` `Real.instZero`	—	`MeasureTheory.setIntegral_congr_fun` `measurableSet_Ioi` `BorelSpace.opensMeasurable` `Real.borelSpace` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `abs_eq_self` `le_of_lt` `Nat.instAtLeastTwoHAddOfNat` `MeasureTheory.Measure.map_neg_eq_self` `MeasureTheory.Measure.IsAddHaarMeasure.isNegInvariant_of_innerRegular` `instIsTopologicalAddGroupReal` `instIsAddHaarMeasureVolume` `FiniteDimensional.rclike_to_real` `locallyCompact_of_proper` `instProperSpaceReal` `MeasureTheory.Measure.instInnerRegularOfPseudoMetrizableSpaceOfSigmaCompactSpaceOfBorelSpaceOfSigmaFinite` `PseudoEMetricSpace.pseudoMetrizableSpace` `SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `instSecondCountableTopologyReal` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite` `Homeomorph.measurableEmbedding` `IsTopologicalRing.toContinuousNeg` `instIsTopologicalRingReal` `MeasurableEmbedding.integrableOn_map_iff` `abs_neg` `Set.neg_Iic` `neg_zero` `integrableOn_Ici_iff_integrableOn_Ioi` `instMeasurableSingletonClassOfMeasurableEq` `instMeasurableEqOfSecondCountableTopologyOfT2Space` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `Real.noAtoms_volume` `enorm_ne_top` `MeasureTheory.setIntegral_union` `Set.Iic_disjoint_Ioi` `le_rfl` `Set.Iic_union_Ioi` `MeasureTheory.Measure.restrict_univ` `two_mul` `integral_comp_neg_Iic` `measurableSet_Iic` `abs_eq_neg_self` `Mathlib.Tactic.Contrapose.contrapose₄` `MeasureTheory.Integrable.integrableOn` `MeasureTheory.integral_undef` `MulZeroClass.mul_zero`
`integral_comp_neg_Iic` 📖	mathematical	—	`MeasureTheory.integral` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `MeasureTheory.Measure.restrict` `MeasureTheory.MeasureSpace.volume` `Set.Iic` `Real.instPreorder` `Real.instNeg` `Set.Ioi`	—	`Topology.IsClosedEmbedding.measurableEmbedding` `Real.borelSpace` `IsTopologicalRing.toContinuousNeg` `instIsTopologicalRingReal` `Homeomorph.isClosedEmbedding` `MeasurableEmbedding.setIntegral_map` `Real.noAtoms_volume` `MeasureTheory.Measure.map_neg_eq_self` `MeasureTheory.Measure.IsAddHaarMeasure.isNegInvariant_of_innerRegular` `instIsTopologicalAddGroupReal` `instIsAddHaarMeasureVolume` `FiniteDimensional.rclike_to_real` `locallyCompact_of_proper` `instProperSpaceReal` `MeasureTheory.Measure.instInnerRegularOfPseudoMetrizableSpaceOfSigmaCompactSpaceOfBorelSpaceOfSigmaFinite` `PseudoEMetricSpace.pseudoMetrizableSpace` `SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `instSecondCountableTopologyReal` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite` `Set.neg_Ici` `Real.instIsOrderedAddMonoid` `neg_neg`
`integral_comp_neg_Ioi` 📖	mathematical	—	`MeasureTheory.integral` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `MeasureTheory.Measure.restrict` `MeasureTheory.MeasureSpace.volume` `Set.Ioi` `Real.instPreorder` `Real.instNeg` `Set.Iic`	—	`neg_neg` `integral_comp_neg_Iic`
`volume_regionBetween_eq_integral` 📖	mathematical	`MeasureTheory.IntegrableOn` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `MeasurableSet` `Real.instLE`	`DFunLike.coe` `MeasureTheory.Measure` `Prod.instMeasurableSpace` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.prod` `MeasureTheory.MeasureSpace.volume` `regionBetween` `ENNReal.ofReal` `MeasureTheory.integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `MeasureTheory.Measure.restrict` `Pi.instSub` `Real.instSub`	—	`volume_regionBetween_eq_integral'` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.ae_restrict_iff'` `Filter.Eventually.of_forall`
`volume_regionBetween_eq_integral'` 📖	mathematical	`MeasureTheory.IntegrableOn` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `MeasurableSet` `Filter.EventuallyLE` `Real.instLE` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.restrict`	`DFunLike.coe` `Prod.instMeasurableSpace` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `Set` `ENNReal` `MeasureTheory.Measure.prod` `MeasureTheory.MeasureSpace.volume` `regionBetween` `ENNReal.ofReal` `MeasureTheory.integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Pi.instSub` `Real.instSub`	—	`MeasureTheory.Measure.instOuterMeasureClass` `Filter.Eventually.mono` `Real.coe_toNNReal` `sub_nonneg` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `volume_regionBetween_eq_lintegral` `MeasureTheory.instSFiniteOfSigmaFinite` `MeasureTheory.Integrable.aemeasurable` `Real.borelSpace` `PseudoEMetricSpace.pseudoMetrizableSpace` `MeasureTheory.integral_congr_ae` `MeasureTheory.lintegral_congr_ae` `Filter.EventuallyEq.refl` `MeasureTheory.lintegral_coe_eq_integral` `MeasureTheory.integrable_congr` `MeasureTheory.Integrable.sub`

---

← Back to Index