Merge pull request #676 from math-comp/decomp_set

use set instead of fset in decomp

CHANGELOG_UNRELEASED.md

@@ -94,6 +94,16 @@
 - in `lebesgue_measure.v`:
   + notation `_.-ocitv`
   + definition `ocitv_display`
+- in `classical_sets.v`:
+  + lemmas `trivIset_image`, `trivIset_comp`
+  + notation `trivIsets`
+- in `functions.v`:
+  + lemma `patch_pred`, `trivIset_restr`
+- in `measure.v`:
+  + lemma `measure_semi_additive_ord`, `measure_semi_additive_ord_I`
+  + lemma `decomp_finite_set`
+- in `esum.v`:
+  + lemma `fsbig_esum`
 
 ### Changed
 
@@ -140,6 +150,13 @@
     * `mem_factor_itv`
 - lemma `preimage_cst` generalized and moved from `lebesgue_integral.v`
   to `functions.v`
+- in `fsbig.v`:
+  + generalize `exchange_fsum`
++ in `measure.v`:
+  + statement of lemmas `content_fin_bigcup`, `measure_fin_bigcup`, `ring_fsets`,
+    `decomp_triv`, `cover_decomp`, `decomp_set0`, `decompN0`, `Rmu_fin_bigcup`
+  + definitions `decomp`, `measure`
++ lemma `fset_set_image` moved from `measure.v` to `cardinality.v`
 
 ### Renamed
 
@@ -156,6 +173,8 @@
 - in `lebesgue_measure.v`:
   + `itvs` -> `ocitv_type`
   + `measurable_fun_sum` -> `emeasurable_fun_sum`
+- in `classical_sets.v`:
+  + `trivIset_restr` -> `trivIset_widen`
 
 ### Removed
 

theories/classical_sets.v

@@ -2346,6 +2346,22 @@ apply/trivIsetP => -[/=|]; rewrite /bigcup2 /=.
   by move=> [//|j _ _ _]; rewrite setI0.
 Qed.
 
+Lemma trivIset_image (T I I' : Type) (D : set I) (f : I -> I') (F : I' -> set T) :
+  trivIset D (F \o f) -> trivIset (f @` D) F.
+Proof.
+by move=> trivF i j [{}i Di <-] [{}j Dj <-] Ffij; congr (f _); apply: trivF.
+Qed.
+Arguments trivIset_image {T I I'} D f F.
+
+Lemma trivIset_comp (T I I' : Type) (D : set I) (f : I -> I') (F : I' -> set T) :
+    {in D &, injective f} ->
+  trivIset D (F \o f) = trivIset (f @` D) F.
+Proof.
+move=> finj; apply/propext; split; first exact: trivIset_image.
+move=> trivF i j Di Dj Ffij; apply: finj; rewrite ?in_setE//.
+by apply: trivF => //=; [exists i| exists j].
+Qed.
+
 Definition cover T I D (F : I -> set T) := \bigcup_(i in D) F i.
 
 Lemma cover_restr T I D' D (F : I -> set T) :
@@ -2380,11 +2396,13 @@ Definition pblock T (I : pointedType) D (F : I -> set T) (x : T) :=
 
 (* TODO: theory of trivIset, cover, partition, pblock_index and pblock *)
 
+Notation trivIsets X := (trivIset X id).
+
 Lemma trivIset_sets T I D (F : I -> set T) :
-  trivIset D F -> trivIset [set F i | i in D] id.
-Proof. by move=> DF A B [i Di <-{A}] [j Dj <-{B}] /DF ->. Qed.
+  trivIset D F -> trivIsets [set F i | i in D].
+Proof. exact: trivIset_image. Qed.
 
-Lemma trivIset_restr T I D' D (F : I -> set T) :
+Lemma trivIset_widen T I D' D (F : I -> set T) :
 (*  D `<=` D' -> (forall i, D i -> ~ D' i -> F i !=set0) ->*)
   D `<=` D' -> (forall i, D' i -> ~ D i -> F i = set0) ->
   trivIset D F = trivIset D' F.

theories/esum.v

@@ -1,7 +1,7 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect ssralg ssrnum finmap.
 Require Import boolp reals mathcomp_extra ereal classical_sets signed topology.
-Require Import sequences functions cardinality normedtype numfun.
+Require Import sequences functions cardinality normedtype numfun fsbigop.
 
 (******************************************************************************)
 (*                      Summation over classical sets                         *)
