Library Probas

Probas.v: The monad for distributions

Require Export Monads.

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)

Record distr (A:Type) : Type :=
  {μ : M A;
   mu_stable_inv : stable_inv μ;
   mu_stable_plus : stable_plus μ;
   mu_stable_mult : stable_mult μ;
   mu_continuous : continuous μ}.

Hint Resolve mu_stable_plus mu_stable_inv mu_stable_mult mu_continuous.

Properties of measures

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

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

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

Lemma mu_zero_eq : ∀ (A : Type)(m: distr A) f,
   (∀ x, f x ≈ 0) → μ m f ≈ 0.

Lemma mu_one_inv : ∀ (A : Type)(m:distr A),
   μ m (fone A) ≈ 1 → ∀ f, μ m (finv f) ≈ [1-] (μ m f).
Hint Resolve mu_one_inv.

Lemma mu_fplusok : ∀ (A : Type)(m:distr A) f g, fplusok f g →
            μ m f ≤ [1-] μ m g.
Hint Resolve mu_fplusok.

Lemma mu_le_minus : ∀ (A : Type)(m:distr A) (f g:MF A),
     μ m (fminus f g) ≤ μ m f.
Hint Resolve mu_le_minus.

Lemma mu_le_plus : ∀ (A : Type)(m:distr A) (f g:MF A),
     μ m (fplus f g) ≤ μ m f + μ m g.
Hint Resolve mu_le_plus.

Lemma mu_cte : ∀ (A : Type)(m:(distr A)) (c:U),
   μ m (fcte A c) ≈ c * μ m (fone A).
Hint Resolve mu_cte.

Lemma mu_cte_le : ∀ (A : Type)(m:distr A) (c:U), μ m (fcte A c) ≤ c.

Lemma mu_cte_eq : ∀ (A : Type)(m:distr A) (c:U),
   μ m (fone A) ≈ 1 → μ m (fcte A c) ≈ c.

Hint Resolve mu_cte_le mu_cte_eq.

Lemma mu_stable_mult_right : ∀ (A : Type)(m:distr A) (c:U) (f : MF A),
   μ m (fun x ⇒ (f x) * c) ≈ (μ m f) * c.

