feat(MeasureTheory): Outer regular measures are determined by values on bounded open sets (#37312)

We proved that

- Every open set in a metric space is a countable union of bounded open sets.
- Outer regular measures are determined by values on bounded open sets.

Author: CoolRmal

Mathlib/MeasureTheory/Measure/Regular.lean

@@ -482,6 +482,15 @@ theorem ext_isOpen {ν : Measure α} [OuterRegular μ] [OuterRegular ν]
   congr! 4 with t _ ht2
   exact hμν t ht2
 
+/-- Outer regular measures are determined by values on bounded open sets. -/
+theorem ext_isOpen_isBounded {α : Type*} [PseudoMetricSpace α] {mα : MeasurableSpace α}
+    {μ ν : Measure α} [OuterRegular μ] [OuterRegular ν]
+    (hμν : ∀ U, IsOpen U → Bornology.IsBounded U → μ U = ν U) : μ = ν := by
+  refine ext_isOpen fun U hU ↦ ?_
+  obtain ⟨f, hm, hu, hf⟩ := Metric.eq_countable_union_of_isBounded_of_isOpen hU
+  rw [← hu, hm.measure_iUnion, hm.measure_iUnion]
+  exact iSup_congr fun i ↦ hμν (f i) (hf i).2 (hf i).1
+
 end OuterRegular
 
 /-- If a measure `μ` admits finite spanning open sets such that the restriction of `μ` to each set

Mathlib/Topology/MetricSpace/Bounded.lean

@@ -79,6 +79,16 @@ theorem isBounded_closedBall : IsBounded (closedBall x r) :=
 theorem isBounded_ball : IsBounded (ball x r) :=
   isBounded_closedBall.subset ball_subset_closedBall
 
+/-- Every open set in a metric space is a countable union of bounded open sets. -/
+theorem eq_countable_union_of_isBounded_of_isOpen {U : Set α} (hU : IsOpen U) :
+    ∃ f : ℕ → Set α, Monotone f ∧ ⋃ i, f i = U ∧ ∀ i, IsBounded (f i) ∧ IsOpen (f i) := by
+  obtain rfl | ⟨x, -⟩ := U.eq_empty_or_nonempty
+  · exact ⟨fun i ↦ ∅, monotone_const, by simp_all⟩
+  refine ⟨fun i ↦ U ∩ ball x i, fun i j hij ↦ ?_, ?_, fun i ↦ ⟨?_, hU.inter isOpen_ball⟩⟩
+  · exact inter_subset_inter_right _ (ball_subset_ball (Nat.cast_le.2 hij))
+  · simp [← inter_iUnion]
+  · exact isBounded_ball.subset inter_subset_right
+
 /-- Spheres are bounded -/
 theorem isBounded_sphere : IsBounded (sphere x r) :=
   isBounded_closedBall.subset sphere_subset_closedBall