# Probas.v: The monad for distributions

## Definition of distribution

Distributions are monotonic measure functions such that
• μ (1-f) <= 1 - μ f
• f <= 1 -g => μ (f+g) == μ f + μ g
• μ (k * f) = k * μ (f)
• μ (lub f_n) <= lub μ (f_n)

## Properties of measures

Lemma mu_monotonic : forall (A : Type)(m: distr A), monotonic (μ m).
Hint Resolve mu_monotonic.
Implicit Arguments mu_monotonic [A].

Lemma mu_stable_eq : forall (A : Type)(m: distr A), stable (μ m).
Hint Resolve mu_stable_eq.
Implicit Arguments mu_stable_eq [A].

Lemma mu_zero : forall (A : Type)(m: distr A), μ m (fzero A) == 0.
Hint Resolve mu_zero.

Lemma mu_zero_eq : forall (A : Type)(m: distr A) f,
(forall x, f x == 0) -> μ m f == 0.

Lemma mu_one_inv : forall (A : Type)(m:distr A),
μ m (fone A) == 1 -> forall f, μ m (finv f) == [1-] (μ m f).
Hint Resolve mu_one_inv.

Lemma mu_fplusok : forall (A : Type)(m:distr A) f g, fplusok f g ->
μ m f <= [1-] μ m g.
Hint Resolve mu_fplusok.

Lemma mu_le_minus : forall (A : Type)(m:distr A) (f g:MF A),
μ m (fminus f g) <= μ m f.
Hint Resolve mu_le_minus.

Lemma mu_le_plus : forall (A : Type)(m:distr A) (f g:MF A),
μ m (fplus f g) <= μ m f + μ m g.
Hint Resolve mu_le_plus.

Lemma mu_eq_plus : forall (A : Type)(m:distr A) (f g:MF A),
fplusok f g -> μ m (fplus f g) == μ m f + μ m g.
Hint Resolve mu_eq_plus.

Lemma mu_plus_zero : forall (A : Type)(m:distr A) (f g:MF A),
μ m f == 0 -> μ m g == 0 -> μ m (fplus f g) == 0.
Hint Resolve mu_plus_zero.

Lemma mu_plus_pos : forall (A : Type)(m:distr A) (f g:MF A),
0 < μ m (fplus f g) -> orc (0 < μ m f) (0 < μ m g).

Lemma mu_fcte : forall (A : Type)(m:(distr A)) (c:U),
μ m (fcte A c) == c * μ m (fone A).
Hint Resolve mu_fcte.

Lemma mu_fcte_le : forall (A : Type)(m:distr A) (c:U), μ m (fcte A c) <= c.

Lemma mu_fcte_eq : forall (A : Type)(m:distr A) (c:U),
μ m (fone A) == 1 -> μ m (fcte A c) == c.

Hint Resolve mu_fcte_le mu_fcte_eq.

Lemma mu_cte : forall (A : Type)(m:(distr A)) (c:U),
μ m (fun _ => c) == c * μ m (fone A).
Hint Resolve mu_cte.

Lemma mu_cte_le : forall (A : Type)(m:distr A) (c:U), μ m (fun _ => c) <= c.

Lemma mu_cte_eq : forall (A : Type)(m:distr A) (c:U),
μ m (fone A) == 1 -> μ m (fun _ => c) == c.
Hint Resolve mu_cte_le mu_cte_eq.

Lemma mu_stable_mult_right : forall (A : Type)(m:distr A) (c:U) (f : MF A),
μ m (fun x => (f x) * c) == (μ m f) * c.

Lemma mu_stable_minus : forall (A:Type) (m:distr A)(f g : MF A),
g <= f -> μ m (fun x => f x - g x) == μ m f - μ m g.

Lemma mu_inv_minus :
forall (A:Type) (m:distr A)(f: MF A), μ m (finv f) == μ m (fone A) - μ m f.

Lemma mu_stable_le_minus : forall (A:Type) (m:distr A)(f g : MF A),
μ m f - μ m g <= μ m (fun x => f x - g x).

Lemma mu_inv_minus_inv : forall (A:Type) (m:distr A)(f: MF A),
μ m (finv f) + [1-](μ m (fone A)) == [1-](μ m f).

Lemma mu_le_esp_inv : forall (A:Type) (m:distr A)(f g : MF A),
([1-]μ m (finv f)) & μ m g <= μ m (fesp f g).
Hint Resolve mu_le_esp_inv.

