From 6151def442f1453aafb5d9689bc4d8fe155248dd Mon Sep 17 00:00:00 2001
From: Yosuke-Ito-345 <glacier345@gmail.com>
Date: Sat, 5 Jul 2025 20:44:55 +0900
Subject: [PATCH 01/13] changelog

---
 CHANGELOG_UNRELEASED.md | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index f74d42437..6b5518a9d 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -22,6 +22,11 @@
 
 ### Renamed
 
+- in `lebesgue_stieltjes_measure.v`:
+  + `cumulativeNy0` -> `cumulativeNy`
+  + `cumulativey1` -> `cumulativey`
+	+ `cumulativey1` -> `cumulativey`
+
 ### Generalized
 
 - in `lebesgue_stieltjes_measure.v` generalized (codomain is now an `orderNbhsType`):

From a83dc28c50cecb9b5bd7c32e40716699f3a9a9c4 Mon Sep 17 00:00:00 2001
From: Yosuke-Ito-345 <glacier345@gmail.com>
Date: Sun, 13 Jul 2025 14:07:48 +0900
Subject: [PATCH 02/13] Revert "generalize cumulative"

This reverts commit 558558ec2b062927f846362758867e3054a8dc48.

Reason: I mistakenly committed some unnecessary files.
---
 theories/topology_theory/num_topology.v | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/theories/topology_theory/num_topology.v b/theories/topology_theory/num_topology.v
index e265bb2ea..6cd611dc9 100644
--- a/theories/topology_theory/num_topology.v
+++ b/theories/topology_theory/num_topology.v
@@ -137,10 +137,6 @@ HB.instance Definition _ (R : numFieldType) := PseudoPointedMetric.copy R R^o.
 HB.instance Definition _ (R : realFieldType) :=
   Order_isNbhs.Build _ R (@real_order_nbhsE R).
 
-#[export, non_forgetful_inheritance]
-HB.instance Definition _ (R : realType) :=
-  Order_isNbhs.Build _ R (@real_order_nbhsE R).
-
 Module Exports. HB.reexport. End Exports.
 
 End numFieldTopology.

From 5d5b7633aed304a7e2e2501ff45e424e7f88d49b Mon Sep 17 00:00:00 2001
From: Yosuke-Ito-345 <glacier345@gmail.com>
Date: Sun, 13 Jul 2025 14:36:22 +0900
Subject: [PATCH 03/13] generalize cumulative

---
 theories/topology_theory/num_topology.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/theories/topology_theory/num_topology.v b/theories/topology_theory/num_topology.v
index 6cd611dc9..e265bb2ea 100644
--- a/theories/topology_theory/num_topology.v
+++ b/theories/topology_theory/num_topology.v
@@ -137,6 +137,10 @@ HB.instance Definition _ (R : numFieldType) := PseudoPointedMetric.copy R R^o.
 HB.instance Definition _ (R : realFieldType) :=
   Order_isNbhs.Build _ R (@real_order_nbhsE R).
 
+#[export, non_forgetful_inheritance]
+HB.instance Definition _ (R : realType) :=
+  Order_isNbhs.Build _ R (@real_order_nbhsE R).
+
 Module Exports. HB.reexport. End Exports.
 
 End numFieldTopology.

From 7d93d27449144f3b149fb949a70bdcb48536c253 Mon Sep 17 00:00:00 2001
From: Yosuke-Ito-345 <glacier345@gmail.com>
Date: Sun, 13 Jul 2025 15:25:40 +0900
Subject: [PATCH 04/13] move HB ereal_OrderNbhs

---
 theories/ereal.v | 40 ++++++++++++++++++++++++++++++++++++++++
 1 file changed, 40 insertions(+)

diff --git a/theories/ereal.v b/theories/ereal.v
index f2401270d..7491d2d75 100644
--- a/theories/ereal.v
+++ b/theories/ereal.v
@@ -1557,3 +1557,43 @@ rewrite /= opprD addrA subrr distrC subr0 gtr0_norm; last by rewrite invr_gt0.
 rewrite -[ltLHS]mulr1 ltr_pdivrMl // -ltr_pdivrMr // div1r.
 by rewrite (lt_le_trans (floorD1_gt _))// Nfloor !natr1 mulrz_nat ler_nat.
 Qed.
