From 3e8f39f8be9bcc6059b89bdabb10e42ae42b5d31 Mon Sep 17 00:00:00 2001
From: Alessandro Bruni <brun@itu.dk>
Date: Thu, 14 Nov 2024 11:14:04 +0100
Subject: [PATCH] measurable_poweR

---
 theories/ehoelder.v | 74 ++++++++++++++++++---------------------------
 1 file changed, 29 insertions(+), 45 deletions(-)

diff --git a/theories/ehoelder.v b/theories/ehoelder.v
index c24feed96..2ad9eb709 100644
--- a/theories/ehoelder.v
+++ b/theories/ehoelder.v
@@ -175,13 +175,14 @@ Section Lnorme_properties.
   Proof.
     move => H; congr Lnorme; exact /funext.
   Qed.
-  Lemma measurable_poweR r :
+
+Lemma measurable_poweR r :
   measurable_fun [set: \bar R] (@poweR R ^~ r).
-  Proof.
-  move => _ /= B H.
-  rewrite setIidr; last first. 
-    apply subsetT.
-  rewrite [X in measurable X]
+Proof.
+move => _ /= B H.
+rewrite setIidr; last first. 
+  apply subsetT.
+rewrite [X in measurable X]
   (_ : (poweR^~ r @^-1` B) = 
   if (r == 0%R) then 
     (if 1 \in B then [set : \bar R] else set0) 
@@ -190,44 +191,27 @@ Section Lnorme_properties.
     `|` (B `&` [set +oo])
     `|` (if 0 \in B then [set -oo] else set0)
   ); last first.
-  case (r == 0%R) eqn:H0; apply/seteqP; 
-  split => [a //= H1 //= | a //= H1 //=];
-  move : H1; rewrite ?(eqP H0) //= ?poweRe0; 
-  rewrite /poweR ?H0 => H1.
-  - (*r == 0*) 
-  -- by case : ifPn => //=; rewrite notin_setE.
-  -- by move : H1; case : ifPn => //=; rewrite in_setE.
-  - (*r != 0*)
-  -- 
-  case a as [s | | ]. 
-  ---
-  repeat left. exists s; last first => //;
-  exists (s `^ r)%:E; last first => //=; split => //=; 
-  rewrite not_orE; split => //=.
-  ---
-  left; right => //=.
-  ---
-  right. rewrite -in_setE in H1. rewrite H1 //=.
-  --
-  case H1 as [H1 | H1].
-  ---
-  case H1 as [H1 | H1].
-  ----
-  destruct H1 as [b [c [H1 H2]] H3];
-  rewrite not_orE in H2; destruct H2 as [H2 H5].
-  case a as [s | | ] => //=; 
-  move : H4 H3; case c as [s' | | ] => //=; congruence.
-  ----
-  by case H1 as [H1 H2]; move : H1; rewrite H2. 
-  ----
-  move : H1; 
-  case : ifPn => //= => H1 H2; rewrite H2 -in_setE => //=.
-  case : ifP => [_ | ]. case : ifP => //=.
-  move => H0. repeat apply : measurableU.
-  
-
-
-
+case: ifPn => [/eqP ->|r0].
+  case: ifPn => [/set_mem B1|B1]; apply/seteqP; split=> // x /=; rewrite poweRe0// => /mem_set; exact: negP.
+  apply/seteqP; split => [a/=Bar|a/=].
+    case a as [s | | ].
+    - by left; left; exists s => //; exists (s `^ r)%:E => //; split => //; case.
+    - by rewrite /= (negbTE r0) in Bar; left; right => /=; split=> //.
+    - by right; rewrite /= (negbTE r0) in Bar; case: ifPn => //; rewrite notin_setE.
+  case.
+    case.
+      by case=> x; case; case=> [y| |] []+ /not_orP[]// _ _/=; move=> /[swap]->/[swap] <-.
+    by case=> /[swap] ->/=; rewrite (negbTE r0).
+  by case: ifPn => // /[swap] /= -> /=; rewrite (negbTE r0)=>/set_mem.
+case: ifPn => [|_]; first by case: ifPn => //.
+repeat apply : measurableU.
+apply: measurable_image_EFin.
+rewrite -[X in measurableR X] setTI.
+apply: @measurable_powR => //.
+exact: measurable_image_fine.
+exact: measurableI.
+by case: ifP.
+Qed.
 
 
 
@@ -295,4 +279,4 @@ Section Lnorme_properties.
 
 
 
-End Lnorme_properties.
\ No newline at end of file
+End Lnorme_properties.