Lemma mu_stable_inv_inv : forall (A:Type) (m:distr A)(f : MF A),
μ m f <= [1-] μ m (finv f).
Hint Resolve mu_stable_inv_inv.

Lemma mu_stable_div : forall (A:Type) (m:distr A)(k:U)(f : MF A),
~ 0==k -> f <= fcte A k -> μ m (fdiv k f) == μ m f / k.

Lemma mu_stable_div_le : forall (A:Type) (m:distr A)(k:U)(f : MF A),
~ 0==k -> μ m (fdiv k f) <= μ m f / k.

Lemma mu_le_esp : forall (A:Type) (m:distr A)(f g : MF A),
μ m f & μ m g <= μ m (fesp f g).
Hint Resolve mu_le_esp.

Lemma mu_esp_one : forall (A:Type)(m:distr A)(f g:MF A),
1 <= μ m f -> μ m g == μ m (fesp f g).

Lemma mu_esp_zero : forall (A:Type)(m:distr A)(f g:MF A),
μ m (finv f) <= 0 -> μ m g == μ m (fesp f g).

Lemma mu_stable_mult2:
forall (A : Type) (d : distr A), forall (k : U)
(f : MF A), (μ d) (fun x => k * f x) == k * (μ d) f.

Lemma mu_stable_plus2:
forall (A : Type) (d : distr A) (f g: MF A),
fplusok f g -> (μ d) (fun x => f x + g x) == (μ d) f + (μ d) g.

Lemma mu_fzero_eq : forall A m, @μ A m (fun x => 0) == 0.

Lemma fplusok_plus_esp : forall (A : Type) (f g : MF A),
fplusok f (fminus g (fesp f g)).
Hint Resolve fplusok_plus_esp.

Lemma mu_eq_plus_esp :
forall (A : Type) (m : distr A) (f g : MF A),
μ m (fplus f g) == μ m f + (μ m g - (μ m (fesp f g))).
Hint Resolve mu_eq_plus_esp.

Instance Odistr (A:Type) : ord (distr A) :=
{Ole := fun (f g : distr A) => μ f <= μ g;
Oeq := fun (f g : distr A) => μ f == μ g}.
Defined.

Probability of termination

Definition pone A (m:distr A) := μ m (fone A).

Add Parametric Morphism A : (pone (A:=A) )
with signature Oeq ==> Oeq as pone_eq_compat.
Save.
Hint Resolve pone_eq_compat.

Definition Munit : forall A:Type, A -> distr A.
Defined.

Definition Mlet : forall A B:Type, distr A -> (A -> distr B) -> distr B.
Defined.

Lemma Munit_simpl : forall (A:Type) (q:A -> U) x, μ (Munit x) q = q x.

Lemma Mlet_simpl : forall (A B:Type) (m:distr A) (M:A -> distr B) (f:B -> U),
μ (Mlet m M) f = μ m (fun x => (μ (M x) f)).

## Operations on distributions

Lemma Munit_eq_compat : forall A (x y : A), x = y -> Munit x == Munit y.

Lemma Mlet_le_compat : forall (A B : Type) (m1 m2:distr A) (M1 M2 : A -> distr B),
m1 <= m2 -> M1 <= M2 -> Mlet m1 M1 <= Mlet m2 M2.
Hint Resolve Mlet_le_compat.

Add Parametric Morphism (A B : Type) : (Mlet (A:=A) (B:=B))
with signature Ole ==> Ole ==> Ole
as Mlet_le_morphism.
Save.

Add Parametric Morphism (A B : Type) : (Mlet (A:=A) (B:=B))
with signature Ole ==> (@pointwise_relation A (distr B) (@Ole _ _)) ==> Ole
as Mlet_le_pointwise_morphism.
Save.

Instance Mlet_mon2 : forall (A B : Type), monotonic2 (@Mlet A B).
Save.

Definition MLet (A B : Type) : distr A -m> (A -> distr B) -m> distr B
:= mon2 (@Mlet A B).

Lemma MLet_simpl0 : forall (A B:Type) (m:distr A) (M:A -> distr B),
MLet A B m M = Mlet m M.

Lemma MLet_simpl : forall (A B:Type) (m:distr A) (M:A -> distr B)(f:B -> U),
μ (MLet A B m M) f = μ m (fun x => μ (M x) f).