Lemma mu_stable_minus : ∀ (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 :
∀ (A:Type) (m:distr A)(f: MF A), μ m (finv f) ≈ μ m (fone A) - μ m f.

Lemma mu_stable_le_minus : ∀ (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 : ∀ (A:Type) (m:distr A)(f: MF A),
     μ m (finv f) + [1-](μ m (fone A)) ≈ [1-](μ m f).

Lemma mu_le_esp_inv : ∀ (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 : ∀ (A:Type) (m:distr A)(f : MF A),
             μ m f ≤ [1-] μ m (finv f).
Hint Resolve mu_stable_inv_inv.

Lemma mu_stable_div : ∀ (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 : ∀ (A:Type) (m:distr A)(k:U)(f : MF A),
          ¬0 ≈ k → μ m (fdiv k f) ≤ μ m f / k.

Lemma mu_le_esp : ∀ (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 : ∀ (A:Type)(m:distr A)(f g:MF A),
   1 ≤ μ m f → μ m g ≈ μ m (fesp f g).

Lemma mu_esp_zero : ∀ (A:Type)(m:distr A)(f g:MF A),
   μ m (finv f) ≤ 0 → μ m g ≈ μ m (fesp f g).

Lemma mu_stable_mult2:
  ∀ (A : Type) (d : distr A), ∀ (k : U)
  (f : MF A), (μ d) (fun x ⇒ k * f x) ≈ k * (μ d) f.

Lemma mu_stable_plus2:
  ∀ (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 : ∀ A m, @μ A m (fun x ⇒ 0) ≈ 0.

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.

Monadic operators for distributions

Definition Munit : ∀ A:Type, A → distr A.
Defined.

Definition Mlet : ∀ A B:Type, distr A → (A → distr B) → distr B.
Defined.

Lemma Munit_simpl : ∀ (A:Type) (q:A → U) x, μ (Munit x) q = q x.

Lemma Mlet_simpl : ∀ (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 : ∀ A (x y : A), x = y → Munit x ≈ Munit y.

Lemma Mlet_le_compat : ∀ (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 : ∀ (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 : ∀ (A B:Type) (m:distr A) (M:A → distr B),
     MLet A B m M = Mlet m M.

Lemma MLet_simpl : ∀ (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 : ∀ (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 : ∀ (A:Type) (m1 m2:distr A),
  m1 ≤ m2 → ∀ f g : A → U, f ≤ g → μ m1 f ≤ μ m2 g.

Lemma mu_eq_compat : ∀ (A:Type) (m1 m2:distr A),
  m1 ≈ m2 → ∀ 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.

Properties of monadic operators

Lemma Mlet_unit : ∀ (A B:Type) (x:A) (m:A → distr B), Mlet (Munit x) m ≈ m x.

Lemma Mlet_ext : ∀ (A:Type) (m:distr A), Mlet m (fun x ⇒ Munit x) ≈ m.

Lemma Mlet_assoc : ∀ (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 : ∀ (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 : ∀ A : Type, distr A.
Defined.

Lemma le_distr_null : ∀ (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 : ∀ A (k:MF A) (m:M A) f, Mmult k m f = m (fun x ⇒ k x * f x).

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

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

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

Lemma Mmult_continuous : ∀ 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 : ∀ 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 : ∀ A (k1 k2:U) (d:distr A),
             distr_scale k1 (distr_scale k2 d) ≈ distr_scale (k1*k2) d.

Lemma distr_scale_simpl : ∀ 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 : ∀ A (d:distr A), distr_scale 1 d ≈ d.

Lemma distr_scale_zero : ∀ 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 : ∀ (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 : ∀ A k (m:M A) f, Mdiv k m f = m f / k.

Lemma Mdiv_stable_inv : ∀ A (k:U) (d:distr A)(dk : μ d (fone A) ≤ k),
                stable_inv (Mdiv k (μ d)).

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

Lemma Mdiv_stable_mult : ∀ A (k:U)(d:distr A)(dk : μ d (fone A) ≤ k),
                          stable_mult (Mdiv k (μ d)).

Lemma Mdiv_continuous : ∀ 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.

Conditional probabilities

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

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

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

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

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

Lemma mcond_continuous : ∀ 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 : ∀ A (m:distr A) (f:MF A),
          ¬ 0 ≈ μ m f → μ (Mcond m f) (fone A) ≈ 1.

Lemma Mcond_simpl : ∀ 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 : ∀ A (m:distr A) (f g:MF A),
      μ m g ≈ 0 → μ (Mcond m f) g ≈ 0.

Lemma Mcond_null : ∀ A (m:distr A) (f g:MF A),
      μ m f ≈ 0 → μ (Mcond m f) g ≈ 0.

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

Lemma Mcond_decomp :
    ∀ 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 : ∀ A (m:distr A) (f g:MF A),
          μ (Mcond m f) g ≈ (μ (Mcond m g) f * μ m g) / (μ m f).

Least upper bound of increasing sequences of distributions

Lemma M_lub_simpl : ∀ 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 : ∀ d f, Mu d f = μ d f.

Variable muf : nat -m > distr A.

Definition mu_lub: distr A.

Defined.

Lemma mu_lub_le : ∀ n:nat, muf n ≤ mu_lub.

Lemma mu_lub_sup : ∀ m: distr A, (∀ 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 : ∀ 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 : ∀ (A B:Type) (F: (A → distr B) -m > (A → distr B)) (x:A),
            Mfix F x ≤ F (Mfix F) x.

Lemma Mfix_eq : ∀ (A B:Type) (F: (A → distr B) -m > (A → distr B)),
continuous F → ∀ (x:A), Mfix F x ≈ F (Mfix F) x.

Hint Resolve Mfix_le Mfix_eq.

Lemma Mfix_le_compat : ∀ (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 : ∀ (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
    : ∀ 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 : ∀ (mun:nat -m > distr A) (Mn : nat -m > (A → distr B )),
            Mlet (lub mun) (lub Mn) ≤ lub ((MLet A B @² mun) Mn).

Lemma Mlet_lub_le_left : ∀ (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 : ∀ (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 : ∀ (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 :
     ∀ (Fn : nat -m > (A → distr B ) -m > (A → distr B )),
     (∀ n, continuous (Fn n)) →
      Mfix (lub Fn) ≤ lub (MFix A B @ Fn).

End Continuity.

distribution for flip

The distribution associated to flip () is f --> ½ (f true) + ½ (f false)

Definition flip : M bool := mon (fun (f : bool → U) ⇒ ½ * (f true ) + ½ * (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.

Definition ctrue : MF bool := fun (b:bool) ⇒ if b then 1 else 0.
Definition cfalse : MF bool := fun (b:bool) ⇒ if b then 0 else 1.

Lemma flip_ctrue : flip ctrue ≈ ½.

Lemma flip_cfalse : flip cfalse ≈ ½.

Hint Resolve flip_ctrue flip_cfalse.

Definition Flip : distr bool.
Defined.

Lemma Flip_simpl : ∀ f, μ Flip f = ½ * (f true ) + ½ * (f false ).

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 : ∀ n, Unth n ≈ [1-] (sigma (fnth n) n).
Hint Resolve Unth_eq.

Lemma sigma_fnth_one : ∀ n, sigma (fnth n) (S n) ≈ 1.
Hint Resolve sigma_fnth_one.

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

Lemma sigma_fnth_sup : ∀ n m, (m > n) → sigma (fnth n) m ≈ sigma (fnth n) (S n).

Lemma sigma_fnth_le : ∀ n m, (sigma (fnth n) m) ≤ (sigma (fnth n) (S n)).

Hint Resolve sigma_fnth_le.

fnth is a retract

Lemma fnth_retract : ∀ 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 : ∀ A (f:nat → MF A) (n:nat),
    Sigma_fun f n = sigma_fun f n.

Lemma serie_fun_lub_sigma_fun : ∀ A (f:nat → MF A),
     serie_fun f ≈ lub (Sigma_fun f).
Hint Resolve serie_fun_lub_sigma_fun.

Lemma sigma_fun_0 : ∀ A (f:nat → MF A), sigma_fun f 0 ≈ fzero A.

Lemma sigma_fun_S : ∀ A (f:nat→MF A) (n:nat),
      sigma_fun f (S n) ≈ fplus (f n) (sigma_fun f n).

Lemma mu_sigma_le : ∀ 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 : ∀ A (f:nat → MF A) (n:nat),
     (∀ x, retract (fun k ⇒ f k x) n) →
     ∀ k, (k < n)%nat → fplusok (f k) (sigma_fun f k).

Lemma mu_sigma_eq : ∀ A (d:distr A) (f:nat → MF A) (n:nat),
     (∀ x, retract (fun k ⇒ f k x) n) →
      μ d (sigma_fun f n) ≈ sigma (fun k ⇒ μ d (f k)) n.

Lemma mu_serie_le : ∀ A (d:distr A) (f:nat → MF A),
      μ d (serie_fun f) ≤ serie (fun k ⇒ μ d (f k)).

Lemma mu_serie_eq : ∀ A (d:distr A) (f:nat → MF A),
     (∀ x, wretract (fun k ⇒ f k x)) →
      μ d (serie_fun f) ≈ serie (fun k ⇒ μ d (f k)).

Lemma wretract_fplusok : ∀ A (f:nat → MF A),
     (∀ x, wretract (fun k ⇒ f k x)) →
     ∀ k, fplusok (f k) (sigma_fun f k).

Discrete distributions

Instance discrete_mon : ∀ 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 : ∀ A (c : nat → U) (p : nat → A) f,
     discrete c p f = serie (fun k ⇒ c k * f (p k)).

Lemma discrete_stable_inv : ∀ A (c : nat → U) (p : nat → A),
    wretract c → stable_inv (discrete c p).

Lemma discrete_stable_plus : ∀ A (c : nat → U) (p : nat → A),
    stable_plus (discrete c p).

Lemma discrete_stable_mult : ∀ A (c : nat → U) (p : nat → A),
    wretract c → stable_mult (discrete c p).

Lemma discrete_continuous : ∀ 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 : ∀ A, discr A → distr A.
Defined.

Lemma Discrete_simpl : ∀ 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 random n

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 : ∀ 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 : ∀ n (f : MF nat),
random n f = sigma (fun k ⇒ Unth n * f k) (S n).

Properties of random

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

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

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

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

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

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

Lemma Random_total : ∀ n : nat, μ (Random n) (fone nat) ≈ 1.
Hint Resolve Random_total.

Lemma Random_inv : ∀ 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.

Lemma fplusok_mu_fone : ∀ (A B:Type) (d:distr B) (f f':A → MF B),
  (∀ x:A, fplusok (f x) (f' x)) →
  μ d (fone _) ≈ 1 →
  fplusok (fun x : A ⇒ μ d (f x)) (fun x : A ⇒ μ d (f' x)).