From eb829bc0e2c40a27548017b70b16c2458b01d744 Mon Sep 17 00:00:00 2001
From: JakobStiefel <jakobstiefel@hotmail.de>
Date: Fri, 6 Dec 2024 17:52:36 +0100
Subject: [PATCH 01/18] add RegularityCompacts and necessary lemmas

---
 Mathlib/Analysis/SpecificLimits/Basic.lean    | 38 +++++++++++++++++++
 .../MeasureTheory/Measure/MeasureSpace.lean   | 17 +++++++++
 Mathlib/Topology/Instances/ENNReal.lean       | 29 ++++++++++++++
 3 files changed, 84 insertions(+)

diff --git a/Mathlib/Analysis/SpecificLimits/Basic.lean b/Mathlib/Analysis/SpecificLimits/Basic.lean
index d86c021d2cfec..78895cf0dac5f 100644
--- a/Mathlib/Analysis/SpecificLimits/Basic.lean
+++ b/Mathlib/Analysis/SpecificLimits/Basic.lean
@@ -382,6 +382,44 @@ theorem ENNReal.tsum_geometric (r : ℝ≥0∞) : ∑' n : ℕ, r ^ n = (1 - r)
 theorem ENNReal.tsum_geometric_add_one (r : ℝ≥0∞) : ∑' n : ℕ, r ^ (n + 1) = r * (1 - r)⁻¹ := by
   simp only [_root_.pow_succ', ENNReal.tsum_mul_left, ENNReal.tsum_geometric]
 
+/-- Given x > 0, there is a sequence of positive reals summing to x. -/
+theorem NNReal.exists_seq_pos_summable_eq (x : NNReal) (hx : 0 < x) :
+    ∃ f : ℕ → NNReal, (∀ n, 0 < f n) ∧ Summable f ∧ ∑' n, f n = x := by
+  have h : ∑' n : ℕ, x / 2 / 2 ^ n = x := by
+    rw [NNReal.eq_iff, NNReal.coe_tsum]
+    push_cast
+    exact tsum_geometric_two' x
+  refine ⟨fun n : ℕ ↦ x / 2 / 2 ^ n, fun n ↦ by positivity, ?_, h⟩
+  by_contra h1
+  rw [tsum_eq_zero_of_not_summable h1] at h
+  exact hx.ne h
+
+/-- Given some x > 0, there is a sequence of positive reals summing to x. -/
+theorem ENNReal.exists_seq_pos_eq (x : ℝ≥0∞) (hx : 0 < x) :
+    ∃ f : ℕ → ℝ≥0∞, (∀ n, 0 < f n) ∧ ∑' n, f n = x := by
+  by_cases hx_top : x = ∞
+  · use fun _ ↦ ∞
+    simp [forall_const, ENNReal.tsum_top, hx_top, and_self]
+  suffices ∃ f : ℕ → NNReal, (∀ n, 0 < f n) ∧ Summable f ∧ ∑' n, f n = x.toNNReal by
+    obtain ⟨f, hf_pos, hf_sum, hf_eq⟩ := this
+    refine ⟨fun n ↦ f n, ?_, ?_⟩
+    · exact fun n ↦ ENNReal.coe_pos.mpr (hf_pos n)
+    · rw [← ENNReal.coe_tsum hf_sum, hf_eq, ENNReal.coe_toNNReal hx_top]
+  exact NNReal.exists_seq_pos_summable_eq x.toNNReal (ENNReal.toNNReal_pos hx.ne' hx_top)
+
+/-- Given some x > 0, there is a sequence of positive reals summing to something less than x. -/
+theorem ENNReal.exists_seq_pos_lt (x : ℝ≥0∞) (hx : 0 < x) :
+    ∃ f : ℕ → ℝ≥0∞, (∀ n, 0 < f n) ∧ ∑' n, f n < x := by
+  by_cases hx_top : x = ∞
+  · obtain ⟨f, hf_pos, hf_eq⟩ : ∃ f : ℕ → ℝ≥0∞, (∀ n, 0 < f n) ∧ ∑' n, f n = 1 :=
+      ENNReal.exists_seq_pos_eq 1 zero_lt_one
+    refine ⟨f, hf_pos, ?_⟩
+    simp only [hf_eq, hx_top, ENNReal.one_lt_top]
+  · obtain ⟨f, hf⟩ := ENNReal.exists_seq_pos_eq (x / 2) (ENNReal.half_pos hx.ne')
+    refine ⟨f, hf.1, ?_⟩
+    rw [hf.2]
+    exact ENNReal.half_lt_self hx.ne' hx_top
+
 end Geometric
 
 /-!
diff --git a/Mathlib/MeasureTheory/Measure/MeasureSpace.lean b/Mathlib/MeasureTheory/Measure/MeasureSpace.lean
index 92a5dcb5aa47b..960c7ca939ec9 100644
--- a/Mathlib/MeasureTheory/Measure/MeasureSpace.lean
+++ b/Mathlib/MeasureTheory/Measure/MeasureSpace.lean
@@ -626,6 +626,23 @@ theorem tendsto_measure_iInter_le {α ι : Type*} {_ : MeasurableSpace α} {μ :
   exact tendsto_atTop_iInf
     fun i j hij ↦ measure_mono <| biInter_subset_biInter_left fun k hki ↦ le_trans hki hij
 
+/-- Some version of continuity of a measure in the emptyset using the intersection along a set of
+sets. -/
+theorem exists_measure_iInter_lt {α ι : Type*} {_ : MeasurableSpace α} {μ : Measure α}
+    [Nonempty ι] [SemilatticeSup ι] [Countable ι] {f : ι → Set α}
+    (hm : ∀ i, NullMeasurableSet (f i) μ) {ε : ℝ≥0∞} (hε : 0 < ε) (hfin : ∃ i, μ (f i) ≠ ∞)
+    (hfem : ⋂ n, f n = ∅) : ∃ m, μ (⋂ n ≤ m, f n) < ε := by
+  let F m := μ (⋂ n ≤ m, f n)
+  have hFAnti : Antitone F :=
+      fun i j hij => measure_mono (biInter_subset_biInter_left fun k hki => le_trans hki hij)
+  suffices Filter.Tendsto F Filter.atTop (𝓝 0) by
+    rw [ENNReal.tendsto_atTop_zero_iff_lt_of_antitone hFAnti] at this
+    exact this ε hε
+  have hzero : μ (⋂ n, f n) = 0 := by
+    simp only [hfem, measure_empty]
+  rw [← hzero]
+  exact tendsto_measure_iInter_le hm hfin
+
 /-- 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. -/
 theorem tendsto_measure_biInter_gt {ι : Type*} [LinearOrder ι] [TopologicalSpace ι]
diff --git a/Mathlib/Topology/Instances/ENNReal.lean b/Mathlib/Topology/Instances/ENNReal.lean
index 418685fd8c5d4..74df527096cba 100644
--- a/Mathlib/Topology/Instances/ENNReal.lean
+++ b/Mathlib/Topology/Instances/ENNReal.lean
@@ -280,6 +280,35 @@ protected theorem tendsto_atTop_zero [Nonempty β] [SemilatticeSup β] {f : β 
     Tendsto f atTop (𝓝 0) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, f n ≤ ε :=
   .trans (atTop_basis.tendsto_iff nhds_zero_basis_Iic) (by simp only [true_and]; rfl)
 
+theorem tendsto_atTop_zero_iff_le_of_antitone {β : Type*} [Nonempty β] [SemilatticeSup β]
+    {f : β → ℝ≥0∞} (hf : Antitone f) :
+    Filter.Tendsto f Filter.atTop (𝓝 0) ↔ ∀ ε, 0 < ε → ∃ n : β, f n ≤ ε := by
+  rw [ENNReal.tendsto_atTop_zero]
+  refine ⟨fun h ↦ fun ε hε ↦ ?_, fun h ↦ fun ε hε ↦ ?_⟩
+  · obtain ⟨n, hn⟩ := h ε hε
+    exact ⟨n, hn n le_rfl⟩
+  · obtain ⟨n, hn⟩ := h ε hε
+    exact ⟨n, fun m hm ↦ (hf hm).trans hn⟩
+
+theorem tendsto_atTop_zero_iff_lt_of_antitone {β : Type*} [Nonempty β] [SemilatticeSup β]
+    {f : β → ℝ≥0∞} (hf : Antitone f) :
+    Filter.Tendsto f Filter.atTop (𝓝 0) ↔ ∀ ε, 0 < ε → ∃ n : β, f n < ε := by
+  rw [ENNReal.tendsto_atTop_zero_iff_le_of_antitone hf]
+  constructor <;> intro h ε hε
+  · obtain ⟨n, hn⟩ := h (min 1 (ε / 2))
+      (lt_min_iff.mpr ⟨zero_lt_one, (ENNReal.div_pos_iff.mpr ⟨ne_of_gt hε, ENNReal.two_ne_top⟩)⟩)
+    · refine ⟨n, hn.trans_lt ?_⟩
+      by_cases hε_top : ε = ∞
+      · rw [hε_top]
+        exact (min_le_left _ _).trans_lt ENNReal.one_lt_top
+      refine (min_le_right _ _).trans_lt ?_
+      rw [ENNReal.div_lt_iff (Or.inr hε.ne') (Or.inr hε_top)]
+      conv_lhs => rw [← mul_one ε]
+      rw [ENNReal.mul_lt_mul_left hε.ne' hε_top]
+      norm_num
+  · obtain ⟨n, hn⟩ := h ε hε
+    exact ⟨n, hn.le⟩
+
 theorem tendsto_sub : ∀ {a b : ℝ≥0∞}, (a ≠ ∞ ∨ b ≠ ∞) →
     Tendsto (fun p : ℝ≥0∞ × ℝ≥0∞ => p.1 - p.2) (𝓝 (a, b)) (𝓝 (a - b))
   | ∞, ∞, h => by simp only [ne_eq, not_true_eq_false, or_self] at h

From 16547cc8d8320c4bb2b066af9b697a8239b926cd Mon Sep 17 00:00:00 2001
From: JakobStiefel <jakobstiefel@hotmail.de>
Date: Fri, 6 Dec 2024 17:53:23 +0100
Subject: [PATCH 02/18] add RegularityCompacts

---
 .../Measure/RegularityCompacts.lean           | 230 ++++++++++++++++++
 1 file changed, 230 insertions(+)
 create mode 100644 Mathlib/MeasureTheory/Measure/RegularityCompacts.lean

diff --git a/Mathlib/MeasureTheory/Measure/RegularityCompacts.lean b/Mathlib/MeasureTheory/Measure/RegularityCompacts.lean
new file mode 100644
index 0000000000000..218155f35c234
--- /dev/null
+++ b/Mathlib/MeasureTheory/Measure/RegularityCompacts.lean
@@ -0,0 +1,230 @@
+/-
+Copyright (c) 2023 Rémy Degenne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémy Degenne, Peter Pfaffelhuber
+-/
+import Mathlib.Analysis.SpecificLimits.Basic
+import Mathlib.MeasureTheory.MeasurableSpace.Defs
+import Mathlib.MeasureTheory.Measure.Regular
+import Mathlib.Topology.MetricSpace.Polish
+
+/-!
+# Inner regularity of Measures wrt compact sets
+In this file we show that a `FiniteMeasure P`  on a `PseudoEMetricSpace E` is inner regular with
+respect to compact sets: `theorem inner_regularWRT_isCompact_of_complete_countable`.
+-/
+
+open Set MeasureTheory
+
+open scoped ENNReal Topology
+
+variable {α : Type*}
+
+section Topology
+
+namespace UniformSpace
+
+lemma _root_.MeasurableSet.ball {_ : MeasurableSpace α} (x : α)
+    {s : Set (α × α)} (hs : MeasurableSet s) :
+    MeasurableSet (UniformSpace.ball x s) := measurable_prod_mk_left hs
+
+/-- Given a family of points `xs n`, a family of entourages `V n` of the diagonal and a family of
+natural numbers `u n`, the intersection over `n` of the `V n`-neighborhood of `xs 1, ..., xs (u n)`.
+Designed to be relatively compact when `V n` tends to the diagonal. -/
+def interUnionBalls (xs : ℕ → α) (u : ℕ → ℕ) (V : ℕ → Set (α × α)) : Set α :=
+  ⋂ n, ⋃ m ≤ u n, UniformSpace.ball (xs m) (Prod.swap ⁻¹' V n)
+
+lemma totallyBounded_interUnionBalls [UniformSpace α] {p : ℕ → Prop} {U : ℕ → Set (α × α)}
+    (H : (uniformity α).HasBasis p U) (xs : ℕ → α) (u : ℕ → ℕ) :
+    TotallyBounded (interUnionBalls xs u U) := by
+  rw [Filter.HasBasis.totallyBounded_iff H]
+  intro i _
+  have h_subset : interUnionBalls xs u U
+      ⊆ ⋃ m ≤ u i, UniformSpace.ball (xs m) (Prod.swap ⁻¹' U i) :=
+    fun x hx ↦ Set.mem_iInter.1 hx i
+  classical
+  refine ⟨Finset.image xs (Finset.range (u i + 1)), Finset.finite_toSet _, fun x hx ↦ ?_⟩
+  simp only [Finset.coe_image, Finset.coe_range, mem_image, mem_Iio, iUnion_exists, biUnion_and',
+    iUnion_iUnion_eq_right, Nat.lt_succ_iff]
+  exact h_subset hx
+
+/-- The construction `interUnionBalls` is used to have a relatively compact set. -/
+theorem isCompact_closure_interUnionBalls [UniformSpace α] {p : ℕ → Prop} {U : ℕ → Set (α × α)}
+    (H : (uniformity α).HasBasis p U) [CompleteSpace α] (xs : ℕ → α) (u : ℕ → ℕ) :
+    IsCompact (closure (interUnionBalls xs u U)) := by
+  rw [isCompact_iff_totallyBounded_isComplete]
+  refine ⟨TotallyBounded.closure ?_, isClosed_closure.isComplete⟩
+  exact totallyBounded_interUnionBalls H xs u
+
+theorem _root_.MeasureTheory.measure_compl_interUnionBalls_le {_ : MeasurableSpace α}
+    (μ : Measure α) (xs : ℕ → α) (u : ℕ → ℕ) (V : ℕ → Set (α × α)) :
+    μ (UniformSpace.interUnionBalls xs u V)ᶜ ≤
+      ∑' n, μ (⋃ m ≤ u n, UniformSpace.ball (xs m) (Prod.swap ⁻¹' V n))ᶜ := by
+  rw [UniformSpace.interUnionBalls, Set.compl_iInter]
+  exact measure_iUnion_le _
+
+end UniformSpace
+
+end Topology
+
+
+namespace MeasureTheory
+
+variable [MeasurableSpace α] {μ : Measure α}
+
+theorem innerRegularWRT_isCompact_closure_iff [TopologicalSpace α] [R1Space α] :
+    μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed ↔ μ.InnerRegularWRT IsCompact IsClosed := by
+  constructor <;> intro h A hA r hr
+  · rcases h hA r hr with ⟨K, ⟨hK1, hK2, hK3⟩⟩
+    exact ⟨closure K, closure_minimal hK1 hA, hK2, hK3.trans_le (measure_mono subset_closure)⟩
+  · rcases h hA r hr with ⟨K, ⟨hK1, hK2, hK3⟩⟩
+    refine ⟨closure K, closure_minimal hK1 hA, ?_, ?_⟩
+    · simpa only [closure_closure, Function.comp_apply] using hK2.closure
+    · exact hK3.trans_le (measure_mono subset_closure)
+
+lemma innerRegularWRT_isCompact_isClosed_iff_innerRegularWRT_isCompact_closure
+    [TopologicalSpace α] [R1Space α] :
+    μ.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s) IsClosed
+      ↔ μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed := by
+  constructor <;> intro h A hA r hr
+  · obtain ⟨K, hK1, ⟨hK2, _⟩, hK4⟩ := h hA r hr
+    refine ⟨K, hK1, ?_, hK4⟩
+    simp only [closure_closure, Function.comp_apply]
+    exact hK2.closure
+  · obtain ⟨K, hK1, hK2, hK3⟩ := h hA r hr
+    refine ⟨closure K, closure_minimal hK1 hA, ?_, ?_⟩
+    · simpa only [isClosed_closure, and_true]
+    · exact hK3.trans_le (measure_mono subset_closure)
+
+lemma innerRegularWRT_isCompact_isClosed_iff [TopologicalSpace α] [R1Space α] :
+    μ.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s) IsClosed
+      ↔ μ.InnerRegularWRT IsCompact IsClosed :=
+  innerRegularWRT_isCompact_isClosed_iff_innerRegularWRT_isCompact_closure.trans
+    innerRegularWRT_isCompact_closure_iff
+
+theorem innerRegularWRT_of_exists_compl_lt {p q : Set α → Prop} (hpq : ∀ A B, p A → q B → p (A ∩ B))
+    (hμ : ∀ ε, 0 < ε → ∃ K, p K ∧ μ Kᶜ < ε) :
+    μ.InnerRegularWRT p q := by
+  intro A hA r hr
+  obtain ⟨K, hK, hK_subset, h_lt⟩ : ∃ K, p K ∧ K ⊆ A ∧ μ (A \ K) < μ A - r := by
+    obtain ⟨K', hpK', hK'_lt⟩ := hμ (μ A - r) (tsub_pos_of_lt hr)
+    refine ⟨K' ∩ A, hpq K' A hpK' hA, inter_subset_right, ?_⟩
+    · refine (measure_mono fun x ↦ ?_).trans_lt hK'_lt
+      simp only [diff_inter_self_eq_diff, mem_diff, mem_compl_iff, and_imp, imp_self, imp_true_iff]
+  refine ⟨K, hK_subset, hK, ?_⟩
+  have h_lt' : μ A - μ K < μ A - r := le_measure_diff.trans_lt h_lt
+  exact lt_of_tsub_lt_tsub_left h_lt'
+
+theorem innerRegularWRT_isCompact_closure_of_univ [TopologicalSpace α]
+    (hμ : ∀ ε, 0 < ε → ∃ K, IsCompact (closure K) ∧ μ (Kᶜ) < ε) :
+    μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed := by
+  refine innerRegularWRT_of_exists_compl_lt (fun s t hs ht ↦ ?_) hμ
+  have : IsCompact (closure s ∩ t) := hs.inter_right ht
+  refine this.of_isClosed_subset isClosed_closure ?_
+  refine (closure_inter_subset_inter_closure _ _).trans_eq ?_
+  rw [IsClosed.closure_eq ht]
+
+theorem exists_isCompact_closure_measure_lt_of_complete_countable [UniformSpace α] [CompleteSpace α]
+    [SecondCountableTopology α] [(uniformity α).IsCountablyGenerated]
+    [OpensMeasurableSpace α] (P : Measure α) [IsFiniteMeasure P] (ε : ℝ≥0∞) (hε : 0 < ε) :
+    ∃ K, IsCompact (closure K) ∧ P Kᶜ < ε := by
+  cases isEmpty_or_nonempty α
+  case inl =>
+    refine ⟨∅, by simp, ?_⟩
+    rw [← Set.univ_eq_empty_iff.mpr]
+    · simpa only [compl_univ, measure_empty, ENNReal.coe_pos] using hε
+    · assumption
+  case inr =>
+    let seq := TopologicalSpace.denseSeq α
+    have hseq_dense : DenseRange seq := TopologicalSpace.denseRange_denseSeq α
+    obtain ⟨t : ℕ → Set (α × α),
+        hto : ∀ i, t i ∈ (uniformity α).sets ∧ IsOpen (t i) ∧ SymmetricRel (t i),
+        h_basis : (uniformity α).HasAntitoneBasis t⟩ :=
+      (@uniformity_hasBasis_open_symmetric α _).exists_antitone_subbasis
+    let f : ℕ → ℕ → Set α := fun n m ↦ UniformSpace.ball (seq m) (t n)
+    have h_univ n : (⋃ m, f n m) = univ := hseq_dense.iUnion_uniformity_ball (hto n).1
+    have h3 n (ε : ℝ≥0∞) (hε : 0 < ε) : ∃ m, P (⋂ m' ≤ m, (f n m')ᶜ) < ε := by
+      refine exists_measure_iInter_lt (fun m ↦ ?_) hε ⟨0, measure_ne_top P _⟩ ?_
+      · exact ((IsOpen.measurableSet (hto n).2.1).ball _).compl.nullMeasurableSet
+      · rw [← compl_iUnion, h_univ, compl_univ]
+    choose! s' s'bound using h3
+    rcases ENNReal.exists_seq_pos_lt ε hε with ⟨δ, hδ1, hδ2⟩
+    classical
+    let u : ℕ → ℕ := fun n ↦ s' n (δ n)
+    let A := UniformSpace.interUnionBalls seq u t
+    refine ⟨A, UniformSpace.isCompact_closure_interUnionBalls h_basis.toHasBasis seq u, ?_⟩
+    refine ((measure_compl_interUnionBalls_le P seq u t).trans ?_).trans_lt hδ2
+    refine ENNReal.tsum_le_tsum (fun n ↦ ?_)
+    have h'' n : Prod.swap ⁻¹' t n = t n := SymmetricRel.eq (hto n).2.2
+    simp only [h'', compl_iUnion, ge_iff_le]
+    exact (s'bound n (δ n) (hδ1 n)).le
+
+theorem innerRegularWRT_isCompact_closure_of_complete_countable [UniformSpace α] [CompleteSpace α]
+    [SecondCountableTopology α] [(uniformity α).IsCountablyGenerated]
+    [OpensMeasurableSpace α] (P : Measure α) [IsFiniteMeasure P] :
+    P.InnerRegularWRT (IsCompact ∘ closure) IsClosed :=
+  innerRegularWRT_isCompact_closure_of_univ
+    (exists_isCompact_closure_measure_lt_of_complete_countable P)
+
+theorem innerRegularWRT_isCompact_isClosed_of_complete_countable [UniformSpace α] [CompleteSpace α]
+    [SecondCountableTopology α] [(uniformity α).IsCountablyGenerated]
+    [OpensMeasurableSpace α] (P : Measure α) [IsFiniteMeasure P] :
+    P.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s) IsClosed := by
+  have : R1Space α := by
+    exact instR1Space
+  rw [innerRegularWRT_isCompact_isClosed_iff_innerRegularWRT_isCompact_closure]
+  exact innerRegularWRT_isCompact_closure_of_complete_countable P
+
+theorem innerRegularWRT_isCompact_of_complete_countable [UniformSpace α] [CompleteSpace α]
+    [SecondCountableTopology α] [(uniformity α).IsCountablyGenerated]
+    [OpensMeasurableSpace α] (P : Measure α) [IsFiniteMeasure P] :
+    P.InnerRegularWRT IsCompact IsClosed := by
+  rw [← innerRegularWRT_isCompact_closure_iff]
+  exact innerRegularWRT_isCompact_closure_of_complete_countable P
+
+theorem innerRegularWRT_isCompact_isClosed_isOpen_of_complete_countable [PseudoEMetricSpace α]
+    [CompleteSpace α] [SecondCountableTopology α] [OpensMeasurableSpace α]
+    (P : Measure α) [IsFiniteMeasure P] :
+    P.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s) IsOpen :=
+  (innerRegularWRT_isCompact_isClosed_of_complete_countable P).trans
+    (Measure.InnerRegularWRT.of_pseudoMetrizableSpace P)
+
+theorem innerRegularWRT_isCompact_isOpen_of_complete_countable [PseudoEMetricSpace α]
+    [CompleteSpace α] [SecondCountableTopology α] [OpensMeasurableSpace α]
+    (P : Measure α) [IsFiniteMeasure P] :
+    P.InnerRegularWRT IsCompact IsOpen :=
+  (innerRegularWRT_isCompact_of_complete_countable P).trans
+    (Measure.InnerRegularWRT.of_pseudoMetrizableSpace P)
+
+theorem InnerRegularCompactLTTop_of_complete_countable [PseudoEMetricSpace α]
+    [CompleteSpace α] [SecondCountableTopology α] [BorelSpace α]
+    (P : Measure α) [IsFiniteMeasure P] :
+    P.InnerRegularCompactLTTop := by
+  refine ⟨Measure.InnerRegularWRT.measurableSet_of_isOpen ?_ ?_⟩
+  · exact innerRegularWRT_isCompact_isOpen_of_complete_countable P
+  · exact fun s t hs_compact ht_open ↦ hs_compact.inter_right ht_open.isClosed_compl
+
+theorem innerRegular_isCompact_isClosed_measurableSet_of_complete_countable [PseudoEMetricSpace α]
+    [CompleteSpace α] [SecondCountableTopology α] [BorelSpace α]
+    (P : Measure α) [IsFiniteMeasure P] :
+    P.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s) MeasurableSet := by
+  suffices P.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s)
+      fun s ↦ MeasurableSet s ∧ P s ≠ ∞ by
+    convert this
+    simp only [eq_iff_iff, iff_self_and]
+    exact fun _ ↦ measure_ne_top P _
+  refine Measure.InnerRegularWRT.measurableSet_of_isOpen ?_ ?_
+  · exact innerRegularWRT_isCompact_isClosed_isOpen_of_complete_countable P
+  · rintro s t ⟨hs_compact, hs_closed⟩ ht_open
+    rw [diff_eq]
+    exact ⟨hs_compact.inter_right ht_open.isClosed_compl,
+      hs_closed.inter (isClosed_compl_iff.mpr ht_open)⟩
+
+/-- On a Polish space, any finite measure is regular with respect to compact and closed sets. -/
+theorem PolishSpace.innerRegular_isCompact_measurableSet [TopologicalSpace α] [PolishSpace α]
+    [BorelSpace α] (μ : Measure α) [IsFiniteMeasure μ] :
+    μ.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s) MeasurableSet := by
+  letI := upgradePolishSpace α
+  exact innerRegular_isCompact_isClosed_measurableSet_of_complete_countable μ
+
+end MeasureTheory

From 842530e0fa70f5d737652e677a3dbafe32d1b4e9 Mon Sep 17 00:00:00 2001
From: JakobStiefel <jakobstiefel@hotmail.de>
Date: Fri, 6 Dec 2024 18:29:15 +0100
Subject: [PATCH 03/18] update mk_all

---
 Mathlib.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib.lean b/Mathlib.lean
index 9269de2ed24fa..08887c86a51c2 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -3718,6 +3718,7 @@ import Mathlib.MeasureTheory.Measure.Portmanteau
 import Mathlib.MeasureTheory.Measure.ProbabilityMeasure
 import Mathlib.MeasureTheory.Measure.Prod
 import Mathlib.MeasureTheory.Measure.Regular
+import Mathlib.MeasureTheory.Measure.RegularityCompacts
 import Mathlib.MeasureTheory.Measure.Restrict
 import Mathlib.MeasureTheory.Measure.SeparableMeasure
 import Mathlib.MeasureTheory.Measure.Stieltjes

From 8b770f0ecbd8102957390264db5207ab986041be Mon Sep 17 00:00:00 2001
From: JakobStiefel <73285902+JakobStiefel@users.noreply.github.com>
Date: Tue, 10 Dec 2024 12:08:58 +0100
Subject: [PATCH 04/18] clarify docstring

---
 Mathlib/MeasureTheory/Measure/RegularityCompacts.lean | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

diff --git a/Mathlib/MeasureTheory/Measure/RegularityCompacts.lean b/Mathlib/MeasureTheory/Measure/RegularityCompacts.lean
index 218155f35c234..fa75028f6df9b 100644
--- a/Mathlib/MeasureTheory/Measure/RegularityCompacts.lean
+++ b/Mathlib/MeasureTheory/Measure/RegularityCompacts.lean
@@ -9,9 +9,14 @@ import Mathlib.MeasureTheory.Measure.Regular
 import Mathlib.Topology.MetricSpace.Polish
 
 /-!
-# Inner regularity of Measures wrt compact sets
-In this file we show that a `FiniteMeasure P`  on a `PseudoEMetricSpace E` is inner regular with
-respect to compact sets: `theorem inner_regularWRT_isCompact_of_complete_countable`.
+# Inner regularity of finite measures
+
+The main result of this file is `theorem inner_regularWRT_isCompact_of_complete_countable`: 
+A `FiniteMeasure P` on a `PseudoEMetricSpace E` and `CompleteSpace E` with 
+`SecondCountableTopology E` is inner regular with respect to compact sets.
+
+Finite measures on Polish spaces are an important special case, which makes the result 
+`theorem PolishSpace.innerRegular_isCompact_measurableSet` an important result in probability.
 -/
 
 open Set MeasureTheory

From c7917a860981fb93b5b8f06c10fb535e750317cf Mon Sep 17 00:00:00 2001
From: JakobStiefel <73285902+JakobStiefel@users.noreply.github.com>
Date: Tue, 10 Dec 2024 12:11:56 +0100
Subject: [PATCH 05/18] remove blank space

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
---
 Mathlib/MeasureTheory/Measure/RegularityCompacts.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/MeasureTheory/Measure/RegularityCompacts.lean b/Mathlib/MeasureTheory/Measure/RegularityCompacts.lean
index fa75028f6df9b..5123febaae81b 100644
--- a/Mathlib/MeasureTheory/Measure/RegularityCompacts.lean
+++ b/Mathlib/MeasureTheory/Measure/RegularityCompacts.lean
@@ -11,8 +11,8 @@ import Mathlib.Topology.MetricSpace.Polish
 /-!
 # Inner regularity of finite measures
 
-The main result of this file is `theorem inner_regularWRT_isCompact_of_complete_countable`: 
-A `FiniteMeasure P` on a `PseudoEMetricSpace E` and `CompleteSpace E` with 
+The main result of this file is `theorem inner_regularWRT_isCompact_of_complete_countable`:
+A `FiniteMeasure P` on a `PseudoEMetricSpace E` and `CompleteSpace E` with
 `SecondCountableTopology E` is inner regular with respect to compact sets.
 
 Finite measures on Polish spaces are an important special case, which makes the result 

From 2fdf7e7adabd4964ac753f62fbcbfc502ce5066c Mon Sep 17 00:00:00 2001
From: JakobStiefel <73285902+JakobStiefel@users.noreply.github.com>
Date: Tue, 10 Dec 2024 12:12:13 +0100
Subject: [PATCH 06/18] remove blank space

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
---
 Mathlib/MeasureTheory/Measure/RegularityCompacts.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/MeasureTheory/Measure/RegularityCompacts.lean b/Mathlib/MeasureTheory/Measure/RegularityCompacts.lean
index 5123febaae81b..52085cea011cb 100644
--- a/Mathlib/MeasureTheory/Measure/RegularityCompacts.lean
+++ b/Mathlib/MeasureTheory/Measure/RegularityCompacts.lean
@@ -15,7 +15,7 @@ The main result of this file is `theorem inner_regularWRT_isCompact_of_complete_
 A `FiniteMeasure P` on a `PseudoEMetricSpace E` and `CompleteSpace E` with
 `SecondCountableTopology E` is inner regular with respect to compact sets.
 
-Finite measures on Polish spaces are an important special case, which makes the result 
+Finite measures on Polish spaces are an important special case, which makes the result
 `theorem PolishSpace.innerRegular_isCompact_measurableSet` an important result in probability.
 -/
 

From d28f6945bcf60e42e32f8053e9184a4f86772032 Mon Sep 17 00:00:00 2001
From: JakobStiefel <73285902+JakobStiefel@users.noreply.github.com>
Date: Thu, 12 Dec 2024 16:30:20 +0100
Subject: [PATCH 07/18] remove assumption Nonempty \iota

---
 Mathlib/MeasureTheory/Measure/MeasureSpace.lean | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/Mathlib/MeasureTheory/Measure/MeasureSpace.lean b/Mathlib/MeasureTheory/Measure/MeasureSpace.lean
index 960c7ca939ec9..8ac55f54b6fbc 100644
--- a/Mathlib/MeasureTheory/Measure/MeasureSpace.lean
+++ b/Mathlib/MeasureTheory/Measure/MeasureSpace.lean
@@ -629,14 +629,15 @@ theorem tendsto_measure_iInter_le {α ι : Type*} {_ : MeasurableSpace α} {μ :
 /-- Some version of continuity of a measure in the emptyset using the intersection along a set of
 sets. -/
 theorem exists_measure_iInter_lt {α ι : Type*} {_ : MeasurableSpace α} {μ : Measure α}
-    [Nonempty ι] [SemilatticeSup ι] [Countable ι] {f : ι → Set α}
+    [SemilatticeSup ι] [Countable ι] {f : ι → Set α}
     (hm : ∀ i, NullMeasurableSet (f i) μ) {ε : ℝ≥0∞} (hε : 0 < ε) (hfin : ∃ i, μ (f i) ≠ ∞)
     (hfem : ⋂ n, f n = ∅) : ∃ m, μ (⋂ n ≤ m, f n) < ε := by
   let F m := μ (⋂ n ≤ m, f n)
   have hFAnti : Antitone F :=
       fun i j hij => measure_mono (biInter_subset_biInter_left fun k hki => le_trans hki hij)
   suffices Filter.Tendsto F Filter.atTop (𝓝 0) by
-    rw [ENNReal.tendsto_atTop_zero_iff_lt_of_antitone hFAnti] at this
+    rw [@ENNReal.tendsto_atTop_zero_iff_lt_of_antitone
+         _ (nonempty_of_exists hfin) _ _ hFAnti] at this
     exact this ε hε
   have hzero : μ (⋂ n, f n) = 0 := by
     simp only [hfem, measure_empty]

From 864722904d72ed8b029f668f52c3ca24258e7a5b Mon Sep 17 00:00:00 2001
From: JakobStiefel <73285902+JakobStiefel@users.noreply.github.com>
Date: Thu, 12 Dec 2024 17:03:11 +0100
Subject: [PATCH 08/18] add and adjust docstrings

---
 .../Measure/RegularityCompacts.lean           | 20 ++++++++++++++++---
 1 file changed, 17 insertions(+), 3 deletions(-)

diff --git a/Mathlib/MeasureTheory/Measure/RegularityCompacts.lean b/Mathlib/MeasureTheory/Measure/RegularityCompacts.lean
index 52085cea011cb..87a0b40c6c414 100644
--- a/Mathlib/MeasureTheory/Measure/RegularityCompacts.lean
+++ b/Mathlib/MeasureTheory/Measure/RegularityCompacts.lean
@@ -12,8 +12,9 @@ import Mathlib.Topology.MetricSpace.Polish
 # Inner regularity of finite measures
 
 The main result of this file is `theorem inner_regularWRT_isCompact_of_complete_countable`:
-A `FiniteMeasure P` on a `PseudoEMetricSpace E` and `CompleteSpace E` with
-`SecondCountableTopology E` is inner regular with respect to compact sets.
+A finite measure `μ` on a `PseudoEMetricSpace E` and `CompleteSpace E` with
+`SecondCountableTopology E` is inner regular with respect to compact sets. In other 
+words, a finite measure on such a space is a tight measure.
 
 Finite measures on Polish spaces are an important special case, which makes the result
 `theorem PolishSpace.innerRegular_isCompact_measurableSet` an important result in probability.
@@ -107,6 +108,11 @@ lemma innerRegularWRT_isCompact_isClosed_iff [TopologicalSpace α] [R1Space α]
   innerRegularWRT_isCompact_isClosed_iff_innerRegularWRT_isCompact_closure.trans
     innerRegularWRT_isCompact_closure_iff
 
+/--
+If predicate `p` is preserved under intersections with sets satisfying predicate `q`, and sets
+satisfying `p` exploit the space arbitrarily well, then `μ` is inner regular with respect to 
+predicates `p` and `q`.
+-/
 theorem innerRegularWRT_of_exists_compl_lt {p q : Set α → Prop} (hpq : ∀ A B, p A → q B → p (A ∩ B))
     (hμ : ∀ ε, 0 < ε → ∃ K, p K ∧ μ Kᶜ < ε) :
     μ.InnerRegularWRT p q := by
@@ -201,6 +207,11 @@ theorem innerRegularWRT_isCompact_isOpen_of_complete_countable [PseudoEMetricSpa
   (innerRegularWRT_isCompact_of_complete_countable P).trans
     (Measure.InnerRegularWRT.of_pseudoMetrizableSpace P)
 
+/--
+A finite measure `μ` on a `PseudoEMetricSpace E` and `CompleteSpace E` with
+`SecondCountableTopology E` is inner regular with respect to compact sets. In other 
+words, a finite measure on such a space is a tight measure.
+-/
 theorem InnerRegularCompactLTTop_of_complete_countable [PseudoEMetricSpace α]
     [CompleteSpace α] [SecondCountableTopology α] [BorelSpace α]
     (P : Measure α) [IsFiniteMeasure P] :
@@ -225,7 +236,10 @@ theorem innerRegular_isCompact_isClosed_measurableSet_of_complete_countable [Pse
     exact ⟨hs_compact.inter_right ht_open.isClosed_compl,
       hs_closed.inter (isClosed_compl_iff.mpr ht_open)⟩
 
-/-- On a Polish space, any finite measure is regular with respect to compact and closed sets. -/
+/--
+On a Polish space, any finite measure is regular with respect to compact and closed sets. In
+particular, a finite measure on a Polish space is a tight measure.
+-/
 theorem PolishSpace.innerRegular_isCompact_measurableSet [TopologicalSpace α] [PolishSpace α]
     [BorelSpace α] (μ : Measure α) [IsFiniteMeasure μ] :
     μ.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s) MeasurableSet := by

From 2bab2349b288e79c753f72ca9f66ef6fe17da41b Mon Sep 17 00:00:00 2001
From: JakobStiefel <73285902+JakobStiefel@users.noreply.github.com>
Date: Thu, 12 Dec 2024 17:29:36 +0100
Subject: [PATCH 09/18] adjust theorem names

---
 .../Measure/RegularityCompacts.lean           | 40 +++++++++----------
 1 file changed, 19 insertions(+), 21 deletions(-)

diff --git a/Mathlib/MeasureTheory/Measure/RegularityCompacts.lean b/Mathlib/MeasureTheory/Measure/RegularityCompacts.lean
index 87a0b40c6c414..3b9c2fde5226f 100644
--- a/Mathlib/MeasureTheory/Measure/RegularityCompacts.lean
+++ b/Mathlib/MeasureTheory/Measure/RegularityCompacts.lean
@@ -11,9 +11,9 @@ import Mathlib.Topology.MetricSpace.Polish
 /-!
 # Inner regularity of finite measures
 
-The main result of this file is `theorem inner_regularWRT_isCompact_of_complete_countable`:
+The main result of this file is `theorem InnerRegularCompactLTTop`:
 A finite measure `μ` on a `PseudoEMetricSpace E` and `CompleteSpace E` with
-`SecondCountableTopology E` is inner regular with respect to compact sets. In other 
+`SecondCountableTopology E` is inner regular with respect to compact sets. In other
 words, a finite measure on such a space is a tight measure.
 
 Finite measures on Polish spaces are an important special case, which makes the result
@@ -135,7 +135,7 @@ theorem innerRegularWRT_isCompact_closure_of_univ [TopologicalSpace α]
   refine (closure_inter_subset_inter_closure _ _).trans_eq ?_
   rw [IsClosed.closure_eq ht]
 
-theorem exists_isCompact_closure_measure_lt_of_complete_countable [UniformSpace α] [CompleteSpace α]
+theorem exists_isCompact_closure_measure_compl_lt [UniformSpace α] [CompleteSpace α]
     [SecondCountableTopology α] [(uniformity α).IsCountablyGenerated]
     [OpensMeasurableSpace α] (P : Measure α) [IsFiniteMeasure P] (ε : ℝ≥0∞) (hε : 0 < ε) :
     ∃ K, IsCompact (closure K) ∧ P Kᶜ < ε := by
@@ -170,57 +170,55 @@ theorem exists_isCompact_closure_measure_lt_of_complete_countable [UniformSpace
     simp only [h'', compl_iUnion, ge_iff_le]
     exact (s'bound n (δ n) (hδ1 n)).le
 
-theorem innerRegularWRT_isCompact_closure_of_complete_countable [UniformSpace α] [CompleteSpace α]
+theorem innerRegularWRT_isCompact_closure [UniformSpace α] [CompleteSpace α]
     [SecondCountableTopology α] [(uniformity α).IsCountablyGenerated]
     [OpensMeasurableSpace α] (P : Measure α) [IsFiniteMeasure P] :
     P.InnerRegularWRT (IsCompact ∘ closure) IsClosed :=
   innerRegularWRT_isCompact_closure_of_univ
-    (exists_isCompact_closure_measure_lt_of_complete_countable P)
+    (exists_isCompact_closure_measure_compl_lt P)
 
-theorem innerRegularWRT_isCompact_isClosed_of_complete_countable [UniformSpace α] [CompleteSpace α]
+theorem innerRegularWRT_isCompact_isClosed [UniformSpace α] [CompleteSpace α]
     [SecondCountableTopology α] [(uniformity α).IsCountablyGenerated]
     [OpensMeasurableSpace α] (P : Measure α) [IsFiniteMeasure P] :
     P.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s) IsClosed := by
-  have : R1Space α := by
-    exact instR1Space
   rw [innerRegularWRT_isCompact_isClosed_iff_innerRegularWRT_isCompact_closure]
-  exact innerRegularWRT_isCompact_closure_of_complete_countable P
+  exact innerRegularWRT_isCompact_closure P
 
-theorem innerRegularWRT_isCompact_of_complete_countable [UniformSpace α] [CompleteSpace α]
+theorem innerRegularWRT_isCompact [UniformSpace α] [CompleteSpace α]
     [SecondCountableTopology α] [(uniformity α).IsCountablyGenerated]
     [OpensMeasurableSpace α] (P : Measure α) [IsFiniteMeasure P] :
     P.InnerRegularWRT IsCompact IsClosed := by
   rw [← innerRegularWRT_isCompact_closure_iff]
-  exact innerRegularWRT_isCompact_closure_of_complete_countable P
+  exact innerRegularWRT_isCompact_closure P
 
-theorem innerRegularWRT_isCompact_isClosed_isOpen_of_complete_countable [PseudoEMetricSpace α]
+theorem innerRegularWRT_isCompact_isClosed_isOpen [PseudoEMetricSpace α]
     [CompleteSpace α] [SecondCountableTopology α] [OpensMeasurableSpace α]
     (P : Measure α) [IsFiniteMeasure P] :
     P.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s) IsOpen :=
-  (innerRegularWRT_isCompact_isClosed_of_complete_countable P).trans
+  (innerRegularWRT_isCompact_isClosed P).trans
     (Measure.InnerRegularWRT.of_pseudoMetrizableSpace P)
 
-theorem innerRegularWRT_isCompact_isOpen_of_complete_countable [PseudoEMetricSpace α]
+theorem innerRegularWRT_isCompact_isOpen [PseudoEMetricSpace α]
     [CompleteSpace α] [SecondCountableTopology α] [OpensMeasurableSpace α]
     (P : Measure α) [IsFiniteMeasure P] :
     P.InnerRegularWRT IsCompact IsOpen :=
-  (innerRegularWRT_isCompact_of_complete_countable P).trans
+  (innerRegularWRT_isCompact P).trans
     (Measure.InnerRegularWRT.of_pseudoMetrizableSpace P)
 
 /--
 A finite measure `μ` on a `PseudoEMetricSpace E` and `CompleteSpace E` with
-`SecondCountableTopology E` is inner regular with respect to compact sets. In other 
+`SecondCountableTopology E` is inner regular with respect to compact sets. In other
 words, a finite measure on such a space is a tight measure.
 -/
-theorem InnerRegularCompactLTTop_of_complete_countable [PseudoEMetricSpace α]
+theorem InnerRegularCompactLTTop [PseudoEMetricSpace α]
     [CompleteSpace α] [SecondCountableTopology α] [BorelSpace α]
     (P : Measure α) [IsFiniteMeasure P] :
     P.InnerRegularCompactLTTop := by
   refine ⟨Measure.InnerRegularWRT.measurableSet_of_isOpen ?_ ?_⟩
-  · exact innerRegularWRT_isCompact_isOpen_of_complete_countable P
+  · exact innerRegularWRT_isCompact_isOpen P
   · exact fun s t hs_compact ht_open ↦ hs_compact.inter_right ht_open.isClosed_compl
 
-theorem innerRegular_isCompact_isClosed_measurableSet_of_complete_countable [PseudoEMetricSpace α]
+theorem innerRegular_isCompact_isClosed_measurableSet [PseudoEMetricSpace α]
     [CompleteSpace α] [SecondCountableTopology α] [BorelSpace α]
     (P : Measure α) [IsFiniteMeasure P] :
     P.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s) MeasurableSet := by
@@ -230,7 +228,7 @@ theorem innerRegular_isCompact_isClosed_measurableSet_of_complete_countable [Pse
     simp only [eq_iff_iff, iff_self_and]
     exact fun _ ↦ measure_ne_top P _
   refine Measure.InnerRegularWRT.measurableSet_of_isOpen ?_ ?_
-  · exact innerRegularWRT_isCompact_isClosed_isOpen_of_complete_countable P
+  · exact innerRegularWRT_isCompact_isClosed_isOpen P
   · rintro s t ⟨hs_compact, hs_closed⟩ ht_open
     rw [diff_eq]
     exact ⟨hs_compact.inter_right ht_open.isClosed_compl,
@@ -244,6 +242,6 @@ theorem PolishSpace.innerRegular_isCompact_measurableSet [TopologicalSpace α] [
     [BorelSpace α] (μ : Measure α) [IsFiniteMeasure μ] :
     μ.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s) MeasurableSet := by
   letI := upgradePolishSpace α
-  exact innerRegular_isCompact_isClosed_measurableSet_of_complete_countable μ
+  exact innerRegular_isCompact_isClosed_measurableSet μ
 
 end MeasureTheory

From 0f7aac42cfafb6332ee41b73e94293ec9f49307c Mon Sep 17 00:00:00 2001
From: JakobStiefel <73285902+JakobStiefel@users.noreply.github.com>
Date: Thu, 12 Dec 2024 17:48:17 +0100
Subject: [PATCH 10/18] move interUnionBalls to Cauchy.lean

---
 Mathlib/Topology/UniformSpace/Cauchy.lean | 28 +++++++++++++++++++++++
 1 file changed, 28 insertions(+)

diff --git a/Mathlib/Topology/UniformSpace/Cauchy.lean b/Mathlib/Topology/UniformSpace/Cauchy.lean
index b8ae4225ddef4..e482affe0f2b0 100644
--- a/Mathlib/Topology/UniformSpace/Cauchy.lean
+++ b/Mathlib/Topology/UniformSpace/Cauchy.lean
@@ -645,6 +645,34 @@ theorem CauchySeq.totallyBounded_range {s : ℕ → α} (hs : CauchySeq s) :
   rcases le_total m n with hm | hm
   exacts [⟨m, hm, refl_mem_uniformity ha⟩, ⟨n, le_refl n, hn m hm n le_rfl⟩]
 
+/-- Given a family of points `xs n`, a family of entourages `V n` of the diagonal and a family of
+natural numbers `u n`, the intersection over `n` of the `V n`-neighborhood of `xs 1, ..., xs (u n)`.
+Designed to be relatively compact when `V n` tends to the diagonal. -/
+def interUnionBalls (xs : ℕ → α) (u : ℕ → ℕ) (V : ℕ → Set (α × α)) : Set α :=
+  ⋂ n, ⋃ m ≤ u n, UniformSpace.ball (xs m) (Prod.swap ⁻¹' V n)
+
+lemma totallyBounded_interUnionBalls {p : ℕ → Prop} {U : ℕ → Set (α × α)}
+    (H : (uniformity α).HasBasis p U) (xs : ℕ → α) (u : ℕ → ℕ) :
+    TotallyBounded (interUnionBalls xs u U) := by
+  rw [Filter.HasBasis.totallyBounded_iff H]
+  intro i _
+  have h_subset : interUnionBalls xs u U
+      ⊆ ⋃ m ≤ u i, UniformSpace.ball (xs m) (Prod.swap ⁻¹' U i) :=
+    fun x hx ↦ Set.mem_iInter.1 hx i
+  classical
+  refine ⟨Finset.image xs (Finset.range (u i + 1)), Finset.finite_toSet _, fun x hx ↦ ?_⟩
+  simp only [Finset.coe_image, Finset.coe_range, mem_image, mem_Iio, iUnion_exists, biUnion_and',
+    iUnion_iUnion_eq_right, Nat.lt_succ_iff]
+  exact h_subset hx
+
+/-- The construction `interUnionBalls` is used to have a relatively compact set. -/
+theorem isCompact_closure_interUnionBalls {p : ℕ → Prop} {U : ℕ → Set (α × α)}
+    (H : (uniformity α).HasBasis p U) [CompleteSpace α] (xs : ℕ → α) (u : ℕ → ℕ) :
+    IsCompact (closure (interUnionBalls xs u U)) := by
+  rw [isCompact_iff_totallyBounded_isComplete]
+  refine ⟨TotallyBounded.closure ?_, isClosed_closure.isComplete⟩
+  exact totallyBounded_interUnionBalls H xs u
+
 /-!
 ### Sequentially complete space
 

From 2e369113a00774c43f6b99333c8abc93bc8d8482 Mon Sep 17 00:00:00 2001
From: JakobStiefel <73285902+JakobStiefel@users.noreply.github.com>
Date: Thu, 12 Dec 2024 17:53:46 +0100
Subject: [PATCH 11/18] remove interUnionBalls from RegularityCompacts.lean

---
 .../Measure/RegularityCompacts.lean           | 61 ++-----------------
 1 file changed, 5 insertions(+), 56 deletions(-)

diff --git a/Mathlib/MeasureTheory/Measure/RegularityCompacts.lean b/Mathlib/MeasureTheory/Measure/RegularityCompacts.lean
index 3b9c2fde5226f..b3dcefa186fb6 100644
--- a/Mathlib/MeasureTheory/Measure/RegularityCompacts.lean
+++ b/Mathlib/MeasureTheory/Measure/RegularityCompacts.lean
@@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Rémy Degenne, Peter Pfaffelhuber
 -/
 import Mathlib.Analysis.SpecificLimits.Basic
-import Mathlib.MeasureTheory.MeasurableSpace.Defs
 import Mathlib.MeasureTheory.Measure.Regular
 import Mathlib.Topology.MetricSpace.Polish
+import Mathlib.Topology.UniformSpace.Cauchy
 
 /-!
 # Inner regularity of finite measures
@@ -22,61 +22,11 @@ Finite measures on Polish spaces are an important special case, which makes the
 
 open Set MeasureTheory
 
-open scoped ENNReal Topology
-
-variable {α : Type*}
-
-section Topology
-
-namespace UniformSpace
-
-lemma _root_.MeasurableSet.ball {_ : MeasurableSpace α} (x : α)
-    {s : Set (α × α)} (hs : MeasurableSet s) :
-    MeasurableSet (UniformSpace.ball x s) := measurable_prod_mk_left hs
-
-/-- Given a family of points `xs n`, a family of entourages `V n` of the diagonal and a family of
-natural numbers `u n`, the intersection over `n` of the `V n`-neighborhood of `xs 1, ..., xs (u n)`.
-Designed to be relatively compact when `V n` tends to the diagonal. -/
-def interUnionBalls (xs : ℕ → α) (u : ℕ → ℕ) (V : ℕ → Set (α × α)) : Set α :=
-  ⋂ n, ⋃ m ≤ u n, UniformSpace.ball (xs m) (Prod.swap ⁻¹' V n)
-
-lemma totallyBounded_interUnionBalls [UniformSpace α] {p : ℕ → Prop} {U : ℕ → Set (α × α)}
-    (H : (uniformity α).HasBasis p U) (xs : ℕ → α) (u : ℕ → ℕ) :
-    TotallyBounded (interUnionBalls xs u U) := by
-  rw [Filter.HasBasis.totallyBounded_iff H]
-  intro i _
-  have h_subset : interUnionBalls xs u U
-      ⊆ ⋃ m ≤ u i, UniformSpace.ball (xs m) (Prod.swap ⁻¹' U i) :=
-    fun x hx ↦ Set.mem_iInter.1 hx i
-  classical
-  refine ⟨Finset.image xs (Finset.range (u i + 1)), Finset.finite_toSet _, fun x hx ↦ ?_⟩
-  simp only [Finset.coe_image, Finset.coe_range, mem_image, mem_Iio, iUnion_exists, biUnion_and',
-    iUnion_iUnion_eq_right, Nat.lt_succ_iff]
-  exact h_subset hx
-
-/-- The construction `interUnionBalls` is used to have a relatively compact set. -/
-theorem isCompact_closure_interUnionBalls [UniformSpace α] {p : ℕ → Prop} {U : ℕ → Set (α × α)}
-    (H : (uniformity α).HasBasis p U) [CompleteSpace α] (xs : ℕ → α) (u : ℕ → ℕ) :
-    IsCompact (closure (interUnionBalls xs u U)) := by
-  rw [isCompact_iff_totallyBounded_isComplete]
-  refine ⟨TotallyBounded.closure ?_, isClosed_closure.isComplete⟩
-  exact totallyBounded_interUnionBalls H xs u
-
-theorem _root_.MeasureTheory.measure_compl_interUnionBalls_le {_ : MeasurableSpace α}
-    (μ : Measure α) (xs : ℕ → α) (u : ℕ → ℕ) (V : ℕ → Set (α × α)) :
-    μ (UniformSpace.interUnionBalls xs u V)ᶜ ≤
-      ∑' n, μ (⋃ m ≤ u n, UniformSpace.ball (xs m) (Prod.swap ⁻¹' V n))ᶜ := by
-  rw [UniformSpace.interUnionBalls, Set.compl_iInter]
-  exact measure_iUnion_le _
-
-end UniformSpace
-
-end Topology
-
+open scoped ENNReal
 
 namespace MeasureTheory
 
-variable [MeasurableSpace α] {μ : Measure α}
+variable {α : Type*} [MeasurableSpace α] {μ : Measure α}
 
 theorem innerRegularWRT_isCompact_closure_iff [TopologicalSpace α] [R1Space α] :
     μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed ↔ μ.InnerRegularWRT IsCompact IsClosed := by
@@ -110,7 +60,7 @@ lemma innerRegularWRT_isCompact_isClosed_iff [TopologicalSpace α] [R1Space α]
 
 /--
 If predicate `p` is preserved under intersections with sets satisfying predicate `q`, and sets
-satisfying `p` exploit the space arbitrarily well, then `μ` is inner regular with respect to 
+satisfying `p` exploit the space arbitrarily well, then `μ` is inner regular with respect to
 predicates `p` and `q`.
 -/
 theorem innerRegularWRT_of_exists_compl_lt {p q : Set α → Prop} (hpq : ∀ A B, p A → q B → p (A ∩ B))
@@ -162,8 +112,7 @@ theorem exists_isCompact_closure_measure_compl_lt [UniformSpace α] [CompleteSpa
     rcases ENNReal.exists_seq_pos_lt ε hε with ⟨δ, hδ1, hδ2⟩
     classical
     let u : ℕ → ℕ := fun n ↦ s' n (δ n)
-    let A := UniformSpace.interUnionBalls seq u t
-    refine ⟨A, UniformSpace.isCompact_closure_interUnionBalls h_basis.toHasBasis seq u, ?_⟩
+    refine ⟨interUnionBalls seq u t, isCompact_closure_interUnionBalls h_basis.toHasBasis seq u, ?_⟩
     refine ((measure_compl_interUnionBalls_le P seq u t).trans ?_).trans_lt hδ2
     refine ENNReal.tsum_le_tsum (fun n ↦ ?_)
     have h'' n : Prod.swap ⁻¹' t n = t n := SymmetricRel.eq (hto n).2.2

From f39b2c3b65ef59026ff36c6066106a0b8bfdc498 Mon Sep 17 00:00:00 2001
From: JakobStiefel <73285902+JakobStiefel@users.noreply.github.com>
Date: Thu, 12 Dec 2024 18:05:15 +0100
Subject: [PATCH 12/18] remove measure_compl_interUnionBalls_le

---
 Mathlib/MeasureTheory/Measure/RegularityCompacts.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/Mathlib/MeasureTheory/Measure/RegularityCompacts.lean b/Mathlib/MeasureTheory/Measure/RegularityCompacts.lean
index b3dcefa186fb6..33c29812e1977 100644
--- a/Mathlib/MeasureTheory/Measure/RegularityCompacts.lean
+++ b/Mathlib/MeasureTheory/Measure/RegularityCompacts.lean
@@ -113,7 +113,8 @@ theorem exists_isCompact_closure_measure_compl_lt [UniformSpace α] [CompleteSpa
     classical
     let u : ℕ → ℕ := fun n ↦ s' n (δ n)
     refine ⟨interUnionBalls seq u t, isCompact_closure_interUnionBalls h_basis.toHasBasis seq u, ?_⟩
-    refine ((measure_compl_interUnionBalls_le P seq u t).trans ?_).trans_lt hδ2
+    rw [interUnionBalls, Set.compl_iInter]
+    refine ((measure_iUnion_le _).trans ?_).trans_lt hδ2
     refine ENNReal.tsum_le_tsum (fun n ↦ ?_)
     have h'' n : Prod.swap ⁻¹' t n = t n := SymmetricRel.eq (hto n).2.2
     simp only [h'', compl_iUnion, ge_iff_le]

From e3a82c6219ca22c71ead073371ab7d6cd6bd8be1 Mon Sep 17 00:00:00 2001
From: JakobStiefel <73285902+JakobStiefel@users.noreply.github.com>
Date: Thu, 12 Dec 2024 18:11:33 +0100
Subject: [PATCH 13/18] remove measurableSet.ball

---
 Mathlib/MeasureTheory/Measure/RegularityCompacts.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/MeasureTheory/Measure/RegularityCompacts.lean b/Mathlib/MeasureTheory/Measure/RegularityCompacts.lean
index 33c29812e1977..b0bd20e4231fc 100644
--- a/Mathlib/MeasureTheory/Measure/RegularityCompacts.lean
+++ b/Mathlib/MeasureTheory/Measure/RegularityCompacts.lean
@@ -106,7 +106,7 @@ theorem exists_isCompact_closure_measure_compl_lt [UniformSpace α] [CompleteSpa
     have h_univ n : (⋃ m, f n m) = univ := hseq_dense.iUnion_uniformity_ball (hto n).1
     have h3 n (ε : ℝ≥0∞) (hε : 0 < ε) : ∃ m, P (⋂ m' ≤ m, (f n m')ᶜ) < ε := by
       refine exists_measure_iInter_lt (fun m ↦ ?_) hε ⟨0, measure_ne_top P _⟩ ?_
-      · exact ((IsOpen.measurableSet (hto n).2.1).ball _).compl.nullMeasurableSet
+      · exact (measurable_prod_mk_left (IsOpen.measurableSet (hto n).2.1)).compl.nullMeasurableSet
       · rw [← compl_iUnion, h_univ, compl_univ]
     choose! s' s'bound using h3
     rcases ENNReal.exists_seq_pos_lt ε hε with ⟨δ, hδ1, hδ2⟩

From ed853b720a25b52720dd6fb473bca45dc03efe25 Mon Sep 17 00:00:00 2001
From: JakobStiefel <jakobstiefel@hotmail.de>
Date: Thu, 12 Dec 2024 18:37:44 +0100
Subject: [PATCH 14/18] review process

---
 .../MeasureTheory/Measure/MeasureSpace.lean   |  5 +-
 .../Measure/RegularityCompacts.lean           | 70 +++----------------
 Mathlib/Topology/UniformSpace/Cauchy.lean     | 28 ++++++++
 3 files changed, 41 insertions(+), 62 deletions(-)

diff --git a/Mathlib/MeasureTheory/Measure/MeasureSpace.lean b/Mathlib/MeasureTheory/Measure/MeasureSpace.lean
index 960c7ca939ec9..624732f284174 100644
--- a/Mathlib/MeasureTheory/Measure/MeasureSpace.lean
+++ b/Mathlib/MeasureTheory/Measure/MeasureSpace.lean
@@ -629,14 +629,15 @@ theorem tendsto_measure_iInter_le {α ι : Type*} {_ : MeasurableSpace α} {μ :
 /-- Some version of continuity of a measure in the emptyset using the intersection along a set of
 sets. -/
 theorem exists_measure_iInter_lt {α ι : Type*} {_ : MeasurableSpace α} {μ : Measure α}
-    [Nonempty ι] [SemilatticeSup ι] [Countable ι] {f : ι → Set α}
+    [SemilatticeSup ι] [Countable ι] {f : ι → Set α}
     (hm : ∀ i, NullMeasurableSet (f i) μ) {ε : ℝ≥0∞} (hε : 0 < ε) (hfin : ∃ i, μ (f i) ≠ ∞)
     (hfem : ⋂ n, f n = ∅) : ∃ m, μ (⋂ n ≤ m, f n) < ε := by
   let F m := μ (⋂ n ≤ m, f n)
   have hFAnti : Antitone F :=
       fun i j hij => measure_mono (biInter_subset_biInter_left fun k hki => le_trans hki hij)
   suffices Filter.Tendsto F Filter.atTop (𝓝 0) by
-    rw [ENNReal.tendsto_atTop_zero_iff_lt_of_antitone hFAnti] at this
+    rw [@ENNReal.tendsto_atTop_zero_iff_lt_of_antitone
+      _ (nonempty_of_exists hfin) _ _ hFAnti] at this
     exact this ε hε
   have hzero : μ (⋂ n, f n) = 0 := by
     simp only [hfem, measure_empty]
diff --git a/Mathlib/MeasureTheory/Measure/RegularityCompacts.lean b/Mathlib/MeasureTheory/Measure/RegularityCompacts.lean
index 218155f35c234..7cc0b3ba557e8 100644
--- a/Mathlib/MeasureTheory/Measure/RegularityCompacts.lean
+++ b/Mathlib/MeasureTheory/Measure/RegularityCompacts.lean
@@ -4,73 +4,24 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Rémy Degenne, Peter Pfaffelhuber
 -/
 import Mathlib.Analysis.SpecificLimits.Basic
-import Mathlib.MeasureTheory.MeasurableSpace.Defs
+--import Mathlib.MeasureTheory.MeasurableSpace.Ball
 import Mathlib.MeasureTheory.Measure.Regular
 import Mathlib.Topology.MetricSpace.Polish
+import Mathlib.Topology.UniformSpace.Cauchy
 
 /-!
 # Inner regularity of Measures wrt compact sets
-In this file we show that a `FiniteMeasure P`  on a `PseudoEMetricSpace E` is inner regular with
+In this file we show that a finite measure `μ`  on a `PseudoEMetricSpace E` is inner regular with
 respect to compact sets: `theorem inner_regularWRT_isCompact_of_complete_countable`.
 -/
 
 open Set MeasureTheory
 
-open scoped ENNReal Topology
-
-variable {α : Type*}
-
-section Topology
-
-namespace UniformSpace
-
-lemma _root_.MeasurableSet.ball {_ : MeasurableSpace α} (x : α)
-    {s : Set (α × α)} (hs : MeasurableSet s) :
-    MeasurableSet (UniformSpace.ball x s) := measurable_prod_mk_left hs
-
-/-- Given a family of points `xs n`, a family of entourages `V n` of the diagonal and a family of
-natural numbers `u n`, the intersection over `n` of the `V n`-neighborhood of `xs 1, ..., xs (u n)`.
-Designed to be relatively compact when `V n` tends to the diagonal. -/
-def interUnionBalls (xs : ℕ → α) (u : ℕ → ℕ) (V : ℕ → Set (α × α)) : Set α :=
-  ⋂ n, ⋃ m ≤ u n, UniformSpace.ball (xs m) (Prod.swap ⁻¹' V n)
-
-lemma totallyBounded_interUnionBalls [UniformSpace α] {p : ℕ → Prop} {U : ℕ → Set (α × α)}
-    (H : (uniformity α).HasBasis p U) (xs : ℕ → α) (u : ℕ → ℕ) :
-    TotallyBounded (interUnionBalls xs u U) := by
-  rw [Filter.HasBasis.totallyBounded_iff H]
-  intro i _
-  have h_subset : interUnionBalls xs u U
-      ⊆ ⋃ m ≤ u i, UniformSpace.ball (xs m) (Prod.swap ⁻¹' U i) :=
-    fun x hx ↦ Set.mem_iInter.1 hx i
-  classical
-  refine ⟨Finset.image xs (Finset.range (u i + 1)), Finset.finite_toSet _, fun x hx ↦ ?_⟩
-  simp only [Finset.coe_image, Finset.coe_range, mem_image, mem_Iio, iUnion_exists, biUnion_and',
-    iUnion_iUnion_eq_right, Nat.lt_succ_iff]
-  exact h_subset hx
-
-/-- The construction `interUnionBalls` is used to have a relatively compact set. -/
-theorem isCompact_closure_interUnionBalls [UniformSpace α] {p : ℕ → Prop} {U : ℕ → Set (α × α)}
-    (H : (uniformity α).HasBasis p U) [CompleteSpace α] (xs : ℕ → α) (u : ℕ → ℕ) :
-    IsCompact (closure (interUnionBalls xs u U)) := by
-  rw [isCompact_iff_totallyBounded_isComplete]
-  refine ⟨TotallyBounded.closure ?_, isClosed_closure.isComplete⟩
-  exact totallyBounded_interUnionBalls H xs u
-
-theorem _root_.MeasureTheory.measure_compl_interUnionBalls_le {_ : MeasurableSpace α}
-    (μ : Measure α) (xs : ℕ → α) (u : ℕ → ℕ) (V : ℕ → Set (α × α)) :
-    μ (UniformSpace.interUnionBalls xs u V)ᶜ ≤
-      ∑' n, μ (⋃ m ≤ u n, UniformSpace.ball (xs m) (Prod.swap ⁻¹' V n))ᶜ := by
-  rw [UniformSpace.interUnionBalls, Set.compl_iInter]
-  exact measure_iUnion_le _
-
-end UniformSpace
-
-end Topology
-
+open scoped ENNReal
 
 namespace MeasureTheory
 
-variable [MeasurableSpace α] {μ : Measure α}
+variable {α : Type*} [MeasurableSpace α] {μ : Measure α}
 
 theorem innerRegularWRT_isCompact_closure_iff [TopologicalSpace α] [R1Space α] :
     μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed ↔ μ.InnerRegularWRT IsCompact IsClosed := by
@@ -145,15 +96,16 @@ theorem exists_isCompact_closure_measure_lt_of_complete_countable [UniformSpace
     have h_univ n : (⋃ m, f n m) = univ := hseq_dense.iUnion_uniformity_ball (hto n).1
     have h3 n (ε : ℝ≥0∞) (hε : 0 < ε) : ∃ m, P (⋂ m' ≤ m, (f n m')ᶜ) < ε := by
       refine exists_measure_iInter_lt (fun m ↦ ?_) hε ⟨0, measure_ne_top P _⟩ ?_
-      · exact ((IsOpen.measurableSet (hto n).2.1).ball _).compl.nullMeasurableSet
+      · exact (measurable_prod_mk_left (IsOpen.measurableSet (hto n).2.1)).compl.nullMeasurableSet
       · rw [← compl_iUnion, h_univ, compl_univ]
     choose! s' s'bound using h3
     rcases ENNReal.exists_seq_pos_lt ε hε with ⟨δ, hδ1, hδ2⟩
     classical
     let u : ℕ → ℕ := fun n ↦ s' n (δ n)
-    let A := UniformSpace.interUnionBalls seq u t
-    refine ⟨A, UniformSpace.isCompact_closure_interUnionBalls h_basis.toHasBasis seq u, ?_⟩
-    refine ((measure_compl_interUnionBalls_le P seq u t).trans ?_).trans_lt hδ2
+    let A := interUnionBalls seq u t
+    refine ⟨interUnionBalls seq u t, isCompact_closure_interUnionBalls h_basis.toHasBasis seq u, ?_⟩
+    rw [interUnionBalls, Set.compl_iInter]
+    refine ((measure_iUnion_le _).trans ?_).trans_lt hδ2
     refine ENNReal.tsum_le_tsum (fun n ↦ ?_)
     have h'' n : Prod.swap ⁻¹' t n = t n := SymmetricRel.eq (hto n).2.2
     simp only [h'', compl_iUnion, ge_iff_le]
@@ -170,8 +122,6 @@ theorem innerRegularWRT_isCompact_isClosed_of_complete_countable [UniformSpace 
     [SecondCountableTopology α] [(uniformity α).IsCountablyGenerated]
     [OpensMeasurableSpace α] (P : Measure α) [IsFiniteMeasure P] :
     P.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s) IsClosed := by
-  have : R1Space α := by
-    exact instR1Space
   rw [innerRegularWRT_isCompact_isClosed_iff_innerRegularWRT_isCompact_closure]
   exact innerRegularWRT_isCompact_closure_of_complete_countable P
 
diff --git a/Mathlib/Topology/UniformSpace/Cauchy.lean b/Mathlib/Topology/UniformSpace/Cauchy.lean
index b8ae4225ddef4..e482affe0f2b0 100644
--- a/Mathlib/Topology/UniformSpace/Cauchy.lean
+++ b/Mathlib/Topology/UniformSpace/Cauchy.lean
@@ -645,6 +645,34 @@ theorem CauchySeq.totallyBounded_range {s : ℕ → α} (hs : CauchySeq s) :
   rcases le_total m n with hm | hm
   exacts [⟨m, hm, refl_mem_uniformity ha⟩, ⟨n, le_refl n, hn m hm n le_rfl⟩]
 
+/-- Given a family of points `xs n`, a family of entourages `V n` of the diagonal and a family of
+natural numbers `u n`, the intersection over `n` of the `V n`-neighborhood of `xs 1, ..., xs (u n)`.
+Designed to be relatively compact when `V n` tends to the diagonal. -/
+def interUnionBalls (xs : ℕ → α) (u : ℕ → ℕ) (V : ℕ → Set (α × α)) : Set α :=
+  ⋂ n, ⋃ m ≤ u n, UniformSpace.ball (xs m) (Prod.swap ⁻¹' V n)
+
+lemma totallyBounded_interUnionBalls {p : ℕ → Prop} {U : ℕ → Set (α × α)}
+    (H : (uniformity α).HasBasis p U) (xs : ℕ → α) (u : ℕ → ℕ) :
+    TotallyBounded (interUnionBalls xs u U) := by
+  rw [Filter.HasBasis.totallyBounded_iff H]
+  intro i _
+  have h_subset : interUnionBalls xs u U
+      ⊆ ⋃ m ≤ u i, UniformSpace.ball (xs m) (Prod.swap ⁻¹' U i) :=
+    fun x hx ↦ Set.mem_iInter.1 hx i
+  classical
+  refine ⟨Finset.image xs (Finset.range (u i + 1)), Finset.finite_toSet _, fun x hx ↦ ?_⟩
+  simp only [Finset.coe_image, Finset.coe_range, mem_image, mem_Iio, iUnion_exists, biUnion_and',
+    iUnion_iUnion_eq_right, Nat.lt_succ_iff]
+  exact h_subset hx
+
+/-- The construction `interUnionBalls` is used to have a relatively compact set. -/
+theorem isCompact_closure_interUnionBalls {p : ℕ → Prop} {U : ℕ → Set (α × α)}
+    (H : (uniformity α).HasBasis p U) [CompleteSpace α] (xs : ℕ → α) (u : ℕ → ℕ) :
+    IsCompact (closure (interUnionBalls xs u U)) := by
+  rw [isCompact_iff_totallyBounded_isComplete]
+  refine ⟨TotallyBounded.closure ?_, isClosed_closure.isComplete⟩
+  exact totallyBounded_interUnionBalls H xs u
+
 /-!
 ### Sequentially complete space
 

From 82d8bae8fb0ae3cfea8f5b5ad450ffb88d730851 Mon Sep 17 00:00:00 2001
From: JakobStiefel <jakobstiefel@hotmail.de>
Date: Thu, 12 Dec 2024 18:50:56 +0100
Subject: [PATCH 15/18] merge

---
 .../MeasureTheory/Measure/RegularityCompacts.lean  | 14 --------------
 1 file changed, 14 deletions(-)

diff --git a/Mathlib/MeasureTheory/Measure/RegularityCompacts.lean b/Mathlib/MeasureTheory/Measure/RegularityCompacts.lean
index 5a0ddf740fdcc..b0bd20e4231fc 100644
--- a/Mathlib/MeasureTheory/Measure/RegularityCompacts.lean
+++ b/Mathlib/MeasureTheory/Measure/RegularityCompacts.lean
@@ -4,20 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Rémy Degenne, Peter Pfaffelhuber
 -/
 import Mathlib.Analysis.SpecificLimits.Basic
-<<<<<<< HEAD
---import Mathlib.MeasureTheory.MeasurableSpace.Ball
-=======
->>>>>>> e3a82c6219ca22c71ead073371ab7d6cd6bd8be1
 import Mathlib.MeasureTheory.Measure.Regular
 import Mathlib.Topology.MetricSpace.Polish
 import Mathlib.Topology.UniformSpace.Cauchy
 
 /-!
-<<<<<<< HEAD
-# Inner regularity of Measures wrt compact sets
-In this file we show that a finite measure `μ`  on a `PseudoEMetricSpace E` is inner regular with
-respect to compact sets: `theorem inner_regularWRT_isCompact_of_complete_countable`.
-=======
 # Inner regularity of finite measures
 
 The main result of this file is `theorem InnerRegularCompactLTTop`:
@@ -27,7 +18,6 @@ words, a finite measure on such a space is a tight measure.
 
 Finite measures on Polish spaces are an important special case, which makes the result
 `theorem PolishSpace.innerRegular_isCompact_measurableSet` an important result in probability.
->>>>>>> e3a82c6219ca22c71ead073371ab7d6cd6bd8be1
 -/
 
 open Set MeasureTheory
@@ -122,10 +112,6 @@ theorem exists_isCompact_closure_measure_compl_lt [UniformSpace α] [CompleteSpa
     rcases ENNReal.exists_seq_pos_lt ε hε with ⟨δ, hδ1, hδ2⟩
     classical
     let u : ℕ → ℕ := fun n ↦ s' n (δ n)
-<<<<<<< HEAD
-    let A := interUnionBalls seq u t
-=======
->>>>>>> e3a82c6219ca22c71ead073371ab7d6cd6bd8be1
     refine ⟨interUnionBalls seq u t, isCompact_closure_interUnionBalls h_basis.toHasBasis seq u, ?_⟩
     rw [interUnionBalls, Set.compl_iInter]
     refine ((measure_iUnion_le _).trans ?_).trans_lt hδ2

From ee4438a36534e739a1e7402ec1525cc88a82a22b Mon Sep 17 00:00:00 2001
From: JakobStiefel <jakobstiefel@hotmail.de>
Date: Wed, 18 Dec 2024 12:16:59 +0100
Subject: [PATCH 16/18] remove assumption IsFiniteMeasure

---
 .../Measure/RegularityCompacts.lean           | 48 +++++++++++++++----
 1 file changed, 39 insertions(+), 9 deletions(-)

diff --git a/Mathlib/MeasureTheory/Measure/RegularityCompacts.lean b/Mathlib/MeasureTheory/Measure/RegularityCompacts.lean
index b0bd20e4231fc..7474edd47dd26 100644
--- a/Mathlib/MeasureTheory/Measure/RegularityCompacts.lean
+++ b/Mathlib/MeasureTheory/Measure/RegularityCompacts.lean
@@ -89,6 +89,13 @@ theorem exists_isCompact_closure_measure_compl_lt [UniformSpace α] [CompleteSpa
     [SecondCountableTopology α] [(uniformity α).IsCountablyGenerated]
     [OpensMeasurableSpace α] (P : Measure α) [IsFiniteMeasure P] (ε : ℝ≥0∞) (hε : 0 < ε) :
     ∃ K, IsCompact (closure K) ∧ P Kᶜ < ε := by
+  /-
+  If α is empty, the result is trivial.
+
+  Otherwise, fix a dense sequence `seq` and an antitone basis `t` of entourages. We find a sequence
+  of natural numbers `u n`, such that `interUnionBalls seq u t`, which is the intersection over
+  `n` of the `t n`-neighborhood of `seq 1, ..., seq (u n)`, covers the space arbitrarily well.
+  -/
   cases isEmpty_or_nonempty α
   case inl =>
     refine ⟨∅, by simp, ?_⟩
@@ -157,18 +164,41 @@ theorem innerRegularWRT_isCompact_isOpen [PseudoEMetricSpace α]
 
 /--
 A finite measure `μ` on a `PseudoEMetricSpace E` and `CompleteSpace E` with
-`SecondCountableTopology E` is inner regular with respect to compact sets. In other
-words, a finite measure on such a space is a tight measure.
+`SecondCountableTopology E` is inner regular. In other words, a finite measure
+on such a space is a tight measure.
 -/
-theorem InnerRegularCompactLTTop [PseudoEMetricSpace α]
+theorem InnerRegular_of_pseudoEMetricSpace_completeSpace_secondCountable [PseudoEMetricSpace α]
     [CompleteSpace α] [SecondCountableTopology α] [BorelSpace α]
     (P : Measure α) [IsFiniteMeasure P] :
-    P.InnerRegularCompactLTTop := by
-  refine ⟨Measure.InnerRegularWRT.measurableSet_of_isOpen ?_ ?_⟩
+    P.InnerRegular := by
+  refine @Measure.InnerRegularCompactLTTop.instInnerRegularOfSigmaFinite _ _ _ _
+      ⟨Measure.InnerRegularWRT.measurableSet_of_isOpen ?_ ?_⟩ _
   · exact innerRegularWRT_isCompact_isOpen P
   · exact fun s t hs_compact ht_open ↦ hs_compact.inter_right ht_open.isClosed_compl
 
-theorem innerRegular_isCompact_isClosed_measurableSet [PseudoEMetricSpace α]
+/--
+A measure `μ` on a `PseudoEMetricSpace E` and `CompleteSpace E` with
+`SecondCountableTopology E` is inner regular for finite measure sets with respect to compact sets.
+-/
+theorem InnerRegularCompactLTTop_of_pseudoEMetricSpace_completeSpace_secondCountable
+    [PseudoEMetricSpace α] [CompleteSpace α] [SecondCountableTopology α] [BorelSpace α]
+    (μ : Measure α) :
+    μ.InnerRegularCompactLTTop := by
+  constructor; intro A ⟨hA1, hA2⟩ r hr
+  have IRC : Measure.InnerRegularCompactLTTop (μ.restrict A) := by
+    exact @Measure.InnerRegular.instInnerRegularCompactLTTop _ _ _ _
+        (@InnerRegular_of_pseudoEMetricSpace_completeSpace_secondCountable _ _ _ _ _ _
+        (μ.restrict A) (@Restrict.isFiniteMeasure _ _ _ μ (fact_iff.mpr hA2.lt_top)))
+  have hA2' : (μ.restrict A) A ≠ ⊤ := by
+    rwa [Measure.restrict_apply_self]
+  have hr' : r < μ.restrict A A := by
+    rwa [Measure.restrict_apply_self]
+  obtain ⟨K, ⟨hK1, hK2, hK3⟩⟩ := @MeasurableSet.exists_lt_isCompact_of_ne_top
+      _ _ (μ.restrict A) _ IRC _ hA1 hA2' r hr'
+  use K, hK1, hK2
+  rwa [Measure.restrict_eq_self μ hK1] at hK3
+
+theorem innerRegular_isCompact_isClosed_measurableSet_of_finite [PseudoEMetricSpace α]
     [CompleteSpace α] [SecondCountableTopology α] [BorelSpace α]
     (P : Measure α) [IsFiniteMeasure P] :
     P.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s) MeasurableSet := by
@@ -188,10 +218,10 @@ theorem innerRegular_isCompact_isClosed_measurableSet [PseudoEMetricSpace α]
 On a Polish space, any finite measure is regular with respect to compact and closed sets. In
 particular, a finite measure on a Polish space is a tight measure.
 -/
-theorem PolishSpace.innerRegular_isCompact_measurableSet [TopologicalSpace α] [PolishSpace α]
-    [BorelSpace α] (μ : Measure α) [IsFiniteMeasure μ] :
+theorem PolishSpace.innerRegular_isCompact_isClosed_measurableSet [TopologicalSpace α]
+    [PolishSpace α] [BorelSpace α] (μ : Measure α) [IsFiniteMeasure μ] :
     μ.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s) MeasurableSet := by
   letI := upgradePolishSpace α
-  exact innerRegular_isCompact_isClosed_measurableSet μ
+  exact innerRegular_isCompact_isClosed_measurableSet_of_finite μ
 
 end MeasureTheory

From d541b6c22306796d0d64239321e55639992f85e7 Mon Sep 17 00:00:00 2001
From: JakobStiefel <jakobstiefel@hotmail.de>
Date: Wed, 18 Dec 2024 17:10:22 +0100
Subject: [PATCH 17/18] remove lemmas

---
 Mathlib/Analysis/SpecificLimits/Basic.lean    | 38 -------------------
 .../Measure/RegularityCompacts.lean           |  2 +-
 2 files changed, 1 insertion(+), 39 deletions(-)

diff --git a/Mathlib/Analysis/SpecificLimits/Basic.lean b/Mathlib/Analysis/SpecificLimits/Basic.lean
index 78895cf0dac5f..d86c021d2cfec 100644
--- a/Mathlib/Analysis/SpecificLimits/Basic.lean
+++ b/Mathlib/Analysis/SpecificLimits/Basic.lean
@@ -382,44 +382,6 @@ theorem ENNReal.tsum_geometric (r : ℝ≥0∞) : ∑' n : ℕ, r ^ n = (1 - r)
 theorem ENNReal.tsum_geometric_add_one (r : ℝ≥0∞) : ∑' n : ℕ, r ^ (n + 1) = r * (1 - r)⁻¹ := by
   simp only [_root_.pow_succ', ENNReal.tsum_mul_left, ENNReal.tsum_geometric]
 
-/-- Given x > 0, there is a sequence of positive reals summing to x. -/
-theorem NNReal.exists_seq_pos_summable_eq (x : NNReal) (hx : 0 < x) :
-    ∃ f : ℕ → NNReal, (∀ n, 0 < f n) ∧ Summable f ∧ ∑' n, f n = x := by
-  have h : ∑' n : ℕ, x / 2 / 2 ^ n = x := by
-    rw [NNReal.eq_iff, NNReal.coe_tsum]
-    push_cast
-    exact tsum_geometric_two' x
-  refine ⟨fun n : ℕ ↦ x / 2 / 2 ^ n, fun n ↦ by positivity, ?_, h⟩
-  by_contra h1
-  rw [tsum_eq_zero_of_not_summable h1] at h
-  exact hx.ne h
-
-/-- Given some x > 0, there is a sequence of positive reals summing to x. -/
-theorem ENNReal.exists_seq_pos_eq (x : ℝ≥0∞) (hx : 0 < x) :
-    ∃ f : ℕ → ℝ≥0∞, (∀ n, 0 < f n) ∧ ∑' n, f n = x := by
-  by_cases hx_top : x = ∞
-  · use fun _ ↦ ∞
-    simp [forall_const, ENNReal.tsum_top, hx_top, and_self]
-  suffices ∃ f : ℕ → NNReal, (∀ n, 0 < f n) ∧ Summable f ∧ ∑' n, f n = x.toNNReal by
-    obtain ⟨f, hf_pos, hf_sum, hf_eq⟩ := this
-    refine ⟨fun n ↦ f n, ?_, ?_⟩
-    · exact fun n ↦ ENNReal.coe_pos.mpr (hf_pos n)
-    · rw [← ENNReal.coe_tsum hf_sum, hf_eq, ENNReal.coe_toNNReal hx_top]
-  exact NNReal.exists_seq_pos_summable_eq x.toNNReal (ENNReal.toNNReal_pos hx.ne' hx_top)
-
-/-- Given some x > 0, there is a sequence of positive reals summing to something less than x. -/
-theorem ENNReal.exists_seq_pos_lt (x : ℝ≥0∞) (hx : 0 < x) :
-    ∃ f : ℕ → ℝ≥0∞, (∀ n, 0 < f n) ∧ ∑' n, f n < x := by
-  by_cases hx_top : x = ∞
-  · obtain ⟨f, hf_pos, hf_eq⟩ : ∃ f : ℕ → ℝ≥0∞, (∀ n, 0 < f n) ∧ ∑' n, f n = 1 :=
-      ENNReal.exists_seq_pos_eq 1 zero_lt_one
-    refine ⟨f, hf_pos, ?_⟩
-    simp only [hf_eq, hx_top, ENNReal.one_lt_top]
-  · obtain ⟨f, hf⟩ := ENNReal.exists_seq_pos_eq (x / 2) (ENNReal.half_pos hx.ne')
-    refine ⟨f, hf.1, ?_⟩
-    rw [hf.2]
-    exact ENNReal.half_lt_self hx.ne' hx_top
-
 end Geometric
 
 /-!
diff --git a/Mathlib/MeasureTheory/Measure/RegularityCompacts.lean b/Mathlib/MeasureTheory/Measure/RegularityCompacts.lean
index 7474edd47dd26..f9b7e3c6dbb59 100644
--- a/Mathlib/MeasureTheory/Measure/RegularityCompacts.lean
+++ b/Mathlib/MeasureTheory/Measure/RegularityCompacts.lean
@@ -116,7 +116,7 @@ theorem exists_isCompact_closure_measure_compl_lt [UniformSpace α] [CompleteSpa
       · exact (measurable_prod_mk_left (IsOpen.measurableSet (hto n).2.1)).compl.nullMeasurableSet
       · rw [← compl_iUnion, h_univ, compl_univ]
     choose! s' s'bound using h3
-    rcases ENNReal.exists_seq_pos_lt ε hε with ⟨δ, hδ1, hδ2⟩
+    rcases ENNReal.exists_pos_sum_of_countable' (ne_of_gt hε) ℕ with ⟨δ, hδ1, hδ2⟩
     classical
     let u : ℕ → ℕ := fun n ↦ s' n (δ n)
     refine ⟨interUnionBalls seq u t, isCompact_closure_interUnionBalls h_basis.toHasBasis seq u, ?_⟩

From 49b22c30039f62a4907be2fddfd617a362c1e407 Mon Sep 17 00:00:00 2001
From: JakobStiefel <jakobstiefel@hotmail.de>
Date: Tue, 7 Jan 2025 17:19:19 +0100
Subject: [PATCH 18/18] change theorems into instances

---
 .../Measure/RegularityCompacts.lean           | 37 +++++++++++++++----
 1 file changed, 29 insertions(+), 8 deletions(-)

diff --git a/Mathlib/MeasureTheory/Measure/RegularityCompacts.lean b/Mathlib/MeasureTheory/Measure/RegularityCompacts.lean
index f9b7e3c6dbb59..1d8e91a4aa967 100644
--- a/Mathlib/MeasureTheory/Measure/RegularityCompacts.lean
+++ b/Mathlib/MeasureTheory/Measure/RegularityCompacts.lean
@@ -60,7 +60,7 @@ lemma innerRegularWRT_isCompact_isClosed_iff [TopologicalSpace α] [R1Space α]
 
 /--
 If predicate `p` is preserved under intersections with sets satisfying predicate `q`, and sets
-satisfying `p` exploit the space arbitrarily well, then `μ` is inner regular with respect to
+satisfying `p` cover the space arbitrarily well, then `μ` is inner regular with respect to
 predicates `p` and `q`.
 -/
 theorem innerRegularWRT_of_exists_compl_lt {p q : Set α → Prop} (hpq : ∀ A B, p A → q B → p (A ∩ B))
@@ -167,7 +167,7 @@ A finite measure `μ` on a `PseudoEMetricSpace E` and `CompleteSpace E` with
 `SecondCountableTopology E` is inner regular. In other words, a finite measure
 on such a space is a tight measure.
 -/
-theorem InnerRegular_of_pseudoEMetricSpace_completeSpace_secondCountable [PseudoEMetricSpace α]
+instance InnerRegular_of_pseudoEMetricSpace_completeSpace_secondCountable [PseudoEMetricSpace α]
     [CompleteSpace α] [SecondCountableTopology α] [BorelSpace α]
     (P : Measure α) [IsFiniteMeasure P] :
     P.InnerRegular := by
@@ -177,10 +177,20 @@ theorem InnerRegular_of_pseudoEMetricSpace_completeSpace_secondCountable [Pseudo
   · exact fun s t hs_compact ht_open ↦ hs_compact.inter_right ht_open.isClosed_compl
 
 /--
-A measure `μ` on a `PseudoEMetricSpace E` and `CompleteSpace E` with
-`SecondCountableTopology E` is inner regular for finite measure sets with respect to compact sets.
+A special case of `innerRegular_of_pseudoEMetricSpace_completeSpace_secondCountable` for Polish
+spaces: A finite measure on a Polish space is a tight measure.
 -/
-theorem InnerRegularCompactLTTop_of_pseudoEMetricSpace_completeSpace_secondCountable
+instance InnerRegular_of_polishSpace [TopologicalSpace α]
+    [PolishSpace α] [BorelSpace α] (P : Measure α) [IsFiniteMeasure P] :
+    P.InnerRegular := by
+  letI := upgradePolishSpace α
+  exact InnerRegular_of_pseudoEMetricSpace_completeSpace_secondCountable P
+
+/--
+A measure `μ` on a `PseudoEMetricSpace E` and `CompleteSpace E` with `SecondCountableTopology E`
+is inner regular for finite measure sets with respect to compact sets.
+-/
+instance InnerRegularCompactLTTop_of_pseudoEMetricSpace_completeSpace_secondCountable
     [PseudoEMetricSpace α] [CompleteSpace α] [SecondCountableTopology α] [BorelSpace α]
     (μ : Measure α) :
     μ.InnerRegularCompactLTTop := by
@@ -198,6 +208,17 @@ theorem InnerRegularCompactLTTop_of_pseudoEMetricSpace_completeSpace_secondCount
   use K, hK1, hK2
   rwa [Measure.restrict_eq_self μ hK1] at hK3
 
+/--
+A special case of `innerRegularCompactLTTop_of_pseudoEMetricSpace_completeSpace_secondCountable`
+for Polish spaces: A measure `μ` on a Polish space inner regular for finite measure sets with
+respect to compact sets.
+-/
+instance InnerRegularCompactLTTop_of_polishSpace
+    [TopologicalSpace α] [PolishSpace α] [BorelSpace α] (μ : Measure α) :
+    μ.InnerRegularCompactLTTop := by
+  letI := upgradePolishSpace α
+  exact InnerRegularCompactLTTop_of_pseudoEMetricSpace_completeSpace_secondCountable μ
+
 theorem innerRegular_isCompact_isClosed_measurableSet_of_finite [PseudoEMetricSpace α]
     [CompleteSpace α] [SecondCountableTopology α] [BorelSpace α]
     (P : Measure α) [IsFiniteMeasure P] :
@@ -219,9 +240,9 @@ On a Polish space, any finite measure is regular with respect to compact and clo
 particular, a finite measure on a Polish space is a tight measure.
 -/
 theorem PolishSpace.innerRegular_isCompact_isClosed_measurableSet [TopologicalSpace α]
-    [PolishSpace α] [BorelSpace α] (μ : Measure α) [IsFiniteMeasure μ] :
-    μ.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s) MeasurableSet := by
+    [PolishSpace α] [BorelSpace α] (P : Measure α) [IsFiniteMeasure P] :
+    P.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s) MeasurableSet := by
   letI := upgradePolishSpace α
-  exact innerRegular_isCompact_isClosed_measurableSet_of_finite μ
+  exact innerRegular_isCompact_isClosed_measurableSet_of_finite P
 
 end MeasureTheory