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 instSeparatelyContinuousAddOfContinuousAdd IsSemitopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing normedCommRing IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal instIntCast SummationFilter.unconditional	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Real MeasureTheory.MeasureSpace.toMeasurableSpace measureSpace DFunLike.coe ContinuousMap pseudoMetricSpace ContinuousMap.instFunLike MeasureTheory.MeasureSpace.volume	—	compactSpace_Icc ConditionallyCompleteLinearOrder.toCompactIccSpace instOrderTopologyReal instSeparatelyContinuousAddOfContinuousAdd IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing 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 instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE instIsOrderedCancelAddMonoid 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 IsSemitopologicalRing.toContinuousNeg IsTopologicalRing.toIsSemitopologicalRing 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 IsSemitopologicalRing.toContinuousNeg IsTopologicalRing.toIsSemitopologicalRing 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 Real 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 MeasureTheory.Measure Real 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	—	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.IntegrableOn.sub

---

← Back to Index