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.

source

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

source

theorem right_lim_eq_of_tendsto {α : Type u_1} {β : Type u_2} [linear_order α] [topological_space β] [hα : topological_space α] [h'α : order_topology α] [t2_space β] {f : α → β} {a : α} {y : β} (h : nhds_within a (set.Ioi a) ≠ ⊥) (h' : filter.tendsto f (nhds_within a (set.Ioi a)) (nhds y)) :

function.right_lim f a = y

source

theorem right_lim_eq_Inf {α : Type u_1} {β : Type u_2} [linear_order α] [topological_space β] [conditionally_complete_linear_order β] [order_topology β] {f : α → β} (hf : monotone f) {x : α} [topological_space α] [order_topology α] (h : nhds_within x (set.Ioi x) ≠ ⊥) :

function.right_lim f x = has_Inf.Inf (f '' set.Ioi x)

source

theorem exists_seq_monotone_tendsto_at_top_at_top (α : Type u_1) [semilattice_sup α] [nonempty α] [filter.at_top.is_countably_generated] :

∃ (xs : ℕ → α), monotone xs ∧ filter.tendsto xs filter.at_top filter.at_top

source

theorem exists_seq_antitone_tendsto_at_top_at_bot (α : Type u_1) [semilattice_inf α] [nonempty α] [h2 : filter.at_bot.is_countably_generated] :

∃ (xs : ℕ → α), antitone xs ∧ filter.tendsto xs filter.at_top filter.at_bot

source

theorem supr_eq_supr_subseq_of_antitone {ι₁ : Type u_1} {ι₂ : Type u_2} {α : Type u_3} [preorder ι₂] [complete_lattice α] {l : filter ι₁} [l.ne_bot] {f : ι₂ → α} {φ : ι₁ → ι₂} (hf : antitone f) (hφ : filter.tendsto φ l filter.at_bot) :

(⨆ (i : ι₂), f i) = ⨆ (i : ι₁), f (φ i)

source

theorem measure_theory.tendsto_measure_Ico_at_top {α : Type u_1} {mα : measurable_space α} [semilattice_sup α] [no_max_order α] [filter.at_top.is_countably_generated] (μ : measure_theory.measure α) (a : α) :

filter.tendsto (λ (x : α), ⇑μ (set.Ico a x)) filter.at_top (nhds (⇑μ (set.Ici a)))

source

theorem measure_theory.tendsto_measure_Ioc_at_bot {α : Type u_1} {mα : measurable_space α} [semilattice_inf α] [no_min_order α] [filter.at_bot.is_countably_generated] (μ : measure_theory.measure α) (a : α) :

filter.tendsto (λ (x : α), ⇑μ (set.Ioc x a)) filter.at_bot (nhds (⇑μ (set.Iic a)))

source

theorem measure_theory.tendsto_measure_Iic_at_top {α : Type u_1} {mα : measurable_space α} [semilattice_sup α] [filter.at_top.is_countably_generated] (μ : measure_theory.measure α) :

filter.tendsto (λ (x : α), ⇑μ (set.Iic x)) filter.at_top (nhds (⇑μ set.univ))

source

theorem measure_theory.tendsto_measure_Ici_at_bot {α : Type u_1} {mα : measurable_space α} [semilattice_inf α] [h : filter.at_bot.is_countably_generated] (μ : measure_theory.measure α) :

filter.tendsto (λ (x : α), ⇑μ (set.Ici x)) filter.at_bot (nhds (⇑μ set.univ))

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

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

function.right_lim ⇑f x = ⇑f x

source

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

(⨅ (r : ↥(set.Ioi x)), ⇑f ↑r) = ⇑f x

source

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

(⨅ (r : {r' // x < ↑r'}), ⇑f ↑r) = ⇑f 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) :