Merge pull request #353 from math-comp/measure_20210324

Caratheodory theorem

CHANGELOG_UNRELEASED.md

@@ -3,7 +3,7 @@
 ## [Unreleased]
 
 ### Added
-  
+
 - in `ereal.v`:
   + lemmas `big_nat_widenl`, `big_geq_mkord`
   + lemmas `lee_sum_nneg_natr`, `lee_sum_nneg_natl`
@@ -12,6 +12,18 @@
   + lemmas `ereal_pseries_sum_nat`, `lte_lim`
   + lemmas `is_cvg_ereal_nneg_natsum_cond`, `is_cvg_ereal_nneg_natsum`
   + lemma `ereal_pseriesD`, `ereal_pseries0`, `eq_ereal_pseries`
+- in `classical_sets.v`, lemma `subset_bigsetU_cond`
+- in `measure.v`:
+  + lemma `eq_bigcupB_of_bigsetU`
+  + definitions `caratheodory_type`
+  + definition `caratheodory_measure` and lemma `caratheodory_measure_complete`
+  + internal definitions and lemmas that may be deprecated and hidden in the future:
+    * `caratheodory_measurable`, notation `... .-measurable`,
+    * `le_caratheodory_measurable`, `outer_measure_bigcup_lim`,
+      `caratheodory_measurable_{set0,setC,setU_le,setU,bigsetU,setI,setD}`
+      `disjoint_caratheodoryIU`, `caratheodory_additive`,
+          `caratheodory_lim_lee`, `caratheodory_measurable_trivIset_bigcup`,
+      `caratheodory_measurable_bigcup`
 
 ### Changed
 
@@ -24,7 +36,7 @@
     * lemmas `ereal_nondecreasing_series`, `ereal_nneg_series_lim_ge`
     * lemmas `is_cvg_ereal_nneg_series_cond`, `is_cvg_ereal_nneg_series`
     * lemmas `ereal_nneg_series_lim_ge0`, `ereal_nneg_series_pinfty`
-
+- in `classical_sets.v`, lemma `subset_bigsetU`
 
 ### Renamed
 

theories/classical_sets.v

@@ -822,11 +822,19 @@ rewrite big_ord_recl /= (IHn (fun i => F i.+1)) predeqE => x; split.
 by move=> [[|i] Fi]; [left|right; exists i].
 Qed.
 
-Lemma subset_bigsetU m n F : (m <= n)%N ->
-  \big[setU/set0]_(i < m) F i `<=` \big[setU/set0]_(i < n) F i.
+Lemma subset_bigsetU F :
+  {homo (fun n => \big[setU/set0]_(i < n) F i) : n m / (n <= m)%N >-> n `<=` m}.
 Proof.
-rewrite !bigcup_ord => mn x [i im ?]; exists i => //.
-by rewrite /mkset (leq_trans im).
+move=> m n mn; rewrite !bigcup_ord => x [i im Fix].
+by exists i => //=; rewrite (leq_trans im).
+Qed.
+
+Lemma subset_bigsetU_cond (P : pred nat) F :
+  {homo (fun n => \big[setU/set0]_(i < n | P i) F i)
+    : n m / (n <= m)%N >-> n `<=` m}.
+Proof.
+move=> n m nm; rewrite big_mkcond [in X in _ `<=` X]big_mkcond/=.
+exact: (@subset_bigsetU (fun i => if P i then F i else _)).
 Qed.
 
 Lemma bigcap_ord n F :