Module FormalML.ProbTheory.RbarExpectation

Require Import Reals.

Require Import Lra Lia.
Require Import List Permutation.
Require Import Morphisms EquivDec Program.
Require Import Coquelicot.Coquelicot.
Require Import Classical_Prop.
Require Import Classical.
Require Import RealRandomVariable.

Require Import Utils.
Require Export SimpleExpectation Expectation.
Require Import Almost.
Import ListNotations.

Set Bullet Behavior "Strict Subproofs".

Local Open Scope R.

Require Import RandomVariableFinite.

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

  Local Open Scope prob.

  Definition Rbar_NonnegExpectation
             (rv_X : Ts -> Rbar)
             {pofrf:Rbar_NonnegativeFunction rv_X} : Rbar :=
    (SimpleExpectationSup
       (fun
           (rvx2: Ts -> R)
           (rv2 : RandomVariable dom borel_sa rvx2)
           (frf2: FiniteRangeFunction rvx2) =>
           NonnegativeFunction rvx2 /\
           (Rbar_rv_le rvx2 rv_X))).

  Lemma Rbar_NonnegExpectation_ext
        {rv_X1 rv_X2 : Ts -> Rbar}
        (nnf1:Rbar_NonnegativeFunction rv_X1)
        (nnf2:Rbar_NonnegativeFunction rv_X2):
    rv_eq rv_X1 rv_X2 ->
    Rbar_NonnegExpectation rv_X1 = Rbar_NonnegExpectation rv_X2.

  Lemma Rbar_NonnegExpectation_pf_irrel
        {rv_X: Ts -> R}
        (nnf1 nnf2:Rbar_NonnegativeFunction rv_X) :
    Rbar_NonnegExpectation rv_X (pofrf:=nnf1) = Rbar_NonnegExpectation rv_X (pofrf:=nnf2).

  Definition Rbar_pos_fun_part (f : Ts -> Rbar) : (Ts -> Rbar) :=
    fun x => Rbar_max (f x) 0.
    
  Definition Rbar_neg_fun_part (f : Ts -> Rbar) : (Ts -> Rbar) :=
    fun x => Rbar_max (Rbar_opp (f x)) 0.

  Program Definition Rbar_neg_fun_part_alt (f : Ts -> Rbar) : (Ts -> Rbar) :=
    Rbar_pos_fun_part (fun x => Rbar_opp (f x)).

  Lemma Rbar_neg_fun_part_alt_rveq (f : Ts -> Rbar) :
    rv_eq (Rbar_neg_fun_part f) (Rbar_neg_fun_part_alt f).

  Instance Rbar_opp_measurable (f : Ts -> Rbar) :
    RbarMeasurable f ->
    RbarMeasurable (fun x => Rbar_opp (f x)).

  Global Instance Rbar_pos_fun_part_measurable (f : Ts -> Rbar) :
    RbarMeasurable f ->
    RbarMeasurable (Rbar_pos_fun_part f).

  Instance Rbar_neg_fun_part_measurable (f : Ts -> Rbar) :
      RbarMeasurable f ->
      RbarMeasurable (Rbar_neg_fun_part f).

  Global Instance Rbar_pos_fun_part_rv (f : Ts -> Rbar)
         (rv : RandomVariable dom Rbar_borel_sa f) :
    RandomVariable dom Rbar_borel_sa (Rbar_pos_fun_part f).

  Global Instance Rbar_neg_fun_part_rv (f : Ts -> Rbar)
         (rv : RandomVariable dom Rbar_borel_sa f) :
    RandomVariable dom Rbar_borel_sa (Rbar_neg_fun_part f).

  Global Instance Rbar_pos_fun_pos (f : Ts -> Rbar) :
    Rbar_NonnegativeFunction (Rbar_pos_fun_part f).

  Global Instance Rbar_neg_fun_pos (f : Ts -> Rbar) :
    Rbar_NonnegativeFunction (Rbar_neg_fun_part f).

  Definition Rbar_Expectation (rv_X : Ts -> Rbar) : option Rbar :=
    Rbar_minus' (Rbar_NonnegExpectation (Rbar_pos_fun_part rv_X))
                (Rbar_NonnegExpectation (Rbar_neg_fun_part rv_X)).

  Lemma Rbar_Expectation_ext {rv_X1 rv_X2 : Ts -> Rbar} :
    rv_eq rv_X1 rv_X2 ->
    Rbar_Expectation rv_X1 = Rbar_Expectation rv_X2.

  Global Instance Rbar_Expectation_proper : Proper (rv_eq ==> eq) Rbar_Expectation.

  Lemma Rbar_NonnegExpectation_le
        (rv_X1 rv_X2 : Ts -> Rbar)
        {nnf1 : Rbar_NonnegativeFunction rv_X1}
        {nnf2 : Rbar_NonnegativeFunction rv_X2} :
    Rbar_rv_le rv_X1 rv_X2 ->
    Rbar_le (Rbar_NonnegExpectation rv_X1) (Rbar_NonnegExpectation rv_X2).

  Lemma Rbar_NonnegExpectation_const (c : R) (nnc : 0 <= c) :
    (@Rbar_NonnegExpectation (const c) (nnfconst _ nnc)) = c.

  Lemma Rbar_NonnegExpectation_const0 :
    (@Rbar_NonnegExpectation (const 0) (nnfconst _ z_le_z)) = 0.

  Lemma Rbar_NonnegExpectation_pos
        (rv_X : Ts -> Rbar)
        {nnf : Rbar_NonnegativeFunction rv_X} :
    Rbar_le 0 (Rbar_NonnegExpectation rv_X).

  Lemma is_finite_Rbar_NonnegExpectation_le
        (rv_X1 rv_X2 : Ts -> Rbar)
        {nnf1 : Rbar_NonnegativeFunction rv_X1}
        {nnf2 : Rbar_NonnegativeFunction rv_X2} :
    Rbar_rv_le rv_X1 rv_X2 ->
    is_finite (Rbar_NonnegExpectation rv_X2) ->
    is_finite (Rbar_NonnegExpectation rv_X1).

      
  Lemma NNExpectation_Rbar_NNExpectation
        (rv_X : Ts -> R)
        (xpos : NonnegativeFunction rv_X) :
    NonnegExpectation rv_X = Rbar_NonnegExpectation rv_X.
  
  Lemma NNExpectation_Rbar_NNExpectation'
        (rv_X : Ts -> R)
        (xpos : NonnegativeFunction rv_X)
        (xpos' : Rbar_NonnegativeFunction rv_X) :
    NonnegExpectation rv_X = Rbar_NonnegExpectation rv_X.
  
  Lemma simple_Rbar_NonnegExpectation (rv_X : Ts -> R)
        {rv : RandomVariable dom borel_sa rv_X}
        {rv' : RandomVariable dom Rbar_borel_sa rv_X}
        {nnf : Rbar_NonnegativeFunction rv_X}
        {frf : FiniteRangeFunction rv_X} :
    Finite (SimpleExpectation rv_X) = Rbar_NonnegExpectation rv_X.
  
  Lemma Rbar_pos_fun_pos_fun (rv_X : Ts -> R) :
    rv_eq (Rbar_pos_fun_part rv_X) (pos_fun_part rv_X).
  
  Lemma Rbar_neg_fun_neg_fun (rv_X : Ts -> R) :
    rv_eq (Rbar_neg_fun_part rv_X) (neg_fun_part rv_X).

  Lemma Expectation_Rbar_Expectation
        (rv_X : Ts -> R) :
    Expectation rv_X = Rbar_Expectation rv_X.

    Lemma Expectation_rvlim_ge
        (Xn : nat -> Ts -> Rbar)
        (Xn_pos : forall n, Rbar_NonnegativeFunction (Xn n)) :
      (forall (n:nat), Rbar_rv_le (Xn n) (Xn (S n))) ->
      forall n, Rbar_le (Rbar_NonnegExpectation (Xn n)) (Rbar_NonnegExpectation (Rbar_rvlim Xn)).

  Lemma sigma_f_Rbar_ge_g (f g : Ts -> Rbar)
        {rvf:RandomVariable dom Rbar_borel_sa f}
        {rvg:RandomVariable dom Rbar_borel_sa g} :
    sa_sigma (fun omega : Ts => Rbar_ge (f omega) (g omega)).

  Lemma ELim_seq_NonnegExpectation_pos
        (rvxn : nat -> Ts -> Rbar)
        (posvn: forall n, Rbar_NonnegativeFunction (rvxn n)) :
    Rbar_le 0 (ELim_seq (fun n : nat => Rbar_NonnegExpectation (rvxn n))).

  Lemma ELim_seq_Expectation_m_infty
        (rvxn : nat -> Ts -> Rbar)
        (posvn: forall n, Rbar_NonnegativeFunction (rvxn n)) :
    ELim_seq (fun n : nat => Rbar_NonnegExpectation (rvxn n)) = m_infty -> False.

  Lemma Rbar_abs_left1 (a : Rbar) : Rbar_le a 0 -> Rbar_abs a = Rbar_opp a.

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

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

        (posphi: NonnegativeFunction cphi)
        (Xn_pos : forall n, Rbar_NonnegativeFunction (Xn n))
    :
      (forall (n:nat), Rbar_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) => Rbar_ge (Xn n omega) (cphi omega))) /\
      pre_event_equiv (pre_union_of_collection (fun n => fun (omega:Ts) => (Rbar_ge (Xn n omega) (cphi omega))))
                  pre_Ω.
  
  Lemma monotone_convergence_E_phi_lim2_Rbar_rvlim
        (Xn : nat -> Ts -> Rbar)
        (cphi : Ts -> R)

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

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

      (forall (n:nat), Rbar_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 => Rbar_ge_dec (Xn n omega) (cphi omega)))))
                 (NonnegExpectation cphi).

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

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

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

      (forall (n:nat), Rbar_rv_le (Xn n) (Xn (S n))) ->
      (forall (omega:Ts), cphi omega = 0 \/ Rbar_lt (cphi omega) ((Rbar_rvlim Xn) omega)) ->
      Rbar_le (NonnegExpectation cphi)
              (ELim_seq (fun n => Rbar_NonnegExpectation (Xn n))).

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

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

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

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

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

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

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

    (forall (n:nat), Rbar_rv_le (Xn n) (Xn (S n))) ->
    Rbar_rv_le phi (Rbar_rvlim Xn) ->
    Rbar_le
      (NonnegExpectation phi)
      (ELim_seq (fun n => (Rbar_NonnegExpectation (Xn n)))).

  Lemma Rbar_monotone_convergence
        (X : Ts -> Rbar)
        (Xn : nat -> Ts -> Rbar)
        (rvx : RandomVariable dom Rbar_borel_sa X)
        (posX: Rbar_NonnegativeFunction X)
        (Xn_rv : forall n, RandomVariable dom Rbar_borel_sa (Xn n))
        (Xn_pos : forall n, Rbar_NonnegativeFunction (Xn n)) :
    (forall (n:nat), Rbar_rv_le (Xn n) X) ->
    (forall (n:nat), Rbar_rv_le (Xn n) (Xn (S n))) ->
    (forall (omega:Ts), is_Elim_seq (fun n => Xn n omega) (X omega)) ->
    ELim_seq (fun n => Rbar_NonnegExpectation (Xn n)) = (Rbar_NonnegExpectation X).

  Lemma monotone_convergence_Rbar_rvlim
        (Xn : nat -> Ts -> Rbar)
        (Xn_rv : forall n, RandomVariable dom Rbar_borel_sa (Xn n))
        (Xn_pos : forall n, Rbar_NonnegativeFunction (Xn n)) :
    (forall (n:nat), Rbar_rv_le (Xn n) (Xn (S n))) ->
    ELim_seq (fun n => Rbar_NonnegExpectation (Xn n)) = Rbar_NonnegExpectation (Rbar_rvlim Xn).

  Lemma monotone_convergence_Rbar_rvlim_fin
        (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))) ->
    ELim_seq (fun n => NonnegExpectation (Xn n)) = Rbar_NonnegExpectation (Rbar_rvlim Xn).

  Global Instance Rbar_NonnegativeFunction_const_posreal (c: posreal) :
    Rbar_NonnegativeFunction (const (B:=Ts) c).
  
  Lemma Rbar_NonnegExpectation_scale (c: posreal)
        (rv_X : Ts -> Rbar)
        {pofrf:Rbar_NonnegativeFunction rv_X} :
    Rbar_NonnegExpectation (Rbar_rvmult (const c) rv_X) =
    Rbar_mult c (Rbar_NonnegExpectation rv_X).

  Lemma Rbar_Expectation_scale_pos (c:posreal) (rv_X : Ts -> Rbar) :
    Rbar_NonnegExpectation (Rbar_pos_fun_part (Rbar_rvmult (const c) rv_X)) =
    Rbar_mult c (Rbar_NonnegExpectation (Rbar_pos_fun_part rv_X)).
  
  Lemma Rbar_Expectation_scale_neg (c:posreal) (rv_X : Ts -> Rbar) :
    Rbar_NonnegExpectation (fun x : Ts => Rbar_neg_fun_part (Rbar_rvmult (const c) rv_X) x) =
    Rbar_mult c (Rbar_NonnegExpectation (Rbar_neg_fun_part rv_X)).

  Lemma Rbar_Expectation_scale_posreal (c: posreal)
        (rv_X : Ts -> Rbar) :
    let Ex_rv := Rbar_Expectation rv_X in
    let Ex_c_rv := Rbar_Expectation (Rbar_rvmult (const c) rv_X) in
    Ex_c_rv =
    match Ex_rv with
    | Some x => Some (Rbar_mult c x)
    | None => None
    end.

  Lemma Rbar_NonnegExpectation_plus
        (rv_X1 rv_X2 : Ts -> Rbar)
        {rv1 : RandomVariable dom Rbar_borel_sa rv_X1}
        {rv2 : RandomVariable dom Rbar_borel_sa rv_X2}
        {nnf1:Rbar_NonnegativeFunction rv_X1}
        {nnf2:Rbar_NonnegativeFunction rv_X2} :
    Rbar_NonnegExpectation (Rbar_rvplus rv_X1 rv_X2) =
    Rbar_plus (Rbar_NonnegExpectation rv_X1) (Rbar_NonnegExpectation rv_X2).

  Lemma Rbar_pos_fun_part_pos (rv_X : Ts -> Rbar)
        {nnf : Rbar_NonnegativeFunction rv_X} :
    rv_eq rv_X (Rbar_pos_fun_part rv_X).

  Lemma Rbar_neg_fun_part_pos (rv_X : Ts -> Rbar)
        {nnf : Rbar_NonnegativeFunction rv_X} :
    rv_eq (Rbar_neg_fun_part rv_X) (fun x => (const 0) x).

  Instance nnf_0 :
    (@Rbar_NonnegativeFunction Ts (fun x => const 0 x)).

  Lemma Rbar_Expectation_pos_pofrf (rv_X : Ts -> Rbar)
        {nnf : Rbar_NonnegativeFunction rv_X} :
    Rbar_Expectation rv_X = Some (Rbar_NonnegExpectation rv_X).

  Lemma Rbar_Expectation_zero_pos
        (X : Ts -> Rbar)
        {rv : RandomVariable dom Rbar_borel_sa X}
        {pofrf : Rbar_NonnegativeFunction X} :
    Rbar_Expectation X = Some (Finite 0) ->
    ps_P (preimage_singleton (has_pre := Rbar_borel_has_preimages) X (Finite 0)) = 1.

  Lemma Rbar_Expectation_nonneg_zero_almost_zero
        (X : Ts -> Rbar)
        {rv : RandomVariable dom Rbar_borel_sa X}
        {pofrf :Rbar_NonnegativeFunction X} :
    Rbar_Expectation X = Some (Finite 0) ->
    almostR2 Prts eq X (const (Finite 0)).

    Global Instance Rbar_nnfabs
           (rv_X : Ts -> Rbar) :
      Rbar_NonnegativeFunction (Rbar_rvabs rv_X).

    Lemma Rbar_pos_fun_part_le rv_X :
      Rbar_rv_le (Rbar_pos_fun_part rv_X) (Rbar_rvabs rv_X).

    Lemma Rbar_neg_fun_part_le rv_X :
      Rbar_rv_le (Rbar_neg_fun_part rv_X) (Rbar_rvabs rv_X).

  Lemma Rbar_Expectation_abs_then_finite (rv_X:Ts->Rbar)
    : match Rbar_Expectation (Rbar_rvabs rv_X) with
       | Some (Finite _) => True
       | _ => False
       end ->
       match Rbar_Expectation rv_X with
       | Some (Finite _) => True
       | _ => False
       end.

    Lemma Rbar_rv_pos_neg_id (rv_X:Ts->Rbar) :
      rv_eq (rv_X) (Rbar_rvplus (Rbar_pos_fun_part rv_X) (Rbar_rvopp (Rbar_neg_fun_part rv_X))).

  Lemma Rbar_Expectation_opp
        (rv_X : Ts -> Rbar) :
    let Ex_rv := Rbar_Expectation rv_X in
    let Ex_o_rv := Rbar_Expectation (Rbar_rvopp rv_X) in
    Ex_o_rv =
    match Ex_rv with
    | Some x => Some (Rbar_opp x)
    | None => None
    end.

  Lemma Rbar_Expectation_scale (c: R)
        (rv_X : Ts -> Rbar) :
    c <> 0 ->
    let Ex_rv := Rbar_Expectation rv_X in
    let Ex_c_rv := Rbar_Expectation (Rbar_rvmult (const c) rv_X) in
    Ex_c_rv =
    match Ex_rv with
    | Some x => Some (Rbar_mult c x)
    | None => None
    end.

  Global Instance Rbar_ELimInf_seq_pos
         (Xn : nat -> Ts -> Rbar)
         (Xn_pos : forall n, Rbar_NonnegativeFunction (Xn n)) :
    Rbar_NonnegativeFunction
      (fun omega : Ts => (ELimInf_seq (fun n : nat => Xn n omega))).

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

  Instance EFatou_Y_pos
         (Xn : nat -> Ts -> Rbar)
         (Xn_pos : forall n, Rbar_NonnegativeFunction (Xn n)) :
    forall (n:nat), Rbar_NonnegativeFunction (EFatou_Y Xn n).

  Lemma EFatou_Y_incr_Rbar (Xn : nat -> Ts -> Rbar) n omega :
    Rbar_le (EFatou_Y Xn n omega) (EFatou_Y Xn (S n) omega).
     
  Instance EFatou_Y_meas
           (Xn : nat -> Ts -> Rbar)
           (Xn_pos : forall n, Rbar_NonnegativeFunction (Xn n))
           (Xn_rv : forall n, RbarMeasurable (Xn n)) :
    forall (n:nat), RbarMeasurable (EFatou_Y Xn n).
    
    Instance EFatou_Y_rv
         (Xn : nat -> Ts -> Rbar)
         (Xn_rv : forall n, RandomVariable dom Rbar_borel_sa (Xn n))
         (Xn_pos : forall n, Rbar_NonnegativeFunction (Xn n))
      :
    forall (n:nat), RandomVariable dom Rbar_borel_sa (EFatou_Y Xn n).

  Lemma ElimInf_increasing
        (f : nat -> Rbar) :
    (forall (n:nat), Rbar_le (f n) (f (S n))) ->
    ELim_seq f = ELimInf_seq f.

  Lemma inf_ElimInf
        (f : nat -> Rbar) (n:nat) :
    Rbar_le (Inf_seq (fun k : nat => f (k + n)%nat))
            (ELimInf_seq f).

  Lemma ElimInf_increasing2
        (f : nat -> Rbar) :
    (forall (n:nat), Rbar_le (f n) (f (S n))) ->
    forall (l:Rbar),
      is_Elim_seq f l <-> is_ELimInf_seq f l.

  Lemma incr_Rbar_le_strong f
        (incr:forall (n:nat), Rbar_le (f n) (f (S n))) a b :
    le a b -> Rbar_le (f a) (f b).

  Lemma is_ELimInf_Sup_Seq (f: nat -> Rbar)
        (incr:forall (n:nat), Rbar_le (f n) (f (S n))) :
    is_ELimInf_seq f (Sup_seq f).

  Lemma Elim_seq_Inf_seq
        (f : nat -> Rbar)
        (incr:forall (n:nat),
            Rbar_le (Inf_seq (fun k : nat => f (k + n)%nat))
                    (Inf_seq (fun k : nat => f (k + (S n))%nat))) :
    is_Elim_seq
      (fun n : nat => Inf_seq (fun k : nat => f (k + n)%nat))
      (ELimInf_seq f).

  Lemma Rbar_NN_Fatou
        (Xn : nat -> Ts -> Rbar)
        (Xn_pos : forall n, Rbar_NonnegativeFunction (Xn n))
        (Xn_rv : forall n, RandomVariable dom Rbar_borel_sa (Xn n))
        (lim_rv : RandomVariable dom Rbar_borel_sa
                                 (fun omega => ELimInf_seq (fun n => Xn n omega))) :
    Rbar_le (Rbar_NonnegExpectation (fun omega => ELimInf_seq (fun n => Xn n omega)))
            (ELimInf_seq (fun n => Rbar_NonnegExpectation (Xn n))).

