Module FormalML.ProbTheory.Event

Require Import Program.Basics.
Require Import Classical.
Require Import QArith Coq.Reals.Rbase Coq.Reals.RList.
Require Import Coq.Reals.Rfunctions.
Require Import Coq.Reals.Rprod Coq.Reals.ROrderedType.
Require Import Ranalysis_reg utils.Finite.
Require Import Coquelicot.Coquelicot.
Require Import Lia Lra.
Require Import Reals.Integration.
Require Import Rtrigo_def.
Require Import List.
Require Finite.

Require Import Program.Basics.
Require Import Coq.Reals.Rbase.
Require Import Coq.Reals.Rfunctions.
Require Import Coq.Reals.RiemannInt.
Require ClassicalDescription.

Require Import Lra Lia.
Require Import List Permutation.

Require Import Morphisms EquivDec.

Require Import Classical ClassicalFacts.
Require Ensembles.

Require Import Utils DVector.
Import ListNotations.

Set Bullet Behavior "Strict Subproofs".

Declare Scope prob.

Section pre_ev.
  Definition pre_event T := T -> Prop.

  Definition pre_event_sub {T} (A B:pre_event T) := forall x, A x -> B x.
  Definition pre_event_equiv {T} (A B:pre_event T) := forall x, A x <-> B x.
  
  Global Instance pre_event_equiv_equiv {T} : Equivalence (@pre_event_equiv T).

  Global Instance pre_event_equiv_sub {T} : subrelation pre_event_equiv (@pre_event_sub T).

  Global Instance pre_event_sub_pre {T} : PreOrder (@pre_event_sub T).

  Global Instance pre_event_sub_part {T} : PartialOrder pre_event_equiv (@pre_event_sub T).

  Definition pre_Ω {T} : pre_event T
    := fun x: T => True.

  Definition pre_event_none {T} : pre_event T
    := fun x: T => False.

  Definition pre_event_singleton {T} (m:T) : pre_event T
    := fun x => x=m.
  
  Definition pre_event_union {T} (A B:pre_event T) : pre_event T
    := fun x:T => A x \/ B x.
  
  Definition pre_event_inter {T} (A B:pre_event T) : pre_event T
    := fun x:T => A x /\ B x.
  
  Definition pre_event_complement {T} (A:pre_event T) : pre_event T
    := fun x:T => not (A x).

  Definition pre_event_diff {T} (A B:pre_event T) : pre_event T
    := fun x:T => A x /\ not (B x).

  Definition pre_event_lem {T} (A:pre_event T) : Prop
    := forall x, A x \/ ~ A x.

  Definition pre_event_disjoint {T} (A B:pre_event T) : Prop
    := forall x, A x -> B x -> False.

  Local Notation "∅" := pre_event_none : prob.
  Local Notation "a ∪ b" := (pre_event_union a b) (at level 50) : prob.
  Local Notation "a ∩ b" := (pre_event_inter a b) (at level 50) : prob.
  Local Notation "¬ a" := (pre_event_complement a) (at level 20) : prob.
  Local Notation "a \ b" := (pre_event_diff a b) (at level 50) : prob.
  Local Notation "a ≤ b" := (pre_event_sub a b) (at level 70) : prob.

  Local Open Scope prob.

  Global Instance pre_event_disjoint_symm {T}: Symmetric (@pre_event_disjoint T).
  
  Global Instance pre_event_union_proper {T} :
    Proper (pre_event_equiv ==> pre_event_equiv ==> pre_event_equiv) (@pre_event_union T).

  Global Instance pre_event_inter_proper {T} :
    Proper (pre_event_equiv ==> pre_event_equiv ==> pre_event_equiv) (@pre_event_inter T).

  Global Instance pre_event_complement_proper {T} :
    Proper (pre_event_equiv ==> pre_event_equiv) (@pre_event_complement T).

  Global Instance pre_event_diff_proper {T} :
    Proper (pre_event_equiv ==> pre_event_equiv ==> pre_event_equiv) (@pre_event_diff T).

  Global Instance pre_event_union_sub_proper {T} :
    Proper (pre_event_sub ==> pre_event_sub ==> pre_event_sub) (@pre_event_union T).

  Global Instance pre_event_inter_sub_proper {T} :
    Proper (pre_event_sub ==> pre_event_sub ==> pre_event_sub) (@pre_event_inter T).

  Global Instance pre_event_complement_sub_proper {T} :
    Proper (pre_event_sub --> pre_event_sub) (@pre_event_complement T).

  Global Instance pre_event_diff_sub_proper {T} :
    Proper (pre_event_sub ==> pre_event_sub --> pre_event_sub) (@pre_event_diff T).

  Global Instance pre_event_disjoint_proper {T} :
    Proper (pre_event_sub --> pre_event_sub --> impl) (@pre_event_disjoint T).

  Global Instance pre_event_disjoint_eq_proper {A} : Proper (pre_event_equiv ==> pre_event_equiv ==> iff) (@pre_event_disjoint A).

  Lemma pre_event_diff_derived {T} (A B:T->Prop) : A \ B === A ∩ ¬B.

  Lemma pre_event_disjoint_inter {T} (A B:pre_event T) :
    pre_event_disjoint A B <-> A ∩ B === ∅.

  Lemma pre_event_disjoint_diff {T} (A B:pre_event T) : pre_event_disjoint A (B \ A).

  Hint Resolve pre_event_disjoint_diff : prob.

  Lemma pre_event_disjoint_complement {T} (A:pre_event T) : pre_event_disjoint A (¬ A).

  Hint Resolve pre_event_disjoint_complement : prob.

  Lemma pre_event_sub_true {T} (A:pre_event T) : A ≤ pre_Ω.

  Lemma pre_event_false_sub {T} (A:pre_event T) : ∅ ≤ A.

  Hint Resolve pre_event_sub_true pre_event_false_sub : prob.

  Lemma pre_event_sub_union_l {T} (A B:pre_event T) : A ≤ A ∪ B.

  Lemma pre_event_sub_union_r {T} (A B:pre_event T) : B ≤ A ∪ B.

  Hint Resolve pre_event_sub_union_l pre_event_sub_union_r : prob.

  Lemma pre_event_inter_sub_l {T} (A B:pre_event T) : A ∩ B ≤ A.

  Lemma pre_event_inter_sub_r {T} (A B:pre_event T) : A ∩ B ≤ B.

  Hint Resolve pre_event_inter_sub_l pre_event_inter_sub_r : prob.

  Lemma pre_event_union_true_l {T} (A:pre_event T) : pre_Ω ∪ A === pre_Ω.

  Lemma pre_event_union_true_r {T} (A:pre_event T) : A ∪ pre_Ω === pre_Ω.

  Hint Rewrite @pre_event_union_true_l @pre_event_union_true_r : prob.

  Lemma pre_event_union_false_l {T} (A:pre_event T) : ∅ ∪ A === A.

  Lemma pre_event_union_false_r {T} (A:pre_event T) : A ∪ ∅ === A.

  Hint Rewrite @pre_event_union_false_l @pre_event_union_false_r : prob.

  Lemma pre_event_union_complement {T} (A:pre_event T) :
    pre_event_lem A ->
    A ∪ ¬ A === pre_Ω.

  Lemma pre_event_inter_true_l {T} (A:pre_event T) : pre_Ω ∩ A === A.

  Lemma pre_event_inter_true_r {T} (A:pre_event T) : A ∩ pre_Ω === A.

  Hint Rewrite @pre_event_inter_true_l @pre_event_inter_true_r : prob.

  Lemma pre_event_inter_false_l {T} (A:pre_event T) : ∅ ∩ A === ∅.

  Lemma pre_event_inter_false_r {T} (A:pre_event T) : A ∩ ∅ === ∅.

  Hint Rewrite @pre_event_inter_false_l @pre_event_inter_false_r : prob.

  Lemma pre_event_inter_complement {T} (A:pre_event T) :
    A ∩ ¬ A === ∅.

  Hint Rewrite @pre_event_inter_complement : prob.

  Lemma pre_event_diff_true_l {T} (A:pre_event T) : pre_Ω \ A === ¬ A.

  Lemma pre_event_diff_true_r {T} (A:pre_event T) : A \ pre_Ω === ∅.

  Hint Rewrite @pre_event_diff_true_l @pre_event_diff_true_r : prob.

  Lemma pre_event_diff_false_l {T} (A:pre_event T) : ∅ \ A === ∅.

  Lemma pre_event_diff_false_r {T} (A:pre_event T) : A \ ∅ === A.

  Hint Rewrite @pre_event_diff_false_l @pre_event_diff_false_r : prob.


  Lemma pre_event_diff_sub {T:Type} (x y:pre_event T) : x \ y ≤ x.

  Hint Resolve pre_event_diff_sub : prob.

  Lemma pre_event_union_comm {T} (A B:pre_event T) : A ∪ B === B ∪ A.

  Lemma pre_event_inter_comm {T} (A B:pre_event T) : A ∩ B === B ∩ A.

  Lemma pre_event_union_self {T} (A:pre_event T) : A ∪ A === A.

  Lemma pre_event_inter_self {T} (A:pre_event T) : A ∩ A === A.

  Lemma pre_event_diff_self {T} (A:pre_event T) : A \ A === ∅.

  Lemma pre_event_union_not_self {T} (A:pre_event T) :
    pre_event_lem A ->
    A ∪ ¬ A === pre_Ω.

  Hint Rewrite @pre_event_union_self @pre_event_inter_self @pre_event_diff_self : prob.

  Lemma pre_event_complement_swap {T} (A B:pre_event T) :
    pre_event_lem A ->
    pre_event_lem B ->
    ¬ A === B <-> A === ¬ B.

  Lemma pre_event_not_not {T} (A:pre_event T) :
    pre_event_lem A ->
    ¬ (¬ A) === A.

  Lemma pre_event_not_all {T} :
    ¬ (@pre_Ω T) === ∅.

  Lemma pre_event_not_none {T} :
    ¬ ∅ === (@pre_Ω T).

  Hint Rewrite @pre_event_not_all @pre_event_not_none : prob.

  Lemma pre_event_inter_not_self {T} (A B:pre_event T) : A ∩ ¬ A === ∅.

  Lemma pre_event_union_assoc {T} (A B C:pre_event T) : A ∪ (B ∪ C) === (A ∪ B) ∪ C.

  Lemma pre_event_inter_assoc {T} (A B C:pre_event T) : A ∩ (B ∩ C) === (A ∩ B) ∩ C.

  Lemma pre_event_union_inter_distr {T} (A B C:pre_event T) : A ∪ (B ∩ C) === (A ∪ B) ∩ (A ∪ C).

  Lemma pre_event_inter_union_distr {T} (A B C:pre_event T) : A ∩ (B ∪ C) === (A ∩ B) ∪ (A ∩ C).

  Hint Rewrite @pre_event_union_self @pre_event_inter_self @pre_event_inter_not_self : prob.

  Lemma pre_event_union_diff {T:Type} (A B:pre_event T) :
    pre_event_lem A ->
    A ∪ (B \ A) === A ∪ B.

  Lemma pre_event_union_sub_l {T:Type} (A B:pre_event T) :
    B ≤ A -> A ∪ B === A.

  Lemma pre_event_union_sub_r {T:Type} (A B:pre_event T) :
    A ≤ B -> A ∪ B === B.

  Lemma pre_event_union_diff_sub {T:Type} (A B:pre_event T) :
    pre_event_lem A ->
    A ≤ B -> A ∪ (B \ A) === B.


  Lemma pre_event_complement_inj {A} (x y:pre_event A) :
    pre_event_equiv (pre_event_complement x) (pre_event_complement y) ->
    pre_event_equiv x y.


  Definition pre_collection_is_pairwise_disjoint {T: Type} (collection: nat -> pre_event T) :=
    forall n1 n2 : nat, n1 <> n2 ->
                 pre_event_disjoint (collection n1) (collection n2).

  Global Instance pre_collection_is_pairwise_disjoint_pre_event_sub_proper {T: Type}:
    Proper (pointwise_relation _ pre_event_sub --> impl) (@pre_collection_is_pairwise_disjoint T).

  Global Instance pre_collection_is_pairwise_disjoint_pre_event_equiv_proper {T: Type}:
    Proper (pointwise_relation _ pre_event_equiv --> iff) (@pre_collection_is_pairwise_disjoint T).

  Definition pre_union_of_collection {T: Type} (collection: nat -> pre_event T) : pre_event T :=
    fun t:T => (exists n, (collection n) t).

  Definition pre_inter_of_collection {T: Type} (collection: nat -> pre_event T) : pre_event T :=
    fun t:T => (forall n, (collection n) t).


  Global Instance pre_union_of_collection_proper {T:Type} : Proper (pointwise_relation _ pre_event_equiv ==> pre_event_equiv) (@pre_union_of_collection T).

  Global Instance pre_union_of_collection_sub_proper {T:Type} : Proper (pointwise_relation _ pre_event_sub ==> pre_event_sub) (@pre_union_of_collection T).

  Global Instance pre_inter_of_collection_proper {T:Type} : Proper (pointwise_relation _ pre_event_equiv ==> pre_event_equiv) (@pre_inter_of_collection T).

  Global Instance pre_inter_of_collection_sub_proper {T:Type} : Proper (pointwise_relation _ pre_event_sub ==> pre_event_sub) (@pre_inter_of_collection T).

  Lemma pre_union_of_collection_const {T:Type} (c:pre_event T) : pre_event_equiv (pre_union_of_collection (fun _ => c)) c.
  
  Hint Rewrite @pre_union_of_collection_const : prob.

  Lemma pre_collection_is_pairwise_disjoint_sub {T:Type} (coll:nat -> pre_event T) (f:pre_event T -> pre_event T):
    (forall a, f a ≤ a) ->
    pre_collection_is_pairwise_disjoint coll ->
    pre_collection_is_pairwise_disjoint (fun n => f (coll n)).

  Lemma pre_event_complement_union {T:Type} (E1 E2:pre_event T) :
    pre_event_equiv (pre_event_complement (pre_event_union E1 E2))
                    (pre_event_inter (pre_event_complement E1) (pre_event_complement E2)).

  Lemma pre_event_complement_inter {T:Type} (E1 E2:pre_event T) :
    pre_event_equiv (pre_event_complement (pre_event_inter E1 E2))
                    (pre_event_union (pre_event_complement E1) (pre_event_complement E2)).

  Lemma pre_event_complement_union_of_collection {T:Type} (E : nat -> pre_event T) :
    pre_event_equiv (pre_event_complement (pre_union_of_collection E))
                    (pre_inter_of_collection (fun n => pre_event_complement (E n))).

  Lemma pre_event_inter_diff' {T:Type} (a b c:pre_event T) :
    pre_event_equiv (pre_event_inter a (pre_event_diff b c))
                    (pre_event_diff (pre_event_inter a b) (pre_event_inter a c)).

  Lemma pre_event_inter_diff {T:Type} (a b c:pre_event T) :
    pre_event_equiv (pre_event_inter a (pre_event_diff b c))
                    (pre_event_diff (pre_event_inter a b) c).

  Lemma pre_event_inter_countable_union_distr {T} (A:pre_event T) (coll:nat->pre_event T) :
    A ∩ pre_union_of_collection coll === pre_union_of_collection (fun n => A ∩ (coll n)).

  Lemma pre_event_inter_countable_inter_distr {T} (A:pre_event T) (coll:nat->pre_event T) :
    A ∩ pre_inter_of_collection coll === pre_inter_of_collection (fun n => A ∩ (coll n)).

  Lemma pre_event_diff_countable_union_distr {T} (A:pre_event T) (coll:nat->pre_event T) :
    A \ pre_union_of_collection coll === pre_inter_of_collection (fun n => A \ (coll n)).

  Lemma pre_event_countable_union_diff_distr {T} (A:pre_event T) (coll:nat->pre_event T) :
    (pre_union_of_collection coll) \ A === pre_union_of_collection (fun n => (coll n) \ A).

  Definition pre_event_preimage {Ts: Type} {Td: Type}
             (X: Ts -> Td)
             (B: pre_event Td)
    := fun omega: Ts => B (X omega).

  Global Instance pre_event_preimage_proper {Ts: Type} {Td: Type} :
    Proper (rv_eq ==> pre_event_equiv ==> pre_event_equiv) (@pre_event_preimage Ts Td).

  Class SigmaAlgebra (T:Type) :=
    {
    sa_sigma : pre_event T -> Prop;
    
    sa_countable_union (collection: nat -> pre_event T) :
      (forall n, sa_sigma (collection n)) ->
      sa_sigma (pre_union_of_collection collection);
    
    sa_complement (A:pre_event T) :
      sa_sigma A -> sa_sigma (pre_event_complement A) ;
    
    sa_all : sa_sigma pre_Ω
                      
    }.

  Lemma sa_pre_dec {T} (A:pre_event T) : pre_event_lem A.

  Global Instance sa_proper {T} (s: SigmaAlgebra T) : Proper (pre_event_equiv ==> iff) sa_sigma.

  Hint Resolve sa_pre_dec : prob.

  Definition sa_sub {T} (s1 s2:SigmaAlgebra T) : Prop
    := pre_event_sub (sa_sigma (SigmaAlgebra := s1)) (sa_sigma (SigmaAlgebra := s2)).

  Definition sa_equiv {T} (s1 s2:SigmaAlgebra T) : Prop
    := pre_event_equiv (sa_sigma (SigmaAlgebra := s1)) (sa_sigma (SigmaAlgebra := s2)).

  Global Instance sa_equiv_equiv T : Equivalence (@sa_equiv T).

  Global Instance sa_equiv_sub {T} : subrelation sa_equiv (@sa_sub T).

  Global Instance sa_sub_pre {T} : PreOrder (@sa_sub T).

  Global Instance sa_sub_part {T} : PartialOrder sa_equiv (@sa_sub T).

  Lemma sa_equiv_subs {T} (s1 s2:SigmaAlgebra T)
    : sa_equiv s1 s2 <-> (sa_sub s1 s2 /\ sa_sub s2 s1).

  Lemma ps_pre_event_union_complement {T} {s : SigmaAlgebra T} (A:pre_event T) :
    sa_sigma A ->
    A ∪ ¬ A === pre_Ω.

  Lemma ps_pre_event_union_not_self {T} {s : SigmaAlgebra T} (A:pre_event T) :
    sa_sigma A ->
    A ∪ ¬ A === pre_Ω.

  Lemma ps_pre_event_union_diff {T:Type} {s : SigmaAlgebra T} (A B:pre_event T) : sa_sigma A ->
                                                                                  A ∪ (B \ A) === A ∪ B.

  Lemma ps_pre_event_union_diff_sub {T:Type} {s : SigmaAlgebra T} (A B:pre_event T) : sa_sigma A ->
                                                                                      A ≤ B -> A ∪ (B \ A) === B.

  Hint Resolve ps_pre_event_union_complement ps_pre_event_union_not_self ps_pre_event_union_diff ps_pre_event_union_diff_sub : prob.

  Lemma sa_notnot {T} {s: SigmaAlgebra T} (A:pre_event T) : sa_sigma A -> forall x, ~ ~ A x -> A x.

  Lemma sa_none {T} {s: SigmaAlgebra T} : sa_sigma (∅).

  Hint Resolve sa_all sa_none sa_complement : prob.

  Lemma sa_sigma_const {T} (s: SigmaAlgebra T) {P} (Plem:P\/~P) : sa_sigma (fun _ : T => P).

  Lemma sa_sigma_const_classic {T} (s: SigmaAlgebra T) P : sa_sigma (fun _ : T => P).

  Lemma sa_pre_countable_inter {T} {s: SigmaAlgebra T} (collection: nat -> pre_event T) :
    (forall n, sa_sigma (collection n)) ->
    sa_sigma (pre_inter_of_collection collection).

  Definition pre_list_collection {T} (l:list (pre_event T)) (d:pre_event T) : nat -> pre_event T
    := fun n => nth n l d.

  Definition pre_list_union {T} (l:list (pre_event T)) : pre_event T
    := fun x => exists a, In a l /\ a x.

  Definition pre_list_inter {T} (l:list (pre_event T)) : pre_event T
    := fun x => forall a, In a l -> a x.

  Lemma pre_event_inter_pre_list_union_distr {T} (A:pre_event T) (l: list (pre_event T)) :
    A ∩ pre_list_union l === pre_list_union (map (pre_event_inter A) l).

  Lemma pre_event_union_diff_distr {T} (A:pre_event T) (l: list (pre_event T)) :
    pre_list_union l \ A === pre_list_union (map (fun x => x \ A) l).

  Lemma pre_list_union_union {T} (l:list (pre_event T)) :
    pre_union_of_collection (pre_list_collection l ∅) === pre_list_union l.

  Lemma pre_list_inter_inter {T} (l:list (pre_event T)) :
    pre_inter_of_collection (pre_list_collection l pre_Ω) === pre_list_inter l.

  Lemma pre_list_union_nil {T:Type} :
    @pre_list_union T [] === ∅.

  Lemma pre_list_union_cons {T} (x1 : pre_event T) (l:list (pre_event T)):
    pre_list_union (x1::l) === x1 ∪ (pre_list_union l).

  Hint Rewrite @pre_list_union_nil @pre_list_union_cons : prob.

  Lemma pre_list_union_singleton {T} (En:pre_event T) :
    pre_list_union [En] === En.

  Hint Rewrite @pre_list_union_singleton : prob.

  Lemma pre_list_union_app {T} (l1 l2:list (pre_event T)):
    pre_list_union (l1 ++ l2) === (pre_list_union l1) ∪ (pre_list_union l2).

  Hint Rewrite @pre_list_union_app : prob.

  Lemma pre_list_union2 {T} (x1 x2 : pre_event T) :
    pre_list_union [x1 ; x2] === x1 ∪ x2.

  Lemma pre_list_inter_nil {T:Type} :
    @pre_list_inter T [] === pre_Ω.

  Lemma pre_list_inter_cons {T} (x1 : pre_event T) (l:list (pre_event T)):
    pre_list_inter (x1::l) === x1 ∩ (pre_list_inter l).

  Hint Rewrite @pre_list_inter_nil @pre_list_inter_cons : prob.

  Lemma pre_list_inter_singleton {T} (En:pre_event T) :
    pre_list_inter [En] === En.

  Hint Rewrite @pre_list_inter_singleton : prob.

  Lemma pre_list_inter_app {T} (l1 l2:list (pre_event T)):
    pre_list_inter (l1 ++ l2) === (pre_list_inter l1) ∩ (pre_list_inter l2).

  Hint Rewrite @pre_list_inter_app : prob.

  Lemma pre_list_inter2 {T} (x1 x2 : pre_event T) :
    pre_list_inter [x1 ; x2] === x1 ∩ x2.

  Lemma pre_event_complement_list_union {T:Type} (E:list (pre_event T)) :
    pre_event_equiv (pre_event_complement (pre_list_union E))
                    (pre_list_inter (map pre_event_complement E)).

  Lemma pre_event_complement_list_inter {T:Type} (E:list (pre_event T)) :
    pre_event_equiv (pre_event_complement (pre_list_inter E))
                    (pre_list_union (map pre_event_complement E)).

  Lemma pre_list_union_concat {T} (l:list (list (pre_event T))) :
    pre_event_equiv (pre_list_union (concat l)) (pre_list_union (map pre_list_union l)).

  Lemma pre_list_collection_disjoint {T} (l:list (pre_event T)) :
    ForallOrdPairs pre_event_disjoint l <->
    pre_collection_is_pairwise_disjoint (pre_list_collection l ∅).

  Lemma pre_list_collection_sigma {T} {s : SigmaAlgebra T} (l:list (pre_event T)) (d:pre_event T) :
    ((forall x : pre_event T, In x l -> sa_sigma x) /\ sa_sigma d) <->
    (forall n : nat, sa_sigma (pre_list_collection l d n)).

  Lemma sa_pre_list_union {T} {s: SigmaAlgebra T} (l:list (pre_event T)) :
    (forall x, In x l -> sa_sigma x) ->
    sa_sigma (pre_list_union l).

  Lemma sa_pre_list_inter {T} {s: SigmaAlgebra T} (l:list (pre_event T)) :
    (forall x, In x l -> sa_sigma x) ->
    sa_sigma (pre_list_inter l).

  Lemma sa_union {T} {s: SigmaAlgebra T} {A₁ A₂} :
    sa_sigma A₁ -> sa_sigma A₂ -> sa_sigma (A₁ ∪ A₂).

  Lemma sa_inter {T} {s: SigmaAlgebra T} {A₁ A₂} :
    sa_sigma A₁ -> sa_sigma A₂ -> sa_sigma (A₁ ∩ A₂).

  Hint Resolve sa_union sa_inter : prob.

  Lemma sa_diff {T} {s: SigmaAlgebra T} {A₁ A₂} :
    sa_sigma A₁ -> sa_sigma A₂ -> sa_sigma (A₁ \ A₂).

  Hint Resolve sa_diff : prob.

  Lemma pre_union_of_collection_sup {T} (coll:nat->pre_event T) n : (coll n) ≤ (pre_union_of_collection coll).

