Integral

📁 Source: Mathlib/MeasureTheory/Group/Integral.lean

Statistics

Metric	Count
Definitions	0
Theorems comp_add_left, comp_add_right, comp_div_left, comp_div_right, comp_inv, comp_mul_left, comp_mul_right, comp_neg, comp_sub_left, comp_sub_right, comp_inv, comp_inv_Ici, comp_inv_Iic, comp_inv_Iio, comp_inv_Ioi, comp_neg, comp_neg_Ici, comp_neg_Iic, comp_neg_Iio, comp_neg_Ioi, integrable_comp_div_left, integrable_comp_sub_left, integral_add_left_eq_self, integral_add_right_eq_self, integral_div_left_eq_self, integral_div_right_eq_self, integral_eq_zero_of_add_left_eq_neg, integral_eq_zero_of_add_right_eq_neg, integral_eq_zero_of_mul_left_eq_neg, integral_eq_zero_of_mul_right_eq_neg, integral_inv_eq_self, integral_mul_left_eq_self, integral_mul_right_eq_self, integral_neg_eq_self, integral_smul_eq_self, integral_sub_left_eq_self, integral_sub_right_eq_self, integral_vadd_eq_self	38
Total	38

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
integrable_comp_div_left 📖	mathematical	—	Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup DivInvMonoid.toDiv Group.toDivInvMonoid	—	div_inv_eq_mul mul_inv_cancel_left Integrable.comp_mul_left Integrable.comp_inv Integrable.comp_div_left
integrable_comp_sub_left 📖	mathematical	—	Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	sub_neg_eq_add add_neg_cancel_left Integrable.comp_add_left Integrable.comp_neg Integrable.comp_sub_left
integral_add_left_eq_self 📖	mathematical	—	integral AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	MeasurableEquiv.measurableEmbedding MeasurableEmbedding.integral_map map_add_left_eq_self
integral_add_right_eq_self 📖	mathematical	—	integral AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	MeasurableEquiv.measurableEmbedding MeasurableEmbedding.integral_map map_add_right_eq_self
integral_div_left_eq_self 📖	mathematical	—	integral DivInvMonoid.toDiv Group.toDivInvMonoid	—	div_eq_mul_inv integral_inv_eq_self integral_mul_left_eq_self
integral_div_right_eq_self 📖	mathematical	—	integral DivInvMonoid.toDiv Group.toDivInvMonoid	—	div_eq_mul_inv integral_mul_right_eq_self
integral_eq_zero_of_add_left_eq_neg 📖	mathematical	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	integral NegZeroClass.toZero	—	IsAddTorsionFree.of_isTorsionFree instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors Real.instIsDomain GroupWithZero.toNoZeroSMulDivisors IsDomain.toIsCancelMulZero RCLike.charZero_rclike self_eq_neg integral_neg integral_add_left_eq_self
integral_eq_zero_of_add_right_eq_neg 📖	mathematical	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	integral NegZeroClass.toZero	—	IsAddTorsionFree.of_isTorsionFree instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors Real.instIsDomain GroupWithZero.toNoZeroSMulDivisors IsDomain.toIsCancelMulZero RCLike.charZero_rclike self_eq_neg integral_neg integral_add_right_eq_self
integral_eq_zero_of_mul_left_eq_neg 📖	mathematical	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	integral NegZeroClass.toZero	—	IsAddTorsionFree.of_isTorsionFree instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors Real.instIsDomain GroupWithZero.toNoZeroSMulDivisors IsDomain.toIsCancelMulZero RCLike.charZero_rclike integral_mul_left_eq_self
integral_eq_zero_of_mul_right_eq_neg 📖	mathematical	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	integral NegZeroClass.toZero	—	IsAddTorsionFree.of_isTorsionFree instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors Real.instIsDomain GroupWithZero.toNoZeroSMulDivisors IsDomain.toIsCancelMulZero RCLike.charZero_rclike integral_mul_right_eq_self
integral_inv_eq_self 📖	mathematical	—	integral InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	MeasurableEquiv.measurableEmbedding MeasurableEmbedding.integral_map Measure.map_inv_eq_self
integral_mul_left_eq_self 📖	mathematical	—	integral MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	MeasurableEquiv.measurableEmbedding MeasurableEmbedding.integral_map map_mul_left_eq_self
integral_mul_right_eq_self 📖	mathematical	—	integral MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	MeasurableEquiv.measurableEmbedding MeasurableEmbedding.integral_map map_mul_right_eq_self
integral_neg_eq_self 📖	mathematical	—	integral NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	MeasurableEquiv.measurableEmbedding MeasurableEmbedding.integral_map Measure.map_neg_eq_self
integral_smul_eq_self 📖	mathematical	—	integral SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction	—	MeasurableEquiv.measurableEmbedding MeasurableEmbedding.integral_map map_smul
integral_sub_left_eq_self 📖	mathematical	—	integral SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	sub_eq_add_neg integral_neg_eq_self integral_add_left_eq_self
integral_sub_right_eq_self 📖	mathematical	—	integral SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	sub_eq_add_neg integral_add_right_eq_self
integral_vadd_eq_self 📖	mathematical	—	integral HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction	—	MeasurableEquiv.measurableEmbedding MeasurableEmbedding.integral_map map_vadd