Lemma Mlet_eq_compat : forall (A B : Type) (m1 m2:distr A) (M1 M2 : A -> distr B),
m1 == m2 -> M1==M2 -> Mlet m1 M1 == Mlet m2 M2.
Hint Resolve Mlet_eq_compat.

Add Parametric Morphism (A B : Type) : (Mlet (A:=A) (B:=B))
with signature Oeq ==> Oeq ==> Oeq
as Mlet_eq_morphism.
Save.

Add Parametric Morphism (A B : Type) : (Mlet (A:=A) (B:=B))
with signature Oeq ==> (@pointwise_relation A (distr B) (@Oeq _ _)) ==> Oeq
as Mlet_Oeq_pointwise_morphism.
Save.

Lemma mu_le_compat : forall (A:Type) (m1 m2:distr A),
m1 <= m2 -> forall f g : A -> U, f <= g -> μ m1 f <= μ m2 g.

Lemma mu_eq_compat : forall (A:Type) (m1 m2:distr A),
m1 == m2 -> forall f g : A -> U, f == g -> μ m1 f == μ m2 g.
Hint Immediate mu_le_compat mu_eq_compat.

Add Parametric Morphism (A : Type) : (μ (A:=A))
with signature Ole ==> Ole
as mu_le_morphism.
Save.

Add Parametric Morphism (A : Type) : (μ (A:=A))
with signature Oeq ==> Oeq
as mu_eq_morphism.
Save.

Add Parametric Morphism (A:Type) (a:distr A) : (@μ A a)
with signature (@pointwise_relation A U (@eq _) ==> Oeq) as mu_distr_eq_morphism.
Save.

Add Parametric Morphism (A:Type) (a:distr A) : (@μ A a)
with signature (@pointwise_relation A U (@Oeq _ _) ==> Oeq) as mu_distr_Oeq_morphism.
Save.

Add Parametric Morphism (A:Type) (a:distr A) : (@μ A a)
with signature (@pointwise_relation _ _ (@Ole _ _) ==> Ole) as mu_distr_le_morphism.
Save.

Add Parametric Morphism (A B:Type) : (@Mlet A B)
with signature (Ole ==> @pointwise_relation _ _ (@Ole _ _) ==> Ole) as mlet_distr_le_morphism.
Save.

Add Parametric Morphism (A B:Type) : (@Mlet A B)
with signature (Oeq ==> @pointwise_relation _ _ (@Oeq _ _) ==> Oeq) as mlet_distr_eq_morphism.
Save.

Lemma Mlet_unit : forall (A B:Type) (x:A) (m:A -> distr B), Mlet (Munit x) m == m x.

Lemma Mlet_ext : forall (A:Type) (m:distr A), Mlet m (fun x => Munit x) == m.

Lemma Mlet_assoc : forall (A B C:Type) (m1: distr A) (m2:A -> distr B) (m3:B -> distr C),
Mlet (Mlet m1 m2) m3 == Mlet m1 (fun x:A => Mlet (m2 x) m3).

Lemma let_indep : forall (A B:Type) (m1:distr A) (m2: distr B) (f:MF B),
μ m1 (fun _ => μ m2 f) == pone m1 * (μ m2 f).

## A specific distribution

Definition distr_null : forall A : Type, distr A.
Defined.

Lemma le_distr_null : forall (A:Type) (m : distr A), distr_null A <= m.
Hint Resolve le_distr_null.

## Scaling a distribution

Definition Mmult A (k:MF A) (m:M A) : M A.
Defined.

Lemma Mmult_simpl : forall A (k:MF A) (m:M A) f, Mmult k m f = m (fun x => k x * f x).

Lemma Mmult_stable_inv : forall A (k:MF A) (d:distr A), stable_inv (Mmult k (μ d)).

Lemma Mmult_stable_plus : forall A (k:MF A) (d:distr A), stable_plus (Mmult k (μ d)).

Lemma Mmult_stable_mult : forall A (k:MF A) (d:distr A), stable_mult (Mmult k (μ d)).

Lemma Mmult_continuous : forall A (k:MF A) (d:distr A), continuous (Mmult k (μ d)).

Definition distr_mult A (k:MF A) (d:distr A) : distr A.
Defined.

