Add section: cdf of lebesgue stieltjes measure (#1639)

* add section cdf_of_lebesgue_stieltjes_mesure

---------

Co-authored-by: Reynald Affeldt <reynald.affeldt@aist.go.jp>

Author: Yosuke-Ito-345

CHANGELOG_UNRELEASED.md

@@ -112,6 +112,14 @@
 
 - in `lebesgue_integral_definition.v`:
   + lemmas `le_measure_sintegral`, `ge0_le_measure_integral`
+- in `probability.v`:
+  + lemma `cdf_lebesgue_stieltjes_id`
+
+- in `real_interval.v`:
+  + lemma `itvNybndEbigcup`
+
+- in `lebesgue_stieltjes_measure.v`:
+  + mixin `isCumulativeBounded`, structure `CumulativeBounded` with type `cumulative_bounded`
 
 ### Changed
 
@@ -238,6 +246,9 @@
       `LspaceType` to `ae_eq_op`, `ae_eq_op_refl`, `ae_eq_op_sym`, `ae_eq_op_trans`, `aeEqMfun`
    * renamed lemma `LequivP` to `ae_eqP`
 
+- moved from `measurable_realfun.v` to `lebesgue_stieltjes_measure.v`:
+  + definitions `measurableTypeR`, `measurableR`
+  + lemmas `measurable_set1`, `measurable_itv`
 
 ### Renamed
 

reals/real_interval.v

@@ -167,6 +167,15 @@ rewrite in_itv /= andbT => xy; exists (trunc y).+1 => //=.
 by rewrite in_itv /= xy /= truncnS_gt.
 Qed.
 
+Lemma itvNybndEbigcup b x : [set` Interval -oo%O (BSide b x)] =
+  \bigcup_k [set` Interval (BRight (- k%:R)) (BSide b x)].
+Proof.
+rewrite predeqE => y; split=> /=; last first.
+  by move=> [n _]/=; rewrite in_itv => /andP[ny yx]; rewrite in_itv.
+rewrite in_itv /= => yx; exists (trunc `|y|).+1 => //=; rewrite in_itv/=.
+by rewrite yx /= andbT ltrNl (le_lt_trans (ler_norm _))// normrN truncnS_gt.
+Qed.
+
 Lemma itvoyEbigcup x :
   `]x, +oo[%classic = \bigcup_k `[x + k.+1%:R^-1, +oo[%classic.
 Proof.

theories/lebesgue_stieltjes_measure.v

@@ -36,6 +36,9 @@ From mathcomp Require Import realfun.
 (*                                 f is a cumulative function.                *)
 (* completed_lebesgue_stieltjes_measure f == the completed Lebesgue-Stieltjes *)
 (*                                 measure                                    *)
+(*     cumulative_bounded R l r == type of cumulative functions f such that   *)
+(*                                 f @ -oo --> l and f @ +oo --> r            *)
+(*                                 The HB class is CumulativeBounded.         *)
 (* ```                                                                        *)
 (*                                                                            *)
 (******************************************************************************)
@@ -541,3 +544,102 @@ HB.instance Definition _ (f : cumulative R) :=
 
 End completed_lebesgue_stieltjes_measure.
 Arguments completed_lebesgue_stieltjes_measure {R}.
+
+Section salgebra_R_ssets.
+Variable R : realType.
+
+Definition measurableTypeR := g_sigma_algebraType (R.-ocitv.-measurable).
+Definition measurableR : set (set R) :=
+  (R.-ocitv.-measurable).-sigma.-measurable.
+
+HB.instance Definition _ := Pointed.on R.
+HB.instance Definition R_isMeasurable :
+  isMeasurable default_measure_display R :=
+  @isMeasurable.Build _ measurableTypeR measurableR
+    measurable0 (@measurableC _ _) (@bigcupT_measurable _ _).
+(*HB.instance (Real.sort R) R_isMeasurable.*)
+
+Lemma measurable_set1 (r : R) : measurable [set r].
+Proof.
+rewrite set1_bigcap_oc; apply: bigcap_measurable => // k _.
+by apply: sub_sigma_algebra; exact/is_ocitv.
+Qed.
+#[local] Hint Resolve measurable_set1 : core.
+
+Lemma measurable_itv (i : interval R) : measurable [set` i].
+Proof.
+have moc (a b : R) : measurable `]a, b].
+  by apply: sub_sigma_algebra; apply: is_ocitv.
+have mopoo (x : R) : measurable `]x, +oo[.
+  by rewrite itv_bndy_bigcup_BRight; exact: bigcup_measurable.
+have mnooc (x : R) : measurable `]-oo, x].
+  by rewrite -setCitvr; exact/measurableC.
+have ooE (a b : R) : `]a, b[%classic = `]a, b] `\ b.
+  case: (boolP (a < b)) => ab; last by rewrite !set_itv_ge ?set0D.
+  by rewrite -setUitv1// setUDK// => x [->]; rewrite /= in_itv/= ltxx andbF.
+have moo (a b : R) : measurable `]a, b[.
+  by rewrite ooE; exact: measurableD.
+have mcc (a b : R) : measurable `[a, b].
+  case: (boolP (a <= b)) => ab; last by rewrite set_itv_ge.
+  by rewrite -setU1itv//; apply/measurableU.
+have mco (a b : R) : measurable `[a, b[.
+  case: (boolP (a < b)) => ab; last by rewrite set_itv_ge.
+  by rewrite -setU1itv//; apply/measurableU.
+have oooE (b : R) : `]-oo, b[%classic = `]-oo, b] `\ b.
+  by rewrite -setUitv1// setUDK// => x [->]; rewrite /= in_itv/= ltxx.
+case: i => [[[] a|[]] [[] b|[]]] => //; do ?by rewrite set_itv_ge.
+- by rewrite -setU1itv//; exact/measurableU.
+- by rewrite oooE; exact/measurableD.
+- by rewrite set_itvNyy.
+Qed.
+#[local] Hint Resolve measurable_itv : core.
+
+End salgebra_R_ssets.
+#[global]
+Hint Extern 0 (measurable [set _]) => solve [apply: measurable_set1] : core.
+#[global]
+Hint Extern 0 (measurable [set` _] ) => exact: measurable_itv : core.
+
+HB.mixin Record isCumulativeBounded (R : numFieldType) (l r : R) (f : R -> R) := {
+  cumulativeNy0 : f @ -oo --> l ;
+  cumulativey1 : f @ +oo --> r }.
+
+#[short(type=cumulativeBounded)]
+HB.structure Definition CumulativeBounded (R : numFieldType) (l r : R) :=
+  { f of isCumulativeBounded R l r f & Cumulative R f}.
+
+Arguments cumulativeNy0 {R l r} s.
+Arguments cumulativey1 {R l r} s.
+
+Section probability_measure_of_lebesgue_stieltjes_mesure.
+Context {R : realType} (f : cumulativeBounded (0:R) (1:R)).
+Local Open Scope measure_display_scope.
+
+Let T := g_sigma_algebraType R.-ocitv.-measurable.
+Let lsf := lebesgue_stieltjes_measure f.
+
+Let lebesgue_stieltjes_setT : lsf setT = 1%E.
+Proof.
+rewrite -(bigcup_itvT false false).
+pose I n : set R := `]- (n%:R), n%:R]%classic.
+have : (lsf \o I) n @[n --> \oo] --> 1%E.
+  have -> : lsf \o I = (fun n => (f n%:R)%:E - (f (- n%:R))%:E)%E.
+    apply/funext=> n; rewrite /= /lsf/= /lebesgue_stieltjes_measure.
+    rewrite /measure_extension measurable_mu_extE/=; last exact: is_ocitv.
+    by rewrite wlength_itv_bnd// ge0_cp.
+  rewrite -(sube0 1); apply: cvgeB => //.
+  - by apply/cvg_EFin; [near=> F
+                       |exact/(cvg_comp _ _ (@cvgr_idn R))/cumulativey1].
+  - apply/cvg_EFin; [by near=> F|apply: (cvg_ninftyP _ _).1 => //].
+      exact: cumulativeNy0.
+    by apply: (cvg_comp _ _ (@cvgr_idn R)); rewrite ninfty.
+have : (lsf \o I) n @[n --> \oo] --> lsf (\bigcup_n I n).
+  apply: nondecreasing_cvg_mu; rewrite /I//; first exact: bigcup_measurable.
+  by move=> *; apply/subsetPset/subset_itv; rewrite leBSide/= ?lerN2 ler_nat.
+exact: cvg_unique.
+Unshelve. all: end_near. Qed.
+
+HB.instance Definition _ := @Measure_isProbability.Build _ _ _
+  (lebesgue_stieltjes_measure f) lebesgue_stieltjes_setT.
+
+End probability_measure_of_lebesgue_stieltjes_mesure.

theories/measurable_realfun.v

@@ -183,52 +183,6 @@ End puncture_ereal_itv.
 Section salgebra_R_ssets.
 Variable R : realType.
 
-Definition measurableTypeR := g_sigma_algebraType (R.-ocitv.-measurable).
-Definition measurableR : set (set R) :=
-  (R.-ocitv.-measurable).-sigma.-measurable.
-
-HB.instance Definition _ := Pointed.on R.
-HB.instance Definition R_isMeasurable :
-  isMeasurable default_measure_display R :=
-  @isMeasurable.Build _ measurableTypeR measurableR
-    measurable0 (@measurableC _ _) (@bigcupT_measurable _ _).
-(*HB.instance (Real.sort R) R_isMeasurable.*)
-
-Lemma measurable_set1 (r : R) : measurable [set r].
-Proof.
-rewrite set1_bigcap_oc; apply: bigcap_measurable => // k _.
-by apply: sub_sigma_algebra; exact/is_ocitv.
-Qed.
-#[local] Hint Resolve measurable_set1 : core.
-
-Lemma measurable_itv (i : interval R) : measurable [set` i].
-Proof.
-have moc (a b : R) : measurable `]a, b].
-  by apply: sub_sigma_algebra; apply: is_ocitv.
-have mopoo (x : R) : measurable `]x, +oo[.
-  by rewrite itv_bndy_bigcup_BRight; exact: bigcup_measurable.
-have mnooc (x : R) : measurable `]-oo, x].
-  by rewrite -setCitvr; exact/measurableC.
-have ooE (a b : R) : `]a, b[%classic = `]a, b] `\ b.
-  case: (boolP (a < b)) => ab; last by rewrite !set_itv_ge ?set0D.
-  by rewrite -setUitv1// setUDK// => x [->]; rewrite /= in_itv/= ltxx andbF.
-have moo (a b : R) : measurable `]a, b[.
-  by rewrite ooE; exact: measurableD.
-have mcc (a b : R) : measurable `[a, b].
-  case: (boolP (a <= b)) => ab; last by rewrite set_itv_ge.
-  by rewrite -setU1itv//; apply/measurableU.
-have mco (a b : R) : measurable `[a, b[.
-  case: (boolP (a < b)) => ab; last by rewrite set_itv_ge.
-  by rewrite -setU1itv//; apply/measurableU.
-have oooE (b : R) : `]-oo, b[%classic = `]-oo, b] `\ b.
-  by rewrite -setUitv1// setUDK// => x [->]; rewrite /= in_itv/= ltxx.
-case: i => [[[] a|[]] [[] b|[]]] => //; do ?by rewrite set_itv_ge.
-- by rewrite -setU1itv//; exact/measurableU.
-- by rewrite oooE; exact/measurableD.
-- by rewrite set_itvNyy.
-Qed.
-#[local] Hint Resolve measurable_itv : core.
-
 Lemma measurable_fun_itv_bndo_bndc (a : itv_bound R) (b : R)
     (f : R -> R) :
   measurable_fun [set` Interval a (BLeft b)] f ->
@@ -387,8 +341,7 @@ Qed.
 
 End salgebra_R_ssets.
 #[global]
-Hint Extern 0 (measurable [set _]) => solve [apply: measurable_set1|
-                                            apply: emeasurable_set1] : core.
+Hint Extern 0 (measurable [set _]) => solve [apply: emeasurable_set1] : core.
 #[global]
 Hint Extern 0 (measurable [set` _] ) => exact: measurable_itv : core.
 

