feat(measure_theory/stieltjes_measure): Stieltjes measures associated to monotone functions (#8266)

Given a monotone right-continuous real function `f`, there exists a measure giving mass `f b - f a` to the interval `(a, b]`. These measures are called Stieltjes measures, and are especially important in probability theory. The real Lebesgue measure is a particular case of this construction, for `f x = x`. This PR extends the already existing construction of the Lebesgue measure to cover all Stieltjes measures.

Author: sgouezel

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'

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 _ _)

src/measure_theory/measure/lebesgue.lean

@@ -4,262 +4,54 @@ 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
 
 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]