From ba71227018495f058e750a453664cc0a6843ed53 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Tue, 24 Jun 2025 23:25:12 +0900
Subject: [PATCH] integral_sum and fix integrable_sum

---
 CHANGELOG_UNRELEASED.md                       |  5 +++
 .../lebesgue_integrable.v                     | 37 +++++++++++++++----
 2 files changed, 35 insertions(+), 7 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 399f8064a6..26d20e2db9 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -88,6 +88,8 @@
 
 - in `set_interval.v`:
   + lemma `memB_itv`, `memB_itv0`
+- in `lebesgue_integrable.v`:
+  + lemma `integral_sum`
 
 ### Changed
 
@@ -237,6 +239,9 @@
 - in `derive.v`:
   + lemmas `is_deriveX`, `deriveX`, `exp_derive`, `exp_derive1`
 
+- in `lebesgue_integrable.v`:
+  + lemma `integrable_sum`
+
 ### Deprecated
 
 - in `set_interval.v`:
diff --git a/theories/lebesgue_integral_theory/lebesgue_integrable.v b/theories/lebesgue_integral_theory/lebesgue_integrable.v
index ae594688ee..d147e9c45d 100644
--- a/theories/lebesgue_integral_theory/lebesgue_integrable.v
+++ b/theories/lebesgue_integral_theory/lebesgue_integrable.v
@@ -186,14 +186,15 @@ apply: (@le_lt_trans _ _ (\int[mu]_(x in D) (`|f x| + `|g x|))).
 by rewrite ge0_integralD //; [exact: lte_add_pinfty| exact: measurableT_comp..].
 Qed.
 
-Lemma integrable_sum (s : seq (T -> \bar R)) :
-  (forall h, h \in s -> mu_int h) -> mu_int (fun x => \sum_(h <- s) h x).
+Lemma integrable_sum I (s : seq I) (P : pred I) (h : I -> T -> \bar R) :
+  (forall i, P i -> mu_int (h i)) ->
+  mu_int (fun x => \sum_(i <- s | P i) h i x).
 Proof.
-elim: s => [_|h s ih hs].
+elim: s => [_|i s ih hs].
   by under eq_fun do rewrite big_nil; exact: integrable0.
-under eq_fun do rewrite big_cons; apply: integrableD => //.
-- by apply: hs; rewrite in_cons eqxx.
-- by apply: ih => k ks; apply: hs; rewrite in_cons ks orbT.
+under eq_fun do rewrite big_cons.
+have [Pi|Pi] := boolP (P i); last exact: ih.
+by apply: integrableD => //; [exact: hs|exact: ih].
 Qed.
 
 Lemma integrableB f g : mu_int f -> mu_int g -> mu_int (f \- g).
@@ -622,7 +623,7 @@ Section integralD.
 Local Open Scope ereal_scope.
 Context d (T : measurableType d) (R : realType).
 Variables (mu : {measure set T -> \bar R}) (D : set T) (mD : measurable D).
-Variables (f1 f2 : T -> \bar R).
+Variables f1 f2 : T -> \bar R.
 Hypotheses (if1 : mu.-integrable D f1) (if2 : mu.-integrable D f2).
 
 Let mf1 : measurable_fun D f1. Proof. exact: measurable_int if1. Qed.
@@ -681,6 +682,28 @@ Qed.
 
 End integralD.
 
+Section integral_sum.
+Local Open Scope ereal_scope.
+Context d (T : measurableType d) (R : realType).
+Variables (mu : {measure set T -> \bar R}) (D : set T) (mD : measurable D).
+Variables (I : Type) (f : I -> (T -> \bar R)).
+Hypothesis intf : forall n, mu.-integrable D (f n).
+
+Lemma integral_sum (s : seq I) (P : pred I) :
+  \int[mu]_(x in D) (\sum_(k <- s | P k) f k x) =
+  \sum_(k <- s | P k) \int[mu]_(x in D) (f k x).
+Proof.
+elim: s => [|h t ih].
+  under eq_integral do rewrite big_nil.
+  by rewrite integral0 big_nil.
+rewrite big_cons -ih -integralD//; last exact: integrable_sum.
+case: ifPn => Ph.
+  by apply: eq_integral => x xD; rewrite big_cons Ph.
+by apply: eq_integral => x xD; rewrite big_cons/= (negbTE Ph).
+Qed.
+
+End integral_sum.
+
 Section integralB.
 Local Open Scope ereal_scope.
 Context d (T : measurableType d) (R : realType).