addressing comments by Quentin (almost done)

Co-authored-by: Tragicus <[email protected]>

theories/charge.v

@@ -37,9 +37,6 @@ Require Import esum measure realfun lebesgue_measure lebesgue_integral.
 (*               cscale r nu == charge nu scaled by a factor r : R            *)
 (*          charge_add n1 n2 == the charge corresponding to the sum of        *)
 (*                              charges n1 and n2                             *)
-(*        cpushforward nu mf == pushforward charge of nu along                *)
-(*                              measurable function f, mf is a proof that     *)
-(*                              f is measurable function                      *)
 (* charge_of_finite_measure mu == charge corresponding to a finite measure mu *)
 (*                                                                            *)
 (* * Theory                                                                   *)
@@ -450,31 +447,29 @@ Local Open Scope ereal_scope.
 Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (f : T1 -> T2).
 Variables (R : realFieldType) (nu : {charge set T1 -> \bar R}).
 
-Definition cpushforward (mf : measurable_fun setT f) A := nu (f @^-1` A).
-
 Hypothesis mf : measurable_fun setT f.
 
-Let cpushforward0 : cpushforward mf set0 = 0.
-Proof. by rewrite /cpushforward preimage_set0 charge0. Qed.
+Let pushforward0 : pushforward nu mf set0 = 0.
+Proof. by rewrite /pushforward preimage_set0 charge0. Qed.
 
-Let cpushforward_finite A : measurable A -> cpushforward mf A \is a fin_num.
+Let pushforward_finite A : measurable A -> pushforward nu mf A \is a fin_num.
 Proof.
 move=> mA; apply: fin_num_measure.
 by rewrite -[X in measurable X]setTI; exact: mf.
 Qed.
 
-Let cpushforward_sigma_additive : semi_sigma_additive (cpushforward mf).
+Let pushforward_sigma_additive : semi_sigma_additive (pushforward nu mf).
 Proof.
-move=> F mF tF mUF; rewrite /cpushforward preimage_bigcup.
+move=> F mF tF mUF; rewrite /pushforward preimage_bigcup.
 apply: charge_semi_sigma_additive.
 - by move=> n; rewrite -[X in measurable X]setTI; exact: mf.
 - apply/trivIsetP => /= i j _ _ ij; rewrite -preimage_setI.
   by move/trivIsetP : tF => /(_ _ _ _ _ ij) ->//; rewrite preimage_set0.
 - by rewrite -preimage_bigcup -[X in measurable X]setTI; exact: mf.
 Qed.
 
-HB.instance Definition _ := isCharge.Build _ _ _ (cpushforward mf)
-  cpushforward0 cpushforward_finite cpushforward_sigma_additive.
+HB.instance Definition _ := isCharge.Build _ _ _ (pushforward nu mf)
+  pushforward0 pushforward_finite pushforward_sigma_additive.
 
 End pushforward_charge.
 
@@ -495,7 +490,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 -> cpushforward nu mf `<< pushforward mu mf.
+  nu `<< mu -> pushforward nu mf `<< pushforward mu mf.
 Proof.
 by move=> numu A mA; apply: numu; rewrite -[X in measurable X]setTI; exact: mf.
 Qed.
@@ -1900,8 +1895,8 @@ Lemma Radon_Nikodym_cscale mu nu c E : measurable E -> nu `<< mu ->
 Proof.
 move=> mE numu; apply: integral_ae_eq => [//| | |A AE mA].
 - apply: (integrableS measurableT) => //.
-  by apply: Radon_Nikodym_integrable => /=; exact: dominates_cscale.
-- by apply: measurable_funTS; exact: emeasurable_funM.
+  exact/Radon_Nikodym_integrable/dominates_cscale.
+- exact/measurable_funTS/emeasurable_funM.
 - rewrite integralZl//; last first.
     by apply: (integrableS measurableT) => //; exact: Radon_Nikodym_integrable.
   rewrite -Radon_Nikodym_integral => //; last exact: dominates_cscale.
@@ -1932,7 +1927,8 @@ Variables (nu : {charge set T -> \bar R})
 
 Lemma Radon_Nikodym_chain_rule : nu `<< mu -> mu `<< la ->
   ae_eq la setT ('d nu '/d la)
-                ('d nu '/d mu \* 'd [the charge _ _ of charge_of_finite_measure mu] '/d la).
+                ('d nu '/d mu \*
+                  'd [the charge _ _ of charge_of_finite_measure mu] '/d la).
 Proof.
 have [Pnu [Nnu nuPN]] := Hahn_decomposition nu.
 move=> numu mula; have nula := measure_dominates_trans numu mula.

theories/constructive_ereal.v

@@ -594,7 +594,7 @@ Implicit Type (x : \bar R).
 
 Definition fin_num := [qualify a x : \bar R | (x != -oo) && (x != +oo)].
 Fact fin_num_key : pred_key fin_num. Proof. by []. Qed.
-Canonical fin_num_keyd := KeyedQualifier fin_num_key.
+(*Canonical fin_num_keyd := KeyedQualifier fin_num_key.*)
 
 Lemma fin_numE x : (x \is a fin_num) = (x != -oo) && (x != +oo).
 Proof. by []. Qed.

theories/measure.v

@@ -117,6 +117,7 @@ From HB Require Import structures.
 (* * Instances of measures                                                    *)
 (*  pushforward mf m == pushforward/image measure of m by f, where mf is a    *)
 (*                      proof that f is measurable                            *)
+(*                      m has type set T -> \bar R.                           *)
 (*              \d_a == Dirac measure                                         *)
 (*         msum mu n == the measure corresponding to the sum of the measures  *)
 (*                      mu_0, ..., mu_{n-1}                                   *)
@@ -1652,22 +1653,25 @@ Arguments measure_bigcup {d R T} _ _.
 #[global] Hint Extern 0 (sigma_additive _) =>
   solve [apply: measure_sigma_additive] : core.
 
+Definition pushforward d1 d2 (T1 : measurableType d1) (T2 : measurableType d2)
+  (R : realFieldType) (m : set T1 -> \bar R) (f : T1 -> T2)
+  of measurable_fun setT f := fun A => m (f @^-1` A).
+Arguments pushforward {d1 d2 T1 T2 R} m {f}.
+
 Section pushforward_measure.
 Local Open Scope ereal_scope.
