Jordan

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

Statistics

Metric	Count
Definitions JordanDecomposition, instInhabited, instInvolutiveNeg, instSMul, instSMulReal, instZero, negPart, posPart, toSignedMeasure, toJordanDecomposition, toJordanDecompositionEquiv, totalVariation	12
Theorems coe_smul, exists_compl_positive_negative, ext, ext_iff, mutuallySingular, negPart_finite, neg_negPart, neg_posPart, posPart_finite, real_smul_def, real_smul_neg, real_smul_negPart_neg, real_smul_negPart_nonneg, real_smul_nonneg, real_smul_posPart_neg, real_smul_posPart_nonneg, smul_negPart, smul_posPart, toJordanDecomposition_toSignedMeasure, toSignedMeasure_injective, toSignedMeasure_neg, toSignedMeasure_smul, toSignedMeasure_zero, zero_negPart, zero_posPart, absolutelyContinuous_ennreal_iff, mutuallySingular_ennreal_iff, mutuallySingular_iff, null_of_totalVariation_zero, of_diff_eq_zero_of_symmDiff_eq_zero_negative, of_diff_eq_zero_of_symmDiff_eq_zero_positive, of_inter_eq_of_symmDiff_eq_zero_negative, of_inter_eq_of_symmDiff_eq_zero_positive, subset_negative_null_set, subset_positive_null_set, toJordanDecompositionEquiv_apply, toJordanDecompositionEquiv_symm_apply, toJordanDecomposition_eq, toJordanDecomposition_neg, toJordanDecomposition_smul, toJordanDecomposition_smul_real, toJordanDecomposition_spec, toJordanDecomposition_zero, toSignedMeasure_toJordanDecomposition, totalVariation_absolutelyContinuous_iff, totalVariation_mutuallySingular_iff, totalVariation_neg, totalVariation_zero	48
Total	60

MeasureTheory

Definitions

Name	Category	Theorems
JordanDecomposition 📖	CompData	24 math math: SignedMeasure.toJordanDecomposition_zero, JordanDecomposition.real_smul_nonneg, JordanDecomposition.real_smul_neg, SignedMeasure.toJordanDecomposition_smul_real, JordanDecomposition.zero_posPart, JordanDecomposition.toSignedMeasure_injective, JordanDecomposition.neg_negPart, SignedMeasure.toJordanDecomposition_neg, JordanDecomposition.zero_negPart, JordanDecomposition.smul_posPart, JordanDecomposition.real_smul_posPart_nonneg, JordanDecomposition.coe_smul, JordanDecomposition.smul_negPart, JordanDecomposition.toSignedMeasure_smul, JordanDecomposition.real_smul_posPart_neg, JordanDecomposition.toSignedMeasure_neg, JordanDecomposition.neg_posPart, JordanDecomposition.real_smul_negPart_neg, JordanDecomposition.toSignedMeasure_zero, JordanDecomposition.real_smul_negPart_nonneg, SignedMeasure.toJordanDecompositionEquiv_apply, JordanDecomposition.real_smul_def, SignedMeasure.toJordanDecomposition_smul, SignedMeasure.toJordanDecompositionEquiv_symm_apply

MeasureTheory.JordanDecomposition

Definitions

