diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 44dd7732e2..036df781a0 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -15,6 +15,24 @@
 - 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`:
@@ -22,10 +40,15 @@
 
 ### 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
 
diff --git a/classical/classical_sets.v b/classical/classical_sets.v
index 09d777f9fc..ad1e6af4da 100644
--- a/classical/classical_sets.v
+++ b/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" :=
diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v
index cff517b764..1bff02bdae 100644
--- a/classical/mathcomp_extra.v
+++ b/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).
diff --git a/theories/constructive_ereal.v b/theories/constructive_ereal.v
index 7afea39414..a4cddb5d6d 100644
--- a/theories/constructive_ereal.v
+++ b/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)
diff --git a/theories/exp.v b/theories/exp.v
index bdf6e57959..367daac7cc 100644
--- a/theories/exp.v
+++ b/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))).
diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v
index 4c93a76a61..fc2cf96e9d 100644
--- a/theories/lebesgue_integral.v
+++ b/theories/lebesgue_integral.v
@@ -1037,6 +1037,13 @@ Qed.
 Lemma integral0 D : \int_(x in D) (cst 0 x) = 0.
 Proof. by rewrite ge0_integralE// erestrict0 nnintegral0. Qed.
 
+Lemma integral0_eq D f :
+  (forall x, D x -> f x = 0) -> \int_(x in D) f x = 0.
+Proof.
+move=> f0; under eq_integral; first by move=> x /[1!inE] /f0 ->; over.
+by rewrite integral0.
+Qed.
+
 Lemma integral_ge0 D f : (forall x, D x -> 0 <= f x) -> 0 <= \int_(x in D) f x.
 Proof.
 move=> f0; rewrite ge0_integralE// nnintegral_ge0// => x.
@@ -1719,7 +1726,7 @@ End semi_linearity.
 Lemma emeasurable_funN d (T : measurableType d) (R : realType) D (f : T -> \bar R) :
   measurable D -> measurable_fun D f -> measurable_fun D (fun x => - f x)%E.
 Proof.
-by move=> mD mf; apply: measurable_fun_comp => //; exact: emeasurable_fun_minus.
+by move=> mD mf; apply: measurable_funT_comp => //; exact: emeasurable_fun_minus.
 Qed.
 
 Section approximation_sfun.
@@ -2439,8 +2446,8 @@ transitivity (lim (fun n => \int[pushforward mu mphi]_x (f_ n x)%:E)).
   - by move=> y _ m n mn; rewrite lee_fin; apply/lefP/ndf_.
 rewrite (_ : (fun _ => _) = (fun n => \int[mu]_x (EFin \o f_ n \o phi) x)).
   rewrite -monotone_convergence//; last 3 first.
-    - move=> n /=; apply: measurable_fun_comp; first exact: measurable_fun_EFin.
-      by apply: measurable_fun_comp => //; exact: measurable_sfun.
+    - move=> n /=; apply: measurable_funT_comp; first exact: measurable_fun_EFin.
+      by apply: measurable_funT_comp => //; exact: measurable_sfun.
     - by move=> n x _ /=; rewrite lee_fin.
     - by move=> x _ m n mn; rewrite lee_fin; exact/lefP/ndf_.
   by apply: eq_integral => x _ /=; apply/cvg_lim => //; exact: f_f.
@@ -2535,7 +2542,7 @@ Let integralT_measure_sum (f : {nnsfun T >-> R}) :
 Proof.
 under eq_integral do rewrite fimfunE -fsumEFin//.
 rewrite ge0_integral_fsum//; last 2 first.
-  - move=> r /=; apply: measurable_fun_comp => //.
+  - move=> r /=; apply: measurable_funT_comp => //.
     exact/measurable_funrM/measurable_fun_indic.
   - by move=> r t _; rewrite EFinM nnfun_muleindic_ge0.
 transitivity (\sum_(i \in range f)
@@ -2645,7 +2652,7 @@ Lemma integral_measure_series_nnsfun (D : set T) (mD : measurable D)
 Proof.
 under eq_integral do rewrite fimfunE -fsumEFin//.
 rewrite ge0_integral_fsum//; last 2 first.
-  - move=> r /=; apply: measurable_fun_comp => //.
+  - move=> r /=; apply: measurable_funT_comp => //.
     exact/measurable_funrM/measurable_fun_indic.
   - by move=> r t _; rewrite EFinM nnfun_muleindic_ge0.
 transitivity (\sum_(i \in range f)
@@ -2783,14 +2790,14 @@ Lemma le_integral_abse (D : set T) (mD : measurable D) (g : T -> \bar R) a :
   a%:E * mu (D `&` [set x | `|g x| >= a%:E]) <= \int[mu]_(x in D) `|g x|.
 Proof.
 move=> mg a0; have ? : measurable (D `&` [set x | a%:E <= `|g x|]).
