Radon nikodym cscale (#1076)

* radon nikodym derivative scale and add

---------

Co-authored-by: Reynald Affeldt <[email protected]>

CHANGELOG_UNRELEASED.md

@@ -42,6 +42,13 @@
 - in `lebesgue_integral.v`:
   + `mfun` instances for `expR` and `comp`
 
+- in `charge.v`:
+  + lemmas `dominates_cscale`, `Radon_Nikodym_cscale`
+  + definition `cadd`, lemmas `dominates_caddl`, `Radon_Nikodym_cadd`
+
+- in `lebesgue_integral.v`:
+  + lemma `abse_integralP`
+
 ### Changed
 
 - in `hoelder.v`:
@@ -71,6 +78,8 @@
 
 - in `probability.v`:
   + `markov` now uses `Num.nneg`
+- in `lebesgue_integral.v`:
+  + order of arguments in the lemma `le_abse_integral`
 
 ### Renamed
 
@@ -114,6 +123,9 @@
 - in `topology.v`:
   + `ball_filter` generalized to `realDomainType`
 
+- in `lebesgue_integral.v`:
+  + weaken an hypothesis of `integral_ae_eq`
+
 ### Deprecated
 
 ### Removed

theories/charge.v

@@ -370,6 +370,38 @@ HB.instance Definition _ := isCharge.Build _ _ _ cscale
 
 End charge_scale.
 
+Section charge_add.
+Local Open Scope ereal_scope.
+Context d (T : measurableType d) (R : realType).
+Variables (m1 m2 : {charge set T -> \bar R}).
+
+Definition cadd := m1 \+ m2.
+
+Let cadd0 : cadd set0 = 0.
+Proof. by rewrite /cadd 2!charge0 adde0. Qed.
+
+Let cadd_finite A : measurable A -> cadd A \is a fin_num.
+Proof. by move=> mA; rewrite fin_numD !fin_num_measure. Qed.
+
+Let cadd_sigma_additive : semi_sigma_additive cadd.
+Proof.
+move=> F mF tF mUF; rewrite /cadd.
+under eq_fun do rewrite big_split; apply: cvg_trans.
+  (* TODO: IIRC explicit arguments were added to please Coq 8.14, rm if not needed anymore *)
+  apply: (@cvgeD _ _ _ R (fun x => \sum_(0 <= i < x) (m1 (F i)))
+                         (fun x => \sum_(0 <= i < x) (m2 (F i)))
+                         (m1 (\bigcup_n F n)) (m2 (\bigcup_n F n))).
+  - by rewrite fin_num_adde_defr// fin_num_measure.
+  - exact: charge_semi_sigma_additive.
+  - exact: charge_semi_sigma_additive.
+exact: cvg_id.
+Qed.
+
+HB.instance Definition _ := isCharge.Build _ _ _ cadd
+  cadd0 cadd_finite cadd_sigma_additive.
+
+End charge_add.
+
 Section positive_negative_set.
 Context d (T : semiRingOfSetsType d) (R : numDomainType).
 Implicit Types nu : set T -> \bar R.
@@ -1548,3 +1580,54 @@ Qed.
 
 End radon_nikodym.
 Notation "'d nu '/d mu" := (Radon_Nikodym mu nu) : charge_scope.
+
+Section radon_nikodym_lemmas.
+
+Lemma dominates_cscale d (T : measurableType d) (R : realType)
+  (mu : {sigma_finite_measure set T -> \bar R})
+  (nu : {charge set T -> \bar R})
+  (c : R) : nu `<< mu -> cscale c nu `<< mu.
+Proof. by move=> numu E mE /numu; rewrite /cscale => ->//; rewrite mule0. Qed.
+
+Lemma Radon_Nikodym_cscale d (T : measurableType d) (R : realType)
+  (mu : {sigma_finite_measure set T -> \bar R})
+  (nu : {charge set T -> \bar R}) (c : R) :
+  nu `<< mu ->
+  ae_eq mu [set: T] ('d [the charge _ _ of cscale c nu] '/d mu)
+                    (fun x => c%:E * 'd nu '/d mu x).
+Proof.
+move=> numu; apply: integral_ae_eq => [//| | |E mE].
+- by apply: Radon_Nikodym_integrable; exact: dominates_cscale.
+  apply: emeasurable_funM => //.
+  exact: measurable_int (Radon_Nikodym_integrable _).
+- rewrite integralZl//; last first.
+    by apply: (integrableS measurableT) => //; exact: Radon_Nikodym_integrable.
+  rewrite -Radon_Nikodym_integral => //; last exact: dominates_cscale.
+  by rewrite -Radon_Nikodym_integral.
+Qed.
+
+Lemma dominates_caddl d (T : measurableType d)
+  (R : realType) (mu : {sigma_finite_measure set T -> \bar R})
+  (nu0 nu1 : {charge set T -> \bar R}) :
+  nu0 `<< mu -> nu1 `<< mu ->
+  cadd nu0 nu1 `<< mu.
+Proof.
+by move=> nu0mu nu1mu A mA A0; rewrite /cadd nu0mu// nu1mu// adde0.
+Qed.
+
+Lemma Radon_Nikodym_cadd d (T : measurableType d) (R : realType)
+    (mu : {sigma_finite_measure set T -> \bar R})
+    (nu0 nu1 : {charge set T -> \bar R}) :
+  nu0 `<< mu -> nu1 `<< mu ->
+  ae_eq mu [set: T] ('d [the charge _ _ of cadd nu0 nu1] '/d mu)
+                    ('d nu0 '/d mu \+ 'd nu1 '/d mu).
+Proof.
+move=> nu0mu nu1mu; apply: integral_ae_eq => [//| | |E mE].
+- by apply: Radon_Nikodym_integrable => /=; exact: dominates_caddl.
+  by apply: emeasurable_funD; exact: measurable_int (Radon_Nikodym_integrable _).
+- rewrite integralD => //; [|exact: integrableS (Radon_Nikodym_integrable _)..].
+  rewrite -Radon_Nikodym_integral //=; last exact: dominates_caddl.
+  by rewrite -Radon_Nikodym_integral // -Radon_Nikodym_integral.
+Qed.
+
+End radon_nikodym_lemmas.

theories/lebesgue_integral.v

@@ -3382,7 +3382,7 @@ move=> if1 if2; rewrite (integralD_EFin mD if1); last first.
 by rewrite -integralN//; exact: integrable_add_def.
 Qed.
 
-Lemma le_abse_integral d (R : realType) (T : measurableType d)
+Lemma le_abse_integral d (T : measurableType d) (R : realType)
   (mu : {measure set T -> \bar R}) (D : set T) (f : T -> \bar R)
   (mD : measurable D) : measurable_fun D f ->
   (`| \int[mu]_(x in D) (f x) | <= \int[mu]_(x in D) `|f x|)%E.
@@ -3395,6 +3395,19 @@ by rewrite -ge0_integralD // -?fune_abse//;
   [exact: measurable_funepos | exact: measurable_funeneg].
 Qed.
 
+Lemma abse_integralP d (T : measurableType d) (R : realType)
+    (mu : {measure set T -> \bar R}) (D : set T) (f : T -> \bar R) :
+    measurable D -> measurable_fun D f ->
+  (`| \int[mu]_(x in D) f x | < +oo <-> \int[mu]_(x in D) `|f x| < +oo)%E.
+Proof.
+move=> mD mf; split => [|] foo; last first.
+  exact: (le_lt_trans (le_abse_integral mu mD mf) foo).
+under eq_integral do rewrite -/((abse \o f) _) fune_abse.
+rewrite ge0_integralD//;[|exact/measurable_funepos|exact/measurable_funeneg].
+move: foo; rewrite integralE/= -fin_num_abs fin_numB => /andP[fpoo fnoo].
+by rewrite lte_add_pinfty// ltey_eq ?fpoo ?fnoo.
+Qed.
+
 Section integral_indic.
 Local Open Scope ereal_scope.
 Context d (T : measurableType d) (R : realType)
@@ -4348,13 +4361,13 @@ by move/cvg_lim => h2; rewrite setI_bigcupr -h2// h1.
 Qed.
 
 Lemma integral_ae_eq (D : set T) (mD : measurable D) (g f : T -> \bar R) :
-  mu.-integrable D f -> mu.-integrable D g ->
+  mu.-integrable D f -> measurable_fun D g ->
   (forall E, measurable E -> \int[mu]_(x in E) f x = \int[mu]_(x in E) g x) ->
   ae_eq mu D f g.
 Proof.
-move=> mf mg fg.
-have msf := measurable_int mf.
-have msg := measurable_int mg.
+move=> fi mg fg; have mf := measurable_int fi; have gi : mu.-integrable D g.
+  apply/integrableP; split => //; apply/abse_integralP => //; rewrite -fg//.
+  by apply/abse_integralP => //; case/integrableP : fi.
 have mugf : mu (D `&` [set x | g x < f x]) = 0 by exact: integral_measure_lt.
 have mufg : mu (D `&` [set x | f x < g x]) = 0.
   by apply: integral_measure_lt => // E mE; rewrite fg.
@@ -4365,8 +4378,8 @@ apply/negligibleP.
   by rewrite h; apply: emeasurable_fun_neq.
 rewrite h set_neq_lt setIUr measureU//.
 - by rewrite [X in X + _]mufg add0e [LHS]mugf.
-- by apply: emeasurable_fun_lt.
-- by apply: emeasurable_fun_lt.
+- exact: emeasurable_fun_lt.
+- exact: emeasurable_fun_lt.
 - apply/seteqP; split => [x [[Dx/= + [_]]]|//].
   by move=> /lt_trans => /[apply]; rewrite ltxx.
 Qed.