Documentation Verification Report

SumMeasure

📁 Source: Mathlib/MeasureTheory/Integral/Bochner/SumMeasure.lean

Statistics

Metric	Count
Definitions	0
Theorems `summable_integral`, `summable_of_dirac`, `hasSum_integral_measure`, `hasSum_integral_sum_dirac`, `integrable_sum_dirac`, `integrable_sum_dirac_iff`, `integrable_sum_measure`, `integrable_sum_measure_iff`, `integral_count`, `integral_countable`, `integral_countable'`, `integral_finset`, `integral_fintype`, `integral_sum_dirac`, `integral_sum_dirac_eq_tsum`, `integral_sum_measure`, `setIntegral_countable`, `setIntegral_finset`	18
Total	18

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasSum_integral_measure` 📖	mathematical	`Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Measure.sum`	`HasSum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `integral` `Measure.sum` `SummationFilter.unconditional`	—	`Integrable.mono_measure` `Measure.le_sum` `Finset.sum_congr` `integral_finset_sum_measure` `Filter.HasBasis.tendsto_right_iff` `Metric.nhds_basis_ball` `CanLift.prf` `NNReal.canLift` `LT.lt.le` `Filter.Tendsto.add` `ENNReal.instContinuousAdd` `Filter.tendsto_id` `tendsto_const_nhds` `lt_mem_nhds` `ENNReal.instOrderTopology` `ENNReal.lt_add_right` `LT.lt.ne` `ENNReal.coe_ne_zero` `NNReal.coe_ne_zero` `LT.lt.ne'` `Filter.Eventually.mono` `Filter.Tendsto.eventually` `hasSum_lintegral_measure` `Measure.sum_add_sum_compl` `Metric.mem_ball` `coe_nndist` `NNReal.coe_lt_coe` `ENNReal.coe_lt_coe` `LE.le.trans_lt` `nndist_integral_add_measure_le_lintegral` `integrable_add_measure` `PseudoEMetricSpace.pseudoMetrizableSpace` `lt_of_add_lt_add_left` `ENNReal.addLeftReflectLT` `lintegral_finset_sum_measure` `lintegral_add_measure`
`hasSum_integral_sum_dirac` 📖	mathematical	`Summable` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instMul` `ENNReal.toReal` `Norm.norm` `NormedAddCommGroup.toNorm` `SummationFilter.unconditional`	`HasSum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Real` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `NormedSpace.toModule` `Real.normedField` `ENNReal.toReal` `integral` `Measure.sum` `ENNReal` `Measure` `Measure.instSMul` `Algebra.toSMul` `ENNReal.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.right` `Measure.dirac` `SummationFilter.unconditional`	—	`IsScalarTower.right` `integral_smul_measure` `integral_dirac` `hasSum_integral_measure` `integrable_sum_dirac`
`integrable_sum_dirac` 📖	mathematical	`Summable` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instMul` `ENNReal.toReal` `Norm.norm` `NormedAddCommGroup.toNorm` `SummationFilter.unconditional`	`Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Measure.sum` `ENNReal` `Measure` `Measure.instSMul` `Algebra.toSMul` `ENNReal.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.right` `Measure.dirac`	—	`integrable_sum_measure` `IsScalarTower.right` `Integrable.smul_measure` `integrable_dirac` `integral_smul_measure` `integral_dirac` `Real.instCompleteSpace`
`integrable_sum_dirac_iff` 📖	mathematical	—	`Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Measure.sum` `ENNReal` `Measure` `Measure.instSMul` `Algebra.toSMul` `ENNReal.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.right` `Measure.dirac` `Summable` `Real` `Real.instAddCommMonoid` `Real.pseudoMetricSpace` `Real.instMul` `ENNReal.toReal` `Norm.norm` `NormedAddCommGroup.toNorm` `SummationFilter.unconditional`	—	`IsScalarTower.right` `Integrable.summable_of_dirac` `integrable_sum_dirac`
`integrable_sum_measure` 📖	mathematical	`Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Summable` `Real` `Real.instAddCommMonoid` `Real.pseudoMetricSpace` `integral` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `Real.normedField` `Norm.norm` `NormedAddCommGroup.toNorm` `SummationFilter.unconditional`	`Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Measure.sum`	—	`aestronglyMeasurable_sum_measure_iff` `PseudoEMetricSpace.pseudoMetrizableSpace` `Integrable.aestronglyMeasurable` `HasFiniteIntegral.eq_1` `lintegral_sum_measure` `ofReal_integral_eq_lintegral_ofReal` `Integrable.norm` `ae_of_all` `Measure.instOuterMeasureClass` `norm_nonneg` `ofReal_norm_eq_enorm` `Summable.tsum_ofReal_lt_top`
`integrable_sum_measure_iff` 📖	mathematical	—	`Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Measure.sum` `Summable` `Real` `Real.instAddCommMonoid` `Real.pseudoMetricSpace` `integral` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `Real.normedField` `Norm.norm` `NormedAddCommGroup.toNorm` `SummationFilter.unconditional`	—	`Integrable.mono_measure` `Measure.le_sum` `Integrable.summable_integral` `integrable_sum_measure`
`integral_count` 📖	mathematical	—	`integral` `Measure.count` `Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Finset.univ`	—	`integral_fintype` `Finite.of_fintype` `Measure.count.isFiniteMeasure` `Finset.sum_congr` `count_real_singleton'` `one_smul`
`integral_countable` 📖	mathematical	`Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`integral` `tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Real` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `NormedSpace.toModule` `Real.normedField` `Measure.real` `Set` `Set.instSingletonSet` `SummationFilter.unconditional`	—	`IsScalarTower.right` `Measure.sum_smul_dirac` `integral_sum_measure` `integral_smul_measure` `integral_dirac` `measureReal_def`
`integral_countable'` 📖	mathematical	`Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`integral` `tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Real` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `NormedSpace.toModule` `Real.normedField` `Measure.real` `Set` `Set.instSingletonSet` `SummationFilter.unconditional`	—	`integral_countable`
`integral_finset` 📖	mathematical	`IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `SetLike.coe` `Finset` `Finset.instSetLike`	`integral` `Measure.restrict` `SetLike.coe` `Finset` `Finset.instSetLike` `Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Real` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `NormedSpace.toModule` `Real.normedField` `Measure.real` `Set` `Set.instSingletonSet`	—	`setIntegral_finset`
`integral_fintype` 📖	mathematical	`Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`integral` `Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Finset.univ` `Real` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `NormedSpace.toModule` `Real.normedField` `Measure.real` `Set` `Set.instSingletonSet`	—	`setIntegral_finset` `Finset.coe_univ` `Measure.restrict_univ`
`integral_sum_dirac` 📖	mathematical	—	`integral` `Measure.sum` `ENNReal` `Measure` `Measure.instSMul` `Algebra.toSMul` `ENNReal.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.right` `Measure.dirac` `tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Real` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `NormedSpace.toModule` `Real.normedField` `ENNReal.toReal` `SummationFilter.unconditional`	—	`IsScalarTower.right` `integral_sum_measure` `integral_smul_measure` `integral_dirac` `complete_of_proper` `FiniteDimensional.proper_real` `integral_undef` `tsum_eq_zero_of_not_summable` `Summable.norm` `norm_smul` `NormedSpace.toNormSMulClass` `ENNReal.abs_toReal` `integrable_sum_dirac`
`integral_sum_dirac_eq_tsum` 📖	mathematical	`Summable` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instMul` `ENNReal.toReal` `Norm.norm` `NormedAddCommGroup.toNorm` `SummationFilter.unconditional`	`integral` `Measure.sum` `ENNReal` `Measure` `Measure.instSMul` `Algebra.toSMul` `ENNReal.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.right` `Measure.dirac` `tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Real` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `NormedSpace.toModule` `Real.normedField` `ENNReal.toReal` `SummationFilter.unconditional`	—	`IsScalarTower.right` `HasSum.tsum_eq` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `SummationFilter.instNeBotUnconditional` `hasSum_integral_sum_dirac`
`integral_sum_measure` 📖	mathematical	`Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Measure.sum`	`integral` `Measure.sum` `tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SummationFilter.unconditional`	—	`HasSum.tsum_eq` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `SummationFilter.instNeBotUnconditional` `hasSum_integral_measure`
`setIntegral_countable` 📖	mathematical	`IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`integral` `Measure.restrict` `tsum` `Set.Elem` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Real` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `NormedSpace.toModule` `Real.normedField` `Measure.real` `Set` `Set.instSingletonSet` `Set.instMembership` `SummationFilter.unconditional`	—	`Set.countable_coe_iff` `integrable_map_measure` `Integrable.aestronglyMeasurable` `map_comap_subtype_coe` `Set.Countable.measurableSet` `IntegrableOn.eq_1` `Measurable.aemeasurable` `measurable_subtype_coe` `integral_subtype_comap` `integral_countable` `Subtype.instMeasurableSingletonClass` `measureReal_def` `Measure.comap_apply` `Subtype.coe_injective` `MeasurableSet.subtype_image` `MeasurableSet.singleton` `Set.image_singleton`
`setIntegral_finset` 📖	mathematical	`IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `SetLike.coe` `Finset` `Finset.instSetLike`	`integral` `Measure.restrict` `SetLike.coe` `Finset` `Finset.instSetLike` `Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Real` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `NormedSpace.toModule` `Real.normedField` `Measure.real` `Set` `Set.instSingletonSet`	—	`setIntegral_countable` `Finset.countable_toSet` `Finset.tsum_subtype'`

