4
$\begingroup$

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

$\endgroup$
0

1 Answer 1

2
$\begingroup$

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.
$\endgroup$
1
  • $\begingroup$ I was actually learning to use Coq for probabilistic reasoning with your strub/xhl on the side as a resource. Thank you for that and this answer. $\endgroup$
    – lyfeng
    Apr 20 at 0:08

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.