complete thm 2.13

CHANGELOG_UNRELEASED.md

@@ -58,55 +58,6 @@
   + change implicits of `measurable_funP`
 
 
-- in file `normedtype.v`,
-     changed `completely_regular_space` to depend on uniform separators
-     which removes the dependency on `R`.  The old formulation can be
-     recovered easily with `uniform_separatorP`.
-
-- moved from `Rstruct.v` to `Rstruct_topology.v`
-  + lemmas `continuity_pt_nbhs`, `continuity_pt_cvg`,
-    `continuity_ptE`, `continuity_pt_cvg'`, `continuity_pt_dnbhs`
-    and `nbhs_pt_comp`
-
-- moved from `real_interval.v` to `normedtype.v`
-  + lemmas `set_itvK`, `RhullT`, `RhullK`, `set_itv_setT`,
-    `Rhull_smallest`, `le_Rhull`, `neitv_Rhull`, `Rhull_involutive`,
-    `disj_itv_Rhull`
-- in `topology.v`:
-  + lemmas `subspace_pm_ball_center`, `subspace_pm_ball_sym`,
-    `subspace_pm_ball_triangle`, `subspace_pm_entourage` turned
-	into local `Let`'s
-
-- in `lebesgue_integral.v`:
-  + structure `SimpleFun` now inside a module `HBSimple`
-  + structure `NonNegSimpleFun` now inside a module `HBNNSimple`
-  + lemma `cst_nnfun_subproof` has now a different statement
-  + lemma `indic_nnfun_subproof` has now a different statement
-- in `mathcomp_extra.v`:
-  + definition `idempotent_fun`
-
-- in `topology_structure.v`:
-  + definitions `regopen`, `regclosed`
-  + lemmas `closure_setC`, `interiorC`, `closureU`, `interiorU`,
-           `closureEbigcap`, `interiorEbigcup`,
-	   `closure_open_regclosed`, `interior_closed_regopen`,
-	   `closure_interior_idem`, `interior_closure_idem`
-
-- in file `topology_structure.v`,
-  + mixin `isContinuous`, type `continuousType`, structure `Continuous`
-  + new lemma `continuousEP`.
-  + new definition `mkcts`.
-
-- in file `subspace_topology.v`,
-  + new lemmas `continuous_subspace_setT`, `nbhs_prodX_subspace_inE`, and
-    `continuous_subspace_prodP`.
-  + type `continuousFunType`, HB structure `ContinuousFun`
-
-- in file `subtype_topology.v`,
-  + new lemmas `subspace_subtypeP`, `subspace_sigL_continuousP`,
-    `subspace_valL_continuousP'`, `subspace_valL_continuousP`, `sigT_of_setXK`,
-    `setX_of_sigTK`, `setX_of_sigT_continuous`, and `sigT_of_setX_continuous`.
-
 - in `lebesgue_integrale.v`
   + change implicits of `measurable_funP`
 
@@ -137,13 +88,6 @@
 
 ### Removed
 
-- in `lebesgue_integral.v`:
-  + definition `cst_mfun`
-  + lemma `mfun_cst`
-
-- in `cardinality.v`:
-  + lemma `cst_fimfun_subproof`
-
 - in `lebesgue_integral.v`:
   + lemma `cst_mfun_subproof` (use lemma `measurable_cst` instead)
   + lemma `cst_nnfun_subproof` (turned into a `Let`)

_CoqProject

@@ -86,6 +86,7 @@ theories/lebesgue_integral.v
 theories/ftc.v
 theories/hoelder.v
 theories/probability.v
+theories/independence.v
 theories/convex.v
 theories/charge.v
 theories/kernel.v

classical/mathcomp_extra.v

@@ -538,3 +538,38 @@ Qed.
 Definition sigT_fun {I : Type} {X : I -> Type} {T : Type}
   (f : forall i, X i -> T) (x : {i & X i}) : T :=
   (f (projT1 x) (projT2 x)).
+
+(* PR 114 to finmap in progress *)
+Section FsetPartitions.
+Variables T I : choiceType.
+Implicit Types (x y z : T) (A B D X : {fset T}) (P Q : {fset {fset T}}).
+Implicit Types (J : pred I) (F : I -> {fset T}).
+
+Variables (R : Type) (idx : R) (op : Monoid.com_law idx).
+Let rhs_cond P K E :=
+  (\big[op/idx]_(A <- P) \big[op/idx]_(x <- A | K x) E x)%fset.
+Let rhs P E := (\big[op/idx]_(A <- P) \big[op/idx]_(x <- A) E x)%fset.
+
+Lemma partition_disjoint_bigfcup (f : T -> R) (F : I -> {fset T})
+  (K : {fset I}) :
+  (forall i j, i \in K -> j \in K -> i != j -> [disjoint F i & F j])%fset ->
+  \big[op/idx]_(i <- \big[fsetU/fset0]_(x <- K) (F x)) f i =
+  \big[op/idx]_(k <- K) (\big[op/idx]_(i <- F k) f i).
+Proof.
+move=> disjF; pose P := [fset F i | i in K & F i != fset0]%fset.
+have trivP : trivIfset P.
+  apply/trivIfsetP => _ _ /imfsetP[i iK ->] /imfsetP[j jK ->] neqFij.
+  move: iK; rewrite !inE/= => /andP[iK Fi0].
+  move: jK; rewrite !inE/= => /andP[jK Fj0].
+  by apply: (disjF _ _ iK jK); apply: contraNneq neqFij => ->.
+have -> : (\bigcup_(i <- K) F i)%fset = fcover P.
+  apply/esym; rewrite /P fcover_imfset big_mkcond /=; apply eq_bigr => i _.
+  by case: ifPn => // /negPn/eqP.
+rewrite big_trivIfset // /rhs big_imfset => [|i j iK /andP[jK notFj0] eqFij] /=.
+  rewrite big_filter big_mkcond; apply eq_bigr => i _.
+  by case: ifPn => // /negPn /eqP ->;  rewrite big_seq_fset0.
+move: iK; rewrite !inE/= => /andP[iK Fi0].
+by apply: contraNeq (disjF _ _ iK jK) _; rewrite -fsetI_eq0 eqFij fsetIid.
+Qed.
+
+End FsetPartitions.

theories/Make

@@ -52,6 +52,7 @@ lebesgue_integral.v
 ftc.v
 hoelder.v
 probability.v
+independence.v
 lebesgue_stieltjes_measure.v
 convex.v
 charge.v