Documentation Verification Report

ConvergenceInMeasure

📁 Source: Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean

Statistics

Metric	Count
Definitions `seqTendstoAeSeq`, `seqTendstoAeSeqAux`, `TendstoInMeasure`	3
Theorems `exists_nat_measure_lt_two_inv`, `seqTendstoAeSeq_spec`, `seqTendstoAeSeq_strictMono`, `seqTendstoAeSeq_succ`, `aemeasurable`, `aestronglyMeasurable`, `comp`, `congr'`, `congr_left`, `congr_right`, `exists_seq_tendstoInMeasure_atTop`, `exists_seq_tendsto_ae`, `exists_seq_tendsto_ae'`, `indicator`, `mono`, `eLpNorm_le_of_tendstoInMeasure`, `exists_seq_tendstoInMeasure_atTop_iff`, `tendstoInMeasure_ae_unique`, `tendstoInMeasure_iff_dist`, `tendstoInMeasure_iff_enorm`, `tendstoInMeasure_iff_measureReal_dist`, `tendstoInMeasure_iff_measureReal_enorm`, `tendstoInMeasure_iff_measureReal_norm`, `tendstoInMeasure_iff_norm`, `tendstoInMeasure_iff_tendsto_toNNReal`, `tendstoInMeasure_of_ne_top`, `tendstoInMeasure_of_tendsto_Lp`, `tendstoInMeasure_of_tendsto_ae`, `tendstoInMeasure_of_tendsto_ae_of_measurable_edist`, `tendstoInMeasure_of_tendsto_eLpNorm`, `tendstoInMeasure_of_tendsto_eLpNorm_of_ne_top`, `tendstoInMeasure_of_tendsto_eLpNorm_of_stronglyMeasurable`, `tendstoInMeasure_of_tendsto_eLpNorm_top`	33
Total	36

MeasureTheory

Definitions

