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.

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

def Iotop {R : Type u_1} [LinearOrder R] (a b : R) : Set R

Iotop a b is the interval Ioo a b if b is not top, and Ioc a b if b is top. This makes sure that any element which is not bot belongs to an interval Iotop a b, and also that these intervals are all open. These two properties together are important in the proof of StieltjesFunction.outer_Ioc.

Equations

• Iotop a b = if IsTop b then Set.Ioc a b else Set.Ioo a b

theorem Iotop_subset_Ioc {R : Type u_1} [LinearOrder R] {a b : R} : Iotop a b ⊆ Set.Ioc a b

theorem Ioo_subset_Iotop {R : Type u_1} [LinearOrder R] {a b : R} : Set.Ioo a b ⊆ Iotop a b

theorem isOpen_Iotop {R : Type u_1} [LinearOrder R] [TopologicalSpace R] [OrderTopology R] (a b : R) : IsOpen (Iotop a b)

def botSet {R : Type u_1} [LinearOrder R] : Set R

botSet is the set of all bottom elements.

Equations

• botSet = {x : R | IsBot x}

@[simp]

theorem Ioc_diff_botSet {R : Type u_1} [LinearOrder R] (a b : R) : Set.Ioc a b \ botSet = Set.Ioc a b

theorem notMem_botSet_of_lt {R : Type u_1} [LinearOrder R] {x y : R} (h : x < y) : y ∉ botSet

theorem subsingleton_botSet {R : Type u_1} [LinearOrder R] : botSet.Subsingleton

theorem measurableSet_botSet {R : Type u_1} [LinearOrder R] [MeasurableSpace R] [MeasurableSingletonClass R] : MeasurableSet botSet

theorem botSet_eq_singleton_of_isBot {R : Type u_1} [LinearOrder R] {x : R} (hx : IsBot x) : botSet = {x}

Basic properties of Stieltjes functions

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

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

• toFun : R → ℝ

  The underlying function R → ℝ.

  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} [LinearOrder R] [TopologicalSpace R] : CoeFun (StieltjesFunction R) fun (x : StieltjesFunction R) => R → ℝ

Equations

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

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

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

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

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

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

theorem StieltjesFunction.iInf_Ioi_eq {R : Type u_1} [LinearOrder R] [TopologicalSpace R] [OrderTopology R] [DenselyOrdered R] [NoMaxOrder R] (f : StieltjesFunction R) (x : R) : ⨅ (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) [LinearOrder R] [TopologicalSpace R] (c : ℝ) : StieltjesFunction R

A constant function is a Stieltjes function.

Equations

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

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

Equations

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

@[simp]

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

def StieltjesFunction.add {R : Type u_1} [LinearOrder 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} [LinearOrder 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} [LinearOrder 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} [LinearOrder 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} [LinearOrder R] [TopologicalSpace R] (x : R) : ↑0 x = 0

@[simp]

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

