# 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 #

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

Instances For
theorem StieltjesFunction.ext_iff {f : StieltjesFunction} {g : StieltjesFunction} :
f = g ∀ (x : ), f x = g x
theorem StieltjesFunction.ext {f : StieltjesFunction} {g : StieltjesFunction} (h : ∀ (x : ), f x = g x) :
f = g
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
@[simp]

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

Equations
Instances For
@[simp]

Constant functions are Stieltjes function.

Equations
• = { toFun := fun (x : ) => c, mono' := , right_continuous' := }
Instances For
@[simp]
theorem StieltjesFunction.const_apply (c : ) (x : ) :
x = c

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
@[simp]
theorem StieltjesFunction.add_apply (f : StieltjesFunction) (g : StieltjesFunction) (x : ) :
(f + g) x = f x + g x
noncomputable def Monotone.stieltjesFunction {f : } (hf : ) :

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 := , mono' := , right_continuous' := }
Instances For
theorem Monotone.stieltjesFunction_eq {f : } (hf : ) (x : ) :
hf.stieltjesFunction x =

### The outer measure associated to a Stieltjes function #

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

Equations
Instances For
@[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₂ : } (h : s₁ s₂) :
f.length s₁ f.length s₂

The Stieltjes outer measure associated to a Stieltjes function.

Equations
• f.outer =
Instances For
theorem StieltjesFunction.outer_le_length (f : StieltjesFunction) (s : ) :
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.outer_trim (f : StieltjesFunction) :
f.outer.trim = f.outer

### The measure associated to a Stieltjes function #

@[irreducible]

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

Equations
Instances For
theorem StieltjesFunction.measure_def (f : StieltjesFunction) :
f.measure = { toOuterMeasure := f.outer, m_iUnion := , trim_le := }
@[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)) :
theorem StieltjesFunction.isProbabilityMeasure (f : StieltjesFunction) (hf_bot : Filter.Tendsto (↑f) Filter.atBot (nhds 0)) (hf_top : Filter.Tendsto (↑f) Filter.atTop (nhds 1)) :
theorem StieltjesFunction.eq_of_measure_of_tendsto_atBot (f : StieltjesFunction) (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 : StieltjesFunction) (g : StieltjesFunction) {y : } (hfg : f.measure = g.measure) (hy : f y = g y) :
f = g
@[simp]
theorem StieltjesFunction.measure_const (c : ) :
.measure = 0
@[simp]
theorem StieltjesFunction.measure_add (f : StieltjesFunction) (g : StieltjesFunction) :
(f + g).measure = f.measure + g.measure
@[simp]
theorem StieltjesFunction.measure_smul (c : NNReal) (f : StieltjesFunction) :
(c f).measure = c f.measure