generalize pushforward (#1661)

Generalize pushforward

Author: t6s

CHANGELOG_UNRELEASED.md

@@ -113,6 +113,7 @@
   + lemma `ae_eq_comp2`
   + lemma `ae_foralln`
   + lemma `ae_eqe_mul2l`
+  + definition `pushforward` (to take a function instead of a proof)
 
 - new file `ess_sup_inf.v`:
   + lemma `measure0_ae`

theories/charge.v

@@ -488,16 +488,16 @@ Variables (R : realFieldType) (nu : {charge set T1 -> \bar R}).
 
 Hypothesis mf : measurable_fun setT f.
 
-Let pushforward0 : pushforward nu mf set0 = 0.
+Let pushforward0 : pushforward nu f set0 = 0.
 Proof. by rewrite /pushforward preimage_set0 charge0. Qed.
 
-Let pushforward_finite A : measurable A -> pushforward nu mf A \is a fin_num.
+Let pushforward_finite A : measurable A -> pushforward nu f A \is a fin_num.
 Proof.
 move=> mA; apply: fin_num_measure.
 by rewrite -[X in measurable X]setTI; exact: mf.
 Qed.
 
-Let pushforward_sigma_additive : semi_sigma_additive (pushforward nu mf).
+Let pushforward_sigma_additive : semi_sigma_additive (pushforward nu f).
 Proof.
 move=> F mF tF mUF; rewrite /pushforward preimage_bigcup.
 apply: charge_semi_sigma_additive.
@@ -507,7 +507,7 @@ apply: charge_semi_sigma_additive.
 - by rewrite -preimage_bigcup -[X in measurable X]setTI; exact: mf.
 Qed.
 
-HB.instance Definition _ := isCharge.Build _ _ _ (pushforward nu mf)
+HB.instance Definition _ := isCharge.Build _ _ _ (pushforward nu f)
   pushforward0 pushforward_finite pushforward_sigma_additive.
 
 End pushforward_charge.
@@ -528,7 +528,7 @@ Section dominates_pushforward.
 Lemma dominates_pushforward d d' (T : measurableType d) (T' : measurableType d')
   (R : realType) (mu : {measure set T -> \bar R})
   (nu : {charge set T -> \bar R}) (f : T -> T') (mf : measurable_fun setT f) :
-  nu `<< mu -> pushforward nu mf `<< pushforward mu mf.
+  nu `<< mu -> pushforward nu f `<< pushforward mu f.
 Proof.
 by move=> numu A mA; apply: numu; rewrite -[X in measurable X]setTI; exact: mf.
 Qed.

theories/lebesgue_integral_theory/lebesgue_integrable.v

@@ -757,7 +757,7 @@ Let mf_mixin := isMeasurableFun.Build _ _ _ _ _ mf.
 Let mf_pack := MeasurableFun.Pack (MeasurableFun.Class mf_mixin).
 
 Lemma integrable_pushforward :
-  measurable D -> (pushforward mu mphi).-integrable D f.
+  measurable D -> (pushforward mu phi).-integrable D f.
 Proof.
 move=> mD; apply/integrableP; split; first exact: (measurable_funP mf_pack).
 move/integrableP : (intf) => [_]; apply: le_lt_trans.
@@ -768,7 +768,7 @@ Qed.
 Local Open Scope ereal_scope.
 
 Lemma integral_pushforward : measurable D ->
-  \int[pushforward mu mphi]_(y in D) f y =
+  \int[pushforward mu phi]_(y in D) f y =
   \int[mu]_(x in phi @^-1` D) (f \o phi) x.
 Proof.
 move=> mD.
@@ -782,7 +782,7 @@ rewrite -[X in _ = _ - X]ge0_integral_pushforward//; last first.
 rewrite -integralB//=; last first.
 - by apply: integrable_funeneg => //=; exact: integrable_pushforward.
 - by apply: integrable_funepos => //=; exact: integrable_pushforward.
-- by apply/eq_integral => x _; rewrite /= [in LHS](funeposneg f).
+- by apply/eq_integral=> // x _; rewrite /= [in LHS](funeposneg f).
 Qed.
 
 End transfer.

theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v

@@ -520,14 +520,14 @@ Import HBNNSimple.
 
 Lemma ge0_integral_pushforward D (f : Y -> \bar R) :
   measurable D -> measurable_fun D f -> {in D, forall y, 0 <= f y} ->
-  \int[pushforward mu mphi]_(y in D) f y =
+  \int[pushforward mu phi]_(y in D) f y =
   \int[mu]_(x in phi @^-1` D) (f \o phi) x.
 Proof.
 move=> mD mf f0.
 have mphiD : measurable (phi @^-1` D).
   by rewrite -(setTI (_ @^-1` _)); exact: (measurable_funP mphi_pack).
 pose f_ := nnsfun_approx mD mf.
-transitivity (limn (fun n => \int[pushforward mu mphi]_(x in D) (f_ n x)%:E)).
+transitivity (limn (fun n => \int[pushforward mu phi]_(x in D) (f_ n x)%:E)).
   rewrite -monotone_convergence//.
   - apply: eq_integral => y /[!inE] yD; apply/esym/cvg_lim => //.
     by apply: cvg_nnsfun_approx=> // *; apply: f0; rewrite inE.

theories/measure.v

@@ -157,9 +157,9 @@ From mathcomp Require Import sequences esum numfun.
 (*                                                                            *)
 (* ## Instances of measures                                                   *)
 (* ```                                                                        *)
-(*  pushforward m mf == pushforward/image measure of m by f, where mf is a    *)
-(*                      proof that f is measurable                            *)
-(*                      m has type set T -> \bar R.                           *)
+(*   pushforward m f == pushforward of a set function m : set T1 -> \bar R    *)
+(*                      by f : T1 -> T2;  pushforward/image measure if m is   *)
+(*                      a measure and f measurable                            *)
 (*              \d_a == Dirac measure                                         *)
 (*         msum mu n == the measure corresponding to the sum of the measures  *)
 (*                      mu_0, ..., mu_{n-1}                                   *)
@@ -2245,8 +2245,8 @@ Arguments measure_bigcup {d R T} _ _.
 
 Definition pushforward d1 d2 (T1 : sigmaRingType d1) (T2 : sigmaRingType d2)
   (R : realFieldType) (m : set T1 -> \bar R) (f : T1 -> T2)
-  of measurable_fun [set: T1] f := fun A => m (f @^-1` A).
-Arguments pushforward {d1 d2 T1 T2 R} m {f}.
+  := fun A => m (f @^-1` A).
+Arguments pushforward {d1 d2 T1 T2 R}.
 
 Section pushforward_measure.
 Local Open Scope ereal_scope.
@@ -2255,13 +2255,13 @@ Context d d' (T1 : measurableType d) (T2 : measurableType d')
 Variables (m : {measure set T1 -> \bar R}) (f : T1 -> T2).
 Hypothesis mf : measurable_fun [set: T1] f.
 
-Let pushforward0 : pushforward m mf set0 = 0.
+Let pushforward0 : pushforward m f set0 = 0.
 Proof. by rewrite /pushforward preimage_set0 measure0. Qed.
 
-Let pushforward_ge0 A : 0 <= pushforward m mf A.
+Let pushforward_ge0 A : 0 <= pushforward m f A.
 Proof. by apply: measure_ge0; rewrite -[X in measurable X]setIT; apply: mf. Qed.
 
-Let pushforward_sigma_additive : semi_sigma_additive (pushforward m mf).
+Let pushforward_sigma_additive : semi_sigma_additive (pushforward m f).
 Proof.
 move=> F mF tF mUF; rewrite /pushforward preimage_bigcup.
 apply: measure_semi_sigma_additive.
@@ -2272,7 +2272,7 @@ apply: measure_semi_sigma_additive.
 Qed.
 
 HB.instance Definition _ := isMeasure.Build _ _ _
-  (pushforward m mf) pushforward0 pushforward_ge0 pushforward_sigma_additive.
+  (pushforward m f) pushforward0 pushforward_ge0 pushforward_sigma_additive.
 
 End pushforward_measure.
 

theories/probability.v

@@ -105,7 +105,7 @@ Proof. by rewrite preimage_range probability_setT. Qed.
 
 Definition distribution d d' (T : measurableType d) (T' : measurableType d')
     (R : realType) (P : probability T R) (X : {mfun T >-> T'}) :=
-  pushforward P (@measurable_funP _ _ _ _ _ X).
+  pushforward P X.
 
 Section distribution_is_probability.
 Context d d' {T : measurableType d} {T' : measurableType d'} {R : realType}