Stieltjes measures on the real line

Consider a function f : ℝ → ℝ which is monotone and right-continuous. Then one can define a corresponding measure, giving mass f b - f a to the interval (a, b]. We implement more generally this notion for f : R → ℝ where R is a conditionally complete dense linear order.

Main definitions

• StieltjesFunction R is a structure containing a function from R → ℝ, together with the assertions that it is monotone and right-continuous. To f : StieltjesFunction R, one associates a Borel measure f.measure.
• f.measure_Ioc asserts that f.measure (Ioc a b) = ofReal (f b - f a)
• f.measure_Ioo asserts that f.measure (Ioo a b) = ofReal (leftLim f b - f a).
• f.measure_Icc and f.measure_Ico are analogous.
• Monotone.stieltjesFunction: to a monotone function f, associate the Stieltjes function equal to the right limit of f. This makes it possible to associate a Stieltjes measure to any monotone function.

Implementation

We define Stieltjes functions over any conditionally complete dense linear order, to be able to cover the cases of ℝ≥0 and [0, T] in addition to the classical case of ℝ. This creates a few issues, mostly with the management of bottom and top elements. To handle these, we need two technical definitions:

• Iotop a b is the interval Ioo a b if b is not top, and Ioc a b if b is top.
• botSet is the empty set if there is no bot element, and {x} if x is bot.

These definitions are just handy tools for some proofs of this file, so they are only included there, and not exported.

Note that the theory of Stieltjes measures is not completely satisfactory when there is a bot element x: any Stieljes measure gives zero mass to {x} in this case, so the Dirac mass at x is not representable as a Stieljes measure.

Basic properties of Stieltjes functions

structure StieltjesFunction (R : Type u_1) [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] : Type u_1

Bundled monotone right-continuous real functions, used to construct Stieltjes measures.

• toFun : R → ℝ

  The underlying function ℝ → ℝ.

  Do NOT use directly. Use the coercion instead.

• mono' : Monotone ↑self
• right_continuous' (x : R) : ContinuousWithinAt (↑self) (Set.Ici x) x

instance StieltjesFunction.instCoeFun {R : Type u_1} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] : CoeFun (StieltjesFunction R) fun (x : StieltjesFunction R) => R → ℝ

Equations

• StieltjesFunction.instCoeFun = { coe := StieltjesFunction.toFun }

theorem StieltjesFunction.ext {R : Type u_1} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] {f g : StieltjesFunction R} (h : ∀ (x : R), ↑f x = ↑g x) : f = g

theorem StieltjesFunction.ext_iff {R : Type u_1} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] {f g : StieltjesFunction R} : f = g ↔ ∀ (x : R), ↑f x = ↑g x

theorem StieltjesFunction.mono {R : Type u_1} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) : Monotone ↑f

theorem StieltjesFunction.right_continuous {R : Type u_1} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) (x : R) : ContinuousWithinAt (↑f) (Set.Ici x) x

theorem StieltjesFunction.rightLim_eq {R : Type u_1} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] (f : StieltjesFunction R) (x : R) : Function.rightLim (↑f) x = ↑f x

theorem StieltjesFunction.iInf_Ioi_eq (f : StieltjesFunction ℝ) (x : ℝ) : ⨅ (r : ↑(Set.Ioi x)), ↑f ↑r = ↑f x

theorem StieltjesFunction.iInf_rat_gt_eq (f : StieltjesFunction ℝ) (x : ℝ) : ⨅ (r : { r' : ℚ // x < ↑r' }), ↑f ↑↑r = ↑f x

def StieltjesFunction.id : StieltjesFunction ℝ

The identity of ℝ as a Stieltjes function, used to construct Lebesgue measure.

Equations

• StieltjesFunction.id = { toFun := id, mono' := StieltjesFunction.id._proof_1, right_continuous' := StieltjesFunction.id._proof_2 }

@[simp]

theorem StieltjesFunction.id_apply (a : ℝ) : ↑StieltjesFunction.id a = id a

@[simp]

theorem StieltjesFunction.id_leftLim (x : ℝ) : Function.leftLim (↑StieltjesFunction.id) x = x

def StieltjesFunction.const (R : Type u_1) [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] (c : ℝ) : StieltjesFunction R

