maximal inequality

math-comp · Oct 2, 2023 · 696c00a · 696c00a
1 parent 33f74fc
commit 696c00a
Show file tree

Hide file tree

Showing 2 changed files with 412 additions and 0 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -37,6 +37,20 @@
     `measurable_closed_ball`, `lebesgue_measure_closed_ball`,
     `measurable_scale_cball`
 
+- in `classical_sets.v`:
+  + lemmas `trivIsetT_bigcup`, `mem_not_I`
+
+- in `sequences.v`:
+  + lemma `nneseries_tail_cvg`
+
+- in `normedtype.v`:
+  + lemmas `open_subball`, `closed_disjoint_closed_ball`
+
+- in `lebesgue_measure.v`:
+  + lemmas `measure_sigma_sub_additive_tail`, `outer_measure_sigma_subadditive_tail`
+  + definition `vitali_cover`
+  + lemma `vitali_theorem`
+
 ### Changed
 
 ### Renamed