+(*
+Section ereal_OrderNbhs.
+Variable R : realFieldType.
+
+Open Scope ring_scope.
+
+Lemma ereal_order_nbhsE (x : \bar R) :
+  nbhs x = filter_from (fun i => itv_open_ends i /\ x \in i) (fun i => [set` i]).
+Proof.
+apply/seteqP; split=> A.
+  rewrite /nbhs/=/ereal_nbhs/=; case x =>[r||].
+  - rewrite /nbhs/=/nbhs_ball_/filter_from/=; case=> e e_pos ball_re.
+    exists `](r - e)%:E, (r + e)%:E[ =>[|y/=].
+      split; first by rewrite/itv_open_ends/=; right.
+      rewrite in_itv/= EFinB gte_subl// EFinD lteDl//; exact/andP.
+    rewrite in_itv/= => /[dup]/gte_lte_real/fineK<-.
+    rewrite !lte_fin => fy; apply: ball_re.
+    by rewrite /ball_/= -opprB normrN ltr_norml ltrBrDl (ltrBlDl _ r).
+  - case=> M [? MA]; rewrite /filter_from/=.
+    exists `]M%:E, +oo[ =>[|y/=]; rewrite in_itv/= andbT; last exact: MA.
+    by split; first by rewrite/itv_open_ends; left.
+  - case=> M [? MA]; rewrite /filter_from/=.
+    exists `]-oo, M%:E[ =>[|y/=]; rewrite in_itv/=; last exact: MA.
+    by split; first by rewrite /itv_open_ends; left.
+rewrite /filter_from/= => [][][][[]r|[]][[]s|[]][][];
+  rewrite /itv_is_ray/itv_is_bd_open// in_itv/= =>_.
+  - rewrite /nbhs/=/ereal_nbhs/= => /[dup]/gte_lte_real/fineK<-.
+    case/andP=> rx sx rsA; apply: (nbhs_interval rx sx) => *.
+    by apply: rsA =>/=; rewrite in_itv/=; apply/andP.
+  - rewrite nbhsE/= => rx ?; exists (`]r, +oo[)%classic; rewrite /open_nbhs//.
+    by split; [rewrite set_itvE; exact: open_ereal_gt_ereal | exact: rx].
+  - rewrite nbhsE/= => xs ?; exists (`]-oo, s[)%classic; rewrite /open_nbhs//.
+    by split; [rewrite set_itvE; exact: open_ereal_lt_ereal | exact: xs].
+  - by rewrite set_itvE/= subTset => _ ->; exact: filter_nbhsT.
+Qed.
+
+HB.instance Definition _ := Order_isNbhs.Build _ (\bar R) ereal_order_nbhsE.
+
+End ereal_OrderNbhs.
+*)

From fdf3cbb2aeab4d1c13354eb39ad6470f78be6c00 Mon Sep 17 00:00:00 2001
From: Yosuke-Ito-345 <glacier345@gmail.com>
Date: Sun, 13 Jul 2025 15:52:08 +0900
Subject: [PATCH 05/13] delete unnecessary comment

---
 theories/ereal.v | 40 ----------------------------------------
 1 file changed, 40 deletions(-)

diff --git a/theories/ereal.v b/theories/ereal.v
index 7491d2d75..f2401270d 100644
--- a/theories/ereal.v
+++ b/theories/ereal.v
@@ -1557,43 +1557,3 @@ rewrite /= opprD addrA subrr distrC subr0 gtr0_norm; last by rewrite invr_gt0.
 rewrite -[ltLHS]mulr1 ltr_pdivrMl // -ltr_pdivrMr // div1r.
 by rewrite (lt_le_trans (floorD1_gt _))// Nfloor !natr1 mulrz_nat ler_nat.
 Qed.
-(*
-Section ereal_OrderNbhs.
-Variable R : realFieldType.
-
-Open Scope ring_scope.
-
-Lemma ereal_order_nbhsE (x : \bar R) :
-  nbhs x = filter_from (fun i => itv_open_ends i /\ x \in i) (fun i => [set` i]).
-Proof.
-apply/seteqP; split=> A.
-  rewrite /nbhs/=/ereal_nbhs/=; case x =>[r||].
-  - rewrite /nbhs/=/nbhs_ball_/filter_from/=; case=> e e_pos ball_re.
-    exists `](r - e)%:E, (r + e)%:E[ =>[|y/=].
-      split; first by rewrite/itv_open_ends/=; right.
-      rewrite in_itv/= EFinB gte_subl// EFinD lteDl//; exact/andP.
-    rewrite in_itv/= => /[dup]/gte_lte_real/fineK<-.
-    rewrite !lte_fin => fy; apply: ball_re.
-    by rewrite /ball_/= -opprB normrN ltr_norml ltrBrDl (ltrBlDl _ r).
-  - case=> M [? MA]; rewrite /filter_from/=.
-    exists `]M%:E, +oo[ =>[|y/=]; rewrite in_itv/= andbT; last exact: MA.
-    by split; first by rewrite/itv_open_ends; left.
-  - case=> M [? MA]; rewrite /filter_from/=.
-    exists `]-oo, M%:E[ =>[|y/=]; rewrite in_itv/=; last exact: MA.
-    by split; first by rewrite /itv_open_ends; left.
-rewrite /filter_from/= => [][][][[]r|[]][[]s|[]][][];
-  rewrite /itv_is_ray/itv_is_bd_open// in_itv/= =>_.
-  - rewrite /nbhs/=/ereal_nbhs/= => /[dup]/gte_lte_real/fineK<-.
-    case/andP=> rx sx rsA; apply: (nbhs_interval rx sx) => *.
-    by apply: rsA =>/=; rewrite in_itv/=; apply/andP.
-  - rewrite nbhsE/= => rx ?; exists (`]r, +oo[)%classic; rewrite /open_nbhs//.
-    by split; [rewrite set_itvE; exact: open_ereal_gt_ereal | exact: rx].
-  - rewrite nbhsE/= => xs ?; exists (`]-oo, s[)%classic; rewrite /open_nbhs//.
-    by split; [rewrite set_itvE; exact: open_ereal_lt_ereal | exact: xs].
-  - by rewrite set_itvE/= subTset => _ ->; exact: filter_nbhsT.
-Qed.
-
-HB.instance Definition _ := Order_isNbhs.Build _ (\bar R) ereal_order_nbhsE.
-
-End ereal_OrderNbhs.
-*)

From dad97a03d0c47d55605b5eb2c4ceba3b24353b7a Mon Sep 17 00:00:00 2001
From: Yosuke-Ito-345 <glacier345@gmail.com>
Date: Sun, 13 Jul 2025 15:58:29 +0900
Subject: [PATCH 06/13] document

---
 CHANGELOG_UNRELEASED.md | 50 ++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 49 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 6b5518a9d..fd74e1e5c 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -6,6 +6,42 @@
 
 - in `constructive_ereal.v`:
   + lemma `ltgte_fin_num`
+- in `unstable.v`:
+  + lemma `sqrtK`
+
+- in `realfun.v`:
+  + instance `is_derive1_sqrt`
+- in `mathcomp_extra.v`:
+  + lemmas `subrKC`, `sumr_le0`, `card_fset_sum1`
+
+- in `functions.v`:
+  + lemmas `fct_prodE`, `prodrfctE`
+
+- in `exp.v:
+  + lemma `norm_expR`
+- in `hoelder.v`
+  + lemma `hoelder_conj_ge1`
+
+- in `reals.v`:
+  + definition `irrational`
+  + lemmas `irrationalE`, `rationalP` 
+
+- in `constructive_ereal.v`:
+  + lemma `gte_lte_real`
+
+- in `ereal_normedtype.v`:
+  + lemma `ereal_order_nbhsE`
+
+- in `topology_structure.v`:
+  + lemmas `denseI`, `dense0`
+
+- in `pseudometric_normed_Zmodule.v`:
+  + lemma `dense_set1C`
+
+- new file `borel_hierarchy.v`:
+  + definitions `Gdelta`, `Fsigma`
+  + lemmas `closed_Fsigma`, `Gdelta_measurable`, `Gdelta_subspace_open`,
+    `irrational_Gdelta`, `not_rational_Gdelta`
 
 - in `num_normedtype.v`:
   + lemma `nbhs_infty_gtr`
@@ -20,12 +56,24 @@
   + lemmas `wlength_ge0`, `cumulative_content_sub_fsum`, `wlength_sigma_subadditive`, `lebesgue_stieltjes_measure_unique`
   + definitions `lebesgue_stieltjes_measure`, `completed_lebesgue_stieltjes_measure`
 
+- in `lebesgue_stieltjes_measure.v` generalized:
+  + lemma `right_continuousW`, 
+  + record `isCumulative`
+  + definition `Cumulative`
+
+- in `lebesgue_stieltjes_measure.v` specialized:
+  + lemma `nondecreasing_right_continuousP`
+  + definition `CumulativeBounded`
+
+- in `lebesgue_stieltjes_measure.v`, according to generalization of `Cumulative`, modified:
+  + lemmas `wlength_ge0`, `cumulative_content_sub_fsum`, `wlength_sigma_subadditive`, `lebesgue_stieltjes_measure_unique`
+  + definitions `lebesgue_stieltjes_measure`, `completed_lebesgue_stieltjes_measure`
+
 ### Renamed
 
 - in `lebesgue_stieltjes_measure.v`:
   + `cumulativeNy0` -> `cumulativeNy`
   + `cumulativey1` -> `cumulativey`
-	+ `cumulativey1` -> `cumulativey`
 
 ### Generalized
 

From c1cb0da13268dbe176e32a807a7d2b92c5781f44 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Mon, 14 Jul 2025 11:55:49 +0900
Subject: [PATCH 07/13] nitpick

---
 CHANGELOG_UNRELEASED.md | 13 +++++--------
 1 file changed, 5 insertions(+), 8 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index fd74e1e5c..0efb741e6 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -27,10 +27,7 @@
   + lemmas `irrationalE`, `rationalP` 
 
 - in `constructive_ereal.v`:
-  + lemma `gte_lte_real`
-
-- in `ereal_normedtype.v`:
-  + lemma `ereal_order_nbhsE`
+  + lemma `gte_lte_fin_num`
 
 - in `topology_structure.v`:
   + lemmas `denseI`, `dense0`
@@ -56,13 +53,13 @@
   + lemmas `wlength_ge0`, `cumulative_content_sub_fsum`, `wlength_sigma_subadditive`, `lebesgue_stieltjes_measure_unique`
   + definitions `lebesgue_stieltjes_measure`, `completed_lebesgue_stieltjes_measure`
 
-- in `lebesgue_stieltjes_measure.v` generalized:
-  + lemma `right_continuousW`, 
+- in `lebesgue_stieltjes_measure.v` generalized (codomain is now an `orderNbhsType`):
+  + lemma `right_continuousW`
   + record `isCumulative`
   + definition `Cumulative`
 
-- in `lebesgue_stieltjes_measure.v` specialized:
-  + lemma `nondecreasing_right_continuousP`
+- in `lebesgue_stieltjes_measure.v` specialized from `numFieldType` to `realFieldType`:
+  + lemma `nondecreasing_right_continuousP` 
   + definition `CumulativeBounded`
 
 - in `lebesgue_stieltjes_measure.v`, according to generalization of `Cumulative`, modified:

From 0de92f05f7f5089ae4f17a59b7cfca0d7747242e Mon Sep 17 00:00:00 2001
From: Yosuke-Ito-345 <glacier345@gmail.com>
Date: Mon, 21 Jul 2025 11:19:29 +0900
Subject: [PATCH 08/13] add lemma lebesgue_stieltjes_cdf_id

---
 theories/probability.v | 65 ++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 63 insertions(+), 2 deletions(-)

diff --git a/theories/probability.v b/theories/probability.v
index 06fed1326..c7112b1a3 100644
--- a/theories/probability.v
+++ b/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,7 +257,7 @@ 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.
 
@@ -282,7 +287,63 @@ have : lsf `]- n%:R, r] @[n --> \oo] --> lsf (\bigcup_n `]-n%:R, r]%classic).
 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 (g_sigma_algebraType R.-ocitv.-measurable) R).
+Local Open Scope measure_display_scope.
+
+Let T := g_sigma_algebraType R.-ocitv.-measurable.
+
+Let idTR : T -> R := idfun.
+
+#[local] HB.instance Definition _ :=
+  @isMeasurableFun.Build _ _ T R 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 T) (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.
+case: (leP a b) => [ab | ba]; last first.
+  by rewrite set_itv_ge ?wlength0 ?measure0// bnd_simp -leNgt ltW.
+rewrite wlength_itv_bnd// EFinB !fineK ?cdf_fin_num//.
+rewrite /fcdf/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.
+exact/(le_lt_trans _ (ltry 1))/probability_le1.
+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.

From 8fbb4ae87d70595992c4faac0763e73a14f7e8f3 Mon Sep 17 00:00:00 2001
From: Yosuke-Ito-345 <glacier345@gmail.com>
Date: Mon, 21 Jul 2025 15:19:08 +0900
Subject: [PATCH 09/13] document

---
 CHANGELOG_UNRELEASED.md | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 0efb741e6..b41c5c449 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -35,6 +35,9 @@
 - in `pseudometric_normed_Zmodule.v`:
   + lemma `dense_set1C`
 
+- in `probability.v`:
+	  + lemmas `cdf_fin_num`, `lebesgue_stieltjes_cdf_id`
+
 - new file `borel_hierarchy.v`:
   + definitions `Gdelta`, `Fsigma`
   + lemmas `closed_Fsigma`, `Gdelta_measurable`, `Gdelta_subspace_open`,

From 6045dee1b3db6a36ac63cfbf373d105e8437e263 Mon Sep 17 00:00:00 2001
From: Yosuke-Ito-345 <glacier345@gmail.com>
Date: Sat, 23 Aug 2025 21:50:54 +0900
Subject: [PATCH 10/13] update changelog

---
 CHANGELOG_UNRELEASED.md | 45 -----------------------------------------
 1 file changed, 45 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index b41c5c449..cae072a21 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -6,34 +6,6 @@
 
 - in `constructive_ereal.v`:
   + lemma `ltgte_fin_num`
-- in `unstable.v`:
-  + lemma `sqrtK`
-
-- in `realfun.v`:
-  + instance `is_derive1_sqrt`
-- in `mathcomp_extra.v`:
-  + lemmas `subrKC`, `sumr_le0`, `card_fset_sum1`
-
-- in `functions.v`:
-  + lemmas `fct_prodE`, `prodrfctE`
-
-- in `exp.v:
-  + lemma `norm_expR`
-- in `hoelder.v`
-  + lemma `hoelder_conj_ge1`
-
-- in `reals.v`:
-  + definition `irrational`
-  + lemmas `irrationalE`, `rationalP` 
-
-- in `constructive_ereal.v`:
-  + lemma `gte_lte_fin_num`
-
-- in `topology_structure.v`:
-  + lemmas `denseI`, `dense0`
-
-- in `pseudometric_normed_Zmodule.v`:
-  + lemma `dense_set1C`
 
 - in `probability.v`:
 	  + lemmas `cdf_fin_num`, `lebesgue_stieltjes_cdf_id`
@@ -48,19 +20,6 @@
 
 ### Changed
 
-- in `lebesgue_stieltjes_measure.v` specialized from `numFieldType` to `realFieldType`:
-  + lemma `nondecreasing_right_continuousP` 
-  + definition `CumulativeBounded`
-
-- in `lebesgue_stieltjes_measure.v`, according to generalization of `Cumulative`, modified:
-  + lemmas `wlength_ge0`, `cumulative_content_sub_fsum`, `wlength_sigma_subadditive`, `lebesgue_stieltjes_measure_unique`
-  + definitions `lebesgue_stieltjes_measure`, `completed_lebesgue_stieltjes_measure`
-
-- in `lebesgue_stieltjes_measure.v` generalized (codomain is now an `orderNbhsType`):
-  + lemma `right_continuousW`
-  + record `isCumulative`
-  + definition `Cumulative`
-
 - in `lebesgue_stieltjes_measure.v` specialized from `numFieldType` to `realFieldType`:
   + lemma `nondecreasing_right_continuousP` 
   + definition `CumulativeBounded`
@@ -71,10 +30,6 @@
 
 ### Renamed
 
-- in `lebesgue_stieltjes_measure.v`:
-  + `cumulativeNy0` -> `cumulativeNy`
-  + `cumulativey1` -> `cumulativey`
-
 ### Generalized
 
 - in `lebesgue_stieltjes_measure.v` generalized (codomain is now an `orderNbhsType`):

From 6bd613d63dec753c0538f2a466107ae3a0e29fab Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Sun, 24 Aug 2025 00:07:41 +0900
Subject: [PATCH 11/13] more systematic use of measurableTypeR

---
 theories/ftc.v                        |  2 +-
 theories/lebesgue_measure.v           |  6 +++---
 theories/lebesgue_stieltjes_measure.v | 10 +++++-----
 theories/probability.v                | 22 +++++++++-------------
 4 files changed, 18 insertions(+), 22 deletions(-)

diff --git a/theories/ftc.v b/theories/ftc.v
index 4abdd3a67..8399560d6 100644
--- a/theories/ftc.v
+++ b/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.
 
diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v
index f75da4bc9..a6d9a7356 100644
--- a/theories/lebesgue_measure.v
+++ b/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.
diff --git a/theories/lebesgue_stieltjes_measure.v b/theories/lebesgue_stieltjes_measure.v
index c099013a8..c6eb7627d 100644
--- a/theories/lebesgue_stieltjes_measure.v
+++ b/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.
diff --git a/theories/probability.v b/theories/probability.v
index c7112b1a3..fd58bfb94 100644
--- a/theories/probability.v
+++ b/theories/probability.v
@@ -261,13 +261,12 @@ 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.
@@ -290,22 +289,19 @@ Unshelve. all: by end_near. Qed.
 End cdf_of_lebesgue_stieltjes_measure.
 
 Section lebesgue_stieltjes_measure_of_cdf.
-Context {R : realType}
-  (P : probability (g_sigma_algebraType R.-ocitv.-measurable) R).
+Context {R : realType} (P : probability (measurableTypeR R) R).
 Local Open Scope measure_display_scope.
 
-Let T := g_sigma_algebraType R.-ocitv.-measurable.
-
-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 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].
+by move=> *; apply: fine_le; [exact: cdf_fin_num.. | exact: cdf_nondecreasing].
 Qed.
 
 Let fcdf_rc : right_continuous fcdf.
@@ -328,7 +324,7 @@ Proof. exact/fine_cvg/cvg_cdfy1. Qed.
 
 Let lscdf := lebesgue_stieltjes_measure fcdf.
 
-Lemma lebesgue_stieltjes_cdf_id (A : set T) (mA : measurable A) : lscdf A = P A.
+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/=.

From 1529325880190b8558ec47bdd53334a794dab534 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Sun, 24 Aug 2025 00:47:48 +0900
Subject: [PATCH 12/13] nitpick

---
 theories/probability.v | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/theories/probability.v b/theories/probability.v
index fd58bfb94..6927b7e6e 100644
--- a/theories/probability.v
+++ b/theories/probability.v
@@ -281,7 +281,7 @@ 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.
@@ -327,16 +327,16 @@ 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 /lebesgue_stieltjes_measure /measure_extension/=.
 rewrite measurable_mu_extE/=; last exact: is_ocitv.
-case: (leP a b) => [ab | ba]; last first.
+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 /fcdf/cdf/distribution/pushforward !preimage_id.
+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.
-exact/(le_lt_trans _ (ltry 1))/probability_le1.
+by rewrite -ge0_fin_numE// fin_num_measure.
 Qed.
 
 End lebesgue_stieltjes_measure_of_cdf.

From b3655d47493f65366d5481e0f65b491311180087 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Sun, 24 Aug 2025 00:50:49 +0900
Subject: [PATCH 13/13] fix

---
 CHANGELOG_UNRELEASED.md | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index cae072a21..60c4e915b 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -8,12 +8,7 @@
   + lemma `ltgte_fin_num`
 
 - in `probability.v`:
-	  + lemmas `cdf_fin_num`, `lebesgue_stieltjes_cdf_id`
-
-- new file `borel_hierarchy.v`:
-  + definitions `Gdelta`, `Fsigma`
-  + lemmas `closed_Fsigma`, `Gdelta_measurable`, `Gdelta_subspace_open`,
-    `irrational_Gdelta`, `not_rational_Gdelta`
+  + lemmas `cdf_fin_num`, `lebesgue_stieltjes_cdf_id`
 
 - in `num_normedtype.v`:
   + lemma `nbhs_infty_gtr`