UnitPartition

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

Statistics

Metric	Count
Definitions hasIntegralVertices, admissibleIndex, box, index, prepartition, tag	6
Theorems le_hasIntegralVertices_of_isBounded, upper_sub_lower, box_index_tag_eq_self, box_injective, box_lower, box_upper, diam_boxIcc, disjoint, eq_of_mem_smul_span_of_index_eq_index, index_apply, index_tag, integralSum_eq_tsum_div, mem_admissibleIndex_iff, mem_admissibleIndex_of_mem_box, mem_box_iff, mem_box_iff', mem_box_iff_index, mem_prepartition_boxes_iff, mem_prepartition_iff, mem_smul_span_iff, prepartition_isHenstock, prepartition_isPartition, prepartition_isSubordinate, prepartition_tag, setFinite_index, tag_apply, tag_index_eq_self_of_mem_smul_span, tag_injective, tag_mem, tag_mem_smul_span, volume_box, tendsto_card_div_pow_atTop_volume, tendsto_card_div_pow_atTop_volume', tendsto_tsum_div_pow_atTop_integral	34
Total	40

BoxIntegral

Definitions

Name	Category	Theorems
hasIntegralVertices 📖	MathDef	1 math math: le_hasIntegralVertices_of_isBounded

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
le_hasIntegralVertices_of_isBounded 📖	mathematical	Bornology.IsBounded Pi.instBornology Real PseudoMetricSpace.toBornology Real.pseudoMetricSpace	hasIntegralVertices Set Set.instLE Box.toSet	—	Bornology.IsBounded.subset_ball_lt Real.instIsStrictOrderedRing Nat.ceil_pos Real.instIsOrderedAddMonoid Real.instIsOrderedRing Real.instNontrivial Int.cast_neg_natCast le_trans IsOrderedAddMonoid.toAddLeftMono covariant_swap_add_of_covariant_add pi_norm_lt_iff Nat.cast_pos le_of_lt Metric.ball_subset_ball Nat.le_ceil

BoxIntegral.unitPartition

Definitions

