From b3260f37e534430ea20630d2a7130e33a010a152 Mon Sep 17 00:00:00 2001
From: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Date: Thu, 6 Jan 2022 07:05:28 +0000
Subject: [PATCH] feat(measure_theory/constructions/borel_space): new lemma
 tendsto_measure_cthickening (#11009)

Prove that, when `r` tends to `0`, the measure of the `r`-thickening of a set `s` tends to the measure of `s`.
---
 .../constructions/borel_space.lean            | 40 +++++++++++++++++
 src/measure_theory/measure/measure_space.lean | 44 +++++++++++++++++++
 2 files changed, 84 insertions(+)

diff --git a/src/measure_theory/constructions/borel_space.lean b/src/measure_theory/constructions/borel_space.lean
index 20180e6b34e82..9a0acc5f4cf62 100644
--- a/src/measure_theory/constructions/borel_space.lean
+++ b/src/measure_theory/constructions/borel_space.lean
@@ -1309,6 +1309,7 @@ lemma measurable.inf_nndist {f : β → α} (hf : measurable f) {s : set α} :
   measurable (λ x, inf_nndist (f x) s) :=
 measurable_inf_nndist.comp hf
 
+section
 variables [second_countable_topology α]
 
 @[measurability]
@@ -1329,6 +1330,45 @@ lemma measurable.nndist {f g : β → α} (hf : measurable f) (hg : measurable g
   measurable (λ b, nndist (f b) (g b)) :=
 (@continuous_nndist α _).measurable2 hf hg
 
+end
+
+/-- If a set has a closed thickening with finite measure, then the measure of its `r`-closed
+thickenings converges to the measure of its closure as `r` tends to `0`. -/
+lemma tendsto_measure_cthickening {μ : measure α} {s : set α}
+  (hs : ∃ R > 0, μ (cthickening R s) ≠ ∞) :
+  tendsto (λ r, μ (cthickening r s)) (𝓝 0) (𝓝 (μ (closure s))) :=
+begin
+  have A : tendsto (λ r, μ (cthickening r s)) (𝓝[Ioi 0] 0) (𝓝 (μ (closure s))),
+  { rw closure_eq_Inter_cthickening,
+    exact tendsto_measure_bInter_gt (λ r hr, is_closed_cthickening.measurable_set)
+      (λ i j ipos ij, cthickening_mono ij _) hs },
+  have B : tendsto (λ r, μ (cthickening r s)) (𝓝[Iic 0] 0) (𝓝 (μ (closure s))),
+  { apply tendsto.congr' _ tendsto_const_nhds,
+    filter_upwards [self_mem_nhds_within],
+    assume r hr,
+    rw cthickening_of_nonpos hr },
+  convert B.sup A,
+  exact (nhds_left_sup_nhds_right' 0).symm,
+end
+
+/-- If a closed set has a closed thickening with finite measure, then the measure of its `r`-closed
+thickenings converges to its measure as `r` tends to `0`. -/
+lemma tendsto_measure_cthickening_of_is_closed {μ : measure α} {s : set α}
+  (hs : ∃ R > 0, μ (cthickening R s) ≠ ∞) (h's : is_closed s) :
+  tendsto (λ r, μ (cthickening r s)) (𝓝 0) (𝓝 (μ s)) :=
+begin
+  convert tendsto_measure_cthickening hs,
+  exact h's.closure_eq.symm
+end
+
+/-- Given a compact set in a proper space, the measure of its `r`-closed thickenings converges to
+its measure as `r` tends to `0`. -/
+lemma tendsto_measure_cthickening_of_is_compact [proper_space α] {μ : measure α}
+  [is_finite_measure_on_compacts μ] {s : set α} (hs : is_compact s) :
+  tendsto (λ r, μ (cthickening r s)) (𝓝 0) (𝓝 (μ s)) :=
+tendsto_measure_cthickening_of_is_closed
+  ⟨1, zero_lt_one, (bounded.measure_lt_top hs.bounded.cthickening).ne⟩ hs.is_closed
+
 end metric_space
 
 section emetric_space
diff --git a/src/measure_theory/measure/measure_space.lean b/src/measure_theory/measure/measure_space.lean
index 6f0a11448c5ab..9093a5b02a559 100644
--- a/src/measure_theory/measure/measure_space.lean
+++ b/src/measure_theory/measure/measure_space.lean
@@ -351,6 +351,50 @@ begin
   exact tendsto_at_top_infi (assume n m hnm, measure_mono $ hm hnm),
 end
 
+/-- The measure of the intersection of a decreasing sequence of measurable
+sets indexed by a linear order with first countable topology is the limit of the measures. -/
+lemma tendsto_measure_bInter_gt {ι : Type*} [linear_order ι] [topological_space ι]
+  [order_topology ι] [densely_ordered ι] [topological_space.first_countable_topology ι]
+  {s : ι → set α} {a : ι}
+  (hs : ∀ r > a, measurable_set (s r)) (hm : ∀ i j, a < i → i ≤ j → s i ⊆ s j)
+  (hf : ∃ r > a, μ (s r) ≠ ∞) :
+  tendsto (μ ∘ s) (𝓝[Ioi a] a) (𝓝 (μ (⋂ r > a, s r))) :=
+begin
+  refine tendsto_order.2 ⟨λ l hl, _, λ L hL, _⟩,
+  { filter_upwards [self_mem_nhds_within],
+    assume r hr,
+    exact hl.trans_le (measure_mono (bInter_subset_of_mem hr)) },
+  obtain ⟨u, u_anti, u_pos, u_lim⟩ : ∃ (u : ℕ → ι), strict_anti u ∧ (∀ (n : ℕ), a < u n)
+    ∧ tendsto u at_top (𝓝 a),
+  { rcases hf with ⟨r, ar, hr⟩,
+    rcases exists_seq_strict_anti_tendsto' ar with ⟨w, w_anti, w_mem, w_lim⟩,
+    exact ⟨w, w_anti, λ n, (w_mem n).1, w_lim⟩ },
+  have A : tendsto (μ ∘ (s ∘ u)) at_top (𝓝(μ (⋂ n, s (u n)))),
+  { refine tendsto_measure_Inter (λ n, hs _ (u_pos n)) _ _,
+    { assume m n hmn,
+      exact hm _ _ (u_pos n) (u_anti.antitone hmn) },
+    { rcases hf with ⟨r, rpos, hr⟩,
+      obtain ⟨n, hn⟩ : ∃ (n : ℕ), u n < r := ((tendsto_order.1 u_lim).2 r rpos).exists,
+      refine ⟨n, ne_of_lt (lt_of_le_of_lt _ hr.lt_top)⟩,
+      exact measure_mono (hm _ _ (u_pos n) hn.le) } },
+  have B : (⋂ n, s (u n)) = (⋂ r > a, s r),
+  { apply subset.antisymm,
+    { simp only [subset_Inter_iff, gt_iff_lt],
+      assume r rpos,
+      obtain ⟨n, hn⟩ : ∃ n, u n < r := ((tendsto_order.1 u_lim).2 _ rpos).exists,
+      exact subset.trans (Inter_subset _ n) (hm (u n) r (u_pos n) hn.le) },
+    { simp only [subset_Inter_iff, gt_iff_lt],
+      assume n,
+      apply bInter_subset_of_mem,
+      exact u_pos n } },
+  rw B at A,
+  obtain ⟨n, hn⟩ : ∃ n, μ (s (u n)) < L := ((tendsto_order.1 A).2 _ hL).exists,
+  have : Ioc a (u n) ∈ 𝓝[>] a := Ioc_mem_nhds_within_Ioi ⟨le_rfl, u_pos n⟩,
+  filter_upwards [this],
+  assume r hr,
+  exact lt_of_le_of_lt (measure_mono (hm _ _ hr.1 hr.2)) hn,
+end
+
 /-- One direction of the **Borel-Cantelli lemma**: if (sᵢ) is a sequence of sets such
 that `∑ μ sᵢ` is finite, then the limit superior of the `sᵢ` is a null set. -/
 lemma measure_limsup_eq_zero {s : ℕ → set α} (hs : ∑' i, μ (s i) ≠ ∞) : μ (limsup at_top s) = 0 :=