generic lemmas from kernels PR

CHANGELOG_UNRELEASED.md

@@ -15,17 +15,40 @@
 - in `constructive_ereal.v`:
   + lemma `oppe_inj`
 
+- in `mathcomp_extra.v`:
+  + lemma `add_onemK`
+  + function `swap`
+- in `classical_sets.v`:
+  + lemmas `setT0`, `set_unit`, `set_bool`
+  + lemmas `xsection_preimage_snd`, `ysection_preimage_fst`
+- in `exp.v`:
+  + lemma `expR_ge0`
+- in `measure.v`
+  + lemmas `measurable_curry`, `measurable_fun_fst`, `measurable_fun_snd`,
+    `measurable_fun_swap`, `measurable_fun_pair`, `measurable_fun_if_pair`
+  + lemmas `dirac0`, `diracT`
+  + lemma `finite_measure_sigma_finite`
+- in `lebesgue_measure.v`:
+  + lemma `measurable_fun_opp`
+- in `lebesgue_integral.v`
+  + lemmas `integral0_eq`, `fubini_tonelli`
+
 ### Changed
 
 - in `fsbigop.v`:
   + implicits of `eq_fsbigr`
 
 ### Renamed
 
+- in `measurable.v`:
+  + `measurable_fun_comp` -> `measurable_funT_comp`
+
 ### Generalized
 
 - in `esum.v`:
   + lemma `esum_esum`
+- in `measure.v`
+  + lemma `measurable_fun_comp`
 
 ### Deprecated
 

classical/classical_sets.v

@@ -1088,9 +1088,31 @@ End InitialSegment.
 Lemma setT_unit : [set: unit] = [set tt].
 Proof. by apply/seteqP; split => // -[]. Qed.
 
+Lemma set_unit (A : set unit) : A = set0 \/ A = setT.
+Proof.
+have [->|/set0P[[] Att]] := eqVneq A set0; [by left|right].
+by apply/seteqP; split => [|] [].
+Qed.
+
 Lemma setT_bool : [set: bool] = [set true; false].
 Proof. by rewrite eqEsubset; split => // [[]] // _; [left|right]. Qed.
 
+Lemma set_bool (B : set bool) :
+  [\/ B == [set true], B == [set false], B == set0 | B == setT].
+Proof.
+have [Bt|Bt] := boolP (true \in B); have [Bf|Bf] := boolP (false \in B).
+- have -> : B = setT by apply/seteqP; split => // -[] _; exact: set_mem.
+  by apply/or4P; rewrite eqxx/= !orbT.
+- suff : B = [set true] by move=> ->; apply/or4P; rewrite eqxx.
+  apply/seteqP; split => -[]// /mem_set; last by move=> _; exact: set_mem.
+  by rewrite (negbTE Bf).
+- suff : B = [set false] by move=> ->; apply/or4P; rewrite eqxx/= orbT.
+  apply/seteqP; split => -[]// /mem_set; last by move=> _; exact: set_mem.
+  by rewrite (negbTE Bt).
+- suff : B = set0 by move=> ->; apply/or4P; rewrite eqxx/= !orbT.
+  by apply/seteqP; split => -[]//=; rewrite 2!notin_set in Bt, Bf.
+Qed.
+
 (* TODO: other lemmas that relate fset and classical sets *)
 Lemma fdisjoint_cset (T : choiceType) (A B : {fset T}) :
   [disjoint A & B]%fset = [disjoint [set` A] & [set` B]].
@@ -2179,7 +2201,6 @@ Notation "[ 'get' x | E ]" := (get (fun x => E))
   (at level 0, x name, format "[ 'get'  x  |  E ]") : form_scope.
 
 Section PointedTheory.
-
 Context {T : pointedType}.
 
 Lemma getPex (P : set T) : (exists x, P x) -> P (get P).
@@ -2198,6 +2219,9 @@ Proof. exact: (xget_unique point). Qed.
 Lemma getPN (P : set T) : (forall x, ~ P x) -> get P = point.
 Proof. exact: (xgetPN point). Qed.
 
+Lemma setT0 : setT != set0 :> set T.
+Proof. by apply/eqP => /seteqP[] /(_ point) /(_ Logic.I). Qed.
+
 End PointedTheory.
 
 Variant squashed T : Prop := squash (x : T).
@@ -3083,6 +3107,14 @@ rewrite predeqE /ysection /= => x; split; last by rewrite 3!inE.
 by rewrite inE => -[Xxy Yxy]; rewrite 2!inE.
 Qed.
 
