Module FormalML.ProbTheory.Expectation

Require Import Reals.

Require Import Lra Lia.
Require Import List Permutation.
Require Import Morphisms EquivDec Program.
Require Import Coquelicot.Rbar Coquelicot.Lub Coquelicot.Lim_seq Coquelicot.Hierarchy.
Require Import Classical_Prop.
Require Import Classical.

Require Import Utils.
Require Import NumberIso.
Require Export Almost SimpleExpectation.

Import ListNotations.

Set Bullet Behavior "Strict Subproofs".

Section Expectation_sec.
  
  Context
    {Ts:Type}
    {dom: SigmaAlgebra Ts}
    {Prts: ProbSpace dom}.


  Definition BoundedNonnegativeFunction
             (rv_X1 rv_X2 : Ts -> R) :=
    NonnegativeFunction rv_X2 /\ rv_le rv_X2 rv_X1.

  Definition SimpleExpectationSup
             (E : forall
                 (rvx:Ts -> R)
                 (rv : RandomVariable dom borel_sa rvx)
                 (frf:FiniteRangeFunction rvx), Prop) : Rbar
    := Lub_Rbar (fun (x : R) =>
                   exists rvx rv frf,
                     E rvx rv frf /\ (SimpleExpectation rvx) = x).
  
  Definition NonnegExpectation
             (rv_X : Ts -> R)
             {pofrf:NonnegativeFunction rv_X} : Rbar :=
    (SimpleExpectationSup
       (fun
           (rvx2: Ts -> R)
           (rv2 : RandomVariable dom borel_sa rvx2)
           (frf2:FiniteRangeFunction rvx2) =>
           (BoundedNonnegativeFunction rv_X rvx2))).

  Lemma frf_NonnegExpectation
        (rv_X : Ts -> R)
        {rvx_rv : RandomVariable dom borel_sa rv_X}
        {pofrf:NonnegativeFunction rv_X}
        {frf:FiniteRangeFunction rv_X} :
    NonnegExpectation rv_X = SimpleExpectation rv_X.

  Global Instance bnnf_eq_proper : Proper (rv_eq ==> rv_eq ==> iff) BoundedNonnegativeFunction.
  
  Lemma NonnegExpectation_ext
        {rv_X1 rv_X2 : Ts -> R}
        (nnf1:NonnegativeFunction rv_X1)
        (nnf2:NonnegativeFunction rv_X2):
    rv_eq rv_X1 rv_X2 ->
    NonnegExpectation rv_X1 = NonnegExpectation rv_X2.

  Lemma NonnegExpectation_re
        {rv_X1 rv_X2 : Ts -> R}
        (eqq:rv_eq rv_X1 rv_X2)
        {nnf1:NonnegativeFunction rv_X1} :
    NonnegExpectation rv_X1 = NonnegExpectation rv_X2 (pofrf:=((proj1 (NonnegativeFunction_proper _ _ eqq)) nnf1)).

  Lemma NonnegExpectation_pf_irrel
        {rv_X: Ts -> R}
        (nnf1 nnf2:NonnegativeFunction rv_X) :
    NonnegExpectation rv_X (pofrf:=nnf1) = NonnegExpectation rv_X (pofrf:=nnf2).

  Definition Rbar_minus' (x y : Rbar) : option Rbar :=
    Rbar_plus' x (Rbar_opp y).
  
  Definition Expectation (rv_X : Ts -> R) : option Rbar :=
    Rbar_minus' (NonnegExpectation (pos_fun_part rv_X))
                (NonnegExpectation (neg_fun_part rv_X)).
  
  Lemma pos_fun_part_pos (rv_X : Ts -> R)
        {nnf : NonnegativeFunction rv_X} :
    rv_eq rv_X (pos_fun_part rv_X).

  Lemma neg_fun_part_pos (rv_X : Ts -> R)
        {nnf : NonnegativeFunction rv_X} :
    rv_eq (const 0) (neg_fun_part rv_X).

  Lemma Expectation_ext {rv_X1 rv_X2 : Ts -> R} :
    rv_eq rv_X1 rv_X2 ->
    Expectation rv_X1 = Expectation rv_X2.

  Global Instance Expectation_proper : Proper (rv_eq ==> eq) Expectation.
  
  Definition rvmean (rv_X:Ts -> R) : option Rbar :=
    Expectation rv_X.

  Definition variance (rv_X : Ts -> R) : option Rbar :=
    match rvmean rv_X with
    | Some (Finite m) => Expectation (rvsqr (rvminus rv_X (const m)))
    | _ => None
    end.

  Lemma lub_rbar_scale0 (c:posreal) (E : R -> Prop) (l:Rbar) :
    is_lub_Rbar E l -> is_lub_Rbar (fun x => E (x/c)) (Rbar_mult c l).
  
  Lemma lub_rbar_scale (c:posreal) (E : R -> Prop) :
    Lub_Rbar (fun x => E (x / c)) = Rbar_mult c (Lub_Rbar E).

  Global Instance rv_scale_le_proper (c:posreal) :
    Proper (rv_le ==> rv_le) (@rvscale Ts c).

  Lemma NonnegExpectation_scale (c: posreal)
        (rv_X : Ts -> R)
        {pofrf:NonnegativeFunction rv_X} :
    NonnegExpectation (rvscale c rv_X) =
    Rbar_mult c (NonnegExpectation rv_X).
  
  Lemma Expectation_scale_pos (c:posreal) (rv_X : Ts -> R) :
    NonnegExpectation (fun x : Ts => pos_fun_part (rvscale c rv_X) x) =
    Rbar_mult c (NonnegExpectation (pos_fun_part rv_X)).
  
  Lemma Expectation_scale_neg (c:posreal) (rv_X : Ts -> R) :
    NonnegExpectation (fun x : Ts => neg_fun_part (rvscale c rv_X) x) =
    Rbar_mult c (NonnegExpectation (neg_fun_part rv_X)).

  Lemma Rbar_mult_pos_pinf (c : posreal):
    Rbar_mult c p_infty = p_infty.

  Lemma Rbar_mult_pos_minf (c : posreal):
    Rbar_mult c m_infty = m_infty.

  Lemma scale_Rbar_plus (c : posreal) (x y : Rbar) :
    Rbar_plus' (Rbar_mult c x) (Rbar_mult c y) =
    match (Rbar_plus' x y) with
    | Some x' => Some (Rbar_mult c x')
    | None => None
    end.

  Lemma scale_Rbar_diff (c : posreal) (x y : Rbar) :
    Rbar_plus' (Rbar_mult c x) (Rbar_opp (Rbar_mult c y)) =
    match (Rbar_plus' x (Rbar_opp y)) with
    | Some x' => Some (Rbar_mult c x')
    | None => None
    end.

  Lemma Expectation_scale_posreal (c: posreal)
        (rv_X : Ts -> R) :
    let Ex_rv := Expectation rv_X in
    let Ex_c_rv := Expectation (rvscale c rv_X) in
    Ex_c_rv =
    match Ex_rv with
    | Some x => Some (Rbar_mult c x)
    | None => None
    end.
  
  Lemma Expectation_opp
        (rv_X : Ts -> R) :
    let Ex_rv := Expectation rv_X in
    let Ex_o_rv := Expectation (rvopp rv_X) in
    Ex_o_rv =
    match Ex_rv with
    | Some x => Some (Rbar_opp x)
    | None => None
    end.

  Lemma lub_Rbar_witness (E : R -> Prop) (l : Rbar) (b:R):
    is_lub_Rbar E l -> Rbar_lt b l ->
    exists (x:R), E x /\ x > b.

  Lemma lub_rbar_inf_witness (E : R -> Prop) :
    is_lub_Rbar E p_infty -> forall (b:R), exists (x:R), E x /\ x>b.

  Lemma lub_bar_nonempty (E : R -> Prop) :
    (exists (x:R), E x) -> ~(Lub_Rbar E = m_infty).

  Lemma lub_rbar_sum_inf1 (E1 E2 : R -> Prop) :
    (exists (x:R), E1 x) -> Lub_Rbar E2 = p_infty ->
    Rbar_plus (Lub_Rbar E1) (Lub_Rbar E2) = p_infty.

  Lemma lub_rbar_sum_inf2 (E1 E2 : R -> Prop) :
    (exists (x:R), E1 x) -> Lub_Rbar E2 = p_infty ->
    is_lub_Rbar (fun x => exists x1 x2, E1 x1 /\ E2 x2 /\ x = x1 + x2) p_infty.

  Lemma lub_rbar_sum_inf3 (E1 E2 : R -> Prop) :
    (exists (x:R), E2 x) -> Lub_Rbar E1 = p_infty ->
    is_lub_Rbar (fun x => exists x1 x2, E1 x1 /\ E2 x2 /\ x = x1 + x2) p_infty.

  Lemma lub_rbar_sum (E1 E2 : R -> Prop) :
    (exists (x:R), E1 x) -> (exists (x:R), E2 x) ->
    Rbar_plus (Lub_Rbar E1) (Lub_Rbar E2) =
    Lub_Rbar (fun x => exists x1 x2, E1 x1 /\ E2 x2 /\ x = x1 + x2).

  Lemma Expectation_witness (l: Rbar) (b : R)
        (rv_X: Ts -> R)
        {nnf:NonnegativeFunction rv_X} :
    Rbar_lt b l -> NonnegExpectation rv_X = l ->
    exists (x:R), (exists (rvx : Ts -> R) (rv : RandomVariable dom borel_sa rvx)
                (frf : FiniteRangeFunction rvx),
                 BoundedNonnegativeFunction rv_X rvx /\ SimpleExpectation rvx = x) /\ x > b.

  Lemma NonnegExpectation_le
        (rv_X1 rv_X2 : Ts -> R)
        {nnf1 : NonnegativeFunction rv_X1}
        {nnf2 : NonnegativeFunction rv_X2} :
    rv_le rv_X1 rv_X2 ->
    Rbar_le (NonnegExpectation rv_X1) (NonnegExpectation rv_X2).

  Lemma Lub_Rbar_const (c:R) :
    Lub_Rbar (fun x => x = c) = c.

  Lemma NonnegExpectation_const (c : R) (nnc : 0 <= c) :
    (@NonnegExpectation (const c) (nnfconst _ nnc)) = c.
  
  Lemma NonnegExpectation_scale' c
        (rv_X : Ts -> R)
        {pofrf:NonnegativeFunction rv_X}
        {pofrf2:NonnegativeFunction (rvscale c rv_X)} :
    0 <= c ->
    NonnegExpectation (rvscale c rv_X) =
    Rbar_mult c (NonnegExpectation rv_X).

  Lemma Expectation_scale (c: R)
        (rv_X : Ts -> R) :
    c <> 0 ->
    let Ex_rv := Expectation rv_X in
    let Ex_c_rv := Expectation (rvscale c rv_X) in
    Ex_c_rv =
    match Ex_rv with
    | Some x => Some (Rbar_mult c x)
    | None => None
    end.

  Lemma Expectation_pos_pofrf (rv_X : Ts -> R)
        {nnf : NonnegativeFunction rv_X} :
    Expectation rv_X = Some (NonnegExpectation rv_X).

  Lemma Expectation_simple
        (rv_X : Ts -> R)
        {rvx_rv : RandomVariable dom borel_sa rv_X}
        {frf:FiniteRangeFunction rv_X} :
    Expectation rv_X = Some (Finite (SimpleExpectation rv_X)).

  Lemma Expectation_const (c:R) :
    Expectation (const c) = Some (Finite c).

  Lemma z_le_z : 0 <= 0.

  Lemma NonnegExpectation_const0 :
    (@NonnegExpectation (const 0) (nnfconst _ z_le_z)) = 0.

  Lemma NonnegExpectation_pos
        (rv_X : Ts -> R)
        {nnf : NonnegativeFunction rv_X} :
    Rbar_le 0 (NonnegExpectation rv_X).

  Lemma Finite_NonnegExpectation_le
        (rv_X1 rv_X2 : Ts -> R)
        (nnf1 : NonnegativeFunction rv_X1)
        (nnf2 : NonnegativeFunction rv_X2) :
    rv_le rv_X1 rv_X2 ->
    is_finite (NonnegExpectation rv_X2) ->
    is_finite (NonnegExpectation rv_X1).

  Lemma Expectation_abs_then_finite (rv_X:Ts->R)
    : match Expectation (rvabs rv_X) with
       | Some (Finite _) => True
       | _ => False
       end ->
       match Expectation rv_X with
       | Some (Finite _) => True
       | _ => False
       end.

  Lemma pos_part_le
        (rvp rvn : Ts -> R)
        (p : NonnegativeFunction rvp)
        (n : NonnegativeFunction rvn) :
    rv_le (fun x : Ts => pos_fun_part (rvminus rvp rvn) x) rvp.

  Lemma neg_part_le
        (rvp rvn : Ts -> R)
        (p : NonnegativeFunction rvp)
        (n : NonnegativeFunction rvn) :
    rv_le (fun x : Ts => neg_fun_part (rvminus rvp rvn) x) rvn.


  Definition Rbar_ge_dec (x y : Rbar) := Rbar_le_dec y x.

  Definition simple_approx (X:Ts->Rbar) (n:nat) : Ts -> R
    := fun ω : Ts =>
         let Xw := X ω in
         if Rbar_ge_dec Xw (INR n) then (INR n) else
           match find (fun start => if Rbar_ge_dec Xw (Finite start) then true else false)
                      (rev (map (fun x => (INR x / (2^n)))
                                (seq 0 (n*(2^n))))) with
           | Some r => r
           | None => (INR 0)
           end.

  Definition interval_dec : forall r r1 r2 :R, {r1 <= r < r2} + {~(r1 <= r < r2)}.

  Lemma simple_approx_vals (X:Ts->Rbar) (n:nat) :
    forall (omega:Ts),
      In (simple_approx X n omega)
         (map (fun x => INR x / (2^n)) (seq 0 (S (n*(2^n))))).

  Program Instance simple_approx_frf (X:Ts->Rbar) (n:nat) :
    FiniteRangeFunction (simple_approx X n) :=
    {frf_vals := map (fun x => INR x / (2^n)) (seq 0 (S (n*(2^n))))}.

  Lemma simple_approx_preimage_inf (X:Ts -> Rbar) (n:nat) :
    Rbar_NonnegativeFunction X ->
    forall (omega:Ts), simple_approx X n omega = INR n <-> Rbar_ge (X omega) (INR n).
  
  Lemma find_some_break {A} f (l:list A) r :
    find f l = Some r ->
    exists l1 l2, l = l1 ++ r::l2 /\ Forall (fun x => f x = false) l1.

  Lemma simple_approx_preimage_fin0 (X:Ts -> Rbar) (n:nat) :
    Rbar_NonnegativeFunction X ->
    forall (omega:Ts) (k:nat),
      Rbar_lt (X omega) (INR n)->
      (simple_approx X n omega)*(2^n) = (INR k) <->
      Rbar_le (INR k) (Rbar_mult (X omega) (2^n)) /\
      Rbar_lt (Rbar_mult (X omega) (2^n)) (INR (S k)).

  Lemma simple_approx_preimage_fin (X:Ts -> Rbar) (n:nat) :
    Rbar_NonnegativeFunction X ->
    forall (omega:Ts),
      Rbar_lt (X omega) (INR n) ->
      forall (k:nat),
        simple_approx X n omega = (INR k)/2^n <->
        Rbar_le ((INR k)/2^n) (X omega) /\
        Rbar_lt (X omega) ((INR (S k))/2^n).
  
  Lemma simple_approx_preimage_fin2 (X:Ts -> Rbar) (n:nat) :
    Rbar_NonnegativeFunction X ->
    forall (omega:Ts),
    forall (k:nat),
      (k < n*2^n)%nat ->
      simple_approx X n omega = (INR k)/2^n <->
      Rbar_le ((INR k)/2^n) (X omega) /\
      Rbar_lt (X omega) ((INR (S k))/2^n).
  
  Lemma simple_approx_le (X:Ts->Rbar) (posX : Rbar_NonnegativeFunction X) :
    forall n ω, Rbar_le (simple_approx X n ω) (X ω).

  Lemma simple_approx_exists (X:Ts -> Rbar) (n:nat) :
    forall (omega:Ts),
    exists (k:nat), simple_approx X n omega = (INR k)/2^n.

  Lemma simple_approx_pos (X:Ts->Rbar) (n:nat) (ω:Ts) :
    0 <= (simple_approx X n ω).

  Instance simple_approx_pofrf (X:Ts->Rbar) (n:nat) :
    NonnegativeFunction (simple_approx X n).

  Lemma simple_approx_range_event (X : Ts -> Rbar) (n:nat) (r : R) :
    let rvals := filter (fun z => if Rle_dec z r then true else false)
                         (map (fun x : nat => INR x / 2 ^ n) (seq 0 (S (n * 2 ^ n)))) in
    pre_event_equiv (fun omega : Ts => Rbar_le (simple_approx X n omega) r)
                    (pre_list_union (map (fun z => (fun omega => simple_approx X n omega = z))
                                 rvals)).

  Lemma simple_approx_inf_event (X:Ts -> Rbar) (n:nat)
        (posx : Rbar_NonnegativeFunction X) :
    pre_event_equiv (pre_event_preimage (simple_approx X n) (pre_event_singleton (INR n)))
                (pre_event_preimage X (fun r => Rbar_ge r (INR n))).

  Lemma simple_approx_fin_event (X:Ts -> Rbar) (n:nat)
        (posx : Rbar_NonnegativeFunction X) :
    forall (k : nat),
      (k < n*2^n)%nat ->
      pre_event_equiv
        (pre_event_preimage (simple_approx X n) (pre_event_singleton ((INR k)/2^n)))
        (pre_event_preimage X (fun z => Rbar_le ((INR k)/2^n) z /\
                                        Rbar_lt z ((INR (S k))/2^n))).

  Lemma simple_approx_inf_measurable (X:Ts -> Rbar) (n:nat)
        (posx : Rbar_NonnegativeFunction X)
        (ranx : RandomVariable dom Rbar_borel_sa X) :
    sa_sigma (pre_event_preimage (simple_approx X n) (pre_event_singleton (INR n))).

  Lemma simple_approx_fin_measurable (X:Ts -> Rbar) (n:nat)
        (posx : Rbar_NonnegativeFunction X)
        (ranx : RandomVariable dom Rbar_borel_sa X) :
    forall (k : nat),
      (k < n*2^n)%nat ->
      sa_sigma (pre_event_preimage (simple_approx X n) (pre_event_singleton ((INR k)/2^n))).

  Instance simple_approx_rv (X : Ts -> Rbar)
           {posx : Rbar_NonnegativeFunction X}
           {rvx : RandomVariable dom Rbar_borel_sa X}
    : forall (n:nat), RandomVariable dom borel_sa (simple_approx X n).

  Lemma simple_approx_bound (X:Ts -> Rbar) (n:nat) :
    Rbar_NonnegativeFunction X ->
    forall (omega:Ts),
      Rbar_lt (X omega) (INR n) ->
      forall (k:nat), Rbar_le ((INR k)/2^n) (X omega) ->
                (INR k)/2^n <= simple_approx X n omega .

  Lemma simple_approx_increasing (X:Ts->Rbar) (posX : Rbar_NonnegativeFunction X)
        (n:nat) (ω : Ts) :
    simple_approx X n ω <= simple_approx X (S n) ω.
  
  Lemma simple_approx_increasing2 (X:Ts->Rbar) (posX : Rbar_NonnegativeFunction X)
        (k:nat) (ω : Ts) :
    forall (n:nat), simple_approx X n ω <= simple_approx X (n+k) ω.

  Lemma Rbar_plus_lt_compat_r (a b : Rbar) (c : R) :
    Rbar_lt a b -> Rbar_lt (Rbar_plus a c) (Rbar_plus b c).

  Lemma Rbar_minus_lt_compat_r (a b : Rbar) (c : R) :
    Rbar_lt a b -> Rbar_lt (Rbar_minus a c) (Rbar_minus b c).

  Lemma simple_approx_delta (X:Ts -> Rbar) (n:nat) (ω : Ts) (posX : Rbar_NonnegativeFunction X) :
    Rbar_lt (X ω) (INR n) -> Rbar_lt (Rbar_minus (X ω) (simple_approx X n ω)) (/ (2^n)).

  Lemma simple_approx_lim (X:Ts -> Rbar) (posX : Rbar_NonnegativeFunction X) (eps : posreal) :
    forall (ω : Ts),
      is_finite (X ω) ->
      exists (n:nat), ((X ω) - (simple_approx X n ω)) < eps.

  Lemma simple_approx_lim_seq (X:Ts -> Rbar) (posX : Rbar_NonnegativeFunction X) :
    forall (ω : Ts), is_lim_seq(fun n => simple_approx X n ω) (X ω).

  Lemma simple_NonnegExpectation
        (rv_X : Ts -> R)
        {rv : RandomVariable dom borel_sa rv_X}
        {nnf : NonnegativeFunction rv_X}
        {frf : FiniteRangeFunction rv_X} :
    Finite (SimpleExpectation rv_X) = NonnegExpectation rv_X.

  Lemma simple_expectation_real
        (rv_X : Ts -> R)
        {rv : RandomVariable dom borel_sa rv_X}
        {nnf : NonnegativeFunction rv_X}
        {frf : FiniteRangeFunction rv_X} :
    is_finite (NonnegExpectation rv_X).


  Lemma f_ge_g_le0_eq (f g : Ts -> R) :
    (pre_event_equiv (fun omega : Ts => f omega >= g omega)
                 (fun omega : Ts => (rvminus g f) omega <= 0)).
  
  Lemma sigma_f_ge_g
        (f g : Ts -> R)
        (f_rv : RandomVariable dom borel_sa f)
        (g_rv : RandomVariable dom borel_sa g) :
    sa_sigma (fun omega : Ts => f omega >= g omega).

  Lemma monotone_convergence_Ec
        (X : Ts -> Rbar )
        (Xn : nat -> Ts -> R)
        (cphi : Ts -> R)

        (Xn_rv : forall n, RandomVariable dom borel_sa (Xn n))
        (sphi : FiniteRangeFunction cphi)
        (phi_rv : RandomVariable dom borel_sa cphi)

        (posphi: NonnegativeFunction cphi)
        (Xn_pos : forall n, NonnegativeFunction (Xn n))
    :

      (forall (n:nat), Rbar_rv_le (Xn n) X) ->
      (forall (omega:Ts), cphi omega = 0 \/ Rbar_lt (cphi omega) (X omega) ) ->
      (forall (omega:Ts), is_lim_seq (fun n => Xn n omega) (X omega)) ->
      (forall (n:nat), sa_sigma (fun (omega:Ts) => (Xn n omega) >= cphi omega)) /\
      pre_event_equiv (pre_union_of_collection (fun n => fun (omega:Ts) => (Xn n omega) >= cphi omega))
                  pre_Ω.
  
  Lemma monotone_convergence_Ec2
        (Xn : nat -> Ts -> R)
        (cphi : Ts -> R)

        (Xn_rv : forall n, RandomVariable dom borel_sa (Xn n))
        (sphi : FiniteRangeFunction cphi)
        (phi_rv : RandomVariable dom borel_sa cphi)

        (posphi: NonnegativeFunction cphi)
        (Xn_pos : forall n, NonnegativeFunction (Xn n))
    :
      (forall (n:nat), rv_le (Xn n) (Xn (S n))) ->
      (forall (omega:Ts), cphi omega = 0 \/ Rbar_lt (cphi omega) ((Rbar_rvlim Xn) omega)) ->
      (forall (n:nat), sa_sigma (fun (omega:Ts) => (Xn n omega) >= cphi omega)) /\
      pre_event_equiv (pre_union_of_collection (fun n => fun (omega:Ts) => (Xn n omega) >= cphi omega))
                  pre_Ω.

  Lemma lim_prob
        (En : nat -> event dom)
        (E : event dom) :
    (forall (n:nat), event_sub (En n) (En (S n))) ->
    event_equiv (union_of_collection En) E ->
    is_lim_seq (fun n => ps_P (En n)) (ps_P E).

  Lemma lim_prob_descending
        (En : nat -> event dom)
        (E : event dom) :
    (forall (n:nat), event_sub (En (S n)) (En n)) ->
    event_equiv (inter_of_collection En) E ->
    is_lim_seq (fun n => ps_P (En n)) (ps_P E).

  Lemma is_lim_seq_list_sum (l:list (nat->R)) (l2:list R) :
    Forall2 is_lim_seq l (map Finite l2) ->
    is_lim_seq (fun n => list_sum (map (fun x => x n) l)) (list_sum l2).

  Existing Instance nodup_perm.
  Existing Instance Permutation_map'.

  Lemma simpleFunEventIndicator
        (phi : Ts -> R)
        {rphi : RandomVariable dom borel_sa phi}
        (sphi : FiniteRangeFunction phi)
        {P : event dom}
        (dec:forall x, {P x} + {~ P x}) :
    SimpleExpectation (rvmult phi (EventIndicator dec)) =
    list_sum (map (fun v => v * (ps_P (event_inter
                                      (preimage_singleton phi v)
                                      P)))
                  (nodup Req_EM_T frf_vals)).

  Lemma monotone_convergence_E_phi_lim
        (X : Ts -> Rbar )
        (Xn : nat -> Ts -> R)
        (cphi : Ts -> R)

        (Xn_rv : forall n, RandomVariable dom borel_sa (Xn n))
        (sphi : FiniteRangeFunction cphi)
        (phi_rv : RandomVariable dom borel_sa cphi)

        (posphi: NonnegativeFunction cphi)
        (Xn_pos : forall n, NonnegativeFunction (Xn n))
    :

      (forall (n:nat), Rbar_rv_le (Xn n) X) ->
      (forall (n:nat), rv_le (Xn n) (Xn (S n))) ->
      (forall (omega:Ts), cphi omega = 0 \/ Rbar_lt (cphi omega) (X omega)) ->
      (forall (omega:Ts), is_lim_seq (fun n => Xn n omega) (X omega)) ->
      is_lim_seq (fun n => NonnegExpectation
                          (rvmult cphi
                                  (EventIndicator
                                     (fun omega => Rge_dec (Xn n omega) (cphi omega)))))
                 (NonnegExpectation cphi).

  Lemma monotone_convergence_E_phi_lim2
        (Xn : nat -> Ts -> R)
        (cphi : Ts -> R)

        (Xn_rv : forall n, RandomVariable dom borel_sa (Xn n))
        (sphi : FiniteRangeFunction cphi)
        (phi_rv : RandomVariable dom borel_sa cphi)

        (posphi: NonnegativeFunction cphi)
        (Xn_pos : forall n, NonnegativeFunction (Xn n))
    :

      (forall (n:nat), rv_le (Xn n) (Xn (S n))) ->
      (forall (omega:Ts), cphi omega = 0 \/ Rbar_lt (cphi omega) ((Rbar_rvlim Xn) omega)) ->
      is_lim_seq (fun n => NonnegExpectation
                          (rvmult cphi
                                  (EventIndicator
                                     (fun omega => Rge_dec (Xn n omega) (cphi omega)))))
                 (NonnegExpectation cphi).

  Lemma monotone_convergence0_cphi
        (X : Ts -> Rbar )
        (Xn : nat -> Ts -> R)
        (cphi : Ts -> R)

        (rvx : RandomVariable dom Rbar_borel_sa X)
        (Xn_rv : forall n, RandomVariable dom borel_sa (Xn n))
        (sphi : FiniteRangeFunction cphi)
        (phi_rv : RandomVariable dom borel_sa cphi)

        (posX: Rbar_NonnegativeFunction X)
        (posphi: NonnegativeFunction cphi)
        (Xn_pos : forall n, NonnegativeFunction (Xn n))
    :

      (forall (n:nat), Rbar_rv_le (Xn n) X) ->
      (forall (n:nat), rv_le (Xn n) (Xn (S n))) ->
      (forall (omega:Ts), cphi omega = 0 \/ Rbar_lt (cphi omega) (X omega)) ->
      (forall (omega:Ts), is_lim_seq (fun n => Xn n omega) (X omega)) ->
      (forall (n:nat), is_finite (NonnegExpectation (Xn n))) ->
      Rbar_le (NonnegExpectation cphi)
              (Lim_seq (fun n => real (NonnegExpectation (Xn n)))).

  Lemma monotone_convergence0_cphi2
        (Xn : nat -> Ts -> R)
        (cphi : Ts -> R)

        (Xn_rv : forall n, RandomVariable dom borel_sa (Xn n))
        (sphi : FiniteRangeFunction cphi)
        (phi_rv : RandomVariable dom borel_sa cphi)

        (posphi: NonnegativeFunction cphi)
        (Xn_pos : forall n, NonnegativeFunction (Xn n))
    :

      (forall (n:nat), rv_le (Xn n) (Xn (S n))) ->
      (forall (omega:Ts), cphi omega = 0 \/ Rbar_lt (cphi omega) ((Rbar_rvlim Xn) omega)) ->
      (forall (n:nat), is_finite (NonnegExpectation (Xn n))) ->
      Rbar_le (NonnegExpectation cphi)
              (Lim_seq (fun n => real (NonnegExpectation (Xn n)))).

  Lemma monotone_convergence0_Rbar (c:R)
        (X : Ts -> Rbar )
        (Xn : nat -> Ts -> R)
        (phi : Ts -> R)

        (rvx : RandomVariable dom Rbar_borel_sa X)
        (Xn_rv : forall n, RandomVariable dom borel_sa (Xn n))
        (sphi : FiniteRangeFunction phi)
        (phi_rv : RandomVariable dom borel_sa phi)

        (posX: Rbar_NonnegativeFunction X)
        (posphi: NonnegativeFunction phi)
        (Xn_pos : forall n, NonnegativeFunction (Xn n))
    :

      (forall (n:nat), Rbar_rv_le (Xn n) X) ->
      (forall (n:nat), rv_le (Xn n) (Xn (S n))) ->
      (forall (n:nat), is_finite (NonnegExpectation (Xn n))) ->
      Rbar_rv_le phi X ->
      (forall (omega:Ts), is_lim_seq (fun n => Xn n omega) (X omega)) ->
      0 < c < 1 ->
      Rbar_le (Rbar_mult c (NonnegExpectation phi))
              (Lim_seq (fun n => (NonnegExpectation (Xn n)))).

  Lemma monotone_convergence0_Rbar2 (c:R)
        (Xn : nat -> Ts -> R)
        (phi : Ts -> R)

        (Xn_rv : forall n, RandomVariable dom borel_sa (Xn n))
        (sphi : FiniteRangeFunction phi)
        (phi_rv : RandomVariable dom borel_sa phi)

        (posphi: NonnegativeFunction phi)
        (Xn_pos : forall n, NonnegativeFunction (Xn n))
    :

      (forall (n:nat), rv_le (Xn n) (Xn (S n))) ->
      (forall (n:nat), is_finite (NonnegExpectation (Xn n))) ->
      Rbar_rv_le phi (Rbar_rvlim Xn) ->
      0 < c < 1 ->
      Rbar_le (Rbar_mult c (NonnegExpectation phi))
              (Lim_seq (fun n => (NonnegExpectation (Xn n)))).

  Lemma Lim_seq_NonnegExpectation_pos
        (rvxn : nat -> Ts -> R)
        (posvn: forall n, NonnegativeFunction (rvxn n)) :
    Rbar_le 0 (Lim_seq (fun n : nat => NonnegExpectation (rvxn n))).

  Lemma Lim_seq_Expectation_m_infty
        (rvxn : nat -> Ts -> R)
        (posvn: forall n, NonnegativeFunction (rvxn n)) :
    Lim_seq (fun n : nat => NonnegExpectation (rvxn n)) = m_infty -> False.

  Lemma monotone_convergence00
        (X : Ts -> Rbar )
        (Xn : nat -> Ts -> R)
        (phi : Ts -> R)

        (rvx : RandomVariable dom Rbar_borel_sa X)
        (Xn_rv : forall n, RandomVariable dom borel_sa (Xn n))
        (sphi : FiniteRangeFunction phi)
        (phi_rv : RandomVariable dom borel_sa phi)

        (posX: Rbar_NonnegativeFunction X)
        (posphi: NonnegativeFunction phi)
        (Xn_pos : forall n, NonnegativeFunction (Xn n)) :

    (forall (n:nat), Rbar_rv_le (Xn n) X) ->
    (forall (n:nat), rv_le (Xn n) (Xn (S n))) ->
    (forall (n:nat), is_finite (NonnegExpectation (Xn n))) ->
    Rbar_rv_le phi X ->
    (forall (omega:Ts), is_lim_seq (fun n => Xn n omega) (X omega)) ->
    Rbar_le
      (NonnegExpectation phi)
      (Lim_seq (fun n => (NonnegExpectation (Xn n)))).
  Lemma monotone_convergence
        (X : Ts -> R )
        (Xn : nat -> Ts -> R)
        (rvx : RandomVariable dom borel_sa X)
        (posX: NonnegativeFunction X)
        (Xn_rv : forall n, RandomVariable dom borel_sa (Xn n))
        (Xn_pos : forall n, NonnegativeFunction (Xn n)) :
    (forall (n:nat), rv_le (Xn n) X) ->
    (forall (n:nat), rv_le (Xn n) (Xn (S n))) ->
    (forall (n:nat), is_finite (NonnegExpectation (Xn n))) ->
    (forall (omega:Ts), is_lim_seq (fun n => Xn n omega) (X omega)) ->
    Lim_seq (fun n => NonnegExpectation (Xn n)) = (NonnegExpectation X).

  Lemma ex_monotone_convergence
        (Xn : nat -> Ts -> R)
        (Xn_rv : forall n, RandomVariable dom borel_sa (Xn n))
        (Xn_pos : forall n, NonnegativeFunction (Xn n)) :
    (forall (n:nat), rv_le (Xn n) (Xn (S n))) ->
    (forall (n:nat), is_finite (NonnegExpectation (Xn n))) ->
    ex_lim_seq (fun n => NonnegExpectation (Xn n)).

  
  Global Instance LimInf_seq_pos
         (Xn : nat -> Ts -> R)
         (Xn_pos : forall n, NonnegativeFunction (Xn n)) :
    NonnegativeFunction
      (fun omega : Ts => (LimInf_seq (fun n : nat => Xn n omega))).

  Definition Fatou_Y (Xn : nat -> Ts -> R) (n:nat) :=
    fun (omega : Ts) => Inf_seq (fun (k:nat) => Xn (k+n)%nat omega).

  Lemma is_finite_Fatou_Y
        (Xn : nat -> Ts -> R)
        (Xn_pos : forall n, NonnegativeFunction (Xn n))
        (n : nat) :
    forall (omega:Ts), is_finite (Fatou_Y Xn n omega).
   
  Instance Fatou_Y_pos
         (Xn : nat -> Ts -> R)
         (Xn_pos : forall n, NonnegativeFunction (Xn n)) :
    forall (n:nat), NonnegativeFunction (Fatou_Y Xn n).

  Lemma Fatou_Y_incr_Rbar (Xn : nat -> Ts -> R) n omega :
    Rbar_le (Fatou_Y Xn n omega) (Fatou_Y Xn (S n) omega).
     
  Lemma Fatou_Y_incr (Xn : nat -> Ts -> R)
        (Xn_pos : forall n, NonnegativeFunction (Xn n)) n omega:
    Fatou_Y Xn n omega <= Fatou_Y Xn (S n) omega.

    Instance Fatou_Y_meas
             (Xn : nat -> Ts -> R)
             (Xn_pos : forall n, NonnegativeFunction (Xn n))
             (Xn_rv : forall n, RealMeasurable dom (Xn n)) :
      forall (n:nat), RealMeasurable dom (Fatou_Y Xn n).
    
    Instance Fatou_Y_rv
         (Xn : nat -> Ts -> R)
         (Xn_rv : forall n, RandomVariable dom borel_sa (Xn n))
         (Xn_pos : forall n, NonnegativeFunction (Xn n))
      :
    forall (n:nat), RandomVariable dom borel_sa (Fatou_Y Xn n).

  Lemma limInf_increasing
        (f : nat -> R) :
    (forall (n:nat), f n <= f (S n)) ->
    Lim_seq f = LimInf_seq f.

  Lemma limInf_increasing2
        (f : nat -> R) :
    (forall (n:nat), f n <= f (S n)) ->
    forall (l:Rbar),
      is_lim_seq f l <-> is_LimInf_seq f l.

  Lemma inf_limInf
        (f : nat -> R) (n:nat) :
    Rbar_le (Inf_seq (fun k : nat => f (k + n)%nat))
            (LimInf_seq f).

  Lemma incr_le_strong f
        (incr:forall (n:nat), f n <= f (S n)) a b :
    (a <= b)%nat -> f a <= f b.

  Lemma is_LimInf_Sup_Seq (f: nat -> R)
        (incr:forall (n:nat), f n <= f (S n)) :
    is_LimInf_seq f (Sup_seq f).

  Lemma lim_seq_Inf_seq
        (f : nat -> R)
        (fin:forall n, is_finite (Inf_seq (fun n0 : nat => f (n0 + n)%nat)))
        (incr:forall (n:nat),
            Inf_seq (fun k : nat => f (k + n)%nat) <=
            Inf_seq (fun k : nat => f (k + (S n))%nat)) :
    is_lim_seq
      (fun n : nat => Inf_seq (fun k : nat => f (k + n)%nat))
      (LimInf_seq f).

  Lemma Fatou
        (Xn : nat -> Ts -> R)
        (Xn_pos : forall n, NonnegativeFunction (Xn n))
        (Xn_rv : forall n, RandomVariable dom borel_sa (Xn n))
        (fin_exp : forall n, is_finite (NonnegExpectation (Xn n)))
        (isf:forall omega, is_finite (LimInf_seq (fun n : nat => Xn n omega)))

        (lim_rv : RandomVariable dom borel_sa
                                 (fun omega => LimInf_seq (fun n => Xn n omega))) :
    Rbar_le (NonnegExpectation (fun omega => LimInf_seq (fun n => Xn n omega)))
            (LimInf_seq (fun n => NonnegExpectation (Xn n))).

  Lemma Expectation_zero_pos
        (X : Ts -> R)
        {rv : RandomVariable dom borel_sa X}
        {pofrf :NonnegativeFunction X} :
    Expectation X = Some (Finite 0) ->
    ps_P (preimage_singleton X 0) = 1.

  Lemma NonnegExpectation_simple_approx
        (rv_X1 : Ts -> R)
        {rv1 : RandomVariable dom borel_sa rv_X1}
        {nnf1:NonnegativeFunction rv_X1} :
     Lim_seq
         (fun n : nat =>
          NonnegExpectation (simple_approx (fun x : Ts => rv_X1 x) n)) =
       NonnegExpectation rv_X1.

  Lemma NonnegExpectation_sum
        (rv_X1 rv_X2 : Ts -> R)
        {rv1 : RandomVariable dom borel_sa rv_X1}
        {rv2 : RandomVariable dom borel_sa rv_X2}
        {nnf1:NonnegativeFunction rv_X1}
        {nnf2:NonnegativeFunction rv_X2} :
    NonnegExpectation (rvplus rv_X1 rv_X2) =
    Rbar_plus (NonnegExpectation rv_X1) (NonnegExpectation rv_X2).

  Lemma Expectation_dif_pos_unique2
        (rxp1 rxn1 rxp2 rxn2 : Ts -> R)
        (rp1 : RandomVariable dom borel_sa rxp1)
        (rn1 : RandomVariable dom borel_sa rxn1)
        (rp2 : RandomVariable dom borel_sa rxp2)
        (rn2 : RandomVariable dom borel_sa rxn2)

        (pp1 : NonnegativeFunction rxp1)
        (pn1 : NonnegativeFunction rxn1)
        (pp2 : NonnegativeFunction rxp2)
        (pn2 : NonnegativeFunction rxn2) :
    rv_eq (rvminus rxp1 rxn1) (rvminus rxp2 rxn2) ->
    is_finite (NonnegExpectation rxn1) ->
    is_finite (NonnegExpectation rxn2) ->
    Rbar_minus (NonnegExpectation rxp1) (NonnegExpectation rxn1) =
    Rbar_minus (NonnegExpectation rxp2) (NonnegExpectation rxn2).
  
  Lemma Expectation_dif_pos_unique
        (rvp rvn : Ts -> R)
        (pr : RandomVariable dom borel_sa rvp)
        (nr : RandomVariable dom borel_sa rvn)
        (p : NonnegativeFunction rvp)
        (n : NonnegativeFunction rvn) :
    is_finite (NonnegExpectation rvn) ->
    Expectation (rvminus rvp rvn) =
    Rbar_minus' (NonnegExpectation rvp)
                (NonnegExpectation rvn).

  Lemma Expectation_sum
        (rv_X1 rv_X2 : Ts -> R)
        {rv1 : RandomVariable dom borel_sa rv_X1}
        {rv2 : RandomVariable dom borel_sa rv_X2} :
    
    is_finite (NonnegExpectation (neg_fun_part rv_X1)) ->
    is_finite (NonnegExpectation (neg_fun_part rv_X2)) ->
    Expectation (rvplus rv_X1 rv_X2) =
    match Expectation rv_X1, Expectation rv_X2 with
    | Some exp1, Some exp2 => Some (Rbar_plus exp1 exp2)
    | _, _ => None
    end.

  Lemma Expectation_not_none
        (rv_X : Ts -> R)
        {rv : RandomVariable dom borel_sa rv_X} :
    match Expectation rv_X with
    | Some r => True
    | _ => False
    end ->
    is_finite (NonnegExpectation (pos_fun_part rv_X)) \/
    is_finite (NonnegExpectation (neg_fun_part rv_X)).

  Lemma neg_fun_opp (rv_X : Ts -> R) :
    rv_eq (fun x => nonneg ((neg_fun_part (rvopp rv_X)) x))
          (fun x => nonneg ((pos_fun_part rv_X) x)).

  Lemma Expectation_not_none_alt
        (rv_X : Ts -> R)
        {rv : RandomVariable dom borel_sa rv_X} :
    match Expectation rv_X with
    | Some r => True
    | _ => False
    end ->
    is_finite (NonnegExpectation (neg_fun_part (rvopp rv_X))) \/
    is_finite (NonnegExpectation (neg_fun_part rv_X)).

  Lemma Finite_Rbar_plus' (a b : Rbar) :
    forall (c:R),
      Rbar_plus' a b = Some (Finite c) ->
      is_finite a /\ is_finite b.

  Lemma Finite_Rbar_opp (a : Rbar) :
    is_finite (Rbar_opp a) <-> is_finite a.

  Lemma Finite_Rbar_minus' (a b : Rbar) :
    forall (c:R),
      Rbar_minus' a b = Some (Finite c) ->
      is_finite a /\ is_finite b.

  Lemma rvopp_opp (f : Ts -> R) :
    rv_eq (rvopp (rvopp f)) f.

  Lemma Expectation_sum_isfin_fun2
        (rv_X1 rv_X2 : Ts -> R)
        {rv1 : RandomVariable dom borel_sa rv_X1}
        {rv2 : RandomVariable dom borel_sa rv_X2} :
    forall (c:R),
      Expectation rv_X2 = Some (Finite c) ->
      match Expectation rv_X1 with
      | Some exp1 => Expectation (rvplus rv_X1 rv_X2) = Some (Rbar_plus exp1 c)
      | _ => True
      end.

  Lemma Expectation_sum_finite
        (rv_X1 rv_X2 : Ts -> R)
        {rv1 : RandomVariable dom borel_sa rv_X1}
        {rv2 : RandomVariable dom borel_sa rv_X2} :
    forall (e1 e2:R),
      Expectation rv_X1 = Some (Finite e1) ->
      Expectation rv_X2 = Some (Finite e2) ->
      Expectation (rvplus rv_X1 rv_X2) = Some (Finite (e1 + e2)).

  Lemma Expectation_le
        (rv_X1 rv_X2 : Ts -> R) :
    forall (e1 e2 : Rbar),
      Expectation rv_X1 = Some e1 ->
      Expectation rv_X2 = Some e2 ->
      rv_le rv_X1 rv_X2 ->
      Rbar_le e1 e2.
 
  Lemma Markov_ineq
        (X : Ts -> R)
        (rv : RandomVariable dom borel_sa X)
        (pofrf : NonnegativeFunction X)
        (a : posreal) :
    Rbar_le (a * (ps_P (event_ge dom X a))) (NonnegExpectation X).
      
  Lemma Markov_ineq_div
        (X : Ts -> R)
        (rv : RandomVariable dom borel_sa X)
        (pofrf : NonnegativeFunction X)
        (a : posreal) :
    Rbar_le (ps_P (event_ge dom X a)) (Rbar_div_pos (NonnegExpectation X) a).

  Lemma rsqr_pos (a : posreal) : (0 < Rsqr a).

  Lemma Rabs_Rsqr_ge (x : R) (a : posreal) :
    Rabs x >= a <-> Rsqr x >= Rsqr a.

  Lemma Chebyshev_ineq_div_mean0
        (X : Ts -> R)
        (rv : RandomVariable dom borel_sa X)
        (a : posreal) :
    Rbar_le (ps_P (event_ge dom (rvabs X) a))
            (Rbar_div_pos
               (NonnegExpectation (rvsqr X))
               (mkposreal _ (rsqr_pos a))).

  Lemma Chebyshev_ineq_div_mean
        (X : Ts -> R)
        (rv : RandomVariable dom borel_sa X)
        (mean : R)
        (a : posreal) :
    Rbar_le (ps_P (event_ge dom (rvabs (rvminus X (const mean))) a))
            (Rbar_div_pos
               (NonnegExpectation (rvsqr (rvminus X (const mean))))
               (mkposreal _ (rsqr_pos a))).

  Lemma Chebyshev_ineq_div
        (X : Ts -> R)
        (rv : RandomVariable dom borel_sa X)
        (a : posreal) :
    match (Expectation X) with
      | Some (Finite mean) =>
        Rbar_le (ps_P (event_ge dom (rvabs (rvminus X (const mean))) a))
                (Rbar_div_pos
                   (NonnegExpectation (rvsqr (rvminus X (const mean))))
                   (mkposreal _ (rsqr_pos a)))
      | _ => True
    end.

  Lemma Expectation_sqr (rv_X :Ts->R) :
    Expectation (rvsqr rv_X) = Some (NonnegExpectation (rvsqr rv_X)).

