tentative formalization of Vitali's theorem

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -103,6 +103,86 @@
     `measurable_closed_ball`, `lebesgue_measure_closed_ball`,
     `measurable_scale_cball`
 
+- in `nomedtype.v`:
+  + lemmas `ball0`, `ball_itv`,
+  + lemmas `closed_ball0`, `closed_ball_itv`
+
+- in `mathcomp_extra.v`:
+  + lemma `leq_ltn_expn`
+
+- in `classical_sets.v`:
+  + lemma `set_cons1`, `trivIset_bigcup`
+  + definition `maximal_disjoint_subcollection`
+  + lemma `ex_maximal_disjoint_subcollection`
+
+- in `topology.v`:
+  + lemma `separated_open_countable`
+
+- in `normedtype.v`:
+  + definitions `scale_ball`, `scale_cball`
+  + lemmas `scale_ball1`, `scale_ball_neq0`, `sub_scale_ball`
+  + lemmas `scale_cball1`, `scale_cball_neq0`, `scale_cball_itv`
+  + lemmas `separated_open_countable`, `separated_closed_ball_countable`
+  + lemmas `vitali_lemma_finite`, `vitali_lemma_finite_cover`
+  + definition `vitali_collection_partition`
+  + lemmas `vitali_collection_partition_ub_gt0`,
+    `ex_vitali_collection_partition`, `cover_vitali_collection_partition`,
+    `disjoint_vitali_collection_partition`
+  + lemma `separated_closed_ball_countable`
+  + lemmas `vitali_lemma`, `vitali_lemma_cover`
+
+- in `lebesgue_measure.v`:
+  + lemmas `measurable_ball`, `lebesgue_measure_ball`,
+    `measurable_closed_ball`, `lebesgue_measure_closed_ball`,
+    `measurable_scale_cball`
+
+- in `nomedtype.v`:
+  + lemmas `ball0`, `ball_itv`,
+  + lemmas `closed_ball0`, `closed_ball_itv`
+
+- in `mathcomp_extra.v`:
+  + lemma `leq_ltn_expn`
+
+- in `classical_sets.v`:
+  + lemma `set_cons1`, `trivIset_bigcup`
+  + definition `maximal_disjoint_subcollection`
+  + lemma `ex_maximal_disjoint_subcollection`
+
+- in `topology.v`:
+  + lemma `separated_open_countable`
+
+- in `normedtype.v`:
+  + definitions `scale_ball`, `scale_cball`
+  + lemmas `scale_ball1`, `scale_ball_neq0`, `sub_scale_ball`
+  + lemmas `scale_cball1`, `scale_cball_neq0`, `scale_cball_itv`
+  + lemmas `separated_open_countable`, `separated_closed_ball_countable`
+  + lemmas `vitali_lemma_finite`, `vitali_lemma_finite_cover`
+  + definition `vitali_collection_partition`
+  + lemmas `vitali_collection_partition_ub_gt0`,
+    `ex_vitali_collection_partition`, `cover_vitali_collection_partition`,
+    `disjoint_vitali_collection_partition`
+  + lemma `separated_closed_ball_countable`
+  + lemmas `vitali_lemma`, `vitali_lemma_cover`
+
+- in `lebesgue_measure.v`:
+  + lemmas `measurable_ball`, `lebesgue_measure_ball`,
+    `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
 
 - `mnormalize` moved from `kernel.v` to `measure.v` and generalized
@@ -136,6 +216,27 @@
 
 ### Generalized
 
+- in `exp.v`:
+  + lemmas `convex_expR`, `ler_power_pos` (now `ler_powR`)
+- in `exp.v`:
+  + lemma `ln_power_pos` (now `ln_powR`)
+  + lemma `ln_power_pos`
+- in file `lebesgue_integral.v`, updated `le_approx`.
+
+- in `sequences.v`:
+  + lemmas `is_cvg_nneseries_cond`, `is_cvg_npeseries_cond`
+  + lemmas `is_cvg_nneseries`, `is_cvg_npeseries`
+  + lemmas `nneseries_ge0`, `npeseries_le0`
+
+- in `measure.v`:
+  + lemmas `measureDI`, `measureD`, `measureUfinl`, `measureUfinr`,
+    `null_set_setU`, `measureU0`
+    (from measure to content)
+  + lemma `subset_measure0` (from `realType` to `realFieldType`)
+
+- in `classical_sets.v`:
+  + `set_nil` from `choiceType` to `eqType`
+
 - in `classical_sets.v`:
   + `set_nil` from `choiceType` to `eqType`
 

classical/classical_sets.v

@@ -1124,6 +1124,9 @@ Proof. by move=> k; apply/val_inj. Qed.
 Lemma IIordK {n} : cancel (@IIord n) ordII.
 Proof. by move=> k; apply/val_inj. Qed.
 
+Lemma mem_not_I N n : (n \in ~` `I_N) = (N <= n).
+Proof. by rewrite in_setC /mkset /in_mem /mem /= /in_set asboolb -leqNgt. Qed.
+
 End InitialSegment.
 
 Lemma setT_unit : [set: unit] = [set tt].
@@ -2567,6 +2570,17 @@ have [nm|nm] := eqVneq n m; first by apply: (tB m) => //; rewrite -nm.
 exact: (H _ _ _ _ nm).
 Qed.
 
+Lemma trivIsetT_bigcup T1 T2 (I : eqType) (D : I -> set T1) (F : T1 -> set T2) :
+  trivIset setT D ->
+  trivIset (\bigcup_i D i) F ->
+  trivIset setT (fun i => \bigcup_(t in D i) F t).
+Proof.
+move=> D0 h i j _ _ [t [[m Dim Fmt] [n Djn Fnt]]].
+have mn : m = n by apply: h => //; [exists i|exists j|exists t].
+rewrite {}mn {m} in Dim Fmt *.
+by apply: D0 => //; exists n.
+Qed.
+
 Definition cover T I D (F : I -> set T) := \bigcup_(i in D) F i.
 
 Lemma coverE T I D (F : I -> set T) : cover D F = \bigcup_(i in D) F i.