From 9b15f732e3061ab43a5b5000c4a7d1e28f334fd6 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Mon, 2 Dec 2024 15:03:21 +0900
Subject: [PATCH 1/2] instances for measures

- restriction of finite measure is finite
- scaling of finite measure is finite
---
 theories/measure.v | 33 +++++++++++++++++++++++++++++++++
 1 file changed, 33 insertions(+)

diff --git a/theories/measure.v b/theories/measure.v
index 6cfd34f05..d7b8335f5 100644
--- a/theories/measure.v
+++ b/theories/measure.v
@@ -3394,6 +3394,39 @@ HB.instance Definition _ := @isFinite.Build d T R k finite.
 
 HB.end.
 
+Section finite_restr.
+Context d (T : measurableType d) (R : realType).
+Variables (mu : {finite_measure set T -> \bar R}) (D : set T).
+Hypothesis mD : measurable D.
+
+Local Notation restr := (mrestr mu mD).
+
+Let fin_num_restr : fin_num_fun restr.
+Proof.
+move=> A mA; have := fin_num_measure mu A mA.
+rewrite !ge0_fin_numE//=; apply: le_lt_trans.
+by apply: le_measure => //; rewrite inE//=; exact: measurableI.
+Qed.
+
+HB.instance Definition _ := @Measure_isFinite.Build _ T _ restr fin_num_restr.
+
+End finite_restr.
+
+Section finite_mscale.
+Context d (T : measurableType d) (R : realType).
+Variables (mu : {finite_measure set T -> \bar R}) (r : {nonneg R}).
+
+Local Notation scale := (mscale r mu).
+
+Let fin_num_scale : fin_num_fun scale.
+Proof.
+by move=> A mA; have muA := fin_num_measure mu A mA; rewrite fin_numM.
+Qed.
+
+HB.instance Definition _ := @Measure_isFinite.Build _ T _ scale fin_num_scale.
+
+End finite_mscale.
+
 HB.factory Record Measure_isSFinite d (T : sigmaRingType d)
     (R : realType) (k : set T -> \bar R) of isMeasure _ _ _ k := {
   s_finite : exists s : {finite_measure set T -> \bar R}^nat,

From f0f01ad96d7ab3ec30c1c62340894107c7cbe674 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Tue, 3 Dec 2024 09:27:52 +0900
Subject: [PATCH 2/2] to please Coq 8.19.2

---
 theories/measure.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/measure.v b/theories/measure.v
index d7b8335f5..ef3c416c8 100644
--- a/theories/measure.v
+++ b/theories/measure.v
@@ -3405,7 +3405,7 @@ Let fin_num_restr : fin_num_fun restr.
 Proof.
 move=> A mA; have := fin_num_measure mu A mA.
 rewrite !ge0_fin_numE//=; apply: le_lt_trans.
-by apply: le_measure => //; rewrite inE//=; exact: measurableI.
+by rewrite /mrestr; apply: le_measure => //; rewrite inE//=; exact: measurableI.
 Qed.
 
 HB.instance Definition _ := @Measure_isFinite.Build _ T _ restr fin_num_restr.