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

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

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

Instances For

source

theorem StieltjesFunction.mono' (self : StieltjesFunction) :

Monotone ↑self

source

theorem StieltjesFunction.right_continuous' (self : StieltjesFunction) (x : ℝ) :

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

source

instance StieltjesFunction.instCoeFun :

CoeFun StieltjesFunction fun (x : StieltjesFunction) => ℝ → ℝ

Equations

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

source

theorem StieltjesFunction.ext_iff {f : StieltjesFunction} {g : StieltjesFunction} :

f = g ↔ ∀ (x : ℝ), ↑f x = ↑g x

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

def StieltjesFunction.const (c : ℝ) :

StieltjesFunction

Constant functions are Stieltjes function.

Equations

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

Instances For

source

@[simp]

theorem StieltjesFunction.const_apply (c : ℝ) (x : ℝ) :

↑(StieltjesFunction.const c) x = c

source

def StieltjesFunction.add (f : StieltjesFunction) (g : StieltjesFunction) :

StieltjesFunction

The sum of two Stieltjes functions is a Stieltjes function.

Equations

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

Instances For

source

instance StieltjesFunction.instAddZeroClass :

AddZeroClass StieltjesFunction

Equations

StieltjesFunction.instAddZeroClass = AddZeroClass.mk StieltjesFunction.instAddZeroClass.proof_1 StieltjesFunction.instAddZeroClass.proof_2

source

instance StieltjesFunction.instAddCommMonoid :

AddCommMonoid StieltjesFunction

Equations

StieltjesFunction.instAddCommMonoid = AddCommMonoid.mk StieltjesFunction.instAddCommMonoid.proof_4

source

instance StieltjesFunction.instModuleNNReal :

Module NNReal StieltjesFunction

Equations

StieltjesFunction.instModuleNNReal = Module.mk StieltjesFunction.instModuleNNReal.proof_7 StieltjesFunction.instModuleNNReal.proof_8

source

@[simp]

theorem StieltjesFunction.add_apply (f : StieltjesFunction) (g : StieltjesFunction) (x : ℝ) :

↑(f + g) x = ↑f x + ↑g x

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

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

Instances For

source

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

↑hf.stieltjesFunction x = Function.rightLim f x

source

theorem StieltjesFunction.countable_leftLim_ne (f : StieltjesFunction) :

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

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

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

Instances For

source

@[simp]

theorem StieltjesFunction.length_empty (f : StieltjesFunction) :

f.length ∅ = 0

source

@[simp]

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

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

source

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

f.length s₁ ≤ f.length s₂

source

def StieltjesFunction.outer (f : StieltjesFunction) :

MeasureTheory.OuterMeasure ℝ

The Stieltjes outer measure associated to a Stieltjes function.

Equations

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

Instances For

source

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

f.outer s ≤ f.length 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]