add a definition of RN derivative (tentative)

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -67,16 +67,18 @@
 - in `classical_sets.v`:
   + lemmas `preimage_mem_true`, `preimage_mem_false`
 - in `measure.v`:
-  + definition `dominates`, notation `` `<< ``
-  + lemma `dominates_trans`
+  + definition `measure_dominates`, notation `` `<< ``
+  + lemma `measure_dominates_trans`
 - in `measure.v`:
   + defintion `mfrestr`
 - in `charge.v`:
   + definition `measure_of_charge`
   + definition `crestr0`
   + definitions `jordan_neg`, `jordan_pos`
   + lemmas `jordan_decomp`, `jordan_pos_dominates`, `jordan_neg_dominates`
+  + definition `radon_nikodym_derivative`, notation `_.-derivative _`
   + lemma `radon_nikodym_finite`, theorem `Radon_Nikodym`
+  + lemma `integrable_radon_nikodym_derivative`
 
 - in `measure.v`:
   + lemmas `measurable_pair1`, `measurable_pair2`

theories/charge.v

@@ -39,6 +39,8 @@ Require Import esum measure realfun lebesgue_measure lebesgue_integral.
 (*        jordan_neg nu nuPN == the charge obtained by restricting the charge *)
 (*                              nu to the positive set N of the Hahn          *)
 (*                              decomposition nuPN: hahn_decomposition nu P N *)
+(*         mu.-derivative nu == Radon-Nikodym derivative of nu w.r.t. mu if   *)
+(*                              mu dominates nu, cst -oo otherwise            *)
 (*                                                                            *)
 (******************************************************************************)
 
@@ -48,6 +50,7 @@ Reserved Notation "{ 'additive_charge' 'set' T '->' '\bar' R }"
 Reserved Notation "{ 'charge' 'set' T '->' '\bar' R }"
   (at level 36, T, R at next level,
     format "{ 'charge'  'set'  T  '->'  '\bar'  R }").
+Reserved Notation "mu .-derivative" (at level 2, format "mu .-derivative").
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -364,10 +367,10 @@ Context d (R : numDomainType) (T : measurableType d).
 Implicit Types nu : set T -> \bar R.
 
 Definition positive_set nu (P : set T) :=
-  measurable P /\ forall E, measurable E -> E `<=` P -> nu E >= 0.
+  measurable P /\ forall A, measurable A -> A `<=` P -> nu A >= 0.
 
 Definition negative_set nu (N : set T) :=
-  measurable N /\ forall E, measurable E -> E `<=` N -> nu E <= 0.
+  measurable N /\ forall A, measurable A -> A `<=` N -> nu A <= 0.
 
 End positive_negative_set.
 
@@ -863,7 +866,7 @@ Variables mu nu : {measure set T -> \bar R}.
 
 Definition approxRN := [set g : T -> \bar R | [/\
   forall x, 0 <= g x, mu.-integrable [set: T] g &
-  forall E, measurable E -> \int[mu]_(x in E) g x <= nu E] ].
+  forall A, measurable A -> \int[mu]_(x in A) g x <= nu A] ].
 
 Let approxRN_neq0 : approxRN !=set0.
 Proof.
