Proof of interchange_psum using esum

experimental_reals/distr.v

@@ -525,9 +525,6 @@ Qed.
 
 End DLetDLet.
 
-#[deprecated(since="1.17.0", note="use `dlet_dlet` instead")]
-Notation __deprecated__dlet_dlet := dlet_dlet (only parsing).
-
 (* -------------------------------------------------------------------- *)
 Section DLetAlg.
 Context {T U : choiceType} (mu mu1 mu2 : {distr T / R}).
@@ -744,6 +741,8 @@ End Std.
 Notation __deprecated__dmargin_dlet := dmargin_dlet (only parsing).
 #[deprecated(since="1.17.0", note="use `dlet_dmargin` instead")]
 Notation __deprecated__dlet_dmargin := dlet_dmargin (only parsing).
+#[deprecated(since="1.17.0", note="use `dlet_dlet` instead")]
+Notation __deprecated__dlet_dlet := dlet_dlet (only parsing).
 
 Notation dfst mu := (dmargin fst mu).
 Notation dsnd mu := (dmargin snd mu).

experimental_reals/realsum.v

@@ -1104,8 +1104,62 @@ 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 (fun x => PosSum.psum (fun y => S x y)).
+
+Lemma sm_col y :  summable (fun x => `|S x y|).
+Proof.
+apply: (le_summable (F2 := fun x => PosSum.psum (fun y' => S x y'))) => //  x.
+by apply/andP; split; [exact: normr_ge0 | exact: ger1_psum y (H1 x)].
+Qed.
+
+Lemma inner_LHS x : (PosSum.psum (fun y => S x y))%:E = \esum_(y in [set: U]) `|S x y|%:E.
+Proof.
+by rewrite -psum_abs -esum_psum// summable_abs.
+Qed.
+
+Lemma HLHS : (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 inner_LHS.
+Qed.
+
+Lemma inner_RHS y : (PosSum.psum (fun x => S x y))%:E = \esum_(x in [set: T]) `|S x y|%:E.
+Proof.
+rewrite -psum_abs -esum_psum//; exact : sm_col.
+Qed.
+
+Lemma summable_psum : (\esum_(y in [set: U]) (PosSum.psum (fun x => S x y))%:E < +oo)%E.
+Proof.
+under eq_esum => y _ do rewrite inner_RHS.
+rewrite exchange_esum.
+ + by move => ? ?; rewrite lee_fin.
+ + by rewrite  -HLHS ltey.
+Qed.
+
+Lemma interchange_summable  : summable (fun y : U => psum (S^~ y)).
+Proof.
+apply/esum_summableP; rewrite /esum.summable.
+apply: le_lt_trans summable_psum; apply  le_esum.
+- by move=> y _; exact: abse_ge0.
+- by move=> y _; rewrite /comp/= ger0_norm// ge0_psum.
+Qed.
+
+Lemma interchange_psum' :
+  PosSum.psum (fun x => PosSum.psum (fun y => S x y)) =
+  PosSum.psum (fun y => PosSum.psum (fun x => S x y)).
+Proof.
+apply: EFin_inj; rewrite HLHS exchange_esum.
++ by move => ? ?; rewrite lee_fin.
+under eq_esum => ? _ do rewrite -inner_RHS.
+rewrite -esum_psum//; last first. exact: interchange_summable.
+by move=> y; exact: ge0_psum.
+Qed.
+End PSumInterchangeEsum.
 
 (* -------------------------------------------------------------------- *)
 Section SumTheory.

theories/measure_theory/measurable_structure.v

@@ -1319,6 +1319,9 @@ HB.instance Definition _ := @isMeasurable.Build (sigma_display G)
 
 End g_salgebra_instance.
 
+HB.instance Definition _ {T : pointedType} (G : set_system T) :=
+  Pointed.on (g_sigma_algebraType G).
+
 Notation "G .-sigma" := (sigma_display G) : measure_display_scope.
 Notation "G .-sigma.-measurable" :=
   (measurable : set_system (g_sigma_algebraType G)) : classical_set_scope.
@@ -1592,7 +1595,7 @@ Definition measure_prod_display :
 Proof. exact. Qed.
 
 Section product_salgebra_instance.
-Context d1 d2 (T1 : semiRingOfSetsType d1) (T2 : semiRingOfSetsType d2).
+Context {d1} {d2} {T1 : semiRingOfSetsType d1} {T2 : semiRingOfSetsType d2}.
 Let f1 := @fst T1 T2.
 Let f2 := @snd T1 T2.
 
@@ -1621,7 +1624,12 @@ Notation "p .-prod.-measurable" :=
   ((p.-prod).-measurable : set_system (_ * _)) :
     classical_set_scope.
 
-Lemma measurableX d1 d2 (T1 : semiRingOfSetsType d1) (T2 : semiRingOfSetsType d2)
+HB.instance Definition _
+    d d' (X : pmeasurableType d) (Y : pmeasurableType d') :=
+  Measurable.on (X * Y)%type.
+
+Lemma measurableX
+    d1 d2 (T1 : semiRingOfSetsType d1) (T2 : semiRingOfSetsType d2)
     (A : set T1) (B : set T2) :
   measurable A -> measurable B -> measurable (A `*` B).
 Proof.