-  by apply: emeasurable_fun_c_infty => //; exact: measurable_fun_comp.
+  by apply: emeasurable_fun_c_infty => //; exact: measurable_funT_comp.
 apply: (@le_trans _ _ (\int[mu]_(x in D `&` [set x | `|g x| >= a%:E]) `|g x|)).
   rewrite -integral_cstr//; apply: ge0_le_integral => //.
   - by move=> x _ /=; exact/ltW.
   - exact/EFin_measurable_fun/measurable_fun_cst.
-  - by apply: measurable_fun_comp => //; exact: measurable_funS mg.
+  - by apply: measurable_funT_comp => //; exact: measurable_funS mg.
   - by move=> x /= [].
-by apply: subset_integral => //; exact: measurable_fun_comp.
+by apply: subset_integral => //; exact: measurable_funT_comp.
 Qed.
 
 End subset_integral.
@@ -2832,8 +2839,8 @@ Lemma eq_integrable f g : {in D, f =1 g} -> mu_int f -> mu_int g.
 Proof.
 move=> fg [mf fi]; split; first exact: eq_measurable_fun mf.
 rewrite (le_lt_trans _ fi)//; apply: ge0_le_integral=> //.
-  by apply: measurable_fun_comp => //; exact: eq_measurable_fun mf.
-  by apply: measurable_fun_comp => //; exact: eq_measurable_fun mf.
+  by apply: measurable_funT_comp => //; exact: eq_measurable_fun mf.
+  by apply: measurable_funT_comp => //; exact: eq_measurable_fun mf.
 by move=> x Dx; rewrite fg// inE.
 Qed.
 
@@ -2841,20 +2848,20 @@ Lemma le_integrable f g : measurable_fun D f ->
   (forall x, D x -> `|f x| <= `|g x|) -> mu_int g -> mu_int f.
 Proof.
 move=> mf fg [mfg goo]; split => //; rewrite (le_lt_trans _ goo) //.
-by apply: ge0_le_integral => //; exact: measurable_fun_comp.
+by apply: ge0_le_integral => //; exact: measurable_funT_comp.
 Qed.
 
 Lemma integrableN f : mu_int f -> mu_int (-%E \o f).
 Proof.
 move=> [mf foo]; split; last by rewrite /comp; under eq_fun do rewrite abseN.
-by rewrite /comp; apply: measurable_fun_comp =>//; exact: emeasurable_fun_minus.
+by rewrite /comp; apply: measurable_funT_comp =>//; exact: emeasurable_fun_minus.
 Qed.
 
 Lemma integrablerM (k : R) f : mu_int f -> mu_int (fun x => k%:E * f x).
 Proof.
 move=> [mf foo]; split; first exact: measurable_funeM.
 under eq_fun do rewrite abseM.
-by rewrite ge0_integralM// ?lte_mul_pinfty//; exact: measurable_fun_comp.
+by rewrite ge0_integralM// ?lte_mul_pinfty//; exact: measurable_funT_comp.
 Qed.
 
 Lemma integrableMr (k : R) f : mu_int f -> mu_int (f \* cst k%:E).
@@ -2867,11 +2874,11 @@ Proof.
 move=> [mf foo] [mg goo]; split; first exact: emeasurable_funD.
 apply: (@le_lt_trans _ _ (\int[mu]_(x in D) (`|f x| + `|g x|))).
   apply: ge0_le_integral => //.
-  - by apply: measurable_fun_comp => //; exact: emeasurable_funD.
-  - by apply: emeasurable_funD; apply: measurable_fun_comp.
+  - by apply: measurable_funT_comp => //; exact: emeasurable_funD.
+  - by apply: emeasurable_funD; apply: measurable_funT_comp.
   - by move=> *; exact: lee_abs_add.
 by rewrite ge0_integralD //; [exact: lte_add_pinfty|
-  exact: measurable_fun_comp|exact: measurable_fun_comp].
+  exact: measurable_funT_comp|exact: measurable_funT_comp].
 Qed.
 
 Lemma integrableB f g : mu_int f -> mu_int g -> mu_int (f \- g).
@@ -2893,8 +2900,8 @@ Lemma integrable_funepos f : mu_int f -> mu_int f^\+.
 Proof.
 move=> [Df foo]; split; first exact: emeasurable_fun_funepos.
 apply: le_lt_trans foo; apply: ge0_le_integral => //.
-- by apply/measurable_fun_comp => //; exact: emeasurable_fun_funepos.
-- exact/measurable_fun_comp.
+- by apply/measurable_funT_comp => //; exact: emeasurable_fun_funepos.
+- exact/measurable_funT_comp.
 - by move=> t Dt; rewrite -/((abse \o f) t) fune_abse gee0_abs// lee_addl.
 Qed.
 
@@ -2902,8 +2909,8 @@ Lemma integrable_funeneg f : mu_int f -> mu_int f^\-.
 Proof.
 move=> [Df foo]; split; first exact: emeasurable_fun_funeneg.
 apply: le_lt_trans foo; apply: ge0_le_integral => //.
-- by apply/measurable_fun_comp => //; exact: emeasurable_fun_funeneg.
-- exact/measurable_fun_comp.
+- by apply/measurable_funT_comp => //; exact: emeasurable_fun_funeneg.
+- exact/measurable_funT_comp.
 - by move=> t Dt; rewrite -/((abse \o f) t) fune_abse gee0_abs// lee_addr.
 Qed.
 
@@ -2912,7 +2919,7 @@ Lemma integral_funeneg_lt_pinfty f : mu_int f ->
 Proof.
 move=> [mf]; apply: le_lt_trans; apply: ge0_le_integral => //.
 - by apply: emeasurable_fun_funeneg => //; exact: emeasurable_funN.
-- exact: measurable_fun_comp.
+- exact: measurable_funT_comp.
 - move=> x Dx; have [fx0|/ltW fx0] := leP (f x) 0.
     rewrite lee0_abs// /funeneg.
     by move: fx0; rewrite -{1}oppe0 -lee_oppr => /max_idPl ->.
@@ -2925,7 +2932,7 @@ Lemma integral_funepos_lt_pinfty f : mu_int f ->
 Proof.
 move=> [mf]; apply: le_lt_trans; apply: ge0_le_integral => //.
 - by apply: emeasurable_fun_funepos => //; exact: emeasurable_funN.
-- exact: measurable_fun_comp.
+- exact: measurable_funT_comp.
 - move=> x Dx; have [fx0|/ltW fx0] := leP (f x) 0.
     rewrite lee0_abs// /funepos.
     by move: (fx0) => /max_idPr ->; rewrite -lee_oppr oppe0.
@@ -2940,7 +2947,7 @@ rewrite fin_numElt; apply/andP; split.
   by rewrite (@lt_le_trans _ _ 0) ?lte_ninfty//; exact: integral_ge0.
 case: fi => mf; apply: le_lt_trans; apply: ge0_le_integral => //.
 - exact/emeasurable_fun_funeneg.
-- exact/measurable_fun_comp.
+- exact/measurable_funT_comp.
 - by move=> x Dx; rewrite -/((abse \o f) x) (fune_abse f) lee_addr.
 Qed.
 
@@ -2952,7 +2959,7 @@ rewrite fin_numElt; apply/andP; split.
   by rewrite (@lt_le_trans _ _ 0) ?lte_ninfty//; exact: integral_ge0.
 case: fi => mf; apply: le_lt_trans; apply: ge0_le_integral => //.
 - exact/emeasurable_fun_funepos.
-- exact/measurable_fun_comp.
+- exact/measurable_funT_comp.
 - by move=> x Dx; rewrite -/((abse \o f) x) (fune_abse f) lee_addl.
 Qed.
 
@@ -3073,7 +3080,7 @@ Lemma integrableS (E D : set T) (f : T -> \bar R) :
 Proof.
 move=> mE mD DE [mf ifoo]; split; first exact: measurable_funS mf.
 apply: le_lt_trans ifoo; apply: subset_integral => //.
-exact: measurable_fun_comp.
+exact: measurable_funT_comp.
 Qed.
 
 Lemma integrable_mkcond D f : measurable D ->
