rebase

Author: affeldt-aist

theories/measure.v

@@ -1464,14 +1464,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.