Add

📁 Source: Mathlib/MeasureTheory/Integral/Lebesgue/Add.lean

Statistics

Metric	Count
Definitions	0
Theorems le_lintegral_add, lintegral_add_aux, lintegral_add_left, lintegral_add_left', lintegral_add_right, lintegral_add_right', lintegral_const_mul, lintegral_const_mul', lintegral_const_mul'', lintegral_const_mul_le, lintegral_eapprox_le_lintegral, lintegral_eq_iSup_eapprox_lintegral, lintegral_finset_sum, lintegral_finset_sum', lintegral_iSup, lintegral_iSup', lintegral_iSup_ae, lintegral_iSup_directed, lintegral_iSup_directed_of_measurable, lintegral_liminf_le, lintegral_liminf_le', lintegral_lintegral_mul, lintegral_mul_const, lintegral_mul_const', lintegral_mul_const'', lintegral_mul_const_le, lintegral_tendsto_of_tendsto_of_monotone, lintegral_trim, lintegral_trim_ae, lintegral_tsum, measure_support_eapprox_lt_top, setLIntegral_trim, setLIntegral_trim_ae	33
Total	33

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
le_lintegral_add 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring lintegral	—	lintegral_def ENNReal.biSup_add_biSup_le' zero_le Pi.instCanonicallyOrderedAddForall ENNReal.instCanonicallyOrderedAdd le_iSup₂_of_le add_le_add IsOrderedAddMonoid.toAddLeftMono Pi.isOrderedAddMonoid ENNReal.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add Eq.ge SimpleFunc.add_lintegral
lintegral_add_aux 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace	lintegral Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	SimpleFunc.iSup_eapprox_apply ENNReal.iSup_add_iSup_of_monotone instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat SimpleFunc.monotone_eapprox lintegral_iSup Measurable.add' ContinuousAdd.measurableMul₂ ENNReal.borelSpace ENNReal.instSecondCountableTopology ENNReal.instContinuousAdd Measurable.fun_comp SimpleFunc.measurable Measurable.snd measurable_id' add_le_add IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add SimpleFunc.add_lintegral SimpleFunc.lintegral_eq_lintegral SimpleFunc.lintegral_mono le_rfl lintegral_eq_iSup_eapprox_lintegral
lintegral_add_left 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace	lintegral Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	le_antisymm exists_measurable_le_lintegral_eq lintegral_mono le_add_tsub ENNReal.instOrderedSub lintegral_add_aux Measurable.sub ENNReal.instMeasurableSub₂ add_le_add_right IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid lintegral_mono_fn' le_refl tsub_le_iff_left le_lintegral_add
lintegral_add_left' 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace	lintegral Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	lintegral_congr_ae lintegral_add_left Filter.EventuallyEq.fun_add Measure.instOuterMeasureClass ae_eq_refl
lintegral_add_right 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace	lintegral Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	lintegral_add_right' Measurable.aemeasurable
lintegral_add_right' 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace	lintegral Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	add_comm lintegral_add_left'
lintegral_const_mul 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace	lintegral Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	SimpleFunc.iSup_eapprox_apply ENNReal.mul_iSup lintegral_iSup SimpleFunc.measurable mul_le_mul_right IsOrderedMonoid.toMulLeftMono ENNReal.instIsOrderedMonoid SimpleFunc.monotone_eapprox SimpleFunc.const_mul_lintegral SimpleFunc.lintegral_eq_lintegral lintegral_eq_iSup_eapprox_lintegral
lintegral_const_mul' 📖	mathematical	—	lintegral ENNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	MulZeroClass.zero_mul lintegral_const le_antisymm ENNReal.mul_inv_cancel mul_comm lintegral_const_mul_le mul_assoc one_mul mul_le_mul_right IsOrderedMonoid.toMulLeftMono ENNReal.instIsOrderedMonoid
lintegral_const_mul'' 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace	lintegral Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	lintegral_congr_ae Filter.EventuallyEq.fun_comp Measure.instOuterMeasureClass lintegral_const_mul
lintegral_const_mul_le 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring lintegral	—	lintegral_def ENNReal.mul_iSup iSup_le iSup_le_iff SimpleFunc.const_mul_lintegral le_iSup_of_le le_imp_le_of_le_of_le mul_le_mul_right IsOrderedMonoid.toMulLeftMono ENNReal.instIsOrderedMonoid le_refl le_rfl
lintegral_eapprox_le_lintegral 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace	Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder SimpleFunc.lintegral SimpleFunc.eapprox lintegral	—	lintegral_eq_iSup_eapprox_lintegral le_iSup
lintegral_eq_iSup_eapprox_lintegral 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace	lintegral iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder SimpleFunc.lintegral SimpleFunc.eapprox	—	SimpleFunc.iSup_eapprox_apply lintegral_iSup SimpleFunc.measurable SimpleFunc.monotone_eapprox SimpleFunc.lintegral_eq_lintegral
lintegral_finset_sum 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace	lintegral Finset.sum ENNReal.instAddCommMonoid	—	lintegral_finset_sum' Measurable.aemeasurable
lintegral_finset_sum' 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace	lintegral Finset.sum ENNReal.instAddCommMonoid	—	Finset.induction_on lintegral_const MulZeroClass.zero_mul Finset.sum_insert lintegral_add_left' Finset.forall_mem_insert
lintegral_iSup 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace Monotone Nat.instPreorder Pi.preorder PartialOrder.toPreorder ENNReal.instPartialOrder	lintegral iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder	—	le_antisymm lintegral_eq_nnreal iSup_le ENNReal.le_of_forall_lt_one_mul_le ENNReal.lt_iff_exists_coe ENNReal.coe_lt_coe Set.inter_iUnion Set.inter_univ Set.ext ENNReal.instCanonicallyOrderedAdd ENNReal.coe_eq_zero right_ne_zero_of_mul lt_of_lt_of_le mul_lt_mul_of_pos_right IsStrictOrderedRing.toMulPosStrictMono NNReal.instIsStrictOrderedRing pos_iff_ne_zero NNReal.instCanonicallyOrderedAdd one_mul lt_iSup_iff Set.mem_iUnion le_of_lt Set.inter_subset_inter_right le_trans measurableSet_le BorelSpace.opensMeasurable ENNReal.borelSpace OrderTopology.to_orderClosedTopology ENNReal.instOrderTopology ENNReal.instSecondCountableTopology SimpleFunc.measurable SimpleFunc.const_mul_lintegral SimpleFunc.lintegral.eq_1 Finset.sum_congr Monotone.measure_iUnion instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat instIsCountablyGenerated_atTop OrderTopology.of_linearLocallyFinite instDiscreteTopologyNat TopologicalSpace.SecondCountableTopology.to_separableSpace TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace Countable.LindelofSpace instCountableNat PseudoEMetricSpace.pseudoMetrizableSpace ENNReal.mul_iSup ENNReal.finsetSum_iSup_of_monotone mul_le_mul_right IsOrderedMonoid.toMulLeftMono ENNReal.instIsOrderedMonoid measure_mono Measure.instOuterMeasureClass iSup_mono SimpleFunc.restrict_lintegral le_of_eq lintegral_mono_fn' le_refl SimpleFunc.restrict_apply Set.indicator_apply_le iSup_lintegral_le
lintegral_iSup' 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace Filter.Eventually Monotone Nat.instPreorder PartialOrder.toPreorder ENNReal.instPartialOrder ae Measure Measure.instFunLike Measure.instOuterMeasureClass	lintegral iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder	—	Measure.instOuterMeasureClass aeSeq.prop_of_mem_aeSeqSet lintegral_congr_ae Filter.EventuallyEq.symm aeSeq.iSup instCountableNat iSup_apply lintegral_iSup aeSeq.measurable aeSeq.aeSeq_n_eq_fun_n_ae
lintegral_iSup_ae 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace Filter.Eventually Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ae Measure Measure.instFunLike Measure.instOuterMeasureClass	lintegral iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder	—	Measure.instOuterMeasureClass exists_measurable_superset_of_null ae_iff ae_all_iff instCountableNat Filter.Eventually.mono measure_eq_zero_iff_ae_notMem lintegral_congr_ae lintegral_iSup Measurable.piecewise measurable_const monotone_nat_of_le_succ le_refl Set.notMem_subset
lintegral_iSup_directed 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace Directed Pi.hasLe Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder	lintegral iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder	—	Measure.instOuterMeasureClass Filter.univ_mem' aeSeq.aeSeq_eq_fun_of_mem_aeSeqSet le_rfl lintegral_congr_ae Filter.EventuallyEq.symm aeSeq.iSup aeSeq.aeSeq_n_eq_fun_n_ae lintegral_iSup_directed_of_measurable aeSeq.measurable
lintegral_iSup_directed_of_measurable 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace Directed Pi.hasLe Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder	lintegral iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder	—	nonempty_encodable isEmpty_or_nonempty ciSup_of_empty bot_eq_zero' ENNReal.instCanonicallyOrderedAdd lintegral_const MulZeroClass.zero_mul le_antisymm iSup_le le_iSup_of_le Directed.le_sequence le_iSup lintegral_iSup Directed.sequence_mono lintegral_mono
lintegral_liminf_le 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace	Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder lintegral Filter.liminf ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder Filter.atTop Nat.instPreorder	—	lintegral_liminf_le' Measurable.aemeasurable
lintegral_liminf_le' 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace	Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder lintegral Filter.liminf ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder Filter.atTop Nat.instPreorder	—	Filter.liminf_eq_iSup_iInf_of_nat lintegral_iSup' AEMeasurable.biInf ENNReal.borelSpace ENNReal.instOrderTopology ENNReal.instSecondCountableTopology Set.to_countable SetCoe.countable instCountableNat ae_of_all Measure.instOuterMeasureClass iInf_le_iInf_of_subset le_trans iSup_mono le_iInf₂_lintegral
lintegral_lintegral_mul 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace	lintegral Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	lintegral_const_mul'' lintegral_mul_const''
lintegral_mul_const 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace	lintegral Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	mul_comm lintegral_const_mul
lintegral_mul_const' 📖	mathematical	—	lintegral ENNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	mul_comm lintegral_const_mul'
lintegral_mul_const'' 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace	lintegral Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	mul_comm lintegral_const_mul''
lintegral_mul_const_le 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring lintegral	—	mul_comm lintegral_const_mul_le
lintegral_tendsto_of_tendsto_of_monotone 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace Filter.Eventually Monotone Nat.instPreorder PartialOrder.toPreorder ENNReal.instPartialOrder ae Measure Measure.instFunLike Measure.instOuterMeasureClass Filter.Tendsto Filter.atTop nhds ENNReal.instTopologicalSpace	lintegral	—	Measure.instOuterMeasureClass lintegral_mono_ae Filter.Eventually.mono lintegral_iSup' lintegral_congr_ae Filter.mp_mem Filter.univ_mem' tendsto_nhds_unique ENNReal.instT2Space Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat tendsto_atTop_iSup LinearOrder.supConvergenceClass ENNReal.instOrderTopology
lintegral_trim 📖	mathematical	MeasurableSpace MeasurableSpace.instLE Measurable ENNReal ENNReal.measurableSpace	lintegral Measure.trim	—	Measurable.ennreal_induction lintegral_indicator setLIntegral_const trim_measurableSet_eq lintegral_add_left Measurable.mono le_rfl lintegral_iSup
lintegral_trim_ae 📖	mathematical	MeasurableSpace MeasurableSpace.instLE AEMeasurable ENNReal ENNReal.measurableSpace Measure.trim	lintegral	—	lintegral_congr_ae ae_eq_of_ae_eq_trim lintegral_trim
lintegral_tsum 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace	lintegral tsum ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace SummationFilter.unconditional	—	ENNReal.tsum_eq_iSup_sum lintegral_iSup_directed Finset.countable Finset.aemeasurable_fun_sum ContinuousAdd.measurableMul₂ ENNReal.borelSpace ENNReal.instSecondCountableTopology ENNReal.instContinuousAdd Finset.sum_le_sum_of_subset ENNReal.instCanonicallyOrderedAdd Finset.subset_union_left Finset.subset_union_right lintegral_finset_sum'
measure_support_eapprox_lt_top 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace	Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe Measure Set Measure.instFunLike Function.support instZeroENNReal SimpleFunc SimpleFunc.instFunLike SimpleFunc.eapprox Top.top instTopENNReal	—	SimpleFunc.measure_support_lt_top_of_lintegral_ne_top LT.lt.ne LE.le.trans_lt lintegral_eapprox_le_lintegral Ne.lt_top
setLIntegral_trim 📖	mathematical	MeasurableSpace MeasurableSpace.instLE Measurable ENNReal ENNReal.measurableSpace MeasurableSet	lintegral Measure.restrict Measure.trim	—	setLIntegral_trim_ae Measurable.aemeasurable
setLIntegral_trim_ae 📖	mathematical	MeasurableSpace MeasurableSpace.instLE AEMeasurable ENNReal ENNReal.measurableSpace Measure.trim MeasurableSet	lintegral Measure.restrict	—	lintegral_trim_ae restrict_trim AEMeasurable.restrict

---

← Back to Index