feat(measure_theory/regular): more material on regular measures (#7680)

This PR:
* defines weakly regular measures
* shows that for weakly regular measures any finite measure set can be approximated from inside by closed sets
* shows that for regular measures any finite measure set can be approximated from inside by compact sets
* shows that any finite measure on a metric space is weakly regular
* shows that any locally finite measure on a sigma compact locally compact metric space is regular

docs/references.bib

@@ -120,6 +120,23 @@ @InProceedings{   beylin1996
   isbn          = "978-3-540-70722-6"
 }
 
+@book {billingsley1999,
+    AUTHOR = {Billingsley, Patrick},
+     TITLE = {Convergence of probability measures},
+    SERIES = {Wiley Series in Probability and Statistics: Probability and
+              Statistics},
+   EDITION = {Second},
+      NOTE = {A Wiley-Interscience Publication},
+ PUBLISHER = {John Wiley \& Sons, Inc., New York},
+      YEAR = {1999},
+     PAGES = {x+277},
+      ISBN = {0-471-19745-9},
+   MRCLASS = {60B10 (28A33 60F17)},
+  MRNUMBER = {1700749},
+       DOI = {10.1002/9780470316962},
+       URL = {https://doi.org/10.1002/9780470316962},
+}
+
 @Book{            borceux-vol1,
   title         = {Handbook of Categorical Algebra: Volume 1, Basic Category
                   Theory},

src/analysis/specific_limits.lean

@@ -823,6 +823,11 @@ begin
   exact ⟨ε', hp, (ennreal.tsum_coe_eq hc).symm ▸ lt_trans (coe_lt_coe.2 hcr) hrε⟩
 end
 
+theorem exists_pos_sum_of_encodable' {ε : ℝ≥0∞} (hε : 0 < ε) (ι) [encodable ι] :
+  ∃ ε' : ι → ℝ≥0∞, (∀ i, 0 < ε' i) ∧ (∑' i, ε' i) < ε :=
+let ⟨δ, δpos, hδ⟩ := exists_pos_sum_of_encodable hε ι in
+  ⟨λ i, δ i, λ i, ennreal.coe_pos.2 (δpos i), hδ⟩
+
 end ennreal
 
 /-!