Documentation Verification Report

Egorov

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

Statistics

Metric	Count
Definitions `iUnionNotConvergentSeq`, `notConvergentSeq`, `notConvergentSeqLTIndex`	3
Theorems `exists_notConvergentSeq_lt`, `iUnionNotConvergentSeq_measurableSet`, `iUnionNotConvergentSeq_subset`, `measure_iUnionNotConvergentSeq`, `measure_inter_notConvergentSeq_eq_zero`, `measure_notConvergentSeq_tendsto_zero`, `mem_notConvergentSeq_iff`, `notConvergentSeqLTIndex_spec`, `notConvergentSeq_antitone`, `notConvergentSeq_measurableSet`, `tendstoUniformlyOn_diff_iUnionNotConvergentSeq`, `tendstoUniformlyOn_of_ae_tendsto`, `tendstoUniformlyOn_of_ae_tendsto'`, `tendstoUniformlyOn_of_ae_tendsto_of_measurable_edist`, `tendstoUniformlyOn_of_ae_tendsto_of_measurable_edist'`	15
Total	18

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tendstoUniformlyOn_of_ae_tendsto` 📖	mathematical	`StronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `MeasurableSet` `Filter.Eventually` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `Real` `Real.instLT` `Real.instZero`	`Set` `Set.instHasSubset` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `ENNReal.ofReal` `TendstoUniformlyOn` `Filter.atTop` `SemilatticeSup.toPartialOrder` `Set.instSDiff`	—	`Measure.instOuterMeasureClass` `tendstoUniformlyOn_of_ae_tendsto_of_measurable_edist` `StronglyMeasurable.measurable` `TopologicalSpace.MetrizableSpace.toPseudoMetrizableSpace` `ENNReal.instMetrizableSpace` `ENNReal.borelSpace` `StronglyMeasurable.edist`
`tendstoUniformlyOn_of_ae_tendsto'` 📖	mathematical	`StronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `Filter.Eventually` `Filter.Tendsto` `Filter.atTop` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `nhds` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `Real` `Real.instLT` `Real.instZero`	`MeasurableSet` `ENNReal` `Preorder.toLE` `ENNReal.instPartialOrder` `DFunLike.coe` `Set` `ENNReal.ofReal` `TendstoUniformlyOn` `Compl.compl` `Set.instCompl`	—	`Measure.instOuterMeasureClass` `tendstoUniformlyOn_of_ae_tendsto_of_measurable_edist'` `StronglyMeasurable.measurable` `TopologicalSpace.MetrizableSpace.toPseudoMetrizableSpace` `ENNReal.instMetrizableSpace` `ENNReal.borelSpace` `StronglyMeasurable.edist`
`tendstoUniformlyOn_of_ae_tendsto_of_measurable_edist` 📖	mathematical	`Measurable` `ENNReal` `ENNReal.measurableSpace` `EDist.edist` `PseudoEMetricSpace.toEDist` `MeasurableSet` `Filter.Eventually` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `Real` `Real.instLT` `Real.instZero`	`Set` `Set.instHasSubset` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `ENNReal.ofReal` `TendstoUniformlyOn` `PseudoEMetricSpace.toUniformSpace` `Filter.atTop` `SemilatticeSup.toPartialOrder` `Set.instSDiff`	—	`Measure.instOuterMeasureClass` `Egorov.iUnionNotConvergentSeq_subset` `Egorov.iUnionNotConvergentSeq_measurableSet` `Egorov.measure_iUnionNotConvergentSeq` `Egorov.tendstoUniformlyOn_diff_iUnionNotConvergentSeq`
`tendstoUniformlyOn_of_ae_tendsto_of_measurable_edist'` 📖	mathematical	`Measurable` `ENNReal` `ENNReal.measurableSpace` `EDist.edist` `PseudoEMetricSpace.toEDist` `Filter.Eventually` `Filter.Tendsto` `Filter.atTop` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `Real` `Real.instLT` `Real.instZero`	`MeasurableSet` `Preorder.toLE` `ENNReal.instPartialOrder` `DFunLike.coe` `Set` `ENNReal.ofReal` `TendstoUniformlyOn` `Compl.compl` `Set.instCompl`	—	`Measure.instOuterMeasureClass` `tendstoUniformlyOn_of_ae_tendsto_of_measurable_edist` `MeasurableSet.univ` `measure_ne_top` `Filter.mp_mem` `Filter.univ_mem'` `Set.compl_eq_univ_diff`