@@ -105,6 +105,9 @@ move=> Afin a0; rewrite -esum_fset => [|i]; rewrite ?fset_setK//.
 by rewrite in_fset_set ?inE//; apply: a0.
 Qed.
 
+Lemma fsbig_esum (A : set T) a : finite_set A -> (forall x, 0 <= a x) ->
+  \sum_(x \in A) (a x) = \esum_(x in A) a x.
+Proof. by move=> *; rewrite fsbig_finite//= sum_fset_set. Qed.
 End esum_realType.
 
 Lemma esum_ge [R : realType] [T : choiceType] (I : set T) (a : T -> \bar R) x :

theories/fsbigop.v

@@ -522,12 +522,12 @@ move=> /andP[Pi Qi]; exists i; rewrite 2?inE ?andbT//.
 by exists j; rewrite 2?inE ?andbT.
 Qed.
 
-Lemma exchange_fsum (T : choiceType) (R : realDomainType) (P Q : set T)
-     (f : T -> T -> \bar R) :
+Lemma exchange_fsum (T1 T2 : choiceType) (R : realDomainType) (P : set T1) (Q : set T2)
+     (f : T1 -> T2 -> \bar R) :
     finite_set P -> finite_set Q ->
   (\sum_(i \in P) \sum_(j \in Q) f i j = \sum_(j \in Q) \sum_(i \in P) f i j)%E.
 Proof.
-move=> Pfin Qfin; rewrite 2?pair_fsum//; pose swap (x : T * T) := (x.2, x.1).
+move=> Pfin Qfin; rewrite 2?pair_fsum//; pose swap (x : T2 * T1) := (x.2, x.1).
 apply: (reindex_fsbig swap).
 split=> [? [? ?]//|[? ?] [? ?] /set_mem[? ?] /set_mem[? ?] [-> ->]//|].
 by move=> [i j] [? ?]; exists (j, i).

theories/functions.v

@@ -1800,6 +1800,10 @@ End patch.
 Notation restrict := (patch (fun=> point)).
 Notation "f \_ D" := (restrict D f) : fun_scope.
 
+Lemma patch_pred {I T} (D : {pred I}) (d f : I -> T) :
+  patch d D f = fun i => if D i then f i else d i.
+Proof. by apply/funext => i; rewrite /patch mem_setE. Qed.
+
 Lemma preimage_restrict (aT : Type) (rT : pointedType)
      (f : aT -> rT) (D : set aT) (B : set rT) :
   (f \_ D) @^-1` B = (if point \in B then ~` D else set0) `|` D `&` f @^-1` B.
@@ -1835,6 +1839,18 @@ Lemma restrict_comp {aT} {rT sT : pointedType} (h : rT -> sT) (f : aT -> rT) D :
 Proof. by move=> hp; apply/funext => x; rewrite /patch/=; case: ifP. Qed.
 Arguments restrict_comp {aT rT sT} h f D.
 
+Lemma trivIset_restr (T I : Type) (D D' : set I) (F : I -> set T) :
+    trivIset D' (F \_ D) = trivIset (D `&` D') F.
+Proof.
+apply/propext; split=> FDtriv i j.
+  move=> [Di D'i] [Dj D'j] [x [Fix Fjx]]; apply: FDtriv => //.
+  by exists x; split => /=; rewrite ?patchT ?in_setE.
+move=> D'i D'j [x []]; rewrite /patch.
+do 2![case: ifPn => //]; rewrite !in_setE => Di Dj Fix Fjx.
+by apply: FDtriv => //; exists x.
+Qed.
+
+
 (**************************************)
 (* Restriction of domain and codomain *)
 (**************************************)

theories/lebesgue_integral.v

@@ -601,8 +601,8 @@ Lemma measure_fsbig (I : choiceType) (A : set I) (F : I -> set T) :
   (forall i, A i -> measurable (F i)) -> trivIset A F ->
   m (\big[setU/set0]_(i \in A) F i) = \sum_(i \in A) m (F i).
 Proof.
-move=> Afin Fm Ft; rewrite !fsbig_finite//=.
-by rewrite -!bigcup_fset_set// measure_fin_bigcup.
+move=> Afin Fm Ft.
+by rewrite fsbig_finite// -measure_fin_bigcup// bigcup_fset_set.
 Qed.
 
 Lemma additive_nnsfunr (g f : {nnsfun T >-> R}) x :