Documentation Verification Report

PreVariation

📁 Source: Mathlib/MeasureTheory/Measure/PreVariation.lean

Statistics

Metric	Count
Definitions `IsSigmaSubadditiveSetFun`, `ennrealPreVariation`, `preVariation`, `preVariationFun`	4
Theorems `sup_measurableSetSubtype_eq_biUnion`, `empty`, `exists_Finpartition_sum_ge`, `exists_Finpartition_sum_gt`, `iUnion`, `mono`, `sum_le`, `sum_le_preVariationFun_iUnion`, `sum_le_preVariationFun_iUnion'`, `sum_le_preVariationFun_of_subset`	10
Total	14

MeasureTheory

Definitions

Name	Category	Theorems
`IsSigmaSubadditiveSetFun` 📖	MathDef	1 math math: `VectorMeasure.isSigmaSubadditiveSetFun_enorm`
`ennrealPreVariation` 📖	CompOp	—
`preVariation` 📖	CompOp	—
`preVariationFun` 📖	CompOp	8 math math: `preVariation.iUnion`, `preVariation.sum_le`, `preVariation.sum_le_preVariationFun_iUnion'`, `preVariation.empty`, `preVariation.exists_Finpartition_sum_ge`, `preVariation.sum_le_preVariationFun_iUnion`, `preVariation.sum_le_preVariationFun_of_subset`, `preVariation.mono`

