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].

Main definitions #

StieltjesFunction is a structure containing a function from ℝ → ℝ, together with the assertions that it is monotone and right-continuous. To f : StieltjesFunction, 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.

Basic properties of Stieltjes functions #

source

structure StieltjesFunction :

Type

toFun : ℝ → ℝ
mono' : Monotone ↑s
right_continuous' : ∀ (x : ℝ), ContinuousWithinAt (↑s) (Set.Ici x) x

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

Instances For

source

instance StieltjesFunction.instCoeFun :

CoeFun StieltjesFunction fun x => ℝ → ℝ

Equations

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

source

theorem StieltjesFunction.ext {f : StieltjesFunction} {g : StieltjesFunction} (h : ∀ (x : ℝ), ↑f x = ↑g x) :

f = g

source

theorem StieltjesFunction.mono (f : StieltjesFunction) :

Monotone ↑f

source

theorem StieltjesFunction.right_continuous (f : StieltjesFunction) (x : ℝ) :

ContinuousWithinAt (↑f) (Set.Ici x) x

source

theorem StieltjesFunction.rightLim_eq (f : StieltjesFunction) (x : ℝ) :

Function.rightLim (↑f) x = ↑f x

source

theorem StieltjesFunction.iInf_Ioi_eq (f : StieltjesFunction) (x : ℝ) :

⨅ (r : ↑(Set.Ioi x)), ↑f ↑r = ↑f x

source

theorem StieltjesFunction.iInf_rat_gt_eq (f : StieltjesFunction) (x : ℝ) :

⨅ (r : { r' // x < ↑r' }), ↑f ↑↑r = ↑f x

source

@[simp]

theorem StieltjesFunction.id_apply (a : ℝ) :

↑StieltjesFunction.id a = id a

source

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 }

Instances For

source

@[simp]

theorem StieltjesFunction.id_leftLim (x : ℝ) :

Function.leftLim (↑StieltjesFunction.id) x = x

source

instance StieltjesFunction.instInhabited :

Inhabited StieltjesFunction

Equations

StieltjesFunction.instInhabited = { default := StieltjesFunction.id }

source

noncomputable def Monotone.stieltjesFunction {f : ℝ → ℝ} (hf : Monotone f) :

StieltjesFunction

If a function f : ℝ → ℝ 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

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

Instances For

source

theorem Monotone.stieltjesFunction_eq {f : ℝ → ℝ} (hf : Monotone f) (x : ℝ) :

↑(Monotone.stieltjesFunction hf) x = Function.rightLim f x

source

theorem StieltjesFunction.countable_leftLim_ne (f : StieltjesFunction) :

Set.Countable {x | Function.leftLim (↑f) x ≠ ↑f x}

The outer measure associated to a Stieltjes function #

source

def StieltjesFunction.length (f : StieltjesFunction) (s : Set ℝ) :

ENNReal

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

Equations

StieltjesFunction.length f s = ⨅ (a : ℝ) (b : ℝ) (_ : s ⊆ Set.Ioc a b), ENNReal.ofReal (↑f b - ↑f a)

Instances For

source

@[simp]

theorem StieltjesFunction.length_empty (f : StieltjesFunction) :

StieltjesFunction.length f ∅ = 0

source

@[simp]

theorem StieltjesFunction.length_Ioc (f : StieltjesFunction) (a : ℝ) (b : ℝ) :

StieltjesFunction.length f (Set.Ioc a b) = ENNReal.ofReal (↑f b - ↑f a)

source

theorem StieltjesFunction.length_mono (f : StieltjesFunction) {s₁ : Set ℝ} {s₂ : Set ℝ} (h : s₁ ⊆ s₂) :

StieltjesFunction.length f s₁ ≤ StieltjesFunction.length f s₂

source

def StieltjesFunction.outer (f : StieltjesFunction) :

MeasureTheory.OuterMeasure ℝ

The Stieltjes outer measure associated to a Stieltjes function.

Equations

StieltjesFunction.outer f = MeasureTheory.OuterMeasure.ofFunction (StieltjesFunction.length f) (_ : StieltjesFunction.length f ∅ = 0)

Instances For

source

theorem StieltjesFunction.outer_le_length (f : StieltjesFunction) (s : Set ℝ) :

↑(StieltjesFunction.outer f) s ≤ StieltjesFunction.length f s

source

theorem StieltjesFunction.length_subadditive_Icc_Ioo (f : StieltjesFunction) {a : ℝ} {b : ℝ} {c : ℕ → ℝ} {d : ℕ → ℝ} (ss : Set.Icc a b ⊆ ⋃ (i : ℕ), Set.Ioo (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.

source

@[simp]