Constant functions are Stieltjes function.

Equations

• StieltjesFunction.const R c = { toFun := fun (x : R) => c, mono' := ⋯, right_continuous' := ⋯ }

instance StieltjesFunction.instInhabited {R : Type u_1} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] : Inhabited (StieltjesFunction R)

Equations

• StieltjesFunction.instInhabited = { default := StieltjesFunction.const R 0 }

@[simp]

theorem StieltjesFunction.const_apply {R : Type u_1} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] (c : ℝ) (x : R) : ↑(StieltjesFunction.const R c) x = c

def StieltjesFunction.add {R : Type u_1} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] (f g : StieltjesFunction R) : StieltjesFunction R

The sum of two Stieltjes functions is a Stieltjes function.

Equations

• f.add g = { toFun := fun (x : R) => ↑f x + ↑g x, mono' := ⋯, right_continuous' := ⋯ }

instance StieltjesFunction.instAddZeroClass {R : Type u_1} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] : AddZeroClass (StieltjesFunction R)

Equations

• StieltjesFunction.instAddZeroClass = { zero := StieltjesFunction.const R 0, add := StieltjesFunction.add, zero_add := ⋯, add_zero := ⋯ }

instance StieltjesFunction.instAddCommMonoid {R : Type u_1} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] : AddCommMonoid (StieltjesFunction R)

Equations

• One or more equations did not get rendered due to their size.

instance StieltjesFunction.instModuleNNReal {R : Type u_1} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] : Module NNReal (StieltjesFunction R)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem StieltjesFunction.zero_apply {R : Type u_1} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] (x : R) : ↑0 x = 0

@[simp]

theorem StieltjesFunction.add_apply {R : Type u_1} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] (f g : StieltjesFunction R) (x : R) : ↑(f + g) x = ↑f x + ↑g x

noncomputable def Monotone.stieltjesFunction {R : Type u_1} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] {f : R → ℝ} (hf : Monotone f) : StieltjesFunction R

If a function f : R → ℝ is monotone, then the function mapping x to the right limit of f at x is a Stieltjes function, i.e., it is monotone and right-continuous.

Equations

• hf.stieltjesFunction = { toFun := Function.rightLim f, mono' := ⋯, right_continuous' := ⋯ }

theorem Monotone.stieltjesFunction_eq {f : ℝ → ℝ} (hf : Monotone f) (x : ℝ) : ↑hf.stieltjesFunction x = Function.rightLim f x

theorem StieltjesFunction.countable_leftLim_ne {R : Type u_1} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] (f : StieltjesFunction R) : {x : R | Function.leftLim (↑f) x ≠ ↑f x}.Countable

The outer measure associated to a Stieltjes function

def StieltjesFunction.length {R : Type u_1} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) (s : Set R) : ENNReal

Length of an interval. This is the largest monotone function which correctly measures all intervals.

Equations

• f.length s = if IsEmpty R then 0 else ⨅ (a : R), ⨅ (b : R), ⨅ (_ : s \ botSet✝ ⊆ Set.Ioc a b), ENNReal.ofReal (↑f b - ↑f a)

theorem StieltjesFunction.length_eq {R : Type u_1} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) [Nonempty R] (s : Set R) : f.length s = ⨅ (a : R), ⨅ (b : R), ⨅ (_ : s \ botSet✝ ⊆ Set.Ioc a b), ENNReal.ofReal (↑f b - ↑f a)

theorem StieltjesFunction.length_eq_of_isEmpty {R : Type u_1} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) [IsEmpty R] (s : Set R) : f.length s = 0

@[simp]

theorem StieltjesFunction.length_empty {R : Type u_1} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) : f.length ∅ = 0

@[simp]

theorem StieltjesFunction.length_Ioc {R : Type u_1} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) (a b : R) : f.length (Set.Ioc a b) = ENNReal.ofReal (↑f b - ↑f a)

theorem StieltjesFunction.length_mono {R : Type u_1} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) {s₁ s₂ : Set R} (h : s₁ ⊆ s₂) : f.length s₁ ≤ f.length s₂

theorem StieltjesFunction.length_diff_botSet {R : Type u_1} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) {s : Set R} : f.length (s \ botSet✝) = f.length s