Lemma distr_mult_assoc : forall A (k1 k2:MF A) (d:distr A),
distr_mult k1 (distr_mult k2 d) == distr_mult (fun x => k1 x * k2 x) d.

Add Parametric Morphism (A B : Type) : (distr_mult (A:=A))
with signature Oeq ==> Oeq ==> Oeq
as distr_mult_eq_compat.
Save.

Scaling with a constant functions

Definition distr_scale A (k:U) (d:distr A) : distr A := distr_mult (fcte A k) d.

Lemma distr_scale_assoc : forall A (k1 k2:U) (d:distr A),
distr_scale k1 (distr_scale k2 d) == distr_scale (k1*k2) d.

Lemma distr_scale_simpl : forall A (k:U) (d:distr A)(f:MF A),
μ (distr_scale k d) f == k * μ d f.

Add Parametric Morphism A : (distr_scale (A:=A))
with signature Oeq ==> Oeq ==> Oeq
as distr_scale_eq_compat.
Save.
Hint Resolve distr_scale_eq_compat.

Lemma distr_scale_one : forall A (d:distr A), distr_scale 1 d == d.

Lemma distr_scale_zero : forall A (d:distr A), distr_scale 0 d == distr_null A.

Hint Resolve distr_scale_simpl distr_scale_assoc distr_scale_one distr_scale_zero.

Lemma let_indep_distr : forall (A B:Type) (m1:distr A) (m2: distr B),
Mlet m1 (fun _ => m2) == distr_scale (pone m1) m2.

Definition Mdiv A (k:U) (m:M A) : M A := UDiv k @ m.

Lemma Mdiv_simpl : forall A k (m:M A) f, Mdiv k m f = m f / k.

Lemma Mdiv_stable_inv : forall A (k:U) (d:distr A)(dk : μ d (fone A) <= k),
stable_inv (Mdiv k (μ d)).

Lemma Mdiv_stable_plus : forall A (k:U)(d:distr A), stable_plus (Mdiv k (μ d)).

Lemma Mdiv_stable_mult : forall A (k:U)(d:distr A)(dk : μ d (fone A) <= k),
stable_mult (Mdiv k (μ d)).

Lemma Mdiv_continuous : forall A (k:U)(d:distr A), continuous (Mdiv k (μ d)).

Definition distr_div A (k:U) (d:distr A) (dk : μ d (fone A) <= k)
: distr A.
Defined.

Lemma distr_div_simpl : forall A (k:U) (d:distr A) (dk : μ d (fone A) <= k) f,
μ (distr_div _ _ dk) f = μ d f / k.

## Conditional probabilities

Definition mcond A (m:M A) (f:MF A) : M A.
Defined.

Lemma mcond_simpl : forall A (m:M A) (f g: MF A),
mcond m f g = m (fconj f g) / m f.

Lemma mcond_stable_plus : forall A (m:distr A) (f: MF A), stable_plus (mcond (μ m) f).

Lemma mcond_stable_inv : forall A (m:distr A) (f: MF A), stable_inv (mcond (μ m) f).

Lemma mcond_stable_mult : forall A (m:distr A) (f: MF A), stable_mult (mcond (μ m) f).

Lemma mcond_continuous : forall A (m:distr A) (f: MF A), continuous (mcond (μ m) f).

Definition Mcond A (m:distr A) (f:MF A) : distr A :=
Build_distr (mcond_stable_inv m f) (mcond_stable_plus m f)
(mcond_stable_mult m f) (mcond_continuous m f).

Lemma Mcond_total : forall A (m:distr A) (f:MF A),
~ 0 == μ m f -> μ (Mcond m f) (fone A) == 1.

Lemma Mcond_simpl : forall A (m:distr A) (f g:MF A),
μ (Mcond m f) g = μ m (fconj f g) / μ m f.
Hint Resolve Mcond_simpl.

Lemma Mcond_zero_stable : forall A (m:distr A) (f g:MF A),
μ m g == 0 -> μ (Mcond m f) g == 0.

Lemma Mcond_null : forall A (m:distr A) (f g:MF A),
μ m f == 0 -> μ (Mcond m f) g == 0.

Lemma Mcond_conj : forall A (m:distr A) (f g:MF A),
μ m (fconj f g) == μ (Mcond m f) g * μ m f.