End RbarExpectation.

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

    
  Lemma event_restricted_Rbar_NonnegExpectation P (pf1 : ps_P P = 1) pf (f : Ts -> Rbar)
        (nnf : Rbar_NonnegativeFunction f) :
    @Rbar_NonnegExpectation Ts dom prts f nnf =
    @Rbar_NonnegExpectation _ _ (event_restricted_prob_space prts P pf)
                       (event_restricted_function P f) _.

  Lemma event_restricted_Rbar_Expectation P (pf1 : ps_P P = 1) pf (f : Ts -> Rbar) :
    @Rbar_Expectation Ts dom prts f =
    @Rbar_Expectation _ _ (event_restricted_prob_space prts P pf)
                       (event_restricted_function P f).

End EventRestricted.

Section almost.

    Context {Ts:Type}
          {dom: SigmaAlgebra Ts}.

  Context (prts: ProbSpace dom).

  Instance Rbar_pos_fun_part_proper_almostR2 : Proper (almostR2 prts eq ==> almostR2 prts eq)
                                            (fun x x0 => Rbar_pos_fun_part x x0).

  Instance Rbar_neg_fun_part_proper_almostR2 : Proper (almostR2 prts eq ==> almostR2 prts eq)
                                            (fun x x0 => Rbar_neg_fun_part x x0).

  Lemma Rbar_NonnegExpectation_almostR2_0 x
        {nnf:Rbar_NonnegativeFunction x} :
    almostR2 prts eq x (const 0) ->
    Rbar_NonnegExpectation x = 0.

  
  Lemma Rbar_NonnegExpectation_EventIndicator_as x {P} (dec:dec_event P)
        {xrv:RandomVariable dom Rbar_borel_sa x}
        {xnnf:Rbar_NonnegativeFunction x}
    :
      ps_P P = 1 ->
    Rbar_NonnegExpectation x = Rbar_NonnegExpectation (Rbar_rvmult x (EventIndicator dec)).

  
  Lemma Rbar_NonnegExpectation_almostR2_proper x y
        {xrv:RandomVariable dom Rbar_borel_sa x}
        {yrv:RandomVariable dom Rbar_borel_sa y}
        {xnnf:Rbar_NonnegativeFunction x}
        {ynnf:Rbar_NonnegativeFunction y} :
    almostR2 prts eq x y ->
    Rbar_NonnegExpectation x = Rbar_NonnegExpectation y.

  Lemma Rbar_Expectation_almostR2_proper x y
        {xrv:RandomVariable dom Rbar_borel_sa x}
        {yrv:RandomVariable dom Rbar_borel_sa y} :
    almostR2 prts eq x y ->
    Rbar_Expectation x = Rbar_Expectation y.

  
  Lemma Rbar_pos_neg_id (x:Rbar) :
    x = Rbar_plus (Rbar_max x 0) (Rbar_opp (Rbar_max (Rbar_opp x) 0)).

  Lemma Rbar_max_minus_nneg (x y : Rbar) :
    Rbar_le 0 x ->
    Rbar_le 0 y ->
    (x = 0 \/ y = 0) ->
    Rbar_max (Rbar_minus x y) 0 = x.

    Program Definition pinf_Indicator
          (f : Ts -> Rbar) :=
    EventIndicator (P := (fun x => (f x) = p_infty)) _.

  Instance Rbar_positive_indicator_prod (f : Ts -> Rbar) (c : posreal) :
    Rbar_NonnegativeFunction (rvscale c (pinf_Indicator f)).

  Lemma finite_Rbar_NonnegExpectation_le_inf
        (f : Ts -> Rbar)
        (fpos : Rbar_NonnegativeFunction f)
        (c : posreal) :
    is_finite (Rbar_NonnegExpectation f) ->
    Rbar_le (NonnegExpectation (rvscale c (pinf_Indicator f)))
            (Rbar_NonnegExpectation f).
  
  Lemma finite_Rbar_NonnegExpectation_le_inf2
        (f : Ts -> Rbar)
        (rv : RandomVariable dom Rbar_borel_sa f)
        (fpos : Rbar_NonnegativeFunction f) :
    is_finite (Rbar_NonnegExpectation f) ->
    forall (c:posreal), Rbar_le (c * (ps_P (exist _ _ (sa_pinf_Rbar f rv))))
            (Rbar_NonnegExpectation f).

   Lemma finite_Rbar_NonnegExpectation_never_inf
        (f : Ts -> Rbar)
        (rv : RandomVariable dom Rbar_borel_sa f)
        (fpos : Rbar_NonnegativeFunction f) :
    is_finite (Rbar_NonnegExpectation f) ->
    ps_P (exist sa_sigma _ (sa_pinf_Rbar f rv)) = 0.

  Lemma finite_Rbar_NonnegExpectation_almostR2_finite
        (f : Ts -> Rbar)
        (rv : RandomVariable dom Rbar_borel_sa f)
        (fpos : Rbar_NonnegativeFunction f) :
    is_finite (Rbar_NonnegExpectation f) ->
    ps_P (exist sa_sigma _ (sa_finite_Rbar f rv)) = 1.

  Lemma finite_Rbar_NonnegExpectation_almost_finite
        (f : Ts -> Rbar)
        (rv : RandomVariable dom Rbar_borel_sa f)
        (fpos : Rbar_NonnegativeFunction f) :
    is_finite (Rbar_NonnegExpectation f) ->
    almost prts (fun x => is_finite (f x)).

  Class Rbar_IsFiniteExpectation (rv_X:Ts->Rbar)
    := Rbar_is_finite_expectation :
         match Rbar_Expectation rv_X with
         | Some (Finite _) => True
         | _ => False
         end.

  Lemma Rbar_rvabs_plus_posfun_negfun
        (f : Ts -> Rbar ) :
    rv_eq (Rbar_rvabs f)
          (Rbar_rvplus (Rbar_pos_fun_part f) (Rbar_neg_fun_part f)).
  
  Instance IsFiniteExpectation_Rbar f : IsFiniteExpectation prts f -> Rbar_IsFiniteExpectation f.


  Lemma finiteExp_Rbar_rvabs
        (f : Ts -> Rbar)
        {rv : RandomVariable dom Rbar_borel_sa f}:
    Rbar_IsFiniteExpectation f <->
    is_finite (Rbar_NonnegExpectation (Rbar_rvabs f)).

  Lemma finite_Rbar_Expectation_almostR2_finite
        (f : Ts -> Rbar)
        (rv : RandomVariable dom Rbar_borel_sa f) :
    Rbar_IsFiniteExpectation f ->
    ps_P (exist sa_sigma _ (sa_finite_Rbar f rv)) = 1.

  Lemma IsFiniteExpectation_nneg_is_almost_finite (f : Ts -> Rbar)
        {rv : RandomVariable dom Rbar_borel_sa f}
        {nnf : Rbar_NonnegativeFunction f} :
    Rbar_IsFiniteExpectation f ->
    almost prts (fun x => is_finite (f x)).

  Lemma Rbar_IsFiniteExpectation_proper_almostR2 rv_X1 rv_X2
        {rv1:RandomVariable dom Rbar_borel_sa rv_X1}
        {rv2:RandomVariable dom Rbar_borel_sa rv_X2} :
    Rbar_IsFiniteExpectation rv_X1 ->
    almostR2 prts eq rv_X1 rv_X2 ->
    Rbar_IsFiniteExpectation rv_X2.

    Lemma Rbar_rv_le_pos_fun_part (rv_X1 rv_X2 : Ts -> Rbar) :
      Rbar_rv_le rv_X1 rv_X2 ->
      Rbar_rv_le (fun x : Ts => Rbar_pos_fun_part rv_X1 x)
                 (fun x : Ts => Rbar_pos_fun_part rv_X2 x).

    Lemma Rbar_rv_le_neg_fun_part (rv_X1 rv_X2 : Ts -> Rbar) :
      Rbar_rv_le rv_X1 rv_X2 ->
      Rbar_rv_le (fun x : Ts => Rbar_neg_fun_part rv_X2 x)
                 (fun x : Ts => Rbar_neg_fun_part rv_X1 x).

  Lemma Rbar_IsFiniteExpectation_bounded (rv_X1 rv_X2 rv_X3 : Ts -> Rbar)
        {isfe1:Rbar_IsFiniteExpectation rv_X1}
        {isfe2:Rbar_IsFiniteExpectation rv_X3}
    :
      Rbar_rv_le rv_X1 rv_X2 ->
      Rbar_rv_le rv_X2 rv_X3 ->
      Rbar_IsFiniteExpectation rv_X2.

  
  Lemma Rbar_IsFiniteExpectation_parts f :
    Rbar_IsFiniteExpectation f ->
    Rbar_IsFiniteExpectation (Rbar_pos_fun_part f) /\
    Rbar_IsFiniteExpectation (Rbar_neg_fun_part f).

  Lemma Rbar_IsFiniteExpectation_from_fin_parts (f:Ts->Rbar) :
    Rbar_lt (Rbar_NonnegExpectation (Rbar_pos_fun_part f)) p_infty ->
    Rbar_lt (Rbar_NonnegExpectation (Rbar_neg_fun_part f)) p_infty ->
    Rbar_IsFiniteExpectation f.


  Lemma finexp_almost_finite rv_X
        {rv : RandomVariable dom Rbar_borel_sa rv_X} :
    Rbar_IsFiniteExpectation rv_X ->
    almost prts (fun x => is_finite (rv_X x)).

  Lemma finexp_almost_finite_part rv_X
        {rv : RandomVariable dom Rbar_borel_sa rv_X} :
    Rbar_IsFiniteExpectation rv_X ->
    almostR2 prts eq rv_X (Rbar_finite_part rv_X).


  Global Instance finite_part_rv rv_X
         {rv : RandomVariable dom Rbar_borel_sa rv_X} :
    RandomVariable dom borel_sa (Rbar_finite_part rv_X).

  Lemma finexp_Rbar_exp_finpart rv_X
        {rv : RandomVariable dom Rbar_borel_sa rv_X} :
    Rbar_IsFiniteExpectation rv_X ->
    Rbar_Expectation rv_X = Expectation (Rbar_finite_part rv_X).
  
  Lemma Rbar_finexp_finexp rv_X
        {rv : RandomVariable dom Rbar_borel_sa rv_X} :
    Rbar_IsFiniteExpectation rv_X ->
    IsFiniteExpectation prts (Rbar_finite_part rv_X).

  Global Instance Rbar_IsFiniteExpectation_const (c:R) : Rbar_IsFiniteExpectation (const c).

  Lemma Rbar_finexp_almost_plus rv_X1 rv_X2
        {rv1 : RandomVariable dom Rbar_borel_sa rv_X1}
        {rv2 : RandomVariable dom Rbar_borel_sa rv_X2} :
    Rbar_IsFiniteExpectation rv_X1 ->
    Rbar_IsFiniteExpectation rv_X2 ->
    almostR2 prts eq (Rbar_rvplus rv_X1 rv_X2) (rvplus (Rbar_finite_part rv_X1) (Rbar_finite_part rv_X2)).

  Global Instance Rbar_is_finite_expectation_isfe_plus
         (rv_X1 rv_X2 : Ts -> Rbar)
         {rv1 : RandomVariable dom Rbar_borel_sa rv_X1}
         {rv2 : RandomVariable dom Rbar_borel_sa rv_X2}
         {isfe1: Rbar_IsFiniteExpectation rv_X1}
         {isfe2: Rbar_IsFiniteExpectation rv_X2} :
    Rbar_IsFiniteExpectation (Rbar_rvplus rv_X1 rv_X2).

  Global Instance Rbar_IsFiniteExpectation_proper :
    Proper (rv_eq ==> iff) Rbar_IsFiniteExpectation.

  Global Instance Rbar_mult_eq_proper
          : Proper (rv_eq ==> rv_eq ==> rv_eq) (@Rbar_rvmult Ts).

  Global Instance Rbar_IsFiniteExpectation_min
         (rv_X1 rv_X2 : Ts -> Rbar)
         {rv1 : RandomVariable dom Rbar_borel_sa rv_X1}
         {rv2 : RandomVariable dom Rbar_borel_sa rv_X2}
         {isfe1:Rbar_IsFiniteExpectation rv_X1}
         {isfe2:Rbar_IsFiniteExpectation rv_X2} :
    Rbar_IsFiniteExpectation (Rbar_rvmin rv_X1 rv_X2).

  Global Instance Rbar_IsFiniteExpectation_max
         (rv_X1 rv_X2 : Ts -> Rbar)
         {rv1 : RandomVariable dom Rbar_borel_sa rv_X1}
         {rv2 : RandomVariable dom Rbar_borel_sa rv_X2}
         {isfe1:Rbar_IsFiniteExpectation rv_X1}
         {isfe2:Rbar_IsFiniteExpectation rv_X2} :
    Rbar_IsFiniteExpectation (Rbar_rvmax rv_X1 rv_X2).

  Global Instance Rbar_IsFiniteExpectation_choice
         (c: Ts -> bool) (rv_X1 rv_X2 : Ts -> Rbar)
         {rv1 : RandomVariable dom Rbar_borel_sa rv_X1}
         {rv2 : RandomVariable dom Rbar_borel_sa rv_X2}
         {isfe1:Rbar_IsFiniteExpectation rv_X1}
         {isfe2:Rbar_IsFiniteExpectation rv_X2} :
    Rbar_IsFiniteExpectation (Rbar_rvchoice c rv_X1 rv_X2).

  
  Global Instance Rbar_IsFiniteExpectation_scale c f :
    Rbar_IsFiniteExpectation f ->
    Rbar_IsFiniteExpectation (Rbar_rvmult (const (Finite c)) f).

  Lemma Rbar_Expectation_const (c:R) :
    Rbar_Expectation (const c) = Some (Finite c).

  Global Instance Rbar_IsFiniteExpectation_indicator f {P} (dec:dec_pre_event P)
       {rv : RandomVariable dom Rbar_borel_sa f}:
  sa_sigma P ->
  Rbar_IsFiniteExpectation f ->
  Rbar_IsFiniteExpectation (Rbar_rvmult f (EventIndicator dec)).

  Lemma Rbar_IsFiniteExpectation_Finite (rv_X:Ts->Rbar)
        {isfe:Rbar_IsFiniteExpectation rv_X} :
    { x : R | Rbar_Expectation rv_X = Some (Finite x)}.

  Definition Rbar_FiniteExpectation (rv_X:Ts->Rbar)
             {isfe:Rbar_IsFiniteExpectation rv_X} : R
    := proj1_sig (Rbar_IsFiniteExpectation_Finite rv_X).


  Ltac Rbar_simpl_finite
    := repeat match goal with
              | [|- context [proj1_sig ?x]] => destruct x; simpl
              | [H: context [proj1_sig ?x] |- _] => destruct x; simpl in H
              end.

  Lemma FinExp_Rbar_FinExp (f:Ts->R)
        {rv:RandomVariable dom borel_sa f}
        {isfe:IsFiniteExpectation prts f}:
    Rbar_FiniteExpectation f =
    FiniteExpectation prts f.

  Lemma Rbar_FiniteExpectation_const (c:R) : Rbar_FiniteExpectation (const c) = c.

  Lemma Rbar_Expectation_sum_finite
        (rv_X1 rv_X2 : Ts -> Rbar)
        {rv1 : RandomVariable dom Rbar_borel_sa rv_X1}
        {rv2 : RandomVariable dom Rbar_borel_sa rv_X2} :
    forall (e1 e2:R),
      Rbar_Expectation rv_X1 = Some (Finite e1) ->
      Rbar_Expectation rv_X2 = Some (Finite e2) ->
      Rbar_Expectation (Rbar_rvplus rv_X1 rv_X2) = Some (Finite (e1 + e2)).

  Lemma pos_part_neg_part_rvplus (f g : Ts -> R) :
    rv_eq
      (rvplus
         (pos_fun_part (rvplus f g))
         (rvplus
            (neg_fun_part f)
            (neg_fun_part g)))
      (rvplus
         (neg_fun_part (Rbar_rvplus f g))
         (rvplus
            (pos_fun_part f)
            (pos_fun_part g))).


  Lemma pos_part_neg_part_Rbar_rvplus (f g : Ts -> Rbar) :
    (forall x, ex_Rbar_plus (f x) (g x)) ->
    rv_eq
      (Rbar_rvplus
         (Rbar_pos_fun_part (Rbar_rvplus f g))
         (Rbar_rvplus
            (Rbar_neg_fun_part f)
            (Rbar_neg_fun_part g)))
      (Rbar_rvplus
         (Rbar_neg_fun_part (Rbar_rvplus f g))
         (Rbar_rvplus
            (Rbar_pos_fun_part f)
            (Rbar_pos_fun_part g))).

  Lemma Rbar_NonnegExpectation_pos_part_neg_part_Rbar_rvplus (f g : Ts -> Rbar)
        {rvf : RandomVariable dom Rbar_borel_sa f}
        {rvg : RandomVariable dom Rbar_borel_sa g} :
    (forall x, ex_Rbar_plus (f x) (g x)) ->
    Rbar_plus
      (Rbar_NonnegExpectation (Rbar_pos_fun_part (Rbar_rvplus f g)))
      (Rbar_plus
          (Rbar_NonnegExpectation (Rbar_neg_fun_part f))
          (Rbar_NonnegExpectation (Rbar_neg_fun_part g))) =
    Rbar_plus
      (Rbar_NonnegExpectation (Rbar_neg_fun_part (Rbar_rvplus f g)))
      (Rbar_plus
         (Rbar_NonnegExpectation (Rbar_pos_fun_part f))
         (Rbar_NonnegExpectation (Rbar_pos_fun_part g))).

    Lemma Rbar_IsFiniteNonnegExpectation (X:Ts->Rbar)
          {posX: Rbar_NonnegativeFunction X}
          {isfeX: Rbar_IsFiniteExpectation X} :
      is_finite (Rbar_NonnegExpectation X).

    Lemma Rbar_pos_sum_bound (rv_X1 rv_X2 : Ts -> Rbar) :
      (forall x, ex_Rbar_plus (rv_X1 x) (rv_X2 x)) ->
      Rbar_rv_le (Rbar_pos_fun_part (Rbar_rvplus rv_X1 rv_X2))
                 (Rbar_rvplus (Rbar_pos_fun_part rv_X1)
                              (Rbar_pos_fun_part rv_X2)).

    Lemma Rbar_neg_sum_bound (rv_X1 rv_X2 : Ts -> Rbar) :
      (forall x, ex_Rbar_plus (rv_X1 x) (rv_X2 x)) ->
      Rbar_rv_le (Rbar_neg_fun_part (Rbar_rvplus rv_X1 rv_X2))
                 (Rbar_rvplus (Rbar_neg_fun_part rv_X1)
                              (Rbar_neg_fun_part rv_X2)).

  Lemma Rbar_Expectation_finite
        (rv_X1 : Ts -> Rbar)
        {rv1 : RandomVariable dom Rbar_borel_sa rv_X1} :
    Rbar_IsFiniteExpectation rv_X1 ->
    is_finite (Rbar_NonnegExpectation (Rbar_pos_fun_part rv_X1)) /\
    is_finite (Rbar_NonnegExpectation (Rbar_neg_fun_part rv_X1)).

  Lemma Rbar_Expectation_pinf
        (rv_X1 : Ts -> Rbar)
        {rv1 : RandomVariable dom Rbar_borel_sa rv_X1} :
    Rbar_Expectation rv_X1 = Some p_infty ->
    Rbar_NonnegExpectation (Rbar_pos_fun_part rv_X1) = p_infty /\
    is_finite (Rbar_NonnegExpectation (Rbar_neg_fun_part rv_X1)).

  Lemma Rbar_Expectation_minf
        (rv_X1 : Ts -> Rbar)
        {rv1 : RandomVariable dom Rbar_borel_sa rv_X1} :
    Rbar_Expectation rv_X1 = Some m_infty ->
    is_finite (Rbar_NonnegExpectation (Rbar_pos_fun_part rv_X1)) /\
    Rbar_NonnegExpectation (Rbar_neg_fun_part rv_X1) = p_infty.

  Lemma Rbar_Expectation_sum_finite_left
        (rv_X1 rv_X2 : Ts -> Rbar)
        {rv1 : RandomVariable dom Rbar_borel_sa rv_X1}
        {rv2 : RandomVariable dom Rbar_borel_sa rv_X2} :
    (forall x, ex_Rbar_plus (rv_X1 x) (rv_X2 x)) ->
    forall (e1:R) (e2:Rbar),
      Rbar_Expectation rv_X1 = Some (Finite e1) ->
      Rbar_Expectation rv_X2 = Some e2 ->
      Rbar_Expectation (Rbar_rvplus rv_X1 rv_X2) = Some (Rbar_plus e1 e2).

  Lemma Rbar_Expectation_sum_finite_right
        (rv_X1 rv_X2 : Ts -> Rbar)
        {rv1 : RandomVariable dom Rbar_borel_sa rv_X1}
        {rv2 : RandomVariable dom Rbar_borel_sa rv_X2} :
    (forall x, ex_Rbar_plus (rv_X1 x) (rv_X2 x)) ->
    forall (e1:Rbar) (e2:R),
      Rbar_Expectation rv_X1 = Some e1 ->
      Rbar_Expectation rv_X2 = Some (Finite e2) ->
      Rbar_Expectation (Rbar_rvplus rv_X1 rv_X2) = Some (Rbar_plus e1 e2).

  Lemma Rbar_Expectation_sum
        (rv_X1 rv_X2 : Ts -> Rbar)
        {rv1 : RandomVariable dom Rbar_borel_sa rv_X1}
        {rv2 : RandomVariable dom Rbar_borel_sa rv_X2} :
    (forall x, ex_Rbar_plus (rv_X1 x) (rv_X2 x)) ->
    forall (e1 e2:Rbar),
      Rbar_Expectation rv_X1 = Some e1 ->
      Rbar_Expectation rv_X2 = Some e2 ->
      ex_Rbar_plus e1 e2 ->
      Rbar_Expectation (Rbar_rvplus rv_X1 rv_X2) = Some (Rbar_plus e1 e2).
   
  Lemma Rbar_Expectation_minus_finite
        (rv_X1 rv_X2 : Ts -> Rbar)
        {rv1 : RandomVariable dom Rbar_borel_sa rv_X1}
        {rv2 : RandomVariable dom Rbar_borel_sa rv_X2} :
    forall (e1 e2:R),
      Rbar_Expectation rv_X1 = Some (Finite e1) ->
      Rbar_Expectation rv_X2 = Some (Finite e2) ->
      Rbar_Expectation (Rbar_rvminus rv_X1 rv_X2) = Some (Finite (e1 - e2)).

  Lemma Rbar_FiniteExpectation_Rbar_Expectation (rv_X:Ts->Rbar)
        {isfe:Rbar_IsFiniteExpectation rv_X} :
    Rbar_Expectation rv_X = Some (Finite (Rbar_FiniteExpectation rv_X)).

  Lemma Rbar_FiniteExpectation_Rbar_NonnegExpectation (rv_X:Ts->Rbar)
        {nnf:Rbar_NonnegativeFunction rv_X}
        {isfe:Rbar_IsFiniteExpectation rv_X} :
    Rbar_NonnegExpectation rv_X = Finite (Rbar_FiniteExpectation rv_X).

  
  Lemma Rbar_FiniteExpectation_proper_almostR2 (rv_X1 rv_X2 : Ts -> Rbar)
        {rrv1:RandomVariable dom Rbar_borel_sa rv_X1}
        {rrv2:RandomVariable dom Rbar_borel_sa rv_X2}
        {isfe1:Rbar_IsFiniteExpectation rv_X1}
        {isfe2:Rbar_IsFiniteExpectation rv_X2}
    :
      almostR2 prts eq rv_X1 rv_X2 ->
      Rbar_FiniteExpectation rv_X1 = Rbar_FiniteExpectation rv_X2.

  Lemma Rbar_FiniteExpectation_plus
        (rv_X1 rv_X2 : Ts -> Rbar)
        {rv1 : RandomVariable dom Rbar_borel_sa rv_X1}
        {rv2 : RandomVariable dom Rbar_borel_sa rv_X2}
        {isfe1:Rbar_IsFiniteExpectation rv_X1}
        {isfe2:Rbar_IsFiniteExpectation rv_X2} :
    Rbar_FiniteExpectation (Rbar_rvplus rv_X1 rv_X2) =
    Rbar_FiniteExpectation rv_X1 + Rbar_FiniteExpectation rv_X2.

  Lemma Rbar_IsFiniteExpectation_opp (rv_X : Ts -> Rbar)
        {rv : RandomVariable dom Rbar_borel_sa rv_X}
        {isfe: Rbar_IsFiniteExpectation rv_X} :
    Rbar_IsFiniteExpectation (Rbar_rvopp rv_X).

  Global Instance Rbar_is_finite_expectation_isfe_minus
         (rv_X1 rv_X2 : Ts -> Rbar)
         {rv1 : RandomVariable dom Rbar_borel_sa rv_X1}
         {rv2 : RandomVariable dom Rbar_borel_sa rv_X2}
         {isfe1: Rbar_IsFiniteExpectation rv_X1}
         {isfe2: Rbar_IsFiniteExpectation rv_X2} :
    Rbar_IsFiniteExpectation (Rbar_rvminus rv_X1 rv_X2).
  
  Lemma Rbar_FiniteExpectation_minus
        (rv_X1 rv_X2 : Ts -> Rbar)
        {rv1 : RandomVariable dom Rbar_borel_sa rv_X1}
        {rv2 : RandomVariable dom Rbar_borel_sa rv_X2}
        {isfe1:Rbar_IsFiniteExpectation rv_X1}
        {isfe2:Rbar_IsFiniteExpectation rv_X2} :
    Rbar_FiniteExpectation (Rbar_rvminus rv_X1 rv_X2) =
    Rbar_FiniteExpectation rv_X1 - Rbar_FiniteExpectation rv_X2.

  Lemma Rbar_NonnegExpectation_minus_bounded2
        (rv_X1 : Ts -> Rbar)
        (rv_X2 : Ts -> Rbar)
        {rv1 : RandomVariable dom Rbar_borel_sa rv_X1}
        {rv2 : RandomVariable dom Rbar_borel_sa rv_X2}
        {nnf1:Rbar_NonnegativeFunction rv_X1}
        (c:R)
        (cpos:0 <= c)
        (bounded2: Rbar_rv_le rv_X2 (const c))
        {nnf2:Rbar_NonnegativeFunction rv_X2}
        {nnf12:Rbar_NonnegativeFunction (Rbar_rvminus rv_X1 rv_X2)} :
    Rbar_NonnegExpectation (Rbar_rvminus rv_X1 rv_X2) =
    Rbar_minus (Rbar_NonnegExpectation rv_X1) (Rbar_NonnegExpectation rv_X2).

  Lemma Rbar_FiniteExpectation_ext rv_X1 rv_X2
        {isfe1:Rbar_IsFiniteExpectation rv_X1}
        {isfe2:Rbar_IsFiniteExpectation rv_X2}
        (eqq: rv_eq rv_X1 rv_X2)
    :
    Rbar_FiniteExpectation rv_X1 = Rbar_FiniteExpectation rv_X2.
           
  Lemma Rbar_FiniteExpectation_ext_alt {rv_X1 rv_X2}
        {isfe1:Rbar_IsFiniteExpectation rv_X1}
        (eqq: rv_eq rv_X1 rv_X2)
    :
      Rbar_FiniteExpectation rv_X1 =
      Rbar_FiniteExpectation rv_X2 (isfe:=proj1 (Rbar_IsFiniteExpectation_proper _ _ eqq) isfe1).