Lemma sa_countable_union_iso {T : Type} (SigmaAlgebra : SigmaAlgebra T) {Index: Type} {iso:Isomorphism Index nat}
      (collection : Index -> pre_event T) :
  (forall i, sa_sigma (collection i)) -> sa_sigma (fun omega => exists i:Index, collection i omega).

Lemma sa_pre_countable_inter_iso {T : Type} (SigmaAlgebra : SigmaAlgebra T) {Index: Type} {iso:Isomorphism Index nat}
      (collection : Index -> pre_event T) :
  (forall i, sa_sigma (collection i)) -> sa_sigma (fun omega => forall i:Index, collection i omega).
  
End pre_ev.

Section event.
  Context {T:Type}.

  Definition event (σ:SigmaAlgebra T) := {e : pre_event T | sa_sigma e}.

  Definition event_pre {σ:SigmaAlgebra T} : event σ -> (T->Prop)
    := fun e => proj1_sig e.

  Lemma sa_sigma_event_pre {σ : SigmaAlgebra T} (E:event σ): sa_sigma (event_pre E).

  Context {σ:SigmaAlgebra T}.
  
  Program Definition event_sub (x y:event σ) := pre_event_sub x y.

  Program Definition event_equiv (x y:event σ) := pre_event_equiv x y.
  
  Global Instance event_equiv_equiv : Equivalence event_equiv.

  Global Instance event_equiv_sub : subrelation event_equiv event_sub.

  Global Instance event_sub_pre : PreOrder event_sub.

  Global Instance event_sub_part : PartialOrder event_equiv event_sub.

  Definition Ω : event σ
    := exist _ _ sa_all.

  Definition event_none : event σ
    := exist _ _ sa_none.

  Program Definition event_singleton (m:T) : sa_sigma (pre_event_singleton m) -> event σ
    := fun sa => exist _ _ sa.
  
  Definition event_union (A B:event σ) : event σ
    := exist _ _ (sa_union (proj2_sig A) (proj2_sig B)).
  
  Definition event_inter (A B:event σ) : event σ
    := exist _ _ (sa_inter (proj2_sig A) (proj2_sig B)).
  
  Definition event_complement (A:event σ) : event σ
    := exist _ _ (sa_complement _ (proj2_sig A)).

  Definition event_diff (A B:event σ) : event σ
    := exist _ _ (sa_diff (proj2_sig A) (proj2_sig B)).

  Program Definition event_lem (A:event σ) : Prop
    := pre_event_lem A.

  Program Definition event_disjoint (A B:event σ) : Prop
    := pre_event_disjoint A B.

  Notation "∅" := event_none : prob.
  Notation "a ∪ b" := (event_union a b) (at level 50) : prob.
  Notation "a ∩ b" := (event_inter a b) (at level 50) : prob.
  Notation "¬ a" := (event_complement a) (at level 20) : prob.
  Notation "a \ b" := (event_diff a b) (at level 50) : prob.
  Notation "a ≤ b" := (event_sub a b) (at level 70) : prob.

  Local Open Scope prob.

  Global Instance event_union_proper :
    Proper (event_equiv ==> event_equiv ==> event_equiv) event_union.

  Global Instance event_inter_proper :
    Proper (event_equiv ==> event_equiv ==> event_equiv) event_inter.

  Global Instance event_complement_proper :
    Proper (event_equiv ==> event_equiv) event_complement.

  Global Instance event_diff_proper :
    Proper (event_equiv ==> event_equiv ==> event_equiv) event_diff.

  Global Instance event_union_sub_proper :
    Proper (event_sub ==> event_sub ==> event_sub) event_union.

  Global Instance event_inter_sub_proper :
    Proper (event_sub ==> event_sub ==> event_sub) event_inter.

  Global Instance event_complement_sub_proper :
    Proper (event_sub --> event_sub) event_complement.

  Global Instance event_diff_sub_proper :
    Proper (event_sub ==> event_sub --> event_sub) event_diff.

  Global Instance event_disjoint_proper :
    Proper (event_sub --> event_sub --> impl) event_disjoint.


  Lemma event_diff_derived (A B:event σ) : A \ B === A ∩ ¬B.

  Lemma event_disjoint_inter (A B:event σ) :
    event_disjoint A B <-> A ∩ B === ∅.

  Lemma event_disjoint_diff (A B:event σ) : event_disjoint A (B \ A).

  Hint Resolve event_disjoint_diff : prob.

  Lemma event_disjoint_complement (A:event σ) : event_disjoint A (¬ A).

  Hint Resolve event_disjoint_complement : prob.

  Global Instance event_disjoint_sym : Symmetric event_disjoint.

  Instance event_disjoint_proper' :
    Proper (event_equiv ==> event_equiv ==> impl) event_disjoint.

  Lemma event_sub_true (A:event σ) : A ≤ Ω.

  Lemma event_false_sub (A:event σ) : ∅ ≤ A.

  Hint Resolve event_sub_true event_false_sub : prob.

  Lemma event_sub_union_l (A B:event σ) : A ≤ A ∪ B.

  Lemma event_sub_union_r (A B:event σ) : B ≤ A ∪ B.

  Hint Resolve event_sub_union_l event_sub_union_r : prob.

  Lemma event_inter_sub_l (A B:event σ) : A ∩ B ≤ A.

  Lemma event_inter_sub_r (A B:event σ) : A ∩ B ≤ B.

  Hint Resolve event_inter_sub_l event_inter_sub_r : prob.

  Lemma event_union_true_l (A:event σ) : Ω ∪ A === Ω.

  Lemma event_union_true_r (A:event σ) : A ∪ Ω === Ω.

  Hint Rewrite @event_union_true_l @event_union_true_r : prob.

  Lemma event_union_false_l (A:event σ) : ∅ ∪ A === A.

  Lemma event_union_false_r (A:event σ) : A ∪ ∅ === A.

  Hint Rewrite @event_union_false_l @event_union_false_r : prob.

  Lemma event_union_complement (A:event σ) :
    event_lem A ->
    A ∪ ¬ A === Ω.

  Lemma event_inter_true_l (A:event σ) : Ω ∩ A === A.

  Lemma event_inter_true_r (A:event σ) : A ∩ Ω === A.

  Hint Rewrite @event_inter_true_l @event_inter_true_r : prob.

  Lemma event_inter_false_l (A:event σ) : ∅ ∩ A === ∅.

  Lemma event_inter_false_r (A:event σ) : A ∩ ∅ === ∅.

  Hint Rewrite @event_inter_false_l @event_inter_false_r : prob.

  Lemma event_inter_complement (A:event σ) :
    A ∩ ¬ A === ∅.

  Hint Rewrite @event_inter_complement : prob.

  Lemma event_diff_true_l (A:event σ) : Ω \ A === ¬ A.

  Lemma event_diff_true_r (A:event σ) : A \ Ω === ∅.

  Hint Rewrite @event_diff_true_l @event_diff_true_r : prob.

  Lemma event_diff_false_l (A:event σ) : ∅ \ A === ∅.

  Lemma event_diff_false_r (A:event σ) : A \ ∅ === A.

  Hint Rewrite @event_diff_false_l @event_diff_false_r : prob.


  Lemma event_diff_sub (x y:event σ) : x \ y ≤ x.

  Hint Resolve event_diff_sub : prob.

  Lemma event_union_comm (A B:event σ) : A ∪ B === B ∪ A.

  Lemma event_inter_comm (A B:event σ) : A ∩ B === B ∩ A.

  Lemma event_union_self (A:event σ) : A ∪ A === A.

  Lemma event_inter_self (A:event σ) : A ∩ A === A.

  Lemma event_diff_self (A:event σ) : A \ A === ∅.

  Lemma event_union_not_self (A:event σ) :
    event_lem A ->
    A ∪ ¬ A === Ω.

  Hint Rewrite @event_union_self @event_inter_self @event_diff_self : prob.

  Lemma event_complement_swap (A B:event σ) :
    event_lem A ->
    event_lem B ->
    ¬ A === B <-> A === ¬ B.

  Lemma event_not_not (A:event σ) :
    event_lem A ->
    ¬ (¬ A) === A.

  Lemma event_not_all :
    ¬ Ω === ∅.

  Lemma event_not_none :
    ¬ ∅ === Ω.

  Hint Rewrite @event_not_all @event_not_none : prob.

  Lemma event_inter_not_self (A B:event σ) : A ∩ ¬ A === ∅.

  Lemma event_union_assoc (A B C:event σ) : A ∪ (B ∪ C) === (A ∪ B) ∪ C.

  Lemma event_inter_assoc (A B C:event σ) : A ∩ (B ∩ C) === (A ∩ B) ∩ C.

  Lemma event_union_inter_distr (A B C:event σ) : A ∪ (B ∩ C) === (A ∪ B) ∩ (A ∪ C).

  Lemma event_inter_union_distr (A B C:event σ) : A ∩ (B ∪ C) === (A ∩ B) ∪ (A ∩ C).

  Hint Rewrite @event_union_self @event_inter_self @event_inter_not_self : prob.

  Lemma event_union_diff (A B:event σ) :
    event_lem A ->
    A ∪ (B \ A) === A ∪ B.

  Lemma event_union_sub_l (A B:event σ) :
    B ≤ A -> A ∪ B === A.

  Lemma event_union_sub_r (A B:event σ) :
    A ≤ B -> A ∪ B === B.

  Lemma event_union_diff_sub (A B:event σ) :
    event_lem A ->
    A ≤ B -> A ∪ (B \ A) === B.


  Lemma event_complement_inj (x y:event σ) :
    event_equiv (event_complement x) (event_complement y) ->
    event_equiv x y.


  Program Definition collection_pre (collection: nat -> event σ) : nat -> pre_event T
    := fun n => collection n.

  Lemma sa_collection_pre (collection: nat -> event σ) n :
    sa_sigma (collection_pre collection n).
  
  Definition collection_is_pairwise_disjoint (collection: nat -> event σ) :=
    forall n1 n2 : nat, n1 <> n2 -> event_disjoint (collection n1) (collection n2).

  Lemma collection_is_pairwise_disjoint_pre collection :
    collection_is_pairwise_disjoint collection <->
    pre_collection_is_pairwise_disjoint (collection_pre collection).


  Global Instance collection_is_pairwise_disjoint_event_sub_proper :
    Proper (pointwise_relation _ event_sub --> impl) (@collection_is_pairwise_disjoint).

  Program Definition union_of_collection (collection: nat -> event σ) : event σ :=
    fun t => (exists n, (collection n) t).

  Program Definition inter_of_collection (collection: nat -> event σ) : event σ :=
    fun t => (forall n, (collection n) t).

  Global Instance union_of_collection_proper : Proper (pointwise_relation _ event_equiv ==> event_equiv) union_of_collection.

  Global Instance union_of_collection_sub_proper : Proper (pointwise_relation _ event_sub ==> event_sub) union_of_collection.

  Global Instance inter_of_collection_proper : Proper (pointwise_relation _ event_equiv ==> event_equiv) inter_of_collection.

  Global Instance inter_of_collection_sub_proper : Proper (pointwise_relation _ event_sub ==> event_sub) inter_of_collection.

  Program Definition union_of_collection_pre (collection: nat -> (event σ)) : event σ
    := exist _ (pre_union_of_collection (collection_pre collection)) _.

  Program Definition inter_of_collection_pre (collection: nat -> (event σ)) : event σ
    := exist _ (pre_inter_of_collection (collection_pre collection)) _.

  Lemma union_of_collection_as_pre (collection: nat -> (event σ)) :
    event_equiv (union_of_collection collection) (union_of_collection_pre collection).

  Lemma pre_of_union_of_collection (E:nat -> event σ) :
    pre_event_equiv (event_pre (union_of_collection E)) (pre_union_of_collection (fun n => event_pre (E n))).

  Lemma inter_of_collection_as_pre (collection: nat -> (event σ)) :
    event_equiv (inter_of_collection collection) (inter_of_collection_pre collection).

  Lemma union_of_collection_const (c:event σ) : event_equiv (union_of_collection (fun _ => c)) c.

  Lemma union_of_collection_complement (coll : nat -> event σ) :
    event_equiv (¬ union_of_collection coll) (inter_of_collection (fun n => ¬ (coll n))).

  Lemma inter_of_collection_complement (coll : nat -> event σ) :
    event_equiv (¬ inter_of_collection coll) (union_of_collection (fun n => ¬ (coll n))).

  Hint Rewrite @union_of_collection_const : prob.
  Hint Rewrite @union_of_collection_complement : prob.
  Hint Rewrite @inter_of_collection_complement : prob.

  Lemma collection_is_pairwise_disjoint_sub (coll:nat -> event σ) (f:event σ -> event σ):
    (forall a, f a ≤ a) ->
    collection_is_pairwise_disjoint coll ->
    collection_is_pairwise_disjoint (fun n => f (coll n)).

  Lemma event_inter_countable_union_distr (A:event σ) (coll:nat->event σ) :
    A ∩ union_of_collection coll === union_of_collection (fun n => A ∩ (coll n)).

  Lemma sa_dec (A:event σ) : event_lem A.

  Lemma ps_event_union_complement (A:event σ) :
    A ∪ ¬ A === Ω.

  Lemma ps_event_union_not_self (A:event σ) :
    A ∪ ¬ A === Ω.

  Lemma ps_event_union_diff {s : SigmaAlgebra T} (A B:event σ) :
    A ∪ (B \ A) === A ∪ B.

  Lemma ps_event_union_diff_sub (A B:event σ) :
    A ≤ B -> A ∪ (B \ A) === B.

  Hint Resolve ps_event_union_complement ps_event_union_not_self ps_event_union_diff ps_event_union_diff_sub : prob.

  Lemma event_notnot (A:event σ) : event_complement (event_complement A) === A.

  Hint Resolve sa_all sa_none sa_complement : prob.

  Definition event_const {P} : event σ
    := exist _ _ (sa_sigma_const σ (classic P)).

  Definition list_collection (l:list (event σ)) (d:event σ) : nat -> event σ
    := fun n => nth n l d.

  Lemma collection_pre_list_collection (l:list (event σ)) d :
    pointwise_relation _ pre_event_equiv
                       (collection_pre (list_collection l d)) (pre_list_collection (map (@proj1_sig _ _) l) (proj1_sig d)).

  Program Definition list_union (l:list (event σ)) : event σ
    := fun x => exists a, In a l /\ a x.

  Program Definition list_inter (l:list (event σ)) : event σ
    := fun x => forall a, In a l -> a x.

  Program Definition list_union_pre (l:list (event σ)) : event σ
    := exist _ (pre_list_union (map (@proj1_sig _ _) l)) _.

  Program Definition list_inter_pre (l:list (event σ)) : event σ
    := exist _ (pre_list_inter (map (@proj1_sig _ _) l)) _.

  Lemma list_union_as_pre (l:list (event σ)) :
    event_equiv (list_union l) (list_union_pre l).

  Lemma list_inter_as_pre (l:list (event σ)) :
    event_equiv (list_inter l) (list_inter_pre l).

  Lemma event_inter_list_union_distr (A:event σ) (l: list (event σ)) :
    A ∩ list_union l === list_union (map (event_inter A) l).

  Lemma list_union_union (l:list (event σ)) :
    union_of_collection (list_collection l ∅) === list_union l.

  Lemma list_inter_inter (l:list (event σ)) :
    inter_of_collection (list_collection l Ω) === list_inter l.

  Lemma list_union_nil :
    list_union [] === ∅.

  Lemma list_union_cons (x1 : event σ) (l:list (event σ)):
    list_union (x1::l) === x1 ∪ (list_union l).

  Hint Rewrite @list_union_nil @list_union_cons : prob.

  Lemma list_union_singleton (En:event σ) :
    list_union [En] === En.

  Hint Rewrite @list_union_singleton : prob.

  Lemma list_union_app (l1 l2:list (event σ)):
    list_union (l1 ++ l2) === (list_union l1) ∪ (list_union l2).

  Hint Rewrite @list_union_app : prob.

  Lemma list_union2 (x1 x2 : event σ) :
    list_union [x1 ; x2] === x1 ∪ x2.

  Lemma list_inter_nil :
    list_inter [] === Ω.

  Lemma list_inter_cons (x1 : event σ) (l:list (event σ)):
    list_inter (x1::l) === x1 ∩ (list_inter l).

  Hint Rewrite @list_inter_nil @list_inter_cons : prob.

  Lemma list_inter_singleton (En:event σ) :
    list_inter [En] === En.

  Hint Rewrite @list_inter_singleton : prob.

  Lemma list_inter_app (l1 l2:list (event σ)):
    list_inter (l1 ++ l2) === (list_inter l1) ∩ (list_inter l2).

  Hint Rewrite @list_inter_app : prob.

  Lemma list_inter2 (x1 x2 : event σ) :
    list_inter [x1 ; x2] === x1 ∩ x2.

  Lemma list_collection_disjoint (l:list (event σ)) :
    ForallOrdPairs event_disjoint l <->
    collection_is_pairwise_disjoint (list_collection l ∅).

  Lemma union_of_collection_sup (coll:nat->event σ) n : (coll n) ≤ (union_of_collection coll).

  Lemma list_union_cons_proper x y l1 l2 :
    event_equiv x y ->
    event_equiv (list_union l1) (list_union l2) ->
    event_equiv (list_union (x::l1)) (list_union (y::l2)).

  Global Instance list_union_perm :
    Proper (@Permutation _ ==> event_equiv) list_union.


  Global Instance list_union_Forall2_prop :
    Proper (Forall2 event_equiv ==> event_equiv) list_union.

  Lemma diff_inter_compl (A B : event σ) :
    (event_equiv (event_diff A B)
                 (event_inter A (event_complement B))).
  
  Lemma union_diff (A B : event σ) :
    event_equiv A (event_union (event_diff A B) (event_inter A B)).

  Lemma sub_diff_union (A B : event σ) :
    event_sub B A ->
    event_equiv A (event_union (event_diff A B) B).

  Lemma union_diff_inter (A:event σ) (E : nat -> event σ) :
        event_equiv (union_of_collection (fun n : nat => event_diff A (E n)))
                    (event_diff A (inter_of_collection E)).

  Section take.
  Definition collection_take {A} (En : nat -> A) (n:nat) := map En (seq 0 n).

  Lemma collection_take_length {A} (En : nat -> A) (n:nat) :
    length (collection_take En n) = n.

  Lemma collection_take_nth_in a En n x:
    proj1_sig (nth a (collection_take En n) event_none) x <->
    (a < n /\ proj1_sig (En a) x)%nat.

  Lemma In_collection_take {A} (En : nat -> A) a n:
    In a (collection_take En n) ->
    exists m, (m < n)%nat /\ a = En m.
  
  Lemma collection_take_Sn {A} n (En : nat -> A) :
    (collection_take En (S n)) = collection_take En n ++ (En n::nil).

  Lemma collection_take1 {A} (En : nat -> A) : collection_take En 1 = [En 0%nat].

  Lemma collection_take_sub (En:nat -> event σ) n :
    pointwise_relation _ event_sub (list_collection (collection_take En n) event_none) En.

  Lemma collection_take_preserves_disjoint En n:
    collection_is_pairwise_disjoint En ->
    ForallOrdPairs event_disjoint (collection_take En n).

  End take.

  Lemma event_union_list_union (c:nat->event σ) :
    event_equiv
      (union_of_collection
         (fun n => list_union
                  (collection_take c (S n))))
      (union_of_collection c).

  Lemma inter_of_collection_nested_collapse (P:nat -> event σ) (f:nat->nat->nat)
    (fsurj:forall x, exists a b, f a b = x) :
    event_equiv
      (inter_of_collection
         (fun n =>
            (inter_of_collection
               (fun m => P (f m n)))))
      (inter_of_collection P).

  Corollary inter_of_collection_nested_plus (P:nat -> event σ) :
    event_equiv
      (inter_of_collection
         (fun n =>
            (inter_of_collection
               (fun m => P (m + n)%nat))))
      (inter_of_collection P).