def StieltjesFunction.outer {R : Type u_1} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) : MeasureTheory.OuterMeasure R

The Stieltjes outer measure associated to a Stieltjes function.

Equations

• f.outer = MeasureTheory.OuterMeasure.ofFunction f.length ⋯

theorem StieltjesFunction.outer_le_length {R : Type u_1} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) (s : Set R) : f.outer s ≤ f.length s

theorem StieltjesFunction.length_subadditive_Icc_Ioo {R : Type u_1} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) [OrderTopology R] {a b : R} {c d : ℕ → R} (ss : Set.Icc a b ⊆ ⋃ (i : ℕ), Iotop✝ (c i) (d i)) : ENNReal.ofReal (↑f b - ↑f a) ≤ ∑' (i : ℕ), ENNReal.ofReal (↑f (d i) - ↑f (c i))

If a compact interval [a, b] is covered by a union of open interval (c i, d i), then f b - f a ≤ ∑ f (d i) - f (c i). This is an auxiliary technical statement to prove the same statement for half-open intervals, the point of the current statement being that one can use compactness to reduce it to a finite sum, and argue by induction on the size of the covering set.

To be able to handle also the top element if there is one, we use Iotop instead of Ioo in the statement. As these intervals are all open, this does not change the proof.

@[simp]

theorem StieltjesFunction.outer_Ioc {R : Type u_1} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) [OrderTopology R] [DenselyOrdered R] (a b : R) : f.outer (Set.Ioc a b) = ENNReal.ofReal (↑f b - ↑f a)

theorem StieltjesFunction.measurableSet_Ioi {R : Type u_1} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) {c : R} : MeasurableSet (Set.Ioi c)

theorem StieltjesFunction.outer_trim {R : Type u_1} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) [OrderTopology R] [MeasurableSpace R] [BorelSpace R] [DenselyOrdered R] : f.outer.trim = f.outer

theorem StieltjesFunction.borel_le_measurable {R : Type u_1} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) [OrderTopology R] [SecondCountableTopology R] : borel R ≤ f.outer.caratheodory

The measure associated to a Stieltjes function

@[irreducible]

def StieltjesFunction.measure {R : Type u_2} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) [OrderTopology R] [MeasurableSpace R] [BorelSpace R] [SecondCountableTopology R] [DenselyOrdered R] : MeasureTheory.Measure R

The measure associated to a Stieltjes function, giving mass f b - f a to the interval (a, b]. If there is a bot element, it gives zero mass to it.

Equations

• f.measure = let __OuterMeasure := f.outer; { toOuterMeasure := __OuterMeasure, m_iUnion := ⋯, trim_le := ⋯ }

theorem StieltjesFunction.measure_def {R : Type u_2} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) [OrderTopology R] [MeasurableSpace R] [BorelSpace R] [SecondCountableTopology R] [DenselyOrdered R] : f.measure = let __OuterMeasure := f.outer; { toOuterMeasure := __OuterMeasure, m_iUnion := ⋯, trim_le := ⋯ }

@[simp]

theorem StieltjesFunction.measure_Ioc {R : Type u_1} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) [OrderTopology R] [MeasurableSpace R] [BorelSpace R] [SecondCountableTopology R] [DenselyOrdered R] (a b : R) : f.measure (Set.Ioc a b) = ENNReal.ofReal (↑f b - ↑f a)

@[simp]

theorem StieltjesFunction.measure_singleton {R : Type u_1} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) [OrderTopology R] [MeasurableSpace R] [BorelSpace R] [SecondCountableTopology R] [DenselyOrdered R] (a : R) : f.measure {a} = ENNReal.ofReal (↑f a - Function.leftLim (↑f) a)

@[simp]

theorem StieltjesFunction.measure_Icc {R : Type u_1} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) [OrderTopology R] [MeasurableSpace R] [BorelSpace R] [SecondCountableTopology R] [DenselyOrdered R] (a b : R) : f.measure (Set.Icc a b) = ENNReal.ofReal (↑f b - Function.leftLim (↑f) a)

@[simp]