Name	Category	Theorems
`TendstoInMeasure` 📖	MathDef	28 math math: `tendstoInMeasure_iff_measureReal_norm`, `TendstoInMeasure.exists_seq_tendstoInMeasure_atTop`, `UniformIntegrable.uniformIntegrable_of_tendstoInMeasure`, `tendstoInMeasure_of_tendsto_eLpNorm_of_stronglyMeasurable`, `tendstoInMeasure_of_tendsto_eLpNorm_top`, `tendstoInMeasure_iff_tendsto_Lp`, `tendstoInMeasure_iff_norm`, `tendstoInMeasure_of_tendsto_ae_of_measurable_edist`, `TendstoInMeasure.indicator`, `tendstoInMeasure_iff_measureReal_dist`, `TendstoInMeasure.mono`, `UnifIntegrable.unifIntegrable_of_tendstoInMeasure`, `tendstoInMeasure_iff_dist`, `tendstoInMeasure_of_tendsto_eLpNorm`, `TendstoInMeasure.congr'`, `tendstoInMeasure_iff_measureReal_enorm`, `tendstoInMeasure_of_ne_top`, `tendstoInMeasure_of_tendsto_Lp`, `tendstoInMeasure_iff_tendsto_toNNReal`, `TendstoInMeasure.congr_right`, `tendstoInMeasure_of_tendsto_eLpNorm_of_ne_top`, `exists_seq_tendstoInMeasure_atTop_iff`, `TendstoInMeasure.congr_left`, `tendstoInMeasure_iff_enorm`, `TendstoInMeasure.congr`, `tendstoInMeasure_of_tendsto_ae`, `TendstoInMeasure.comp`, `tendstoInMeasure_iff_tendsto_Lp_finite`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eLpNorm_le_of_tendstoInMeasure` 📖	mathematical	`Filter.Eventually` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `eLpNorm` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `TendstoInMeasure` `PseudoEMetricSpace.toEDist` `PseudoMetricSpace.toPseudoEMetricSpace` `AEStronglyMeasurable`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `eLpNorm` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm`	—	`Measure.instOuterMeasureClass` `TendstoInMeasure.exists_seq_tendsto_ae'` `Lp.eLpNorm_le_of_ae_tendsto` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `instIsCountablyGenerated_atTop` `OrderTopology.of_linearLocallyFinite` `instDiscreteTopologyNat` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace` `Countable.LindelofSpace` `instCountableNat` `PseudoEMetricSpace.pseudoMetrizableSpace` `Filter.Tendsto.eventually`
`exists_seq_tendstoInMeasure_atTop_iff` 📖	mathematical	`AEStronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	`TendstoInMeasure` `PseudoEMetricSpace.toEDist` `Filter.atTop` `Nat.instPreorder` `StrictMono` `Filter.Eventually` `Filter.Tendsto` `nhds` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass`	—	`Measure.instOuterMeasureClass` `TendstoInMeasure.exists_seq_tendsto_ae` `TendstoInMeasure.comp` `StrictMono.tendsto_atTop` `tendstoInMeasure_iff_tendsto_toNNReal` `Mathlib.Tactic.Push.not_forall_eq` `Filter.not_tendsto_iff_exists_frequently_notMem` `Filter.HasBasis.mem_iff` `NNReal.nhds_zero_basis` `Filter.extraction_of_frequently_atTop` `Set.notMem_Iio` `Set.notMem_subset` `tendstoInMeasure_of_tendsto_ae` `lt_irrefl` `lt_of_le_of_lt` `ge_of_tendsto'` `instClosedIciTopology` `OrderTopology.to_orderClosedTopology` `NNReal.instOrderTopology` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat`
`tendstoInMeasure_ae_unique` 📖	mathematical	`TendstoInMeasure` `PseudoEMetricSpace.toEDist` `EMetricSpace.toPseudoEMetricSpace`	`Filter.EventuallyEq` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass`	—	`Measure.instOuterMeasureClass` `TendstoInMeasure.exists_seq_tendsto_ae'` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `instIsCountablyGenerated_atTop` `OrderTopology.of_linearLocallyFinite` `instDiscreteTopologyNat` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace` `Countable.LindelofSpace` `instCountableNat` `PseudoEMetricSpace.pseudoMetrizableSpace` `TendstoInMeasure.comp` `Filter.mp_mem` `Filter.univ_mem'` `tendsto_nhds_unique` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `Filter.Tendsto.comp`
`tendstoInMeasure_iff_dist` 📖	mathematical	—	`TendstoInMeasure` `PseudoEMetricSpace.toEDist` `PseudoMetricSpace.toPseudoEMetricSpace` `Filter.Tendsto` `ENNReal` `DFunLike.coe` `Measure` `Set` `Measure.instFunLike` `setOf` `Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `nhds` `ENNReal.instTopologicalSpace` `instZeroENNReal`	—	`edist_dist` `ENNReal.ofReal_le_ofReal_iff` `dist_nonneg` `ENNReal.ofReal_pos` `tendstoInMeasure_of_ne_top` `ENNReal.le_ofReal_iff_toReal_le` `ENNReal.toReal_pos` `LT.lt.ne'`
`tendstoInMeasure_iff_enorm` 📖	mathematical	—	`TendstoInMeasure` `PseudoEMetricSpace.toEDist` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Filter.Tendsto` `ENNReal` `DFunLike.coe` `Measure` `Set` `Measure.instFunLike` `setOf` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ENorm.enorm` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `SeminormedAddGroup.toContinuousENorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `nhds` `ENNReal.instTopologicalSpace` `instZeroENNReal`	—	`tendstoInMeasure_of_ne_top`
`tendstoInMeasure_iff_measureReal_dist` 📖	mathematical	—	`TendstoInMeasure` `PseudoEMetricSpace.toEDist` `PseudoMetricSpace.toPseudoEMetricSpace` `Filter.Tendsto` `Real` `Measure.real` `setOf` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instZero`	—	`tendstoInMeasure_iff_dist` `ENNReal.tendsto_toReal_zero_iff` `measure_ne_top`
`tendstoInMeasure_iff_measureReal_enorm` 📖	mathematical	—	`TendstoInMeasure` `PseudoEMetricSpace.toEDist` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Filter.Tendsto` `Real` `Measure.real` `setOf` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ENorm.enorm` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `SeminormedAddGroup.toContinuousENorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `nhds` `Real.pseudoMetricSpace` `Real.instZero`	—	`tendstoInMeasure_iff_enorm` `ENNReal.tendsto_toReal_zero_iff` `measure_ne_top`
`tendstoInMeasure_iff_measureReal_norm` 📖	mathematical	—	`TendstoInMeasure` `PseudoEMetricSpace.toEDist` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Filter.Tendsto` `Real` `Measure.real` `setOf` `Real.instLE` `Norm.norm` `SeminormedAddCommGroup.toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instZero`	—	`tendstoInMeasure_iff_norm` `ENNReal.tendsto_toReal_zero_iff` `measure_ne_top`
`tendstoInMeasure_iff_norm` 📖	mathematical	—	`TendstoInMeasure` `PseudoEMetricSpace.toEDist` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Filter.Tendsto` `ENNReal` `DFunLike.coe` `Measure` `Set` `Measure.instFunLike` `setOf` `Real` `Real.instLE` `Norm.norm` `SeminormedAddCommGroup.toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `nhds` `ENNReal.instTopologicalSpace` `instZeroENNReal`	—	`dist_eq_norm_sub`
`tendstoInMeasure_iff_tendsto_toNNReal` 📖	mathematical	—	`TendstoInMeasure` `Filter.Tendsto` `NNReal` `ENNReal.toNNReal` `DFunLike.coe` `Measure` `Set` `ENNReal` `Measure.instFunLike` `setOf` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `EDist.edist` `nhds` `NNReal.instTopologicalSpace` `NNReal.instZero`	—	`measure_ne_top` `ENNReal.tendsto_toNNReal_iff'` `ENNReal.tendsto_toNNReal_iff` `ENNReal.zero_ne_top`
`tendstoInMeasure_of_ne_top` 📖	mathematical	`Filter.Tendsto` `ENNReal` `DFunLike.coe` `Measure` `Set` `Measure.instFunLike` `setOf` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `EDist.edist` `nhds` `ENNReal.instTopologicalSpace` `instZeroENNReal`	`TendstoInMeasure`	—	`IsOrderedRing.toZeroLEOneClass` `ENNReal.instIsOrderedRing` `NeZero.charZero_one` `ENNReal.instCharZero` `tendsto_of_tendsto_of_tendsto_of_le_of_le` `ENNReal.instOrderTopology` `tendsto_const_nhds` `zero_le` `ENNReal.instCanonicallyOrderedAdd` `measure_mono` `Measure.instOuterMeasureClass` `Set.setOf_subset_setOf_of_imp` `le_imp_le_of_le_of_le` `le_refl`
`tendstoInMeasure_of_tendsto_Lp` 📖	mathematical	`Filter.Tendsto` `AEEqFun` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddSubgroup` `AEEqFun.instAddGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `Lp` `nhds` `Lp.instNormedAddCommGroup`	`TendstoInMeasure` `PseudoEMetricSpace.toEDist` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `AEEqFun.cast` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AEEqFun` `AddSubgroup` `AEEqFun.instAddGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `Lp`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `tendstoInMeasure_of_tendsto_eLpNorm` `LT.lt.ne` `LT.lt.trans_le` `zero_lt_one` `IsOrderedRing.toZeroLEOneClass` `ENNReal.instIsOrderedRing` `NeZero.charZero_one` `ENNReal.instCharZero` `Fact.elim` `Lp.aestronglyMeasurable` `Lp.tendsto_Lp_iff_tendsto_eLpNorm'`
`tendstoInMeasure_of_tendsto_ae` 📖	mathematical	`AEStronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `Filter.Eventually` `Filter.Tendsto` `Filter.atTop` `Nat.instPreorder` `nhds` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass`	`TendstoInMeasure` `PseudoEMetricSpace.toEDist` `Filter.atTop` `Nat.instPreorder`	—	`Measure.instOuterMeasureClass` `aestronglyMeasurable_of_tendsto_ae` `PseudoEMetricSpace.pseudoMetrizableSpace` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `instIsCountablyGenerated_atTop` `OrderTopology.of_linearLocallyFinite` `instDiscreteTopologyNat` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace` `Countable.LindelofSpace` `instCountableNat` `TendstoInMeasure.congr` `Filter.EventuallyEq.symm` `tendstoInMeasure_of_tendsto_ae_of_measurable_edist` `StronglyMeasurable.measurable` `TopologicalSpace.MetrizableSpace.toPseudoMetrizableSpace` `ENNReal.instMetrizableSpace` `ENNReal.borelSpace` `StronglyMeasurable.edist` `ae_all_iff` `Filter.mp_mem` `Filter.univ_mem'`
`tendstoInMeasure_of_tendsto_ae_of_measurable_edist` 📖	mathematical	`Measurable` `ENNReal` `ENNReal.measurableSpace` `EDist.edist` `PseudoEMetricSpace.toEDist` `Filter.Eventually` `Filter.Tendsto` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass`	`TendstoInMeasure` `PseudoEMetricSpace.toEDist` `Filter.atTop` `Nat.instPreorder`	—	`Measure.instOuterMeasureClass` `ENNReal.tendsto_atTop_zero` `CanLift.prf` `ENNReal.canLift` `tendstoUniformlyOn_of_ae_tendsto_of_measurable_edist'` `instCountableNat` `NNReal.coe_pos` `ENNReal.coe_pos` `Filter.eventually_atTop` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `EMetric.tendstoUniformlyOn_iff` `Set.compl_subset_compl` `Set.mem_compl_iff` `Set.notMem_setOf_iff` `PseudoEMetricSpace.edist_comm` `not_le` `LE.le.trans` `measure_mono` `ENNReal.ofReal_coe_nnreal`
`tendstoInMeasure_of_tendsto_eLpNorm` 📖	mathematical	`AEStronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Filter.Tendsto` `ENNReal` `eLpNorm` `ContinuousENorm.toENorm` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `SeminormedAddGroup.toContinuousENorm` `Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `nhds` `ENNReal.instTopologicalSpace` `instZeroENNReal`	`TendstoInMeasure` `PseudoEMetricSpace.toEDist` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace`	—	`tendstoInMeasure_of_tendsto_eLpNorm_top` `tendstoInMeasure_of_tendsto_eLpNorm_of_ne_top`
`tendstoInMeasure_of_tendsto_eLpNorm_of_ne_top` 📖	mathematical	`AEStronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Filter.Tendsto` `ENNReal` `eLpNorm` `ContinuousENorm.toENorm` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `SeminormedAddGroup.toContinuousENorm` `Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `nhds` `ENNReal.instTopologicalSpace` `instZeroENNReal`	`TendstoInMeasure` `PseudoEMetricSpace.toEDist` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`TendstoInMeasure.congr` `Filter.EventuallyEq.symm` `Measure.instOuterMeasureClass` `tendstoInMeasure_of_tendsto_eLpNorm_of_stronglyMeasurable` `eLpNorm_congr_ae` `Filter.EventuallyEq.sub`
`tendstoInMeasure_of_tendsto_eLpNorm_of_stronglyMeasurable` 📖	mathematical	`StronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Filter.Tendsto` `ENNReal` `eLpNorm` `ContinuousENorm.toENorm` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `SeminormedAddGroup.toContinuousENorm` `Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `nhds` `ENNReal.instTopologicalSpace` `instZeroENNReal`	`TendstoInMeasure` `PseudoEMetricSpace.toEDist` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`tendstoInMeasure_of_ne_top` `ENNReal.Tendsto.const_mul` `Filter.Tendsto.ennrpow_const` `one_div` `LT.lt.ne'` `ENNReal.tendsto_nhds_zero` `Filter.Eventually.mono` `ENNReal.zero_rpow_of_pos` `ENNReal.toReal_pos` `MulZeroClass.mul_zero` `le_trans` `ENNReal.inv_mul_le_iff` `inv_inv` `edist_eq_enorm_sub` `mul_meas_ge_le_pow_eLpNorm'` `StronglyMeasurable.aestronglyMeasurable` `StronglyMeasurable.sub` `IsTopologicalAddGroup.to_continuousSub` `SeminormedAddCommGroup.toIsTopologicalAddGroup`
`tendstoInMeasure_of_tendsto_eLpNorm_top` 📖	mathematical	`Filter.Tendsto` `ENNReal` `eLpNorm` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `SeminormedAddGroup.toContinuousENorm` `Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `Top.top` `instTopENNReal` `nhds` `ENNReal.instTopologicalSpace` `instZeroENNReal`	`TendstoInMeasure` `PseudoEMetricSpace.toEDist` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`tendstoInMeasure_of_ne_top` `ENNReal.tendsto_nhds_zero` `Filter.Eventually.mono` `Nat.instAtLeastTwoHAddOfNat` `eLpNorm_exponent_top` `ENNReal.div_pos_iff` `LT.lt.ne'` `ENNReal.ofNat_ne_top` `LE.le.trans_lt` `ENNReal.half_lt_self` `LE.le.trans` `le_of_eq` `edist_eq_enorm_sub` `Eq.le` `ae_lt_of_essSup_lt` `Filter.isBounded_le_of_top` `Measure.instOuterMeasureClass` `LT.lt.le`

