transfer lemma

CHANGELOG_UNRELEASED.md

@@ -39,6 +39,10 @@
   + lemmas `subset_fst_set`, `subset_snd_set`, `fst_set_fst`, `snd_set_snd`,
     `fset_setM`, `snd_setM`, `fst_setMR`
   + lemmas `xsection_snd_set`, `ysection_fst_set`
+  + Hint about `measurable_fun_normr`
+- in `lebesgue_integral.v`:
+  + lemma `integral_pushforward`
+
 
 ### Changed
 
@@ -49,6 +53,10 @@
 - moved from `lebesgue_integral.v` to `classical_sets.v`:
   + `mem_set_pair1` -> `mem_xsection`
   + `mem_set_pair2` -> `mem_ysection`
+- in `lebesgue_measure.v`:
+  + `pushforward` requires a proof that its argument is measurable
+- in `lebesgue_integral.v`:
+  + change implicits of `integralM_indic`
 
 ### Renamed
 

theories/lebesgue_integral.v

@@ -2196,6 +2196,7 @@ by rewrite preimage_nnfun0.
 Qed.
 
 End integralM_indic.
+Arguments integralM_indic {d T R m D} mD f.
 
 Section integral_mscale.
 Local Open Scope ereal_scope.
@@ -2389,6 +2390,57 @@ Qed.
 
 End integral_cst.
 
+Section transfer.
+Local Open Scope ereal_scope.
+Variables (d1 d2 : _) (X : measurableType d1) (Y : measurableType d2).
+Variables (phi : X -> Y) (mphi : measurable_fun setT phi).
+Variables (R : realType) (mu : {measure set X -> \bar R}).
+
+Lemma integral_pushforward (f : Y -> \bar R) :
+  measurable_fun setT f -> (forall y, 0 <= f y) ->
+  \int[pushforward mu mphi]_y f y = \int[mu]_x (f \o phi) x.
+Proof.
+move=> mf f0.
+have [f_ [ndf_ f_f]] := approximation measurableT mf (fun t _ => f0 t).
+transitivity (lim (fun n => \int[pushforward mu mphi]_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.
+apply/funext => n.
+have mfnphi r : measurable (f_ n @^-1` [set r] \o phi).
+  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 nnfun_muleindic_ge0.
+  apply eq_bigr => r _; rewrite integralM_indic_nnsfun// integral_indic//=.
+  rewrite (integralM_indic _ (fun r => f_ n @^-1` [set r] \o phi))//.
+    by congr (_ * _); 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 nnfun_muleindic_ge0.
+by apply eq_integral => x _; rewrite sumEFin -fimfunE.
+Qed.
+
+End transfer.
+
 Section integral_dirac.
 Local Open Scope ereal_scope.
 Variables (d : measure_display) (T : measurableType d) (a : T) (R : realType).

theories/lebesgue_measure.v

@@ -1521,6 +1521,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

@@ -84,7 +84,8 @@ From HB Require Import structures.
 (*     isMeasure == factory corresponding to the type of measures             *)
 (*     Measure == structure corresponding to measures                         *)
 (*                                                                            *)
-(*   pushforward f m == pushforward/image measure of m by f                   *)
+(*  pushforward mf m == pushforward/image measure of m by f, where mf is a    *)
+(*                      proof that f is measurable                            *)
 (*              \d_a == Dirac measure                                         *)
 (*         msum mu n == the measure corresponding to the sum of the measures  *)
 (*                      mu_0, ..., mu_{n-1}                                   *)
@@ -1461,18 +1462,19 @@ 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).
+Definition pushforward (mf : measurable_fun setT f) A := m (f @^-1` A).
+
+Hypothesis mf : measurable_fun setT f.
 
-Let pushforward0 : pushforward set0 = 0.
+Let pushforward0 : pushforward mf set0 = 0.
 Proof. by rewrite /pushforward preimage_set0 measure0. Qed.
 
-Let pushforward_ge0 A : 0 <= pushforward A.
+Let pushforward_ge0 A : 0 <= pushforward mf A.
 Proof. by apply: measure_ge0; rewrite -[X in measurable X]setIT; apply: mf. Qed.
 
-Let pushforward_sigma_additive : semi_sigma_additive pushforward.
+Let pushforward_sigma_additive : semi_sigma_additive (pushforward mf).
 Proof.
 move=> F mF tF mUF; rewrite /pushforward preimage_bigcup.
 apply: measure_semi_sigma_additive.
@@ -1483,7 +1485,7 @@ apply: measure_semi_sigma_additive.
 Qed.
 
 HB.instance Definition _ := isMeasure.Build _ _ _
-  pushforward pushforward0 pushforward_ge0 pushforward_sigma_additive.
+  (pushforward mf) pushforward0 pushforward_ge0 pushforward_sigma_additive.
 
 End pushforward_measure.