IntegralConvolution

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

Statistics

Metric	Count
Definitions	0
Theorems integrable_conv_iff, integrable_mconv_iff, integral_conv, integral_mconv	4
Total	4

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
integrable_conv_iff 📖	mathematical	AEStronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Measure.conv	Integrable SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Filter.Eventually AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass ae Measure Measure.instFunLike Measure.instOuterMeasureClass Real Real.pseudoMetricSpace NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Norm.norm NormedAddCommGroup.toNorm	—	Measure.instOuterMeasureClass integrable_map_measure AEMeasurable.add AEMeasurable.fst aemeasurable_id AEMeasurable.snd integrable_prod_iff AEStronglyMeasurable.comp_measurable Measurable.add Measurable.fst measurable_id' Measurable.snd
integrable_mconv_iff 📖	mathematical	AEStronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Measure.mconv	Integrable SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Filter.Eventually MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass ae Measure Measure.instFunLike Measure.instOuterMeasureClass Real Real.pseudoMetricSpace NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Norm.norm NormedAddCommGroup.toNorm	—	Measure.instOuterMeasureClass integrable_map_measure AEMeasurable.mul AEMeasurable.fst aemeasurable_id AEMeasurable.snd integrable_prod_iff AEStronglyMeasurable.comp_measurable Measurable.mul Measurable.fst measurable_id' Measurable.snd
integral_conv 📖	mathematical	Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Measure.conv	integral AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	integral_map AEMeasurable.add AEMeasurable.fst aemeasurable_id AEMeasurable.snd integral_prod integrable_map_measure
integral_mconv 📖	mathematical	Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Measure.mconv	integral MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	—	integral_map AEMeasurable.mul AEMeasurable.fst aemeasurable_id AEMeasurable.snd integral_prod integrable_map_measure

---

← Back to Index