Theorem Dominated_convergence
          (fn : nat -> Ts -> Rbar)
          (f : Ts -> Rbar) (g : Ts -> R)
          {rvn : forall n, RandomVariable dom Rbar_borel_sa (fn n)}
          {rvf : RandomVariable dom Rbar_borel_sa f}
          {rvg : RandomVariable dom Rbar_borel_sa g}
          {isfefn : forall n, Rbar_IsFiniteExpectation (fn n)}
          {isfef: Rbar_IsFiniteExpectation f}
          {isfeg: Rbar_IsFiniteExpectation g} :
    (forall n, Rbar_rv_le (Rbar_rvabs (fn n)) g) ->
    (forall x, is_Elim_seq (fun n => fn n x) (f x)) ->
    is_lim_seq (fun n => Rbar_FiniteExpectation (fn n)) (Rbar_FiniteExpectation f).

  Theorem Dominated_convergence_almost
          (fn : nat -> Ts -> Rbar)
          (f g : Ts -> Rbar)
          {rvn : forall n, RandomVariable dom Rbar_borel_sa (fn n)}
          {rvf : RandomVariable dom Rbar_borel_sa f}
          {rvg : RandomVariable dom Rbar_borel_sa g}
          {isfefn : forall n, Rbar_IsFiniteExpectation (fn n)}
          {isfe: Rbar_IsFiniteExpectation f} :
    Rbar_IsFiniteExpectation g ->
    (forall n, almostR2 prts Rbar_le (Rbar_rvabs (fn n)) g) ->
    (almost prts (fun x => is_Elim_seq (fun n => fn n x) (f x))) ->
    is_lim_seq (fun n => Rbar_FiniteExpectation (fn n)) (Rbar_FiniteExpectation f).

  
