Documentation Verification Report

DivergenceTheorem

📁 Source: Mathlib/Analysis/BoxIntegral/DivergenceTheorem.lean

Statistics

Metric	Count
Definitions	0
Theorems `hasIntegral_GP_divergence_of_forall_hasDerivWithinAt`, `hasIntegral_GP_pderiv`, `norm_volume_sub_integral_face_upper_sub_lower_smul_le`	3
Total	3

BoxIntegral

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasIntegral_GP_divergence_of_forall_hasDerivWithinAt` 📖	mathematical	`ContinuousWithinAt` `Pi.topologicalSpace` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `DFunLike.coe` `OrderEmbedding` `Box` `Set` `Box.instLE` `Set.instLE` `instFunLikeOrderEmbedding` `Box.Icc` `HasFDerivWithinAt` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Pi.addCommGroup` `Real.instAddCommGroup` `Pi.Function.module` `Real.semiring` `Real.instAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `NormedAddCommGroup.toAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	`HasIntegral` `Fin.fintype` `IntegrationParams.GP` `Finset.sum` `Finset.univ` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `ContinuousLinearMap.funLike` `Pi.single` `Real.instZero` `Real.instOne` `BoxAdditiveMap.volume` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `integral` `Box.face` `Fin.insertNth` `Box.upper` `Box.lower`	—	`HasIntegral.sum` `hasIntegral_GP_pderiv` `RingHomCompTriple.ids` `Finite.of_fintype`
`hasIntegral_GP_pderiv` 📖	mathematical	`ContinuousWithinAt` `Pi.topologicalSpace` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `DFunLike.coe` `OrderEmbedding` `Box` `Set` `Box.instLE` `Set.instLE` `instFunLikeOrderEmbedding` `Box.Icc` `HasFDerivWithinAt` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Pi.addCommGroup` `Real.instAddCommGroup` `Pi.Function.module` `Real.semiring` `Real.instAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `SeminormedAddCommGroup.toAddCommGroup`	`HasIntegral` `Fin.fintype` `IntegrationParams.GP` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.funLike` `Pi.single` `Real.instZero` `Real.instOne` `BoxAdditiveMap.volume` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `integral` `Box.face` `Fin.insertNth` `Box.upper` `Box.lower`	—	`HasFDerivWithinAt.continuousWithinAt` `instContinuousAddForallOfIsTopologicalSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instContinuousSMulForall` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `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` `integrable_of_continuousOn` `Box.continuousOn_face_Icc` `HasIntegral.of_le_Henstock_of_forall_isLittleO` `IntegrationParams.gp_le` `le_top` `ENNReal.toReal_nonneg` `Nat.instAtLeastTwoHAddOfNat` `Filter.Eventually.and` `Ioc_mem_nhdsGT` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `one_half_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Filter.HasBasis.tendsto_iff` `nhdsWithin_hasBasis` `Metric.nhds_basis_closedBall` `half_pos` `Filter.mp_mem` `Filter.univ_mem'` `Set.inter_subset_inter` `Metric.closedBall_subset_closedBall` `subset_refl` `Set.instReflSubset` `dist_eq_norm` `dist_triangle_right` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `covariant_swap_add_of_covariant_add` `add_halves` `CharZero.NeZero.two` `RCLike.charZero_rclike` `Filter.Tendsto.mul_const` `IsTopologicalSemiring.toContinuousMul` `Filter.Tendsto.pow` `Filter.Tendsto.const_mul` `continuousWithinAt_id` `Filter.Tendsto.eventually` `ge_mem_nhds` `instOrderTopologyReal` `MulZeroClass.mul_zero` `zero_pow` `MulZeroClass.zero_mul` `Real.instIsOrderedRing` `Real.instNontrivial` `Filter.Eventually.exists` `nhdsGT_neBot` `LinearOrderedSemiField.toDenselyOrdered` `instNoMaxOrderOfNontrivial` `Set.left_mem_Icc` `Box.lower_le_upper` `Set.right_mem_Icc` `ContinuousOn.mono` `Box.le_iff_Icc` `Set.subset_inter` `Set.MapsTo.mono` `Box.mapsTo_insertNth_face_Icc` `Set.Subset.rfl` `integral_sub` `LE.le.trans` `norm_sub_le` `BoxAdditiveMap.volume_apply` `norm_smul` `NormedSpace.toNormSMulClass` `Finset.abs_prod` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `dist_le_pi_dist` `Box.upper_mem_Icc` `Box.lower_mem_Icc` `two_mul` `Finset.prod_le_prod` `Real.instZeroLEOneClass` `IsOrderedRing.toPosMulMono` `abs_nonneg` `Finset.prod_const` `Fintype.card_fin` `norm_nonneg` `norm_integral_le_of_le_const` `LE.le.trans_eq` `Box.coe_eq_pi` `MeasureTheory.measureReal_def` `Real.volume_pi_Ioc_toReal` `Finset.prod_le_one` `sub_nonneg` `le_abs_self` `LT.lt.le` `one_mul` `exists_pos_mul_lt` `Filter.HasBasis.mem_iff` `Asymptotics.IsLittleO.def` `HasFDerivAtFilter.isLittleO` `norm_volume_sub_integral_face_upper_sub_lower_smul_le` `mul_right_comm` `Box.volume_apply`
`norm_volume_sub_integral_face_upper_sub_lower_smul_le` 📖	mathematical	`ContinuousOn` `Pi.topologicalSpace` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `DFunLike.coe` `OrderEmbedding` `Box` `Set` `Box.instLE` `Set.instLE` `instFunLikeOrderEmbedding` `Box.Icc` `Set.instMembership` `Real.instLT` `Real.instZero` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `ContinuousLinearMap` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `Real.instAddCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Pi.Function.module` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `ContinuousLinearMap.funLike` `Pi.instSub` `Real.instSub` `Real.instMul` `NormedRing.toNorm` `Pi.normedRing` `Fin.fintype` `NormedCommRing.toNormedRing` `NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `Box.distortion`	`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` `Box.upper` `Box.lower` `Pi.single` `Real.instOne` `integral` `Box.face` `Bot.bot` `IntegrationParams` `OrderBot.toBot` `IntegrationParams.instPartialOrder` `BoundedOrder.toOrderBot` `IntegrationParams.instBoundedOrder` `Fin.insertNth` `BoxAdditiveMap.volume` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `NNReal.toReal`	—	`Nat.instAtLeastTwoHAddOfNat` `Set.left_mem_Icc` `Box.lower_le_upper` `Set.right_mem_Icc` `integrable_of_continuousOn` `Box.continuousOn_face_Icc` `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` `Fin.insertNth_sub_same` `ContinuousLinearMap.map_sub` `Mathlib.Tactic.Abel.unfold_sub` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Tactic.Abel.const_add_termg` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_neg` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Abel.term_add_termg` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Abel.zero_termg` `add_zero` `Box.mapsTo_insertNth_face_Icc` `LE.le.trans` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `dist_eq_norm` `Metric.dist_le_diam_of_mem` `IsCompact.isBounded` `Box.isCompact_Icc` `LT.lt.le` `two_mul` `add_mul` `Distrib.rightDistribClass` `norm_sub_le_of_le` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass` `add_add_sub_cancel` `add_sub_cancel` `integral_sub` `Box.volume_face_mul` `SemigroupAction.mul_smul` `Finite.of_fintype` `Box.volume_apply` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `BoxAdditiveMap.toSMul_apply` `integral_const` `BoxAdditiveMap.volume.eq_1` `integrable_const` `Integrable.sub` `ContinuousLinearMap.map_smul` `mul_one` `norm_integral_le_of_le_const` `mul_assoc` `Box.diam_Icc_le_of_distortion_le` `le_of_lt` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial` `Mathlib.Meta.NormNum.instAtLeastTwo` `MeasureTheory.measureReal_def` `MeasureTheory.Measure.toBoxAdditive_apply` `Semigroup.to_isAssociative` `CommMagma.to_isCommutative`

---

← Back to Index