Library discprob.prob.markov

From discprob.prob Require Export prob countable stochastic_order.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype choice fintype bigop.
Require Export Reals Psatz.


Lemma markov {A} {Ω: distrib A} (X: rrvar Ω) a :
  (∀ x, X x ≥ 0) →
  a > 0 →
  ex_Ex X →
  pr_ge X a ≤ Ex X / a.

Lemma chebyshev {A} {Ω: distrib A} (X: rrvar Ω) a :
  a > 0 →
  ex_Var X →
  pr_ge (mkRvar Ω (λ a, Rabs (X a - Ex X))) a ≤ Var X / a^2.