From 73982039f9800a261e28ba41f303260cf4feb4a4 Mon Sep 17 00:00:00 2001
From: Lionel Blatter <lionel.blatter@wanadoo.fr>
Date: Tue, 30 Jun 2026 10:46:09 +0200
Subject: [PATCH] Add proof for interchange_psum using esum

---
 experimental_reals/realsum.v | 43 ++++++++++++++++++++++++++++++++++--
 1 file changed, 41 insertions(+), 2 deletions(-)

diff --git a/experimental_reals/realsum.v b/experimental_reals/realsum.v
index 80b7b2e90c..56b7c443a8 100644
--- a/experimental_reals/realsum.v
+++ b/experimental_reals/realsum.v
@@ -694,6 +694,11 @@ case=> J ->; exists J.
 by under [in RHS]eq_bigr do rewrite normr_id.
 Qed.
 
+Lemma esum_psum_abs S :
+  summable \`| S | ->
+ (PosSum.psum (fun y => S y))%:E = \esum_(y in [set: T]) `|S y|%:E.
+Proof. by move => ?; rewrite -psum_abs -esum_psum. Qed.
+
 Lemma eq_psum_abs S1 S2 : \`|S1| =1 \`|S2| -> PosSum.psum S1 = PosSum.psum S2.
 Proof.
 by move=> eqS; rewrite -[LHS]psum_abs -[RHS]psum_abs; apply/eq_psum.
@@ -1077,8 +1082,42 @@ Qed.
 
 End PSumInterchange.
 
-#[deprecated(since="1.17.0", note="use `interchange_psum` instead")]
-Notation __admitted__interchange_psum := interchange_psum (only parsing).
+(* -------------------------------------------------------------------- *)
+Section PSumInterchangeEsum.
+Context {R : realType} {T U : choiceType} (S: T -> U -> R).
+Hypothesis H1 : (forall x, summable (S x)).
+Hypothesis H2 : summable (PosSum.psum \o S).
+
+Lemma esum_psum_abs2:
+  (PosSum.psum (fun x => PosSum.psum (fun y => S x y)))%:E =
+  \esum_(x in [set: T]) \esum_(y in [set: U]) `|S x y|%:E.
+Proof.
+rewrite -esum_psum//; first by move=> x; exact: ge0_psum.
+by apply: eq_esum => x _; rewrite esum_psum_abs // summable_abs.
+Qed.
+
+Lemma interchange_psum_alt :
+  PosSum.psum (PosSum.psum \o S) =
+  PosSum.psum (fun y => PosSum.psum (S ^~ y)).
+Proof.
+apply: EFin_inj; rewrite esum_psum_abs2 exchange_esum.
++ by move => ? ?; rewrite lee_fin.
+have summable_y y : summable (fun x : T => `|S x y|).
++ apply: (le_summable (g := fun x => PosSum.psum (fun y' => S x y'))) => //  x.
+  by apply/andP; split; [exact: normr_ge0 | exact: ger1_psum y (H1 x)].
+under eq_esum => y _ do rewrite -esum_psum_abs //.
+rewrite -esum_psum//.
++ by move=> y; exact: ge0_psum.
+apply /esum_summableP; rewrite /esum.summable.
+apply: (@le_lt_trans _ _ (\esum_(y in [set: U]) (PosSum.psum (fun x => S x y))%:E)).
++ by apply  le_esum=> y _; rewrite /comp/= ger0_norm// ge0_psum.
+under eq_esum => y _ do rewrite esum_psum_abs//.
+rewrite exchange_esum.
+ + by move => ? ?; rewrite lee_fin.
+ + by rewrite  -esum_psum_abs2 ltey.
+Qed.
+
+End PSumInterchangeEsum.
 
 (* -------------------------------------------------------------------- *)
 Section SumTheory.