Name	Category	Theorems
admissibleIndex 📖	CompOp	4 math math: mem_prepartition_boxes_iff, mem_admissibleIndex_iff, mem_admissibleIndex_of_mem_box, mem_prepartition_iff
box 📖	CompOp	17 math math: mem_box_iff', prepartition_tag, box_upper, mem_prepartition_boxes_iff, mem_admissibleIndex_iff, tag_mem, box_injective, mem_box_iff, box_index_tag_eq_self, disjoint, box_lower, setFinite_index, mem_prepartition_iff, mem_box_iff_index, volume_box, box.upper_sub_lower, diam_boxIcc
index 📖	CompOp	6 math math: index_tag, mem_admissibleIndex_of_mem_box, box_index_tag_eq_self, index_apply, mem_box_iff_index, tag_index_eq_self_of_mem_smul_span
prepartition 📖	CompOp	7 math math: prepartition_tag, mem_prepartition_boxes_iff, prepartition_isSubordinate, integralSum_eq_tsum_div, prepartition_isPartition, mem_prepartition_iff, prepartition_isHenstock
tag 📖	CompOp	7 math math: tag_injective, prepartition_tag, tag_mem, index_tag, tag_apply, tag_index_eq_self_of_mem_smul_span, tag_mem_smul_span

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
box_index_tag_eq_self 📖	mathematical	BoxIntegral.Box Finset Finset.instMembership BoxIntegral.Prepartition.boxes BoxIntegral.TaggedPrepartition.toPrepartition prepartition	box index BoxIntegral.TaggedPrepartition.tag	—	mem_prepartition_boxes_iff prepartition_tag index_tag
box_injective 📖	mathematical	—	BoxIntegral.Box box	—	Mathlib.Tactic.Contrapose.contrapose₁ BoxIntegral.Box.ne_of_disjoint_coe disjoint
box_lower 📖	mathematical	—	BoxIntegral.Box.lower box Real DivInvMonoid.toDiv Real.instDivInvMonoid Real.instIntCast Real.instNatCast	—	—
box_upper 📖	mathematical	—	BoxIntegral.Box.upper box Real DivInvMonoid.toDiv Real.instDivInvMonoid Real.instAdd Real.instIntCast Real.instOne Real.instNatCast	—	—
diam_boxIcc 📖	mathematical	—	Real Real.instLE Metric.diam pseudoMetricSpacePi Real.pseudoMetricSpace DFunLike.coe OrderEmbedding BoxIntegral.Box Set BoxIntegral.Box.instLE Set.instLE instFunLikeOrderEmbedding BoxIntegral.Box.Icc box DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne Real.instNatCast	—	BoxIntegral.Box.Icc_eq_pi ENNReal.toReal_le_of_le_ofReal Mathlib.Meta.Positivity.div_nonneg_of_pos_of_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Nat.cast_nonneg' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass Metric.ediam_pi_le_of_le Real.ediam_Icc box.upper_sub_lower
disjoint 📖	mathematical	—	Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice BoxIntegral.Box.toSet box	—	not_iff_comm Set.not_disjoint_iff mem_box_iff_index tag_mem
eq_of_mem_smul_span_of_index_eq_index 📖	—	Submodule Int.instSemiring Pi.addCommMonoid Real Real.instAddCommMonoid AddCommGroup.toIntModule Pi.addCommGroup Real.instAddCommGroup SetLike.instMembership Submodule.setLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne Submodule.instAddCommMonoidWithOne Pi.semiring Real.semiring DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Submodule.pointwiseDistribMulAction Pi.distribMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal AddGroup.int_smulCommClass' Pi.addGroup Real.instAddGroup Pi.distribSMul Real.instAddMonoid NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.instInv Real.instNatCast Submodule.span Set.range DFunLike.coe Module.Basis NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.Function.module Semiring.toModule Module.Basis.instFunLike Pi.basisFun index	—	—	AddGroup.int_smulCommClass' tag_index_eq_self_of_mem_smul_span
index_apply 📖	mathematical	—	index Int.ceil Real Real.instRing Real.linearOrder Real.instFloorRing Real.instMul Real.instNatCast	—	—
index_tag 📖	mathematical	—	index tag	—	mem_box_iff_index tag_mem
integralSum_eq_tsum_div 📖	mathematical	BoxIntegral.hasIntegralVertices Set Set.instLE BoxIntegral.Box.toSet	BoxIntegral.integralSum Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Set.indicator Real.instZero BoxIntegral.BoxAdditiveMap.toSMul Top.top WithTop BoxIntegral.Box WithTop.top 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 FiniteDimensional.rclike_to_real Real.measurableSpace Real.borelSpace SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace instIsTopologicalAddGroupReal TopologicalSpace.SecondCountableTopology.to_separableSpace instSecondCountableTopologyReal instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper instProperSpaceReal Real.locallyFinite_volume prepartition DivInvMonoid.toDiv Real.instDivInvMonoid tsum Set.Elem Set.instInter Set.smulSet Function.hasSMul Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Real.instInv Real.instNatCast SetLike.coe Submodule Int.instSemiring Pi.addCommMonoid Real.instAddCommMonoid AddCommGroup.toIntModule Pi.addCommGroup Real.instAddCommGroup Submodule.setLike Submodule.span Set.range DFunLike.coe Module.Basis Real.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.Function.module Semiring.toModule Module.Basis.instFunLike Pi.basisFun Set.instMembership SummationFilter.unconditional Monoid.toNatPow Real.instMonoid Fintype.card	—	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 AddGroup.int_smulCommClass' Submodule.coe_pointwise_smul Ne.isUnit inv_ne_zero NeZero.charZero RCLike.charZero_rclike ZSpan.smul ZSpan.setFinite_inter pi_properSpace Bornology.IsBounded.subset BoxIntegral.Box.isBounded tsum_fintype SummationFilter.instLeAtTopUnconditional Finset.sum_set_coe Finset.sum_div Finset.sum_congr Set.indicator_apply MulZeroClass.mul_zero Finset.sum_ite Finset.sum_const_zero add_zero Finset.sum_bij Finset.mem_filter mem_prepartition_boxes_iff mem_admissibleIndex_of_mem_box Set.mem_toFinset prepartition_tag tag_index_eq_self_of_mem_smul_span eq_of_mem_smul_span_of_index_eq_index box_injective box_index_tag_eq_self tag_mem_smul_span MeasureTheory.measureReal_def volume_box ENNReal.toReal_div ENNReal.toReal_one ENNReal.toReal_pow ENNReal.toReal_natCast mul_comm_div one_mul
mem_admissibleIndex_iff 📖	mathematical	—	Finset Finset.instMembership admissibleIndex BoxIntegral.Box BoxIntegral.Box.instLE box	—	admissibleIndex.eq_1 Set.Finite.mem_toFinset Set.mem_setOf_eq BoxIntegral.Box.coe_subset_coe
mem_admissibleIndex_of_mem_box 📖	mathematical	BoxIntegral.hasIntegralVertices BoxIntegral.Box BoxIntegral.Box.instMembershipForallReal	Finset Finset.instMembership admissibleIndex index	—	Int.cast_sub Int.cast_one
mem_box_iff 📖	mathematical	—	BoxIntegral.Box BoxIntegral.Box.instMembershipForallReal box Real Real.instLT DivInvMonoid.toDiv Real.instDivInvMonoid Real.instIntCast Real.instNatCast Real.instLE Real.instAdd Real.instOne	—	—
mem_box_iff' 📖	mathematical	—	BoxIntegral.Box BoxIntegral.Box.instMembershipForallReal box Real Real.instLT Real.instIntCast Real.instMul Real.instNatCast Real.instLE Real.instAdd Real.instOne	—	Nat.cast_pos Real.instIsOrderedRing Real.instNontrivial le_div_iff₀' PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing div_lt_iff₀'
mem_box_iff_index 📖	mathematical	—	BoxIntegral.Box BoxIntegral.Box.instMembershipForallReal box index	—	Int.cast_add Int.cast_one add_sub_cancel_right
mem_prepartition_boxes_iff 📖	mathematical	—	BoxIntegral.Box Finset Finset.instMembership BoxIntegral.Prepartition.boxes BoxIntegral.TaggedPrepartition.toPrepartition prepartition admissibleIndex box	—	mem_prepartition_iff
mem_prepartition_iff 📖	mathematical	—	BoxIntegral.Box BoxIntegral.TaggedPrepartition BoxIntegral.TaggedPrepartition.instMembershipBox prepartition Finset Finset.instMembership admissibleIndex box	—	BoxIntegral.Box.exists_mem prepartition.eq_1 Finset.mem_image
mem_smul_span_iff 📖	mathematical	—	Submodule Int.instSemiring Pi.addCommMonoid Real Real.instAddCommMonoid AddCommGroup.toIntModule Pi.addCommGroup Real.instAddCommGroup SetLike.instMembership Submodule.setLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne Submodule.instAddCommMonoidWithOne Pi.semiring Real.semiring DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Submodule.pointwiseDistribMulAction Pi.distribMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal AddGroup.int_smulCommClass' Pi.addGroup Real.instAddGroup Pi.distribSMul Real.instAddMonoid NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.instInv Real.instNatCast Submodule.span Set.range DFunLike.coe Module.Basis NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.Function.module Semiring.toModule Module.Basis.instFunLike Pi.basisFun Set Set.instMembership RingHom CommSemiring.toSemiring Int.instCommSemiring RingHom.instFunLike algebraMap Ring.toIntAlgebra Real.instRing Real.instMul	—	AddGroup.int_smulCommClass' Ne.isUnit inv_ne_zero NeZero.charZero RCLike.charZero_rclike ZSpan.smul RingHomInvPair.ids Module.Basis.mem_span_iff_repr_mem Int.instIsDomain Real.instNontrivial AddCommGroup.intIsScalarTower instIsTorsionFreeIntOfIsAddTorsionFree instIsAddTorsionFreeOfAddLeftStrictMonoOfAddRightStrictMono IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add Module.Basis.repr_isUnitSMul Pi.basisFun_repr Units.val_inv_eq_inv_val inv_inv
prepartition_isHenstock 📖	mathematical	—	BoxIntegral.TaggedPrepartition.IsHenstock prepartition	—	mem_prepartition_iff prepartition_tag BoxIntegral.Box.coe_subset_Icc tag_mem
prepartition_isPartition 📖	mathematical	BoxIntegral.hasIntegralVertices	BoxIntegral.TaggedPrepartition.IsPartition prepartition	—	BoxIntegral.TaggedPrepartition.mem_toPrepartition mem_prepartition_iff mem_admissibleIndex_of_mem_box mem_box_iff_index
prepartition_isSubordinate 📖	mathematical	Real Real.instLT Real.instZero Real.instLE DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne Real.instNatCast	BoxIntegral.TaggedPrepartition.IsSubordinate prepartition Set Set.instMembership Set.Ioi Real.instPreorder	—	mem_prepartition_iff le_trans Metric.dist_le_diam_of_mem BoxIntegral.Box.isBounded_Icc Finite.of_fintype prepartition_tag BoxIntegral.Box.coe_subset_Icc tag_mem diam_boxIcc
prepartition_tag 📖	mathematical	Finset Finset.instMembership admissibleIndex	BoxIntegral.TaggedPrepartition.tag prepartition box tag	—	BoxIntegral.Box.exists_mem tag_injective box_injective
setFinite_index 📖	mathematical	MeasureTheory.NullMeasurableSet MeasurableSpace.pi Real Real.measurableSpace MeasureTheory.MeasureSpace.volume MeasureTheory.MeasureSpace.pi Real.measureSpace	Set.Finite setOf Set Set.instHasSubset BoxIntegral.Box.toSet box	—	Set.Finite.subset MeasureTheory.Measure.finite_const_le_meas_of_disjoint_iUnion₀ one_div MeasureTheory.NullMeasurableSet.inter MeasurableSet.nullMeasurableSet BoxIntegral.Box.measurableSet_coe Finite.to_countable Finite.of_fintype Disjoint.aedisjoint Disjoint.inter_left Disjoint.inter_right disjoint lt_top_iff_ne_top MeasureTheory.measure_lt_top_of_subset Set.mem_setOf Set.inter_eq_self_of_subset_left volume_box le_refl
tag_apply 📖	mathematical	—	tag Real DivInvMonoid.toDiv Real.instDivInvMonoid Real.instAdd Real.instIntCast Real.instOne Real.instNatCast	—	—
tag_index_eq_self_of_mem_smul_span 📖	mathematical	Submodule Int.instSemiring Pi.addCommMonoid Real Real.instAddCommMonoid AddCommGroup.toIntModule Pi.addCommGroup Real.instAddCommGroup SetLike.instMembership Submodule.setLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne Submodule.instAddCommMonoidWithOne Pi.semiring Real.semiring DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Submodule.pointwiseDistribMulAction Pi.distribMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal AddGroup.int_smulCommClass' Pi.addGroup Real.instAddGroup Pi.distribSMul Real.instAddMonoid NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.instInv Real.instNatCast Submodule.span Set.range DFunLike.coe Module.Basis NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.Function.module Semiring.toModule Module.Basis.instFunLike Pi.basisFun	tag index	—	AddGroup.int_smulCommClass' mem_smul_span_iff tag_apply index_apply Int.cast_sub Int.cast_one sub_add_cancel Int.ceil_intCast Real.instIsStrictOrderedRing div_eq_iff NeZero.charZero RCLike.charZero_rclike mul_comm
tag_injective 📖	mathematical	—	tag	—	RCLike.charZero_rclike AddRightCancelSemigroup.toIsRightCancelAdd div_left_inj' Nat.cast_ne_zero
tag_mem 📖	mathematical	—	BoxIntegral.Box BoxIntegral.Box.instMembershipForallReal box tag	—	mem_box_iff tag.eq_1 add_div Nat.cast_pos Real.instIsOrderedRing Real.instNontrivial lt_add_of_pos_right IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Mathlib.Meta.Positivity.pos_of_isNat Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one le_rfl
tag_mem_smul_span 📖	mathematical	—	Submodule Int.instSemiring Pi.addCommMonoid Real Real.instAddCommMonoid AddCommGroup.toIntModule Pi.addCommGroup Real.instAddCommGroup SetLike.instMembership Submodule.setLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne Submodule.instAddCommMonoidWithOne Pi.semiring Real.semiring DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Submodule.pointwiseDistribMulAction Pi.distribMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal AddGroup.int_smulCommClass' Pi.addGroup Real.instAddGroup Pi.distribSMul Real.instAddMonoid NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.instInv Real.instNatCast Submodule.span Set.range DFunLike.coe Module.Basis NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.Function.module Semiring.toModule Module.Basis.instFunLike Pi.basisFun tag	—	AddGroup.int_smulCommClass' mem_smul_span_iff tag_apply div_eq_inv_mul mul_assoc mul_inv_cancel_of_invertible RCLike.charZero_rclike one_mul map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass eq_intCast
volume_box 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.MeasureSpace.pi Real Real.measureSpace Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.MeasureSpace.volume BoxIntegral.Box.toSet box DivInvMonoid.toDiv ENNReal.instDivInvMonoid AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring ENNReal.instCommSemiring AddMonoidWithOne.toNatCast Fintype.card	—	BoxIntegral.Box.coe_eq_pi MeasureTheory.Measure.pi_pi MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite instIsAddHaarMeasureVolume FiniteDimensional.rclike_to_real Real.borelSpace SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace instIsTopologicalAddGroupReal TopologicalSpace.SecondCountableTopology.to_separableSpace instSecondCountableTopologyReal instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper instProperSpaceReal Finset.prod_congr Real.volume_Ioc box.upper_sub_lower Finset.prod_const ENNReal.ofReal_div_of_pos Nat.cast_pos Real.instIsOrderedRing Real.instNontrivial ENNReal.ofReal_one ENNReal.ofReal_natCast one_div ENNReal.inv_pow

