put in better shape to RFC

_CoqProject

@@ -26,11 +26,11 @@ theories/cardinality.v
 theories/esum.v
 theories/fsbigop.v
 theories/set_interval.v
+theories/lebesgue_measure.v
 theories/forms.v
 theories/derive.v
 theories/measure.v
 theories/numfun.v
-theories/lebesgue_measure.v
 theories/lebesgue_integral.v
 theories/probability.v
 theories/summability.v

theories/lebesgue_integral.v

@@ -2370,6 +2370,63 @@ Qed.
 
 End integral_dirac.
 
+
+Section transfer.
+Local Open Scope ereal_scope.
+Variables (d1 d2 : _) (T1 : measurableType d1) (T2 : measurableType d2).
+Variables (phi : T1 -> T2) (mphi : measurable_fun setT phi).
+Variables (R : realType) (mu : {measure set T1 -> \bar R}).
+
+Lemma transfer (f : T2 -> \bar R) :
+  measurable_fun setT f -> (forall y, 0 <= f y) ->
+  \int[mpushforward mphi mu]_y f y =
+  \int[mu]_x (f \o phi) x.
+Proof.
+move=> mf f0.
+pose pt2 := phi point.
+have [f_ [ndf_ f_f]] := approximation measurableT mf (fun t _ => f0 t).
+transitivity
+    (lim (fun n => \int[mpushforward mphi mu]_x (f_ n x)%:E)).
+  rewrite -monotone_convergence//.
+  - by apply: eq_integral => y _; apply/esym/cvg_lim => //; exact: f_f.
+  - by move=> n; exact/EFin_measurable_fun.
+  - by move=> n y _; rewrite lee_fin.
+  - 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.
+    - 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.
+rewrite funeqE => n.
+have mfnphi : forall r, measurable (f_ n @^-1` [set r] \o phi).
+  move=> r.
+  rewrite -[_ \o _]/(phi @^-1` (f_ n @^-1` [set r])) -(setTI (_ @^-1` _)).
+  exact/mphi.
+transitivity (\sum_(k <- fset_set (range (f_ n)))
+  \int[mu]_x (k * \1_(((f_ n) @^-1` [set k]) \o phi) x)%:E).
+  under eq_integral do rewrite fimfunE -sumEFin.
+  rewrite ge0_integral_sum//; last 2 first.
+    - move=> y; apply/EFin_measurable_fun; apply: measurable_funM.
+        exact: measurable_fun_cst.
+      by rewrite (_ : \1_ _ = mindic R (measurable_sfunP (f_ n) y)).
+    - by move=> y x _; rewrite muleindic_ge0.
+  apply eq_bigr => r _; rewrite integralM_indic_nnsfun// integral_indic//.
+  rewrite /= /mpushforward.
+  rewrite (@integralM_indic _ _ _ _ _ _ (fun r => f_ n @^-1` [set r] \o phi))//.
+    by congr (_ * _)%E; rewrite [RHS](@integral_indic).
+  by move=> r0; rewrite preimage_nnfun0.
+rewrite -ge0_integral_sum//; last 2 first.
+  - move=> r; apply/EFin_measurable_fun; apply: measurable_funM.
+      exact: measurable_fun_cst.
+    by rewrite (_ : \1_ _ = mindic R (mfnphi r)).
+  - by move=> r x _; rewrite muleindic_ge0.
+by apply eq_integral => x _; rewrite sumEFin -fimfunE.
+Qed.
+
+End transfer.
+
 Section integral_measure_sum_nnsfun.
 Local Open Scope ereal_scope.
 Variables (d : _) (T : measurableType d) (R : realType).

theories/lebesgue_measure.v

@@ -1504,6 +1504,9 @@ Qed.
 
 End standard_measurable_fun.
 
+#[global] Hint Extern 0 (measurable_fun _ normr) =>
+  solve [exact: measurable_fun_normr] : core.
+
 Section measurable_fun_realType.
 Variables (d : measure_display) (T : measurableType d) (R : realType).
 Implicit Types (D : set T) (f g : T -> R).

theories/measure.v

@@ -1454,14 +1454,19 @@ 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 mpushforward d d' (T1 : measurableType d) (T2 : measurableType d')
+    (R : realFieldType) (f : T1 -> T2) (mf : measurable_fun setT f)
+    (m : {measure set T1 -> \bar R}) A :=
+  m (f @^-1` A).
+
 Section pushforward_measure.
 Local Open Scope ereal_scope.
 Variables (d d' : measure_display).
 Variables (T1 : measurableType d) (T2 : measurableType d') (f : T1 -> T2).
 Hypothesis mf : measurable_fun setT f.
 Variables (R : realFieldType) (m : {measure set T1 -> \bar R}).
 
-Definition pushforward A := m (f @^-1` A).
+Local Notation pushforward := (mpushforward mf m).
 
 Let pushforward0 : pushforward set0 = 0.
 Proof. by rewrite /pushforward preimage_set0 measure0. Qed.