# mathlib3documentation

measure_theory.measure.stieltjes

# Stieltjes measures on the real line #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.
theorem infi_Ioi_eq_infi_rat_gt {f : } (x : ) (hf : bdd_below (f '' set.Ioi x)) (hf_mono : monotone f) :
( (r : (set.Ioi x)), f r) = (q : {q' // x < q'}), f q
theorem right_lim_eq_of_tendsto {α : Type u_1} {β : Type u_2} [linear_order α] [hα : topological_space α] [h'α : order_topology α] [t2_space β] {f : α β} {a : α} {y : β} (h : (set.Ioi a) ) (h' : (set.Ioi a)) (nhds y)) :
= y
theorem right_lim_eq_Inf {α : Type u_1} {β : Type u_2} [linear_order α] {f : α β} (hf : monotone f) {x : α} (h : (set.Ioi x) ) :
theorem exists_seq_monotone_tendsto_at_top_at_top (α : Type u_1) [nonempty α]  :
(xs : α),
theorem exists_seq_antitone_tendsto_at_top_at_bot (α : Type u_1) [nonempty α]  :
(xs : α),
theorem supr_eq_supr_subseq_of_antitone {ι₁ : Type u_1} {ι₂ : Type u_2} {α : Type u_3} [preorder ι₂] {l : filter ι₁} [l.ne_bot] {f : ι₂ α} {φ : ι₁ ι₂} (hf : antitone f) (hφ : filter.at_bot) :
( (i : ι₂), f i) = (i : ι₁), f (φ i)
theorem measure_theory.tendsto_measure_Ico_at_top {α : Type u_1} {mα : measurable_space α} [no_max_order α] (μ : measure_theory.measure α) (a : α) :
filter.tendsto (λ (x : α), μ (set.Ico a x)) filter.at_top (nhds (μ (set.Ici a)))
theorem measure_theory.tendsto_measure_Ioc_at_bot {α : Type u_1} {mα : measurable_space α} [no_min_order α] (μ : measure_theory.measure α) (a : α) :
filter.tendsto (λ (x : α), μ (set.Ioc x a)) filter.at_bot (nhds (μ (set.Iic a)))

### Basic properties of Stieltjes functions #

structure stieltjes_function  :

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

Instances for stieltjes_function
@[protected, instance]
Equations
theorem stieltjes_function.infi_rat_gt_eq (f : stieltjes_function) (x : ) :
( (r : {r' // x < r'}), f r) = f x
@[simp]
theorem stieltjes_function.id_apply (a : ) :
@[protected]

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

Equations
@[simp]
@[protected, instance]
Equations
noncomputable def monotone.stieltjes_function {f : } (hf : monotone f) :

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

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

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

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₂
@[protected]
noncomputable def stieltjes_function.outer (f : stieltjes_function) :

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 #

@[protected, irreducible]
noncomputable def stieltjes_function.measure (f : stieltjes_function) :

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

Equations
Instances for stieltjes_function.measure
@[simp]
theorem stieltjes_function.measure_Iic (f : stieltjes_function) {l : } (hf : (nhds l)) (x : ) :
theorem stieltjes_function.measure_univ (f : stieltjes_function) {l u : } (hfl : (nhds l)) (hfu : (nhds u)) :
@[protected, instance]