End Expectation_sec.

Section almost_sec.

  Context {Ts:Type}
          {dom: SigmaAlgebra Ts}
          (prts: ProbSpace dom).
  
  Instance pos_fun_part_proper_almostR2 : Proper (almostR2 prts eq ==> almostR2 prts eq)
                                            (fun x x0 => nonneg (pos_fun_part x x0)).

  Instance neg_fun_part_proper_almostR2 : Proper (almostR2 prts eq ==> almostR2 prts eq)
                                            (fun x x0 => nonneg (neg_fun_part x x0)).

  Lemma NonnegExpectation_almostR2_0 x
        {nnf:NonnegativeFunction x} :
    almostR2 prts eq x (const 0) ->
    NonnegExpectation x = 0.

    Lemma NonnegExpectation_EventIndicator_as x {P} (dec:dec_event P)
        {xrv:RandomVariable dom borel_sa x}
        {xnnf:NonnegativeFunction x}
    :
      ps_P P = 1 ->
    NonnegExpectation x = NonnegExpectation (rvmult x (EventIndicator dec)).
  
  Lemma NonnegExpectation_almostR2_proper x y
        {xrv:RandomVariable dom borel_sa x}
        {yrv:RandomVariable dom borel_sa y}
        {xnnf:NonnegativeFunction x}
        {ynnf:NonnegativeFunction y} :
    almostR2 prts eq x y ->
    NonnegExpectation x = NonnegExpectation y.
  
  Lemma Expectation_almostR2_0 x :
    almostR2 prts eq x (const 0) ->
    Expectation x = Some (Finite 0).

  Lemma Expectation_almostR2_proper x y
        {xrv:RandomVariable dom borel_sa x}
        {yrv:RandomVariable dom borel_sa y} :
    almostR2 prts eq x y ->
    Expectation x = Expectation y.

  Lemma pos_fun_mult_ind_ge (X:Ts->R)
        {rv : RandomVariable dom borel_sa X} :
    rv_eq (fun omega => nonneg (pos_fun_part X omega))
          (rvmult X (EventIndicator (event_ge_dec dom X 0))).

  Lemma event_le_dec (σ:SigmaAlgebra Ts) x1 n
        {rv1:RandomVariable σ borel_sa x1} :
    dec_event (event_le σ x1 n).

  Lemma neg_fun_mult_ind_le (X:Ts->R)
        {rv : RandomVariable dom borel_sa X} :
    rv_eq (rvopp (fun omega => nonneg (neg_fun_part X omega)))
          (rvmult X (EventIndicator (event_le_dec dom X 0))).

  Lemma neg_fun_mult_ind_le' (X:Ts->R)
        {rv : RandomVariable dom borel_sa X} :
    rv_eq (fun omega => nonneg (neg_fun_part X omega))
          (rvopp (rvmult X (EventIndicator (event_le_dec dom X 0)))).

  Lemma Expectation_nonneg_zero_almost_zero
        (X : Ts -> R)
        {rv : RandomVariable dom borel_sa X}
        {pofrf :NonnegativeFunction X} :
    Expectation X = Some (Finite 0) ->
    almostR2 prts eq X (const 0).

  Lemma Expectation_mult_indicator_almost_zero
        (X : Ts -> R)
        {rv : RandomVariable dom borel_sa X} :
    (forall P (dec:dec_event P), Expectation (rvmult X (EventIndicator dec))
                            = Some (Finite 0)) ->
    almostR2 prts eq X (const 0).

  Lemma Expectation_mult_indicator_almost_nonneg_zero'
        (X : Ts -> R)
        {rv : RandomVariable dom borel_sa X} :
    (forall P (dec:dec_event P),
        match Expectation (rvmult X (EventIndicator dec)) with
        | Some (Finite r) => 0 <= r
        | _ => False
        end) ->
    almostR2 prts eq (fun x : Ts => nonneg (neg_fun_part X x)) (const 0).

  Lemma neg_fun_part_eq_0_nonneg
        (X : Ts -> R)
        {rv : RandomVariable dom borel_sa X} :
    rv_eq (fun x : Ts => nonneg (neg_fun_part X x)) (const 0) ->
    NonnegativeFunction X.

  Lemma neg_fun_part_eq_0_nonneg_almost
        (X : Ts -> R)
        {rv : RandomVariable dom borel_sa X} :
    almostR2 prts eq (fun x : Ts => nonneg (neg_fun_part X x)) (const 0) ->
    almostR2 prts Rle (const 0) X.

  Lemma Expectation_mult_indicator_almost_nonneg'
        (X : Ts -> R)
        {rv : RandomVariable dom borel_sa X} :
    (forall P (dec:dec_event P),
        match Expectation (rvmult X (EventIndicator dec)) with
        | Some (Finite r) => 0 <= r
        | _ => False
        end) ->
    almostR2 prts Rle (const 0) X.

  Lemma Expectation_mult_indicator_almost_nonneg_zero
        (X : Ts -> R)
        {rv : RandomVariable dom borel_sa X} :
    (forall P (dec:dec_event P),
        match Expectation (rvmult X (EventIndicator dec)) with
        | Some r => Rbar_le 0 r
        | _ => False
        end) ->
    almostR2 prts eq (fun x : Ts => nonneg (neg_fun_part X x)) (const 0).

  Lemma Expectation_mult_indicator_almost_nonneg
        (X : Ts -> R)
        {rv : RandomVariable dom borel_sa X} :
    (forall P (dec:dec_event P),
        match Expectation (rvmult X (EventIndicator dec)) with
        | Some r => Rbar_le 0 r
        | _ => False
        end) ->
    almostR2 prts Rle (const 0) X.


