Renamed and added lemmas for setD and bigcup (#2009)

* added setD_bigcapr + renamed bigcupDr to setD_bigcupr

* added preimageD1

---------

Co-authored-by: adjevahi <arthur.djevahirdjian@ens-lyon.fr>
Co-authored-by: Reynald Affeldt <reynald.affeldt@aist.go.jp>

Author: 3 people

CHANGELOG_UNRELEASED.md

@@ -2,18 +2,6 @@
 
 ## [Unreleased]
 
-### Renamed
-- in `functions.v`
-  + lemma `scalrfctE` -> `scalerfctE` (deprecating `scalrfctE`)
-
-### Changed
-- in `functions.v`
-  + lemma `fctE` (include `zerofctE` and `onefctE`)
-
-### Added
-- in `functions.v`:
-  + lemmas `zerofctE`, `onefctE`
-
 ### Added
 - in `set_interval.v`:
   + lemmas `setU_itvob1`, `setU_1itvob`
@@ -26,6 +14,7 @@
   + definitions `cross`, `cross12`
   + lemmas `smallest_sub_sub`, `bigcap_closed_smallest`, `smallest_sub_iff`
   + lemma `preimage_set_systemS`
+  + lemma `setD_bigcapr`
 
 - in `measurable_structure.v`:
   + lemmas `g_sigma_algebra_cross`, `g_sigma_algebra_rectangle`
@@ -186,12 +175,9 @@
   + lemma `ge0_integration_by_substitution_shift_itvy`,
     `ge0_integration_by_substitution_shift_itvNy`
 
-### Changed
+- in `functions.v`:
+  + lemmas `zerofctE`, `onefctE`
 
-- moved from `measurable_structure.v` to `classical_sets.v`:
-  + definition `preimage_set_system`
-  + lemmas `preimage_set_system0`, `preimage_set_systemU`, `preimage_set_system_comp`,
-    `preimage_set_system_id`
 - in `functions.v`:
   + lemmas `linfunP`, `linfun_eqP`
   + instances of `SubLmodule` and `pointedType` on `{linear _->_ | _ }`
@@ -221,11 +207,14 @@
   + lemma `ge0_esum`
   + lemma `esum_ge`
 
-- in `realsum.v`:
-  + lemma `__admitted__psumB` proved and renamed to `psumB`
+- in `functions.v`:
+  + lemma `preimageD1`
 
 ### Changed
 
+- in `realsum.v`:
+  + lemma `__admitted__psumB` proved and renamed to `psumB`
+
 - moved from `measurable_structure.v` to `classical_sets.v`:
   + definition `preimage_set_system`
   + lemmas `preimage_set_system0`, `preimage_set_systemU`, `preimage_set_system_comp`,
@@ -335,6 +324,12 @@
   + definition `seqD`
   + lemmas `eq_bigcup_seqD`, `trivIset_seqD`, `seqDU_seqD`, `bigcup_bigsetU_bigcup`
 
+- in `functions.v`
+  + lemma `fctE` (include `zerofctE` and `onefctE`)
+
+- in `classical_sets.v`
+  + lemma `bigcupDr` -> `setD_bigcupr` (deprecating `bigcupDr`)
+
 ### Renamed
 
 - in `tvs.v`:
@@ -384,6 +379,9 @@
 - in `realsum.v`:
   + `psum` -> `PosSum.psum`
 
+- in `functions.v`
+  + lemma `scalrfctE` -> `scalerfctE` (deprecating `scalrfctE`)
+
 ### Generalized
 
 - in `measurable_structure.v`:

classical/classical_sets.v

@@ -2115,10 +2115,19 @@ Lemma setC_bigsetI U (s : seq T) (f : T -> set U) (P : pred T) :
   \big[setU/set0]_(t <- s | P t) ~` f t.
 Proof. by elim/big_rec2: _ => [|i X Y Pi <-]; rewrite ?setCT ?setCI. Qed.
 
+#[deprecated(since="mathcomp-analysis 1.17.0", note="use `setD_bigcupr` instead")]
 Lemma bigcupDr (F : I -> set T) (P : set I) (A : set T) : P !=set0 ->
   \bigcap_(i in P) (A `\` F i) = A `\` \bigcup_(i in P) F i.
 Proof. by move=> PN0; rewrite setDE setC_bigcup -bigcapIr. Qed.
 
+Lemma setD_bigcupr (F : I -> set T) (P : set I) (A : set T) : P !=set0 ->
+  A `\` \bigcup_(i in P) F i = \bigcap_(i in P) (A `\` F i).
+Proof. by move=> PN0; rewrite setDE setC_bigcup -bigcapIr. Qed.
+
+Lemma setD_bigcapr (F : I -> set T) [P : set I] (A : set T) :
+  A `\` \bigcap_(i in P)  F i = \bigcup_(i in P)  (A `\` F i).
+Proof. by rewrite setDE setC_bigcap setI_bigcupr. Qed.
+
 Lemma setD_bigcupl (F : I -> set T) (P : set I) (A : set T) :
   \bigcup_(i in P) F i `\` A = \bigcup_(i in P) (F i `\` A).
 Proof. by rewrite setDE setI_bigcupl; under eq_bigcupr do rewrite -setDE. Qed.

classical/functions.v

@@ -2766,6 +2766,15 @@ Definition fctE :=
   (cstE, compE, opprfctE, addrfctE, mulrfctE, scalerfctE, exprfctE,
    zerofctE, onefctE).
 
+Lemma preimageD1 {T : Type} {Z : zmodType} (f g : T -> Z) (z : Z) :
+  (f \+ g) @^-1`[set z] =
+  \bigcup_(a in range f) (f @^-1` [set a] `&` g @^-1` [set z - a]).
+Proof.
+rewrite eqEsubset; split => [x <-|x [a _ /= [<- ->]]].
+  by exists (f x) => /=; [exact/imageT|rewrite addrC addKr].
+by rewrite subrKC.
+Qed.
+
 End function_space_lemmas.
 
 #[deprecated(since="mathcomp-analysis 1.17.0", use=scalerfctE)]

theories/lebesgue_integral_theory/lebesgue_integral_definition.v

@@ -170,7 +170,7 @@ Proof.
 rewrite !sintegralE; set F := f @` _; set G := g @` _; set FG := _ @` _.
 pose pf x := f @^-1` [set x]; pose pg y := g @^-1` [set y].
 transitivity (\sum_(z \in FG) z%:E * \sum_(a \in F) m (pf a `&` pg (z - a)%R)).
-  apply: eq_fsbigr => z _; rewrite preimage_add -fsbig_setU// measure_fsbig//.
+  apply: eq_fsbigr => z _; rewrite preimageD1 -fsbig_setU// measure_fsbig//.
     by move=> x Fx; exact: measurableI.
   exact/trivIset_setIr/trivIset_preimage1.
 under eq_fsbigr do rewrite ge0_mule_fsumr//; rewrite exchange_fsbig//=.

theories/lebesgue_integral_theory/measurable_fun_approximation.v

@@ -725,7 +725,7 @@ exists (\bigcup_(i in range f) dK i); split.
 - by rewrite -bigsetU_fset_set//; apply: bigsetU_compact=>// i _; case: (dkP i).
 - by move=> z [y _ dy]; have [_ /(_ _ dy) []] := dkP y.
 - have -> : A `\` \bigcup_(i in range f) dK i = \bigcup_(i in range f) J i.
-    rewrite -bigcupDr /= ?eqEsubset; first by exists (f point), point.
+    rewrite setD_bigcupr /= ?eqEsubset; first by exists (f point), point.
     split => z; first by move=> /(_ (f z)) [//| ? ?]; exists (f z).
     case => ? [? _ <-] [[zab /= <- nfz]] ? [r _ <-]; split => //.
     by move: nfz; apply: contra_not => /[dup] /dKsub ->.

theories/lebesgue_integral_theory/simple_functions.v

@@ -227,16 +227,6 @@ move=> x0; apply/seteqP.
 by split=> [z/= <-|z/= ->]; rewrite [x * _]mulrC (mulfK, divfK).
 Qed.
 
-Lemma preimage_add T (R : numDomainType) (f g : T -> R) z :
-  (f \+ g) @^-1` [set z] = \bigcup_(a in f @` setT)
-    ((f @^-1` [set a]) `&` (g @^-1` [set z - a])).
-Proof.
-apply/seteqP; split=> [x /= fgz|x [_ /= [y _ <-]] [fxfy gzf]]; last first.
-  by rewrite gzf -fxfy addrC subrK.
-exists (z - g x); first by exists x; rewrite // -fgz addrK.
-by split; rewrite 1?subKr // -fgz addrK.
-Qed.
-
 Section simple_bounded.
 Context d (T : sigmaRingType d) (R : realType).
 

theories/measure_theory/measure_function.v

@@ -739,7 +739,7 @@ have mDbigcup I (D : set I) (A : set T) (B : I -> set T) : finite_set D ->
     measurable_fin_trivIset (A `\` \bigcup_(i in D) B i).
   have [->|/set0P D0] := eqVneq D set0.
     by rewrite bigcup0// setD0 => *; apply: mdW.
-  move=> Dfin Am Bm; rewrite -bigcupDr//; apply: mdisj_bigcap=> // i Di.
+  move=> Dfin Am Bm; rewrite setD_bigcupr//; apply: mdisj_bigcap=> // i Di.
   by have [F [Ffin Fm -> ?]] := semi_measurableD A (B i) Am (Bm _ Di); exists F.
 have mdU : fin_trivIset_closed measurable_fin_trivIset.
   elim/Pchoice=> I D F Dfin Ftriv Fm.
@@ -760,7 +760,7 @@ have mdDI : setD_closed measurable_fin_trivIset.
   have [->|/set0P F'N0] := eqVneq F' set0.
     by rewrite bigcup_set0 setD0; exists F.
   rewrite setD_bigcupl; apply: mdU => //; first by apply: trivIset_setIr.
-  move=> X DX; rewrite -bigcupDr//; apply: mdisj_bigcap => //.
+  move=> X DX; rewrite setD_bigcupr//; apply: mdisj_bigcap => //.
   move=> Y DY; case: (semi_measurableD X Y); [exact: Fm|exact: F'm|].
   by move=> G [Gfin Gm -> Gtriv]; exists G.
 apply: smallest_sub => //; split=> //; first by apply: mdW.