noncomputable def Monotone.stieltjesFunction {R : Type u_1} [LinearOrder 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 {R : Type u_1} [LinearOrder R] [TopologicalSpace R] [OrderTopology R] {f : R → ℝ} (hf : Monotone f) (x : R) : ↑hf.stieltjesFunction x = Function.rightLim f x

theorem StieltjesFunction.countable_leftLim_ne {R : Type u_1} [LinearOrder 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} [LinearOrder 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} [LinearOrder 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} [LinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) [IsEmpty R] (s : Set R) : f.length s = 0

@[simp]

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

@[simp]

theorem StieltjesFunction.length_Ioc {R : Type u_1} [LinearOrder 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} [LinearOrder 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} [LinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) {s : Set R} : f.length (s \ botSet) = f.length s

def StieltjesFunction.outer {R : Type u_1} [LinearOrder 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} [LinearOrder 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} [LinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) [OrderTopology R] [CompactIccSpace 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} [LinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) [OrderTopology R] [CompactIccSpace 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} [LinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) {c : R} : MeasurableSet (Set.Ioi c)

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

theorem StieltjesFunction.borel_le_measurable {R : Type u_1} [LinearOrder 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} [LinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) [OrderTopology R] [CompactIccSpace 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} [LinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) [OrderTopology R] [CompactIccSpace 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} [LinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) [OrderTopology R] [CompactIccSpace 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} [LinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) [OrderTopology R] [CompactIccSpace 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} [LinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) [OrderTopology R] [CompactIccSpace 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} [LinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) [OrderTopology R] [CompactIccSpace 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} [LinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) [OrderTopology R] [CompactIccSpace 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)

@[simp]

theorem StieltjesFunction.measure_botSet {R : Type u_1} [LinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) [OrderTopology R] [CompactIccSpace R] [MeasurableSpace R] [BorelSpace R] [SecondCountableTopology R] [DenselyOrdered R] : f.measure botSet = 0

theorem StieltjesFunction.measure_Iic {R : Type u_1} [LinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) [OrderTopology R] [CompactIccSpace R] [MeasurableSpace R] [BorelSpace R] [SecondCountableTopology R] [DenselyOrdered 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} [LinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) [OrderTopology R] [CompactIccSpace R] [MeasurableSpace R] [BorelSpace R] [SecondCountableTopology R] [DenselyOrdered 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} [LinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) [OrderTopology R] [CompactIccSpace R] [MeasurableSpace R] [BorelSpace R] [SecondCountableTopology R] [DenselyOrdered 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} [LinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) [OrderTopology R] [CompactIccSpace R] [MeasurableSpace R] [BorelSpace R] [SecondCountableTopology R] [DenselyOrdered 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} [LinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) [OrderTopology R] [CompactIccSpace 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} [LinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) [OrderTopology R] [CompactIccSpace 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} [LinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) [OrderTopology R] [CompactIccSpace 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} [LinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) [OrderTopology R] [CompactIccSpace R] [MeasurableSpace R] [BorelSpace R] [SecondCountableTopology R] [DenselyOrdered R] (hf : Filter.Tendsto (↑f) Filter.atBot Filter.atBot) (x : R) : f.measure (Set.Iio x) = ⊤

theorem StieltjesFunction.measure_univ {R : Type u_1} [LinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) [OrderTopology R] [CompactIccSpace R] [MeasurableSpace R] [BorelSpace R] [SecondCountableTopology R] [DenselyOrdered R] [Nonempty 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} [LinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) [OrderTopology R] [CompactIccSpace 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} [LinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) [OrderTopology R] [CompactIccSpace R] [MeasurableSpace R] [BorelSpace R] [SecondCountableTopology R] [DenselyOrdered R] [Nonempty R] (hf : Filter.Tendsto (↑f) Filter.atBot Filter.atBot) : f.measure Set.univ = ⊤

theorem StieltjesFunction.isFiniteMeasure {R : Type u_1} [LinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) [OrderTopology R] [CompactIccSpace R] [MeasurableSpace R] [BorelSpace R] [SecondCountableTopology R] [DenselyOrdered 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.isFiniteMeasure_of_forall_abs_le {R : Type u_1} [LinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) [OrderTopology R] [CompactIccSpace R] [MeasurableSpace R] [BorelSpace R] [SecondCountableTopology R] [DenselyOrdered R] {C : ℝ} (h : ∀ (x : R), |↑f x| ≤ C) : MeasureTheory.IsFiniteMeasure f.measure

theorem StieltjesFunction.isProbabilityMeasure {R : Type u_1} [LinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) [OrderTopology R] [CompactIccSpace R] [MeasurableSpace R] [BorelSpace R] [SecondCountableTopology R] [DenselyOrdered R] [Nonempty 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} [LinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) [OrderTopology R] [CompactIccSpace 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} [LinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) [OrderTopology R] [CompactIccSpace R] [MeasurableSpace R] [BorelSpace R] [SecondCountableTopology R] [DenselyOrdered 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} [LinearOrder R] [TopologicalSpace R] (f : StieltjesFunction R) [OrderTopology R] [CompactIccSpace 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} [LinearOrder R] [TopologicalSpace R] [OrderTopology R] [CompactIccSpace 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} [LinearOrder R] [TopologicalSpace R] [OrderTopology R] [CompactIccSpace R] [MeasurableSpace R] [BorelSpace R] [SecondCountableTopology R] [DenselyOrdered R] : StieltjesFunction.measure 0 = 0

@[simp]

theorem StieltjesFunction.measure_add {R : Type u_1} [LinearOrder R] [TopologicalSpace R] [OrderTopology R] [CompactIccSpace 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} [LinearOrder R] [TopologicalSpace R] [OrderTopology R] [CompactIccSpace R] [MeasurableSpace R] [BorelSpace R] [SecondCountableTopology R] [DenselyOrdered R] (c : NNReal) (f : StieltjesFunction R) : (c • f).measure = c • f.measure