Documentation Verification Report

DominatedConvergence

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

Statistics

Metric	Count
Definitions	0
Theorems `tendsto_setIntegral`, `continuous_primitive`, `hasSum_integral_of_dominated_convergence`, `hasSum_integral_of_summable_integral_norm`, `integral_tsum`, `integral_tsum_of_summable_integral_norm`, `tendsto_integral_filter_of_dominated_convergence`, `tendsto_integral_filter_of_norm_le_const`, `tendsto_integral_of_dominated_convergence`, `continuousAt_of_dominated_interval`, `continuousAt_parametric_primitive_of_dominated`, `continuousOn_primitive`, `continuousOn_primitive_Icc`, `continuousOn_primitive_interval`, `continuousOn_primitive_interval'`, `continuousOn_primitive_interval_left`, `continuousWithinAt_of_dominated_interval`, `continuousWithinAt_primitive`, `continuous_of_dominated_interval`, `continuous_parametric_intervalIntegral_of_continuous`, `continuous_parametric_intervalIntegral_of_continuous'`, `continuous_parametric_primitive_of_continuous`, `continuous_primitive`, `hasSum_integral_of_dominated_convergence`, `hasSum_intervalIntegral_of_summable_norm`, `tendsto_integral_filter_of_dominated_convergence`, `tsum_intervalIntegral_eq_of_summable_norm`	27
Total	27

