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

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

instance StieltjesFunction.instCoeFun : CoeFun StieltjesFunction fun (x : StieltjesFunction) => ℝ → ℝ

Equations

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

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

theorem StieltjesFunction.mono (f : StieltjesFunction) : Monotone ↑f

theorem StieltjesFunction.right_continuous (f : StieltjesFunction) (x : ℝ) : ContinuousWithinAt (↑f) (Set.Ici x) x

theorem StieltjesFunction.rightLim_eq (f : StieltjesFunction) (x : ℝ) : 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

instance StieltjesFunction.instInhabited : Inhabited StieltjesFunction

Equations

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

def StieltjesFunction.const (c : ℝ) : StieltjesFunction

Constant functions are Stieltjes function.

Equations

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

@[simp]

theorem StieltjesFunction.const_apply (c x : ℝ) : ↑(StieltjesFunction.const c) x = c

def StieltjesFunction.add (f 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' := ⋯ }

instance StieltjesFunction.instAddZeroClass : AddZeroClass StieltjesFunction

Equations

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

instance StieltjesFunction.instAddCommMonoid : AddCommMonoid StieltjesFunction

Equations

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

instance StieltjesFunction.instModuleNNReal : Module NNReal StieltjesFunction

Equations

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

@[simp]

theorem StieltjesFunction.add_apply (f g : StieltjesFunction) (x : ℝ) : ↑(f + g) x = ↑f x + ↑g x

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' := ⋯ }

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

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

The outer measure associated to a Stieltjes function

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)

@[simp]

theorem StieltjesFunction.length_empty (f : StieltjesFunction) : f.length ∅ = 0

@[simp]

theorem StieltjesFunction.length_Ioc (f : StieltjesFunction) (a b : ℝ) : f.length (Set.Ioc a b) = ENNReal.ofReal (↑f b - ↑f a)

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

def StieltjesFunction.outer (f : StieltjesFunction) : MeasureTheory.OuterMeasure ℝ

The Stieltjes outer measure associated to a Stieltjes function.

Equations

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

theorem StieltjesFunction.outer_le_length (f : StieltjesFunction) (s : Set ℝ) : f.outer s ≤ f.length s

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.

@[simp]

theorem StieltjesFunction.outer_Ioc (f : StieltjesFunction) (a b : ℝ) : f.outer (Set.Ioc a b) = ENNReal.ofReal (↑f b - ↑f a)

theorem StieltjesFunction.measurableSet_Ioi (f : StieltjesFunction) {c : ℝ} : MeasurableSet (Set.Ioi c)

theorem StieltjesFunction.outer_trim (f : StieltjesFunction) : f.outer.trim = f.outer

theorem StieltjesFunction.borel_le_measurable (f : StieltjesFunction) : borel ℝ ≤ f.outer.caratheodory

The measure associated to a Stieltjes function

theorem StieltjesFunction.measure_def (f : StieltjesFunction) : f.measure = { toOuterMeasure := f.outer, m_iUnion := ⋯, trim_le := ⋯ }

@[irreducible]

def StieltjesFunction.measure (f : StieltjesFunction) : MeasureTheory.Measure ℝ

The measure associated to a Stieltjes function, giving mass f b - f a to the interval (a, b].

Equations

• StieltjesFunction.measure = StieltjesFunction.wrapped✝.1

@[simp]

theorem StieltjesFunction.measure_Ioc (f : StieltjesFunction) (a b : ℝ) : f.measure (Set.Ioc a b) = ENNReal.ofReal (↑f b - ↑f a)

@[simp]

theorem StieltjesFunction.measure_singleton (f : StieltjesFunction) (a : ℝ) : f.measure {a} = ENNReal.ofReal (↑f a - Function.leftLim (↑f) a)

@[simp]

theorem StieltjesFunction.measure_Icc (f : StieltjesFunction) (a b : ℝ) : f.measure (Set.Icc a b) = ENNReal.ofReal (↑f b - Function.leftLim (↑f) a)

@[simp]

theorem StieltjesFunction.measure_Ioo (f : StieltjesFunction) {a b : ℝ} : f.measure (Set.Ioo a b) = ENNReal.ofReal (Function.leftLim (↑f) b - ↑f a)

@[simp]

theorem StieltjesFunction.measure_Ico (f : StieltjesFunction) (a b : ℝ) : f.measure (Set.Ico a b) = ENNReal.ofReal (Function.leftLim (↑f) b - Function.leftLim (↑f) a)

theorem StieltjesFunction.measure_Iic (f : StieltjesFunction) {l : ℝ} (hf : Filter.Tendsto (↑f) Filter.atBot (nhds l)) (x : ℝ) : f.measure (Set.Iic x) = ENNReal.ofReal (↑f x - l)

theorem StieltjesFunction.measure_Ici (f : StieltjesFunction) {l : ℝ} (hf : Filter.Tendsto (↑f) Filter.atTop (nhds l)) (x : ℝ) : f.measure (Set.Ici x) = ENNReal.ofReal (l - Function.leftLim (↑f) x)

theorem StieltjesFunction.measure_univ (f : StieltjesFunction) {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.isFiniteMeasure (f : StieltjesFunction) {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 (f : StieltjesFunction) (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 (f : StieltjesFunction) : MeasureTheory.IsLocallyFiniteMeasure f.measure

Equations

• ⋯ = ⋯

theorem StieltjesFunction.eq_of_measure_of_tendsto_atBot (f g : StieltjesFunction) {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 (f g : StieltjesFunction) {y : ℝ} (hfg : f.measure = g.measure) (hy : ↑f y = ↑g y) : f = g

@[simp]

theorem StieltjesFunction.measure_const (c : ℝ) : (StieltjesFunction.const c).measure = 0

@[simp]

theorem StieltjesFunction.measure_add (f g : StieltjesFunction) : (f + g).measure = f.measure + g.measure

@[simp]

theorem StieltjesFunction.measure_smul (c : NNReal) (f : StieltjesFunction) : (c • f).measure = c • f.measure