Name	Category	Theorems
instInhabited 📖	CompOp	—
instInvolutiveNeg 📖	CompOp	6 math math: real_smul_neg, neg_negPart, MeasureTheory.SignedMeasure.toJordanDecomposition_neg, toSignedMeasure_neg, neg_posPart, real_smul_def
instSMul 📖	CompOp	8 math math: real_smul_nonneg, real_smul_neg, smul_posPart, coe_smul, smul_negPart, toSignedMeasure_smul, real_smul_def, MeasureTheory.SignedMeasure.toJordanDecomposition_smul
instSMulReal 📖	CompOp	9 math math: real_smul_nonneg, real_smul_neg, MeasureTheory.SignedMeasure.toJordanDecomposition_smul_real, real_smul_posPart_nonneg, coe_smul, real_smul_posPart_neg, real_smul_negPart_neg, real_smul_negPart_nonneg, real_smul_def
instZero 📖	CompOp	4 math math: MeasureTheory.SignedMeasure.toJordanDecomposition_zero, zero_posPart, zero_negPart, toSignedMeasure_zero
negPart 📖	CompOp	22 math math: MeasureTheory.SignedMeasure.rnDeriv_def, MeasureTheory.SignedMeasure.HaveLebesgueDecomposition.negPart, MeasureTheory.SignedMeasure.totalVariation_mutuallySingular_iff, MeasureTheory.SignedMeasure.toJordanDecomposition_eq_of_eq_add_withDensity, MeasureTheory.SignedMeasure.singularPart_totalVariation, negPart_finite, MeasureTheory.SignedMeasure.singularPart_mutuallySingular, neg_negPart, exists_compl_positive_negative, MeasureTheory.SignedMeasure.not_haveLebesgueDecomposition_iff, MeasureTheory.Measure.jordanDecompositionOfToSignedMeasureSub_negPart, zero_negPart, MeasureTheory.SignedMeasure.jordanDecomposition_add_withDensity_mutuallySingular, smul_negPart, real_smul_posPart_neg, neg_posPart, real_smul_negPart_neg, real_smul_negPart_nonneg, ext_iff, MeasureTheory.SignedMeasure.totalVariation_absolutelyContinuous_iff, MeasureTheory.SignedMeasure.toJordanDecomposition_spec, mutuallySingular
posPart 📖	CompOp	22 math math: MeasureTheory.Measure.jordanDecompositionOfToSignedMeasureSub_posPart, MeasureTheory.SignedMeasure.rnDeriv_def, MeasureTheory.SignedMeasure.totalVariation_mutuallySingular_iff, MeasureTheory.SignedMeasure.toJordanDecomposition_eq_of_eq_add_withDensity, MeasureTheory.SignedMeasure.HaveLebesgueDecomposition.posPart, MeasureTheory.SignedMeasure.singularPart_totalVariation, MeasureTheory.SignedMeasure.singularPart_mutuallySingular, zero_posPart, posPart_finite, neg_negPart, exists_compl_positive_negative, MeasureTheory.SignedMeasure.not_haveLebesgueDecomposition_iff, smul_posPart, real_smul_posPart_nonneg, MeasureTheory.SignedMeasure.jordanDecomposition_add_withDensity_mutuallySingular, real_smul_posPart_neg, neg_posPart, real_smul_negPart_neg, ext_iff, MeasureTheory.SignedMeasure.totalVariation_absolutelyContinuous_iff, MeasureTheory.SignedMeasure.toJordanDecomposition_spec, mutuallySingular
toSignedMeasure 📖	CompOp	9 math math: MeasureTheory.Measure.jordanDecompositionOfToSignedMeasureSub_toSignedMeasure, MeasureTheory.SignedMeasure.toSignedMeasure_toJordanDecomposition, toSignedMeasure_injective, exists_compl_positive_negative, toSignedMeasure_smul, toSignedMeasure_neg, toJordanDecomposition_toSignedMeasure, toSignedMeasure_zero, MeasureTheory.SignedMeasure.toJordanDecompositionEquiv_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_smul 📖	mathematical	—	Real MeasureTheory.JordanDecomposition instSMulReal NNReal.toReal NNReal instSMul	—	real_smul_def NNReal.coe_nonneg Real.toNNReal_coe
exists_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 toSignedMeasure MeasureTheory.VectorMeasure.instZero Compl.compl Set Set.instCompl DFunLike.coe MeasureTheory.Measure ENNReal MeasureTheory.Measure.instFunLike posPart instZeroENNReal negPart	—	mutuallySingular MeasureTheory.VectorMeasure.restrict_le_restrict_of_subset_le instIsTopologicalAddGroupReal posPart_finite negPart_finite toSignedMeasure.eq_1 MeasureTheory.Measure.toSignedMeasure_sub_apply MeasureTheory.measureReal_def nonpos_iff_eq_zero ENNReal.instCanonicallyOrderedAdd MeasureTheory.measure_mono MeasureTheory.Measure.instOuterMeasureClass ENNReal.toReal_zero zero_sub neg_le IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add MeasureTheory.VectorMeasure.zero_apply neg_zero ENNReal.toReal_nonneg sub_zero
ext 📖	—	posPart negPart	—	—	—
ext_iff 📖	mathematical	—	posPart negPart	—	ext
mutuallySingular 📖	mathematical	—	MeasureTheory.Measure.MutuallySingular posPart negPart	—	—
negPart_finite 📖	mathematical	—	MeasureTheory.IsFiniteMeasure negPart	—	—
neg_negPart 📖	mathematical	—	negPart MeasureTheory.JordanDecomposition InvolutiveNeg.toNeg instInvolutiveNeg posPart	—	—
neg_posPart 📖	mathematical	—	posPart MeasureTheory.JordanDecomposition InvolutiveNeg.toNeg instInvolutiveNeg negPart	—	—
posPart_finite 📖	mathematical	—	MeasureTheory.IsFiniteMeasure posPart	—	—
real_smul_def 📖	mathematical	—	Real MeasureTheory.JordanDecomposition instSMulReal Real.instLE Real.instZero Real.decidableLE NNReal instSMul Real.toNNReal InvolutiveNeg.toNeg instInvolutiveNeg Real.instNeg	—	—
real_smul_neg 📖	mathematical	Real Real.instLT Real.instZero	MeasureTheory.JordanDecomposition instSMulReal InvolutiveNeg.toNeg instInvolutiveNeg NNReal instSMul Real.toNNReal Real.instNeg	—	not_le
real_smul_negPart_neg 📖	mathematical	Real Real.instLT Real.instZero	negPart MeasureTheory.JordanDecomposition instSMulReal NNReal MeasureTheory.Measure MeasureTheory.Measure.instSMul Algebra.toSMul ENNReal instCommSemiringNNReal CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instAlgebraNNReal Algebra.id IsScalarTower.right Real.toNNReal Real.instNeg posPart	—	IsScalarTower.right real_smul_def smul_posPart not_le neg_negPart
real_smul_negPart_nonneg 📖	mathematical	Real Real.instLE Real.instZero	negPart MeasureTheory.JordanDecomposition instSMulReal NNReal MeasureTheory.Measure MeasureTheory.Measure.instSMul Algebra.toSMul ENNReal instCommSemiringNNReal CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instAlgebraNNReal Algebra.id IsScalarTower.right Real.toNNReal	—	IsScalarTower.right real_smul_def smul_negPart
real_smul_nonneg 📖	mathematical	Real Real.instLE Real.instZero	MeasureTheory.JordanDecomposition instSMulReal NNReal instSMul Real.toNNReal	—	—
real_smul_posPart_neg 📖	mathematical	Real Real.instLT Real.instZero	posPart MeasureTheory.JordanDecomposition instSMulReal NNReal MeasureTheory.Measure MeasureTheory.Measure.instSMul Algebra.toSMul ENNReal instCommSemiringNNReal CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instAlgebraNNReal Algebra.id IsScalarTower.right Real.toNNReal Real.instNeg negPart	—	IsScalarTower.right real_smul_def smul_negPart not_le neg_posPart
real_smul_posPart_nonneg 📖	mathematical	Real Real.instLE Real.instZero	posPart MeasureTheory.JordanDecomposition instSMulReal NNReal MeasureTheory.Measure MeasureTheory.Measure.instSMul Algebra.toSMul ENNReal instCommSemiringNNReal CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instAlgebraNNReal Algebra.id IsScalarTower.right Real.toNNReal	—	IsScalarTower.right real_smul_def smul_posPart
smul_negPart 📖	mathematical	—	negPart NNReal MeasureTheory.JordanDecomposition instSMul MeasureTheory.Measure MeasureTheory.Measure.instSMul Algebra.toSMul ENNReal instCommSemiringNNReal CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instAlgebraNNReal Algebra.id IsScalarTower.right	—	—
smul_posPart 📖	mathematical	—	posPart NNReal MeasureTheory.JordanDecomposition instSMul MeasureTheory.Measure MeasureTheory.Measure.instSMul Algebra.toSMul ENNReal instCommSemiringNNReal CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instAlgebraNNReal Algebra.id IsScalarTower.right	—	—
toJordanDecomposition_toSignedMeasure 📖	mathematical	—	MeasureTheory.SignedMeasure.toJordanDecomposition toSignedMeasure	—	toSignedMeasure_injective MeasureTheory.SignedMeasure.toSignedMeasure_toJordanDecomposition
toSignedMeasure_injective 📖	mathematical	—	MeasureTheory.JordanDecomposition MeasureTheory.SignedMeasure toSignedMeasure	—	exists_compl_positive_negative MeasureTheory.SignedMeasure.of_symmDiff_compl_positive_negative MeasurableSet.compl compl_compl MeasureTheory.Measure.ext instIsTopologicalAddGroupReal posPart_finite negPart_finite toSignedMeasure.eq_1 MeasureTheory.Measure.toSignedMeasure_sub_apply MeasurableSet.inter MeasureTheory.measureReal_def nonpos_iff_eq_zero ENNReal.instCanonicallyOrderedAdd MeasureTheory.measure_mono MeasureTheory.Measure.instOuterMeasureClass Set.inter_subset_right ENNReal.toReal_zero sub_zero Set.inter_union_compl MeasureTheory.measureReal_union MeasureTheory.measure_ne_top Set.disjoint_of_subset_left Set.disjoint_of_subset_right disjoint_compl_right zero_add MeasureTheory.measureReal_eq_measureReal_iff MeasureTheory.SignedMeasure.of_inter_eq_of_symmDiff_eq_zero_positive
toSignedMeasure_neg 📖	mathematical	—	toSignedMeasure MeasureTheory.JordanDecomposition InvolutiveNeg.toNeg instInvolutiveNeg MeasureTheory.SignedMeasure MeasureTheory.VectorMeasure.instNeg Real Real.instAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instIsTopologicalAddGroupReal	—	MeasureTheory.VectorMeasure.ext instIsTopologicalAddGroupReal MeasureTheory.VectorMeasure.neg_apply posPart_finite negPart_finite toSignedMeasure.eq_1 MeasureTheory.Measure.toSignedMeasure_sub_apply neg_sub neg_posPart neg_negPart
toSignedMeasure_smul 📖	mathematical	—	toSignedMeasure NNReal MeasureTheory.JordanDecomposition instSMul MeasureTheory.SignedMeasure MeasureTheory.VectorMeasure.instSMul Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instSemiringNNReal NNReal.instDistribMulActionOfReal AddCommMonoid.toAddMonoid Module.toDistribMulAction Real.semiring Semiring.toModule SMulCommClass.continuousConstSMul Real.instMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Algebra.to_smulCommClass instCommSemiringNNReal NNReal.instAlgebraOfReal Algebra.id Real.instCommSemiring IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.commRing instIsTopologicalRingReal	—	MeasureTheory.VectorMeasure.ext SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal MeasureTheory.VectorMeasure.smul_apply instIsTopologicalAddGroupReal posPart_finite negPart_finite toSignedMeasure.eq_1 MeasureTheory.Measure.toSignedMeasure_sub_apply smul_sub IsScalarTower.right smul_posPart smul_negPart MeasureTheory.measureReal_nnreal_smul_apply
toSignedMeasure_zero 📖	mathematical	—	toSignedMeasure MeasureTheory.JordanDecomposition instZero MeasureTheory.SignedMeasure MeasureTheory.VectorMeasure.instZero Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	—	MeasureTheory.VectorMeasure.ext instIsTopologicalAddGroupReal posPart_finite negPart_finite toSignedMeasure.eq_1 MeasureTheory.Measure.toSignedMeasure_sub_apply zero_posPart zero_negPart sub_self MeasureTheory.VectorMeasure.coe_zero Pi.zero_apply
zero_negPart 📖	mathematical	—	negPart MeasureTheory.JordanDecomposition instZero MeasureTheory.Measure MeasureTheory.Measure.instZero	—	—
zero_posPart 📖	mathematical	—	posPart MeasureTheory.JordanDecomposition instZero MeasureTheory.Measure MeasureTheory.Measure.instZero	—	—

