Documentation Verification Report

JordanSub

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

Statistics

Metric	Count
Definitions `jordanDecompositionOfToSignedMeasureSub`	1
Theorems `jordanDecompositionOfToSignedMeasureSub_negPart`, `jordanDecompositionOfToSignedMeasureSub_posPart`, `jordanDecompositionOfToSignedMeasureSub_toSignedMeasure`, `mutually_singular_measure_sub`, `sub_apply_eq_zero_of_isHahnDecomposition`, `sub_toSignedMeasure_eq_toSignedMeasure_sub`, `toJordanDecomposition_toSignedMeasure_sub`, `toSignedMeasure_restrict_sub`	8
Total	9

MeasureTheory.Measure

Definitions

Name	Category	Theorems
`jordanDecompositionOfToSignedMeasureSub` 📖	CompOp	4 math math: `jordanDecompositionOfToSignedMeasureSub_posPart`, `toJordanDecomposition_toSignedMeasure_sub`, `jordanDecompositionOfToSignedMeasureSub_toSignedMeasure`, `jordanDecompositionOfToSignedMeasureSub_negPart`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`jordanDecompositionOfToSignedMeasureSub_negPart` 📖	mathematical	—	`MeasureTheory.JordanDecomposition.negPart` `jordanDecompositionOfToSignedMeasureSub` `MeasureTheory.Measure` `instSub`	—	—
`jordanDecompositionOfToSignedMeasureSub_posPart` 📖	mathematical	—	`MeasureTheory.JordanDecomposition.posPart` `jordanDecompositionOfToSignedMeasureSub` `MeasureTheory.Measure` `instSub`	—	—
`jordanDecompositionOfToSignedMeasureSub_toSignedMeasure` 📖	mathematical	—	`MeasureTheory.JordanDecomposition.toSignedMeasure` `jordanDecompositionOfToSignedMeasureSub` `MeasureTheory.SignedMeasure` `MeasureTheory.VectorMeasure.instSub` `Real` `Real.instAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `instIsTopologicalAddGroupReal` `toSignedMeasure`	—	`instIsTopologicalAddGroupReal` `MeasureTheory.JordanDecomposition.posPart_finite` `MeasureTheory.JordanDecomposition.negPart_finite`
`mutually_singular_measure_sub` 📖	mathematical	—	`MutuallySingular` `MeasureTheory.Measure` `instSub`	—	`MeasureTheory.exists_isHahnDecomposition` `MeasureTheory.IsHahnDecomposition.measurableSet` `sub_apply_eq_zero_of_isHahnDecomposition` `MeasureTheory.IsHahnDecomposition.compl`
`sub_apply_eq_zero_of_isHahnDecomposition` 📖	mathematical	`MeasureTheory.IsHahnDecomposition`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `instFunLike` `instSub` `instZeroENNReal`	—	`restrict_eq_zero` `restrict_sub_eq_restrict_sub_restrict` `MeasureTheory.IsHahnDecomposition.measurableSet` `sub_eq_zero_of_le` `MeasureTheory.IsHahnDecomposition.le_on`
`sub_toSignedMeasure_eq_toSignedMeasure_sub` 📖	mathematical	—	`MeasureTheory.SignedMeasure` `MeasureTheory.VectorMeasure.instSub` `Real` `Real.instAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `instIsTopologicalAddGroupReal` `toSignedMeasure` `MeasureTheory.Measure` `instSub` `isFiniteMeasure_sub`	—	`instIsTopologicalAddGroupReal` `isFiniteMeasure_sub` `MeasureTheory.exists_isHahnDecomposition` `MeasureTheory.IsHahnDecomposition.compl` `MeasureTheory.isFiniteMeasureRestrict` `toSignedMeasure_restrict_sub` `MeasureTheory.isFiniteMeasureZero` `toSignedMeasure_congr` `restrict_eq_zero` `sub_apply_eq_zero_of_isHahnDecomposition` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `MeasureTheory.VectorMeasure.restrict_add_restrict_compl` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `MeasureTheory.IsHahnDecomposition.measurableSet` `toSignedMeasure_zero` `zero_add` `toSignedMeasure_restrict_eq_restrict_toSignedMeasure` `MeasurableSet.compl` `sub_eq_add_neg` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.term_add_constg` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Tactic.Abel.const_add_termg` `add_zero` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_neg` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_ofNat`
`toJordanDecomposition_toSignedMeasure_sub` 📖	mathematical	—	`MeasureTheory.SignedMeasure.toJordanDecomposition` `MeasureTheory.SignedMeasure` `MeasureTheory.VectorMeasure.instSub` `Real` `Real.instAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `instIsTopologicalAddGroupReal` `toSignedMeasure` `jordanDecompositionOfToSignedMeasureSub`	—	`MeasureTheory.JordanDecomposition.toSignedMeasure_injective` `instIsTopologicalAddGroupReal` `MeasureTheory.SignedMeasure.toSignedMeasure_toJordanDecomposition` `jordanDecompositionOfToSignedMeasureSub_toSignedMeasure`
`toSignedMeasure_restrict_sub` 📖	mathematical	`MeasureTheory.IsHahnDecomposition`	`toSignedMeasure` `restrict` `MeasureTheory.Measure` `instSub` `MeasureTheory.isFiniteMeasureRestrict` `isFiniteMeasure_sub` `MeasureTheory.VectorMeasure` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `MeasureTheory.VectorMeasure.instSub` `Real.instAddCommGroup` `instIsTopologicalAddGroupReal` `MeasureTheory.VectorMeasure.restrict`	—	`MeasureTheory.IsHahnDecomposition.measurableSet` `MeasureTheory.isFiniteMeasureRestrict` `isFiniteMeasure_sub` `instIsTopologicalAddGroupReal` `eq_sub_iff_add_eq` `toSignedMeasure_restrict_eq_restrict_toSignedMeasure` `MeasureTheory.isFiniteMeasureAdd` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `toSignedMeasure_add` `restrict_sub_eq_restrict_sub_restrict` `sub_add_cancel_of_le` `MeasureTheory.IsHahnDecomposition.le_on` `toSignedMeasure.congr_simp`

---

← Back to Index