MeasureTheory.Egorov

Definitions

Name	Category	Theorems
`iUnionNotConvergentSeq` 📖	CompOp	4 math math: `tendstoUniformlyOn_diff_iUnionNotConvergentSeq`, `iUnionNotConvergentSeq_subset`, `iUnionNotConvergentSeq_measurableSet`, `measure_iUnionNotConvergentSeq`
`notConvergentSeq` 📖	CompOp	7 math math: `measure_inter_notConvergentSeq_eq_zero`, `notConvergentSeqLTIndex_spec`, `notConvergentSeq_antitone`, `notConvergentSeq_measurableSet`, `mem_notConvergentSeq_iff`, `measure_notConvergentSeq_tendsto_zero`, `exists_notConvergentSeq_lt`
`notConvergentSeqLTIndex` 📖	CompOp	1 math math: `notConvergentSeqLTIndex_spec`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_notConvergentSeq_lt` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Measurable` `ENNReal` `ENNReal.measurableSpace` `EDist.edist` `PseudoEMetricSpace.toEDist` `MeasurableSet` `Filter.Eventually` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	`Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `Set` `Set.instInter` `notConvergentSeq` `SemilatticeSup.toPartialOrder` `ENNReal.ofReal` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid` `Real.instInv` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`MeasureTheory.Measure.instOuterMeasureClass` `Nat.instAtLeastTwoHAddOfNat` `ENNReal.tendsto_atTop` `ENNReal.zero_ne_top` `measure_notConvergentSeq_tendsto_zero` `ENNReal.ofReal_pos` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `pow_pos` `IsStrictOrderedRing.toZeroLEOneClass` `inv_pos_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `zero_add` `le_rfl`
`iUnionNotConvergentSeq_measurableSet` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Measurable` `ENNReal` `ENNReal.measurableSpace` `EDist.edist` `PseudoEMetricSpace.toEDist` `MeasurableSet` `Filter.Eventually` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	`iUnionNotConvergentSeq`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasurableSet.iUnion` `instCountableNat` `MeasurableSet.inter` `notConvergentSeq_measurableSet`
`iUnionNotConvergentSeq_subset` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Measurable` `ENNReal` `ENNReal.measurableSpace` `EDist.edist` `PseudoEMetricSpace.toEDist` `MeasurableSet` `Filter.Eventually` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	`Set` `Set.instHasSubset` `iUnionNotConvergentSeq`	—	`MeasureTheory.Measure.instOuterMeasureClass` `iUnionNotConvergentSeq.eq_1` `Set.inter_iUnion` `Set.inter_subset_left`
`measure_iUnionNotConvergentSeq` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Measurable` `ENNReal` `ENNReal.measurableSpace` `EDist.edist` `PseudoEMetricSpace.toEDist` `MeasurableSet` `Filter.Eventually` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	`Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `Set` `iUnionNotConvergentSeq` `ENNReal.ofReal`	—	`MeasureTheory.Measure.instOuterMeasureClass` `le_trans` `MeasureTheory.measure_iUnion_le` `instCountableNat` `Nat.instAtLeastTwoHAddOfNat` `ENNReal.tsum_le_tsum` `notConvergentSeqLTIndex_spec` `half_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `ENNReal.ofReal_mul` `LT.lt.le` `ENNReal.tsum_mul_left` `ENNReal.ofReal_tsum_of_nonneg` `le_of_lt` `pow_pos` `IsStrictOrderedRing.toZeroLEOneClass` `inv_pos_of_pos` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `inv_eq_one_div` `summable_geometric_two` `tsum_geometric_two` `div_mul_cancel₀` `two_ne_zero` `ZeroLEOneClass.neZero.two` `Real.instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `le_refl`
`measure_inter_notConvergentSeq_eq_zero` 📖	mathematical	`Filter.Eventually` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	`DFunLike.coe` `Set` `ENNReal` `Set.instInter` `Set.iInter` `notConvergentSeq` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `instZeroENNReal`	—	`MeasureTheory.Measure.instOuterMeasureClass` `nonpos_iff_eq_zero` `ENNReal.instCanonicallyOrderedAdd` `MeasureTheory.measure_mono` `Mathlib.Tactic.Push.not_forall_eq` `LT.lt.le`
`measure_notConvergentSeq_tendsto_zero` 📖	mathematical	`Measurable` `ENNReal` `ENNReal.measurableSpace` `EDist.edist` `PseudoEMetricSpace.toEDist` `MeasurableSet` `Filter.Eventually` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	`Filter.Tendsto` `DFunLike.coe` `Set` `Set.instInter` `notConvergentSeq` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Filter.atTop` `nhds` `ENNReal.instTopologicalSpace` `instZeroENNReal`	—	`MeasureTheory.Measure.instOuterMeasureClass` `isEmpty_or_nonempty` `Unique.instSubsingleton` `tendsto_const_nhds` `measure_inter_notConvergentSeq_eq_zero` `Set.inter_iInter` `MeasureTheory.tendsto_measure_iInter_atTop` `Filter.atTop.isCountablyGenerated` `MeasurableSet.nullMeasurableSet` `MeasurableSet.inter` `notConvergentSeq_measurableSet` `Set.inter_subset_inter_right` `notConvergentSeq_antitone` `ne_top_of_le_ne_top` `MeasureTheory.measure_mono` `Set.inter_subset_left`
`mem_notConvergentSeq_iff` 📖	mathematical	—	`Set` `Set.instMembership` `notConvergentSeq` `Preorder.toLE` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ENNReal.instInv` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `EDist.edist` `PseudoEMetricSpace.toEDist`	—	—
`notConvergentSeqLTIndex_spec` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Measurable` `ENNReal` `ENNReal.measurableSpace` `EDist.edist` `PseudoEMetricSpace.toEDist` `MeasurableSet` `Filter.Eventually` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	`Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `Set` `Set.instInter` `notConvergentSeq` `SemilatticeSup.toPartialOrder` `notConvergentSeqLTIndex` `ENNReal.ofReal` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid` `Real.instInv` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`MeasureTheory.Measure.instOuterMeasureClass` `Nat.instAtLeastTwoHAddOfNat` `exists_notConvergentSeq_lt`
`notConvergentSeq_antitone` 📖	mathematical	—	`Antitone` `Set` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `notConvergentSeq`	—	`Set.iUnion₂_mono'` `le_trans` `Set.Subset.rfl`
`notConvergentSeq_measurableSet` 📖	mathematical	`Measurable` `ENNReal` `ENNReal.measurableSpace` `EDist.edist` `PseudoEMetricSpace.toEDist`	`MeasurableSet` `notConvergentSeq`	—	`MeasurableSet.iUnion` `Prop.countable` `measurableSet_lt` `BorelSpace.opensMeasurable` `ENNReal.borelSpace` `ENNReal.instSecondCountableTopology` `OrderTopology.to_orderClosedTopology` `ENNReal.instOrderTopology` `measurable_const`
`tendstoUniformlyOn_diff_iUnionNotConvergentSeq` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Measurable` `ENNReal` `ENNReal.measurableSpace` `EDist.edist` `PseudoEMetricSpace.toEDist` `MeasurableSet` `Filter.Eventually` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	`TendstoUniformlyOn` `PseudoEMetricSpace.toUniformSpace` `Filter.atTop` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Set` `Set.instSDiff` `iUnionNotConvergentSeq`	—	`MeasureTheory.Measure.instOuterMeasureClass` `EMetric.tendstoUniformlyOn_iff` `ENNReal.exists_inv_nat_lt` `LT.lt.ne'` `Filter.eventually_atTop` `SemilatticeSup.instIsDirectedOrder` `Nat.instAtLeastTwoHAddOfNat` `half_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `PseudoEMetricSpace.edist_comm` `lt_of_le_of_lt` `Mathlib.Tactic.Push.not_and_eq` `mem_notConvergentSeq_iff`

---

← Back to Index