Documentation Verification Report

Hahn

📁 Source: Mathlib/MeasureTheory/VectorMeasure/Decomposition/Hahn.lean

Statistics

Metric	Count
Definitions `measureOfNegatives`	1
Theorems `bddBelow_measureOfNegatives`, `exists_compl_positive_negative`, `exists_isCompl_positive_negative`, `exists_subset_restrict_nonpos`, `of_symmDiff_compl_positive_negative`, `zero_mem_measureOfNegatives`	6
Total	7

MeasureTheory.SignedMeasure

Definitions

Name	Category	Theorems
`measureOfNegatives` 📖	CompOp	2 math math: `bddBelow_measureOfNegatives`, `zero_mem_measureOfNegatives`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bddBelow_measureOfNegatives` 📖	mathematical	—	`BddBelow` `Real` `Real.instLE` `measureOfNegatives`	—	`Mathlib.Tactic.Push.not_forall_eq` `le_trans` `Set.diff_union_of_subset` `Set.subset_iUnion` `MeasureTheory.VectorMeasure.of_union` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `Set.disjoint_sdiff_left` `MeasurableSet.diff` `MeasurableSet.iUnion` `instCountableNat` `add_le_of_nonpos_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `MeasureTheory.VectorMeasure.restrict_le_restrict_iUnion` `OrderTopology.to_orderClosedTopology` `instOrderTopologyReal` `MeasureTheory.VectorMeasure.nonpos_of_restrict_le_zero` `MeasureTheory.VectorMeasure.restrict_le_zero_subset` `Set.diff_subset` `le_of_lt` `exists_nat_gt` `Real.instIsStrictOrderedRing` `Real.instArchimedean` `lt_irrefl` `LT.lt.trans_le` `neg_lt` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Real.instIsOrderedCancelAddMonoid` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `contravariant_lt_of_covariant_le`
`exists_compl_positive_negative` 📖	mathematical	—	`Set` `MeasurableSet` `MeasureTheory.VectorMeasure` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Preorder.toLE` `PartialOrder.toPreorder` `MeasureTheory.VectorMeasure.instPartialOrder` `Real.partialOrder` `MeasureTheory.VectorMeasure.restrict` `MeasureTheory.VectorMeasure.instZero` `Compl.compl` `Set.instCompl`	—	`exists_seq_tendsto_sInf` `instOrderTopologyReal` `TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology` `PseudoEMetricSpace.pseudoMetrizableSpace` `zero_mem_measureOfNegatives` `bddBelow_measureOfNegatives` `MeasurableSet.iUnion` `instCountableNat` `MeasureTheory.VectorMeasure.restrict_le_restrict_iUnion` `Real.instIsOrderedAddMonoid` `OrderTopology.to_orderClosedTopology` `le_antisymm` `le_of_tendsto_of_tendsto` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `tendsto_const_nhds` `Filter.Eventually.of_forall` `Set.diff_union_of_subset` `Set.subset_iUnion` `MeasureTheory.VectorMeasure.of_union` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `Set.disjoint_sdiff_left` `MeasurableSet.diff` `add_le_of_nonpos_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `MeasureTheory.VectorMeasure.nonpos_of_restrict_le_zero` `MeasureTheory.VectorMeasure.restrict_le_zero_subset` `Set.diff_subset` `csInf_le` `MeasurableSet.compl` `MeasureTheory.VectorMeasure.restrict_le_restrict_iff` `exists_subset_restrict_nonpos` `Set.disjoint_of_subset_right` `Set.Subset.trans` `disjoint_compl_right` `lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Real.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `not_le` `MeasurableSet.union` `MeasureTheory.VectorMeasure.restrict_le_restrict_union` `compl_compl`
`exists_isCompl_positive_negative` 📖	mathematical	—	`Set` `MeasurableSet` `MeasureTheory.VectorMeasure` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Preorder.toLE` `PartialOrder.toPreorder` `MeasureTheory.VectorMeasure.instPartialOrder` `Real.partialOrder` `MeasureTheory.VectorMeasure.restrict` `MeasureTheory.VectorMeasure.instZero` `IsCompl` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `Set.instBoundedOrder`	—	`exists_compl_positive_negative` `MeasurableSet.compl` `isCompl_compl`
`exists_subset_restrict_nonpos` 📖	mathematical	`Real` `Real.instLT` `MeasureTheory.VectorMeasure.measureOf'` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instZero`	`Set` `MeasurableSet` `Set.instHasSubset` `MeasureTheory.VectorMeasure` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Preorder.toLE` `PartialOrder.toPreorder` `MeasureTheory.VectorMeasure.instPartialOrder` `Real.partialOrder` `MeasureTheory.VectorMeasure.restrict` `MeasureTheory.VectorMeasure.instZero` `Real.instLT` `MeasureTheory.VectorMeasure.measureOf'` `Real.instZero`	—	`by_contradiction` `ne_of_lt` `MeasureTheory.VectorMeasure.not_measurable` `Set.Subset.refl` `Set.ext` `MeasureTheory.VectorMeasure.of_disjoint_iUnion` `instCountableNat` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `add_comm` `MeasureTheory.VectorMeasure.of_add_of_diff` `MeasurableSet.iUnion` `Set.iUnion_subset` `le_add_of_nonneg_right` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `tsum_nonneg` `OrderTopology.to_orderClosedTopology` `instOrderTopologyReal` `le_of_lt` `HasSum.summable` `MeasureTheory.VectorMeasure.m_iUnion` `Summable.of_nonneg_of_le` `Nat.one_div_pos_of_nat` `Real.instIsStrictOrderedRing` `Summable.comp_injective` `instIsUniformAddGroupReal` `Real.instCompleteSpace` `Nat.succ_injective` `Summable.tendsto_atTop_of_pos` `one_div` `Nat.cast_add_one_pos` `Real.instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `add_neg_cancel_right` `Filter.tendsto_atTop_add_const_right` `MeasurableSet.diff` `Set.diff_subset` `Mathlib.Tactic.Push.not_forall_eq` `MeasureTheory.VectorMeasure.restrict_le_restrict_iff` `Filter.tendsto_atTop_atTop` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `le_of_max_le_right` `le_rfl` `Nat.cast_one` `lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Tactic.Ring.inv_mul` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `neg_neg_of_pos` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Tactic.Linarith.without_one_mul` `Mathlib.Tactic.CancelDenoms.sub_subst` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Real.instIsOrderedRing` `Mathlib.Tactic.CancelDenoms.add_subst` `le_of_max_le_left` `inv_lt_of_inv_lt₀` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Set.diff_subset_diff_right` `Set.iUnion₂_subset_iUnion` `Set.Subset.trans` `tsub_add_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `LE.le.trans_lt`
`of_symmDiff_compl_positive_negative` 📖	mathematical	`MeasurableSet` `MeasureTheory.VectorMeasure` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Preorder.toLE` `PartialOrder.toPreorder` `MeasureTheory.VectorMeasure.instPartialOrder` `Real.partialOrder` `MeasureTheory.VectorMeasure.restrict` `MeasureTheory.VectorMeasure.instZero` `Compl.compl` `Set` `Set.instCompl`	`MeasureTheory.VectorMeasure.measureOf'` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `symmDiff` `Set` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `Set.instSDiff` `Real.instZero` `Compl.compl` `Set.instCompl`	—	`Set.symmDiff_def` `Set.diff_eq_compl_inter` `MeasureTheory.VectorMeasure.of_union` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `Set.disjoint_of_subset_left` `Set.inter_subset_left` `Set.disjoint_of_subset_right` `Set.inter_subset_right` `disjoint_comm` `IsCompl.disjoint` `isCompl_compl` `MeasurableSet.inter` `MeasurableSet.compl` `le_antisymm` `MeasureTheory.VectorMeasure.restrict_le_restrict_iff` `MeasureTheory.VectorMeasure.zero_apply` `zero_add` `compl_compl`
`zero_mem_measureOfNegatives` 📖	mathematical	—	`Real` `Set` `Set.instMembership` `measureOfNegatives` `Real.instZero`	—	`MeasurableSet.empty` `MeasureTheory.VectorMeasure.le_restrict_empty` `MeasureTheory.VectorMeasure.empty`

---

← Back to Index