@@ -1316,7 +1319,7 @@ Let f_ge0 := fRN_ge0.
 
 Lemma radon_nikodym_finite : nu `<< mu -> exists f : T -> \bar R,
   [/\ forall x, f x >= 0, mu.-integrable [set: T] f &
-      forall E, measurable E -> nu E = \int[mu]_(x in E) f x].
+      forall A, measurable A -> nu A = \int[mu]_(x in A) f x].
 Proof.
 move=> nu_mu; exists f; split.
   - by move=> x; exact: f_ge0.
@@ -1330,11 +1333,11 @@ pose AP := A `&` P.
 have mAP : measurable AP by exact: measurableI.
 have muAP_gt0 : 0 < mu AP.
   rewrite lt_neqAle measure_ge0// andbT eq_sym.
-  apply/eqP/(@contra_not _ _ (nu_mu _ mAP))/eqP; rewrite gt_eqF //.
+  apply/eqP/(@contra_not _ _ (nu_mu _ mAP))/eqP; rewrite gt_eqF//.
   rewrite (@lt_le_trans _ _ (sigma AP))//.
     rewrite (@lt_le_trans _ _ (sigma A))//; last first.
-      rewrite (charge_partition _ _ mP mN)// gee_addl//.
-      by apply: negN => //; exact: measurableI.
+      rewrite (charge_partition _ _ mP mN)// gee_addl// negN//.
+      exact: measurableI.
     by rewrite sube_gt0// (proj2_sig (epsRN_ex mA abs)).
   rewrite /sigma/= /sigmaRN lee_subel_addl ?fin_num_measure//.
   by rewrite lee_paddl// integral_ge0// => x _; rewrite adde_ge0//; exact: f_ge0.
@@ -1365,10 +1368,9 @@ have hnu S : measurable S -> \int[mu]_(x in S) h x <= nu S.
   rewrite -(setD0 S) -(setDv AP) setDDr.
   have mSIAP : measurable (S `&` AP) by exact: measurableI.
   have mSDAP : measurable (S `\` AP) by exact: measurableD.
-  rewrite integral_setU //.
-  - rewrite measureU//.
-      by apply: lee_add; [exact: hnuN|exact: hnuP].
-    by rewrite setDE setIACA setICl setI0.
+  rewrite integral_setU//.
+  - rewrite measureU//; last by by rewrite setDE setIACA setICl setI0.
+    by apply: lee_add; [exact: hnuN|exact: hnuP].
   - exact: measurable_funTS.
   - by rewrite disj_set2E setDE setIACA setICl setI0.
 have int_h_M : \int[mu]_x h x > M.
@@ -1496,24 +1498,45 @@ rewrite -measure_bigcup//.
 - exact: trivIset_setIl.
 Qed.
 
+Definition radon_nikodym_derivative
+    (mu : {sigma_finite_measure set T -> \bar R})
+    (nu : {charge set T -> \bar R}) : T -> \bar R :=
+  let PN := svalP (cid (svalP (cid (Hahn_decomposition nu)))) in
+  if pselect (nu `<< mu) is left numu then
+    let fp :=
+      sval (cid2 (radon_nikodym_sigma_finite (jordan_pos_dominates PN numu))) in
+    let fn :=
+      sval (cid2 (radon_nikodym_sigma_finite (jordan_neg_dominates PN numu))) in
+    fp \- fn
+  else cst -oo.
+
+Notation "mu .-derivative" := (radon_nikodym_derivative mu) : type_scope.
+
+Lemma integrable_radon_nikodym_derivative
+    (mu : {sigma_finite_measure set T -> \bar R})
+    (nu : {charge set T -> \bar R}) :
+  nu `<< mu -> mu.-integrable [set: T] (mu.-derivative nu).
+Proof.
+move=> h; rewrite /radon_nikodym_derivative; case: pselect => //= h'.
+by apply: integrableB => //; case: cid2.
+Qed.
+
 Theorem Radon_Nikodym
-  (mu : {sigma_finite_measure set T -> \bar R}) (nu : {charge set T -> \bar R}) :
-  nu `<< mu ->
-  exists2 f : T -> \bar R, mu.-integrable [set: T] f &
-    forall E, measurable E -> nu E = \int[mu]_(x in E) f x.
+    (mu : {sigma_finite_measure set T -> \bar R})
+    (nu : {charge set T -> \bar R}) : nu `<< mu ->
+  forall A, measurable A -> nu A = \int[mu]_(x in A) (mu.-derivative nu) x.
 Proof.
-move=> nu_mu; have [P [N nuPN]] := Hahn_decomposition nu.
-have [fp intfp fpE] := @radon_nikodym_sigma_finite mu
-  [the {finite_measure set _ -> \bar _} of jordan_pos nuPN]
-  (jordan_pos_dominates nuPN nu_mu).
-have [fn intfn fnE] := @radon_nikodym_sigma_finite mu
-  [the {finite_measure set _ -> \bar _} of jordan_neg nuPN]
-  (jordan_neg_dominates nuPN nu_mu).
-exists (fp \- fn); first exact: integrableB.
-move=> E mE; rewrite [LHS](jordan_decomp nuPN mE)// integralB//.
-- by rewrite -fpE ?inE// -fnE ?inE.
-- exact: (integrableS measurableT).
-- exact: (integrableS measurableT).
+set PN := svalP (cid (svalP (cid (Hahn_decomposition nu)))).
+move=> h A mA.
+rewrite /radon_nikodym_derivative; case: pselect => // h'.
+rewrite [LHS](jordan_decomp PN mA)// integralB//.
+- set fpE :=
+    (svalP (cid2 (radon_nikodym_sigma_finite (jordan_pos_dominates PN h')))).2.
+  set fnE :=
+    (svalP (cid2 (radon_nikodym_sigma_finite (jordan_neg_dominates PN h')))).2.
+  by rewrite -fpE ?inE// -fnE ?inE.
+- by apply: (integrableS measurableT) => //; case: cid2.
+- by apply: (integrableS measurableT) => //; case: cid2.
 Qed.
 
 End radon_nikodym.

theories/measure.v

@@ -4216,13 +4216,13 @@ Section absolute_continuity.
 Context d (T : measurableType d) (R : realType).
 Implicit Types m : set T -> \bar R.
 
-Definition dominates m1 m2 :=
+Definition measure_dominates m1 m2 :=
   forall A, measurable A -> m2 A = 0 -> m1 A = 0.
 
-Local Notation "m1 `<< m2" := (dominates m1 m2).
+Local Notation "m1 `<< m2" := (measure_dominates m1 m2).
 
-Lemma dominates_trans m1 m2 m3 : m1 `<< m2 -> m2 `<< m3 -> m1 `<< m3.
+Lemma measure_dominates_trans m1 m2 m3 : m1 `<< m2 -> m2 `<< m3 -> m1 `<< m3.
 Proof. by move=> m12 m23 A mA /m23-/(_ mA) /m12; exact. Qed.
 
 End absolute_continuity.
-Notation "m1 `<< m2" := (dominates m1 m2).
+Notation "m1 `<< m2" := (measure_dominates m1 m2).