End event.


Definition event_preimage {Ts: Type} {Td: Type} {σ:SigmaAlgebra Td}
           (X: Ts -> Td)
           (B: event σ) : pre_event Ts
  := fun omega: Ts => proj1_sig B (X omega).

Global Instance event_preimage_proper{Ts: Type} {Td: Type} {σ:SigmaAlgebra Td} :
  Proper (rv_eq ==> event_equiv ==> pre_event_equiv) (@event_preimage Ts Td σ).

Section vec.


  Definition pre_bounded_inter_of_pre_collection {T} {n} (collection: forall i (pf:(i<n)%nat), pre_event T)
  : pre_event T
    := fun t => forall i pf, collection i pf t.

  Definition pre_bounded_inter_of_pre_collection_unbound {T} {n} (collection: forall i (pf:(i<n)%nat), pre_event T)
    : pre_event T
    := pre_inter_of_collection
         (fun i => match lt_dec i n with
                | left pf => collection i pf
                | right _ => pre_Ω
                end).

  Lemma pre_bounded_inter_of_pre_collection_unbound_eq {T} {n} (collection: forall i (pf:(i<n)%nat), pre_event T) :
    pre_bounded_inter_of_pre_collection collection === pre_bounded_inter_of_pre_collection_unbound collection.

  Lemma sa_pre_bounded_inter {T} {n} {σ: SigmaAlgebra T} (collection: forall i (pf:(i<n)%nat), pre_event T) :
    (forall n pf, sa_sigma (collection n pf)) ->
    sa_sigma (pre_bounded_inter_of_pre_collection collection).

  Definition pre_bounded_inter_of_collection {T} {n} {σ: SigmaAlgebra T} (collection: forall i (pf:(i<n)%nat), event σ)
  : pre_event T
    := fun t => forall i pf, proj1_sig (collection i pf) t.

  Definition bounded_inter_of_collection_unbound {T} {n} {σ: SigmaAlgebra T} (collection: forall i (pf:(i<n)%nat), event σ)
    : event σ
    := inter_of_collection
         (fun i => match lt_dec i n with
                | left pf => collection i pf
                | right _ => Ω
                end).

  Lemma pre_bounded_inter_of_collection_unbound_eq {T} {n} {σ: SigmaAlgebra T} (collection: forall i (pf:(i<n)%nat), event σ) :
    pre_bounded_inter_of_collection collection === proj1_sig (bounded_inter_of_collection_unbound collection).

  Lemma sa_bounded_inter {T} {n} {σ: SigmaAlgebra T} (collection: forall i (pf:(i<n)%nat), event σ) :
    sa_sigma (pre_bounded_inter_of_collection collection).

  Definition bounded_inter_of_collection {T} {n} {σ: SigmaAlgebra T} (collection: forall i (pf:(i<n)%nat), event σ)
    : event σ
    := exist _ _ (sa_bounded_inter collection).

  Lemma bounded_inter_of_collection_unbound_eq {T} {n} {σ: SigmaAlgebra T} (collection: forall i (pf:(i<n)%nat), event σ) :
    bounded_inter_of_collection collection === bounded_inter_of_collection_unbound collection.

