# mathlibdocumentation

measure_theory.measure.stieltjes

# 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.left_lim x is the limit of f to the left of x.
• 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 (f.left_lim b - f a).
• f.measure_Icc and f.measure_Ico are analogous.

### Basic properties of Stieltjes functions #

structure stieltjes_function  :
Type

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

@[instance]
Equations

The limit of a Stieltjes function to the left of x (it exists by monotonicity). The fact that it is indeed a left limit is asserted in tendsto_left_lim

Equations
theorem stieltjes_function.left_lim_le (f : stieltjes_function) {x y : } (h : x y) :
theorem stieltjes_function.le_left_lim (f : stieltjes_function) {x y : } (h : x < y) :
@[simp]
theorem stieltjes_function.id_apply (a : ) :

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

Equations
@[simp]
@[instance]
Equations

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

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

Equations
theorem stieltjes_function.length_mono (f : stieltjes_function) {s₁ s₂ : set } (h : s₁ s₂) :
f.length s₁ f.length s₂

The Stieltjes outer measure associated to a Stieltjes function.

Equations
theorem stieltjes_function.length_subadditive_Icc_Ioo (f : stieltjes_function) {a b : } {c d : } (ss : 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.

@[simp]

### The measure associated to a Stieltjes function #

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

Equations