proposition: Lemma __deprecated__pr_dlet E f (mu : {distr U / R}) : \P_[dlet f mu] E = \E_[mu] (fun x => \P_[f x] E).
proof: Proof. rewrite /esp -psum_sum => [x|]; first by rewrite mulr_ge0 ?ge0_pr. rewrite /pr; unlock dlet => /=; rewrite /mlet /=. pose F x y := (E x)%:R * (mu y * f y x). transitivity (psum (fun x => psum (fun y => F x y))); rewrite {}/F. by apply/eq_psum => x; rewrite -psumZ ?ler0n. rewrite __admitted__interchange_psum /=; last first. apply/eq_psum=> y /=; rewrite mulrC -psumZ //. by apply/eq_psum=> x /=; rewrite mulrCA. + have := summable_pr E (dlet f mu); apply/eq_summable. by move=> x; rewrite dletE psumZ ?ler0n. + by move=> y; apply/summable_condl/summable_mlet. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp classical_sets mathcomp_extra) xfinmap ereal reals discrete topology realseq realsum