Lebesgue

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

Statistics

Metric	Count
Definitions HaveLebesgueDecomposition, rnDeriv, singularPart, HaveLebesgueDecomposition, rnDeriv, singularPart	6
Theorems imPart, rePart, integrable_rnDeriv, singularPart_add_withDensity_rnDeriv_eq, negPart, posPart, eq_rnDeriv, eq_singularPart, haveLebesgueDecomposition_mk, haveLebesgueDecomposition_neg, haveLebesgueDecomposition_of_sigmaFinite, haveLebesgueDecomposition_smul, haveLebesgueDecomposition_smul_real, integrable_rnDeriv, jordanDecomposition_add_withDensity_mutuallySingular, measurable_rnDeriv, mutuallySingular_singularPart, not_haveLebesgueDecomposition_iff, rnDeriv_add, rnDeriv_def, rnDeriv_neg, rnDeriv_smul, rnDeriv_sub, singularPart_add, singularPart_add_withDensity_rnDeriv_eq, singularPart_mutuallySingular, singularPart_neg, singularPart_smul, singularPart_smul_nnreal, singularPart_sub, singularPart_totalVariation, singularPart_zero, toJordanDecomposition_eq_of_eq_add_withDensity	33
Total	39

MeasureTheory.ComplexMeasure

Definitions

Name	Category	Theorems
HaveLebesgueDecomposition 📖	CompData	—
rnDeriv 📖	CompOp	2 math math: singularPart_add_withDensity_rnDeriv_eq, integrable_rnDeriv
singularPart 📖	CompOp	1 math math: singularPart_add_withDensity_rnDeriv_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
integrable_rnDeriv 📖	mathematical	—	MeasureTheory.Integrable Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing rnDeriv	—	MeasureTheory.memLp_one_iff_integrable MeasureTheory.memLp_re_im_iff MeasureTheory.SignedMeasure.integrable_rnDeriv
singularPart_add_withDensity_rnDeriv_eq 📖	mathematical	—	MeasureTheory.ComplexMeasure MeasureTheory.VectorMeasure Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Complex.instNormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid MeasureTheory.VectorMeasure.instAdd SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing singularPart MeasureTheory.Measure.withDensityᵥ InnerProductSpace.toNormedSpace Real Real.instRCLike instInnerProductSpaceRealComplex rnDeriv	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing instIsTopologicalRingReal UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul toComplexMeasure_to_signedMeasure MeasureTheory.VectorMeasure.ext MeasureTheory.VectorMeasure.add_apply MeasureTheory.SignedMeasure.toComplexMeasure_apply Complex.ext Complex.add_re MeasureTheory.withDensityᵥ_apply integrable_rnDeriv RCLike.re_eq_complex_re integral_re MeasureTheory.Integrable.integrableOn MeasureTheory.SignedMeasure.integrable_rnDeriv MeasureTheory.SignedMeasure.singularPart_add_withDensity_rnDeriv_eq HaveLebesgueDecomposition.rePart Complex.add_im RCLike.im_eq_complex_im integral_im HaveLebesgueDecomposition.imPart

MeasureTheory.ComplexMeasure.HaveLebesgueDecomposition

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
imPart 📖	mathematical	—	MeasureTheory.SignedMeasure.HaveLebesgueDecomposition DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring MeasureTheory.ComplexMeasure MeasureTheory.SignedMeasure MeasureTheory.VectorMeasure.instAddCommMonoid Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing Real.instAddCommMonoid Real.pseudoMetricSpace Real.normedCommRing instIsTopologicalRingReal MeasureTheory.VectorMeasure.instModule NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedSpace.complexToReal NormedField.toNormedSpace UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsBoundedSMul.toUniformContinuousConstSMul Real.instZero Complex.instZero NormedSpace.toIsBoundedSMul Ring.uniformContinuousConstSMul Real.instRing instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing LinearMap.instFunLike MeasureTheory.ComplexMeasure.im	—	—
rePart 📖	mathematical	—	MeasureTheory.SignedMeasure.HaveLebesgueDecomposition DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring MeasureTheory.ComplexMeasure MeasureTheory.SignedMeasure MeasureTheory.VectorMeasure.instAddCommMonoid Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing Real.instAddCommMonoid Real.pseudoMetricSpace Real.normedCommRing instIsTopologicalRingReal MeasureTheory.VectorMeasure.instModule NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedSpace.complexToReal NormedField.toNormedSpace UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsBoundedSMul.toUniformContinuousConstSMul Real.instZero Complex.instZero NormedSpace.toIsBoundedSMul Ring.uniformContinuousConstSMul Real.instRing instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing LinearMap.instFunLike MeasureTheory.ComplexMeasure.re	—	—

