From cb1d1c98f9e980f61a2c8b43f43f03e7a53404dc Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Mon, 16 Dec 2024 14:40:53 +0900
Subject: [PATCH] add lemma measurable_powRr

---
 CHANGELOG_UNRELEASED.md     |  7 +++++++
 theories/lebesgue_measure.v | 23 +++++++++++++++--------
 2 files changed, 22 insertions(+), 8 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 56017a4e24..bed087256c 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -35,6 +35,9 @@
 - in `probability.v`
   + lemma `integral_distribution` (existsing lemma `integral_distribution` has been renamed)
 
+- in `lebesgue_measure.v`:
+  + lemma `measurable_powRr`
+
 ### Changed
 
 - in `lebesgue_integrale.v`
@@ -100,6 +103,10 @@
 - in `measure.v`:
   + `dynkin_setI_bigsetI` (use `big_ind` instead)
 
+- in `lebesgue_measurable.v`:
+  + notation `measurable_fun_power_pos` (deprecated since 0.6.3)
+  + notation `measurable_power_pos` (deprecated since 0.6.4)
+
 ### Infrastructure
 
 ### Misc
diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v
index 7491d4928d..e249063c6a 100644
--- a/theories/lebesgue_measure.v
+++ b/theories/lebesgue_measure.v
@@ -1180,9 +1180,10 @@ Proof.
 move=> mf.
 exact: (@measurable_comp _ _ _ _ _ _ setT (fun x : R => x ^+ n) _ f).
 Qed.
+#[deprecated(since="mathcomp-analysis 1.4.0", note="use `measurable_funX` instead")]
+Notation measurable_fun_pow := measurable_funX (only parsing).
 
-Lemma measurable_powR (R : realType) p :
-  measurable_fun [set: R] (@powR R ^~ p).
+Lemma measurable_powR (R : realType) p : measurable_fun [set: R] (@powR R ^~ p).
 Proof.
 apply: measurable_fun_if => //.
 - apply: (measurable_fun_bool true).
@@ -1194,14 +1195,20 @@ apply: measurable_fun_if => //.
 Qed.
 #[global] Hint Extern 0 (measurable_fun _ (@powR _ ^~ _)) =>
   solve [apply: measurable_powR] : core.
-#[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_powR` instead")]
-Notation measurable_fun_power_pos := measurable_powR (only parsing).
-#[deprecated(since="mathcomp-analysis 0.6.4", note="use `measurable_powR` instead")]
-Notation measurable_power_pos := measurable_powR (only parsing).
+
+Lemma measurable_powRr {R : realType} b : measurable_fun [set: R] (@powR R b).
+Proof.
+rewrite /powR; apply: measurable_fun_if => //.
+- rewrite preimage_true setTI/=.
+  case: (b == 0); rewrite ?set_true ?set_false.
+  + by apply: measurableT_comp => //; exact: measurable_fun_eqr.
+  + exact: measurable_fun_set0.
+- rewrite preimage_false setTI; apply: measurableT_comp => //.
+  exact: mulrr_measurable.
+Qed.
+
 #[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_maxr` instead")]
 Notation measurable_fun_max := measurable_maxr (only parsing).
-#[deprecated(since="mathcomp-analysis 1.4.0", note="use `measurable_funX` instead")]
-Notation measurable_fun_pow := measurable_funX (only parsing).
 
 Module NGenCInfty.
 Section ngencinfty.