theorem StieltjesFunction.measure_Ioo {R : Type u_1} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) [OrderTopology R] [MeasurableSpace R] [BorelSpace R] [SecondCountableTopology R] [DenselyOrdered R] {a b : R} : f.measure (Set.Ioo a b) = ENNReal.ofReal (Function.leftLim (↑f) b - ↑f a)

@[simp]

theorem StieltjesFunction.measure_Ico {R : Type u_1} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) [OrderTopology R] [MeasurableSpace R] [BorelSpace R] [SecondCountableTopology R] [DenselyOrdered R] (a b : R) : f.measure (Set.Ico a b) = ENNReal.ofReal (Function.leftLim (↑f) b - Function.leftLim (↑f) a)

theorem StieltjesFunction.measure_Iic {R : Type u_1} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) [OrderTopology R] [MeasurableSpace R] [BorelSpace R] [SecondCountableTopology R] [DenselyOrdered R] [NoMinOrder R] {l : ℝ} (hf : Filter.Tendsto (↑f) Filter.atBot (nhds l)) (x : R) : f.measure (Set.Iic x) = ENNReal.ofReal (↑f x - l)

theorem StieltjesFunction.measure_Iio {R : Type u_1} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) [OrderTopology R] [MeasurableSpace R] [BorelSpace R] [SecondCountableTopology R] [DenselyOrdered R] [NoMinOrder R] {l : ℝ} (hf : Filter.Tendsto (↑f) Filter.atBot (nhds l)) (x : R) : f.measure (Set.Iio x) = ENNReal.ofReal (Function.leftLim (↑f) x - l)

theorem StieltjesFunction.measure_Ici {R : Type u_1} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) [OrderTopology R] [MeasurableSpace R] [BorelSpace R] [SecondCountableTopology R] [DenselyOrdered R] [NoMaxOrder R] {l : ℝ} (hf : Filter.Tendsto (↑f) Filter.atTop (nhds l)) (x : R) : f.measure (Set.Ici x) = ENNReal.ofReal (l - Function.leftLim (↑f) x)

theorem StieltjesFunction.measure_Ioi {R : Type u_1} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) [OrderTopology R] [MeasurableSpace R] [BorelSpace R] [SecondCountableTopology R] [DenselyOrdered R] [NoMaxOrder R] {l : ℝ} (hf : Filter.Tendsto (↑f) Filter.atTop (nhds l)) (x : R) : f.measure (Set.Ioi x) = ENNReal.ofReal (l - ↑f x)

theorem StieltjesFunction.measure_Ioi_of_tendsto_atTop_atTop {R : Type u_1} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) [OrderTopology R] [MeasurableSpace R] [BorelSpace R] [SecondCountableTopology R] [DenselyOrdered R] (hf : Filter.Tendsto (↑f) Filter.atTop Filter.atTop) (x : R) : f.measure (Set.Ioi x) = ⊤

theorem StieltjesFunction.measure_Ici_of_tendsto_atTop_atTop {R : Type u_1} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) [OrderTopology R] [MeasurableSpace R] [BorelSpace R] [SecondCountableTopology R] [DenselyOrdered R] (hf : Filter.Tendsto (↑f) Filter.atTop Filter.atTop) (x : R) : f.measure (Set.Ici x) = ⊤

theorem StieltjesFunction.measure_Iic_of_tendsto_atBot_atBot {R : Type u_1} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) [OrderTopology R] [MeasurableSpace R] [BorelSpace R] [SecondCountableTopology R] [DenselyOrdered R] (hf : Filter.Tendsto (↑f) Filter.atBot Filter.atBot) (x : R) : f.measure (Set.Iic x) = ⊤

theorem StieltjesFunction.measure_Iio_of_tendsto_atBot_atBot {R : Type u_1} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) [OrderTopology R] [MeasurableSpace R] [BorelSpace R] [SecondCountableTopology R] [DenselyOrdered R] [NoMinOrder R] (hf : Filter.Tendsto (↑f) Filter.atBot Filter.atBot) (x : R) : f.measure (Set.Iio x) = ⊤

theorem StieltjesFunction.measure_univ {R : Type u_1} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) [OrderTopology R] [MeasurableSpace R] [BorelSpace R] [SecondCountableTopology R] [DenselyOrdered R] [NoMinOrder R] {l u : ℝ} (hfl : Filter.Tendsto (↑f) Filter.atBot (nhds l)) (hfu : Filter.Tendsto (↑f) Filter.atTop (nhds u)) : f.measure Set.univ = ENNReal.ofReal (u - l)