@@ -3125,14 +3132,14 @@ have [M M0 muM] : exists2 M, (0 <= M)%R &
   exists (fine (\int[mu]_(x in D) `|f x|)); first exact/fine_ge0/integral_ge0.
   move=> n.
   rewrite -integral_indic// -ge0_integralM//; last 2 first.
-    - by apply: measurable_fun_comp=> //; exact/measurable_fun_indic.
+    - by apply: measurable_funT_comp=> //; exact/measurable_fun_indic.
     - by move=> *; rewrite lee_fin.
   rewrite fineK//; last first.
     by case: fint => _ foo; rewrite ge0_fin_numE//; exact: integral_ge0.
   apply: ge0_le_integral => //.
   - by move=> *; rewrite lee_fin /indic.
   - exact/EFin_measurable_fun/measurable_funrM/measurable_fun_indic.
-  - by apply: measurable_fun_comp => //; case: fint.
+  - by apply: measurable_funT_comp => //; case: fint.
   - move=> x Dx; rewrite /= indicE.
     have [|xE] := boolP (x \in E); last by rewrite mule0.
     by rewrite /E inE /= => -[->]; rewrite leey.
@@ -3436,13 +3443,13 @@ have le_f_M t : D t -> `|f t| <= M%:E * (f' t)%:E.
 have : 0 <= \int[mu]_(x in D) `|f x|  <= `|M|%:E * mu Df_neq0.
   rewrite integral_ge0//= /Df_neq0 -{2}(setIid D) setIAC -integral_indic//.
   rewrite -/Df_neq0 -ge0_integralM//; last 2 first.
-    - by apply: measurable_fun_comp=> //; exact: measurable_fun_indic.
+    - by apply: measurable_funT_comp=> //; exact: measurable_fun_indic.
     - by move=> x ?; rewrite lee_fin.
   apply: ge0_le_integral => //.
-  - exact: measurable_fun_comp.
+  - exact: measurable_funT_comp.
   - by move=> x Dx; rewrite mule_ge0// lee_fin.
   - apply: emeasurable_funM; first exact: measurable_fun_cst.
-    by apply: measurable_fun_comp => //; exact: measurable_fun_indic.
+    by apply: measurable_funT_comp => //; exact: measurable_fun_indic.
   - move=> x Dx.
     rewrite (le_trans (le_f_M _ Dx))// lee_fin /f' indicE.
     by case: (_ \in _) => //; rewrite ?mulr1 ?mulr0// ler_norm.
@@ -3481,9 +3488,9 @@ move=> mf; split=> [iDf0|Df0].
   transitivity (lim (fun n => mu (D `&` [set x | `|f x| >= n.+1%:R^-1%:E]))).
     apply/esym/cvg_lim => //; apply: nondecreasing_cvg_mu.
     - move=> i; apply: emeasurable_fun_c_infty => //.
-      exact: measurable_fun_comp.
+      exact: measurable_funT_comp.
     - apply: bigcupT_measurable => i.
-      by apply: emeasurable_fun_c_infty => //; exact: measurable_fun_comp.
+      by apply: emeasurable_fun_c_infty => //; exact: measurable_funT_comp.
     - move=> m n mn; apply/subsetPset; apply: setIS => t /=.
       by apply: le_trans; rewrite lee_fin lef_pinv // ?ler_nat // posrE.
   by rewrite (_ : (fun _ => _) = cst 0) ?lim_cst//= funeqE => n /=; rewrite muDf.
@@ -3502,7 +3509,7 @@ have -> : (fun x => `|f x|) = (fun x => lim (f_^~ x)).
   by rewrite min_l// subrr normr0.
 transitivity (lim (fun n => \int[mu]_(x in D) (f_ n x) )).
   apply/esym/cvg_lim => //; apply: cvg_monotone_convergence => //.
-  - move=> n; apply: emeasurable_fun_min => //; first exact: measurable_fun_comp.
+  - move=> n; apply: emeasurable_fun_min => //; first exact: measurable_funT_comp.
     exact: measurable_fun_cst.
   - by move=> n t Dt; rewrite /f_ lexI abse_ge0 //= lee_fin.
   - move=> t Dt m n mn; rewrite /f_ lexI.
@@ -3522,7 +3529,7 @@ have f_bounded n x : D x -> `|f_ n x| <= n%:R%:E.
 have if_0 n : \int[mu]_(x in D) `|f_ n x|  = 0.
   apply: (@ae_eq_integral_abs_bounded _ _ _ n%:R) => //.
     by apply: emeasurable_fun_min => //;
-      [exact: measurable_fun_comp|exact: measurable_fun_cst].
+      [exact: measurable_funT_comp|exact: measurable_fun_cst].
   exact: f_bounded.
 rewrite (_ : (fun _ => _) = cst 0) // ?lim_cst// funeqE => n.
 by rewrite -(if_0 n); apply: eq_integral => x _; rewrite gee0_abs// /f_.
@@ -3579,7 +3586,7 @@ have h1 : mu.-integrable D f <-> mu.-integrable D (fun x => f x * (oneCN x)%:E).
     rewrite (eq_integral (fun x => `|f x| * (\1_(~` N) x)%:E)); last first.
       by move=> t _; rewrite abseM (@gee0_abs _ (\1_(~` N) t)%:E) // lee_fin.
     rewrite -integral_setI_indic//; case: intf => _; apply: le_lt_trans.
-    by apply: subset_integral => //; [exact:measurableI|exact:measurable_fun_comp].
+    by apply: subset_integral => //; [exact:measurableI|exact:measurable_funT_comp].
   split => //; rewrite (funID mN f) -/oneCN -/oneN.
   have ? : measurable_fun D (fun x : T => f x * (oneCN x)%:E).
     by apply: emeasurable_funM=> //; exact/EFin_measurable_fun/measurable_funTS.
@@ -3589,11 +3596,11 @@ have h1 : mu.-integrable D f <-> mu.-integrable D (fun x => f x * (oneCN x)%:E).
   apply: (@le_lt_trans _ _
     (\int[mu]_(x in D) (`|f x * (oneCN x)%:E| + `|f x * (oneN x)%:E|))).
     apply: ge0_le_integral => //.
-    - by apply: measurable_fun_comp => //; exact: emeasurable_funD.
-    - by apply: emeasurable_funD; exact: measurable_fun_comp.
+    - by apply: measurable_funT_comp => //; exact: emeasurable_funD.
+    - by apply: emeasurable_funD; exact: measurable_funT_comp.
     - by move=> *; rewrite lee_abs_add.
   rewrite ge0_integralD//;
-    [|exact: measurable_fun_comp|exact: measurable_fun_comp].
+    [|exact: measurable_funT_comp|exact: measurable_funT_comp].
   by apply: lte_add_pinfty; [case: intCf|case: intone].
 have h2 : mu.-integrable (D `\` N) f <->
     mu.-integrable D (fun x => f x * (oneCN x)%:E).
@@ -3605,7 +3612,7 @@ have h2 : mu.-integrable (D `\` N) f <->
       by move=> t _; rewrite abseM (@gee0_abs _ (\1_(~` N) t)%:E)// lee_fin.
     rewrite -integral_setI_indic //; case: intCf => _; apply: le_lt_trans.
     apply: subset_integral=> //; [exact: measurableI|exact: measurableD|].
-    by apply: measurable_fun_comp => //; apply: measurable_funS mf => // ? [].
+    by apply: measurable_funT_comp => //; apply: measurable_funS mf => // ? [].
   split.
     move=> mDN A mA; rewrite setDE (setIC D) -setIA; apply: measurableI => //.
     exact: mf.
@@ -3699,18 +3706,18 @@ Lemma le_integral_comp_abse d (T : measurableType d) (R : realType)
   (f a%:E) * mu (D `&` [set x | (`|g x| >= a%:E)%E]) <= \int[mu]_(x in D) f `|g x|.
 Proof.
 move=> mg a0; have ? : measurable (D `&` [set x | (a%:E <= `|g x|)%E]).
-  by apply: emeasurable_fun_c_infty => //; exact: measurable_fun_comp.
+  by apply: emeasurable_fun_c_infty => //; exact: measurable_funT_comp.
 apply: (@le_trans _ _ (\int[mu]_(x in D `&` [set x | `|g x| >= a%:E]) f `|g x|)).
   rewrite -integral_cst//; apply: ge0_le_integral => //.
   - by move=> x _ /=; rewrite f0 // lee_fin ltW.
   - exact/measurable_fun_cst.
   - by move=> x _ /=; rewrite f0.
-  - apply: measurable_fun_comp => //; apply: measurable_fun_comp => //.
+  - apply: measurable_funT_comp => //; apply: measurable_funT_comp => //.
     exact: measurable_funS mg.
   - by move=> x /= [Dx]; apply: f_nd;
       rewrite inE /= in_itv /= andbT// lee_fin ltW.
 apply: subset_integral => //; last by move=> x _ /=; rewrite f0.
-by apply: measurable_fun_comp => //; exact: measurable_fun_comp.
+by apply: measurable_funT_comp => //; exact: measurable_funT_comp.
 Qed.
 
 Local Close Scope ereal_scope.
@@ -3916,10 +3923,10 @@ Variable (mu : {measure set T -> \bar R}).
 Lemma integrable_abse (D : set T) : measurable D ->
   forall f : T -> \bar R, mu.-integrable D f -> mu.-integrable D (abse \o f).
 Proof.
-move=> mD f [mf fi]; split; first exact: measurable_fun_comp.
+move=> mD f [mf fi]; split; first exact: measurable_funT_comp.
 apply: le_lt_trans fi; apply: ge0_le_integral => //.
-- by apply: measurable_fun_comp => //; exact: measurable_fun_comp.
-- exact: measurable_fun_comp.
+- by apply: measurable_funT_comp => //; exact: measurable_funT_comp.
+- exact: measurable_funT_comp.
 - by move=> t Dt //=; rewrite abse_id.
 Qed.
 
@@ -4012,8 +4019,8 @@ split => //; have Dfg x : D x -> `| f x | <= g x.
   - by apply: is_cvg_abse; apply/cvg_ex; eexists; exact: f_f.
   - by apply: nearW => n; exact: absfg.
 move: ig => [mg]; apply: le_lt_trans; apply: ge0_le_integral => //.
-- exact: measurable_fun_comp.
-- exact: measurable_fun_comp.
+- exact: measurable_funT_comp.
+- exact: measurable_funT_comp.
 - by move=> x Dx /=; rewrite (gee0_abs (g0 Dx)); exact: Dfg.
 Qed.
 
@@ -4050,7 +4057,7 @@ Qed.
 Let mgg n : measurable_fun D (fun x => 2%:E * g x - g_ n x).
 Proof.
 apply/emeasurable_funB => //; first by apply: measurable_funeM; case: ig.
-by apply/measurable_fun_comp => //; exact: emeasurable_funB.
+by apply/measurable_funT_comp => //; exact: emeasurable_funB.
 Qed.
 
 Let gg_ge0 n x : D x -> 0 <= 2%:E * g x - g_ n x.
@@ -4081,16 +4088,16 @@ rewrite [X in _ <= X -> _](_ : _ = \int[mu]_(x in D) (2%:E * g x)  + -
     - exact: integrablerM.
     - have integrable_normfn : mu.-integrable D (abse \o f_ n).
         apply: le_integrable ig => //.
-        - exact: measurable_fun_comp.
+        - exact: measurable_funT_comp.
         - by move=> x Dx /=; rewrite abse_id (le_trans (absfg _ Dx))// lee_abs.
       suff: mu.-integrable D (fun x => `|f_ n x| + `|f x|).
         apply: le_integrable => //.
-        - by apply: measurable_fun_comp => //; exact: emeasurable_funB.
+        - by apply: measurable_funT_comp => //; exact: emeasurable_funB.
         - move=> x Dx.
           by rewrite /g_ abse_id (le_trans (lee_abs_sub _ _))// lee_abs.
       apply: integrableD; [by []| by []|].
       apply: le_integrable dominated_integrable => //.
-      - exact: measurable_fun_comp.
+      - exact: measurable_funT_comp.
       - by move=> x Dx; rewrite /= abse_id.
   rewrite lim_einf_shift // -lim_einfN; congr (_ + lim_einf _).
   by rewrite funeqE => n /=; rewrite -integral_ge0N// => x Dx; rewrite /g_.
@@ -4173,16 +4180,16 @@ split.
   split => //.
   move: if' => [?]; apply: le_lt_trans.
   rewrite le_eqVlt; apply/orP; left; apply/eqP/ae_eq_integral => //;
-    [exact: measurable_fun_comp|exact: measurable_fun_comp|].
+    [exact: measurable_funT_comp|exact: measurable_funT_comp|].
   exists N; split => //; rewrite -(setCK N); apply: subsetC => x Nx Dx.
   by rewrite /f' /restrict mem_set.
 - have := @dominated_cvg0 _ _ _ _ _ mD _ _ _ mu_ f_f' finv ig' f_g'.
   set X := (X in _ -> X --> _); rewrite [X in X --> _ -> _](_ : _ = X) //.
   apply/funext => n; apply: ae_eq_integral => //.
-  + apply: measurable_fun_comp => //; apply: emeasurable_funB => //.
+  + apply: measurable_funT_comp => //; apply: emeasurable_funB => //.
     apply/(measurable_restrict _ (measurableD _ _) _ _).1 => //.
     by apply: (measurable_funS mD) => // x [].
-  + by rewrite /g_; apply: measurable_fun_comp => //; exact: emeasurable_funB.
+  + by rewrite /g_; apply: measurable_funT_comp => //; exact: emeasurable_funB.
   + exists N; split => //; rewrite -(setCK N); apply: subsetC => x /= Nx Dx.
     by rewrite /f_' /f' /restrict mem_set.
 - have := @dominated_cvg _ _ _ _ _ mD _ _ _ mu_ f_f' finv ig' f_g'.
@@ -4523,7 +4530,7 @@ rewrite (_ : (fun _ => _) = fun x => m2 A2 * (\1_A1 x)%:E); last first.
     [rewrite in_xsectionM// mule1|rewrite mule0 notin_xsectionM].
 rewrite ge0_integralM//.
 - by rewrite muleC integral_indic// setIT.
-- by apply: measurable_fun_comp => //; exact/measurable_fun_indic.
+- by apply: measurable_funT_comp => //; exact/measurable_fun_indic.
 - by move=> x _; rewrite lee_fin.
 Qed.
 
@@ -4638,7 +4645,7 @@ have mA1A2 : measurable (A1 `*` A2) by apply: measurableM.
 transitivity (\int[m2]_y (m1 \o ysection (A1 `*` A2)) y) => //.
 rewrite (_ : _ \o _ = fun y => m1 A1 * (\1_A2 y)%:E).
   rewrite ge0_integralM//; last 2 first.
-    - by apply: measurable_fun_comp => //; exact/measurable_fun_indic.
+    - by apply: measurable_funT_comp => //; exact/measurable_fun_indic.
     - by move=> y _; rewrite lee_fin.
   by rewrite integral_indic ?setIT ?mul1e.
 rewrite funeqE => y; rewrite indicE.
@@ -4982,11 +4989,16 @@ rewrite -monotone_convergence //; first exact: eq_integral.
   + by move=> x _; rewrite lee_fin; move/g_nd : ab => /lefP; exact.
 Qed.
 
+Lemma fubini_tonelli :
+  \int[m1]_x \int[m2]_y f (x, y) = \int[m2]_y \int[m1]_x f (x, y).
+Proof. by rewrite -fubini_tonelli1// fubini_tonelli2. Qed.
+
 End fubini_tonelli.
 
 End fubini_tonelli.
 Arguments fubini_tonelli1 {d1 d2 T1 T2 R m1 m2} sm2 f.
 Arguments fubini_tonelli2 {d1 d2 T1 T2 R m1 m2} sm1 sm2 f.
+Arguments fubini_tonelli {d1 d2 T1 T2 R m1 m2} sm1 sm2 f.
 Arguments measurable_fun_fubini_tonelli_F {d1 d2 T1 T2 R m2} sm2 f.
 Arguments measurable_fun_fubini_tonelli_G {d1 d2 T1 T2 R m1} sm1 f.
 
@@ -5006,28 +5018,28 @@ Lemma fubini1a :
   m.-integrable setT f <-> \int[m1]_x \int[m2]_y `|f (x, y)| < +oo.
 Proof.
 split=> [[_]|] ioo.
-- by rewrite -(fubini_tonelli1 _ (abse \o f))//=; exact: measurable_fun_comp.
-- by split=> //; rewrite fubini_tonelli1//; exact: measurable_fun_comp.
+- by rewrite -(fubini_tonelli1 _ (abse \o f))//=; exact: measurable_funT_comp.
+- by split=> //; rewrite fubini_tonelli1//; exact: measurable_funT_comp.
 Qed.
 
 Lemma fubini1b :
   m.-integrable setT f <-> \int[m2]_y \int[m1]_x `|f (x, y)| < +oo.
 Proof.
 split=> [[_]|] ioo.
-- by rewrite -(fubini_tonelli2 _ _ (abse \o f))//=; exact: measurable_fun_comp.
-- by split=> //; rewrite fubini_tonelli2//; exact: measurable_fun_comp.
+- by rewrite -(fubini_tonelli2 _ _ (abse \o f))//=; exact: measurable_funT_comp.
+- by split=> //; rewrite fubini_tonelli2//; exact: measurable_funT_comp.
 Qed.
 
 Let measurable_fun1 : measurable_fun setT (fun x => \int[m2]_y `|f (x, y)|).
 Proof.
 apply: (measurable_fun_fubini_tonelli_F _ (abse \o f)) => //=.
-exact: measurable_fun_comp.
+exact: measurable_funT_comp.
 Qed.
 
 Let measurable_fun2 : measurable_fun setT (fun y => \int[m1]_x `|f (x, y)|).
 Proof.
 apply: (measurable_fun_fubini_tonelli_G _ (abse \o f)) => //=.
-exact: measurable_fun_comp.
+exact: measurable_funT_comp.
 Qed.
 
 Hypothesis imf : m.-integrable setT f.
@@ -5037,7 +5049,7 @@ Lemma ae_integrable1 :
 Proof.
 have : m1.-integrable setT (fun x => \int[m2]_y `|f (x, y)|).
   split => //; rewrite (le_lt_trans _  (fubini1a.1 imf))// ge0_le_integral //.
-  - exact: measurable_fun_comp.
+  - exact: measurable_funT_comp.
   - by move=> *; exact: integral_ge0.
   - by move=> *; rewrite gee0_abs//; exact: integral_ge0.
 move/integrable_ae => /(_ measurableT) [N [mN N0 subN]]; exists N; split => //.
@@ -5050,7 +5062,7 @@ Lemma ae_integrable2 :
 Proof.
 have : m2.-integrable setT (fun y => \int[m1]_x `|f (x, y)|).
   split => //; rewrite (le_lt_trans _ (fubini1b.1 imf))// ge0_le_integral //.
-  - exact: measurable_fun_comp.
+  - exact: measurable_funT_comp.
   - by move=> *; exact: integral_ge0.
   - by move=> *; rewrite gee0_abs//; exact: integral_ge0.
 move/integrable_ae => /(_ measurableT) [N [mN N0 subN]]; exists N; split => //.
@@ -5084,30 +5096,30 @@ Qed.
 Let integrable_Fplus : m1.-integrable setT Fplus.
 Proof.
 split=> //; apply: le_lt_trans (fubini1a.1 imf); apply: ge0_le_integral => //.
-- exact: measurable_fun_comp.
+- exact: measurable_funT_comp.
 - by move=> x _; exact: integral_ge0.
 - move=> x _; apply: le_trans.
     apply: le_abse_integral => //; apply: emeasurable_fun_funepos => //.
     exact: measurable_fun_prod1.
   apply: ge0_le_integral => //.
-  - apply: measurable_fun_comp => //.
+  - apply: measurable_funT_comp => //.
     by apply: emeasurable_fun_funepos => //; exact: measurable_fun_prod1.
-  - by apply: measurable_fun_comp => //; exact/measurable_fun_prod1.
+  - by apply: measurable_funT_comp => //; exact/measurable_fun_prod1.
   - by move=> y _; rewrite gee0_abs// -/((abse \o f) (x, y)) fune_abse lee_addl.
 Qed.
 
 Let integrable_Fminus : m1.-integrable setT Fminus.
 Proof.
 split=> //; apply: le_lt_trans (fubini1a.1 imf); apply: ge0_le_integral => //.
-- exact: measurable_fun_comp.
+- exact: measurable_funT_comp.
 - by move=> *; exact: integral_ge0.
 - move=> x _; apply: le_trans.
     apply: le_abse_integral => //; apply: emeasurable_fun_funeneg => //.
     exact: measurable_fun_prod1.
   apply: ge0_le_integral => //.
-  + apply: measurable_fun_comp => //; apply: emeasurable_fun_funeneg => //.
+  + apply: measurable_funT_comp => //; apply: emeasurable_fun_funeneg => //.
     exact: measurable_fun_prod1.
-  + by apply: measurable_fun_comp => //; exact: measurable_fun_prod1.
+  + by apply: measurable_funT_comp => //; exact: measurable_fun_prod1.
   + by move=> y _; rewrite gee0_abs// -/((abse \o f) (x, y)) fune_abse lee_addr.
 Qed.
 
@@ -5137,30 +5149,30 @@ Proof. by rewrite GE; exact: emeasurable_funB. Qed.
 Let integrable_Gplus : m2.-integrable setT Gplus.
 Proof.
 split=> //; apply: le_lt_trans (fubini1b.1 imf); apply: ge0_le_integral => //.
-- exact: measurable_fun_comp.
+- exact: measurable_funT_comp.
 - by move=> *; exact: integral_ge0.
 - move=> y _; apply: le_trans.
     apply: le_abse_integral => //; apply: emeasurable_fun_funepos => //.
     exact: measurable_fun_prod2.
   apply: ge0_le_integral => //.
-  - apply: measurable_fun_comp => //.
+  - apply: measurable_funT_comp => //.
     by apply: emeasurable_fun_funepos => //; exact: measurable_fun_prod2.
-  - by apply: measurable_fun_comp => //; exact: measurable_fun_prod2.
+  - by apply: measurable_funT_comp => //; exact: measurable_fun_prod2.
   - by move=> x _; rewrite gee0_abs// -/((abse \o f) (x, y)) fune_abse lee_addl.
 Qed.
 
 Let integrable_Gminus : m2.-integrable setT Gminus.
 Proof.
 split=> //; apply: le_lt_trans (fubini1b.1 imf); apply: ge0_le_integral => //.
-- exact: measurable_fun_comp.
+- exact: measurable_funT_comp.
 - by move=> *; exact: integral_ge0.
 - move=> y _; apply: le_trans.
     apply: le_abse_integral => //; apply: emeasurable_fun_funeneg => //.
     exact: measurable_fun_prod2.
   apply: ge0_le_integral => //.
-  + apply: measurable_fun_comp => //.
+  + apply: measurable_funT_comp => //.
     by apply: emeasurable_fun_funeneg => //; exact: measurable_fun_prod2.
-  + by apply: measurable_fun_comp => //; exact: measurable_fun_prod2.
+  + by apply: measurable_funT_comp => //; exact: measurable_fun_prod2.
   + by move=> x _; rewrite gee0_abs// -/((abse \o f) (x, y)) fune_abse lee_addr.
 Qed.
 
diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v
index 02534fb396..e3b821f8d7 100644
--- a/theories/lebesgue_measure.v
+++ b/theories/lebesgue_measure.v
@@ -695,23 +695,23 @@ Qed.
 
 Lemma __deprecated__itv_cpinfty_pinfty : `[+oo%E, +oo[%classic = [set +oo%E] :> set (\bar R).
 Proof. by rewrite itv_cyy. Qed.
-#[deprecated(since="mathcomp-analysis 1.6.0", note="renamed `itv_cyy`")]
+#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `itv_cyy`")]
 Notation itv_cpinfty_pinfty := __deprecated__itv_cpinfty_pinfty.
 
 Lemma __deprecated__itv_opinfty_pinfty : `]+oo%E, +oo[%classic = set0 :> set (\bar R).
 Proof. by rewrite itv_oyy. Qed.
-#[deprecated(since="mathcomp-analysis 1.6.0", note="renamed `itv_oyy`")]
+#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `itv_oyy`")]
 Notation itv_opinfty_pinfty := __deprecated__itv_opinfty_pinfty.
 
 Lemma __deprecated__itv_cninfty_pinfty : `[-oo%E, +oo[%classic = setT :> set (\bar R).
 Proof. by rewrite itv_cNyy. Qed.
-#[deprecated(since="mathcomp-analysis 1.6.0", note="renamed `itv_cNyy`")]
+#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `itv_cNyy`")]
 Notation itv_cninfty_pinfty := __deprecated__itv_cninfty_pinfty.
 
 Lemma __deprecated__itv_oninfty_pinfty :
   `]-oo%E, +oo[%classic = ~` [set -oo]%E :> set (\bar R).
 Proof. by rewrite itv_oNyy. Qed.
-#[deprecated(since="mathcomp-analysis 1.6.0", note="renamed `itv_oNyy`")]
+#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `itv_oNyy`")]
 Notation itv_oninfty_pinfty := __deprecated__itv_oninfty_pinfty.
 
 Lemma emeasurable_itv_bnd_pinfty b (y : \bar R) :
@@ -1536,6 +1536,12 @@ End coutinuous_measurable.
 
 Section standard_measurable_fun.
 
+Lemma measurable_fun_opp (R : realType) : measurable_fun [set: R] -%R.
+Proof.
+apply: continuous_measurable_fun.
+by have := @opp_continuous R [the normedModType R of R^o].
+Qed.
+
 Lemma measurable_fun_normr (R : realType) (D : set R) :
   measurable_fun D (@normr _ R).
 Proof.
@@ -1586,7 +1592,7 @@ Qed.
 Lemma measurable_funrM D f (k : R) : measurable_fun D f ->
   measurable_fun D (fun x => k * f x).
 Proof.
-apply: (@measurable_fun_comp _ _ _ _ _ _ ( *%R k)).
+apply: (@measurable_funT_comp _ _ _ _ _ _ ( *%R k)).
 by apply: continuous_measurable_fun; apply: mulrl_continuous.
 Qed.
 
@@ -1606,7 +1612,7 @@ Qed.
 Lemma measurable_fun_exprn D n f :
   measurable_fun D f -> measurable_fun D (fun x => f x ^+ n).
 Proof.
-apply: measurable_fun_comp ((@GRing.exp R)^~ n) _ _ _.
+apply: measurable_funT_comp ((@GRing.exp R)^~ n) _ _ _.
 by apply: continuous_measurable_fun; apply: exprn_continuous.
 Qed.
 
@@ -1747,7 +1753,7 @@ Lemma EFin_measurable_fun d (T : measurableType d) (R : realType) (D : set T)
     (g : T -> R) :
   measurable_fun D (EFin \o g) <-> measurable_fun D g.
 Proof.
-split=> [mf mD A mA|]; last by move=> mg; exact: measurable_fun_comp.
+split=> [mf mD A mA|]; last by move=> mg; exact: measurable_funT_comp.
 rewrite [X in measurable X](_ : _ = D `&` (EFin \o g) @^-1` (EFin @` A)).
   by apply: mf => //; exists A => //; exists set0; [constructor|rewrite setU0].
 congr (_ `&` _);rewrite eqEsubset; split=> [|? []/= _ /[swap] -[->//]].
@@ -1814,7 +1820,7 @@ Qed.
 
 Lemma emeasurable_funN D (f : T -> \bar R) :
   measurable_fun D f -> measurable_fun D (\- f).
-Proof. by apply: measurable_fun_comp => //; exact: emeasurable_fun_minus. Qed.
+Proof. by apply: measurable_funT_comp => //; exact: emeasurable_fun_minus. Qed.
 
 Lemma emeasurable_fun_funepos D (f : T -> \bar R) :
   measurable_fun D f -> measurable_fun D f^\+.
@@ -1851,7 +1857,7 @@ rewrite [X in _ --> X](_ : _ = ereal_inf (range (esups (f^~t)))).
 by congr (ereal_inf [set _ | _ in _]); rewrite predeqE.
 Qed.
 
-#[deprecated(since="mathcomp-analysis 1.6.0",
+#[deprecated(since="mathcomp-analysis 0.6.0",
   note="renamed `measurable_fun_lim_esup`")]
 Notation measurable_fun_elim_sup := measurable_fun_lim_esup.
 
diff --git a/theories/measure.v b/theories/measure.v
index 09bbd114fd..2cd64ffb60 100644
--- a/theories/measure.v
+++ b/theories/measure.v
@@ -650,6 +650,11 @@ Canonical semiRingOfSets_choiceType d (T : semiRingOfSetsType d) :=
 Canonical semiRingOfSets_ptType d (T : semiRingOfSetsType d) :=
   PointedType T ptclass.
 
+Lemma measurable_curry (T1 T2 : Type) d (T : semiRingOfSetsType d)
+    (G : T1 * T2 -> set T) (x : T1 * T2) :
+  measurable (G x) <-> measurable (curry G x.1 x.2).
+Proof. by case: x. Qed.
+
 Notation "d .-measurable" := (@measurable d%mdisp) : classical_set_scope.
 Notation "'measurable" :=
   (@measurable default_measure_display) : classical_set_scope.
@@ -972,13 +977,22 @@ Implicit Type D E : set T1.
 Lemma measurable_fun_id D : measurable_fun D id.
 Proof. by move=> mD A mA; apply: measurableI. Qed.
 
-Lemma measurable_fun_comp (f : T2 -> T3) E (g : T1 -> T2) :
-  measurable_fun setT f -> measurable_fun E g -> measurable_fun E (f \o g).
+Lemma measurable_fun_comp F (f : T2 -> T3) E (g : T1 -> T2) :
+  measurable F -> g @` E `<=` F ->
+  measurable_fun F f -> measurable_fun E g -> measurable_fun E (f \o g).
 Proof.
-move=> mf mg /= mE A mA; rewrite comp_preimage; apply/mg => //.
-by rewrite -[X in measurable X]setTI; apply/mf.
+move=> mF FgE mf mg /= mE A mA.
+rewrite comp_preimage.
+rewrite (_ : _ `&` _ = E `&` g @^-1` (F `&` f @^-1` A)); last first.
+  apply/seteqP; split=> [|? [?] []//].
+  by move=> x/= [Ex Afgx]; split => //; split => //; exact: FgE.
+by apply/mg => //; exact: mf.
 Qed.
 
+Lemma measurable_funT_comp (f : T2 -> T3) E (g : T1 -> T2) :
+  measurable_fun setT f -> measurable_fun E g -> measurable_fun E (f \o g).
+Proof. exact: measurable_fun_comp. Qed.
+
 Lemma eq_measurable_fun D (f g : T1 -> T2) :
   {in D, f =1 g} -> measurable_fun D f -> measurable_fun D g.
 Proof.
@@ -1547,10 +1561,20 @@ Arguments measure_bigcup {d R T} mu A.
   solve [apply: measure_sigma_additive] : core.
 #[global] Hint Extern 0 (is_true (0 <= _)) => solve [apply: measure_ge0] : core.
 
-Definition finite_measure d (T : measurableType d) (R : realType)
+Definition finite_measure d (T : measurableType d) (R : numDomainType)
     (mu : set T -> \bar R) :=
   mu setT < +oo.
 
+Lemma finite_measure_sigma_finite d (T : measurableType d) (R : realFieldType)
+  (mu : {measure set T -> \bar R}) :
+  finite_measure mu -> sigma_finite setT mu.
+Proof.
+exists (fun i => if i \in [set 0%N] then setT else set0).
+  by rewrite -bigcup_mkcondr setTI bigcup_const//; exists 0%N.
+move=> n; split; first by case: ifPn.
+by case: ifPn => // _; rewrite ?measure0//; exact: finite_measure.
+Qed.
+
 Section pushforward_measure.
 Local Open Scope ereal_scope.
 Context d d' (T1 : measurableType d) (T2 : measurableType d') (f : T1 -> T2).
@@ -1617,10 +1641,21 @@ Arguments dirac {d T} _ {R}.
 
 Notation "\d_ a" := (dirac a) : ring_scope.
 
-Lemma diracE d (T : measurableType d) (R : realFieldType) a (A : set T) :
-  \d_a A = (a \in A)%:R%:E :> \bar R.
+Section dirac_lemmas_realFieldType.
+Local Open Scope ereal_scope.
+Context d (T : measurableType d) (R : realFieldType).
+
+Lemma diracE a (A : set T) : \d_a A = (a \in A)%:R%:E :> \bar R.
 Proof. by rewrite /dirac indicE. Qed.
 
+Lemma dirac0 (a : T) : \d_a set0 = 0 :> \bar R.
+Proof. by rewrite diracE in_set0. Qed.
+
+Lemma diracT (a : T) : \d_a setT = 1 :> \bar R.
+Proof. by rewrite diracE in_setT. Qed.
+
+End dirac_lemmas_realFieldType.
+
 Section dirac_lemmas.
 Local Open Scope ereal_scope.
 Context d (T : measurableType d) (R : realType).
@@ -2909,8 +2944,7 @@ apply: (@le_trans _ _ (\sum_(k < n) mu (X `&` A k) + mu (X `&` ~` B n))).
 rewrite [in leRHS](caratheodory_measurable_bigsetU MA n) lee_add2r //.
 by rewrite caratheodory_additive.
 Qed.
-
-#[deprecated(since="mathcomp-analysis 1.6.0",
+#[deprecated(since="mathcomp-analysis 0.6.0",
       note="renamed `caratheodory_lime_le`")]
 Notation caratheodory_lim_lee := caratheodory_lime_le.
 
@@ -3624,23 +3658,63 @@ End product_salgebra_g_measurableType.
 Section prod_measurable_fun.
 Context d d1 d2 (T : measurableType d) (T1 : measurableType d1)
         (T2 : measurableType d2).
-Variable f : T -> T1 * T2.
 
-Lemma prod_measurable_funP : measurable_fun setT f <->
-  measurable_fun setT (fst \o f) /\ measurable_fun setT (snd \o f).
+Lemma prod_measurable_funP (h : T -> T1 * T2) : measurable_fun setT h <->
+  measurable_fun setT (fst \o h) /\ measurable_fun setT (snd \o h).
 Proof.
-apply: (@iff_trans _ (preimage_classes (fst \o f) (snd \o f) `<=` measurable)).
+apply: (@iff_trans _ (preimage_classes (fst \o h) (snd \o h) `<=` measurable)).
 - rewrite preimage_classes_comp; split=> [mf A [C HC <-]|f12]; first exact: mf.
   by move=> _ A mA; apply: f12; exists A.
-- split => [h|[mf1 mf2]].
-    split => _ A mA; apply: h; apply: sub_sigma_algebra;
+- split => [h12|[mf1 mf2]].
+    split => _ A mA; apply: h12; apply: sub_sigma_algebra;
     by [left; exists A|right; exists A].
   apply: smallest_sub; first exact: sigma_algebra_measurable.
   by rewrite subUset; split=> [|] A [C mC <-]; [exact: mf1|exact: mf2].
 Qed.
 
+Lemma measurable_fun_pair (f : T -> T1) (g : T -> T2) :
+  measurable_fun setT f -> measurable_fun setT g ->
+  measurable_fun setT (fun x => (f x, g x)).
+Proof. by move=> mf mg; apply/prod_measurable_funP. Qed.
+
 End prod_measurable_fun.
 
+Section prod_measurable_proj.
+Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2).
+
+Lemma measurable_fun_fst : measurable_fun setT (@fst T1 T2).
+Proof.
+by have /prod_measurable_funP[] :=
+  @measurable_fun_id _ [the measurableType _ of (T1 * T2)%type] setT.
+Qed.
+
+Lemma measurable_fun_snd : measurable_fun setT (@snd T1 T2).
+Proof.
+by have /prod_measurable_funP[] :=
+  @measurable_fun_id _ [the measurableType _ of (T1 * T2)%type] setT.
+Qed.
+
+Lemma measurable_fun_swap : measurable_fun [set: T1 * T2] (@swap T1 T2).
+Proof.
+by apply/prod_measurable_funP => /=; split;
+  [exact: measurable_fun_snd|exact: measurable_fun_fst].
+Qed.
+
+End prod_measurable_proj.
+
+Lemma measurable_fun_if_pair d d' (X : measurableType d)
+    (Y : measurableType d') (x y : X -> Y) :
+  measurable_fun setT x -> measurable_fun setT y ->
+  measurable_fun setT (fun tb => if tb.2 then x tb.1 else y tb.1).
+Proof.
+move=> mx my.
+have {}mx : measurable_fun [set: X * bool] (x \o fst).
+  by apply: measurable_funT_comp => //; exact: measurable_fun_fst.
+have {}my : measurable_fun [set: X * bool] (y \o fst).
+  by apply: measurable_funT_comp => //; exact: measurable_fun_fst.
+by apply: measurable_fun_ifT => //=; exact: measurable_fun_snd.
+Qed.
+
 Section partial_measurable_fun.
 Context d d1 d2 (T : measurableType d) (T1 : measurableType d1)
   (T2 : measurableType d2).
@@ -3652,8 +3726,8 @@ Proof.
 move=> mf; pose pairx := fun y : T2 => (x, y).
 have m1pairx : measurable_fun setT (fst \o pairx) by exact/measurable_fun_cst.
 have m2pairx : measurable_fun setT (snd \o pairx) by exact/measurable_fun_id.
-have : measurable_fun setT pairx by exact/(proj2 (prod_measurable_funP _)).
-exact: measurable_fun_comp.
+have ? : measurable_fun setT pairx by exact/(proj2 (prod_measurable_funP _)).
+exact: (measurable_fun_comp _ _ mf).
 Qed.
 
 Lemma measurable_fun_prod2 y :
@@ -3663,7 +3737,7 @@ move=> mf; pose pairy := fun x : T1 => (x, y).
 have m1pairy : measurable_fun setT (fst \o pairy) by exact/measurable_fun_id.
 have m2pairy : measurable_fun setT (snd \o pairy) by exact/measurable_fun_cst.
 have : measurable_fun setT pairy by exact/(proj2 (prod_measurable_funP _)).
-exact: measurable_fun_comp.
+exact: (measurable_fun_comp _ _ mf).
 Qed.
 
 End partial_measurable_fun.
diff --git a/theories/normedtype.v b/theories/normedtype.v
index 4bcbfce7c1..d2e2159cb6 100644
--- a/theories/normedtype.v
+++ b/theories/normedtype.v
@@ -2591,7 +2591,7 @@ Lemma __deprecated__continuous_cvg_dist {R : numFieldType}
   (V W : pseudoMetricNormedZmodType R) (f : V -> W) x l :
   continuous f -> x --> l -> forall e : {posnum R}, `|f l - f x| < e%:num.
 Proof. by move=> cf /cvg_eq->// e; rewrite subrr normr0. Qed.
-#[deprecated(since="mathcomp-analysis 1.6.0",
+#[deprecated(since="mathcomp-analysis 0.6.0",
   note="simply use the fact that `(x --> l) -> (x = l)`")]
 Notation continuous_cvg_dist := __deprecated__continuous_cvg_dist.