Lemma Mcond_decomp :
forall A (m:distr A) (f g:MF A),
μ m g == μ (Mcond m f) g * μ m f + μ (Mcond m (finv f)) g * μ m (finv f).

Lemma Mcond_bayes : forall A (m:distr A) (f g:MF A),
μ (Mcond m f) g == (μ (Mcond m g) f * μ m g) / (μ m f).

Lemma Mcond_mult : forall A (m:distr A) (f g h:MF A),
μ (Mcond m h) (fconj f g) == μ (Mcond m (fconj g h)) f * μ (Mcond m h) g.

Lemma Mcond_conj_simpl : forall A (m:distr A) (f g h:MF A),
(fconj f f == f) -> μ (Mcond m f) (fconj f g) == μ (Mcond m f) g.

Hint Resolve Mcond_mult Mcond_conj_simpl.

## Least upper bound of increasing sequences of distributions

Lemma M_lub_simpl : forall A (h: nat -m> M A) (f:MF A),
lub h f = lub (mshift h f).

Section Lubs.
Variable A : Type.

Definition Mu : distr A -m> M A.
Defined.

Lemma Mu_simpl : forall d f, Mu d f = μ d f.

Variable muf : nat -m> distr A.

Definition mu_lub: distr A.

Defined.

Lemma mu_lub_le : forall n:nat, muf n <= mu_lub.

Lemma mu_lub_sup : forall m: distr A, (forall n:nat, muf n <= m) -> mu_lub <= m.

End Lubs.
Hint Resolve mu_lub_le mu_lub_sup.

### Distributions seen as a Ccpo

Instance cdistr (A:Type) : cpo (distr A) :=
{D0 := distr_null A; lub:=mu_lub (A:=A)}.
Defined.

Lemma distr_lub_simpl : forall A (h : nat -m> distr A) (f:MF A),
μ (lub h) f = lub (mshift (Mu A @ h) f).
Hint Resolve distr_lub_simpl.

## Fixpoints

Definition Mfix (A B:Type) (F: (A -> distr B) -m> (A -> distr B))
: A -> distr B := fixp F.

Definition MFix (A B:Type) : ((A -> distr B) -m> (A -> distr B)) -m> (A -> distr B)
:= Fixp (A -> distr B).

Lemma Mfix_le : forall (A B:Type) (F: (A -> distr B) -m> (A -> distr B)) (x:A),
Mfix F x <= F (Mfix F) x.

Lemma Mfix_eq : forall (A B:Type) (F: (A -> distr B) -m> (A -> distr B)),
continuous F -> forall (x:A), Mfix F x == F (Mfix F) x.

Hint Resolve Mfix_le Mfix_eq.

Lemma Mfix_le_compat : forall (A B:Type) (F G : (A -> distr B)-m> (A -> distr B)),
F <= G -> Mfix F <= Mfix G.

Definition Miter (A B:Type) := Ccpo.iter (D:=A -> distr B).

Lemma Mfix_le_iter : forall (A B:Type) (F:(A -> distr B) -m> (A -> distr B)) (n:nat),
Miter F n <= Mfix F.

## Continuity

Section Continuity.

Variables A B:Type.

Instance Mlet_continuous_right
: forall a:distr A, continuous (D1:= A -> distr B) (D2:=distr B) (MLet A B a).
Save.

Lemma Mlet_continuous_left
: continuous (D1:=distr A) (D2:=(A -> distr B) -m> distr B) (MLet A B).

Hint Resolve Mlet_continuous_right Mlet_continuous_left.

Lemma Mlet_continuous2 : continuous2 (D1:=distr A) (D2:= A->distr B) (D3:=distr B) (MLet A B).
Hint Resolve Mlet_continuous2.

Lemma Mlet_lub_le : forall (mun:nat -m> distr A) (Mn : nat -m> (A -> distr B)),
Mlet (lub mun) (lub Mn) <= lub ((MLet A B @2 mun) Mn).

Lemma Mlet_lub_le_left : forall (mun:nat -m> distr A)
(M : A -> distr B),
Mlet (lub mun) M <= lub (mshift (MLet A B @ mun) M).

Lemma Mlet_lub_le_right : forall (m:distr A)
(Mun : nat -m> (A -> distr B)),
Mlet m (lub Mun) <= lub ((MLet A B m)@Mun).