End vec.

Section dec.

  Definition dec_pre_event {T} (P:T->Prop) := forall x, {P x} + {~ P x}.

  Context {T:Type} {σ:SigmaAlgebra T}.

  Definition dec_event (a:event σ) := forall x, {proj1_sig a x} + {~ proj1_sig a x}.

  Lemma dec_event_inter {a b:event σ} :
    dec_event a -> dec_event b -> dec_event (event_inter a b).

  Lemma dec_event_union {a b:event σ} :
    dec_event a -> dec_event b -> dec_event (event_union a b).
  
  Record dec_sa_event :=
    {
    dsa_event : event σ
    ; dsa_dec : dec_event dsa_event
    }.

  Definition dsa_equiv (x y : dec_sa_event) : Prop
    := event_equiv (dsa_event x) (dsa_event y).

  Global Instance dsa_equiv_equiv : Equivalence dsa_equiv.
  
  Program Definition dsa_Ω : dec_sa_event
    := {| dsa_event := Ω |}.


  Program Definition dsa_none : dec_sa_event
    := {| dsa_event := event_none |}.

  Definition dec_sa_event_inter (e1 e2 : dec_sa_event) : dec_sa_event :=
    {| dsa_event := (event_inter (dsa_event e1) (dsa_event e2))
       ; dsa_dec := dec_event_inter (dsa_dec e1) (dsa_dec e2)
    |} .

  Definition dec_sa_event_union (e1 e2 : dec_sa_event) : dec_sa_event :=
    {| dsa_event := (event_union (dsa_event e1) (dsa_event e2))
       ; dsa_dec := dec_event_union (dsa_dec e1) (dsa_dec e2)
    |} .
  
  Definition refine_dec_sa_event (e : dec_sa_event) (l : list (dec_sa_event)) :=
    map (fun e2 => dec_sa_event_inter e e2) l.

  Definition refine_dec_sa_partitions (l1 l2 : list dec_sa_event) :=
    flat_map (fun e1 => refine_dec_sa_event e1 l2) l1.

  Global Instance dec_sa_event_inter_proper :
    Proper (dsa_equiv ==> dsa_equiv ==> dsa_equiv) dec_sa_event_inter.

  Global Instance dec_sa_event_union_proper :
    Proper (dsa_equiv ==> dsa_equiv ==> dsa_equiv) dec_sa_event_union.

  Global Instance refine_dec_sa_event_proper :
    Proper (dsa_equiv ==> Forall2 dsa_equiv ==> Forall2 dsa_equiv) refine_dec_sa_event.

  Global Instance refine_dec_sa_partitions_proper :
    Proper (Forall2 dsa_equiv ==> Forall2 dsa_equiv ==> Forall2 dsa_equiv) refine_dec_sa_partitions.

  Lemma events_disjoint_refine_event (a : dec_sa_event) (l : list dec_sa_event) :
    ForallOrdPairs event_disjoint (map dsa_event l) ->
    ForallOrdPairs event_disjoint (map dsa_event (refine_dec_sa_event a l)).

  Lemma events_disjoint_refine (l1 l2 : list dec_sa_event) :
    ForallOrdPairs event_disjoint (map dsa_event l1) ->
    ForallOrdPairs event_disjoint (map dsa_event l2) ->
    ForallOrdPairs event_disjoint
                   (map dsa_event (flat_map (fun e1 : dec_sa_event => refine_dec_sa_event e1 l2) l1)).

  Lemma refine_dec_sa_partitions_symm (l1 l2 : list dec_sa_event) :
    exists l',
      Permutation (refine_dec_sa_partitions l1 l2) l' /\
      Forall2 dsa_equiv l' (refine_dec_sa_partitions l2 l1).
  
  Lemma event_equiv_list_union_refine_event a l :
    event_equiv (list_union (map dsa_event l)) Ω ->
    event_equiv (list_union (map dsa_event (refine_dec_sa_event a l))) (dsa_event a).

  Lemma event_equiv_list_union_refine_all l1 l2 :
    event_equiv (list_union (map dsa_event l2)) Ω ->
    event_equiv
      (list_union (map dsa_event (flat_map (fun e1 : dec_sa_event => refine_dec_sa_event e1 l2) l1)))
      (list_union (map dsa_event l1)).

  Definition classic_dec (P : pre_event T) : dec_pre_event P
    := (fun a => ClassicalDescription.excluded_middle_informative (P a)).