MeasureTheory.SignedMeasure

Definitions

Name	Category	Theorems
toJordanDecomposition 📖	CompOp	20 math math: rnDeriv_def, MeasureTheory.Measure.toJordanDecomposition_toSignedMeasure_sub, HaveLebesgueDecomposition.negPart, totalVariation_mutuallySingular_iff, toJordanDecomposition_eq_of_eq_add_withDensity, toJordanDecomposition_zero, HaveLebesgueDecomposition.posPart, singularPart_totalVariation, toSignedMeasure_toJordanDecomposition, toJordanDecomposition_smul_real, singularPart_mutuallySingular, not_haveLebesgueDecomposition_iff, toJordanDecomposition_neg, jordanDecomposition_add_withDensity_mutuallySingular, toJordanDecomposition_eq, MeasureTheory.JordanDecomposition.toJordanDecomposition_toSignedMeasure, toJordanDecompositionEquiv_apply, totalVariation_absolutelyContinuous_iff, toJordanDecomposition_smul, toJordanDecomposition_spec
toJordanDecompositionEquiv 📖	CompOp	2 math math: toJordanDecompositionEquiv_apply, toJordanDecompositionEquiv_symm_apply
totalVariation 📖	CompOp	8 math math: totalVariation_mutuallySingular_iff, mutuallySingular_ennreal_iff, singularPart_totalVariation, totalVariation_zero, absolutelyContinuous_ennreal_iff, mutuallySingular_iff, totalVariation_neg, totalVariation_absolutelyContinuous_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
absolutelyContinuous_ennreal_iff 📖	mathematical	—	MeasureTheory.VectorMeasure.AbsolutelyContinuous Real ENNReal Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace MeasureTheory.Measure.AbsolutelyContinuous totalVariation MeasureTheory.VectorMeasure.ennrealToMeasure	—	MeasurableSet.compl toJordanDecomposition_spec totalVariation.eq_1 MeasureTheory.Measure.add_apply MeasureTheory.VectorMeasure.nonneg_of_zero_le_restrict MeasureTheory.VectorMeasure.zero_le_restrict_subset Set.inter_subset_left toMeasureOfZeroLE_apply instIsTopologicalAddGroupReal MeasureTheory.VectorMeasure.neg_le_neg Real.instIsOrderedAddMonoid neg_zero MeasureTheory.VectorMeasure.neg_apply toMeasureOfLEZero_apply MeasureTheory.VectorMeasure.AbsolutelyContinuous.ennrealToMeasure MeasureTheory.measure_mono_null MeasureTheory.Measure.instOuterMeasureClass Set.inter_subset_right add_zero null_of_totalVariation_zero MeasureTheory.VectorMeasure.ennrealToMeasure_apply
mutuallySingular_ennreal_iff 📖	mathematical	—	MeasureTheory.VectorMeasure.MutuallySingular Real ENNReal Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace MeasureTheory.Measure.MutuallySingular totalVariation MeasureTheory.VectorMeasure.ennrealToMeasure	—	MeasurableSet.compl toJordanDecomposition_spec totalVariation.eq_1 MeasureTheory.Measure.add_apply MeasureTheory.VectorMeasure.nonneg_of_zero_le_restrict MeasureTheory.VectorMeasure.zero_le_restrict_subset Set.inter_subset_left toMeasureOfZeroLE_apply instIsTopologicalAddGroupReal MeasureTheory.VectorMeasure.neg_le_neg Real.instIsOrderedAddMonoid neg_zero MeasureTheory.VectorMeasure.neg_apply toMeasureOfLEZero_apply Set.inter_subset_right add_zero MeasureTheory.VectorMeasure.ennrealToMeasure_apply Set.Subset.refl null_of_totalVariation_zero MeasureTheory.measure_mono_null MeasureTheory.Measure.instOuterMeasureClass
mutuallySingular_iff 📖	mathematical	—	MeasureTheory.VectorMeasure.MutuallySingular Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace MeasureTheory.Measure.MutuallySingular totalVariation	—	MeasurableSet.compl toJordanDecomposition_spec totalVariation.eq_1 MeasureTheory.Measure.add_apply MeasureTheory.VectorMeasure.nonneg_of_zero_le_restrict MeasureTheory.VectorMeasure.zero_le_restrict_subset Set.inter_subset_left toMeasureOfZeroLE_apply instIsTopologicalAddGroupReal MeasureTheory.VectorMeasure.neg_le_neg Real.instIsOrderedAddMonoid neg_zero MeasureTheory.VectorMeasure.neg_apply toMeasureOfLEZero_apply Set.inter_subset_right add_zero null_of_totalVariation_zero MeasureTheory.measure_mono_null MeasureTheory.Measure.instOuterMeasureClass
null_of_totalVariation_zero 📖	mathematical	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike totalVariation instZeroENNReal	MeasureTheory.VectorMeasure.measureOf' Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero	—	toSignedMeasure_toJordanDecomposition instIsTopologicalAddGroupReal MeasureTheory.JordanDecomposition.posPart_finite MeasureTheory.JordanDecomposition.negPart_finite MeasureTheory.JordanDecomposition.toSignedMeasure.eq_1 MeasureTheory.VectorMeasure.coe_sub Pi.sub_apply MeasureTheory.Measure.toSignedMeasure_apply add_eq_zero Unique.instSubsingleton Pi.add_apply MeasureTheory.Measure.coe_add totalVariation.eq_1 sub_self
of_diff_eq_zero_of_symmDiff_eq_zero_negative 📖	—	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 MeasureTheory.VectorMeasure.measureOf' symmDiff Set SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.instSDiff Real.instZero	—	—	instIsTopologicalAddGroupReal of_diff_eq_zero_of_symmDiff_eq_zero_positive neg_zero MeasureTheory.VectorMeasure.neg_le_neg_iff Real.instIsOrderedAddMonoid
of_diff_eq_zero_of_symmDiff_eq_zero_positive 📖	—	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 MeasureTheory.VectorMeasure.measureOf' symmDiff Set SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.instSDiff Real.instZero	—	—	MeasureTheory.VectorMeasure.restrict_le_restrict_iff MeasurableSet.diff Set.diff_subset Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf 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.neg_zero Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_zero 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.Linarith.add_lt_of_le_of_neg Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le Real.instIsOrderedRing MeasureTheory.VectorMeasure.zero_apply Mathlib.Tactic.Linarith.sub_neg_of_lt Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Linarith.le_of_eq_of_le sub_eq_zero_of_eq MeasureTheory.VectorMeasure.of_union TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Set.disjoint_of_subset_left disjoint_sdiff_self_right Set.symmDiff_def
of_inter_eq_of_symmDiff_eq_zero_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 MeasureTheory.VectorMeasure.measureOf' symmDiff Set SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.instSDiff Real.instZero	Set.instInter	—	instIsTopologicalAddGroupReal of_inter_eq_of_symmDiff_eq_zero_positive neg_zero MeasureTheory.VectorMeasure.neg_le_neg_iff Real.instIsOrderedAddMonoid
of_inter_eq_of_symmDiff_eq_zero_positive 📖	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 MeasureTheory.VectorMeasure.measureOf' symmDiff Set SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.instSDiff Real.instZero	Set.instInter	—	subset_positive_null_set MeasurableSet.union MeasurableSet.symmDiff MeasurableSet.inter MeasureTheory.VectorMeasure.restrict_le_restrict_union Real.instIsOrderedAddMonoid OrderTopology.to_orderClosedTopology instOrderTopologyReal Set.symmDiff_subset_union Set.inter_symmDiff_distrib_left Set.inter_subset_right of_diff_eq_zero_of_symmDiff_eq_zero_positive MeasureTheory.VectorMeasure.restrict_le_restrict_subset MeasureTheory.VectorMeasure.of_diff_of_diff_eq_zero TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace zero_add
subset_negative_null_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 MeasureTheory.VectorMeasure.measureOf' Real.instZero Set Set.instHasSubset	—	—	instIsTopologicalAddGroupReal subset_positive_null_set neg_zero MeasureTheory.VectorMeasure.neg_le_neg_iff Real.instIsOrderedAddMonoid
subset_positive_null_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 MeasureTheory.VectorMeasure.measureOf' Real.instZero Set Set.instHasSubset	—	—	MeasureTheory.VectorMeasure.of_union TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Set.disjoint_sdiff_right MeasurableSet.diff Set.union_diff_self Set.union_eq_self_of_subset_left MeasureTheory.VectorMeasure.nonneg_of_zero_le_restrict MeasureTheory.VectorMeasure.restrict_le_restrict_subset HasSubset.Subset.trans Set.instIsTransSubset Set.diff_subset Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf 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.neg_zero Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_zero 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.Linarith.add_lt_of_le_of_neg Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Linarith.le_of_eq_of_le sub_eq_zero_of_eq
toJordanDecompositionEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv MeasureTheory.SignedMeasure MeasureTheory.JordanDecomposition EquivLike.toFunLike Equiv.instEquivLike toJordanDecompositionEquiv toJordanDecomposition	—	—
toJordanDecompositionEquiv_symm_apply 📖	mathematical	—	DFunLike.coe Equiv MeasureTheory.JordanDecomposition MeasureTheory.SignedMeasure EquivLike.toFunLike Equiv.instEquivLike Equiv.symm toJordanDecompositionEquiv MeasureTheory.JordanDecomposition.toSignedMeasure	—	—
toJordanDecomposition_eq 📖	mathematical	MeasureTheory.JordanDecomposition.toSignedMeasure	toJordanDecomposition	—	MeasureTheory.JordanDecomposition.toJordanDecomposition_toSignedMeasure
toJordanDecomposition_neg 📖	mathematical	—	toJordanDecomposition MeasureTheory.SignedMeasure MeasureTheory.VectorMeasure.instNeg Real Real.instAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instIsTopologicalAddGroupReal MeasureTheory.JordanDecomposition InvolutiveNeg.toNeg MeasureTheory.JordanDecomposition.instInvolutiveNeg	—	MeasureTheory.JordanDecomposition.toSignedMeasure_injective instIsTopologicalAddGroupReal toSignedMeasure_toJordanDecomposition MeasureTheory.JordanDecomposition.toSignedMeasure_neg
toJordanDecomposition_smul 📖	mathematical	—	toJordanDecomposition NNReal MeasureTheory.SignedMeasure MeasureTheory.VectorMeasure.instSMul Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instSemiringNNReal NNReal.instDistribMulActionOfReal AddCommMonoid.toAddMonoid Module.toDistribMulAction Real.semiring Semiring.toModule SMulCommClass.continuousConstSMul Real.instMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Algebra.to_smulCommClass instCommSemiringNNReal NNReal.instAlgebraOfReal Algebra.id Real.instCommSemiring IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.commRing instIsTopologicalRingReal MeasureTheory.JordanDecomposition MeasureTheory.JordanDecomposition.instSMul	—	MeasureTheory.JordanDecomposition.toSignedMeasure_injective SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal toSignedMeasure_toJordanDecomposition MeasureTheory.JordanDecomposition.toSignedMeasure_smul
toJordanDecomposition_smul_real 📖	mathematical	—	toJordanDecomposition Real MeasureTheory.SignedMeasure MeasureTheory.VectorMeasure.instSMul Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.semiring Module.toDistribMulAction Semiring.toModule UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.uniformContinuousConstSMul Real.instRing instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal MeasureTheory.JordanDecomposition MeasureTheory.JordanDecomposition.instSMulReal	—	UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal MeasureTheory.JordanDecomposition.ext IsScalarTower.right MeasureTheory.JordanDecomposition.real_smul_posPart_neg instIsTopologicalAddGroupReal neg_smul neg_neg toJordanDecomposition_neg MeasureTheory.JordanDecomposition.neg_posPart Left.nonneg_neg_iff IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid LT.lt.le MeasureTheory.JordanDecomposition.smul_negPart MeasureTheory.JordanDecomposition.real_smul_nonneg MeasureTheory.JordanDecomposition.real_smul_negPart_neg MeasureTheory.JordanDecomposition.neg_negPart MeasureTheory.JordanDecomposition.smul_posPart
toJordanDecomposition_spec 📖	mathematical	—	MeasureTheory.JordanDecomposition.posPart toJordanDecomposition toMeasureOfZeroLE MeasureTheory.JordanDecomposition.negPart toMeasureOfLEZero Compl.compl Set Set.instCompl MeasurableSet.compl	—	exists_compl_positive_negative MeasurableSet.compl
toJordanDecomposition_zero 📖	mathematical	—	toJordanDecomposition MeasureTheory.SignedMeasure MeasureTheory.VectorMeasure.instZero Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace MeasureTheory.JordanDecomposition MeasureTheory.JordanDecomposition.instZero	—	MeasureTheory.JordanDecomposition.toSignedMeasure_injective toSignedMeasure_toJordanDecomposition MeasureTheory.JordanDecomposition.toSignedMeasure_zero
toSignedMeasure_toJordanDecomposition 📖	mathematical	—	MeasureTheory.JordanDecomposition.toSignedMeasure toJordanDecomposition	—	MeasurableSet.compl toJordanDecomposition_spec instIsTopologicalAddGroupReal MeasureTheory.JordanDecomposition.posPart_finite MeasureTheory.JordanDecomposition.negPart_finite MeasureTheory.Measure.toSignedMeasure.congr_simp MeasureTheory.VectorMeasure.ext MeasureTheory.Measure.toSignedMeasure_sub_apply toMeasureOfZeroLE_real_apply toMeasureOfLEZero_real_apply sub_neg_eq_add MeasureTheory.VectorMeasure.of_union TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Disjoint.inf_right Disjoint.inf_left disjoint_compl_right MeasurableSet.inter Set.inter_comm Set.inter_union_compl
totalVariation_absolutelyContinuous_iff 📖	mathematical	—	MeasureTheory.Measure.AbsolutelyContinuous totalVariation MeasureTheory.JordanDecomposition.posPart toJordanDecomposition MeasureTheory.JordanDecomposition.negPart	—	add_eq_zero Unique.instSubsingleton MeasureTheory.Measure.add_apply totalVariation.eq_1 add_zero
totalVariation_mutuallySingular_iff 📖	mathematical	—	MeasureTheory.Measure.MutuallySingular totalVariation MeasureTheory.JordanDecomposition.posPart toJordanDecomposition MeasureTheory.JordanDecomposition.negPart	—	MeasureTheory.Measure.MutuallySingular.add_left_iff
totalVariation_neg 📖	mathematical	—	totalVariation MeasureTheory.SignedMeasure MeasureTheory.VectorMeasure.instNeg Real Real.instAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instIsTopologicalAddGroupReal	—	instIsTopologicalAddGroupReal toJordanDecomposition_neg add_comm
totalVariation_zero 📖	mathematical	—	totalVariation MeasureTheory.SignedMeasure MeasureTheory.VectorMeasure.instZero Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace MeasureTheory.Measure MeasureTheory.Measure.instZero	—	toJordanDecomposition_zero add_zero

---

← Back to Index