End almost.

Section sa_sub.

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

    
  Lemma Rbar_NonnegExpectation_prob_space_sa_sub
        (x:Ts->Rbar)
        {pofrf:Rbar_NonnegativeFunction x}
        {rv:RandomVariable dom2 Rbar_borel_sa x}
        
    :
      @Rbar_NonnegExpectation Ts dom2 (prob_space_sa_sub prts sub) x pofrf =
      @Rbar_NonnegExpectation Ts dom prts x pofrf.

  Lemma Rbar_Expectation_prob_space_sa_sub
        (x:Ts->Rbar)
        {rv:RandomVariable dom2 Rbar_borel_sa x} :
    @Rbar_Expectation Ts dom2 (prob_space_sa_sub prts sub) x =
    @Rbar_Expectation Ts dom prts x.

  Lemma Rbar_IsFiniteExpectation_prob_space_sa_sub
        (x:Ts->Rbar)
        {rv:RandomVariable dom2 Rbar_borel_sa x}
        {isfe:Rbar_IsFiniteExpectation (prob_space_sa_sub prts sub) x} :
    Rbar_IsFiniteExpectation prts x.

  Lemma Rbar_IsFiniteExpectation_prob_space_sa_sub_f
        (x:Ts->Rbar)
        {rv:RandomVariable dom2 Rbar_borel_sa x}
        {isfe:Rbar_IsFiniteExpectation prts x} :
    Rbar_IsFiniteExpectation (prob_space_sa_sub prts sub) x.
  
