Add section: Lebesgue-Stieltjes measure of cdf (#1689)

* add lemma lebesgue_stieltjes_cdf_id

* more systematic use of measurableTypeR

---------

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

Author: Yosuke-Ito-345

CHANGELOG_UNRELEASED.md

@@ -7,6 +7,9 @@
 - in `constructive_ereal.v`:
   + lemma `ltgte_fin_num`
 
+- in `probability.v`:
+  + lemmas `cdf_fin_num`, `lebesgue_stieltjes_cdf_id`
+
 - in `num_normedtype.v`:
   + lemma `nbhs_infty_gtr`
 

theories/ftc.v

@@ -348,7 +348,7 @@ Proof. by move=> xu locf F ax fx; exact: (@continuous_FTC1 _ _ _ u). Qed.
 End FTC.
 
 Definition parameterized_integral {R : realType}
-    (mu : {measure set (g_sigma_algebraType (R.-ocitv.-measurable)) -> \bar R})
+    (mu : {measure set (measurableTypeR R) -> \bar R})
     a x (f : R -> R) : R :=
   (\int[mu]_(t in `[a, x]) f t)%R.
 

theories/lebesgue_measure.v

@@ -335,7 +335,7 @@ End hlength_extension.
 End LebesgueMeasure.
 
 Definition lebesgue_measure {R : realType} :
-  set (g_sigma_algebraType R.-ocitv.-measurable) -> \bar R :=
+  set (measurableTypeR R) -> \bar R :=
   lebesgue_stieltjes_measure idfun.
 HB.instance Definition _ (R : realType) := Measure.on (@lebesgue_measure R).
 HB.instance Definition _ (R : realType) :=
@@ -399,7 +399,7 @@ have mF_ m : mu (F_ m) < completed_mu E + m.+1%:R^-1%:E.
   apply: lee_nneseries => // n _.
   by rewrite -((measurable_mu_extE hlength) (A m n))//; have [/(_ n)] := mA m.
 pose F := \bigcap_n (F_ n).
-have FM : @measurable _ (g_sigma_algebraType R.-ocitv.-measurable) F.
+have FM : @measurable _ (measurableTypeR R) F.
   apply: bigcapT_measurable => k; apply: bigcupT_measurable => i.
   by apply: sub_sigma_algebra; have [/(_ i)] := mA k.
 have EF : E `<=` F by exact: sub_bigcap.
@@ -434,7 +434,7 @@ have mG_ m : mu (G_ m) < completed_mu (F `\` E) + m.+1%:R^-1%:E.
   apply: lee_nneseries => // n _.
   by rewrite -((measurable_mu_extE hlength) (B m n))//; have [/(_ n)] := mB m.
 pose G := \bigcap_n (G_ n).
-have GM : @measurable _ (g_sigma_algebraType R.-ocitv.-measurable) G.
+have GM : @measurable _ (measurableTypeR R) G.
   apply: bigcapT_measurable => k; apply: bigcupT_measurable => i.
   by apply: sub_sigma_algebra; have [/(_ i)] := mB k.
 have FEG : F `\` E `<=` G by exact: sub_bigcap.

theories/lebesgue_stieltjes_measure.v

@@ -510,12 +510,14 @@ Arguments lebesgue_stieltjes_measure {R}.
 #[deprecated(since="mathcomp-analysis 1.1.0", note="renamed `wlength_sigma_subadditive`")]
 Notation wlength_sigma_sub_additive := wlength_sigma_subadditive (only parsing).
 
+Definition measurableTypeR (R : realType) :=
+  g_sigma_algebraType R.-ocitv.-measurable.
+
 Section lebesgue_stieltjes_measure.
 Variable R : realType.
-Let gitvs : measurableType _ := g_sigma_algebraType (@ocitv R).
 
 Lemma lebesgue_stieltjes_measure_unique (f : cumulative R R)
-    (mu : {measure set gitvs -> \bar R}) :
+    (mu : {measure set (measurableTypeR R) -> \bar R}) :
     (forall X, ocitv X -> lebesgue_stieltjes_measure f X = mu X) ->
   forall X, measurable X -> lebesgue_stieltjes_measure f X = mu X.
 Proof.
@@ -550,14 +552,13 @@ 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
+  @isMeasurable.Build _ (measurableTypeR R) measurableR
     measurable0 (@measurableC _ _) (@bigcupT_measurable _ _).
 (*HB.instance (Real.sort R) R_isMeasurable.*)
 
@@ -631,7 +632,6 @@ 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.

theories/probability.v

@@ -169,6 +169,11 @@ Lemma cdf_ge0 r : 0 <= cdf X r. Proof. by []. Qed.
 
 Lemma cdf_le1 r : cdf X r <= 1. Proof. exact: probability_le1. Qed.
 
+Lemma cdf_fin_num r : cdf X r \is a fin_num.
+Proof.
+by rewrite ge0_fin_numE ?cdf_ge0//; exact/(le_lt_trans (cdf_le1 r))/ltry.
+Qed.
+
 Lemma cdf_nondecreasing : nondecreasing_fun (cdf X).
 Proof. by move=> r s rs; rewrite le_measure ?inE//; exact: subitvPr. Qed.
 
@@ -252,17 +257,16 @@ HB.instance Definition _ := isCumulative.Build R _ (\bar R) (cdf X)
 
 End cumulative_distribution_function.
 
-Section cdf_of_lebesgue_stieltjes_mesure.
+Section cdf_of_lebesgue_stieltjes_measure.
 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.
+Let idTR : measurableTypeR R -> R := idfun.
 
 #[local] HB.instance Definition _ :=
-  @isMeasurableFun.Build _ _ T R idTR (@measurable_id _ _ setT).
+  @isMeasurableFun.Build _ _ _ _ idTR (@measurable_id _ _ setT).
+
+Let lsf := lebesgue_stieltjes_measure f.
 
 Lemma cdf_lebesgue_stieltjes_id r : cdf (idTR : {RV lsf >-> R}) r = (f r)%:E.
 Proof.
@@ -277,12 +281,65 @@ have : lsf `]-n%:R, r] @[n --> \oo] --> (f r)%:E.
   apply: (cvg_comp _ _ (cvg_comp _ _ _ (cumulativeNy 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.
+  apply: nondecreasing_cvg_mu => //; 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.
+End cdf_of_lebesgue_stieltjes_measure.
+
+Section lebesgue_stieltjes_measure_of_cdf.
+Context {R : realType} (P : probability (measurableTypeR R) R).
+Local Open Scope measure_display_scope.
+
+Let idTR : measurableTypeR R -> R := idfun.
+
+#[local] HB.instance Definition _ :=
+  @isMeasurableFun.Build _ _ _ _ idTR (@measurable_id _ _ setT).
+
+Let fcdf r := fine (cdf (idTR : {RV P >-> R}) r).
+
+Let fcdf_nd : nondecreasing fcdf.
+Proof.
+by move=> *; apply: fine_le; [exact: cdf_fin_num.. | exact: cdf_nondecreasing].
+Qed.
+
+Let fcdf_rc : right_continuous fcdf.
+Proof.
+move=> a; apply: fine_cvg.
+by rewrite fineK; [exact: cdf_right_continuous | exact: cdf_fin_num].
+Qed.
+
+#[local] HB.instance Definition _ :=
+  isCumulative.Build R _ R fcdf fcdf_nd fcdf_rc.
+
+Let fcdf_Ny0 : fcdf @ -oo --> (0:R).
+Proof. exact/fine_cvg/cvg_cdfNy0. Qed.
+
+Let fcdf_y1 : fcdf @ +oo --> (1:R).
+Proof. exact/fine_cvg/cvg_cdfy1. Qed.
+
+#[local] HB.instance Definition _ :=
+  isCumulativeBounded.Build R 0 1 fcdf fcdf_Ny0 fcdf_y1.
+
+Let lscdf := lebesgue_stieltjes_measure fcdf.
+
+Lemma lebesgue_stieltjes_cdf_id (A : set _) (mA : measurable A) : lscdf A = P A.
+Proof.
+apply: lebesgue_stieltjes_measure_unique => [I [[a b]]/= _ <- | //].
+rewrite /lebesgue_stieltjes_measure /measure_extension/=.
+rewrite measurable_mu_extE/=; last exact: is_ocitv.
+have [ab | ba] := leP a b; last first.
+  by rewrite set_itv_ge ?wlength0 ?measure0// bnd_simp -leNgt ltW.
+rewrite wlength_itv_bnd// EFinB !fineK ?cdf_fin_num//.
+rewrite /cdf /distribution /pushforward !preimage_id.
+have : `]a, b]%classic = `]-oo, b] `\` `]-oo, a] => [|->].
+  by rewrite -[RHS]setCK setCD setCitvl setUC -[LHS]setCK setCitv.
+rewrite measureD ?setIidr//; first exact: subset_itvl.
+by rewrite -ge0_fin_numE// fin_num_measure.
+Qed.
+
+End lebesgue_stieltjes_measure_of_cdf.
 
 HB.lock Definition expectation {d} {T : measurableType d} {R : realType}
   (P : probability T R) (X : T -> R) := (\int[P]_w (X w)%:E)%E.