Lemma Mlet_lub_fun_le_right : forall (m:distr A)
(Mun : A -> nat -m> distr B),
Mlet m (fun x => lub (Mun x)) <= lub ((MLet A B m)@(ishift Mun)).

Lemma Mfix_continuous :
forall (Fn : nat -m> (A -> distr B) -m> (A -> distr B)),
(forall n, continuous (Fn n)) ->
Mfix (lub Fn) <= lub (MFix A B @ Fn).

End Continuity.

## Exact probability : probability of full space is 1

Class Term A (m:distr A) := term_def : μ m (fone A) == 1.
Hint Resolve @term_def.

Lemma Mlet_indep_term : forall A B (d1:distr A) (d2:distr B) {T:Term d1},
Mlet d1 (fun _ => d2) == d2.
Hint Resolve Mlet_indep_term.

Lemma mu_stable_inv_term : forall A (d:distr A) {T:Term d} f, μ d (finv f) == [1-](μ d f).

Instance Munit_term : forall A (a:A), Term (Munit a).
Save.
Hint Resolve Munit_term.

Instance Mlet_term : forall A B (d1:distr A) (d2: A -> distr B)
{T1:Term d1} {T2:forall x, Term (d2 x)}, Term (Mlet d1 d2).
Save.
Hint Resolve Mlet_term.