-Context d d' (T1 : measurableType d) (T2 : measurableType d') (f : T1 -> T2).
-Variables (R : realFieldType) (m : {measure set T1 -> \bar R}).
-
-Definition pushforward (mf : measurable_fun setT f) A := m (f @^-1` A).
-
+Context d d' (T1 : measurableType d) (T2 : measurableType d')
+        (R : realFieldType).
+Variables (m : {measure set T1 -> \bar R}) (f : T1 -> T2).
 Hypothesis mf : measurable_fun setT f.
 
-Let pushforward0 : pushforward mf set0 = 0.
+Let pushforward0 : pushforward m mf set0 = 0.
 Proof. by rewrite /pushforward preimage_set0 measure0. Qed.
 
-Let pushforward_ge0 A : 0 <= pushforward mf A.
+Let pushforward_ge0 A : 0 <= pushforward m mf A.
 Proof. by apply: measure_ge0; rewrite -[X in measurable X]setIT; apply: mf. Qed.
 
-Let pushforward_sigma_additive : semi_sigma_additive (pushforward mf).
+Let pushforward_sigma_additive : semi_sigma_additive (pushforward m mf).
 Proof.
 move=> F mF tF mUF; rewrite /pushforward preimage_bigcup.
 apply: measure_semi_sigma_additive.
@@ -1678,7 +1682,7 @@ apply: measure_semi_sigma_additive.
 Qed.
 
 HB.instance Definition _ := isMeasure.Build _ _ _
-  (pushforward mf) pushforward0 pushforward_ge0 pushforward_sigma_additive.
+  (pushforward m mf) pushforward0 pushforward_ge0 pushforward_sigma_additive.
 
 End pushforward_measure.