theorem StieltjesFunction.measure_univ_of_tendsto_atTop_atTop {R : Type u_1} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) [OrderTopology R] [MeasurableSpace R] [BorelSpace R] [SecondCountableTopology R] [DenselyOrdered R] [Nonempty R] (hf : Filter.Tendsto (↑f) Filter.atTop Filter.atTop) : f.measure Set.univ = ⊤

theorem StieltjesFunction.measure_univ_of_tendsto_atBot_atBot {R : Type u_1} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) [OrderTopology R] [MeasurableSpace R] [BorelSpace R] [SecondCountableTopology R] [DenselyOrdered R] [Nonempty R] [NoMinOrder R] (hf : Filter.Tendsto (↑f) Filter.atBot Filter.atBot) : f.measure Set.univ = ⊤

theorem StieltjesFunction.isFiniteMeasure {R : Type u_1} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) [OrderTopology R] [MeasurableSpace R] [BorelSpace R] [SecondCountableTopology R] [DenselyOrdered R] [NoMinOrder R] {l u : ℝ} (hfl : Filter.Tendsto (↑f) Filter.atBot (nhds l)) (hfu : Filter.Tendsto (↑f) Filter.atTop (nhds u)) : MeasureTheory.IsFiniteMeasure f.measure

theorem StieltjesFunction.isProbabilityMeasure {R : Type u_1} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) [OrderTopology R] [MeasurableSpace R] [BorelSpace R] [SecondCountableTopology R] [DenselyOrdered R] [NoMinOrder R] (hf_bot : Filter.Tendsto (↑f) Filter.atBot (nhds 0)) (hf_top : Filter.Tendsto (↑f) Filter.atTop (nhds 1)) : MeasureTheory.IsProbabilityMeasure f.measure

instance StieltjesFunction.instIsLocallyFiniteMeasure {R : Type u_1} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) [OrderTopology R] [MeasurableSpace R] [BorelSpace R] [SecondCountableTopology R] [DenselyOrdered R] : MeasureTheory.IsLocallyFiniteMeasure f.measure

theorem StieltjesFunction.eq_of_measure_of_tendsto_atBot {R : Type u_1} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) [OrderTopology R] [MeasurableSpace R] [BorelSpace R] [SecondCountableTopology R] [DenselyOrdered R] [NoMinOrder R] (g : StieltjesFunction R) {l : ℝ} (hfg : f.measure = g.measure) (hfl : Filter.Tendsto (↑f) Filter.atBot (nhds l)) (hgl : Filter.Tendsto (↑g) Filter.atBot (nhds l)) : f = g

theorem StieltjesFunction.eq_of_measure_of_eq {R : Type u_1} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) [OrderTopology R] [MeasurableSpace R] [BorelSpace R] [SecondCountableTopology R] [DenselyOrdered R] (g : StieltjesFunction R) {y : R} (hfg : f.measure = g.measure) (hy : ↑f y = ↑g y) : f = g

@[simp]

theorem StieltjesFunction.measure_const {R : Type u_1} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] [MeasurableSpace R] [BorelSpace R] [SecondCountableTopology R] [DenselyOrdered R] (c : ℝ) : (StieltjesFunction.const R c).measure = 0

@[simp]

theorem StieltjesFunction.measure_zero {R : Type u_1} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] [MeasurableSpace R] [BorelSpace R] [SecondCountableTopology R] [DenselyOrdered R] : StieltjesFunction.measure 0 = 0

@[simp]

theorem StieltjesFunction.measure_add {R : Type u_1} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] [MeasurableSpace R] [BorelSpace R] [SecondCountableTopology R] [DenselyOrdered R] (f g : StieltjesFunction R) : (f + g).measure = f.measure + g.measure

@[simp]

theorem StieltjesFunction.measure_smul {R : Type u_1} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] [MeasurableSpace R] [BorelSpace R] [SecondCountableTopology R] [DenselyOrdered R] (c : NNReal) (f : StieltjesFunction R) : (c • f).measure = c • f.measure