Library ALEA.SProbas
Definition of (sub)distribution
Subdistributions are measure functions such that- mu (1-f) <= 1 - mu f
- f <= 1-g -> mu f + mu g <= mu (f+g)
- mu f & mu g <= mu (f & g) - [ mu (f+k) <= mu f + k ] - [ mu (k * f) = k * mu (f) ] - [ mu (lub f_n) <= lub mu (f_n) ]
Record sdistr (A:Type) : Type :=
{smu : M A;
smu_stable_inv : stable_inv smu;
smu_le_plus : le_plus smu;
smu_le_esp : le_esp smu;
smu_le_plus_cte : le_plus_cte smu;
smu_stable_mult : stable_mult smu;
smu_continuous : continuous smu}.
Hint Resolve smu_le_plus smu_stable_inv smu_le_esp smu_stable_mult
smu_continuous.
{smu : M A;
smu_stable_inv : stable_inv smu;
smu_le_plus : le_plus smu;
smu_le_esp : le_esp smu;
smu_le_plus_cte : le_plus_cte smu;
smu_stable_mult : stable_mult smu;
smu_continuous : continuous smu}.
Hint Resolve smu_le_plus smu_stable_inv smu_le_esp smu_stable_mult
smu_continuous.
Lemma smu_monotonic : forall (A : Type)(m: sdistr A), monotonic (smu m).
Hint Resolve smu_monotonic.
Implicit Arguments smu_monotonic [A].
Lemma smu_stable : forall (A : Type)(m: sdistr A), stable (smu m).
Hint Resolve smu_stable.
Implicit Arguments smu_stable [A].
Lemma smu_zero : forall (A : Type)(m: sdistr A), smu m (fzero A) == 0.
Hint Resolve smu_zero.
Lemma smu_stable_mult_right : forall (A : Type)(m:(sdistr A)) (c:U) (f : A -> U),
smu m (fun x => (f x) * c) == (smu m f) * c.
Lemma smu_le_minus_left : forall (A : Type)(m:sdistr A) (f g:A -> U),
smu m (fminus f g) <= smu m f.
Hint Resolve smu_le_minus_left.
Lemma smu_le_minus : forall (A:Type) (m:sdistr A)(f g: A -> U),
g <= f -> smu m (fminus f g) <= smu m f - smu m g.
Hint Resolve smu_le_minus.
Lemma smu_cte : forall (A : Type)(m:(sdistr A)) (c:U),
smu m (fcte A c) == c * smu m (fone A).
Hint Resolve smu_cte.
Lemma smu_cte_le : forall (A : Type)(m:(sdistr A)) (c:U),
smu m (fcte A c) <= c.
Lemma smu_cte_eq : forall (A : Type)(m:(sdistr A)) (c:U),
smu m (fone A) == 1 -> smu m (fcte A c) == c.
Hint Resolve smu_cte_le smu_cte_eq.
Lemma smu_le_minus_cte : forall (A:Type) (m:sdistr A)(f: A -> U) (k:U),
smu m f - k <= smu m (fminus f (fcte A k)).
Lemma smu_inv_le_minus :
forall (A:Type) (m:sdistr A)(f: A -> U), smu m (finv f) <= smu m (fone A) - smu m f.
Lemma smu_inv_minus_inv : forall (A:Type) (m:sdistr A)(f: A -> U),
smu m (finv f) + [1-](smu m (fone A)) <= [1-](smu m f).
Definition stable_plus_sdistr : forall A (m:M A),
stable_plus m -> stable_inv m -> stable_mult m -> continuous m -> sdistr A.
Defined.
Definition distr_sdistr : forall A, distr A -> sdistr A.
Defined.
Definition Sunit A (x:A) : sdistr A := distr_sdistr (Munit x).
Lemma Sunit_unit : forall A (x:A), smu (Sunit x) = unit x.
Lemma Sunit_simpl : forall A (x:A) (f : MF A), smu (Sunit x) f = f x.
Definition Slet : forall A B:Type, (sdistr A) -> (A -> sdistr B) -> sdistr B.
Defined.
Lemma Slet_star : forall (A B:Type) (m:sdistr A) (M : A -> sdistr B),
smu (Slet m M) = star (smu m) (fun x => smu (M x)).
Lemma Slet_simpl : forall A B (m:sdistr A) (M : A -> sdistr B) (f:MF B),
smu (Slet m M) f = smu m (fun x => smu (M x) f).
Non deterministic choice
Instance Osdistr (A : Type) : ord (sdistr A) :=
{ Ole := fun f g => smu f <= smu g;
Oeq := fun f g => smu f == smu g}.
Defined.
Lemma Sunit_compat : forall A (x y : A), x = y -> Sunit x == Sunit y.
Lemma Slet_compat : forall (A B : Type) (m1 m2:sdistr A) (M1 M2 : A-> sdistr B),
m1 == m2 -> M1 == M2 -> Slet m1 M1 == Slet m2 M2.
Lemma le_sdistr_gen : forall (A:Type) (m1 m2:sdistr A),
m1 <= m2 -> forall f g, f <= g -> smu m1 f <= smu m2 g.
Lemma Slet_unit : forall (A B:Type) (x:A) (m:A -> sdistr B), Slet (Sunit x) m == m x.
Lemma M_ext : forall (A:Type) (m:sdistr A), Slet m (fun x => Sunit x) == m.
Lemma Mcomp : forall (A B C:Type) (m1:(sdistr A)) (m2:A -> sdistr B) (m3:B -> sdistr C),
Slet (Slet m1 m2) m3 == Slet m1 (fun x:A => (Slet (m2 x) m3)).
Lemma Slet_le_compat : forall (A B:Type) (m1 m2: sdistr A) (f1 f2 : A -> sdistr B),
m1 <= m2 -> f1 <= f2 -> Slet m1 f1 <= Slet m2 f2.
Lemma M_ext : forall (A:Type) (m:sdistr A), Slet m (fun x => Sunit x) == m.
Lemma Mcomp : forall (A B C:Type) (m1:(sdistr A)) (m2:A -> sdistr B) (m3:B -> sdistr C),
Slet (Slet m1 m2) m3 == Slet m1 (fun x:A => (Slet (m2 x) m3)).
Lemma Slet_le_compat : forall (A B:Type) (m1 m2: sdistr A) (f1 f2 : A -> sdistr B),
m1 <= m2 -> f1 <= f2 -> Slet m1 f1 <= Slet m2 f2.
Definition sdistr_null : forall A : Type, sdistr A.
Defined.
Lemma le_sdistr_null : forall (A:Type) (m : sdistr A), sdistr_null A <= m.
Hint Resolve le_sdistr_null.
Defined.
Lemma le_sdistr_null : forall (A:Type) (m : sdistr A), sdistr_null A <= m.
Hint Resolve le_sdistr_null.
Section Lubs.
Variable A : Type.
Definition Smu : sdistr A -m> M A.
Defined.
Lemma Smu_simpl : forall d f, Smu d f = smu d f.
Variable smuf : nat -m> sdistr A.
Definition smu_lub: sdistr A.
Defined.
Lemma smu_lub_simpl : smu smu_lub = lub (Smu @ smuf).
Lemma smu_lub_le : forall n:nat, smuf n <= smu_lub.
Lemma smu_lub_sup : forall m:sdistr A, (forall n:nat, smuf n <= m) -> smu_lub <= m.
End Lubs.
Variable A : Type.
Definition Smu : sdistr A -m> M A.
Defined.
Lemma Smu_simpl : forall d f, Smu d f = smu d f.
Variable smuf : nat -m> sdistr A.
Definition smu_lub: sdistr A.
Defined.
Lemma smu_lub_simpl : smu smu_lub = lub (Smu @ smuf).
Lemma smu_lub_le : forall n:nat, smuf n <= smu_lub.
Lemma smu_lub_sup : forall m:sdistr A, (forall n:nat, smuf n <= m) -> smu_lub <= m.
End Lubs.