Documentation Verification Report

Measure

📁 Source: Mathlib/Analysis/BoxIntegral/Partition/Measure.lean

Statistics

Metric	Count
Definitions `volume`, `toBoxAdditive`	2
Theorems `Ioo_ae_eq_Icc`, `coe_ae_eq_Icc`, `measurableSet_Icc`, `measurableSet_Ioo`, `measurableSet_coe`, `measure_Icc_lt_top`, `measure_coe_lt_top`, `volume_apply`, `volume_apply'`, `volume_face_mul`, `volume_apply`, `measure_iUnion_toReal`, `toBoxAdditive_apply`	13
Total	15

BoxIntegral.Box

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Ioo_ae_eq_Icc` 📖	mathematical	—	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.MeasureSpace.toMeasurableSpace` `MeasureTheory.MeasureSpace.pi` `Real` `Real.measureSpace` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.MeasureSpace.volume` `DFunLike.coe` `OrderHom` `BoxIntegral.Box` `Set` `PartialOrder.toPreorder` `instPartialOrder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `OrderHom.instFunLike` `Ioo` `OrderEmbedding` `instLE` `Set.instLE` `instFunLikeOrderEmbedding` `Icc`	—	`MeasureTheory.Measure.univ_pi_Ioo_ae_eq_Icc` `MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite` `instIsAddHaarMeasureVolume` `FiniteDimensional.rclike_to_real` `Real.borelSpace` `SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace` `instIsTopologicalAddGroupReal` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `instSecondCountableTopologyReal` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `locallyCompact_of_proper` `instProperSpaceReal` `Real.noAtoms_volume`
`coe_ae_eq_Icc` 📖	mathematical	—	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.MeasureSpace.toMeasurableSpace` `MeasureTheory.MeasureSpace.pi` `Real` `Real.measureSpace` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.MeasureSpace.volume` `toSet` `DFunLike.coe` `OrderEmbedding` `BoxIntegral.Box` `Set` `instLE` `Set.instLE` `instFunLikeOrderEmbedding` `Icc`	—	`MeasureTheory.Measure.instOuterMeasureClass` `coe_eq_pi` `MeasureTheory.Measure.univ_pi_Ioc_ae_eq_Icc` `MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite` `instIsAddHaarMeasureVolume` `FiniteDimensional.rclike_to_real` `Real.borelSpace` `SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace` `instIsTopologicalAddGroupReal` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `instSecondCountableTopologyReal` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `locallyCompact_of_proper` `instProperSpaceReal` `Real.noAtoms_volume`
`measurableSet_Icc` 📖	mathematical	—	`MeasurableSet` `MeasurableSpace.pi` `Real` `Real.measurableSpace` `DFunLike.coe` `OrderEmbedding` `BoxIntegral.Box` `Set` `instLE` `Set.instLE` `instFunLikeOrderEmbedding` `Icc`	—	`measurableSet_Icc` `Pi.opensMeasurableSpace` `instSecondCountableTopologyReal` `BorelSpace.opensMeasurable` `Real.borelSpace` `Pi.orderClosedTopology'` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid`
`measurableSet_Ioo` 📖	mathematical	—	`MeasurableSet` `MeasurableSpace.pi` `Real` `Real.measurableSpace` `DFunLike.coe` `OrderHom` `BoxIntegral.Box` `Set` `PartialOrder.toPreorder` `instPartialOrder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `OrderHom.instFunLike` `Ioo`	—	`MeasurableSet.univ_pi` `measurableSet_Ioo` `BorelSpace.opensMeasurable` `Real.borelSpace` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid`
`measurableSet_coe` 📖	mathematical	—	`MeasurableSet` `MeasurableSpace.pi` `Real` `Real.measurableSpace` `toSet`	—	`coe_eq_pi` `MeasurableSet.univ_pi` `measurableSet_Ioc` `BorelSpace.opensMeasurable` `Real.borelSpace` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid`
`measure_Icc_lt_top` 📖	mathematical	—	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `MeasurableSpace.pi` `Real` `Real.measurableSpace` `Set` `MeasureTheory.Measure.instFunLike` `OrderEmbedding` `BoxIntegral.Box` `instLE` `Set.instLE` `instFunLikeOrderEmbedding` `Icc` `Top.top` `instTopENNReal`	—	`IsCompact.measure_lt_top` `isFiniteMeasureOnCompacts_of_isLocallyFiniteMeasure` `isCompact_Icc`
`measure_coe_lt_top` 📖	mathematical	—	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `MeasurableSpace.pi` `Real` `Real.measurableSpace` `Set` `MeasureTheory.Measure.instFunLike` `toSet` `Top.top` `instTopENNReal`	—	`LE.le.trans_lt` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass` `coe_subset_Icc` `measure_Icc_lt_top`
`volume_apply` 📖	mathematical	—	`DFunLike.coe` `BoxIntegral.BoxAdditiveMap` `Real` `Real.instAddCommMonoid` `Top.top` `WithTop` `BoxIntegral.Box` `WithTop.top` `BoxIntegral.BoxAdditiveMap.instFunLikeBox` `MeasureTheory.Measure.toBoxAdditive` `Finite.of_fintype` `MeasureTheory.MeasureSpace.volume` `MeasureTheory.MeasureSpace.pi` `Real.measureSpace` `MeasureTheory.Measure.instIsLocallyFiniteMeasureForallVolumeOfSigmaFinite` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.instAddGroup` `instIsAddHaarMeasureVolume` `Real.normedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Real.instRCLike` `FiniteDimensional.rclike_to_real` `Real.measurableSpace` `Real.borelSpace` `SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace` `instIsTopologicalAddGroupReal` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `instSecondCountableTopologyReal` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `locallyCompact_of_proper` `instProperSpaceReal` `Real.locallyFinite_volume` `Finset.prod` `Real.instCommMonoid` `Finset.univ` `Real.instSub` `upper` `lower`	—	`Finite.of_fintype` `MeasureTheory.Measure.instIsLocallyFiniteMeasureForallVolumeOfSigmaFinite` `MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite` `instIsAddHaarMeasureVolume` `FiniteDimensional.rclike_to_real` `Real.borelSpace` `SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace` `instIsTopologicalAddGroupReal` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `instSecondCountableTopologyReal` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `locallyCompact_of_proper` `instProperSpaceReal` `Real.locallyFinite_volume` `MeasureTheory.Measure.toBoxAdditive_apply` `coe_eq_pi` `MeasureTheory.measureReal_def` `Real.volume_pi_Ioc_toReal` `lower_le_upper`
`volume_apply'` 📖	mathematical	—	`ENNReal.toReal` `DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.MeasureSpace.toMeasurableSpace` `MeasureTheory.MeasureSpace.pi` `Real` `Real.measureSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `MeasureTheory.MeasureSpace.volume` `toSet` `Finset.prod` `Real.instCommMonoid` `Finset.univ` `Real.instSub` `upper` `lower`	—	`coe_eq_pi` `Real.volume_pi_Ioc_toReal` `lower_le_upper`
`volume_face_mul` 📖	mathematical	—	`Real` `Real.instMul` `Finset.prod` `Real.instCommMonoid` `Finset.univ` `Fin.fintype` `Real.instSub` `upper` `face` `lower`	—	`Finset.prod_congr` `mul_comm` `Fin.prod_univ_succAbove`

BoxIntegral.BoxAdditiveMap

Definitions

Name	Category	Theorems
`volume` 📖	CompOp	4 math math: `BoxIntegral.hasIntegral_GP_pderiv`, `BoxIntegral.hasIntegral_GP_divergence_of_forall_hasDerivWithinAt`, `volume_apply`, `BoxIntegral.norm_volume_sub_integral_face_upper_sub_lower_smul_le`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`volume_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `Real` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `ContinuousLinearMap.funLike` `BoxIntegral.BoxAdditiveMap` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Top.top` `WithTop` `BoxIntegral.Box` `WithTop.top` `instFunLikeBox` `volume` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Finset.prod` `Real.instCommMonoid` `Finset.univ` `Real.instSub` `BoxIntegral.Box.upper` `BoxIntegral.Box.lower`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Finite.of_fintype` `volume.eq_1` `toSMul_apply` `BoxIntegral.Box.volume_apply`

BoxIntegral.Prepartition

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`measure_iUnion_toReal` 📖	mathematical	—	`MeasureTheory.Measure.real` `MeasurableSpace.pi` `Real` `Real.measurableSpace` `iUnion` `Finset.sum` `BoxIntegral.Box` `Real.instAddCommMonoid` `boxes` `BoxIntegral.Box.toSet`	—	`Finset.sum_congr` `ENNReal.toReal_sum` `LT.lt.ne` `BoxIntegral.Box.measure_coe_lt_top` `iUnion_def` `Set.iUnion_congr_Prop` `MeasureTheory.measure_biUnion_finset` `pairwiseDisjoint` `BoxIntegral.Box.measurableSet_coe` `Finite.to_countable`

MeasureTheory.Measure

Definitions

Name	Category	Theorems
`toBoxAdditive` 📖	CompOp	10 math, 5 bridge math: `BoxIntegral.integrable_of_continuousOn`, `BoxIntegral.unitPartition.integralSum_eq_tsum_div`, `MeasureTheory.AEContinuous.hasBoxIntegral`, `BoxIntegral.integrable_of_bounded_and_ae_continuous`, `BoxIntegral.integral_nonneg`, `BoxIntegral.norm_integral_le_of_le_const`, `MeasureTheory.ContinuousOn.hasBoxIntegral`, `toBoxAdditive_apply`, `BoxIntegral.Box.volume_apply`, `BoxIntegral.integrable_of_bounded_and_ae_continuousWithinAt` bridge: `BoxIntegral.hasIntegralIndicatorConst`, `MeasureTheory.SimpleFunc.hasBoxIntegral`, `MeasureTheory.IntegrableOn.hasBoxIntegral`, `BoxIntegral.HasIntegral.of_aeEq_zero`, `MeasureTheory.SimpleFunc.box_integral_eq_integral`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toBoxAdditive_apply` 📖	mathematical	—	`DFunLike.coe` `BoxIntegral.BoxAdditiveMap` `Real` `Real.instAddCommMonoid` `Top.top` `WithTop` `BoxIntegral.Box` `WithTop.top` `BoxIntegral.BoxAdditiveMap.instFunLikeBox` `toBoxAdditive` `real` `MeasurableSpace.pi` `Real.measurableSpace` `BoxIntegral.Box.toSet`	—	—

---

← Back to Index