Theorems · Definition · measure theory

BoundedVariationOn.stieltjesFunctionRightLim

{α : Type u_1} →
  [inst : LinearOrder α] →
    [inst_1 : TopologicalSpace α] →
      [OrderTopology α] →
        {E : Type u_2} →
          [inst_3 : NormedAddCommGroup E] →
            [CompleteSpace E] → {f : α → E} → BoundedVariationOn f Set.univ → α → StieltjesFunction α

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.

Defined in

Mathlib.MeasureTheory.VectorMeasure.BoundedVariation

Cited by

2 results in Mathlib

Foundations

Depth 165 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

LinearOrderTopologicalSpaceOrderTopologyNormedAddCommGroupCompleteSpace