Lemma fplusok_mu_term : forall (A B:Type) (d:distr B) (f f':A -> MF B) {T:Term d},
(forall x:A, fplusok (f x) (f' x)) ->
fplusok (fun x : A => μ d (f x)) (fun x : A => μ d (f' x)).

## distribution for flip

The distribution associated to flip () is f --> [1/2] (f true) + [1/2] (f false)

Definition flip : M bool := mon (fun (f : bool -> U) => [1/2] * (f true) + [1/2] * (f false)).

Lemma flip_stable_inv : stable_inv flip.

Lemma flip_stable_plus : stable_plus flip.

Lemma flip_stable_mult : stable_mult flip.

Lemma flip_continuous : continuous flip.

Lemma flip_true : flip B2U == [1/2].

Lemma flip_false : flip NB2U == [1/2].

Hint Resolve flip_true flip_false.

Definition Flip : distr bool.
Defined.

Lemma Flip_simpl : forall f, μ Flip f = [1/2] * (f true) + [1/2] * (f false).

Instance flip_term : Term Flip.
Save.
Hint Resolve flip_term.

## Uniform distribution beween 0 and n

Require Arith.

### Definition of fnth

fnth n k is defined as [1/]1+n

Definition fnth (n:nat) : nat -> U := fun k => [1/]1+n.

### Basic properties of fnth

Lemma Unth_eq : forall n, Unth n == [1-] (sigma (fnth n) n).
Hint Resolve Unth_eq.

Lemma sigma_fnth_one : forall n, sigma (fnth n) (S n) == 1.
Hint Resolve sigma_fnth_one.

Lemma Unth_inv_eq : forall n, [1-] ([1/]1+n) == sigma (fnth n) n.

Lemma sigma_fnth_sup : forall n m, (m > n) -> sigma (fnth n) m == sigma (fnth n) (S n).

Lemma sigma_fnth_le : forall n m, (sigma (fnth n) m) <= (sigma (fnth n) (S n)).

Hint Resolve sigma_fnth_le.

fnth is a retract
Lemma fnth_retract : forall n:nat,(retract (fnth n) (S n)).

Implicit Arguments fnth_retract [].

## Distributions and general summations

Definition sigma_fun A (f:nat -> MF A) (n:nat) : MF A := fun x => sigma (fun k => f k x) n.
Definition serie_fun A (f:nat -> MF A) : MF A := fun x => serie (fun k => f k x).

Definition Sigma_fun A (f:nat -> MF A) : nat -m> MF A :=
ishift (fun x => Sigma (fun k => f k x)).

Lemma Sigma_fun_simpl : forall A (f:nat -> MF A) (n:nat),
Sigma_fun f n = sigma_fun f n.

Lemma serie_fun_lub_sigma_fun : forall A (f:nat -> MF A),
serie_fun f == lub (Sigma_fun f).
Hint Resolve serie_fun_lub_sigma_fun.

Lemma sigma_fun_0 : forall A (f:nat -> MF A), sigma_fun f 0 == fzero A.

Lemma sigma_fun_S : forall A (f:nat->MF A) (n:nat),
sigma_fun f (S n) == fplus (f n) (sigma_fun f n).

Lemma mu_sigma_le : forall A (d:distr A) (f:nat -> MF A) (n:nat),
μ d (sigma_fun f n) <= sigma (fun k => μ d (f k)) n.

Lemma retract_fplusok : forall A (f:nat -> MF A) (n:nat),
(forall x, retract (fun k => f k x) n) ->
forall k, (k < n)%nat -> fplusok (f k) (sigma_fun f k).

Lemma mu_sigma_eq : forall A (d:distr A) (f:nat -> MF A) (n:nat),
(forall x, retract (fun k => f k x) n) ->
μ d (sigma_fun f n) == sigma (fun k => μ d (f k)) n.

Lemma mu_serie_le : forall A (d:distr A) (f:nat -> MF A),
μ d (serie_fun f) <= serie (fun k => μ d (f k)).

Lemma mu_serie_eq : forall A (d:distr A) (f:nat -> MF A),
(forall x, wretract (fun k => f k x)) ->
μ d (serie_fun f) == serie (fun k => μ d (f k)).

Lemma wretract_fplusok : forall A (f:nat -> MF A),
(forall x, wretract (fun k => f k x)) ->
forall k, fplusok (f k) (sigma_fun f k).

## Discrete distributions

Instance discrete_mon : forall A (c : nat -> U) (p : nat -> A),
monotonic (fun f : A -> U => serie (fun k => c k * f (p k))).
Save.

Definition discrete A (c : nat -> U) (p : nat -> A) : M A :=
mon (fun f : A -> U => serie (fun k => c k * f (p k))).

Lemma discrete_simpl : forall A (c : nat -> U) (p : nat -> A) f,
discrete c p f = serie (fun k => c k * f (p k)).

Lemma discrete_stable_inv : forall A (c : nat -> U) (p : nat -> A),
wretract c -> stable_inv (discrete c p).

Lemma discrete_stable_plus : forall A (c : nat -> U) (p : nat -> A),
stable_plus (discrete c p).

Lemma discrete_stable_mult : forall A (c : nat -> U) (p : nat -> A),
wretract c -> stable_mult (discrete c p).

Lemma discrete_continuous : forall A (c : nat -> U) (p : nat -> A),
continuous (discrete c p).

Record discr (A:Type) : Type :=
{coeff : nat -> U; coeff_retr : wretract coeff; points : nat -> A}.
Hint Resolve coeff_retr.

Definition Discrete : forall A, discr A -> distr A.
Defined.

Lemma Discrete_simpl : forall A (d:discr A),
μ (Discrete d) = discrete (coeff d) (points d).

Definition is_discrete (A:Type) (m: distr A) :=
exists d : discr A, m == Discrete d.

### Distribution for randomn

The distribution associated to random n is f --> sigma (i=0..n) [1]1+n (f i) we cannot factorize [1/]1+n because of possible overflow

Instance random_mon : forall n, monotonic (fun (f:MF nat) => sigma (fun k => Unth n * f k) (S n)).
Save.

Definition random (n:nat):M nat := mon (fun (f:MF nat) => sigma (fun k => Unth n * f k) (S n)).

Lemma random_simpl : forall n (f : MF nat),
random n f = sigma (fun k => Unth n * f k) (S n).

### Properties of random

Lemma random_stable_inv : forall n, stable_inv (random n).

Lemma random_stable_plus : forall n, stable_plus (random n).

Lemma random_stable_mult : forall n, stable_mult (random n).

Lemma random_continuous : forall n, continuous (random n).

Definition Random (n:nat) : distr nat.
Defined.

Lemma Random_simpl : forall (n:nat), μ (Random n) = random n.

Instance Random_total : forall n : nat, Term (Random n).
Save.
Hint Resolve Random_total.

Lemma Random_inv : forall f n, μ (Random n) (finv f) == [1-] (μ (Random n) f).
Hint Resolve Random_inv.

## Tacticals

Ltac mu_plus d :=
match goal with
| |- context [fmont (μ d) (fun x => (Uplus (@?f x) (@?g x)))] =>
rewrite (mu_stable_plus d (f:=f) (g:=g))
end.

Ltac mu_mult d :=
match goal with
| |- context [fmont (μ d) (fun x => (Umult ?k (@?f x)))] =>
rewrite (mu_stable_mult d k f)
end.