diff --git a/docs/overview.yaml b/docs/overview.yaml
index e6a94f886b73c..3ed974377ad10 100644
--- a/docs/overview.yaml
+++ b/docs/overview.yaml
@@ -286,7 +286,8 @@ Analysis:
     the category of measurable spaces: 'Meas'
     Borel sigma-algebra: 'borel_space'
     positive measure: 'measure_theory.measure'
-    Lebesgue measure: 'measure_theory.real.measure_space'
+    Stieltjes measure: 'stieltjes_function.measure'
+    Lebesgue measure: 'real.measure_space'
     Hausdorff measure: 'measure_theory.measure.hausdorff_measure'
     Hausdorff dimension: 'measure_theory.dimH'
     Giry monad: 'measure_theory.measure.measurable_space'
diff --git a/src/data/set/intervals/basic.lean b/src/data/set/intervals/basic.lean
index 0c3abcffa9972..b3694b48a6951 100644
--- a/src/data/set/intervals/basic.lean
+++ b/src/data/set/intervals/basic.lean
@@ -600,6 +600,10 @@ lemma Ico_subset_Ico_iff (h₁ : a₁ < b₁) :
   ⟨this.1, le_of_not_lt $ λ h', lt_irrefl b₂ (h ⟨this.2.le, h'⟩).2⟩,
  λ ⟨h₁, h₂⟩, Ico_subset_Ico h₁ h₂⟩
 
+lemma Ioc_subset_Ioc_iff (h₁ : a₁ < b₁) :
+  Ioc a₁ b₁ ⊆ Ioc a₂ b₂ ↔ b₁ ≤ b₂ ∧ a₂ ≤ a₁ :=
+by { convert @Ico_subset_Ico_iff (order_dual α) _ b₁ b₂ a₁ a₂ h₁; exact (@dual_Ico α _ _ _).symm }
+
 lemma Ioo_subset_Ioo_iff [densely_ordered α] (h₁ : a₁ < b₁) :
   Ioo a₁ b₁ ⊆ Ioo a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂ :=
 ⟨λ h, begin
@@ -1123,6 +1127,10 @@ by { ext x, simp [Ici] }
 @[simp] lemma Ioi_inter_Ioi [is_total α (≤)] {a b : α} : Ioi a ∩ Ioi b = Ioi (a ⊔ b) :=
 by { ext x, simp [Ioi] }
 
+@[simp] lemma Ioc_inter_Ioi [is_total α (≤)] {a b c : α} : Ioc a b ∩ Ioi c = Ioc (a ⊔ c) b :=
+by rw [← Ioi_inter_Iic, inter_assoc, inter_comm, inter_assoc, Ioi_inter_Ioi, inter_comm,
+  Ioi_inter_Iic, sup_comm]
+
 end sup
 
 section both
@@ -1174,10 +1182,13 @@ lemma Iic_inter_Ioc_of_le (h : a₂ ≤ a) : Iic a₂ ∩ Ioc a₁ a = Ioc a₁
 ext $ λ x, ⟨λ H, ⟨H.2.1, H.1⟩, λ H, ⟨H.2, H.1, H.2.trans h⟩⟩
 
 @[simp] lemma Ico_diff_Iio : Ico a b \ Iio c = Ico (max a c) b :=
-ext $ by simp [Ico, Iio, iff_def, max_le_iff] {contextual:=tt}
+ext $ by simp [iff_def] {contextual:=tt}
+
+@[simp] lemma Ioc_diff_Ioi : Ioc a b \ Ioi c = Ioc a (min b c) :=
+ext $ by simp [iff_def] {contextual:=tt}
 
 @[simp] lemma Ico_inter_Iio : Ico a b ∩ Iio c = Ico a (min b c) :=
-ext $ by simp [Ico, Iio, iff_def, lt_min_iff] {contextual:=tt}
+ext $ by simp [iff_def] {contextual:=tt}
 
 @[simp] lemma Ioc_union_Ioc_right : Ioc a b ∪ Ioc a c = Ioc a (max b c) :=
 by rw [Ioc_union_Ioc, min_self]; exact (min_le_left _ _).trans (le_max_left _ _)
diff --git a/src/measure_theory/measure/lebesgue.lean b/src/measure_theory/measure/lebesgue.lean
index 34f101546ed3f..885d6c4661769 100644
--- a/src/measure_theory/measure/lebesgue.lean
+++ b/src/measure_theory/measure/lebesgue.lean
@@ -4,241 +4,28 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Yury Kudryashov
 -/
 import measure_theory.constructions.pi
+import measure_theory.measure.stieltjes
 
 /-!
 # Lebesgue measure on the real line and on `ℝⁿ`
+
+We construct Lebesgue measure on the real line, as a particular case of Stieltjes measure associated
+to the function `x ↦ x`. We obtain as a consequence Lebesgue measure on `ℝⁿ`. We prove their
+basic properties.
 -/
 
 noncomputable theory
-open classical set filter
+open classical set filter measure_theory
 open ennreal (of_real)