MeasureTheory.preVariation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`empty` 📖	mathematical	—	`MeasureTheory.preVariationFun` `Set` `Set.instEmptyCollection` `ENNReal` `instZeroENNReal`	—	`ciSup_unique`
`exists_Finpartition_sum_ge` 📖	mathematical	`MeasurableSet` `NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal`	`ENNReal` `Preorder.toLE` `ENNReal.instPartialOrder` `MeasureTheory.preVariationFun` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `Finset.sum` `Set` `ENNReal.instAddCommMonoid` `Finpartition.parts` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `MeasurableSet.Subtype.instBooleanAlgebra` `HeytingAlgebra.toOrderBot` `BiheytingAlgebra.toHeytingAlgebra` `ENNReal.ofNNReal`	—	`ENNReal.coe_toNNReal` `ne_or_eq` `ENNReal.toNNReal_pos` `ENNReal.sub_lt_self` `ne_of_gt` `ENNReal.coe_pos` `exists_Finpartition_sum_gt` `tsub_add_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `ENNReal.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `ENNReal.instOrderedSub` `ENNReal.add_le_add_iff_right` `ENNReal.coe_ne_top` `le_of_lt` `add_le_add_right` `ENNReal.coe_le_coe_of_le` `Finpartition.instNonempty`
`exists_Finpartition_sum_gt` 📖	mathematical	`MeasurableSet` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `MeasureTheory.preVariationFun`	`Finset.sum` `Set` `ENNReal.instAddCommMonoid` `Finpartition.parts` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `MeasurableSet.Subtype.instBooleanAlgebra` `HeytingAlgebra.toOrderBot` `BiheytingAlgebra.toHeytingAlgebra`	—	—
`iUnion` 📖	mathematical	`MeasureTheory.IsSigmaSubadditiveSetFun` `Set` `Set.instEmptyCollection` `ENNReal` `instZeroENNReal` `MeasurableSet` `Pairwise` `Function.onFun` `Disjoint` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	`HasSum` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `MeasureTheory.preVariationFun` `Set.iUnion` `SummationFilter.unconditional`	—	`Summable.hasSum_iff` `ENNReal.instT2Space` `SummationFilter.instNeBotUnconditional` `ENNReal.summable` `le_antisymm` `sum_le_preVariationFun_iUnion` `ENNReal.le_tsum_of_forall_lt_exists_sum` `MeasurableSet.iUnion` `instCountableNat` `Set.subset_iUnion` `Finset.sum_le_sum` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `Set.inter_iUnion` `Set.inter_eq_left` `Finpartition.le` `MeasurableSet.inter` `Disjoint.mono` `Set.inter_subset_right` `Summable.tsum_finsetSum` `ENNReal.instContinuousAdd` `Finpartition.sum_restrict` `lt_iSup_iff` `lt_of_lt_of_le` `ENNReal.tsum_eq_iSup_nat` `sum_le`
`mono` 📖	mathematical	`MeasurableSet` `Set` `Set.instHasSubset`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `MeasureTheory.preVariationFun`	—	`sum_le_preVariationFun_of_subset` `ENNReal.instCanonicallyOrderedAdd`
`sum_le` 📖	mathematical	`MeasurableSet`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Finset.sum` `Set` `ENNReal.instAddCommMonoid` `Finpartition.parts` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `MeasurableSet.Subtype.instBooleanAlgebra` `HeytingAlgebra.toOrderBot` `BiheytingAlgebra.toHeytingAlgebra` `MeasureTheory.preVariationFun`	—	—
`sum_le_preVariationFun_iUnion` 📖	mathematical	`MeasurableSet` `Pairwise` `Function.onFun` `Set` `Disjoint` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `tsum` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `MeasureTheory.preVariationFun` `SummationFilter.unconditional` `Set.iUnion`	—	`ENNReal.tsum_le_of_sum_range_le` `Finset.sum_congr` `ENNReal.instCanonicallyOrderedAdd` `ENNReal.le_of_forall_pos_le_add` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `Nat.cast_pos'` `NNReal.addLeftMono` `LinearOrderedCommMonoidWithZero.toZeroLeOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `NNReal.instIsStrictOrderedRing` `lt_of_le_of_ne'` `zero_le` `Nat.instCanonicallyOrderedAdd` `lt_top_iff_ne_top` `LE.le.trans_lt` `mono` `MeasurableSet.iUnion` `instCountableNat` `Set.subset_iUnion` `Finset.sum_le_sum` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `Finset.sum_add_distrib` `Finset.sum_const` `Finset.card_range` `nsmul_eq_mul` `mul_div_cancel₀` `ne_of_gt` `add_le_add_left` `covariant_swap_add_of_covariant_add` `sum_le_preVariationFun_iUnion'` `exists_Finpartition_sum_ge`
`sum_le_preVariationFun_iUnion'` 📖	mathematical	`MeasurableSet` `Pairwise` `Function.onFun` `Set` `Disjoint` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Finset.sum` `ENNReal.instAddCommMonoid` `Finset.range` `Finpartition.parts` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `MeasurableSet.Subtype.instBooleanAlgebra` `BiheytingAlgebra.toHeytingAlgebra` `MeasureTheory.preVariationFun` `Set.iUnion`	—	`Set.disjoint_iff_inter_eq_empty` `DistribLattice.instIsModularLattice` `Set.PairwiseDisjoint.supIndep` `MeasurableSet.iUnion` `instCountableNat` `Subtype.coe_le_coe` `Finset.sup_measurableSetSubtype_eq_biUnion` `Set.iUnion₂_subset` `Set.subset_iUnion` `Finpartition.sum_combine` `Finset.sum_le_sum_of_subset` `ENNReal.instCanonicallyOrderedAdd` `Finpartition.parts_subset_extendOfLE` `sum_le`
`sum_le_preVariationFun_of_subset` 📖	mathematical	`MeasurableSet` `Set` `Set.instHasSubset`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Finset.sum` `ENNReal.instAddCommMonoid` `Finpartition.parts` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `MeasurableSet.Subtype.instBooleanAlgebra` `HeytingAlgebra.toOrderBot` `BiheytingAlgebra.toHeytingAlgebra` `MeasureTheory.preVariationFun`	—	`sum_le` `MeasurableSet.diff` `HasSubset.Subset.antisymm` `Set.instAntisymmSubset` `Set.diff_eq_empty` `Set.inter_diff_self` `Set.union_diff_cancel` `DistribLattice.instIsModularLattice` `Finset.sum_le_sum_of_subset` `ENNReal.instCanonicallyOrderedAdd` `Finset.mem_insert_of_mem`

MeasureTheory.preVariation.Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sup_measurableSetSubtype_eq_biUnion` 📖	mathematical	—	`Set` `MeasurableSet` `Finset.sup` `Lattice.toSemilatticeSup` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `MeasurableSet.Subtype.instBooleanAlgebra` `HeytingAlgebra.toOrderBot` `BiheytingAlgebra.toHeytingAlgebra` `Set.iUnion` `Finset` `Finset.instMembership`	—	`Finset.induction_on` `Finset.sup_empty` `Set.iUnion_congr_Prop` `Set.iUnion_of_empty` `instIsEmptyFalse` `Set.iUnion_empty` `Finset.sup_insert` `Set.iUnion_iUnion_eq_or_left`

---

← Back to Index