MeasureTheory.Integrable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`summable_integral` 📖	mathematical	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `MeasureTheory.Measure.sum`	`Summable` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `MeasureTheory.integral` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `Real.normedField` `Norm.norm` `NormedAddCommGroup.toNorm` `SummationFilter.unconditional`	—	`MeasureTheory.integral_toReal` `MeasureTheory.AEStronglyMeasurable.enorm` `MeasureTheory.AEStronglyMeasurable.mono_measure` `aestronglyMeasurable` `MeasureTheory.Measure.le_sum` `MeasureTheory.Measure.instOuterMeasureClass` `toReal_enorm` `ENNReal.summable_toReal` `MeasureTheory.lintegral_sum_measure` `LT.lt.ne`
`summable_of_dirac` 📖	mathematical	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `MeasureTheory.Measure.sum` `ENNReal` `MeasureTheory.Measure` `MeasureTheory.Measure.instSMul` `Algebra.toSMul` `ENNReal.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.right` `MeasureTheory.Measure.dirac`	`Summable` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instMul` `ENNReal.toReal` `Norm.norm` `NormedAddCommGroup.toNorm` `SummationFilter.unconditional`	—	`IsScalarTower.right` `MeasureTheory.integral_smul_measure` `MeasureTheory.integral_dirac` `Real.instCompleteSpace` `summable_integral`

---

← Back to Index