Structures · Analysis
MeasureTheory.SignedMeasure.HaveLebesgueDecomposition
A signed measure s is said to HaveLebesgueDecomposition with respect to a measure μ
if the positive part and the negative part of s both HaveLebesgueDecomposition with
respect to μ.
- Shape
- 2 explicit arguments · adds posPart, negPart
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Provided automatically by
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by12
- MeasureTheory.SignedMeasure.singularPart_add_withDensity_rnDeriv_eq
- MeasureTheory.SignedMeasure.singularPart_add
- MeasureTheory.SignedMeasure.rnDeriv_add
- MeasureTheory.SignedMeasure.rnDeriv_neg
- MeasureTheory.SignedMeasure.rnDeriv_smul
- MeasureTheory.SignedMeasure.haveLebesgueDecomposition_smul_real
- MeasureTheory.SignedMeasure.singularPart_sub
- MeasureTheory.SignedMeasure.HaveLebesgueDecomposition.posPart
- MeasureTheory.SignedMeasure.rnDeriv_sub
- MeasureTheory.SignedMeasure.haveLebesgueDecomposition_smul
- MeasureTheory.SignedMeasure.haveLebesgueDecomposition_neg
- MeasureTheory.SignedMeasure.HaveLebesgueDecomposition.negPart
Ancestors0
No ancestors.