MeasureTheory.ExistsSeqTendstoAe

Definitions

Name	Category	Theorems
`seqTendstoAeSeq` 📖	CompOp	2 math math: `seqTendstoAeSeq_strictMono`, `seqTendstoAeSeq_succ`
`seqTendstoAeSeqAux` 📖	CompOp	1 math math: `seqTendstoAeSeq_succ`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_nat_measure_lt_two_inv` 📖	mathematical	`MeasureTheory.TendstoInMeasure` `PseudoEMetricSpace.toEDist` `Filter.atTop` `Nat.instPreorder`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `setOf` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instInv` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `EDist.edist` `PseudoEMetricSpace.toEDist`	—	`Nat.instAtLeastTwoHAddOfNat` `ENNReal.tendsto_atTop_zero` `ENNReal.pow_pos` `pos_iff_ne_zero` `ENNReal.instCanonicallyOrderedAdd` `pow_ne_zero` `isReduced_of_noZeroDivisors` `ENNReal.instNoZeroDivisors`
`seqTendstoAeSeq_spec` 📖	mathematical	`MeasureTheory.TendstoInMeasure` `PseudoEMetricSpace.toEDist` `Filter.atTop` `Nat.instPreorder` `seqTendstoAeSeq`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `setOf` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instInv` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `EDist.edist` `PseudoEMetricSpace.toEDist`	—	`Nat.instAtLeastTwoHAddOfNat` `exists_nat_measure_lt_two_inv` `le_trans` `le_max_left`
`seqTendstoAeSeq_strictMono` 📖	mathematical	`MeasureTheory.TendstoInMeasure` `PseudoEMetricSpace.toEDist` `Filter.atTop` `Nat.instPreorder`	`StrictMono` `Nat.instPreorder` `seqTendstoAeSeq`	—	`strictMono_nat_of_lt_succ` `seqTendstoAeSeq_succ` `lt_of_lt_of_le` `lt_add_one` `Nat.instZeroLEOneClass` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Nat.instIsOrderedCancelAddMonoid` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `le_max_right`
`seqTendstoAeSeq_succ` 📖	mathematical	`MeasureTheory.TendstoInMeasure` `PseudoEMetricSpace.toEDist` `Filter.atTop` `Nat.instPreorder`	`seqTendstoAeSeq` `seqTendstoAeSeqAux`	—	`seqTendstoAeSeq.eq_2`