Antitone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tendsto_setIntegral` 📖	mathematical	`MeasurableSet` `Antitone` `Set` `Nat.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `MeasureTheory.IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`Filter.Tendsto` `MeasureTheory.integral` `MeasureTheory.Measure.restrict` `Filter.atTop` `nhds` `Set.iInter`	—	`MeasureTheory.integral_indicator` `MeasurableSet.iInter` `instCountableNat` `MeasureTheory.tendsto_integral_of_dominated_convergence` `aestronglyMeasurable_indicator_iff` `MeasureTheory.IntegrableOn.mono_set` `zero_le` `Nat.instCanonicallyOrderedAdd` `MeasureTheory.integrable_indicator_iff` `MeasureTheory.Integrable.norm` `MeasureTheory.Measure.instOuterMeasureClass` `norm_indicator_eq_indicator_norm` `Filter.Eventually.of_forall` `le_imp_le_of_le_of_le` `Set.indicator_le_indicator_apply_of_subset` `LE.le.subset` `norm_nonneg` `le_refl` `Filter.univ_mem'` `le_trans` `tendsto_indicator` `pure_le_nhds`

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasSum_integral_of_dominated_convergence` 📖	mathematical	`AEStronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Filter.Eventually` `Real` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `Summable` `Real.instAddCommMonoid` `Real.pseudoMetricSpace` `SummationFilter.unconditional` `Integrable` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `tsum` `HasSum` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	`integral`	—	`Measure.instOuterMeasureClass` `eventually_countable_forall` `instCountableInterFilter` `Filter.Eventually.mono` `LE.le.trans` `norm_nonneg` `Filter.mp_mem` `Filter.univ_mem'` `Summable.le_tsum` `Real.instIsOrderedAddMonoid` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `SummationFilter.instNeBotUnconditional` `SummationFilter.instLeAtTopUnconditional` `Integrable.mono'` `Filter.EventuallyLE.trans` `Finset.sum_congr` `integral_finset_sum` `tendsto_integral_filter_of_dominated_convergence` `SummationFilter.instIsCountablyGeneratedFinsetFilterUnconditionalOfCountable` `Filter.Eventually.of_forall` `Finset.aestronglyMeasurable_fun_sum` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `norm_sum_le_of_le` `Summable.sum_le_tsum`
`hasSum_integral_of_summable_integral_norm` 📖	mathematical	`Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Summable` `Real` `Real.instAddCommMonoid` `Real.pseudoMetricSpace` `integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `Norm.norm` `NormedAddCommGroup.toNorm` `SummationFilter.unconditional`	`HasSum` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `tsum`	—	`integral_tsum` `lintegral_coe_eq_integral` `Integrable.norm` `ENNReal.coe_nnreal_eq` `coe_nnnorm` `Real.norm_of_nonneg` `integral_nonneg` `Real.instIsOrderedAddMonoid` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `Real.instIsStrictOrderedRing` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `norm_nonneg` `ENNReal.tsum_coe_ne_top_iff_summable` `NNReal.summable_coe` `Summable.abs` `instIsUniformAddGroupReal` `Real.instCompleteSpace` `Summable.hasSum` `Summable.of_norm_bounded` `norm_integral_le_integral_norm` `integral_def`
`integral_tsum` 📖	mathematical	`AEStronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`integral` `tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SummationFilter.unconditional`	—	`AEStronglyMeasurable.enorm` `Measure.instOuterMeasureClass` `Filter.Eventually.mono` `ae_lt_top'` `AEMeasurable.ennreal_tsum` `lintegral_tsum` `ENNReal.tsum_coe_ne_top_iff_summable_coe` `LT.lt.ne` `HasSum.tsum_eq` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `SummationFilter.instNeBotUnconditional` `hasSum_integral_of_dominated_convergence` `Filter.univ_mem'` `le_refl` `aestronglyMeasurable_iff_aemeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `Real.borelSpace` `instSecondCountableTopologyReal` `AEMeasurable.coe_nnreal_real` `AEMeasurable.nnreal_tsum` `AEStronglyMeasurable.aemeasurable` `NNReal.borelSpace` `AEStronglyMeasurable.nnnorm` `lt_top_iff_ne_top` `lintegral_congr_ae` `NNReal.nnnorm_eq` `Filter.mp_mem` `ENNReal.coe_tsum` `NNReal.summable_coe` `Summable.hasSum` `Summable.of_norm` `integral_def` `tsum_zero`
`integral_tsum_of_summable_integral_norm` 📖	mathematical	`Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Summable` `Real` `Real.instAddCommMonoid` `Real.pseudoMetricSpace` `integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `Norm.norm` `NormedAddCommGroup.toNorm` `SummationFilter.unconditional`	`tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`HasSum.tsum_eq` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `SummationFilter.instNeBotUnconditional` `hasSum_integral_of_summable_integral_norm`
`tendsto_integral_filter_of_dominated_convergence` 📖	mathematical	`Filter.Eventually` `AEStronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Real` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `Integrable` `Real.pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `Filter.Tendsto` `nhds`	`integral`	—	`Measure.instOuterMeasureClass` `fact_one_le_one_ennreal` `integral_def` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `L1.integral_def` `tendsto_setToFun_filter_of_dominated_convergence` `dominatedFinMeasAdditive_weightedSMul`
`tendsto_integral_filter_of_norm_le_const` 📖	mathematical	`Filter.Eventually` `AEStronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Real` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `Filter.Tendsto` `nhds`	`integral`	—	`Measure.instOuterMeasureClass` `tendsto_integral_filter_of_dominated_convergence` `integrable_const`
`tendsto_integral_of_dominated_convergence` 📖	mathematical	`AEStronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Integrable` `Real` `Real.pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `Filter.Eventually` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `Filter.Tendsto` `Filter.atTop` `Nat.instPreorder` `nhds`	`integral`	—	`Measure.instOuterMeasureClass` `fact_one_le_one_ennreal` `integral_def` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `L1.integral_def` `tendsto_setToFun_of_dominated_convergence` `dominatedFinMeasAdditive_weightedSMul` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat`

MeasureTheory.Integrable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_primitive` 📖	mathematical	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Real` `Real.measurableSpace`	`Continuous` `Real.pseudoMetricSpace` `intervalIntegral`	—	`intervalIntegral.continuous_primitive` `intervalIntegrable`

intervalIntegral

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousAt_of_dominated_interval` 📖	mathematical	`Filter.Eventually` `MeasureTheory.AEStronglyMeasurable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Real.measurableSpace` `MeasureTheory.Measure.restrict` `Set.uIoc` `Real.linearOrder` `nhds` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `IntervalIntegrable` `Real.pseudoMetricSpace` `NormedAddGroup.toENormedAddMonoid` `NormedAddCommGroup.toNormedAddGroup` `Real.normedAddCommGroup`	`ContinuousAt` `intervalIntegral`	—	`MeasureTheory.Measure.instOuterMeasureClass` `tendsto_integral_filter_of_dominated_convergence` `FirstCountableTopology.nhds_generated_countable`
`continuousAt_parametric_primitive_of_dominated` 📖	mathematical	`MeasureTheory.AEStronglyMeasurable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Real.measurableSpace` `MeasureTheory.Measure.restrict` `Set.uIoc` `Real.linearOrder` `Filter.Eventually` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `nhds` `IntervalIntegrable` `Real.pseudoMetricSpace` `NormedAddGroup.toENormedAddMonoid` `NormedAddCommGroup.toNormedAddGroup` `Real.normedAddCommGroup` `ContinuousAt` `Set` `Set.instMembership` `Set.Ioo` `Real.instPreorder` `DFunLike.coe` `ENNReal` `Set.instSingletonSet` `instZeroENNReal`	`instTopologicalSpaceProd` `intervalIntegral`	—	`MeasureTheory.Measure.instOuterMeasureClass` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.OrdConnected.uIoc_subset` `Set.ordConnected_Ioo` `Set.Ioo_subset_Ioc_self` `Set.Ioc_subset_uIoc` `Ioo_mem_nhds` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `Icc_mem_nhds` `Filter.Eventually.self_of_nhds` `nhds_prod_eq` `Filter.Eventually.mono` `IntervalIntegrable.mono_fun'` `IntervalIntegrable.mono_set_ae` `PseudoEMetricSpace.pseudoMetrizableSpace` `Filter.Eventually.of_forall` `MeasureTheory.AEStronglyMeasurable.mono_set` `MeasureTheory.ae_restrict_of_ae_restrict_of_subset` `integral_sub` `add_assoc` `add_sub_cancel` `integral_add_adjacent_intervals` `continuousAt_congr` `ContinuousAt.add` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousAt.fst'` `continuousAt_of_dominated_interval` `MeasureTheory.ae_imp_of_ae_restrict` `ContinuousAt.snd'` `ContinuousWithinAt.continuousAt` `continuousWithinAt_primitive` `min_eq_right` `LT.lt.le` `max_eq_right` `Nat.instAtLeastTwoHAddOfNat` `Filter.Eventually.and` `norm_sub_le` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Real.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `norm_integral_le_abs_of_norm_le` `IntervalIntegrable.const_mul` `IntervalIntegrable.mono_set'` `squeeze_zero_norm'` `subset_refl` `Set.instReflSubset` `integral_const_mul` `integral_same` `Filter.Tendsto.comp` `Continuous.tendsto'` `continuous_abs` `instOrderTopologyReal` `abs_zero` `IsOrderedAddMonoid.toAddLeftMono` `Filter.tendsto_snd` `sub_self`
`continuousOn_primitive` 📖	mathematical	`MeasureTheory.IntegrableOn` `Real` `Real.measurableSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Set.Icc` `Real.instPreorder`	`ContinuousOn` `Real.pseudoMetricSpace` `MeasureTheory.integral` `MeasureTheory.Measure.restrict` `Set.Ioc`	—	`integral_of_le` `continuousOn_congr` `continuousWithinAt_primitive` `MeasureTheory.NoAtoms.measure_singleton` `min_self` `max_eq_right` `PseudoEMetricSpace.pseudoMetrizableSpace` `MeasureTheory.IntegrableOn.mono` `Set.Ioc_subset_Icc_self` `le_rfl` `Set.Icc_eq_empty` `continuousOn_empty`
`continuousOn_primitive_Icc` 📖	mathematical	`MeasureTheory.IntegrableOn` `Real` `Real.measurableSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Set.Icc` `Real.instPreorder`	`ContinuousOn` `Real.pseudoMetricSpace` `MeasureTheory.integral` `MeasureTheory.Measure.restrict`	—	`MeasureTheory.integral_Icc_eq_integral_Ioc` `continuousOn_primitive`
`continuousOn_primitive_interval` 📖	mathematical	`MeasureTheory.IntegrableOn` `Real` `Real.measurableSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Set.uIcc` `Real.lattice`	`ContinuousOn` `Real.pseudoMetricSpace` `intervalIntegral`	—	`continuousOn_primitive_interval'` `MeasureTheory.IntegrableOn.intervalIntegrable` `Set.left_mem_uIcc`
`continuousOn_primitive_interval'` 📖	mathematical	`IntervalIntegrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedAddGroup.toENormedAddMonoid` `NormedAddCommGroup.toNormedAddGroup` `Real` `Set` `Set.instMembership` `Set.uIcc` `Real.lattice`	`ContinuousOn` `Real.pseudoMetricSpace` `intervalIntegral`	—	`continuousWithinAt_primitive` `MeasureTheory.NoAtoms.measure_singleton` `min_eq_right` `max_eq_right` `PseudoEMetricSpace.pseudoMetrizableSpace` `inf_of_le_left` `sup_of_le_right`
`continuousOn_primitive_interval_left` 📖	mathematical	`MeasureTheory.IntegrableOn` `Real` `Real.measurableSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Set.uIcc` `Real.lattice`	`ContinuousOn` `Real.pseudoMetricSpace` `intervalIntegral`	—	`Set.uIcc_comm` `integral_symm` `ContinuousOn.neg` `IsTopologicalAddGroup.toContinuousNeg` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `continuousOn_primitive_interval`
`continuousWithinAt_of_dominated_interval` 📖	mathematical	`Filter.Eventually` `MeasureTheory.AEStronglyMeasurable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Real.measurableSpace` `MeasureTheory.Measure.restrict` `Set.uIoc` `Real.linearOrder` `nhdsWithin` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `IntervalIntegrable` `Real.pseudoMetricSpace` `NormedAddGroup.toENormedAddMonoid` `NormedAddCommGroup.toNormedAddGroup` `Real.normedAddCommGroup`	`ContinuousWithinAt` `intervalIntegral`	—	`MeasureTheory.Measure.instOuterMeasureClass` `tendsto_integral_filter_of_dominated_convergence` `TopologicalSpace.isCountablyGenerated_nhdsWithin` `FirstCountableTopology.nhds_generated_countable`
`continuousWithinAt_primitive` 📖	mathematical	`DFunLike.coe` `MeasureTheory.Measure` `Real` `Real.measurableSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `Set.instSingletonSet` `instZeroENNReal` `IntervalIntegrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedAddGroup.toENormedAddMonoid` `NormedAddCommGroup.toNormedAddGroup` `Real.instMin` `Real.instMax`	`ContinuousWithinAt` `Real.pseudoMetricSpace` `intervalIntegral` `Set.Icc` `Real.instPreorder`	—	`LE.le.trans` `min_eq_left` `IntervalIntegrable.mono_set` `PseudoEMetricSpace.pseudoMetrizableSpace` `Set.uIcc_subset_uIcc` `min_le_of_left_le` `min_le_right` `le_max_of_le_right` `le_max_right` `integral_add_adjacent_intervals` `min_le_left` `le_max_left` `ContinuousWithinAt.congr` `ContinuousWithinAt.add` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `continuousWithinAt_const` `Filter.eventuallyEq_of_mem` `self_mem_nhdsWithin` `integral_indicator` `ContinuousWithinAt.congr_of_eventuallyEq` `IntervalIntegrable.norm` `Set.right_mem_Icc` `continuousWithinAt_of_dominated_interval` `TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology` `Filter.mp_mem` `Filter.univ_mem'` `aestronglyMeasurable_indicator_iff` `measurableSet_Iic` `BorelSpace.opensMeasurable` `Real.borelSpace` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `MeasureTheory.Measure.restrict_restrict` `Set.uIoc.eq_1` `Set.Iic_def` `Set.Iic_inter_Ioc_of_le` `MeasureTheory.Integrable.aestronglyMeasurable` `MeasureTheory.Measure.instOuterMeasureClass` `norm_zero` `MeasureTheory.compl_mem_ae_iff` `Ne.lt_or_gt` `Filter.Eventually.mono` `mem_nhdsWithin_of_mem_nhds` `Ioi_mem_nhds` `Set.indicator_of_mem` `LT.lt.le` `Iio_mem_nhds` `instClosedIciTopology` `Set.indicator_of_notMem` `continuousWithinAt_of_notMem_closure` `closure_Icc`
`continuous_of_dominated_interval` 📖	mathematical	`MeasureTheory.AEStronglyMeasurable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Real.measurableSpace` `MeasureTheory.Measure.restrict` `Set.uIoc` `Real.linearOrder` `Filter.Eventually` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `IntervalIntegrable` `Real.pseudoMetricSpace` `NormedAddGroup.toENormedAddMonoid` `NormedAddCommGroup.toNormedAddGroup` `Real.normedAddCommGroup`	`Continuous` `intervalIntegral`	—	`MeasureTheory.Measure.instOuterMeasureClass` `continuous_iff_continuousAt` `continuousAt_of_dominated_interval` `Filter.Eventually.of_forall` `Filter.Eventually.mono` `Continuous.continuousAt`
`continuous_parametric_intervalIntegral_of_continuous` 📖	mathematical	`Continuous` `Real` `instTopologicalSpaceProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`intervalIntegral`	—	`Continuous.comp₂` `continuous_parametric_primitive_of_continuous` `continuous_id`
`continuous_parametric_intervalIntegral_of_continuous'` 📖	mathematical	`Continuous` `Real` `instTopologicalSpaceProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`intervalIntegral`	—	`continuous_parametric_intervalIntegral_of_continuous` `continuous_const`
`continuous_parametric_primitive_of_continuous` 📖	mathematical	`Continuous` `Real` `instTopologicalSpaceProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`intervalIntegral`	—	`continuous_iff_continuousAt` `Metric.continuousAt_iff'` `NoMinOrder.exists_lt` `instNoMinOrderOfNontrivial` `Real.instIsOrderedRing` `Real.instNontrivial` `NoMaxOrder.exists_gt` `instNoMaxOrderOfNontrivial` `IsCompact.prod` `isCompact_singleton` `CompactIccSpace.isCompact_Icc` `ConditionallyCompleteLinearOrder.toCompactIccSpace` `instOrderTopologyReal` `IsCompact.bddAbove_image` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `Continuous.continuousOn` `Continuous.norm` `Ioo_mem_nhdsGT` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `Filter.Tendsto.sub` `IsTopologicalAddGroup.to_continuousSub` `instIsTopologicalAddGroupReal` `tendsto_const_nhds` `Filter.tendsto_id` `Filter.Tendsto.add` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Filter.mp_mem` `tendsto_order` `add_zero` `max_lt_iff` `sub_zero` `lt_min_iff` `Filter.univ_mem'` `Set.Icc_subset_Icc` `LT.lt.le` `Filter.Tendsto.mul` `IsTopologicalSemiring.toContinuousMul` `Filter.Tendsto.comp` `ENNReal.tendsto_toReal` `ENNReal.zero_ne_top` `tendsto_measure_Icc` `MeasureTheory.Measure.Regular.toIsFiniteMeasureOnCompacts` `MeasureTheory.Measure.Regular.of_sigmaCompactSpace_of_isLocallyFiniteMeasure` `PseudoEMetricSpace.pseudoMetrizableSpace` `SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `instSecondCountableTopologyReal` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `locallyCompact_of_proper` `instProperSpaceReal` `Real.borelSpace` `MulZeroClass.mul_zero` `MulZeroClass.zero_mul` `Filter.Eventually.exists` `nhdsGT_neBot` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Filter.Eventually.and` `Filter.Eventually.filter_mono` `nhdsWithin_le_nhds` `IsCompact.mem_uniformity_of_prod` `Set.mem_univ` `Metric.dist_mem_uniformity` `nhdsWithin_univ` `Ioo_mem_nhds` `lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Mathlib.Tactic.Ring.add_pf_add_lt` `dist_eq_norm` `Continuous.intervalIntegrable` `Continuous.uncurry_left` `Mathlib.Tactic.Abel.unfold_sub` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Tactic.Abel.const_add_termg` `Mathlib.Tactic.Abel.term_add_termg` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.isInt_neg` `Mathlib.Tactic.Abel.zero_termg` `norm_add_le` `integral_interval_sub_left` `integral_sub` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `covariant_swap_add_of_covariant_add` `norm_integral_le_integral_norm_uIoc` `MeasureTheory.integral_mono_measure` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `MeasureTheory.Measure.restrict_mono` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.uIoc_subset_uIcc` `Set.uIcc_subset_Icc` `AddGroup.toOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `le_refl` `Filter.Eventually.of_forall` `MeasureTheory.Measure.instOuterMeasureClass` `norm_nonneg` `Continuous.integrableOn_Icc` `BorelSpace.opensMeasurable` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `Continuous.sub` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `MeasureTheory.setIntegral_mono_on₀` `continuous_const` `nullMeasurableSet_Icc` `Set.mem_image_of_mem` `Set.singleton_prod` `le_of_lt` `le_of_not_gt` `Mathlib.Tactic.Ring.cast_pos` `Nat.cast_one` `Mathlib.Tactic.Linarith.add_neg` `MeasureTheory.integral_const` `Real.instCompleteSpace` `MeasureTheory.measureReal_restrict_apply` `Set.univ_inter` `mul_comm`
`continuous_primitive` 📖	mathematical	`IntervalIntegrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedAddGroup.toENormedAddMonoid` `NormedAddCommGroup.toNormedAddGroup`	`Continuous` `Real` `Real.pseudoMetricSpace` `intervalIntegral`	—	`continuous_iff_continuousAt` `NoMinOrder.exists_lt` `instNoMinOrderOfNontrivial` `Real.instIsOrderedRing` `Real.instNontrivial` `NoMaxOrder.exists_gt` `instNoMaxOrderOfNontrivial` `ContinuousWithinAt.continuousAt` `continuousWithinAt_primitive` `MeasureTheory.NoAtoms.measure_singleton` `Icc_mem_nhds` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid`
`hasSum_integral_of_dominated_convergence` 📖	mathematical	`MeasureTheory.AEStronglyMeasurable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Real.measurableSpace` `MeasureTheory.Measure.restrict` `Set.uIoc` `Real.linearOrder` `Filter.Eventually` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `IntervalIntegrable` `Real.pseudoMetricSpace` `NormedAddGroup.toENormedAddMonoid` `NormedAddCommGroup.toNormedAddGroup` `Real.normedAddCommGroup` `tsum` `Real.instAddCommMonoid` `SummationFilter.unconditional`	`HasSum` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `intervalIntegral`	—	`MeasureTheory.Measure.instOuterMeasureClass` `intervalIntegral_eq_integral_uIoc` `HasSum.const_smul` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `MeasureTheory.hasSum_integral_of_dominated_convergence` `MeasureTheory.ae_restrict_iff'` `measurableSet_uIoc` `BorelSpace.opensMeasurable` `Real.borelSpace` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `PseudoEMetricSpace.pseudoMetrizableSpace`
`hasSum_intervalIntegral_of_summable_norm` 📖	mathematical	`Summable` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Norm.norm` `ContinuousMap` `Set.Elem` `SetLike.coe` `TopologicalSpace.Compacts` `TopologicalSpace.Compacts.instSetLike` `Set.uIcc` `Real.lattice` `isCompact_uIcc` `Real.linearOrder` `ConditionallyCompleteLinearOrder.toCompactIccSpace` `Real.instConditionallyCompleteLinearOrder` `instOrderTopologyReal` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ContinuousMap.instNorm` `ContinuousMap.instCompactSpaceElemCoeCompacts` `ContinuousMap.restrict` `SummationFilter.unconditional`	`HasSum` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `intervalIntegral` `DFunLike.coe` `ContinuousMap.instFunLike` `MeasureTheory.MeasureSpace.volume` `Real.measureSpace` `tsum`	—	`isCompact_uIcc` `ConditionallyCompleteLinearOrder.toCompactIccSpace` `instOrderTopologyReal` `ContinuousMap.instCompactSpaceElemCoeCompacts` `hasSum_integral_of_dominated_convergence` `Continuous.aestronglyMeasurable` `BorelSpace.opensMeasurable` `Real.borelSpace` `PseudoEMetricSpace.pseudoMetrizableSpace` `secondCountableTopologyEither_of_left` `instSecondCountableTopologyReal` `ContinuousMapClass.map_continuous` `ContinuousMap.instContinuousMapClass` `Filter.univ_mem'` `MeasureTheory.Measure.instOuterMeasureClass` `ContinuousMap.norm_coe_le_norm` `LT.lt.le` `MeasureTheory.ae_of_all` `intervalIntegrable_const` `Real.locallyFinite_volume` `enorm_ne_top` `Summable.hasSum` `Summable.of_norm` `ContinuousMap.instCompleteSpaceOfCompactlyCoherentSpace` `CompactlyCoherentSpace.of_sequentialSpace` `FrechetUrysohnSpace.to_sequentialSpace` `Subtype.instFrechetUrysohnSpace` `FirstCountableTopology.frechetUrysohnSpace` `TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology` `ContinuousMap.summable_apply` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `MeasureTheory.integral_def` `sub_self`
`tendsto_integral_filter_of_dominated_convergence` 📖	mathematical	`Filter.Eventually` `MeasureTheory.AEStronglyMeasurable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Real.measurableSpace` `MeasureTheory.Measure.restrict` `Set.uIoc` `Real.linearOrder` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `IntervalIntegrable` `Real.pseudoMetricSpace` `NormedAddGroup.toENormedAddMonoid` `NormedAddCommGroup.toNormedAddGroup` `Real.normedAddCommGroup`	`Filter.Tendsto` `intervalIntegral` `nhds`	—	`MeasureTheory.Measure.instOuterMeasureClass` `intervalIntegral_eq_integral_uIoc` `Filter.Tendsto.smul` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `tendsto_const_nhds` `MeasureTheory.tendsto_integral_filter_of_dominated_convergence` `MeasureTheory.ae_restrict_iff'` `measurableSet_uIoc` `BorelSpace.opensMeasurable` `Real.borelSpace` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `PseudoEMetricSpace.pseudoMetrizableSpace`
`tsum_intervalIntegral_eq_of_summable_norm` 📖	mathematical	`Summable` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Norm.norm` `ContinuousMap` `Set.Elem` `SetLike.coe` `TopologicalSpace.Compacts` `TopologicalSpace.Compacts.instSetLike` `Set.uIcc` `Real.lattice` `isCompact_uIcc` `Real.linearOrder` `ConditionallyCompleteLinearOrder.toCompactIccSpace` `Real.instConditionallyCompleteLinearOrder` `instOrderTopologyReal` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ContinuousMap.instNorm` `ContinuousMap.instCompactSpaceElemCoeCompacts` `ContinuousMap.restrict` `SummationFilter.unconditional`	`tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `intervalIntegral` `DFunLike.coe` `ContinuousMap.instFunLike` `MeasureTheory.MeasureSpace.volume` `Real.measureSpace`	—	`isCompact_uIcc` `ConditionallyCompleteLinearOrder.toCompactIccSpace` `instOrderTopologyReal` `ContinuousMap.instCompactSpaceElemCoeCompacts` `HasSum.tsum_eq` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `SummationFilter.instNeBotUnconditional` `hasSum_intervalIntegral_of_summable_norm`

---

← Back to Index