prove Ep_dlet when everything converges

theories/analysis/RealSeries.ec

@@ -1002,6 +1002,49 @@ lemma summable_pswap ['a 'b] (s : 'a * 'b -> real) :
   summable s => summable (s \o pswap).
 proof. by apply/summable_bij/bij_pswap. qed.
 
+lemma summable_swap ['a 'b] (fa : 'a -> real) (fb : 'b -> real) (F : 'a -> 'b -> real) :
+     (forall x, 0%r <= fa x)
+  => (forall y, 0%r <= fb y)
+  => (forall x y, 0%r <= F x y)
+  => summable (fun y => sum (fun x => fa x * F x y) * fb y)
+  => (forall y, fb y <> 0%r => summable (fun x => fa x * F x y))
+  => summable (fun x => fa x * sum (fun y => F x y * fb y))
+  /\ (forall x, fa x <> 0%r => summable (fun y => F x y * fb y)).
+proof.
+move=> ge0_fa ge0_fb ge0_F smb subsmb; rewrite andbC &(andaE); split.
+- move=> x nz_fax; pose S := fun y => sum (fun x => fa x * F x y) * fb y.
+  rewrite (@summableZ_iff _ (fa x)) //; move/summable_le_pos: smb.
+  apply => y /=; split.
+  - by apply/mulr_ge0/mulr_ge0/ge0_fb/ge0_F/ge0_fa.
+  move=> _; case: (fb y = 0%r) => [-> // | nz_fb_y].
+  rewrite mulrA; apply: ler_wpmul2r; first exact/ge0_fb.
+  have := ler_big_sum (fun x => fa x * F x y) [x] _ _ _ => //=.
+  - move=> x'; apply: mulr_ge0; [exact/ge0_fa | exact/ge0_F].
+    by apply: subsmb.
+move=> subsmb2; pose S := fun y => sum (fun x => fa x * F x y) * fb y.
+exists (sum S) => J uqJ. pose G y x := fa x * (F x y * fb y).
+have ge0_G: forall x y, 0%r <= G y x.
+- by move=> x y; rewrite mulr_ge0 1?ge0_fa mulr_ge0 (ge0_fb, ge0_F).
+rewrite (@BRA.eq_bigr _ _ (fun x => sum (fun y => G y x))) /=.
+- move=> x _ @/G; rewrite ger0_norm.
+  - apply: mulr_ge0; [exact/ge0_fa | apply: ge0_sum => y /=].
+    by apply: mulr_ge0; [exact/ge0_F | exact/ge0_fb].
+  by rewrite -sumZ /= &(eq_sum) => y /=.
+rewrite -sum_big => [y _ @/G|].
+- case: (fa y = 0%r) => [-> /=|]; first exact/summable0.
+  by move/subsmb2; apply/summableZ.
+apply: ler_sum_pos => /= [y|]; [split | exact/smb].
+- by rewrite Bigreal.sumr_ge0 => x _ @/G; exact/ge0_G.
+move=> _ @/S @/G; case: (fb y = 0%r) => [-> /= | nz_fb_y].
+- by rewrite BRA.big1_eq.
+rewrite -sumZr -(@BRA.eq_bigr _ (fun x => (fa x * F x y) * fb y)) /=.
+- by move=> x _; ring.
+rewrite -BRA.mulr_suml sumZr &(ler_wpmul2r) 1:&ge0_fb.
+apply: ler_big_sum => //=.
+- by move=> x; apply: mulr_ge0; [exact/ge0_fa | exact/ge0_F].
+- by apply: subsmb.
+qed.
+
 lemma pswap_summable (s : 'a * 'b -> real) : 
   summable (s \o pswap) => summable s.
 proof. by move=> /summable_pswap; apply eq_summable => -[//]. qed.

theories/datatypes/Xreal.ec

@@ -1,6 +1,7 @@
 require import AllCore RealSeries List Distr StdBigop DBool DInterval.  
+require import StdOrder.
 require Subtype Bigop.
-import Bigreal Bigint.
+import Bigreal Bigint RealOrder.
 
 (* -------------------------------------------------------------------- *)
 (* Definition of R+                                                     *)
@@ -83,6 +84,9 @@ axiom witness_0 : witness = 0%rp.
 lemma of_real_neg x : x < 0.0 =>  x%rp = 0%rp.
 proof. smt(to_realK val_of_real witness_0). qed.
 
+lemma of_real_le0 x : x <= 0%r => x%rp = 0%rp.
+proof. by rewrite ler_eqVlt; case => [->// | /of_real_neg]. qed.
+
 lemma to_realK_simpl (x:realp) : x%r%rp = x by apply: to_realKd.
 hint simplify to_realK_simpl, of_realK.
 
@@ -384,6 +388,26 @@ proof.
 qed.
 
 (* -------------------------------------------------------------- *)
+lemma md_realP (c : real) (x : xreal) :
+  is_real (c ** x) <=> c <= 0%r \/ x <> oo.
+proof.
+case: x => //= @/( ** ); case: (c <= 0%r) => /=.
+- by move/of_real_le0 => ->.
+- move/ltrNge => gt0_c; rewrite -(inj_eq _ to_real_inj) /=.
+  by rewrite to_pos_pos 1:&ltrW // gtr_eqF.
+qed.
+
+lemma md_eqinfP (c : real) (x : xreal) :
+  c ** x = oo <=> 0%r < c /\ x = oo.
+proof.
+have := md_realP c x; case: (c ** x) => //=.
+- by rewrite negb_and ltrNge.
+- by rewrite negb_or ltrNge.
+qed.
+
+lemma to_real_md (c : real) (x : xreal) :
+  to_real (c ** x) = c%pos * to_real x.
+proof. by case: x => //= @/( ** ); case: (c%rp = 0%rp). qed.
 
 lemma is_real_le x y : x <= y => is_real y => is_real x.
 proof. by case: x y => [x|] [y|]. qed.
@@ -428,6 +452,18 @@ theory Lift.
   op to_real ['a] (f : 'a -> xreal) = 
     fun x => to_real (f x).
 
+  lemma is_realPn ['a] (f : 'a -> xreal) :
+    !is_real f <=> exists x, f x = oo.
+  proof.
+  split.
+  - by case/negb_forall=> /= y fyE; exists y; case: (f y) fyE.
+  - by case=> x fxE; apply/negP => /(_ x); rewrite fxE.
+  qed.
+
+  lemma to_real_mdfun (d : 'a distr) (f : 'a -> xreal) :
+    to_real (d ** f) = fun x => mu1 d x * to_real (f x).
+  proof. by apply/fun_ext=> x; rewrite /to_real to_real_md. qed.
+
   lemma eq_is_real ['a] (f g : 'a -> xreal) :
     (forall (x : 'a), f x = g x) => 
     is_real f = is_real g.
@@ -736,12 +772,71 @@ proof.
   by rewrite big_seq1 /( ** ) /= dunit1E /= one_neq0.
 qed.
 
-lemma Ep_dlet (d:'a distr) (F: 'a -> 'b distr) f : 
+(* -------------------------------------------------------------------- *)
+lemma EP_E ['a] (d : 'a distr) (f : 'a -> xreal) :
+     is_real (d ** f)
+  => summable (to_real (d ** f))
+  => Ep d f = (E d (to_real f))%xr.
+proof.
+move=> rl_f smb_f; rewrite /Ep /= rl_f /= /psuminf smb_f /=; congr.
+by apply: eq_sum => x /=; rewrite to_real_mdfun /= RField.mulrC.
+qed.
+
+(* -------------------------------------------------------------------- *)
+lemma Ep_dlet (d : 'a distr) (F : 'a -> 'b distr) f : 
   Ep (dlet d F) f = Ep d (fun x => Ep (F x) f).
 proof.
-  admit.
+pose D := dlet d F; case: (is_real (D ** f)); last first.
+- admit.
+move=> isrl; case: (summable (to_real (D ** f))); last first.
+- admit.
+pose fa (x : 'a) := mu1 d x.
+pose fb (y : 'b) := to_real f y.
+pose G x y := mu1 (F x) y.
+have ^eqf + ^smb0 - -> smb:
+  to_real (D ** f) = (fun y => sum (fun x => fa x * G x y) * fb y).
+- by apply/fun_ext=> y; rewrite to_real_mdfun /= dlet1E.
+have subsmb: forall y, fb y <> 0%r => summable (fun x => fa x * G x y).
+- move=> y _; apply: summable_mu1_wght => x /=; split.
+  - by apply: ge0_mu1.
+  - by move=> _; apply: le1_mu1.
+have [smb2 subsmb2] := summable_swap _ _ _ _ _ _ smb subsmb.
+- by move=> x; apply: ge0_mu1.
+- by move=> y; apply: to_realP.
+- by move=> x y; apply ge0_mu1.
+rewrite EP_E // /D; rewrite exp_dlet.
+- by apply: eq_summable smb0 => x /=; rewrite RField.mulrC to_real_mdfun.
+have is_real_Fx_f: forall x, x \in d => is_real (F x ** f).
+- move=> x x_d y /=; move/(_ y): isrl; case/md_realP; last first.
+  - by move=> real_fy; apply/md_realP; right.
+  rewrite ler_eqVlt ltrNge ge0_mu /= /D dlet1E sump_eq0P /=.
+  - by move=> x'; apply: mulr_ge0.
+  - by apply: summable_mu1_wght.
+  by move/(_ x); rewrite RField.mulf_eq0 -supportPn x_d /= => ->.
+have smb_Fx_f: forall x, x \in d => summable (to_real (F x ** f)).
+- move=> x x_d; have ->: to_real (F x ** f) = (fun y => G x y * fb y).
+  - by apply/fun_ext=> y; rewrite to_real_mdfun /=.
+  by apply/subsmb2/gtr_eqF/x_d.
+have eqE1: forall x, x \in d => to_real (Ep (F x) f) = E (F x) (to_real f).
+- move=> x x_d; rewrite EP_E /=.
+  - by apply/is_real_Fx_f.
+  - by apply/smb_Fx_f.
+  - by rewrite to_pos_pos // &(exp_ge0) => y _; apply: to_realP.
+apply: (eq_trans _ (E d (fun x => to_real (Ep (F x) f)))%xr).
+- by do 2! congr; apply: eq_exp => x x_d /=; rewrite eqE1.
+rewrite EP_E //=.
+- move=> x /=; apply/md_realP; rewrite ler_eqVlt ltrNge ge0_mu1 /=.
+  case: (x \in d) => [x_d | /supportPn -> //]; right.
+  by rewrite /Ep /= is_real_Fx_f //= /psuminf smb_Fx_f.
+- suff ->: to_real (fun x => mu1 d x ** Ep (F x) f) =
+    (fun x => fa x * sum (fun y => G x y * fb y)) by apply/smb2.
+  apply/fun_ext => x /=; rewrite to_real_mdfun /=.
+  case: (x \in d); last by move/supportPn => @/fa ->.
+  move=> x_d; congr => //; rewrite eqE1 // /E.
+  by apply: eq_sum => /= y; rewrite RField.mulrC.
 qed.
 
+(* -------------------------------------------------------------------- *)
 lemma Ep_dmap (d:'a distr) (F: 'a -> 'b) (f: 'b -> xreal) : 
   Ep (dmap d F) f = Ep d (fun x => f (F x)).
 proof. rewrite /dmap Ep_dlet; apply eq_Ep => x _ /=; apply Ep_dunit. qed.