MeasureTheory.TendstoInMeasure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`aemeasurable` 📖	mathematical	`AEMeasurable` `MeasureTheory.TendstoInMeasure` `PseudoEMetricSpace.toEDist`	`AEMeasurable`	—	`MeasureTheory.Measure.instOuterMeasureClass` `exists_seq_tendsto_ae'` `aemeasurable_of_tendsto_metrizable_ae` `PseudoEMetricSpace.pseudoMetrizableSpace` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `instIsCountablyGenerated_atTop` `OrderTopology.of_linearLocallyFinite` `instDiscreteTopologyNat` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace` `Countable.LindelofSpace` `instCountableNat`
`aestronglyMeasurable` 📖	mathematical	`MeasureTheory.AEStronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `MeasureTheory.TendstoInMeasure` `PseudoEMetricSpace.toEDist`	`MeasureTheory.AEStronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	—	`MeasureTheory.Measure.instOuterMeasureClass` `exists_seq_tendsto_ae'` `aestronglyMeasurable_of_tendsto_ae` `PseudoEMetricSpace.pseudoMetrizableSpace` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `instIsCountablyGenerated_atTop` `OrderTopology.of_linearLocallyFinite` `instDiscreteTopologyNat` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace` `Countable.LindelofSpace` `instCountableNat`
`comp` 📖	mathematical	`MeasureTheory.TendstoInMeasure` `Filter.Tendsto`	`MeasureTheory.TendstoInMeasure`	—	`Filter.Tendsto.comp`
`congr'` 📖	mathematical	`Filter.Eventually` `Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.TendstoInMeasure`	`MeasureTheory.TendstoInMeasure`	—	`MeasureTheory.Measure.instOuterMeasureClass` `Filter.mp_mem` `Filter.univ_mem'` `MeasureTheory.measure_congr` `Filter.tendsto_congr'`
`congr_left` 📖	mathematical	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.TendstoInMeasure`	`MeasureTheory.TendstoInMeasure`	—	`MeasureTheory.Measure.instOuterMeasureClass` `congr` `Filter.EventuallyEq.rfl`
`congr_right` 📖	mathematical	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.TendstoInMeasure`	`MeasureTheory.TendstoInMeasure`	—	`MeasureTheory.Measure.instOuterMeasureClass` `congr` `Filter.EventuallyEq.rfl`
`exists_seq_tendstoInMeasure_atTop` 📖	mathematical	`MeasureTheory.TendstoInMeasure` `PseudoEMetricSpace.toEDist`	`Filter.Tendsto` `Filter.atTop` `Nat.instPreorder` `MeasureTheory.TendstoInMeasure` `PseudoEMetricSpace.toEDist`	—	`Filter.exists_seq_tendsto` `Filter.Tendsto.comp`
`exists_seq_tendsto_ae` 📖	mathematical	`MeasureTheory.TendstoInMeasure` `PseudoEMetricSpace.toEDist` `Filter.atTop` `Nat.instPreorder`	`StrictMono` `Nat.instPreorder` `Filter.Eventually` `Filter.Tendsto` `Filter.atTop` `nhds` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	`Nat.instAtLeastTwoHAddOfNat` `ENNReal.exists_inv_two_pow_lt` `LT.lt.ne'` `pow_succ'` `mul_assoc` `ENNReal.mul_inv_cancel` `ne_of_gt` `Mathlib.Meta.Positivity.pos_of_isNat` `ENNReal.instIsOrderedRing` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `one_mul` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq_spec` `le_rfl` `MeasureTheory.measure_limsup_atTop_eq_zero` `ne_top_of_le_ne_top` `ENNReal.tsum_geometric` `ENNReal.one_sub_inv_two` `inv_inv` `ENNReal.ofNat_ne_top` `ENNReal.tsum_le_tsum` `EMetric.tendsto_atTop` `iSup_congr_Prop` `Set.compl_iInter` `Set.compl_iUnion` `Filter.limsup_eq_iInf_iSup_of_nat` `lt_of_le_of_lt` `pow_one` `mul_comm` `ENNReal.inv_pow` `ENNReal.inv_le_iff_le_mul` `isReduced_of_noZeroDivisors` `ENNReal.instNoZeroDivisors` `ENNReal.instCharZero` `pow_add` `pow_le_pow_right₀` `IsOrderedRing.toZeroLEOneClass` `IsOrderedRing.toPosMulMono` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `le_trans` `LT.lt.le` `LE.le.trans` `le_max_left` `MeasureTheory.ae_iff` `MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq_strictMono` `MeasureTheory.measure_mono_null` `Set.mem_setOf_eq` `not_imp_not`
`exists_seq_tendsto_ae'` 📖	mathematical	`MeasureTheory.TendstoInMeasure` `PseudoEMetricSpace.toEDist`	`Filter.Tendsto` `Filter.atTop` `Nat.instPreorder` `Filter.Eventually` `nhds` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	`MeasureTheory.Measure.instOuterMeasureClass` `exists_seq_tendstoInMeasure_atTop` `exists_seq_tendsto_ae` `Filter.Tendsto.comp` `StrictMono.tendsto_atTop`
`indicator` 📖	mathematical	`MeasureTheory.TendstoInMeasure` `PseudoEMetricSpace.toEDist`	`MeasureTheory.TendstoInMeasure` `PseudoEMetricSpace.toEDist` `Set.indicator`	—	`tendsto_of_tendsto_of_tendsto_of_le_of_le` `ENNReal.instOrderTopology` `tendsto_const_nhds` `ENNReal.instCanonicallyOrderedAdd` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass` `Set.indicator_of_mem` `Set.indicator_of_notMem` `PseudoEMetricSpace.edist_self`
`mono` 📖	mathematical	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `MeasureTheory.TendstoInMeasure`	`MeasureTheory.TendstoInMeasure`	—	`Filter.Tendsto.mono_left`

---

← Back to Index