+Lemma xsection_preimage_snd (Z : Type) (f : T2 -> Z) (A : set Z) (x : T1) :
+  xsection ((f \o snd) @^-1` A) x = f @^-1` A.
+Proof. by apply/seteqP; split; move=> y/=; rewrite /xsection/= inE. Qed.
+
+Lemma ysection_preimage_fst (Z : Type) (f : T1 -> Z) (A : set Z) (y : T2) :
+  ysection ((f \o fst) @^-1` A) y = f @^-1` A.
+Proof. by apply/seteqP; split; move=> x/=; rewrite /ysection/= inE. Qed.
+
 End section.
 
 Notation "B \; A" :=

classical/mathcomp_extra.v

@@ -28,6 +28,8 @@ From mathcomp Require Import finset interval.
 (*               proj i f == f i, where f : forall i, T i                     *)
 (*             dfwith f x == fun j => x if j = i, and f j otherwise           *)
 (*                           given x : T i                                    *)
+(*                 swap x := (x.2, x.1)                                       *)
+(*                                                                            *)
 (******************************************************************************)
 
 Set Implicit Arguments.
@@ -1010,6 +1012,9 @@ Lemma onem1 : `1-1 = 0. Proof. by rewrite /onem subrr. Qed.
 Lemma onemK r : `1-(`1-r) = r.
 Proof. by rewrite /onem opprB addrCA subrr addr0. Qed.
 
+Lemma add_onemK r : r + `1- r = 1.
+Proof. by rewrite /onem addrC subrK. Qed.
+
 Lemma onem_gt0 r : r < 1 -> 0 < `1-r. Proof. by rewrite subr_gt0. Qed.
 
 Lemma onem_ge0 r : r <= 1 -> 0 <= `1-r.
@@ -1101,3 +1106,5 @@ Proof. by move=> z; rewrite /proj dfwithin. Qed.
 
 End DFunWith.
 Arguments dfwith {I T} f i x.
+
+Definition swap (T1 T2 : Type) (x : T1 * T2) := (x.2, x.1).

theories/constructive_ereal.v

@@ -932,13 +932,13 @@ move=> fio; apply/idP/existsP => [/eqP /=|[/= i /andP[Pi /eqP fi]]].
 by apply/eqP/esum_eqyP => //; exists i.
 Qed.
 
-#[deprecated(since="mathcomp 1.6.0", note="renamed `esum_eqNyP`")]
+#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `esum_eqNyP`")]
 Notation esum_ninftyP := esum_eqNyP.
-#[deprecated(since="mathcomp 1.6.0", note="renamed `esum_eqNy`")]
+#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `esum_eqNy`")]
 Notation esum_ninfty := esum_eqNy.
-#[deprecated(since="mathcomp 1.6.0", note="renamed `esum_eqyP`")]
+#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `esum_eqyP`")]
 Notation esum_pinftyP := esum_eqyP.
-#[deprecated(since="mathcomp 1.6.0", note="renamed `esum_eqy`")]
+#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `esum_eqy`")]
 Notation esum_pinfty := esum_eqy.
 
 Lemma adde_ge0 x y : 0 <= x -> 0 <= y -> 0 <= x + y.
@@ -1297,13 +1297,13 @@ rewrite dual_sumeE eqe_oppLR /= esum_eqy => [|i]; rewrite ?eqe_oppLR //.
 by under eq_existsb => i do rewrite eqe_oppLR.
 Qed.
 
-#[deprecated(since="mathcomp 1.6.0", note="renamed `desum_eqNyP`")]
+#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `desum_eqNyP`")]
 Notation desum_ninftyP := desum_eqNyP.
-#[deprecated(since="mathcomp 1.6.0", note="renamed `desum_eqNy`")]
+#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `desum_eqNy`")]
 Notation desum_ninfty := desum_eqNy.
-#[deprecated(since="mathcomp 1.6.0", note="renamed `desum_eqyP`")]
+#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `desum_eqyP`")]
 Notation desum_pinftyP := desum_eqyP.
-#[deprecated(since="mathcomp 1.6.0", note="renamed `desum_eqy`")]
+#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `desum_eqy`")]
 Notation desum_pinfty := desum_eqy.
 
 Lemma dadde_ge0 x y : 0 <= x -> 0 <= y -> 0 <= x + y.
@@ -1384,7 +1384,7 @@ suff: ~ x%:E < (Order.max 0 x + 1)%:E.
 by apply/negP; rewrite -leNgt; apply/Ax/ltr_spaddr; rewrite // le_maxr lexx.
 Qed.
 
-#[deprecated(since="mathcomp 1.6.0", note="renamed `eqyP`")]
+#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `eqyP`")]
 Notation eq_pinftyP := eqyP.
 
 Lemma seq_psume_eq0 (I : choiceType) (r : seq I)

theories/exp.v

@@ -378,6 +378,8 @@ case: (ltrgt0P x) => [x_gt0|x_gt0|->]; last by rewrite expR0.
   by rewrite -(pmulr_lgt0 _ F) expRxMexpNx_1.
 Qed.
 
+Lemma expR_ge0 x : 0 <= expR x. Proof. by rewrite ltW// expR_gt0. Qed.
+
 Lemma expRN x : expR (- x) = (expR x)^-1.
 Proof.
 apply: (mulfI (lt0r_neq0 (expR_gt0 x))).