Documentation Verification Report

UnifTight

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

Statistics

Metric	Count
Definitions `UnifTight`	1
Theorems `add`, `aeeq`, `eventually_cofinite_indicator`, `exists_measurableSet_indicator`, `neg`, `sub`, `tendstoInMeasure_iff_tendsto_Lp`, `tendsto_Lp_of_tendstoInMeasure`, `tendsto_Lp_of_tendsto_ae`, `unifTight_congr_ae`, `unifTight_const`, `unifTight_finite`, `unifTight_iff_ennreal`, `unifTight_iff_real`, `unifTight_of_subsingleton`	15
Total	16

MeasureTheory

Definitions

Name	Category	Theorems
`UnifTight` 📖	MathDef	7 math math: `unifTight_iff_real`, `unifTight_congr_ae`, `tendstoInMeasure_iff_tendsto_Lp`, `unifTight_const`, `unifTight_iff_ennreal`, `unifTight_finite`, `unifTight_of_subsingleton`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tendstoInMeasure_iff_tendsto_Lp` 📖	mathematical	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `MemLp` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toPseudoMetricSpace`	`TendstoInMeasure` `PseudoEMetricSpace.toEDist` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `Filter.atTop` `Nat.instPreorder` `UnifIntegrable` `UnifTight` `Filter.Tendsto` `eLpNorm` `Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `nhds` `ENNReal.instTopologicalSpace` `instZeroENNReal`	—	`tendsto_Lp_of_tendstoInMeasure` `tendstoInMeasure_of_tendsto_eLpNorm` `LT.lt.ne'` `lt_of_lt_of_le` `zero_lt_one` `IsOrderedRing.toZeroLEOneClass` `ENNReal.instIsOrderedRing` `NeZero.charZero_one` `ENNReal.instCharZero` `MemLp.aestronglyMeasurable` `unifIntegrable_of_tendsto_Lp`
`tendsto_Lp_of_tendstoInMeasure` 📖	mathematical	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `AEStronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `MemLp` `ContinuousENorm.toENorm` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `SeminormedAddGroup.toContinuousENorm` `UnifIntegrable` `UnifTight` `TendstoInMeasure` `PseudoEMetricSpace.toEDist` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `Filter.atTop` `Nat.instPreorder`	`Filter.Tendsto` `eLpNorm` `Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `nhds` `ENNReal.instTopologicalSpace` `instZeroENNReal`	—	`Filter.tendsto_of_subseq_tendsto` `instIsCountablyGenerated_atTop` `OrderTopology.of_linearLocallyFinite` `instDiscreteTopologyNat` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace` `Countable.LindelofSpace` `instCountableNat` `PseudoEMetricSpace.pseudoMetrizableSpace` `Measure.instOuterMeasureClass` `TendstoInMeasure.exists_seq_tendsto_ae` `Filter.Tendsto.comp` `tendsto_Lp_of_tendsto_ae`
`tendsto_Lp_of_tendsto_ae` 📖	mathematical	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `AEStronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `MemLp` `ContinuousENorm.toENorm` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `SeminormedAddGroup.toContinuousENorm` `UnifIntegrable` `UnifTight` `Filter.Eventually` `Filter.Tendsto` `Filter.atTop` `Nat.instPreorder` `nhds` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass`	`eLpNorm` `Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `ENNReal.instTopologicalSpace` `instZeroENNReal`	—	`Measure.instOuterMeasureClass` `UnifIntegrable.ae_eq` `UnifTight.aeeq` `MemLp.aestronglyMeasurable` `MemLp.ae_eq` `Filter.EventuallyEq.sub` `eLpNorm_congr_ae` `Filter.Tendsto.congr`
`unifTight_congr_ae` 📖	mathematical	`Filter.EventuallyEq` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass`	`UnifTight`	—	`Measure.instOuterMeasureClass` `UnifTight.aeeq` `Filter.EventuallyEq.symm`
`unifTight_const` 📖	mathematical	`MemLp` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toPseudoMetricSpace`	`UnifTight`	—	`measure_empty` `Measure.instOuterMeasureClass` `le_top` `MemLp.exists_eLpNorm_indicator_compl_lt` `ENNReal.coe_ne_zero` `LT.lt.ne'` `ne_of_lt` `LT.lt.le`
`unifTight_finite` 📖	mathematical	`MemLp` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toPseudoMetricSpace`	`UnifTight`	—	`Finite.exists_equiv_fin` `Equiv.symm_apply_apply`
`unifTight_iff_ennreal` 📖	mathematical	—	`UnifTight` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `eLpNorm` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `Set.indicator` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Compl.compl` `Set` `Set.instCompl`	—	`measure_empty` `Measure.instOuterMeasureClass` `ENNReal.zero_ne_top`
`unifTight_iff_real` 📖	mathematical	—	`UnifTight` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `eLpNorm` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `Set.indicator` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Compl.compl` `Set` `Set.instCompl` `ENNReal.ofReal`	—	`Real.toNNReal_pos` `LE.le.trans_eq` `ENNReal.ofReal_coe_nnreal`
`unifTight_of_subsingleton` 📖	mathematical	`MemLp` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toPseudoMetricSpace`	`UnifTight`	—	`measure_empty` `Measure.instOuterMeasureClass` `le_top` `MemLp.exists_eLpNorm_indicator_compl_lt` `ENNReal.coe_ne_zero` `LT.lt.ne'` `ne_of_lt` `Lean.Meta.FastSubsingleton.elim` `LT.lt.le`