End dec.

Section sa_sub.

  Context {Ts:Type}
          {dom: SigmaAlgebra Ts}
          {dom2 : SigmaAlgebra Ts}
          (sub : sa_sub dom2 dom).
  
  Definition event_sa_sub
             (x:event dom2) : event dom
    := exist _ (event_pre x) (sub _ (proj2_sig x)).

  Global Instance event_sa_sub_equiv_proper :
    Proper (event_equiv ==> event_equiv) event_sa_sub.

  Lemma collection_is_pairwise_disjoint_sa_sub collection :
    collection_is_pairwise_disjoint collection ->
    collection_is_pairwise_disjoint (fun n : nat => event_sa_sub (collection n)).

  Lemma union_of_collection_sa_sub collection :
    event_equiv
      (event_sa_sub (union_of_collection collection))
      (union_of_collection (fun n : nat => event_sa_sub (collection n))).

End sa_sub.

Section pre_make_disjoint.
  Context {T:Type}.
  
  Definition make_pre_collection_disjoint (coll:nat->pre_event T) : nat -> pre_event T
    := fun x => pre_event_diff (coll x) ((pre_union_of_collection (fun y =>
                                                                  if lt_dec y x
                                                                  then coll y
                                                                  else pre_event_none))).

  Lemma make_pre_collection_disjoint_sub (En:nat -> pre_event T) n : pre_event_sub (make_pre_collection_disjoint En n) (En n).

  Lemma make_pre_collection_disjoint0 (En:nat -> pre_event T) :
    pre_event_equiv (make_pre_collection_disjoint En 0) (En 0%nat).

  Hint Rewrite @make_pre_collection_disjoint0 : prob.

  Lemma make_pre_collection_disjoint_in (coll:nat->pre_event T) (x:nat) (e:T) :
    make_pre_collection_disjoint coll x e <->
      (coll x) e /\ forall y, (y < x)%nat -> ~ (coll y) e.
  
  Lemma make_pre_collection_disjoint_disjoint (coll:nat->pre_event T) :
    pre_collection_is_pairwise_disjoint (make_pre_collection_disjoint coll).

  
  Lemma make_pre_collection_disjoint_union (coll:nat->pre_event T) :
    pre_event_equiv (pre_union_of_collection coll)
                    (pre_union_of_collection (make_pre_collection_disjoint coll)).