theories/probability.v

@@ -247,6 +247,38 @@ Unshelve. all: by end_near. Qed.
 
 End cumulative_distribution_function.
 
+Section cdf_of_lebesgue_stieltjes_mesure.
+Context {R : realType} (f : cumulativeBounded (0:R) (1:R)).
+Local Open Scope measure_display_scope.
+
+Let T := g_sigma_algebraType R.-ocitv.-measurable.
+Let lsf := lebesgue_stieltjes_measure f.
+
+Let idTR : T -> R := idfun.
+
+#[local] HB.instance Definition _ :=
+  @isMeasurableFun.Build _ _ T R idTR (@measurable_id _ _ setT).
+
+Lemma cdf_lebesgue_stieltjes_id r : cdf (idTR : {RV lsf >-> R}) r = (f r)%:E.
+Proof.
+rewrite /= preimage_id itvNybndEbigcup.
+have : lsf `]-n%:R, r] @[n --> \oo] --> (f r)%:E.
+  suff : ((f r)%:E - (f (-n%:R))%:E)%E @[n --> \oo] --> (f r)%:E.
+    apply: cvg_trans; apply: near_eq_cvg; near=> n.
+    rewrite /lsf /lebesgue_stieltjes_measure /measure_extension/=.
+    rewrite measurable_mu_extE/= ?wlength_itv_bnd//; last exact: is_ocitv.
+    by rewrite lerNl; near: n; exact: nbhs_infty_ger.
+  rewrite -[X in _ --> X](sube0 (f r)%:E); apply: (cvgeB _ (cvg_cst _ )) => //.
+  apply: (cvg_comp _ _ (cvg_comp _ _ _ (cumulativeNy0 f))) => //.
+  by apply: (cvg_comp _ _ cvgr_idn); rewrite ninfty.
+have : lsf `]- n%:R, r] @[n --> \oo] --> lsf (\bigcup_n `]-n%:R, r]%classic).
+  apply: nondecreasing_cvg_mu; rewrite /I//; first exact: bigcup_measurable.
+  by move=> *; apply/subsetPset/subset_itv; rewrite leBSide//= lerN2 ler_nat.
+exact: cvg_unique.
+Unshelve. all: by end_near. Qed.
+
+End cdf_of_lebesgue_stieltjes_mesure.
+
 HB.lock Definition expectation {d} {T : measurableType d} {R : realType}
   (P : probability T R) (X : T -> R) := (\int[P]_w (X w)%:E)%E.
 Canonical expectation_unlockable := Unlockable expectation.unlock.