Stieltjes measures on the real line #

Consider a function f : ℝ → ℝ which is monotone and right-continuous. Then one can define a corrresponding measure, giving mass f b - f a to the interval (a, b].

Main definitions #

stieltjes_function is a structure containing a function from ℝ → ℝ, together with the assertions that it is monotone and right-continuous. To f : stieltjes_function, one associates a Borel measure f.measure.
f.measure_Ioc asserts that f.measure (Ioc a b) = of_real (f b - f a)
f.measure_Ioo asserts that f.measure (Ioo a b) = of_real (left_lim f b - f a).
f.measure_Icc and f.measure_Ico are analogous.

Basic properties of Stieltjes functions #

source

structure stieltjes_function :

Type

to_fun : ℝ → ℝ
mono' : monotone self.to_fun
right_continuous' : ∀ (x : ℝ), continuous_within_at self.to_fun (set.Ici x) x

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

Instances for stieltjes_function

source

@[protected, instance]

def stieltjes_function.has_coe_to_fun :

has_coe_to_fun stieltjes_function (λ (_x : stieltjes_function), ℝ → ℝ)

Equations

stieltjes_function.has_coe_to_fun = {coe := stieltjes_function.to_fun}

source

theorem stieltjes_function.mono (f : stieltjes_function) :

monotone ⇑f

source

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

continuous_within_at ⇑f (set.Ici x) x

source

@[simp]

theorem stieltjes_function.id_apply (a : ℝ) :

⇑stieltjes_function.id a = id a

source

@[protected]

def stieltjes_function.id :

stieltjes_function

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

Equations

stieltjes_function.id = {to_fun := id ℝ, mono' := stieltjes_function.id._proof_1, right_continuous' := stieltjes_function.id._proof_2}

source

@[simp]

theorem stieltjes_function.id_left_lim (x : ℝ) :

function.left_lim ⇑stieltjes_function.id x = x

source

@[protected, instance]

def stieltjes_function.inhabited :

inhabited stieltjes_function

Equations

stieltjes_function.inhabited = {default := stieltjes_function.id}

source

noncomputable def monotone.stieltjes_function {f : ℝ → ℝ} (hf : monotone f) :

stieltjes_function

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.stieltjes_function = {to_fun := function.right_lim f, mono' := _, right_continuous' := _}

source

theorem monotone.stieltjes_function_eq {f : ℝ → ℝ} (hf : monotone f) (x : ℝ) :

⇑(hf.stieltjes_function) x = function.right_lim f x

source

theorem stieltjes_function.countable_left_lim_ne (f : stieltjes_function) :

{x : ℝ | function.left_lim ⇑f x ≠ ⇑f x}.countable

The outer measure associated to a Stieltjes function #

source

noncomputable def stieltjes_function.length (f : stieltjes_function) (s : set ℝ) :

ennreal

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

Equations

f.length s = ⨅ (a b : ℝ) (h : s ⊆ set.Ioc a b), ennreal.of_real (⇑f b - ⇑f a)

source

@[simp]

theorem stieltjes_function.length_empty (f : stieltjes_function) :

f.length ∅ = 0

source

@[simp]

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

f.length (set.Ioc a b) = ennreal.of_real (⇑f b - ⇑f a)

source

theorem stieltjes_function.length_mono (f : stieltjes_function) {s₁ s₂ : set ℝ} (h : s₁ ⊆ s₂) :

f.length s₁ ≤ f.length s₂

source

@[protected]

noncomputable def stieltjes_function.outer (f : stieltjes_function) :

measure_theory.outer_measure ℝ

The Stieltjes outer measure associated to a Stieltjes function.

Equations

f.outer = measure_theory.outer_measure.of_function f.length _

source

theorem stieltjes_function.outer_le_length (f : stieltjes_function) (s : set ℝ) :

⇑(f.outer) s ≤ f.length s

source

theorem stieltjes_function.length_subadditive_Icc_Ioo (f : stieltjes_function) {a b : ℝ} {c d : ℕ → ℝ} (ss : set.Icc a b ⊆ ⋃ (i : ℕ), set.Ioo (c i) (d i)) :

ennreal.of_real (⇑f b - ⇑f a) ≤ ∑' (i : ℕ), ennreal.of_real (⇑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]

theorem stieltjes_function.outer_Ioc (f : stieltjes_function) (a b : ℝ) :

⇑(f.outer) (set.Ioc a b) = ennreal.of_real (⇑f b - ⇑f a)

source

theorem stieltjes_function.measurable_set_Ioi (f : stieltjes_function) {c : ℝ} :

measurable_set (set.Ioi c)

source

theorem stieltjes_function.outer_trim (f : stieltjes_function) :

f.outer.trim = f.outer

source

theorem stieltjes_function.borel_le_measurable (f : stieltjes_function) :