End pre_make_disjoint.


Section more_pre_props.
  Lemma pre_list_union_map_none {A B} (l:list A) :
    pre_event_equiv (pre_list_union (map (fun _ => pre_event_none) l)) (@pre_event_none B).

  Global Instance pre_list_union_sub_proper {A} :
    Proper (Forall2 pre_event_sub ==> pre_event_sub) (@pre_list_union A).

  Global Instance pre_list_inter_sub_proper {A} :
    Proper (Forall2 pre_event_sub ==> pre_event_sub) (@pre_list_inter A).

  Global Instance pre_list_union_proper {A} :
    Proper (Forall2 pre_event_equiv ==> pre_event_equiv) (@pre_list_union A).

  Global Instance pre_list_inter_proper {A} :
    Proper (Forall2 pre_event_equiv ==> pre_event_equiv) (@pre_list_inter A).

  Lemma pre_collection_take_nth_in {A} a (En:nat -> pre_event A) n x:
    nth a (collection_take En n) pre_event_none x <->
      (a < n /\ (En a) x)%nat.

  Lemma pre_collection_take_sub {A} (En:nat -> pre_event A) n :
    pointwise_relation _ pre_event_sub (pre_list_collection (collection_take En n) pre_event_none) En.

  Lemma pre_collection_take_preserves_disjoint {A} (En:nat -> pre_event A) n:
    pre_collection_is_pairwise_disjoint En ->
    ForallOrdPairs pre_event_disjoint (collection_take En n).

  Lemma pre_list_union_take_collection_sub {A} (E:nat->pre_event A) n :
    pre_event_sub (pre_list_union (collection_take E n)) (pre_union_of_collection E).

  Lemma pre_event_diff_diff_l {A} (a b c : pre_event A) :
    pre_event_equiv (pre_event_diff (pre_event_diff a b) c) (pre_event_diff a (pre_event_union b c)).

  Lemma pre_union_of_collection_lt_S {A} (E:nat->pre_event A) n :
    pre_event_equiv (pre_union_of_collection (fun y : nat => if lt_dec y (S n) then E y else pre_event_none))
                    (pre_event_union (E n) (pre_union_of_collection (fun y : nat => if lt_dec y n then E y else pre_event_none))).

  Lemma pre_collection_is_pairwise_disjoint_inter {T} (an:nat->pre_event T) (a:pre_event T) :
    pre_collection_is_pairwise_disjoint an ->
    pre_collection_is_pairwise_disjoint (fun n : nat => pre_event_inter a (an n)).

  Lemma pre_event_inter_sub_l_equiv {A:Type} (a b:pre_event A) :
    pre_event_sub a b ->
    pre_event_equiv (pre_event_inter a b) a.

  Lemma pre_list_disjoint_inter {A} (a:pre_event A) (l:list (pre_event A)) :
    ForallOrdPairs pre_event_disjoint l ->
    ForallOrdPairs pre_event_disjoint (map (pre_event_inter a) l).