MeasureTheory.UnifTight

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`MeasureTheory.UnifTight` `MeasureTheory.AEStronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`MeasureTheory.exists_Lp_half` `ENNReal.coe_ne_zero` `LT.lt.ne'` `MeasureTheory.measure_empty` `MeasureTheory.Measure.instOuterMeasureClass` `Set.compl_empty` `Set.indicator_univ` `LT.lt.le` `le_top` `Filter.Eventually.exists_measurable_mem_of_smallSets` `MeasureTheory.Measure.cofinite.instIsMeasurablyGenerated` `Filter.Eventually.and` `eventually_cofinite_indicator` `ne_of_lt` `ENNReal.coe_toNNReal` `compl_compl` `Set.indicator_add'` `le_of_lt` `MeasureTheory.AEStronglyMeasurable.indicator`
`aeeq` 📖	—	`MeasureTheory.UnifTight` `Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	—	`MeasureTheory.Measure.instOuterMeasureClass` `LE.le.trans` `le_of_eq` `MeasureTheory.eLpNorm_congr_ae` `Filter.mp_mem` `Filter.univ_mem'`
`eventually_cofinite_indicator` 📖	mathematical	`MeasureTheory.UnifTight`	`Filter.Eventually` `Set` `Filter.smallSets` `MeasureTheory.Measure.cofinite`	—	`pos_iff_ne_zero` `NNReal.instCanonicallyOrderedAdd` `ENNReal.toNNReal_ne_zero` `Filter.eventually_smallSets'` `LE.le.trans` `MeasureTheory.eLpNorm_mono` `norm_indicator_le_of_subset` `MeasureTheory.Measure.compl_mem_cofinite` `lt_top_iff_ne_top` `ENNReal.coe_toNNReal`
`exists_measurableSet_indicator` 📖	mathematical	`MeasureTheory.UnifTight`	`MeasurableSet` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `Top.top` `instTopENNReal` `Preorder.toLE` `MeasureTheory.eLpNorm` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `Set.indicator` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Compl.compl` `Set.instCompl`	—	`Filter.Eventually.exists_measurable_mem_of_smallSets` `MeasureTheory.Measure.cofinite.instIsMeasurablyGenerated` `eventually_cofinite_indicator` `MeasurableSet.compl` `compl_compl`
`neg` 📖	mathematical	`MeasureTheory.UnifTight`	`Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`Set.indicator_neg'` `MeasureTheory.eLpNorm_neg`
`sub` 📖	mathematical	`MeasureTheory.UnifTight` `MeasureTheory.AEStronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`sub_eq_add_neg` `add` `neg` `MeasureTheory.AEStronglyMeasurable.neg` `IsTopologicalAddGroup.toContinuousNeg` `SeminormedAddCommGroup.toIsTopologicalAddGroup`

---

← Back to Index