Vector valued Stieltjes measure associated to a bounded variation function #
Let α be a dense linear order with compact segments (e.g. ℝ or ℝ≥0), and f : α → E a
bounded variation function taking values in a complete additive normed group.
We associate to f a vector measure, called BoundedVariationOn.vectorMeasure. It gives
mass f.rightLim b - f.leftLim a to the interval [a, b] (with similar formulas for
other types of intervals).
For the construction, we define first an additive content on the set semiring of open-closed
intervals (a, b], mapping this interval to f.rightLim b - f.rightLim a. To extend this content
to the whole sigma-algebra, by general extension theorems, it is enough to show that it is
dominated by a finite measure. For this, we can use the Stieltjes measure associated to the
variation of f.rightLim. The extension we get is not exactly the desired vector measure, as we
need to tweak things if there is a bot element a: the previous vector measure gives to {a} the
mass 0 instead of the desired f.rightLim a - f a, so we add a Dirac mass to correct this defect.
The Stieltjes function associated to a bounded variation function. It is given by
the variation of the function f.rightLim from a fixed base point.
Using right limits ensures the right continuity, which is used to construct Stieltjes measures.
Equations
- hf.stieltjesFunctionRightLim x₀ = { toFun := fun (x : α) => variationOnFromTo (Function.rightLim f) Set.univ x₀ x, mono' := ⋯, right_continuous' := ⋯ }
Instances For
The vector measure associated to a bounded variation function f, giving mass
f.rightLim b - f.leftLim a to closed intervals [a, b], and similarly for other intervals.
Equations
- hf.vectorMeasure = ⋯.choose + if h : ∃ (x : α), IsBot x then MeasureTheory.VectorMeasure.dirac h.choose (Function.rightLim f h.choose - f h.choose) else 0