-open_locale big_operators ennreal nnreal
-
-namespace measure_theory
-
-/-!
-### Preliminary definitions
--/
-
-/-- Length of an interval. This is the largest monotonic function which correctly
-  measures all intervals. -/
-def lebesgue_length (s : set ℝ) : ℝ≥0∞ := ⨅a b (h : s ⊆ Ico a b), of_real (b - a)
-
-@[simp] lemma lebesgue_length_empty : lebesgue_length ∅ = 0 :=
-nonpos_iff_eq_zero.1 $ infi_le_of_le 0 $ infi_le_of_le 0 $ by simp
-
-@[simp] lemma lebesgue_length_Ico (a b : ℝ) :
-  lebesgue_length (Ico a b) = of_real (b - a) :=
-begin
-  refine le_antisymm (infi_le_of_le a $ binfi_le b (subset.refl _))
-    (le_infi $ λ a', le_infi $ λ b', le_infi $ λ h, ennreal.coe_le_coe.2 _),
-  cases le_or_lt b a with ab ab,
-  { rw real.to_nnreal_of_nonpos (sub_nonpos.2 ab), apply zero_le },
-  cases (Ico_subset_Ico_iff ab).1 h with h₁ h₂,
-  exact real.to_nnreal_le_to_nnreal (sub_le_sub h₂ h₁)
-end
-
-lemma lebesgue_length_mono {s₁ s₂ : set ℝ} (h : s₁ ⊆ s₂) :
-  lebesgue_length s₁ ≤ lebesgue_length s₂ :=
-infi_le_infi $ λ a, infi_le_infi $ λ b, infi_le_infi2 $ λ h', ⟨subset.trans h h', le_refl _⟩
-
-lemma lebesgue_length_eq_infi_Ioo (s) :
-  lebesgue_length s = ⨅a b (h : s ⊆ Ioo a b), of_real (b - a) :=
-begin
-  refine le_antisymm
-    (infi_le_infi $ λ a, infi_le_infi $ λ b, infi_le_infi2 $ λ h,
-      ⟨subset.trans h Ioo_subset_Ico_self, le_refl _⟩) _,
-  refine le_infi (λ a, le_infi $ λ b, le_infi $ λ h, _),
-  refine ennreal.le_of_forall_pos_le_add (λ ε ε0 _, _),
-  refine infi_le_of_le (a - ε) (infi_le_of_le b $ infi_le_of_le
-    (subset.trans h $ Ico_subset_Ioo_left $ (sub_lt_self_iff _).2 ε0) _),
-  rw ← sub_add,
-  refine le_trans ennreal.of_real_add_le (add_le_add_left _ _),
-  simp only [ennreal.of_real_coe_nnreal, le_refl]
-end
-
-@[simp] lemma lebesgue_length_Ioo (a b : ℝ) :
-  lebesgue_length (Ioo a b) = of_real (b - a) :=
-begin
-  rw ← lebesgue_length_Ico,
-  refine le_antisymm (lebesgue_length_mono Ioo_subset_Ico_self) _,
-  rw lebesgue_length_eq_infi_Ioo (Ioo a b),
-  refine (le_infi $ λ a', le_infi $ λ b', le_infi $ λ h, _),
-  cases le_or_lt b a with ab ab, {simp [ab]},
-  cases (Ioo_subset_Ioo_iff ab).1 h with h₁ h₂,
-  rw [lebesgue_length_Ico],
-  exact ennreal.of_real_le_of_real (sub_le_sub h₂ h₁)
-end
-
-lemma lebesgue_length_eq_infi_Icc (s) :
-  lebesgue_length s = ⨅a b (h : s ⊆ Icc a b), of_real (b - a) :=
-begin
-  refine le_antisymm _
-    (infi_le_infi $ λ a, infi_le_infi $ λ b, infi_le_infi2 $ λ h,
-      ⟨subset.trans h Ico_subset_Icc_self, le_refl _⟩),
-  refine le_infi (λ a, le_infi $ λ b, le_infi $ λ h, _),
-  refine ennreal.le_of_forall_pos_le_add (λ ε ε0 _, _),
-  refine infi_le_of_le a (infi_le_of_le (b + ε) $ infi_le_of_le
-    (subset.trans h $ Icc_subset_Ico_right $ (lt_add_iff_pos_right _).2 ε0) _),
-  rw [← sub_add_eq_add_sub],
-  refine le_trans ennreal.of_real_add_le (add_le_add_left _ _),
-  simp only [ennreal.of_real_coe_nnreal, le_refl]
-end
-
-@[simp] lemma lebesgue_length_Icc (a b : ℝ) :
-  lebesgue_length (Icc a b) = of_real (b - a) :=
-begin
-  rw ← lebesgue_length_Ico,
-  refine le_antisymm _ (lebesgue_length_mono Ico_subset_Icc_self),
-  rw lebesgue_length_eq_infi_Icc (Icc a b),
-  exact infi_le_of_le a (infi_le_of_le b $ infi_le_of_le (by refl) (by simp [le_refl]))
-end
-
-/-- The Lebesgue outer measure, as an outer measure of ℝ. -/
-def lebesgue_outer : outer_measure ℝ :=
-outer_measure.of_function lebesgue_length lebesgue_length_empty
-
-lemma lebesgue_outer_le_length (s : set ℝ) : lebesgue_outer s ≤ lebesgue_length s :=
-outer_measure.of_function_le _
-
-lemma lebesgue_length_subadditive {a b : ℝ} {c d : ℕ → ℝ}
-  (ss : Icc a b ⊆ ⋃i, Ioo (c i) (d i)) :
-  (of_real (b - a) : ℝ≥0∞) ≤ ∑' i, of_real (d i - c i) :=
-begin
-  suffices : ∀ (s:finset ℕ) b
-    (cv : Icc a b ⊆ ⋃ i ∈ (↑s:set ℕ), Ioo (c i) (d i)),
-    (of_real (b - a) : ℝ≥0∞) ≤ ∑ i in s, of_real (d i - c i),
-  { rcases is_compact_Icc.elim_finite_subcover_image (λ (i : ℕ) (_ : i ∈ univ),
-      @is_open_Ioo _ _ _ _ (c i) (d i)) (by simpa using ss) with ⟨s, su, hf, hs⟩,
-    have e : (⋃ i ∈ (↑hf.to_finset:set ℕ),
-      Ioo (c i) (d i)) = (⋃ i ∈ s, Ioo (c i) (d i)), {simp [set.ext_iff]},
-    rw ennreal.tsum_eq_supr_sum,
-    refine le_trans _ (le_supr _ hf.to_finset),
-    exact this hf.to_finset _ (by simpa [e]) },
-  clear ss b,
-  refine λ s, finset.strong_induction_on s (λ s IH b cv, _),
-  cases le_total b a with ab ab,
-  { rw ennreal.of_real_eq_zero.2 (sub_nonpos.2 ab), exact zero_le _ },
-  have := cv ⟨ab, le_refl _⟩, simp at this,
-  rcases this with ⟨i, is, cb, bd⟩,
-  rw [← finset.insert_erase is] at cv ⊢,
-  rw [finset.coe_insert, bUnion_insert] at cv,
-  rw [finset.sum_insert (finset.not_mem_erase _ _)],
-  refine le_trans _ (add_le_add_left (IH _ (finset.erase_ssubset is) (c i) _) _),
-  { refine le_trans (ennreal.of_real_le_of_real _) ennreal.of_real_add_le,
-    rw sub_add_sub_cancel,
-    exact sub_le_sub_right (le_of_lt bd) _ },
-  { rintro x ⟨h₁, h₂⟩,
-    refine (cv ⟨h₁, le_trans h₂ (le_of_lt cb)⟩).resolve_left
-      (mt and.left (not_lt_of_le h₂)) }
-end
-
-@[simp] lemma lebesgue_outer_Icc (a b : ℝ) :
-  lebesgue_outer (Icc a b) = of_real (b - a) :=
-begin
-  refine le_antisymm (by rw ← lebesgue_length_Icc; apply lebesgue_outer_le_length)
-    (le_binfi $ λ f hf, ennreal.le_of_forall_pos_le_add $ λ ε ε0 h, _),
-  rcases ennreal.exists_pos_sum_of_encodable
-    (ennreal.zero_lt_coe_iff.2 ε0) ℕ with ⟨ε', ε'0, hε⟩,
-  refine le_trans _ (add_le_add_left (le_of_lt hε) _),
-  rw ← ennreal.tsum_add,
-  choose g hg using show
-    ∀ i, ∃ p:ℝ×ℝ, f i ⊆ Ioo p.1 p.2 ∧ (of_real (p.2 - p.1) : ℝ≥0∞) <
-      lebesgue_length (f i) + ε' i,
-  { intro i,
-    have := (ennreal.lt_add_right (lt_of_le_of_lt (ennreal.le_tsum i) h)
-        (ennreal.zero_lt_coe_iff.2 (ε'0 i))),
-    conv at this {to_lhs, rw lebesgue_length_eq_infi_Ioo},
-    simpa [infi_lt_iff] },
-  refine le_trans _ (ennreal.tsum_le_tsum $ λ i, le_of_lt (hg i).2),
-  exact lebesgue_length_subadditive (subset.trans hf $
-    Union_subset_Union $ λ i, (hg i).1)
-end
-
-@[simp] lemma lebesgue_outer_singleton (a : ℝ) : lebesgue_outer {a} = 0 :=
-by simpa using lebesgue_outer_Icc a a
-
-@[simp] lemma lebesgue_outer_Ico (a b : ℝ) :
-  lebesgue_outer (Ico a b) = of_real (b - a) :=
-by rw [← Icc_diff_right, lebesgue_outer.diff_null _ (lebesgue_outer_singleton _),
-  lebesgue_outer_Icc]
-
-@[simp] lemma lebesgue_outer_Ioo (a b : ℝ) :
-  lebesgue_outer (Ioo a b) = of_real (b - a) :=
-by rw [← Ico_diff_left, lebesgue_outer.diff_null _ (lebesgue_outer_singleton _), lebesgue_outer_Ico]
-
-@[simp] lemma lebesgue_outer_Ioc (a b : ℝ) :
-  lebesgue_outer (Ioc a b) = of_real (b - a) :=
-by rw [← Icc_diff_left, lebesgue_outer.diff_null _ (lebesgue_outer_singleton _), lebesgue_outer_Icc]
-
-lemma is_lebesgue_measurable_Iio {c : ℝ} :
-  lebesgue_outer.caratheodory.measurable_set' (Iio c) :=
-outer_measure.of_function_caratheodory $ λ t,
-le_infi $ λ a, le_infi $ λ b, le_infi $ λ h, begin
-  refine le_trans (add_le_add
-    (lebesgue_length_mono $ inter_subset_inter_left _ h)
-    (lebesgue_length_mono $ diff_subset_diff_left h)) _,
-  cases le_total a c with hac hca; cases le_total b c with hbc hcb;
-    simp [*, -sub_eq_add_neg, sub_add_sub_cancel', le_refl],
-  { simp [*, ← ennreal.of_real_add, -sub_eq_add_neg, sub_add_sub_cancel', le_refl] },
-  { simp only [ennreal.of_real_eq_zero.2 (sub_nonpos.2 (le_trans hbc hca)), zero_add, le_refl] }
-end
-
-theorem lebesgue_outer_trim : lebesgue_outer.trim = lebesgue_outer :=
-begin
-  refine le_antisymm (λ s, _) (outer_measure.le_trim _),
-  rw outer_measure.trim_eq_infi,
-  refine le_infi (λ f, le_infi $ λ hf,
-    ennreal.le_of_forall_pos_le_add $ λ ε ε0 h, _),
-  rcases ennreal.exists_pos_sum_of_encodable
-    (ennreal.zero_lt_coe_iff.2 ε0) ℕ with ⟨ε', ε'0, hε⟩,
-  refine le_trans _ (add_le_add_left (le_of_lt hε) _),
-  rw ← ennreal.tsum_add,
-  choose g hg using show
-    ∀ i, ∃ s, f i ⊆ s ∧ measurable_set s ∧
-      lebesgue_outer s ≤ lebesgue_length (f i) + of_real (ε' i),
-  { intro i,
-    have := (ennreal.lt_add_right (lt_of_le_of_lt (ennreal.le_tsum i) h)
-        (ennreal.zero_lt_coe_iff.2 (ε'0 i))),
-    conv at this {to_lhs, rw lebesgue_length},
-    simp only [infi_lt_iff] at this,
-    rcases this with ⟨a, b, h₁, h₂⟩,
-    rw ← lebesgue_outer_Ico at h₂,
-    exact ⟨_, h₁, measurable_set_Ico, le_of_lt $ by simpa using h₂⟩ },
-  simp at hg,
-  apply infi_le_of_le (Union g) _,
-  apply infi_le_of_le (subset.trans hf $ Union_subset_Union (λ i, (hg i).1)) _,
-  apply infi_le_of_le (measurable_set.Union (λ i, (hg i).2.1)) _,
-  exact le_trans (lebesgue_outer.Union _) (ennreal.tsum_le_tsum $ λ i, (hg i).2.2)
-end
-
-lemma borel_le_lebesgue_measurable : borel ℝ ≤ lebesgue_outer.caratheodory :=
-begin
-  rw real.borel_eq_generate_from_Iio_rat,
-  refine measurable_space.generate_from_le _,
-  simp [is_lebesgue_measurable_Iio] { contextual := tt }
-end
+open_locale big_operators ennreal nnreal topological_space
 
 /-!
 ### Definition of the Lebesgue measure and lengths of intervals
 -/
 
-/-- Lebesgue measure on the Borel sets
-
-The outer Lebesgue measure is the completion of this measure. (TODO: proof this)
--/
+/-- Lebesgue measure on the Borel sigma algebra, giving measure `b - a` to the interval `[a, b]`. -/
 instance real.measure_space : measure_space ℝ :=
-⟨{to_outer_measure := lebesgue_outer,
-  m_Union := λ f hf, lebesgue_outer.Union_eq_of_caratheodory $
-    λ i, borel_le_lebesgue_measurable _ (hf i),
-  trimmed := lebesgue_outer_trim }⟩
-
-@[simp] theorem lebesgue_to_outer_measure :
-  (volume : measure ℝ).to_outer_measure = lebesgue_outer := rfl
-
-end measure_theory
-
-open measure_theory
+⟨stieltjes_function.id.measure⟩
 
 namespace real
 
@@ -246,20 +33,25 @@ variables {ι : Type*} [fintype ι]
 
 open_locale topological_space
 
-theorem volume_val (s) : volume s = lebesgue_outer s := rfl
+theorem volume_val (s) : volume s = stieltjes_function.id.measure s := rfl
 
-instance has_no_atoms_volume : has_no_atoms (volume : measure ℝ) :=
-⟨lebesgue_outer_singleton⟩
+@[simp] lemma volume_Ico {a b : ℝ} : volume (Ico a b) = of_real (b - a) :=
+by simp [volume_val]
 
-@[simp] lemma volume_Ico {a b : ℝ} : volume (Ico a b) = of_real (b - a) := lebesgue_outer_Ico a b
+@[simp] lemma volume_Icc {a b : ℝ} : volume (Icc a b) = of_real (b - a) :=
+by simp [volume_val]
 
-@[simp] lemma volume_Icc {a b : ℝ} : volume (Icc a b) = of_real (b - a) := lebesgue_outer_Icc a b
+@[simp] lemma volume_Ioo {a b : ℝ} : volume (Ioo a b) = of_real (b - a) :=
+by simp [volume_val]
 
-@[simp] lemma volume_Ioo {a b : ℝ} : volume (Ioo a b) = of_real (b - a) := lebesgue_outer_Ioo a b
+@[simp] lemma volume_Ioc {a b : ℝ} : volume (Ioc a b) = of_real (b - a) :=
+by simp [volume_val]
 
-@[simp] lemma volume_Ioc {a b : ℝ} : volume (Ioc a b) = of_real (b - a) := lebesgue_outer_Ioc a b
+@[simp] lemma volume_singleton {a : ℝ} : volume ({a} : set ℝ) = 0 :=
+by simp [volume_val]
 
-@[simp] lemma volume_singleton {a : ℝ} : volume ({a} : set ℝ) = 0 := lebesgue_outer_singleton a
+instance has_no_atoms_volume : has_no_atoms (volume : measure ℝ) :=
+⟨λ x, volume_singleton⟩
 
 @[simp] lemma volume_interval {a b : ℝ} : volume (interval a b) = of_real (abs (b - a)) :=
 by rw [interval, volume_Icc, max_sub_min_eq_abs]
diff --git a/src/measure_theory/measure/stieltjes.lean b/src/measure_theory/measure/stieltjes.lean
new file mode 100644
index 0000000000000..2db8f22227ebf
--- /dev/null
+++ b/src/measure_theory/measure/stieltjes.lean
@@ -0,0 +1,352 @@
+/-
+Copyright (c) 2021 Sébastien Gouëzel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johannes Hölzl, Yury Kudryashov, Sébastien Gouëzel
+-/
+import measure_theory.constructions.borel_space
+
+/-!
+# 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.
+-/
+
+noncomputable theory
+open classical set filter
+open ennreal (of_real)
+open_locale big_operators ennreal nnreal topological_space
+
+/-! ### Basic properties of Stieltjes functions -/
+
+/-- Bundled monotone right-continuous real functions, used to construct Stieltjes measures. -/
+structure stieltjes_function :=
+(to_fun : ℝ → ℝ)
+(mono' : monotone to_fun)
+(right_continuous' : ∀ x, continuous_within_at to_fun (Ici x) x)
+
+namespace stieltjes_function
+
+instance : has_coe_to_fun stieltjes_function := ⟨_, to_fun⟩
+
+initialize_simps_projections stieltjes_function (to_fun → apply)
+
+variable (f : stieltjes_function)
+
+lemma mono : monotone f := f.mono'
+
+lemma right_continuous (x : ℝ) : continuous_within_at f (Ici x) x := f.right_continuous' x
+
+/-- 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` -/
+@[irreducible] def left_lim (x : ℝ) := Sup (f '' (Iio x))
+
+lemma tendsto_left_lim (x : ℝ) : tendsto f (𝓝[Iio x] x) (𝓝 (f.left_lim x)) :=
+by { rw left_lim, exact f.mono.tendsto_nhds_within_Iio x }
+
+lemma left_lim_le {x y : ℝ} (h : x ≤ y) : f.left_lim x ≤ f y :=
+begin
+  apply le_of_tendsto (f.tendsto_left_lim x),
+  filter_upwards [self_mem_nhds_within],
+  assume z hz,
+  exact (f.mono (le_of_lt hz)).trans (f.mono h)
+end
+
+lemma le_left_lim {x y : ℝ} (h : x < y) : f x ≤ f.left_lim y :=
+begin
+  apply ge_of_tendsto (f.tendsto_left_lim y),
+  apply mem_nhds_within_Iio_iff_exists_Ioo_subset.2 ⟨x, h, _⟩,
+  assume z hz,
+  exact f.mono hz.1.le,
+end
+
+lemma left_lim_le_left_lim {x y : ℝ} (h : x ≤ y) : f.left_lim x ≤ f.left_lim y :=
+begin
+  rcases eq_or_lt_of_le h with rfl|hxy,
+  { exact le_rfl },
+  { exact (f.left_lim_le le_rfl).trans (f.le_left_lim hxy) }
+end
+
+/-- The identity of `ℝ` as a Stieltjes function, used to construct Lebesgue measure. -/
+@[simps] protected def id : stieltjes_function :=
+{ to_fun := id,
+  mono' := λ x y, id,
+  right_continuous' := λ x, continuous_within_at_id }
+
+@[simp] lemma id_left_lim (x : ℝ) : stieltjes_function.id.left_lim x = x :=
+tendsto_nhds_unique (stieltjes_function.id.tendsto_left_lim x) $
+  (continuous_at_id).tendsto.mono_left nhds_within_le_nhds
+
+instance : inhabited stieltjes_function := ⟨stieltjes_function.id⟩
+
+/-! ### The outer measure associated to a Stieltjes function -/
+
+/-- Length of an interval. This is the largest monotonic function which correctly
+  measures all intervals. -/
+def length (s : set ℝ) : ℝ≥0∞ := ⨅a b (h : s ⊆ Ioc a b), of_real (f b - f a)
+
+@[simp] lemma length_empty : f.length ∅ = 0 :=
+nonpos_iff_eq_zero.1 $ infi_le_of_le 0 $ infi_le_of_le 0 $ by simp
+
+@[simp] lemma length_Ioc (a b : ℝ) :
+  f.length (Ioc a b) = of_real (f b - f a) :=
+begin
+  refine le_antisymm (infi_le_of_le a $ binfi_le b (subset.refl _))
+    (le_infi $ λ a', le_infi $ λ b', le_infi $ λ h, ennreal.coe_le_coe.2 _),
+  cases le_or_lt b a with ab ab,
+  { rw real.to_nnreal_of_nonpos (sub_nonpos.2 (f.mono ab)), apply zero_le, },
+  cases (Ioc_subset_Ioc_iff ab).1 h with h₁ h₂,
+  exact real.to_nnreal_le_to_nnreal (sub_le_sub (f.mono h₁) (f.mono h₂))
+end
+
+lemma length_mono {s₁ s₂ : set ℝ} (h : s₁ ⊆ s₂) :
+  f.length s₁ ≤ f.length s₂ :=
+infi_le_infi $ λ a, infi_le_infi $ λ b, infi_le_infi2 $ λ h', ⟨subset.trans h h', le_refl _⟩
+
+open measure_theory
+
+/-- The Stieltjes outer measure associated to a Stieltjes function. -/
+protected def outer : outer_measure ℝ :=
+outer_measure.of_function f.length f.length_empty
+
+lemma outer_le_length (s : set ℝ) : f.outer s ≤ f.length s :=
+outer_measure.of_function_le _
+
+/-- 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. -/
+lemma length_subadditive_Icc_Ioo {a b : ℝ} {c d : ℕ → ℝ}
+  (ss : Icc a b ⊆ ⋃ i, Ioo (c i) (d i)) :
+  of_real (f b - f a) ≤ ∑' i, of_real (f (d i) - f (c i)) :=
+begin
+  suffices : ∀ (s:finset ℕ) b
+    (cv : Icc a b ⊆ ⋃ i ∈ (↑s:set ℕ), Ioo (c i) (d i)),
+    (of_real (f b - f a) : ℝ≥0∞) ≤ ∑ i in s, of_real (f (d i) - f (c i)),
+  { rcases is_compact_Icc.elim_finite_subcover_image (λ (i : ℕ) (_ : i ∈ univ),
+      @is_open_Ioo _ _ _ _ (c i) (d i)) (by simpa using ss) with ⟨s, su, hf, hs⟩,
+    have e : (⋃ i ∈ (↑hf.to_finset:set ℕ), Ioo (c i) (d i)) = (⋃ i ∈ s, Ioo (c i) (d i)),
+      by simp only [ext_iff, exists_prop, finset.set_bUnion_coe, mem_Union, forall_const, iff_self,
+                    finite.mem_to_finset],
+    rw ennreal.tsum_eq_supr_sum,
+    refine le_trans _ (le_supr _ hf.to_finset),
+    exact this hf.to_finset _ (by simpa only [e]) },
+  clear ss b,
+  refine λ s, finset.strong_induction_on s (λ s IH b cv, _),
+  cases le_total b a with ab ab,
+  { rw ennreal.of_real_eq_zero.2 (sub_nonpos.2 (f.mono ab)), exact zero_le _, },
+  have := cv ⟨ab, le_refl _⟩, simp at this,
+  rcases this with ⟨i, is, cb, bd⟩,
+  rw [← finset.insert_erase is] at cv ⊢,
+  rw [finset.coe_insert, bUnion_insert] at cv,
+  rw [finset.sum_insert (finset.not_mem_erase _ _)],
+  refine le_trans _ (add_le_add_left (IH _ (finset.erase_ssubset is) (c i) _) _),
+  { refine le_trans (ennreal.of_real_le_of_real _) ennreal.of_real_add_le,
+    rw sub_add_sub_cancel,
+    exact sub_le_sub_right (f.mono bd.le) _ },
+  { rintro x ⟨h₁, h₂⟩,
+    refine (cv ⟨h₁, le_trans h₂ (le_of_lt cb)⟩).resolve_left
+      (mt and.left (not_lt_of_le h₂)) }
+end
+
+@[simp] lemma outer_Ioc (a b : ℝ) :
+  f.outer (Ioc a b) = of_real (f b - f a) :=
+begin
+  /- It suffices to show that, if `(a, b]` is covered by sets `s i`, then `f b - f a` is bounded
+  by `∑ f.length (s i) + ε`. The difficulty is that `f.length` is expressed in terms of half-open
+  intervals, while we would like to have a compact interval covered by open intervals to use
+  compactness and finite sums, as provided by `length_subadditive_Icc_Ioo`. The trick is to use the
+  right-continuity of `f`. If `a'` is close enough to `a` on its right, then `[a', b]` is still
+  covered by the sets `s i` and moreover `f b - f a'` is very close to `f b - f a` (up to `ε/2`).
+  Also, by definition one can cover `s i` by a half-closed interval `(p i, q i]` with `f`-length
+  very close to  that of `s i` (within a suitably small `ε' i`, say). If one moves `q i` very
+  slightly to the right, then the `f`-length will change very little by right continuity, and we
+  will get an open interval `(p i, q' i)` covering `s i` with `f (q' i) - f (p i)` within `ε' i`
+  of the `f`-length of `s i`. -/
+  refine le_antisymm (by { rw ← f.length_Ioc, apply outer_le_length })
+    (le_binfi $ λ s hs, ennreal.le_of_forall_pos_le_add $ λ ε εpos h, _),
+  let δ := ε/2,
+  have δpos : 0 < δ := nnreal.half_pos εpos,
+  rcases ennreal.exists_pos_sum_of_encodable
+    (ennreal.zero_lt_coe_iff.2 δpos) ℕ with ⟨ε', ε'0, hε⟩,
+  obtain ⟨a', ha', aa'⟩ : ∃ a', f a' - f a < δ ∧ a < a',
+  { have A : continuous_within_at (λ r, f r - f a) (Ioi a) a,
+    { refine continuous_within_at.sub _ continuous_within_at_const,
+      exact (f.right_continuous a).mono Ioi_subset_Ici_self },
+    have B : f a - f a < δ, by rwa [sub_self],
+    exact (((tendsto_order.1 A).2 _ B).and self_mem_nhds_within).exists },
+  have : ∀ i, ∃ p:ℝ×ℝ, s i ⊆ Ioo p.1 p.2 ∧
+                        (of_real (f p.2 - f p.1) : ℝ≥0∞) < f.length (s i) + ε' i,
+  { intro i,
+    have := (ennreal.lt_add_right (lt_of_le_of_lt (ennreal.le_tsum i) h)
+        (ennreal.zero_lt_coe_iff.2 (ε'0 i))),
+    conv at this { to_lhs, rw length },
+    simp only [infi_lt_iff, exists_prop] at this,
+    rcases this with ⟨p, q', spq, hq'⟩,
+    have : continuous_within_at (λ r, of_real (f r - f p)) (Ioi q') q',
+    { apply ennreal.continuous_of_real.continuous_at.comp_continuous_within_at,
+      refine continuous_within_at.sub _ continuous_within_at_const,
+      exact (f.right_continuous q').mono Ioi_subset_Ici_self },
+    rcases (((tendsto_order.1 this).2 _ hq').and self_mem_nhds_within).exists with ⟨q, hq, q'q⟩,
+    exact ⟨⟨p, q⟩, spq.trans (Ioc_subset_Ioo_right q'q), hq⟩ },
+  choose g hg using this,
+  have I_subset : Icc a' b ⊆ ⋃ i, Ioo (g i).1 (g i).2 := calc
+    Icc a' b ⊆ Ioc a b : λ x hx, ⟨aa'.trans_le hx.1, hx.2⟩
+    ... ⊆ ⋃ i, s i : hs
+    ... ⊆ ⋃ i, Ioo (g i).1 (g i).2 : Union_subset_Union (λ i, (hg i).1),
+  calc of_real (f b - f a)
+      = of_real ((f b - f a') + (f a' - f a)) : by rw sub_add_sub_cancel
+  ... ≤ of_real (f b - f a') + of_real (f a' - f a) : ennreal.of_real_add_le
+  ... ≤ (∑' i, of_real (f (g i).2 - f (g i).1)) + of_real δ :
+    add_le_add (f.length_subadditive_Icc_Ioo I_subset) (ennreal.of_real_le_of_real ha'.le)
+  ... ≤ (∑' i, (f.length (s i) + ε' i)) + δ :
+    add_le_add (ennreal.tsum_le_tsum (λ i, (hg i).2.le))
+      (by simp only [ennreal.of_real_coe_nnreal, le_rfl])
+  ... = (∑' i, f.length (s i)) + (∑' i, ε' i) + δ : by rw [ennreal.tsum_add]
+  ... ≤ (∑' i, f.length (s i)) + δ + δ : add_le_add (add_le_add le_rfl hε.le) le_rfl
+  ... = ∑' (i : ℕ), f.length (s i) + ε : by simp [add_assoc, ennreal.add_halves]
+end
+
+lemma measurable_set_Ioi {c : ℝ} :
+  f.outer.caratheodory.measurable_set' (Ioi c) :=
+begin
+  apply outer_measure.of_function_caratheodory (λ t, _),
+  refine le_infi (λ a, le_infi (λ b, le_infi (λ h, _))),
+  refine le_trans (add_le_add
+    (f.length_mono $ inter_subset_inter_left _ h)
+    (f.length_mono $ diff_subset_diff_left h)) _,
+  cases le_total a c with hac hac; cases le_total b c with hbc hbc,
+  { simp only [Ioc_inter_Ioi, f.length_Ioc, hac, sup_eq_max, hbc, le_refl, Ioc_eq_empty,
+      max_eq_right, min_eq_left, Ioc_diff_Ioi, f.length_empty, zero_add, not_lt] },
+  { simp only [hac, hbc, Ioc_inter_Ioi, Ioc_diff_Ioi, f.length_Ioc, min_eq_right,
+      sup_eq_max, ←ennreal.of_real_add, f.mono hac, f.mono hbc, sub_nonneg, sub_add_sub_cancel,
+      le_refl, max_eq_right] },
+  { simp only [hbc, le_refl, Ioc_eq_empty, Ioc_inter_Ioi, min_eq_left, Ioc_diff_Ioi,
+      f.length_empty, zero_add, or_true, le_sup_iff, f.length_Ioc, not_lt] },
+  { simp only [hac, hbc, Ioc_inter_Ioi, Ioc_diff_Ioi, f.length_Ioc, min_eq_right,
+      sup_eq_max, le_refl, Ioc_eq_empty, add_zero, max_eq_left, f.length_empty, not_lt] }
+end
+
+theorem outer_trim : f.outer.trim = f.outer :=
+begin
+  refine le_antisymm (λ s, _) (outer_measure.le_trim _),
+  rw outer_measure.trim_eq_infi,
+  refine le_infi (λ t, le_infi $ λ ht,
+    ennreal.le_of_forall_pos_le_add $ λ ε ε0 h, _),
+  rcases ennreal.exists_pos_sum_of_encodable
+    (ennreal.zero_lt_coe_iff.2 ε0) ℕ with ⟨ε', ε'0, hε⟩,
+  refine le_trans _ (add_le_add_left (le_of_lt hε) _),
+  rw ← ennreal.tsum_add,
+  choose g hg using show
+    ∀ i, ∃ s, t i ⊆ s ∧ measurable_set s ∧
+      f.outer s ≤ f.length (t i) + of_real (ε' i),
+  { intro i,
+    have := (ennreal.lt_add_right (lt_of_le_of_lt (ennreal.le_tsum i) h)
+        (ennreal.zero_lt_coe_iff.2 (ε'0 i))),
+    conv at this {to_lhs, rw length},
+    simp only [infi_lt_iff] at this,
+    rcases this with ⟨a, b, h₁, h₂⟩,
+    rw ← f.outer_Ioc at h₂,
+    exact ⟨_, h₁, measurable_set_Ioc, le_of_lt $ by simpa using h₂⟩ },
+  simp at hg,
+  apply infi_le_of_le (Union g) _,
+  apply infi_le_of_le (subset.trans ht $ Union_subset_Union (λ i, (hg i).1)) _,
+  apply infi_le_of_le (measurable_set.Union (λ i, (hg i).2.1)) _,
+  exact le_trans (f.outer.Union _) (ennreal.tsum_le_tsum $ λ i, (hg i).2.2)
+end
+
+lemma borel_le_measurable : borel ℝ ≤ f.outer.caratheodory :=
+begin
+  rw borel_eq_generate_Ioi,
+  refine measurable_space.generate_from_le _,
+  simp [f.measurable_set_Ioi] { contextual := tt }
+end
+
+/-! ### 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]`. -/
+@[irreducible] protected def measure : measure ℝ :=
+{ to_outer_measure := f.outer,
+  m_Union := λ s hs, f.outer.Union_eq_of_caratheodory $
+    λ i, f.borel_le_measurable _ (hs i),
+  trimmed := f.outer_trim }
+
+@[simp] lemma measure_Ioc (a b : ℝ) : f.measure (Ioc a b) = of_real (f b - f a) :=
+by { rw stieltjes_function.measure, exact f.outer_Ioc a b }
+
+@[simp] lemma measure_singleton (a : ℝ) : f.measure {a} = of_real (f a - f.left_lim a) :=
+begin
+  obtain ⟨u, u_mono, u_lt_a, u_lim⟩ : ∃ (u : ℕ → ℝ), strict_mono u ∧ (∀ (n : ℕ), u n < a)
+    ∧ tendsto u at_top (𝓝 a) := exists_seq_strict_mono_tendsto a,
+  have A : {a} = ⋂ n, Ioc (u n) a,
+  { refine subset.antisymm (λ x hx, by simp [mem_singleton_iff.1 hx, u_lt_a]) (λ x hx, _),
+    simp at hx,
+    have : a ≤ x := le_of_tendsto' u_lim (λ n, (hx n).1.le),
+    simp [le_antisymm this (hx 0).2] },
+  have L1 : tendsto (λ n, f.measure (Ioc (u n) a)) at_top (𝓝 (f.measure {a})),
+  { rw A,
+    refine tendsto_measure_Inter (λ n, measurable_set_Ioc) (λ m n hmn, _) _,
+    { exact Ioc_subset_Ioc (u_mono.monotone hmn) le_rfl },
+    { exact ⟨0, by simp only [measure_Ioc, ennreal.of_real_lt_top]⟩ } },
+  have L2 : tendsto (λ n, f.measure (Ioc (u n) a)) at_top (𝓝 (of_real (f a - f.left_lim a))),
+  { simp only [measure_Ioc],
+    have : tendsto (λ n, f (u n)) at_top (𝓝 (f.left_lim a)),
+    { apply (f.tendsto_left_lim a).comp,
+      exact tendsto_nhds_within_of_tendsto_nhds_of_eventually_within _ u_lim
+        (eventually_of_forall (λ n, u_lt_a n)) },
+    exact ennreal.continuous_of_real.continuous_at.tendsto.comp (tendsto_const_nhds.sub this) },
+  exact tendsto_nhds_unique L1 L2
+end
+
+@[simp] lemma measure_Icc (a b : ℝ) : f.measure (Icc a b) = of_real (f b - f.left_lim a) :=
+begin
+  rcases le_or_lt a b with hab|hab,
+  { have A : disjoint {a} (Ioc a b), by simp,
+    simp [← Icc_union_Ioc_eq_Icc le_rfl hab, -singleton_union, ← ennreal.of_real_add, f.left_lim_le,
+      measure_union A (measurable_set_singleton a) measurable_set_Ioc, f.mono hab] },
+  { simp only [hab, measure_empty, Icc_eq_empty, not_le],
+    symmetry,
+    simp [ennreal.of_real_eq_zero, f.le_left_lim hab] }
+end
+
+@[simp] lemma measure_Ioo {a b : ℝ} : f.measure (Ioo a b) = of_real (f.left_lim b - f a) :=
+begin
+  rcases le_or_lt b a with hab|hab,
+  { simp only [hab, measure_empty, Ioo_eq_empty, not_lt],
+    symmetry,
+    simp [ennreal.of_real_eq_zero, f.left_lim_le hab] },
+  { have A : disjoint (Ioo a b) {b}, by simp,
+    have D : f b - f a = (f b - f.left_lim b) + (f.left_lim b - f a), by abel,
+    have := f.measure_Ioc a b,
+    simp only [←Ioo_union_Icc_eq_Ioc hab le_rfl, measure_singleton,
+      measure_union A measurable_set_Ioo (measurable_set_singleton b), Icc_self] at this,
+    rw [D, ennreal.of_real_add, add_comm] at this,
+    { simpa only [ennreal.add_right_inj, ennreal.of_real_lt_top] },
+    { simp only [f.left_lim_le, sub_nonneg] },
+    { simp only [f.le_left_lim hab, sub_nonneg] } },
+end
+
+@[simp] lemma measure_Ico (a b : ℝ) : f.measure (Ico a b) = of_real (f.left_lim b - f.left_lim a) :=
+begin
+  rcases le_or_lt b a with hab|hab,
+  { simp only [hab, measure_empty, Ico_eq_empty, not_lt],
+    symmetry,
+    simp [ennreal.of_real_eq_zero, f.left_lim_le_left_lim hab] },
+  { have A : disjoint {a} (Ioo a b) := by simp,
+    simp [← Icc_union_Ioo_eq_Ico le_rfl hab, -singleton_union, hab.ne, f.left_lim_le,
+      measure_union A (measurable_set_singleton a) measurable_set_Ioo, f.le_left_lim hab,
+      ← ennreal.of_real_add] }
+end
+
+end stieltjes_function
diff --git a/src/topology/algebra/ordered/basic.lean b/src/topology/algebra/ordered/basic.lean
index b558775f6319a..f246ed05e607d 100644
--- a/src/topology/algebra/ordered/basic.lean
+++ b/src/topology/algebra/ordered/basic.lean
@@ -2695,6 +2695,32 @@ lemma map_cinfi_of_continuous_at_of_monotone {f : α → β} {g : γ → α}
 @map_csupr_of_continuous_at_of_monotone (order_dual α) (order_dual β) _ _ _ _ _ _ _ _ _ _
   Cf Mf.order_dual H
 
+/-- A monotone map has a limit to the left of any point `x`, equal to `Sup (f '' (Iio x))`. -/
+lemma monotone.tendsto_nhds_within_Iio
+  {α : Type*} [linear_order α] [topological_space α] [order_topology α]
+  {f : α → β} (Mf : monotone f) (x : α) :
+  tendsto f (𝓝[Iio x] x) (𝓝 (Sup (f '' (Iio x)))) :=
+begin
+  rcases eq_empty_or_nonempty (Iio x) with h|h, { simp [h] },
+  refine tendsto_order.2 ⟨λ l hl, _, λ m hm, _⟩,
+  { obtain ⟨z, zx, lz⟩ : ∃ (a : α), a < x ∧ l < f a,
+      by simpa only [mem_image, exists_prop, exists_exists_and_eq_and]
+        using exists_lt_of_lt_cSup (nonempty_image_iff.2 h) hl,
+    exact (mem_nhds_within_Iio_iff_exists_Ioo_subset' zx).2
+      ⟨z, zx, λ y hy, lz.trans_le (Mf (hy.1.le))⟩ },
+  { filter_upwards [self_mem_nhds_within],
+    assume y hy,
+    apply lt_of_le_of_lt _ hm,
+    exact le_cSup (Mf.map_bdd_above bdd_above_Iio) (mem_image_of_mem _ hy) }
+end
+
+/-- A monotone map has a limit to the right of any point `x`, equal to `Inf (f '' (Ioi x))`. -/
+lemma monotone.tendsto_nhds_within_Ioi
+  {α : Type*} [linear_order α] [topological_space α] [order_topology α]
+  {f : α → β} (Mf : monotone f) (x : α) :
+  tendsto f (𝓝[Ioi x] x) (𝓝 (Inf (f '' (Ioi x)))) :=
+@monotone.tendsto_nhds_within_Iio (order_dual β) _ _ _ (order_dual α) _ _ _ f Mf.order_dual x
+
 /-- A bounded connected subset of a conditionally complete linear order includes the open interval
 `(Inf s, Sup s)`. -/
 lemma is_connected.Ioo_cInf_cSup_subset {s : set α} (hs : is_connected s) (hb : bdd_below s)
@@ -2759,7 +2785,7 @@ begin
 end
 
 /-- A preconnected set is either one of the intervals `Icc`, `Ico`, `Ioc`, `Ioo`, `Ici`, `Ioi`,
-`Iic`, `Iio`, or `univ`, or `∅`. The converse statement requires `α` to be densely ordererd. Though
+`Iic`, `Iio`, or `univ`, or `∅`. The converse statement requires `α` to be densely ordered. Though
 one can represent `∅` as `(Inf s, Inf s)`, we include it into the list of possible cases to improve
 readability. -/
 lemma set_of_is_preconnected_subset_of_ordered :