BoxIntegral.unitPartition.box

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
upper_sub_lower 📖	mathematical	—	Real Real.instSub BoxIntegral.Box.upper BoxIntegral.unitPartition.box BoxIntegral.Box.lower DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne Real.instNatCast	—	add_div add_sub_cancel_left

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tendsto_card_div_pow_atTop_volume 📖	mathematical	Bornology.IsBounded Pi.instBornology Real PseudoMetricSpace.toBornology Real.pseudoMetricSpace MeasurableSet MeasurableSpace.pi Real.measurableSpace DFunLike.coe MeasureTheory.Measure MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.MeasureSpace.pi Real.measureSpace Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.MeasureSpace.volume frontier Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace instZeroENNReal	Filter.Tendsto DivInvMonoid.toDiv Real.instDivInvMonoid Real.instNatCast Nat.card Set.Elem Set.instInter Set.smulSet Function.hasSMul Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Real.instInv SetLike.coe Submodule Int.instSemiring Pi.addCommMonoid Real.instAddCommMonoid AddCommGroup.toIntModule Pi.addCommGroup Real.instAddCommGroup Submodule.setLike Submodule.span Set.range Module.Basis Real.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.Function.module Semiring.toModule Module.Basis.instFunLike Pi.basisFun Finite.of_fintype Monoid.toNatPow Real.instMonoid Fintype.card Filter.atTop Nat.instPreorder nhds MeasureTheory.Measure.real	—	Finite.of_fintype tsum_const instIsTopologicalAddGroupReal TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace nsmul_eq_mul mul_one RCLike.charZero_rclike MeasureTheory.setIntegral_const Real.instCompleteSpace smul_eq_mul tendsto_tsum_div_pow_atTop_integral continuous_const
tendsto_card_div_pow_atTop_volume' 📖	mathematical	Bornology.IsBounded Pi.instBornology Real PseudoMetricSpace.toBornology Real.pseudoMetricSpace MeasurableSet MeasurableSpace.pi Real.measurableSpace DFunLike.coe MeasureTheory.Measure MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.MeasureSpace.pi Real.measureSpace Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.MeasureSpace.volume frontier Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace instZeroENNReal Set.instHasSubset Set.smulSet Function.hasSMul Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id	Filter.Tendsto DivInvMonoid.toDiv Real.instDivInvMonoid Real.instNatCast Nat.card Set.Elem Set.instInter Real.instInv SetLike.coe Submodule Int.instSemiring Pi.addCommMonoid Real.instAddCommMonoid AddCommGroup.toIntModule Pi.addCommGroup Real.instAddCommGroup Submodule.setLike Submodule.span Set.range Module.Basis Real.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.Function.module Semiring.toModule Module.Basis.instFunLike Pi.basisFun Finite.of_fintype Monoid.toNatPow Real.instMonoid Fintype.card Filter.atTop Real.instPreorder nhds MeasureTheory.Measure.real	—	Finite.of_fintype Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_left tendsto_of_tendsto_of_tendsto_of_le_of_le' instOrderTopologyReal Real.instIsStrictOrderedRing Filter.Tendsto.congr' Filter.Tendsto.mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Filter.Tendsto.comp tendsto_card_div_pow_atTop_volume tendsto_nat_floor_atTop Filter.Tendsto.pow tendsto_nat_floor_div_atTop tendsto_nat_ceil_atTop tendsto_nat_ceil_div_atTop
tendsto_tsum_div_pow_atTop_integral 📖	mathematical	Continuous Real Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Bornology.IsBounded Pi.instBornology PseudoMetricSpace.toBornology MeasurableSet MeasurableSpace.pi Real.measurableSpace DFunLike.coe MeasureTheory.Measure MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.MeasureSpace.pi Real.measureSpace Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.MeasureSpace.volume frontier instZeroENNReal	Filter.Tendsto DivInvMonoid.toDiv Real.instDivInvMonoid tsum Set.Elem Set.instInter Set.smulSet Function.hasSMul Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Real.instInv Real.instNatCast SetLike.coe Submodule Int.instSemiring Pi.addCommMonoid Real.instAddCommMonoid AddCommGroup.toIntModule Pi.addCommGroup Real.instAddCommGroup Submodule.setLike Submodule.span Set.range Module.Basis Real.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.Function.module Semiring.toModule Module.Basis.instFunLike Pi.basisFun Finite.of_fintype Set.instMembership SummationFilter.unconditional Monoid.toNatPow Real.instMonoid Fintype.card Filter.atTop Nat.instPreorder nhds MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.Measure.restrict	—	Finite.of_fintype BoxIntegral.le_hasIntegralVertices_of_isBounded Metric.tendsto_atTop IsCompact.exists_bound_of_continuousOn BoxIntegral.Box.isCompact_Icc Continuous.continuousOn Set.indicator.eq_1 le_max_of_le_right Eq.trans_le norm_zero le_max_left MeasureTheory.Measure.instOuterMeasureClass Filter.mp_mem MeasureTheory.compl_mem_ae_iff Filter.univ_mem' ContinuousOn.continuousAt_indicator 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 Nat.instAtLeastTwoHAddOfNat BoxIntegral.hasIntegral_iff MeasureTheory.AEContinuous.hasBoxIntegral Real.instCompleteSpace half_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing lt_of_le_of_lt LT.lt.trans_le Nat.ceil_pos inv_pos Subtype.prop BoxIntegral.unitPartition.integralSum_eq_tsum_div MeasureTheory.Measure.restrict_restrict_of_subset MeasureTheory.integral_indicator BoxIntegral.unitPartition.prepartition_isSubordinate one_div inv_le_comm₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Nat.cast_zero IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass RCLike.charZero_rclike le_trans Nat.le_ceil Nat.cast_le BoxIntegral.unitPartition.prepartition_isHenstock BoxIntegral.unitPartition.prepartition_isPartition half_lt_self_iff

---

← Back to Index