End more_pre_props.

Coercion event_pre : event >-> Funclass.

Notation "∅" := event_none : prob.
Notation "a ∪ b" := (event_union a b) (at level 50) : prob.
Notation "a ∩ b" := (event_inter a b) (at level 50) : prob.
Notation "¬ a" := (event_complement a) (at level 20) : prob.
Notation "a \ b" := (event_diff a b) (at level 50) : prob.
Notation "a ≤ b" := (event_sub a b) (at level 70) : prob.

Hint Resolve event_disjoint_diff : prob.
Hint Resolve event_disjoint_complement : prob.
Hint Resolve event_sub_true event_false_sub : prob.
Hint Resolve event_sub_union_l event_sub_union_r : prob.
Hint Resolve event_inter_sub_l event_inter_sub_r : prob.
Hint Rewrite @event_union_true_l @event_union_true_r : prob.
Hint Rewrite @event_union_false_l @event_union_false_r : prob.
Hint Rewrite @event_inter_true_l @event_inter_true_r : prob.
Hint Rewrite @event_inter_false_l @event_inter_false_r : prob.
Hint Rewrite @event_inter_complement : prob.
Hint Rewrite @event_diff_true_l @event_diff_true_r : prob.
Hint Rewrite @event_diff_false_l @event_diff_false_r : prob.
Hint Resolve event_diff_sub : prob.
Hint Rewrite @event_union_self @event_inter_self @event_diff_self : prob.
Hint Rewrite @event_not_all @event_not_none : prob.
Hint Rewrite @event_union_self @event_inter_self @event_inter_not_self : prob.
Hint Rewrite @union_of_collection_const : prob.
Hint Resolve ps_event_union_complement ps_event_union_not_self ps_event_union_diff ps_event_union_diff_sub : prob.
Hint Resolve sa_all sa_none sa_complement : prob.
Hint Rewrite @list_union_nil @list_union_cons : prob.
Hint Rewrite @list_union_singleton : prob.
Hint Rewrite @list_union_app : prob.
Hint Rewrite @list_inter_nil @list_inter_cons : prob.
Hint Rewrite @list_inter_singleton : prob.
Hint Rewrite @list_inter_app : prob.