How can I prove has_esp when using mathcomp.analysis?

Question

How can I prove the following goal (which I believe to be true) using mathcomp.analysis?

From mathcomp Require Import all_ssreflect all_algebra.
From mathcomp.analysis Require Import reals distr.
Open Scope ring_scope.
Parameter R : realType.

Goal forall d:{distr R / R}, \E_[d] (fun r => r) <= \E_[d] (fun r => r + 1).
  intro. apply le_exp. (* stuck *)

It compares the expected value of two expressions, r and r+1, in any distribution of real numbers. That lemma le_exp of mathcomp.analysis is informally:

has_esp μ f1 → has_esp μ f2 → (∀ x, f1 x ≤ f2 x) → \E_[μ] f1 ≤ \E_[μ] f2

After applying le_exp, I have trouble proving has_esp, which needs proving the two functions summable. Can it be proved? How?

Page of mathcomp.analysis: https://github.com/math-comp/analysis

Answer 1

E_[d] idfun does not necessarily converge. Take for instance the discrete distribution that maps $2^{n+1}$ to $2^{-n}$ for $n \geq 1$. You can complete the proof if you ask E_[d] idfun to exist.

(* -------------------------------------------------------------------- *)
From mathcomp          Require Import all_ssreflect all_algebra.
From mathcomp.analysis Require Import boolp reals realsum distr.

(* -------------------------------------------------------------------- *)
Set   Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Unset SsrOldRewriteGoalsOrder.

(* -------------------------------------------------------------------- *)
Open Scope ring_scope.

Import GRing Num.Theory.

(* -------------------------------------------------------------------- *)
Section G.
Context {R : realType}.

Lemma L (d : {distr R / R}) :
  \E?_[d] idfun -> \E_[d] idfun <= \E_[d] (+%R^~ 1).
Proof.
move=> smid; apply: le_exp => // [|x]; last by rewrite ler_addl ler01.
have /(summableD smid) := has_expC d 1.
by apply/eq_summable => x /=; rewrite mulrDl !mul1r.
Qed.
End G.