DominatedConvergence

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

Statistics

Metric	Count
Definitions	0
Theorems limsup_lintegral_le, tendsto_lintegral_filter_of_dominated_convergence, tendsto_lintegral_of_dominated_convergence, tendsto_lintegral_of_dominated_convergence', tendsto_of_lintegral_tendsto_of_antitone, tendsto_of_lintegral_tendsto_of_monotone, tendsto_of_lintegral_tendsto_of_monotone_aux	7
Total	7

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
limsup_lintegral_le 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace Filter.EventuallyLE Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ae Measure Measure.instFunLike Measure.instOuterMeasureClass	Filter.limsup ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder lintegral Filter.atTop Nat.instPreorder	—	Measure.instOuterMeasureClass Filter.limsup_eq_iInf_iSup_of_nat iInf_mono iSup₂_lintegral_le lintegral_iInf Measurable.biSup ENNReal.borelSpace ENNReal.instOrderTopology ENNReal.instSecondCountableTopology Set.to_countable SetCoe.countable instCountableNat iSup_le_iSup_of_subset le_trans ne_top_of_le_ne_top lintegral_mono_ae Filter.Eventually.mono ae_all_iff iSup_le
tendsto_lintegral_filter_of_dominated_convergence 📖	mathematical	Filter.Eventually Measurable ENNReal ENNReal.measurableSpace Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ae Measure Measure.instFunLike Measure.instOuterMeasureClass Filter.Tendsto nhds ENNReal.instTopologicalSpace	lintegral	—	Measure.instOuterMeasureClass Filter.tendsto_iff_seq_tendsto Filter.tendsto_atTop' instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Filter.inter_mem Filter.tendsto_add_atTop_iff_nat tendsto_lintegral_of_dominated_convergence Filter.Eventually.mono Filter.Tendsto.comp
tendsto_lintegral_of_dominated_convergence 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace Filter.EventuallyLE Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ae Measure Measure.instFunLike Measure.instOuterMeasureClass Filter.Eventually Filter.Tendsto Filter.atTop Nat.instPreorder nhds ENNReal.instTopologicalSpace	lintegral	—	Measure.instOuterMeasureClass tendsto_of_le_liminf_of_limsup_le ENNReal.instOrderTopology lintegral_congr_ae Filter.Eventually.mono Filter.Tendsto.liminf_eq Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat lintegral_liminf_le limsup_lintegral_le Filter.Tendsto.limsup_eq Filter.isBounded_le_of_top Filter.isBounded_ge_of_bot
tendsto_lintegral_of_dominated_convergence' 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace Filter.EventuallyLE Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ae Measure Measure.instFunLike Measure.instOuterMeasureClass Filter.Eventually Filter.Tendsto Filter.atTop Nat.instPreorder nhds ENNReal.instTopologicalSpace	lintegral	—	Measure.instOuterMeasureClass lintegral_congr_ae tendsto_lintegral_of_dominated_convergence Filter.mp_mem Filter.univ_mem' Filter.EventuallyEq.symm ae_all_iff instCountableNat
tendsto_of_lintegral_tendsto_of_antitone 📖	—	AEMeasurable ENNReal ENNReal.measurableSpace Filter.Tendsto lintegral Filter.atTop Nat.instPreorder nhds ENNReal.instTopologicalSpace Filter.Eventually Antitone PartialOrder.toPreorder ENNReal.instPartialOrder ae Measure Measure.instFunLike Measure.instOuterMeasureClass	—	—	Measure.instOuterMeasureClass LT.lt.ne LE.le.trans_lt lintegral_mono_ae Filter.mp_mem Filter.univ_mem' Ne.lt_top tendsto_atTop_of_antitone ENNReal.instOrderTopology Filter.Tendsto.mono_right Filter.OrderBot.atBot_eq pure_le_nhds ge_of_tendsto' instClosedIciTopology OrderTopology.to_orderClosedTopology Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat tendsto_nhds_unique ENNReal.instT2Space lintegral_tendsto_of_tendsto_of_antitone Filter.EventuallyEq.symm ae_eq_of_ae_le_of_lintegral_le ENNReal.aemeasurable_of_tendsto Eq.le
tendsto_of_lintegral_tendsto_of_monotone 📖	—	AEMeasurable ENNReal ENNReal.measurableSpace Filter.Tendsto lintegral Filter.atTop Nat.instPreorder nhds ENNReal.instTopologicalSpace Filter.Eventually Monotone PartialOrder.toPreorder ENNReal.instPartialOrder ae Measure Measure.instFunLike Measure.instOuterMeasureClass	—	—	Measure.instOuterMeasureClass exists_measurable_le_lintegral_eq Measurable.max BorelSpace.opensMeasurable ENNReal.borelSpace ENNReal.instSecondCountableTopology OrderTopology.to_orderClosedTopology ENNReal.instOrderTopology Filter.mp_mem Filter.univ_mem' max_le LE.le.trans le_antisymm lintegral_mono_ae lintegral_mono tendsto_of_lintegral_tendsto_of_monotone_aux Measurable.aemeasurable Filter.Eventually.of_forall monotone_nat_of_le_succ le_max_right tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds
tendsto_of_lintegral_tendsto_of_monotone_aux 📖	—	AEMeasurable ENNReal ENNReal.measurableSpace Filter.Tendsto lintegral Filter.atTop Nat.instPreorder nhds ENNReal.instTopologicalSpace Filter.Eventually Monotone PartialOrder.toPreorder ENNReal.instPartialOrder ae Measure Measure.instFunLike Measure.instOuterMeasureClass	—	—	Measure.instOuterMeasureClass Filter.mp_mem ae_lt_top' Filter.univ_mem' LT.lt.ne tendsto_atTop_of_monotone ENNReal.instOrderTopology Filter.tendsto_atTop_atTop_iff_of_monotone instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat LE.le.trans not_le ENNReal.lt_add_right one_ne_zero NeZero.charZero_one ENNReal.instCharZero le_of_tendsto' instClosedIicTopology OrderTopology.to_orderClosedTopology Filter.atTop_neBot tendsto_nhds_unique ENNReal.instT2Space lintegral_tendsto_of_tendsto_of_monotone ae_eq_of_ae_le_of_lintegral_le Eq.le

---

← Back to Index