DominatedConvergence

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

Statistics

Metric	Count
Definitions	0
Theorems tendsto_setIntegral, continuous_primitive, continuousOn_Ici_primitive_Ici, continuousOn_Ici_primitive_Ioi, continuousOn_Iic_primitive_Iic, continuousOn_Iic_primitive_Iio, continuousWithinAt_Ici_primitive_Ioi, continuousWithinAt_Iic_primitive_Iio, 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	33
Total	33

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 Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup 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	HasSum ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid integral SummationFilter.unconditional	—	Measure.instOuterMeasureClass eventually_countable_forall 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 UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid integral tsum SummationFilter.unconditional	—	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 UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup 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 UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid integral SummationFilter.unconditional	—	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	Filter.Tendsto integral nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	—	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	Filter.Tendsto integral nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	—	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	Filter.Tendsto integral Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	—	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 UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup intervalIntegral	—	intervalIntegral.continuous_primitive intervalIntegrable

MeasureTheory.IntegrableOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousOn_Ici_primitive_Ici 📖	mathematical	MeasureTheory.IntegrableOn Real Real.measurableSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Set.Ici Real.instPreorder	ContinuousOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.integral Real.measurableSpace MeasureTheory.Measure.restrict Set.Ici Real.instPreorder	—	MeasureTheory.integral_Ici_eq_integral_Ioi continuousOn_Ici_primitive_Ioi mono_set Set.Ioi_subset_Ici_self
continuousOn_Ici_primitive_Ioi 📖	mathematical	MeasureTheory.IntegrableOn Real Real.measurableSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Set.Ioi Real.instPreorder	ContinuousOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.integral Real.measurableSpace MeasureTheory.Measure.restrict Set.Ioi Real.instPreorder Set.Ici	—	continuousWithinAt_iff_continuous_left_right Set.Ici_inter_Iic intervalIntegrable_iff_integrableOn_Ioc_of_le PseudoEMetricSpace.pseudoMetrizableSpace mono_set Set.Ioc_subset_Ioi_self intervalIntegral.integral_Ioi_sub_Ioi sub_sub_cancel intervalIntegral.continuousWithinAt_primitive MeasureTheory.NoAtoms.measure_singleton min_self sup_of_le_right ContinuousWithinAt.congr ContinuousWithinAt.sub IsTopologicalAddGroup.to_continuousSub SeminormedAddCommGroup.toIsTopologicalAddGroup continuousWithinAt_const Set.right_mem_Icc Set.Ici_inter_Ici continuousWithinAt_Ici_primitive_Ioi Set.Ioi_subset_Ioi
continuousOn_Iic_primitive_Iic 📖	mathematical	MeasureTheory.IntegrableOn Real Real.measurableSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Set.Iic Real.instPreorder	ContinuousOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.integral Real.measurableSpace MeasureTheory.Measure.restrict Set.Iic Real.instPreorder	—	MeasureTheory.integral_Iic_eq_integral_Iio continuousOn_Iic_primitive_Iio mono_set Set.Iio_subset_Iic_self
continuousOn_Iic_primitive_Iio 📖	mathematical	MeasureTheory.IntegrableOn Real Real.measurableSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Set.Iio Real.instPreorder	ContinuousOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.integral Real.measurableSpace MeasureTheory.Measure.restrict Set.Iio Real.instPreorder Set.Iic	—	continuousWithinAt_iff_continuous_left_right Set.Iic_inter_Iic inf_of_le_right continuousWithinAt_Iic_primitive_Iio mono_set Set.Iio_subset_Iio Set.Iic_inter_Ici intervalIntegrable_iff_integrableOn_Ico_of_le PseudoEMetricSpace.pseudoMetrizableSpace enorm_ne_top Set.Ico_subset_Iio_self intervalIntegral.integral_symm intervalIntegral.integral_Iio_sub_Iio' neg_sub add_sub_cancel intervalIntegral.continuousWithinAt_primitive MeasureTheory.NoAtoms.measure_singleton max_self ContinuousWithinAt.congr ContinuousWithinAt.add IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup continuousWithinAt_const Set.left_mem_Icc
continuousWithinAt_Ici_primitive_Ioi 📖	mathematical	MeasureTheory.IntegrableOn Real Real.measurableSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Set.Ioi Real.instPreorder	ContinuousWithinAt Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.integral Real.measurableSpace MeasureTheory.Measure.restrict Set.Ioi Real.instPreorder Set.Ici	—	MeasureTheory.integral_indicator measurableSet_Ioi BorelSpace.opensMeasurable Real.borelSpace instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid MeasureTheory.tendsto_integral_filter_of_dominated_convergence TopologicalSpace.isCountablyGenerated_nhdsWithin FirstCountableTopology.nhds_generated_countable TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology PseudoEMetricSpace.pseudoMetrizableSpace Filter.mp_mem self_mem_nhdsWithin Filter.univ_mem' aestronglyMeasurable_indicator_iff MeasureTheory.Integrable.aestronglyMeasurable mono_set Set.Ioi_subset_Ioi MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.ae_of_all norm_indicator_eq_indicator_norm Set.indicator_le_indicator_of_subset norm_nonneg MeasureTheory.integrable_indicator_iff MeasureTheory.Integrable.norm Set.indicator_apply Filter.Tendsto.congr' tendsto_const_nhds mem_nhdsWithin_of_mem_nhds Iio_mem_nhds instClosedIciTopology
continuousWithinAt_Iic_primitive_Iio 📖	mathematical	MeasureTheory.IntegrableOn Real Real.measurableSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Set.Iio Real.instPreorder	ContinuousWithinAt Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.integral Real.measurableSpace MeasureTheory.Measure.restrict Set.Iio Real.instPreorder Set.Iic	—	MeasureTheory.integral_indicator measurableSet_Iio BorelSpace.opensMeasurable Real.borelSpace instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid MeasureTheory.tendsto_integral_filter_of_dominated_convergence TopologicalSpace.isCountablyGenerated_nhdsWithin FirstCountableTopology.nhds_generated_countable TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology PseudoEMetricSpace.pseudoMetrizableSpace Filter.mp_mem self_mem_nhdsWithin Filter.univ_mem' aestronglyMeasurable_indicator_iff MeasureTheory.Integrable.aestronglyMeasurable mono_set Set.Iio_subset_Iio MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.ae_of_all norm_indicator_eq_indicator_norm Set.indicator_le_indicator_of_subset norm_nonneg MeasureTheory.integrable_indicator_iff MeasureTheory.Integrable.norm Set.indicator_apply Filter.Tendsto.congr' tendsto_const_nhds mem_nhdsWithin_of_mem_nhds Ioi_mem_nhds instClosedIicTopology

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 UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup 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	ContinuousAt Real instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup 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 UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.integral Real.measurableSpace MeasureTheory.Measure.restrict Set.Ioc Real.instPreorder Set.Icc	—	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 UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.integral Real.measurableSpace MeasureTheory.Measure.restrict Set.Icc Real.instPreorder	—	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 UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup intervalIntegral Set.uIcc Real.lattice	—	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 UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup intervalIntegral Set.uIcc Real.lattice	—	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 UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup intervalIntegral Set.uIcc Real.lattice	—	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 UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup 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 UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup 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 instReflLe 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 UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup 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	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace 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	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace 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	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 IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing 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 IsTopologicalRing.toIsTopologicalSemiring 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 instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid 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 UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup 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 UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid intervalIntegral SummationFilter.unconditional	—	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 UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid intervalIntegral DFunLike.coe ContinuousMap Real Real.pseudoMetricSpace ContinuousMap.instFunLike MeasureTheory.MeasureSpace.volume Real.measureSpace tsum SummationFilter.unconditional	—	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 UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	—	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 UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid intervalIntegral DFunLike.coe ContinuousMap Real Real.pseudoMetricSpace ContinuousMap.instFunLike MeasureTheory.MeasureSpace.volume Real.measureSpace SummationFilter.unconditional	—	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