MeasureTheory.Integrable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_add_left 📖	mathematical	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	comp_measurable mono_measure Eq.le MeasureTheory.map_add_left_eq_self MeasurableAdd.measurable_const_add
comp_add_right 📖	mathematical	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	comp_measurable mono_measure Eq.le MeasureTheory.map_add_right_eq_self MeasurableAdd.measurable_add_const
comp_div_left 📖	mathematical	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	DivInvMonoid.toDiv Group.toDivInvMonoid	—	MeasureTheory.MeasurePreserving.integrable_comp MeasureTheory.Measure.measurePreserving_div_left aestronglyMeasurable
comp_div_right 📖	mathematical	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	DivInvMonoid.toDiv Group.toDivInvMonoid	—	div_eq_mul_inv comp_mul_right
comp_inv 📖	mathematical	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	comp_measurable mono_measure Eq.le MeasureTheory.Measure.map_inv_eq_self MeasurableInv.measurable_inv
comp_mul_left 📖	mathematical	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	comp_measurable mono_measure Eq.le MeasureTheory.map_mul_left_eq_self MeasurableMul.measurable_const_mul
comp_mul_right 📖	mathematical	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	comp_measurable mono_measure Eq.le MeasureTheory.map_mul_right_eq_self MeasurableMul.measurable_mul_const
comp_neg 📖	mathematical	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	comp_measurable mono_measure Eq.le MeasureTheory.Measure.map_neg_eq_self MeasurableNeg.measurable_neg
comp_sub_left 📖	mathematical	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	MeasureTheory.MeasurePreserving.integrable_comp MeasureTheory.Measure.measurePreserving_sub_left aestronglyMeasurable
comp_sub_right 📖	mathematical	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	sub_eq_add_neg comp_add_right

MeasureTheory.IntegrableOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_inv 📖	mathematical	MeasureTheory.IntegrableOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid Set InvolutiveInv.toInv Set.involutiveInv DivisionMonoid.toInvolutiveInv	—	MeasureTheory.integrable_map_equiv MeasurableEquiv.restrict_map MeasureTheory.Measure.map_inv_eq_self
comp_inv_Ici 📖	mathematical	MeasureTheory.IntegrableOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Set.Iic PartialOrder.toPreorder InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid	Set.Ici	—	Set.inv_Iic inv_inv comp_inv
comp_inv_Iic 📖	mathematical	MeasureTheory.IntegrableOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Set.Ici PartialOrder.toPreorder InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid	Set.Iic	—	Set.inv_Ici inv_inv comp_inv
comp_inv_Iio 📖	mathematical	MeasureTheory.IntegrableOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Set.Ioi PartialOrder.toPreorder InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid	Set.Iio	—	Set.inv_Ioi inv_inv comp_inv
comp_inv_Ioi 📖	mathematical	MeasureTheory.IntegrableOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Set.Iio PartialOrder.toPreorder InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid	Set.Ioi	—	Set.inv_Iio inv_inv comp_inv
comp_neg 📖	mathematical	MeasureTheory.IntegrableOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid Set InvolutiveNeg.toNeg Set.involutiveNeg SubtractionMonoid.toInvolutiveNeg	—	MeasureTheory.integrable_map_equiv MeasurableEquiv.restrict_map MeasureTheory.Measure.map_neg_eq_self
comp_neg_Ici 📖	mathematical	MeasureTheory.IntegrableOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Set.Iic PartialOrder.toPreorder NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	Set.Ici	—	Set.neg_Iic neg_neg comp_neg
comp_neg_Iic 📖	mathematical	MeasureTheory.IntegrableOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Set.Ici PartialOrder.toPreorder NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	Set.Iic	—	Set.neg_Ici neg_neg comp_neg
comp_neg_Iio 📖	mathematical	MeasureTheory.IntegrableOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Set.Ioi PartialOrder.toPreorder NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	Set.Iio	—	Set.neg_Ioi neg_neg comp_neg
comp_neg_Ioi 📖	mathematical	MeasureTheory.IntegrableOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Set.Iio PartialOrder.toPreorder NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	Set.Ioi	—	Set.neg_Iio neg_neg comp_neg

---

← Back to Index