MeasureTheory.SignedMeasure

Definitions

Name	Category	Theorems
HaveLebesgueDecomposition 📖	CompData	8 math math: haveLebesgueDecomposition_mk, MeasureTheory.ComplexMeasure.HaveLebesgueDecomposition.imPart, not_haveLebesgueDecomposition_iff, haveLebesgueDecomposition_smul_real, MeasureTheory.ComplexMeasure.HaveLebesgueDecomposition.rePart, haveLebesgueDecomposition_smul, haveLebesgueDecomposition_of_sigmaFinite, haveLebesgueDecomposition_neg
rnDeriv 📖	CompOp	12 math math: rnDeriv_def, eq_rnDeriv, withDensityᵥ_rnDeriv_eq, absolutelyContinuous_iff_withDensityᵥ_rnDeriv_eq, MeasureTheory.rnDeriv_ae_eq_condExp, measurable_rnDeriv, rnDeriv_smul, singularPart_add_withDensity_rnDeriv_eq, rnDeriv_neg, integrable_rnDeriv, rnDeriv_add, rnDeriv_sub
singularPart 📖	CompOp	10 math math: singularPart_smul, mutuallySingular_singularPart, singularPart_totalVariation, singularPart_add, eq_singularPart, singularPart_zero, singularPart_neg, singularPart_sub, singularPart_add_withDensity_rnDeriv_eq, singularPart_smul_nnreal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_rnDeriv 📖	mathematical	MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing MeasureTheory.VectorMeasure.MutuallySingular ENNReal Real.instAddCommMonoid ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace MeasureTheory.Measure.toENNRealVectorMeasure MeasureTheory.SignedMeasure MeasureTheory.VectorMeasure ESeminormedAddCommMonoid.toAddCommMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.normedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid MeasureTheory.VectorMeasure.instAdd IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal MeasureTheory.Measure.withDensityᵥ InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass rnDeriv	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal MeasureTheory.WithDensityᵥEq.congr_ae Filter.EventuallyEq.symm MeasureTheory.Measure.instOuterMeasureClass PseudoEMetricSpace.pseudoMetrizableSpace Real.borelSpace MeasureTheory.Integrable.ae_eq_of_withDensityᵥ_eq Real.instCompleteSpace integrable_rnDeriv AddLeftCancelSemigroup.toIsLeftCancelAdd instIsTopologicalAddGroupReal eq_singularPart singularPart_add_withDensity_rnDeriv_eq
eq_singularPart 📖	mathematical	MeasureTheory.VectorMeasure.MutuallySingular Real ENNReal Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace MeasureTheory.Measure.toENNRealVectorMeasure MeasureTheory.SignedMeasure MeasureTheory.VectorMeasure ESeminormedAddCommMonoid.toAddCommMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.normedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid MeasureTheory.VectorMeasure.instAdd IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal MeasureTheory.Measure.withDensityᵥ InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal	singularPart	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal PseudoEMetricSpace.pseudoMetrizableSpace Real.borelSpace MeasureTheory.Integrable.congr MeasureTheory.WithDensityᵥEq.congr_ae Filter.EventuallyEq.symm MeasureTheory.Measure.instOuterMeasureClass measurable_zero MeasureTheory.integrable_zero MeasureTheory.withDensityᵥ_zero instIsTopologicalAddGroupReal add_zero MeasureTheory.Measure.withDensityᵥ.eq_1
haveLebesgueDecomposition_mk 📖	mathematical	Measurable Real Real.measurableSpace MeasureTheory.VectorMeasure.MutuallySingular ENNReal Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace MeasureTheory.Measure.toENNRealVectorMeasure MeasureTheory.SignedMeasure MeasureTheory.VectorMeasure ESeminormedAddCommMonoid.toAddCommMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.normedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid MeasureTheory.VectorMeasure.instAdd IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal MeasureTheory.Measure.withDensityᵥ InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal	HaveLebesgueDecomposition	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal measurable_zero MeasureTheory.integrable_zero MeasureTheory.withDensityᵥ_zero instIsTopologicalAddGroupReal add_zero MeasureTheory.Measure.withDensityᵥ.eq_1
haveLebesgueDecomposition_neg 📖	mathematical	—	HaveLebesgueDecomposition MeasureTheory.SignedMeasure MeasureTheory.VectorMeasure.instNeg Real Real.instAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instIsTopologicalAddGroupReal	—	instIsTopologicalAddGroupReal toJordanDecomposition_neg MeasureTheory.JordanDecomposition.neg_posPart HaveLebesgueDecomposition.negPart MeasureTheory.JordanDecomposition.neg_negPart HaveLebesgueDecomposition.posPart
haveLebesgueDecomposition_of_sigmaFinite 📖	mathematical	—	HaveLebesgueDecomposition	—	MeasureTheory.Measure.haveLebesgueDecomposition_of_sigmaFinite MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite MeasureTheory.JordanDecomposition.posPart_finite MeasureTheory.JordanDecomposition.negPart_finite
haveLebesgueDecomposition_smul 📖	mathematical	—	HaveLebesgueDecomposition NNReal MeasureTheory.SignedMeasure MeasureTheory.VectorMeasure.instSMul Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instSemiringNNReal NNReal.instDistribMulActionOfReal AddCommMonoid.toAddMonoid Module.toDistribMulAction Real.semiring NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal 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 NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal	—	SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal toJordanDecomposition_smul IsScalarTower.right MeasureTheory.JordanDecomposition.smul_posPart MeasureTheory.Measure.haveLebesgueDecompositionSMul HaveLebesgueDecomposition.posPart MeasureTheory.JordanDecomposition.smul_negPart HaveLebesgueDecomposition.negPart
haveLebesgueDecomposition_smul_real 📖	mathematical	—	HaveLebesgueDecomposition Real MeasureTheory.SignedMeasure MeasureTheory.VectorMeasure.instSMul Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.semiring Module.toDistribMulAction NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal 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	—	UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal CanLift.prf NNReal.canLift haveLebesgueDecomposition_smul toJordanDecomposition_smul_real IsScalarTower.right MeasureTheory.JordanDecomposition.real_smul_posPart_neg MeasureTheory.Measure.haveLebesgueDecompositionSMul HaveLebesgueDecomposition.negPart MeasureTheory.JordanDecomposition.real_smul_negPart_neg HaveLebesgueDecomposition.posPart
integrable_rnDeriv 📖	mathematical	—	MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing rnDeriv	—	MeasureTheory.Integrable.sub Measurable.aestronglyMeasurable PseudoEMetricSpace.pseudoMetrizableSpace instSecondCountableTopologyReal BorelSpace.opensMeasurable Real.borelSpace Measurable.ennreal_toReal MeasureTheory.Measure.measurable_rnDeriv MeasureTheory.hasFiniteIntegral_toReal_of_lintegral_ne_top LT.lt.ne MeasureTheory.Measure.lintegral_rnDeriv_lt_top MeasureTheory.JordanDecomposition.posPart_finite MeasureTheory.JordanDecomposition.negPart_finite
jordanDecomposition_add_withDensity_mutuallySingular 📖	mathematical	Measurable Real Real.measurableSpace MeasureTheory.VectorMeasure.MutuallySingular ENNReal Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace MeasureTheory.Measure.toENNRealVectorMeasure	MeasureTheory.Measure.MutuallySingular MeasureTheory.Measure MeasureTheory.Measure.instAdd MeasureTheory.JordanDecomposition.posPart toJordanDecomposition MeasureTheory.Measure.withDensity ENNReal.ofReal MeasureTheory.JordanDecomposition.negPart Real.instNeg	—	MeasureTheory.Measure.MutuallySingular.add_left MeasureTheory.Measure.MutuallySingular.add_right MeasureTheory.JordanDecomposition.mutuallySingular MeasureTheory.Measure.MutuallySingular.mono_ac MeasureTheory.VectorMeasure.ennrealToMeasure_toENNRealVectorMeasure totalVariation_mutuallySingular_iff mutuallySingular_ennreal_iff refl MeasureTheory.Measure.AbsolutelyContinuous.instRefl MeasureTheory.withDensity_absolutelyContinuous MeasureTheory.Measure.MutuallySingular.symm MeasureTheory.withDensity_ofReal_mutuallySingular
measurable_rnDeriv 📖	mathematical	—	Measurable Real Real.measurableSpace rnDeriv	—	rnDeriv_def Measurable.sub ContinuousSub.measurableSub₂ Real.borelSpace instSecondCountableTopologyReal IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal Measurable.ennreal_toReal MeasureTheory.Measure.measurable_rnDeriv
mutuallySingular_singularPart 📖	mathematical	—	MeasureTheory.VectorMeasure.MutuallySingular Real ENNReal Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace singularPart MeasureTheory.Measure.toENNRealVectorMeasure	—	mutuallySingular_ennreal_iff singularPart_totalVariation MeasureTheory.VectorMeasure.ennrealToMeasure_toENNRealVectorMeasure MeasureTheory.Measure.MutuallySingular.add_left MeasureTheory.Measure.mutuallySingular_singularPart
not_haveLebesgueDecomposition_iff 📖	mathematical	—	HaveLebesgueDecomposition MeasureTheory.Measure.HaveLebesgueDecomposition MeasureTheory.JordanDecomposition.posPart toJordanDecomposition MeasureTheory.JordanDecomposition.negPart	—	not_or_of_imp not_and_or HaveLebesgueDecomposition.posPart HaveLebesgueDecomposition.negPart
rnDeriv_add 📖	mathematical	—	Filter.EventuallyEq Real MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass rnDeriv MeasureTheory.SignedMeasure MeasureTheory.VectorMeasure.instAdd Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Pi.instAdd Real.instAdd	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal MeasureTheory.Integrable.ae_eq_of_withDensityᵥ_eq Real.instCompleteSpace integrable_rnDeriv MeasureTheory.Integrable.add AddLeftCancelSemigroup.toIsLeftCancelAdd instIsTopologicalAddGroupReal singularPart_add_withDensity_rnDeriv_eq IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.withDensityᵥ_add singularPart_add add_assoc add_comm
rnDeriv_def 📖	mathematical	—	rnDeriv Real Real.instSub ENNReal.toReal MeasureTheory.Measure.rnDeriv MeasureTheory.JordanDecomposition.posPart toJordanDecomposition MeasureTheory.JordanDecomposition.negPart	—	—
rnDeriv_neg 📖	mathematical	—	Filter.EventuallyEq Real MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass rnDeriv MeasureTheory.SignedMeasure MeasureTheory.VectorMeasure.instNeg Real.instAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instIsTopologicalAddGroupReal Pi.instNeg Real.instNeg	—	MeasureTheory.Integrable.ae_eq_of_withDensityᵥ_eq Real.instCompleteSpace instIsTopologicalAddGroupReal integrable_rnDeriv MeasureTheory.Integrable.neg SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.withDensityᵥ_neg IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal AddLeftCancelSemigroup.toIsLeftCancelAdd singularPart_add_withDensity_rnDeriv_eq haveLebesgueDecomposition_neg singularPart_neg neg_add
rnDeriv_smul 📖	mathematical	—	Filter.EventuallyEq Real MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass rnDeriv MeasureTheory.SignedMeasure MeasureTheory.VectorMeasure.instSMul Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.semiring Module.toDistribMulAction NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal 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 Function.hasSMul Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id	—	MeasureTheory.Integrable.ae_eq_of_withDensityᵥ_eq Real.instCompleteSpace UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal integrable_rnDeriv MeasureTheory.Integrable.smul Real.isBoundedSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul MeasureTheory.withDensityᵥ_smul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousAdd AddLeftCancelSemigroup.toIsLeftCancelAdd instIsTopologicalAddGroupReal singularPart_add_withDensity_rnDeriv_eq haveLebesgueDecomposition_smul_real singularPart_smul smul_add
rnDeriv_sub 📖	mathematical	—	Filter.EventuallyEq Real MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass rnDeriv MeasureTheory.SignedMeasure MeasureTheory.VectorMeasure.instSub Real.instAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instIsTopologicalAddGroupReal Pi.instSub Real.instSub	—	instIsTopologicalAddGroupReal MeasureTheory.Measure.instOuterMeasureClass sub_eq_add_neg Mathlib.Tactic.GCongr.rel_imp_rel instIsTransOfTrans IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal rnDeriv_add haveLebesgueDecomposition_neg Filter.EventuallyEq.refl Filter.EventuallyEq.add rnDeriv_neg
singularPart_add 📖	mathematical	—	singularPart MeasureTheory.SignedMeasure MeasureTheory.VectorMeasure.instAdd Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal eq_singularPart MeasureTheory.VectorMeasure.MutuallySingular.add_left ENNReal.instT2Space mutuallySingular_singularPart IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.withDensityᵥ_add integrable_rnDeriv instIsTopologicalAddGroupReal add_assoc add_comm singularPart_add_withDensity_rnDeriv_eq
singularPart_add_withDensity_rnDeriv_eq 📖	mathematical	—	MeasureTheory.SignedMeasure MeasureTheory.VectorMeasure Real ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.normedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid MeasureTheory.VectorMeasure.instAdd Real.instAddCommMonoid Real.pseudoMetricSpace IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal singularPart MeasureTheory.Measure.withDensityᵥ InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal rnDeriv	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instIsTopologicalAddGroupReal MeasureTheory.JordanDecomposition.posPart_finite MeasureTheory.JordanDecomposition.negPart_finite toSignedMeasure_toJordanDecomposition MeasureTheory.JordanDecomposition.toSignedMeasure.eq_1 singularPart.eq_1 rnDeriv_def SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.withDensityᵥ_sub' MeasureTheory.integrable_toReal_of_lintegral_ne_top Measurable.aemeasurable MeasureTheory.Measure.measurable_rnDeriv LT.lt.ne MeasureTheory.Measure.lintegral_rnDeriv_lt_top MeasureTheory.isFiniteMeasure_withDensity MeasureTheory.withDensityᵥ_toReal sub_eq_add_neg MeasureTheory.Measure.singularPart.instIsFiniteMeasure add_comm add_assoc MeasureTheory.isFiniteMeasureAdd MeasureTheory.Measure.toSignedMeasure_add neg_add MeasureTheory.Measure.haveLebesgueDecomposition_add HaveLebesgueDecomposition.posPart HaveLebesgueDecomposition.negPart
singularPart_mutuallySingular 📖	mathematical	—	MeasureTheory.Measure.MutuallySingular MeasureTheory.Measure.singularPart MeasureTheory.JordanDecomposition.posPart toJordanDecomposition MeasureTheory.JordanDecomposition.negPart	—	MeasureTheory.JordanDecomposition.mutuallySingular add_eq_zero Unique.instSubsingleton MeasureTheory.Measure.add_apply MeasureTheory.Measure.haveLebesgueDecomposition_add HaveLebesgueDecomposition.posPart HaveLebesgueDecomposition.negPart not_haveLebesgueDecomposition_iff MeasureTheory.Measure.HaveLebesgueDecomposition.lebesgue_decomposition MeasureTheory.Measure.singularPart_def MeasureTheory.Measure.MutuallySingular.zero_left MeasureTheory.Measure.MutuallySingular.zero_right
singularPart_neg 📖	mathematical	—	singularPart MeasureTheory.SignedMeasure MeasureTheory.VectorMeasure.instNeg Real Real.instAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instIsTopologicalAddGroupReal	—	instIsTopologicalAddGroupReal MeasureTheory.Measure.singularPart.instIsFiniteMeasure MeasureTheory.JordanDecomposition.posPart_finite MeasureTheory.JordanDecomposition.negPart_finite MeasureTheory.Measure.toSignedMeasure_congr toJordanDecomposition_neg MeasureTheory.JordanDecomposition.neg_posPart MeasureTheory.JordanDecomposition.neg_negPart singularPart.eq_1 neg_sub
singularPart_smul 📖	mathematical	—	singularPart Real MeasureTheory.SignedMeasure MeasureTheory.VectorMeasure.instSMul Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.semiring Module.toDistribMulAction NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal 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	—	le_or_gt UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal CanLift.prf NNReal.canLift singularPart_smul_nnreal instIsTopologicalAddGroupReal singularPart.eq_1 IsScalarTower.right toJordanDecomposition_smul_real MeasureTheory.JordanDecomposition.real_smul_posPart_neg MeasureTheory.Measure.singularPart_smul MeasureTheory.JordanDecomposition.real_smul_negPart_neg SMulCommClass.continuousConstSMul Algebra.to_smulCommClass MeasureTheory.Measure.singularPart.instIsFiniteMeasure MeasureTheory.JordanDecomposition.negPart_finite MeasureTheory.isFiniteMeasureSMulNNReal MeasureTheory.Measure.toSignedMeasure_smul MeasureTheory.JordanDecomposition.posPart_finite neg_sub smul_sub IsTopologicalSemiring.toContinuousAdd NNReal.smul_def neg_smul Real.coe_toNNReal le_of_lt neg_pos IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid neg_neg
singularPart_smul_nnreal 📖	mathematical	—	singularPart NNReal MeasureTheory.SignedMeasure MeasureTheory.VectorMeasure.instSMul Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instSemiringNNReal NNReal.instDistribMulActionOfReal AddCommMonoid.toAddMonoid Module.toDistribMulAction Real.semiring NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal 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 NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal	—	SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instIsTopologicalAddGroupReal singularPart.eq_1 UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul instIsUniformAddGroupReal smul_sub IsScalarTower.right MeasureTheory.isFiniteMeasureSMulNNReal MeasureTheory.Measure.toSignedMeasure_smul toJordanDecomposition_smul MeasureTheory.JordanDecomposition.smul_posPart MeasureTheory.Measure.singularPart_smul MeasureTheory.JordanDecomposition.smul_negPart
singularPart_sub 📖	mathematical	—	singularPart MeasureTheory.SignedMeasure MeasureTheory.VectorMeasure.instSub Real Real.instAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instIsTopologicalAddGroupReal	—	instIsTopologicalAddGroupReal sub_eq_add_neg IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal singularPart_add haveLebesgueDecomposition_neg singularPart_neg
singularPart_totalVariation 📖	mathematical	—	totalVariation singularPart MeasureTheory.Measure MeasureTheory.Measure.instAdd MeasureTheory.Measure.singularPart MeasureTheory.JordanDecomposition.posPart toJordanDecomposition MeasureTheory.JordanDecomposition.negPart	—	MeasureTheory.Measure.singularPart.instIsFiniteMeasure MeasureTheory.JordanDecomposition.posPart_finite MeasureTheory.JordanDecomposition.negPart_finite singularPart_mutuallySingular MeasureTheory.JordanDecomposition.toSignedMeasure_injective toSignedMeasure_toJordanDecomposition instIsTopologicalAddGroupReal singularPart.eq_1 MeasureTheory.JordanDecomposition.toSignedMeasure.eq_1 totalVariation.eq_1
singularPart_zero 📖	mathematical	—	singularPart MeasureTheory.SignedMeasure MeasureTheory.VectorMeasure.instZero Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	—	eq_singularPart MeasureTheory.VectorMeasure.MutuallySingular.zero_left IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instIsTopologicalAddGroupReal zero_add MeasureTheory.withDensityᵥ_zero
toJordanDecomposition_eq_of_eq_add_withDensity 📖	mathematical	Measurable Real Real.measurableSpace MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing MeasureTheory.VectorMeasure.MutuallySingular ENNReal Real.instAddCommMonoid ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace MeasureTheory.Measure.toENNRealVectorMeasure MeasureTheory.SignedMeasure MeasureTheory.VectorMeasure ESeminormedAddCommMonoid.toAddCommMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.normedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid MeasureTheory.VectorMeasure.instAdd IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal MeasureTheory.Measure.withDensityᵥ InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal	toJordanDecomposition MeasureTheory.Measure MeasureTheory.Measure.instAdd MeasureTheory.JordanDecomposition.posPart MeasureTheory.Measure.withDensity ENNReal.ofReal MeasureTheory.JordanDecomposition.negPart Real.instNeg jordanDecomposition_add_withDensity_mutuallySingular	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal toJordanDecomposition_eq jordanDecomposition_add_withDensity_mutuallySingular instIsTopologicalAddGroupReal MeasureTheory.JordanDecomposition.posPart_finite MeasureTheory.JordanDecomposition.negPart_finite MeasureTheory.VectorMeasure.ext MeasureTheory.VectorMeasure.sub_apply MeasureTheory.Measure.toSignedMeasure_apply_measurable MeasureTheory.measureReal_add_apply MeasureTheory.measure_ne_top MeasureTheory.isFiniteMeasure_withDensity_ofReal MeasureTheory.Integrable.neg add_sub_add_comm MeasureTheory.JordanDecomposition.toSignedMeasure.eq_1 toSignedMeasure_toJordanDecomposition MeasureTheory.VectorMeasure.add_apply MeasureTheory.withDensityᵥ_eq_withDensity_pos_part_sub_withDensity_neg_part

MeasureTheory.SignedMeasure.HaveLebesgueDecomposition

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
negPart 📖	mathematical	—	MeasureTheory.Measure.HaveLebesgueDecomposition MeasureTheory.JordanDecomposition.negPart MeasureTheory.SignedMeasure.toJordanDecomposition	—	—
posPart 📖	mathematical	—	MeasureTheory.Measure.HaveLebesgueDecomposition MeasureTheory.JordanDecomposition.posPart MeasureTheory.SignedMeasure.toJordanDecomposition	—	—

---

← Back to Index