SumIntegralComparisons

📁 Source: Mathlib/Analysis/SumIntegralComparisons.lean

Statistics

Metric	Count
Definitions	0
Theorems integral_le_sum, integral_le_sum_Ico, sum_le_integral, sum_le_integral_Ico, integral_le_sum, integral_le_sum_Ico, sum_le_integral, sum_le_integral_Ico, integral_le_sum_Ico_of_le, integral_le_sum_mul_Ico_of_antitone_monotone, sum_Ico_le_integral_of_le, sum_mul_Ico_le_integral_of_monotone_antitone	12
Total	12

AntitoneOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
integral_le_sum 📖	mathematical	AntitoneOn Real Real.instPreorder Set.Icc Real.instAdd Real.instNatCast	Real.instLE intervalIntegral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.MeasureSpace.volume Real.measureSpace Finset.sum Real.instAddCommMonoid Finset.range	—	intervalIntegrable Real.locallyFinite_volume instOrderTopologyReal instSecondCountableTopologyReal mono Set.uIcc_of_le IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le Real.instZeroLEOneClass RCLike.charZero_rclike Set.Icc_subset_Icc Real.instIsOrderedRing Nat.cast_zero add_zero intervalIntegral.sum_integral_adjacent_intervals Finset.sum_le_sum Finset.mem_range intervalIntegral.integral_mono_on Nat.cast_add Nat.cast_one LT.lt.le Set.mem_Icc le_trans Finset.sum_congr intervalIntegral.integral_const Real.instCompleteSpace add_sub_add_left_eq_sub add_sub_cancel_left one_mul
integral_le_sum_Ico 📖	mathematical	AntitoneOn Real Real.instPreorder Set.Icc Real.instNatCast	Real.instLE intervalIntegral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.MeasureSpace.volume Real.measureSpace Finset.sum Real.instAddCommMonoid Finset.Ico Nat.instPreorder Nat.instLocallyFiniteOrder	—	Nat.cast_add add_comm zero_add Finset.sum_Ico_add Nat.instIsOrderedCancelAddMonoid StarOrderedRing.toExistsAddOfLE Nat.instStarOrderedRing Nat.Ico_zero_eq_range integral_le_sum Nat.cast_sub add_sub_cancel
sum_le_integral 📖	mathematical	AntitoneOn Real Real.instPreorder Set.Icc Real.instAdd Real.instNatCast	Real.instLE Finset.sum Real.instAddCommMonoid Finset.range intervalIntegral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.MeasureSpace.volume Real.measureSpace	—	intervalIntegrable Real.locallyFinite_volume instOrderTopologyReal instSecondCountableTopologyReal mono Set.uIcc_of_le IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le Real.instZeroLEOneClass RCLike.charZero_rclike Set.Icc_subset_Icc Real.instIsOrderedRing Finset.sum_congr Nat.cast_add Nat.cast_one intervalIntegral.integral_const Real.instCompleteSpace add_sub_add_left_eq_sub add_sub_cancel_left one_mul Finset.sum_le_sum Finset.mem_range intervalIntegral.integral_mono_on Set.mem_Icc le_trans le_add_of_nonneg_right Nat.cast_nonneg Nat.cast_zero add_zero intervalIntegral.sum_integral_adjacent_intervals
sum_le_integral_Ico 📖	mathematical	AntitoneOn Real Real.instPreorder Set.Icc Real.instNatCast	Real.instLE Finset.sum Real.instAddCommMonoid Finset.Ico Nat.instPreorder Nat.instLocallyFiniteOrder intervalIntegral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.MeasureSpace.volume Real.measureSpace	—	Nat.cast_add zero_add add_comm Finset.sum_Ico_add Nat.instIsOrderedCancelAddMonoid StarOrderedRing.toExistsAddOfLE Nat.instStarOrderedRing Nat.Ico_zero_eq_range add_assoc sum_le_integral Nat.cast_sub add_sub_cancel

MonotoneOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
integral_le_sum 📖	mathematical	MonotoneOn Real Real.instPreorder Set.Icc Real.instAdd Real.instNatCast	Real.instLE intervalIntegral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.MeasureSpace.volume Real.measureSpace Finset.sum Real.instAddCommMonoid Finset.range	—	neg_le_neg_iff IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add Finset.sum_neg_distrib intervalIntegral.integral_neg AntitoneOn.sum_le_integral neg
integral_le_sum_Ico 📖	mathematical	MonotoneOn Real Real.instPreorder Set.Icc Real.instNatCast	Real.instLE intervalIntegral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.MeasureSpace.volume Real.measureSpace Finset.sum Real.instAddCommMonoid Finset.Ico Nat.instPreorder Nat.instLocallyFiniteOrder	—	neg_le_neg_iff IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add Finset.sum_neg_distrib intervalIntegral.integral_neg AntitoneOn.sum_le_integral_Ico neg
sum_le_integral 📖	mathematical	MonotoneOn Real Real.instPreorder Set.Icc Real.instAdd Real.instNatCast	Real.instLE Finset.sum Real.instAddCommMonoid Finset.range intervalIntegral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.MeasureSpace.volume Real.measureSpace	—	neg_le_neg_iff IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add Finset.sum_neg_distrib intervalIntegral.integral_neg AntitoneOn.integral_le_sum neg
sum_le_integral_Ico 📖	mathematical	MonotoneOn Real Real.instPreorder Set.Icc Real.instNatCast	Real.instLE Finset.sum Real.instAddCommMonoid Finset.Ico Nat.instPreorder Nat.instLocallyFiniteOrder intervalIntegral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.MeasureSpace.volume Real.measureSpace	—	neg_le_neg_iff IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add Finset.sum_neg_distrib intervalIntegral.integral_neg AntitoneOn.integral_le_sum_Ico neg

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
integral_le_sum_Ico_of_le 📖	mathematical	Real Real.instLE Real.instNatCast MeasureTheory.IntegrableOn MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Set.Ico Real.instPreorder MeasureTheory.MeasureSpace.volume	intervalIntegral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Finset.sum Real.instAddCommMonoid Finset.Ico Nat.instPreorder Nat.instLocallyFiniteOrder	—	intervalIntegral.integral_neg neg_neg Finset.sum_congr Finset.sum_neg_distrib neg_le_neg Real.instIsOrderedAddMonoid sum_Ico_le_integral_of_le MeasureTheory.Integrable.neg
integral_le_sum_mul_Ico_of_antitone_monotone 📖	mathematical	AntitoneOn Real Real.instPreorder Set.Icc Real.instNatCast MonotoneOn Real.instSub Real.instOne Real.instLE Real.instZero	intervalIntegral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instMul MeasureTheory.MeasureSpace.volume Real.measureSpace Finset.sum Real.instAddCommMonoid Finset.Ico Nat.instPreorder Nat.instLocallyFiniteOrder	—	integral_le_sum_Ico_of_le covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Nat.cast_one Real.instZeroLEOneClass RCLike.charZero_rclike AddGroup.toOrderedSub le_trans Nat.cast_add LE.le.trans LT.lt.le mul_le_mul IsOrderedRing.toPosMulMono Real.instIsOrderedRing IsOrderedRing.toMulPosMono sub_add_cancel MeasureTheory.Integrable.mono_measure MeasureTheory.Integrable.mul_of_top_left AntitoneOn.integrableOn_isCompact Real.borelSpace instOrderTopologyReal instSecondCountableTopologyReal MeasureTheory.Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts instIsAddHaarMeasureVolume FiniteDimensional.rclike_to_real CompactIccSpace.isCompact_Icc ConditionallyCompleteLinearOrder.toCompactIccSpace MonotoneOn.memLp_isCompact MeasureTheory.Measure.restrict_mono_set Set.Ico_subset_Icc_self
sum_Ico_le_integral_of_le 📖	mathematical	Real Real.instLE Real.instNatCast MeasureTheory.IntegrableOn MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Set.Ico Real.instPreorder MeasureTheory.MeasureSpace.volume	Finset.sum Real.instAddCommMonoid Finset.Ico Nat.instPreorder Nat.instLocallyFiniteOrder intervalIntegral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal	—	intervalIntegrable_iff_integrableOn_Ico_of_le PseudoEMetricSpace.pseudoMetrizableSpace Real.noAtoms_volume Nat.cast_add Nat.cast_one IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le Real.instZeroLEOneClass enorm_ne_top MeasureTheory.IntegrableOn.mono le_trans RCLike.charZero_rclike LT.lt.trans_le le_rfl Finset.sum_congr intervalIntegral.integral_const Real.instCompleteSpace add_sub_cancel_left one_mul Finset.sum_le_sum intervalIntegral.integral_mono_on_of_le_Ioo Real.locallyFinite_volume Set.Ioo_subset_Ico_self intervalIntegral.sum_integral_adjacent_intervals_Ico
sum_mul_Ico_le_integral_of_monotone_antitone 📖	mathematical	MonotoneOn Real Real.instPreorder Set.Icc Real.instNatCast AntitoneOn Real.instSub Real.instOne Real.instLE Real.instZero	Finset.sum Real.instAddCommMonoid Finset.Ico Nat.instPreorder Nat.instLocallyFiniteOrder Real.instMul intervalIntegral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.MeasureSpace.volume Real.measureSpace	—	sum_Ico_le_integral_of_le covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Nat.cast_one Real.instZeroLEOneClass RCLike.charZero_rclike AddGroup.toOrderedSub le_trans Nat.cast_add LE.le.trans LT.lt.le mul_le_mul IsOrderedRing.toPosMulMono Real.instIsOrderedRing IsOrderedRing.toMulPosMono sub_add_cancel MeasureTheory.Integrable.mono_measure MeasureTheory.Integrable.mul_of_top_left MonotoneOn.integrableOn_isCompact Real.borelSpace instOrderTopologyReal instSecondCountableTopologyReal MeasureTheory.Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts instIsAddHaarMeasureVolume FiniteDimensional.rclike_to_real CompactIccSpace.isCompact_Icc ConditionallyCompleteLinearOrder.toCompactIccSpace AntitoneOn.memLp_isCompact MeasureTheory.Measure.restrict_mono_set Set.Ico_subset_Icc_self

---

← Back to Index