End sa_sub.

Section more_stuff.

    Lemma Rbar_NonnegExpectation_const_pinfty {Ts} {dom: SigmaAlgebra Ts} (prts:ProbSpace dom)
        (pf:Rbar_NonnegativeFunction (const (B:=Ts) p_infty)) :
    Rbar_NonnegExpectation (const p_infty) = p_infty.

  Lemma Rbar_NonnegExpectation_const' {Ts} {dom: SigmaAlgebra Ts} (prts:ProbSpace dom)
        (c : Rbar) (nneg:Rbar_le 0 c) (nnf:Rbar_NonnegativeFunction (const (B:=Ts) c)) :
    Rbar_NonnegExpectation (const c) = c.

  Lemma Rbar_NonnegExpectation_inf_mult_indicator {Ts} {dom: SigmaAlgebra Ts} (prts:ProbSpace dom)
        {P : event dom}
        (dec : dec_event P)
        {pofrf:Rbar_NonnegativeFunction (Rbar_rvmult (const p_infty) (EventIndicator dec))} :
    ps_P P <> 0 ->
    Rbar_NonnegExpectation (Rbar_rvmult (const p_infty) (EventIndicator dec)) = p_infty.
    
  Lemma Rbar_NonnegExpectation_pinfty_prob {Ts} {dom: SigmaAlgebra Ts} (prts:ProbSpace dom)
        rv_X
        {rv:RandomVariable dom Rbar_borel_sa rv_X}
        {pofrf:Rbar_NonnegativeFunction rv_X} :
    ps_P (exist _ _ (sa_pinf_Rbar rv_X rv)) <> 0 ->
    Rbar_NonnegExpectation rv_X = p_infty.

  
  Lemma Rbar_NonnegExpectation_scale' {Ts} {dom: SigmaAlgebra Ts} (prts:ProbSpace dom) c
        (rv_X : Ts -> Rbar)
        {rv:RandomVariable dom Rbar_borel_sa rv_X}
        {pofrf:Rbar_NonnegativeFunction rv_X}
        {pofrf2:Rbar_NonnegativeFunction (Rbar_rvmult (const c) rv_X)} :
    Rbar_le 0 c ->
    Rbar_NonnegExpectation (Rbar_rvmult (const c) rv_X) =
    Rbar_mult c (Rbar_NonnegExpectation rv_X).

  Lemma sum_Rbar_n_rv {Ts} {dom: SigmaAlgebra Ts}
        (Xn : nat -> Ts -> Rbar)
        (Xn_rv : forall n, RandomVariable dom Rbar_borel_sa (Xn n)) :
    forall n,
      RandomVariable dom Rbar_borel_sa (fun a : Ts => sum_Rbar_n (fun n=> Xn n a) n).

  Lemma Rbar_NonnegExpectation_sum {Ts} {dom: SigmaAlgebra Ts} (prts:ProbSpace dom)
        (Xn : nat -> Ts -> Rbar)
        (Xn_rv : forall n, RandomVariable dom Rbar_borel_sa (Xn n))
        (Xn_pos : forall n, Rbar_NonnegativeFunction (Xn n))
        (Xlim_pos : forall n, Rbar_NonnegativeFunction (fun omega : Ts => sum_Rbar_n (fun n : nat => Xn n omega) n))
    : forall n,
    sum_Rbar_n (fun n => Rbar_NonnegExpectation (Xn n)) n =
      Rbar_NonnegExpectation (fun omega => sum_Rbar_n (fun n => (Xn n omega)) n).

  Lemma Rbar_series_expectation {Ts} {dom: SigmaAlgebra Ts} (prts:ProbSpace dom)
        (Xn : nat -> Ts -> Rbar)
        (Xn_rv : forall n, RandomVariable dom Rbar_borel_sa (Xn n))
        (Xn_pos : forall n, Rbar_NonnegativeFunction (Xn n))
        (Xlim_pos : Rbar_NonnegativeFunction (fun omega : Ts => ELim_seq (sum_Rbar_n (fun n : nat => Xn n omega))))
    :
    ELim_seq
      (sum_Rbar_n
         (fun n : nat =>
            Rbar_NonnegExpectation (Xn n))) =
      Rbar_NonnegExpectation (fun omega => ELim_seq (sum_Rbar_n (fun n => (Xn n omega)))).

  
  Lemma Rbar_is_finite_expectation_isfe_minus1
        {Ts} {dom: SigmaAlgebra Ts} (prts:ProbSpace dom)
          (rv_X1 rv_X2 : Ts -> Rbar)
          {rv1:RandomVariable dom Rbar_borel_sa rv_X1}
          {rv2:RandomVariable dom Rbar_borel_sa rv_X2}
          {isfe1:Rbar_IsFiniteExpectation prts rv_X2}
          {isfe2:Rbar_IsFiniteExpectation prts (Rbar_rvminus rv_X1 rv_X2)} :
      Rbar_IsFiniteExpectation prts rv_X1.

    Local Existing Instance Rbar_le_pre.

    Lemma Rbar_NonnegExpectation_almostR2_le
          {Ts} {dom: SigmaAlgebra Ts} (prts:ProbSpace dom)
          (rv_X1 rv_X2 : Ts -> Rbar)
          {rv1:RandomVariable dom Rbar_borel_sa rv_X1}
          {rv2:RandomVariable dom Rbar_borel_sa rv_X2}
          {nnf1 : Rbar_NonnegativeFunction rv_X1}
          {nnf2 : Rbar_NonnegativeFunction rv_X2} :
      almostR2 _ Rbar_le rv_X1 rv_X2 ->
      Rbar_le (Rbar_NonnegExpectation rv_X1) (Rbar_NonnegExpectation rv_X2).
  
  Lemma ELimInf_seq_pos_fun_part {Ts} f :
    Rbar_rv_le
      (fun x : Ts => Rbar_pos_fun_part (fun omega : Ts => ELimInf_seq (fun n : nat => f n omega)) x)
      (fun x : Ts => (fun omega : Ts => ELimInf_seq (fun n : nat => (Rbar_pos_fun_part (f n)) omega)) x).
  
  Lemma ELimInf_seq_sup_neg_fun_part {Ts} f :
    Rbar_rv_le
      (Rbar_neg_fun_part (fun omega : Ts => ELimSup_seq (fun n : nat => f n omega)))
      (fun omega : Ts =>
         ELimInf_seq (fun n : nat => Rbar_neg_fun_part (fun x : Ts => f n x) omega)).

  Lemma ELimInf_seq_neg_fun_part {Ts} f ts :
    ex_Elim_seq (fun n => f n ts) ->
    Rbar_le
      ((Rbar_neg_fun_part (fun omega : Ts => ELimInf_seq (fun n : nat => f n omega))) ts)
      (ELimInf_seq (fun n : nat => Rbar_neg_fun_part (fun x : Ts => f n x) ts)).

End more_stuff.