Lemma Expectation_EventIndicator:
  forall {Ts : Type} {dom : SigmaAlgebra Ts} {Prts : ProbSpace dom} {P : event dom}
    (dec : forall x : Ts, {P x} + {~ P x}), Expectation (EventIndicator dec) = Some (Finite (ps_P P)).

End almost_sec.

Section EventRestricted.
    Context {Ts:Type}
          {dom: SigmaAlgebra Ts}
          (prts: ProbSpace dom).

      Lemma event_restricted_NonnegExpectation P (pf1 : ps_P P = 1) pf (f : Ts -> R)
        (nnf : NonnegativeFunction f) :
    @NonnegExpectation Ts dom prts f nnf =
    @NonnegExpectation _ _ (event_restricted_prob_space prts P pf)
                       (event_restricted_function P f) _.

  Lemma event_restricted_Expectation P (pf1 : ps_P P = 1) pf (f : Ts -> R) :
    @Expectation Ts dom prts f =
    @Expectation _ _ (event_restricted_prob_space prts P pf)
                       (event_restricted_function P f).
End EventRestricted.

Section sa_sub.

    Context {Ts:Type}
          {dom: SigmaAlgebra Ts}
          (prts:ProbSpace dom)
          {dom2 : SigmaAlgebra Ts}
          (sub : sa_sub dom2 dom).

  Lemma NonnegExpectation_prob_space_sa_sub
        (x:Ts -> R)
        {pofrf:NonnegativeFunction x}
        {rv:RandomVariable dom2 borel_sa x}
        
    :
      @NonnegExpectation Ts dom2 (prob_space_sa_sub prts sub) x pofrf =
      @NonnegExpectation Ts dom prts x pofrf.

  Lemma Expectation_prob_space_sa_sub
        (x:Ts->R)
        {rv:RandomVariable dom2 borel_sa x} :
    @Expectation Ts dom2 (prob_space_sa_sub prts sub) x =
    @Expectation Ts dom prts x.

End sa_sub.