From e7871ff1ba0e2f3d0a40b3638f9f33d81ee7fcb2 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Thu, 26 Jun 2025 15:19:07 +0900
Subject: [PATCH] Lfun1_integrable turned into an equivalence

---
 theories/hoelder.v     | 20 +++++++++++---------
 theories/probability.v | 21 +++++++++++++++------
 2 files changed, 26 insertions(+), 15 deletions(-)

diff --git a/theories/hoelder.v b/theories/hoelder.v
index 8b266937bc..3dd2963164 100644
--- a/theories/hoelder.v
+++ b/theories/hoelder.v
@@ -1088,16 +1088,18 @@ by under eq_integral => x _ do rewrite gee0_abs ?lee_fin ?powR_ge0//.
 Qed.
 
 Lemma Lfun1_integrable (f : T -> R) :
-  f \in Lfun mu 1 -> mu.-integrable setT (EFin \o f).
+  f \in Lfun mu 1 <-> mu.-integrable setT (EFin \o f).
 Proof.
-move=> /[dup] lf /Lfun_integrable => /(_ (lexx _)).
-under eq_fun => x do rewrite powRr1//.
-move/integrableP => [mf fley].
-apply/integrableP; split.
-  move: lf; rewrite inE => /andP[/[!inE]/= {}mf _].
-   exact: measurableT_comp.
-rewrite (le_lt_trans _ fley)//=.
-by under [leRHS]eq_integral => x _ do rewrite normr_id.
+split.
+- move=> /[dup] lf /Lfun_integrable => /(_ (lexx _)).
+  under eq_fun => x do rewrite powRr1//.
+  move/integrableP => [mf fley]; apply/integrableP; split.
+    by move: lf; rewrite inE=> /andP[/[!inE]/= {}mf _]; exact: measurableT_comp.
+  rewrite (le_lt_trans _ fley)//=.
+  by under [leRHS]eq_integral => x _ do rewrite normr_id.
+- move/integrableP => [mF iF].
+  rewrite inE; apply/andP; split; rewrite inE/=; first exact/measurable_EFinP.
+  by rewrite /finite_norm Lnorm1.
 Qed.
 
 Lemma Lfun2_integrable_sqr (f : T -> R) : f \in Lfun mu 2%:E ->
diff --git a/theories/probability.v b/theories/probability.v
index 231c38e5bf..b2d10eab06 100644
--- a/theories/probability.v
+++ b/theories/probability.v
@@ -261,7 +261,9 @@ Proof. by rewrite unlock. Qed.
 
 Lemma expectation_fin_num (X : T -> R) : X \in Lfun P 1 ->
   'E_P[X] \is a fin_num.
-Proof. by move=> ?; rewrite unlock integral_fune_fin_num ?Lfun1_integrable. Qed.
+Proof.
+by move=> ?; rewrite unlock integral_fune_fin_num//; exact/Lfun1_integrable.
+Qed.
 
 Lemma expectation_cst r : 'E_P[cst r] = r%:E.
 Proof. by rewrite unlock/= integral_cst//= probability_setT mule1. Qed.
@@ -278,7 +280,9 @@ Qed.
 
 Lemma expectationZl (X : T -> R) (k : R) : X \in Lfun P 1 ->
   'E_P[k \o* X] = k%:E * 'E_P [X].
-Proof. by move=> ?; rewrite unlock muleC -integralZr ?Lfun1_integrable. Qed.
+Proof.
+by move=> ?; rewrite unlock muleC -integralZr//; exact/Lfun1_integrable.
+Qed.
 
 Lemma expectation_ge0 (X : T -> R) : (forall x, 0 <= X x)%R ->
   0 <= 'E_P[X].
@@ -302,11 +306,15 @@ Qed.
 
 Lemma expectationD (X Y : T -> R) : X \in Lfun P 1 -> Y \in Lfun P 1 ->
   'E_P[X \+ Y] = 'E_P[X] + 'E_P[Y].
-Proof. by move=> ? ?; rewrite unlock integralD_EFin ?Lfun1_integrable. Qed.
+Proof.
+by move=> ? ?; rewrite unlock integralD_EFin//; exact/Lfun1_integrable.
+Qed.
 
 Lemma expectationB (X Y : T -> R) : X \in Lfun P 1 -> Y \in Lfun P 1 ->
   'E_P[X \- Y] = 'E_P[X] - 'E_P[Y].
-Proof. by move=> ? ?; rewrite unlock integralB_EFin ?Lfun1_integrable. Qed.
+Proof.
+by move=> ? ?; rewrite unlock integralB_EFin//; exact/Lfun1_integrable.
+Qed.
 
 Lemma expectation_sum (X : seq (T -> R)) :
     (forall Xi, Xi \in X -> Xi \in Lfun P 1) ->
@@ -710,11 +718,12 @@ have le (u : R) : (0 <= u)%R ->
     - by rewrite lerD2r -lee_fin EFinB finEK.
   apply: (le_trans (le_measure _ _ _ le)).
   - rewrite -[[set _ | _]]setTI inE; apply: emeasurable_fun_c_infty => [//|].
-    by apply: emeasurable_funB=> //; apply/measurable_int/(Lfun1_integrable X1).
+    apply: emeasurable_funB=> //.
+    by move/Lfun1_integrable : X1 => /measurable_int.
   - rewrite -[[set _ | _]]setTI inE; apply: emeasurable_fun_c_infty => [//|].
     rewrite measurable_EFinP [X in measurable_fun _ X](_ : _ =
       (fun x => x ^+ 2) \o (fun x => Y x + u))%R//.
-    by apply/measurableT_comp => //; apply/measurable_funD.
+    by apply/measurableT_comp => //; exact/measurable_funD.
   set eps := ((lambda + u) ^ 2)%R.
   have peps : (0 < eps)%R by rewrite exprz_gt0 ?ltr_wpDr.
   rewrite (lee_pdivlMr _ _ peps) muleC.