nitpick

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -53,7 +53,10 @@
   + lemma `nicely_shrinking_fin_num`
 
 - in `probability.v`:
-  + lemmas `measurable_idTR`, `cdf_lebesgue_stieltjes_id`
+  + lemma `cdf_lebesgue_stieltjes_id`
+
+- in `real_interval.v`:
+  + lemma `itvNybndEbigcup`
 
 ### Changed
 

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/probability.v

@@ -253,65 +253,47 @@ Let lsf := lebesgue_stieltjes_measure f.
 
 Let lebesgue_stieltjes_setT : lsf setT = 1%E.
 Proof.
-pose I n := `]-(n%:R):R, n%:R]%classic.
-have <- : \bigcup_n I n = setT.
-  rewrite -subTset=> x _; rewrite /bigcup/=; exists (truncn`|x|).+1=>//.
-  by rewrite /I/= subset_itv_oo_oc// in_itv/= -real_ltr_norml//= truncnS_gt.
-have cvg_cup : (lsf \o I) n @[n --> \oo] --> lsf (\bigcup_n I n).
+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))/f_y1].
+  - apply/cvg_EFin; [by near=> F|apply: (cvg_ninftyP _ _).1 => //].
+    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.
-have cvg_1 : (lsf \o I) n @[n --> \oo] --> 1%E.
-  rewrite /comp/I/lsf/lebesgue_stieltjes_measure/measure_extension/=.
-  suff : ((f n%:R)%:E - (f (1 *- n))%:E)%E @[n --> \oo] --> 1%E => ?.
-    under eq_cvg=> n.
-      rewrite measurable_mu_extE/=; last exact: is_ocitv.
-      rewrite wlength_itv_bnd; last exact: (le_trans _ (ler0n R n)).
-      over.
-    assumption.
-  rewrite -(sube0 1); apply: cvgeB=>//; apply: cvg_EFin; try by near=> F.
-    by rewrite /comp; apply/(cvg_comp _ _ (@cvgr_idn R))/f_y1.
-  rewrite /comp/=; apply: ((iffLR (cvg_ninftyP _ _)) f_Ny0).
-  by apply: (cvg_comp _ _ (@cvgr_idn R)); rewrite ninfty.
-by rewrite -(cvg_unique _ cvg_cup cvg_1).
+exact: cvg_unique.
 Unshelve. all: end_near. Qed.
 
 HB.instance Definition _ := @Measure_isProbability.Build _ _ _
   (lebesgue_stieltjes_measure f) lebesgue_stieltjes_setT.
 
-Let idTR : T -> R := (fun x => x).
-
-Lemma measurable_idTR : measurable_fun setT idTR.
-Proof. by apply: measurable_id. Qed.
+Let idTR : T -> R := idfun.
 
 #[local] HB.instance Definition _ :=
-  @isMeasurableFun.Build _ _ T R idTR measurable_idTR.
-
-Let Xid : {RV lsf >-> R} := idTR.
+  @isMeasurableFun.Build _ _ T R idTR (@measurable_id _ _ setT).
 
-Lemma cdf_lebesgue_stieltjes_id r : cdf Xid r = EFin (f r).
+Lemma cdf_lebesgue_stieltjes_id r : cdf (idTR : {RV lsf >-> R}) r = (f r)%:E.
 Proof.
-rewrite /= preimage_id.
-have <- : (\bigcup_n `]-n%:R, r]%classic) = `]-oo, r]%classic.
-  apply/seteqP; split=> x/=; first by case=> n _/=; rewrite !in_itv/=; case/andP.
-  rewrite in_itv/= => xr; exists (truncn`|x|).+1=>//=; rewrite in_itv/=.
-  apply/andP; split=>//; rewrite ltrNl -normrN.
-  apply: le_lt_trans; [exact: ler_norm | exact: truncnS_gt].
-have cvg_cup : (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//.
-have cvg_fr : (lsf `]-n%:R, r])@[n --> \oo] --> (f r)%:E.
-  suff : ((f r)%:E - (f (-n%:R))%:E)%E@[n --> \oo] --> (f r)%:E.
+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 /lsf /lebesgue_stieltjes_measure /measure_extension/=.
     rewrite measurable_mu_extE/= ?wlength_itv_bnd//; last exact: is_ocitv.
-    near: n; exists (truncn`|r|).+1=>// n/=; rewrite truncn_lt_nat// lerNl.
-    by move/ltW; apply /le_trans; rewrite -normrN ler_norm.
-  rewrite -[X in _ --> X](sube0 (f r)%:E).
-  apply: cvgeB=>//; first exact: cvg_cst.
-  apply: cvg_comp; [apply: cvg_comp; last exact: f_Ny0 | by[]].
-  by apply: cvg_comp; [exact: cvgr_idn | rewrite ninfty].
-by rewrite -(cvg_unique _ cvg_cup cvg_fr).
+    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 _ _ _ f_Ny0)) => //.
+  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.