Module FormalML.ProbTheory.RealRandomVariable

Require Import Qreals.
Require Import Reals.

Require Import Lra Lia.
Require Import List Permutation.
Require Import Morphisms EquivDec Program Equivalence.
Require Import Coquelicot.Coquelicot.
Require Import Classical_Prop.
Require Import Classical.
Require Import IndefiniteDescription ClassicalDescription.

Require Import Utils.
Require Import NumberIso.
Require Import SigmaAlgebras.
Require Export Almost.
Require Export FunctionsToReal ProbSpace BorelSigmaAlgebra.
Require Export RandomVariable.

Import ListNotations.

Set Bullet Behavior "Strict Subproofs".

Section RealRandomVariables.

  Lemma borel_singleton (c:R) :
    sa_sigma (SigmaAlgebra:=borel_sa) (pre_event_singleton c).

  Global Instance borel_has_preimages : HasPreimageSingleton borel_sa.

  Global Instance Rbar_borel_has_preimages : HasPreimageSingleton Rbar_borel_sa.

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

  Section measurable.

    Class RealMeasurable (f: Ts -> R)
      := rmeasurable : forall (r:R), sa_sigma (fun omega : Ts => f omega <= r).

    Instance measurable_rv (rv_X:Ts->R)
             {rm:RealMeasurable rv_X}
      : RandomVariable dom borel_sa rv_X.

    Instance rv_measurable (rv_X:Ts->R)
             {rrv:RandomVariable dom borel_sa rv_X}
      : RealMeasurable rv_X | 3.


    Global Instance RealMeasurable_proper :
      Proper (rv_eq ==> iff) RealMeasurable.
    
    Instance scale_measurable_pos (f : Ts -> R) (c:posreal) :
      RealMeasurable f ->
      RealMeasurable (rvscale c f).

    Instance scale_measurable_neg (f : Ts -> R) (c:posreal) :
      RealMeasurable f ->
      RealMeasurable (rvscale (- c) f).

    Instance constant_measurable (c:R) :
      RealMeasurable (const c).

    Instance scale_measurable (f : Ts -> R) (c:R) :
      RealMeasurable f ->
      RealMeasurable (rvscale c f).

    Lemma sa_sigma_inter_pts
          (rv_X1 rv_X2 : Ts -> R)
          {rv1: RandomVariable dom borel_sa rv_X1}
          {rv2: RandomVariable dom borel_sa rv_X2}
          (c1 c2 : R) :
      sa_sigma (fun omega : Ts => rv_X1 omega = c1 /\
                                  rv_X2 omega = c2).

    
    Instance Ropp_measurable (f : Ts -> R) :
      RealMeasurable f ->
      RealMeasurable (rvopp f).

    Instance plus_measurable (f g : Ts -> R) :
      RealMeasurable f ->
      RealMeasurable g ->
      RealMeasurable (rvplus f g).

    Instance rvsum_measurable
             (Xn : nat -> Ts -> R)
             (Xn_rv : forall n, RealMeasurable (Xn n)) :
      forall (n:nat), RealMeasurable (rvsum Xn n).

    Instance rvsum_measurable_loc (n:nat)
             (Xn : nat -> Ts -> R)
             (Xn_rv : forall m, (m <= n)%nat -> RealMeasurable (Xn m)) :
      RealMeasurable (rvsum Xn n).

    Instance minus_measurable (f g : Ts -> R) :
      RealMeasurable f ->
      RealMeasurable g ->
      RealMeasurable (rvminus f g).
    
    Instance Rsqr_pos_measurable (f : Ts -> R) :
      (forall (x:Ts), (0 <= f x)%R) ->
      RealMeasurable f ->
      RealMeasurable (rvsqr f).

    Lemma measurable_open_continuous (f : Ts -> R) (g : R -> R) :
      continuity g ->
      (forall B: pre_event R, open_set B -> sa_sigma (pre_event_preimage f B)) ->
      (forall B: pre_event R, open_set B ->
                              sa_sigma (pre_event_preimage (fun omega => g (f omega)) B)).

    Instance measurable_continuous (f : Ts -> R) (g : R -> R) :
      continuity g ->
      RealMeasurable f ->
      RealMeasurable (compose g f).

    Instance rvpow_measurable (f : Ts -> R) n :
      RealMeasurable f ->
      RealMeasurable (rvpow f n).

    Instance Rsqr_measurable (f : Ts -> R) :
      RealMeasurable f ->
      RealMeasurable (rvsqr f).

    Instance mult_measurable (f g : Ts -> R) :
      RealMeasurable f ->
      RealMeasurable g ->
      RealMeasurable (rvmult f g).

    Instance Rabs_measurable f :
      RealMeasurable f ->
      RealMeasurable (rvabs f).

    Instance Rsqrt_measurable f :
      RealMeasurable f ->
      RealMeasurable (rvsqrt f).

    Instance max_measurable (f g : Ts -> R) :
      RealMeasurable f ->
      RealMeasurable g ->
      RealMeasurable (rvmax f g).

    Instance min_measurable (f g : Ts -> R) :
      RealMeasurable f ->
      RealMeasurable g ->
      RealMeasurable (rvmin f g).

    Instance rvclip_measurable (f : Ts -> R) (c : nonnegreal) :
      RealMeasurable f ->
      RealMeasurable (rvclip f c).

    Instance pos_fun_part_measurable (f : Ts -> R) :
      RealMeasurable f ->
      RealMeasurable (pos_fun_part f).

    Instance neg_fun_partmeasurable (f : Ts -> R) :
      RealMeasurable f ->
      RealMeasurable (neg_fun_part f).

    Instance rvchoice_measurable (c f g : Ts -> R) :
      RealMeasurable c ->
      RealMeasurable f ->
      RealMeasurable g ->
      RealMeasurable (rvchoice (fun x => if Req_EM_T (c x) 0 then false else true) f g).

    Definition Rbar_rvchoice (c:Ts -> bool) (rv_X1 rv_X2 : Ts -> Rbar)
      := fun omega => if c omega then rv_X1 omega else rv_X2 omega.

    Instance Rbar_rvchoice_measurable (c : Ts -> R) (f g : Ts -> Rbar) :
      RealMeasurable c ->
      RbarMeasurable f ->
      RbarMeasurable g ->
      RbarMeasurable (Rbar_rvchoice (fun x => if Req_EM_T (c x) 0 then false else true) f g).

    Instance ln_measurable (b : Ts -> R) :
      RealMeasurable b ->
      RealMeasurable (fun (x:Ts) => ln (b x)).

    Instance exp_measurable (b : Ts -> R) :
      RealMeasurable b ->
      RealMeasurable (fun (x:Ts) => exp (b x)).
    
    Instance Rpower_measurable (b e : Ts -> R) :
      RealMeasurable b ->
      RealMeasurable e ->
      RealMeasurable (fun (x:Ts) => Rpower (b x) (e x)).

    Instance rvpower_measurable (b e : Ts -> R) :
      RealMeasurable b ->
      RealMeasurable e ->
      RealMeasurable (rvpower b e).
    
    Definition rvlim (f : nat -> Ts -> R) : (Ts -> R) :=
      (fun omega => real (Lim_seq (fun n => f n omega))).

    Instance LimSup_measurable (f : nat -> Ts -> R) :
      (forall n, RealMeasurable (f n)) ->
      (forall omega, is_finite (LimSup_seq (fun n => f n omega))) ->
      RealMeasurable (fun omega => LimSup_seq (fun n => f n omega)).

    Lemma x_plus_x_div_2 (x : Rbar) :
      (Rbar_div_pos (Rbar_plus x x ) (mkposreal 2 Rlt_R0_R2)) = x.

    Instance rvlim_measurable (f : nat -> Ts -> R) :
      (forall n, RealMeasurable (f n)) ->
      (forall (omega:Ts), ex_finite_lim_seq (fun n => f n omega)) ->
      RealMeasurable (rvlim f).

    Section rvs.

      Global Instance rvlim_rv (f: nat -> Ts -> R)
             {rv : forall n, RandomVariable dom borel_sa (f n)} :
        (forall (omega:Ts), ex_finite_lim_seq (fun n => f n omega)) ->
        RandomVariable dom borel_sa (rvlim f).

      Global Instance rvscale_rv (c: R) (rv_X : Ts -> R)
             (rv : RandomVariable dom borel_sa rv_X)
        : RandomVariable dom borel_sa (rvscale c rv_X).

      Global Instance rvopp_rv (rv_X : Ts -> R)
             {rv : RandomVariable dom borel_sa rv_X}
        : RandomVariable dom borel_sa (rvopp rv_X).

      Global Instance rvclip_rv (rv_X : Ts -> R) (c:nonnegreal)
             {rv : RandomVariable dom borel_sa rv_X}
        : RandomVariable dom borel_sa (rvclip rv_X c).

      Global Instance rvplus_rv (rv_X1 rv_X2 : Ts -> R)
             {rv1 : RandomVariable dom borel_sa rv_X1}
             {rv2 : RandomVariable dom borel_sa rv_X2} :
        RandomVariable dom borel_sa (rvplus rv_X1 rv_X2).

      Instance rvsum_rv (Xn : nat -> Ts -> R)
             {rv : forall (n:nat), RandomVariable dom borel_sa (Xn n)} :
        forall (n:nat), RandomVariable dom borel_sa (rvsum Xn n).

      Global Instance rvsum_rv_loc (n:nat)
             (Xn : nat -> Ts -> R)
             (Xn_rv : forall m, (m <= n)%nat -> RandomVariable dom borel_sa (Xn m)) :
        RandomVariable dom borel_sa (rvsum Xn n).

      Global Instance rvminus_rv
             (rv_X1 rv_X2 : Ts -> R)
             {rv1 : RandomVariable dom borel_sa rv_X1}
             {rv2 : RandomVariable dom borel_sa rv_X2} :
        RandomVariable dom borel_sa (rvminus rv_X1 rv_X2) :=
        rvplus_rv rv_X1 (rvopp rv_X2).

      Global Instance rvmult_rv
             (rv_X1 rv_X2 : Ts -> R)
             {rv1 : RandomVariable dom borel_sa rv_X1}
             {rv2 : RandomVariable dom borel_sa rv_X2} :
        RandomVariable dom borel_sa (rvmult rv_X1 rv_X2).

      Global Instance rvpow_rv (rv_X : Ts -> R) n :
        RandomVariable dom borel_sa rv_X ->
        RandomVariable dom borel_sa (rvpow rv_X n).

      Global Instance rvpower_rv
             (rv_X1 rv_X2 : Ts -> R)
             {rv1 : RandomVariable dom borel_sa rv_X1}
             {rv2 : RandomVariable dom borel_sa rv_X2} :
        RandomVariable dom borel_sa (rvpower rv_X1 rv_X2).

      Global Instance rvsqr_rv
             (rv_X : Ts -> R)
             {rv : RandomVariable dom borel_sa rv_X} :
        RandomVariable dom borel_sa (rvsqr rv_X).

      Global Instance rvabs_rv
             (rv_X : Ts -> R)
             {rv : RandomVariable dom borel_sa rv_X} :
        RandomVariable dom borel_sa (rvabs rv_X).

      Global Instance rvsqrt_rv
             (rv_X : Ts -> R)
             {rv : RandomVariable dom borel_sa rv_X} :
        RandomVariable dom borel_sa (rvsqrt rv_X).

      Global Instance rvmax_rv
             (rv_X1 rv_X2 : Ts -> R)
             {rv1 : RandomVariable dom borel_sa rv_X1}
             {rv2 : RandomVariable dom borel_sa rv_X2} :
        RandomVariable dom borel_sa (rvmax rv_X1 rv_X2).
      
      Global Instance rvmin_rv
             (rv_X1 rv_X2 : Ts -> R)
             {rv1 : RandomVariable dom borel_sa rv_X1}
             {rv2 : RandomVariable dom borel_sa rv_X2} :
        RandomVariable dom borel_sa (rvmin rv_X1 rv_X2).

      Global Instance positive_part_rv
             (rv_X : Ts -> R)
             (rv : RandomVariable dom borel_sa rv_X) :
        RandomVariable dom borel_sa (pos_fun_part rv_X).

      Global Instance negative_part_rv
             (rv_X : Ts -> R)
             (rv : RandomVariable dom borel_sa rv_X) :
        RandomVariable dom borel_sa (neg_fun_part rv_X).

      Global Instance positive_part_rv'
             (rv_X : Ts -> R)
             (rv : RandomVariable dom borel_sa rv_X) :
        RandomVariable dom borel_sa (fun x => (pos_fun_part rv_X) x).

      Global Instance negative_part_rv'
             (rv_X : Ts -> R)
             (rv : RandomVariable dom borel_sa rv_X) :
        RandomVariable dom borel_sa (fun x => neg_fun_part rv_X x).

      Global Instance rvchoice_rv
             (rv_C rv_X1 rv_X2 : Ts -> R)
             {rvc : RandomVariable dom borel_sa rv_C}
             {rv1 : RandomVariable dom borel_sa rv_X1}
             {rv2 : RandomVariable dom borel_sa rv_X2} :
        RandomVariable dom borel_sa (rvchoice (fun x => if Req_EM_T (rv_C x) 0 then false else true) rv_X1 rv_X2).

      Instance continuous_compose_rv
               (f: Ts -> R) (g:R->R)
               {frv : RandomVariable dom borel_sa f}
               (gcont : continuity g) :
        RandomVariable dom borel_sa (compose g f).

      Global Instance rvsign_rv (X : Ts -> R)
             {rv : RandomVariable dom borel_sa X} :
        RandomVariable dom borel_sa (rvsign X).

    End rvs.

  End measurable.

  Section Const.

    Global Program Instance scale_constant_random_variable (c: R)
           (rv_X : Ts -> R)
           {crv:ConstantRangeFunction rv_X} : ConstantRangeFunction (rvscale c rv_X)
      := { frf_val := Rmult c frf_val }.

  End Const.

  Section Simple.
    
    Global Program Instance frfscale (c: R)
           (rv_X : Ts -> R)
           {frf:FiniteRangeFunction rv_X} : FiniteRangeFunction (rvscale c rv_X)
      := { frf_vals := map (fun v => Rmult c v) frf_vals }.

    Global Instance frfopp
           {rv_X : Ts -> R}
           {frf:FiniteRangeFunction rv_X} : FiniteRangeFunction (rvopp rv_X)
      := frfscale (-1) rv_X.

    Global Program Instance frfplus
           (rv_X1 rv_X2 : Ts -> R)
           {frf1:FiniteRangeFunction rv_X1}
           {frf2:FiniteRangeFunction rv_X2}
      : FiniteRangeFunction (rvplus rv_X1 rv_X2)
      := { frf_vals := map (fun ab => Rplus (fst ab) (snd ab))
                           (list_prod (frf_vals (FiniteRangeFunction:=frf1))
                                      (frf_vals (FiniteRangeFunction:=frf2))) }.

    Global Instance frfminus
           (rv_X1 rv_X2 : Ts -> R)
           {frf1 : FiniteRangeFunction rv_X1}
           {frf2 : FiniteRangeFunction rv_X2} :
      FiniteRangeFunction (rvminus rv_X1 rv_X2) :=
      frfplus rv_X1 (rvopp rv_X2).

    Global Program Instance frfmult
           (rv_X1 rv_X2 : Ts -> R)
           {frf1:FiniteRangeFunction rv_X1}
           {frf2:FiniteRangeFunction rv_X2}
      : FiniteRangeFunction (rvmult rv_X1 rv_X2)
      := { frf_vals := map (fun ab => Rmult (fst ab) (snd ab))
                           (list_prod (frf_vals (FiniteRangeFunction:=frf1))
                                      (frf_vals (FiniteRangeFunction:=frf2))) }.

    Global Program Instance frfsqr
           (rv_X : Ts -> R)
           {frf:FiniteRangeFunction rv_X} : FiniteRangeFunction (rvsqr rv_X)
      := { frf_vals := map Rsqr frf_vals }.

    Global Program Instance frfsqrt
           (rv_X : Ts -> R)
           {frf:FiniteRangeFunction rv_X} : FiniteRangeFunction (rvsqrt rv_X)
      := { frf_vals := map sqrt frf_vals }.

    Global Program Instance frfpow
           (rv_X : Ts -> R) n
           {frf:FiniteRangeFunction rv_X} : FiniteRangeFunction (rvpow rv_X n)
      := { frf_vals := map (fun x => pow x n) frf_vals }.

    Global Program Instance frfabs
           (rv_X : Ts -> R)
           {frf:FiniteRangeFunction rv_X} : FiniteRangeFunction (rvabs rv_X)
      := { frf_vals := map Rabs frf_vals }.

    Lemma sign_vals :
      forall (x:R),
        -1 = sign x \/ 0 = sign x \/ 1 = sign x.

    Global Program Instance frfsign
           (rv_X : Ts -> R) : FiniteRangeFunction (rvsign rv_X)
      := { frf_vals := (-1) :: 0 :: 1 :: nil }.

    Global Instance frfchoice (c:Ts->bool) x y
           {frfx:FiniteRangeFunction x}
           {frfy:FiniteRangeFunction y}
      : FiniteRangeFunction (rvchoice c x y).
    
    Global Program Instance frfmax
           (rv_X1 rv_X2 : Ts -> R)
           {frf1:FiniteRangeFunction rv_X1}
           {frf2:FiniteRangeFunction rv_X2}
      : FiniteRangeFunction (rvmax rv_X1 rv_X2)
      := { frf_vals := map (fun ab => Rmax (fst ab) (snd ab))
                           (list_prod (frf_vals (FiniteRangeFunction:=frf1))
                                      (frf_vals (FiniteRangeFunction:=frf2))) }.

    Global Program Instance frfmin
           (rv_X1 rv_X2 : Ts -> R)
           {frf1:FiniteRangeFunction rv_X1}
           {frf2:FiniteRangeFunction rv_X2}
      : FiniteRangeFunction (rvmin rv_X1 rv_X2)
      := { frf_vals := map (fun ab => Rmin (fst ab) (snd ab))
                           (list_prod (frf_vals (FiniteRangeFunction:=frf1))
                                      (frf_vals (FiniteRangeFunction:=frf2))) }.

    Global Instance frfsum (X : nat -> Ts -> R)
           {rv : forall (n:nat), FiniteRangeFunction (X n)} (n : nat) :
      FiniteRangeFunction (rvsum X n).
    
    Global Program Instance positive_part_frf'
           (rv_X : Ts -> R)
           {frf: FiniteRangeFunction rv_X } : FiniteRangeFunction (pos_fun_part rv_X)
      := { frf_vals := map (fun x => mknonnegreal (Rmax x 0) _) frf_vals}.
    
    Global Program Instance positive_part_frf
           (rv_X : Ts -> R)
           {frf: FiniteRangeFunction rv_X } : FiniteRangeFunction (fun x => nonneg (pos_fun_part rv_X x))
      := { frf_vals := map (fun x => (Rmax x 0)) frf_vals}.

    Global Program Instance negative_part_frf'
           (rv_X : Ts -> R)
           {frf: FiniteRangeFunction rv_X } : FiniteRangeFunction (neg_fun_part rv_X)
      := { frf_vals := map (fun x => mknonnegreal (Rmax (- x) 0) _) frf_vals}.

    Global Program Instance negative_part_frf
           (rv_X : Ts -> R)
           {frf: FiniteRangeFunction rv_X } : FiniteRangeFunction (fun x => nonneg (neg_fun_part rv_X x))
      := { frf_vals := map (fun x => (Rmax (- x) 0)) frf_vals}.

    Program Instance FiniteRangeFunction_enlarged
            {rv_X : Ts -> R}
            (frf:FiniteRangeFunction rv_X)
            (l:list R)
            (lincl : incl frf_vals l)
      : FiniteRangeFunction rv_X :=
      {
      frf_vals := l
      }.


  End Simple.

  
  Section Indicator.
    
    Class IndicatorRandomVariable
          (rv_X : Ts -> R) :=
      irv_binary : forall x, In (rv_X x) [0;1] .
    

    Global Program Instance IndicatorRandomVariableSimpl
           rv_X
           {irv: IndicatorRandomVariable rv_X} : FiniteRangeFunction rv_X
      := {frf_vals := [0;1]}.

    Global Instance EventIndicator_pre_rv {P : pre_event Ts} (dec:forall x, {P x} + {~ P x}) :
      sa_sigma P ->
      RandomVariable dom borel_sa (EventIndicator dec).

    Global Instance EventIndicator_pre_indicator (P : pre_event Ts) (dec:forall x, {P x} + {~ P x})
      : IndicatorRandomVariable (EventIndicator dec).

    Global Program Instance EventIndicator_pre_frf {P : pre_event Ts} (dec:forall x, {P x} + {~ P x})
      : FiniteRangeFunction (EventIndicator dec) :=
      IndicatorRandomVariableSimpl (EventIndicator dec).

    Global Program Instance EventIndicator_frf {P : event dom} (dec:forall x, {P x} + {~ P x})
      : FiniteRangeFunction (EventIndicator dec) :=
      IndicatorRandomVariableSimpl (EventIndicator dec).

    Global Instance EventIndicator_rv {P : event dom} (dec:forall x, {P x} + {~ P x}) :
      RandomVariable dom borel_sa (EventIndicator dec).
    
    Definition point_preimage_indicator
               (rv_X:Ts -> R)
               (c:R) :=
      EventIndicator (fun x => Req_EM_T (rv_X x) c).

    Global Instance point_preimage_indicator_rv
           {rv_X:Ts -> R}
           (rv: RandomVariable dom borel_sa rv_X)
           (c:R) : RandomVariable dom borel_sa (point_preimage_indicator rv_X c).
    
    Global Instance point_preimage_indicator_frf
           {rv_X:Ts -> R}
           (rv: RandomVariable dom borel_sa rv_X)
           (c:R) : FiniteRangeFunction (point_preimage_indicator rv_X c)
      := IndicatorRandomVariableSimpl _.

    Lemma preimage_indicator_notin (rv_X : Ts -> R) l :
      forall a:Ts,
        ~ In (rv_X a) l ->
        list_sum
          (map
             (fun c => c * (point_preimage_indicator rv_X c a))
             (nodup Req_EM_T l)) = 0.


    Lemma frf_preimage_indicator (rv_X : Ts -> R) {frf:FiniteRangeFunction rv_X} :
      forall a:Ts, rv_X a =
                   list_sum
                     (map
                        (fun c => c * (point_preimage_indicator rv_X c a))
                        (nodup Req_EM_T frf_vals)).

    Lemma frf_preimage_indicator' (rv_X : Ts -> R) {frf:FiniteRangeFunction rv_X} :
      pointwise_relation Ts eq rv_X
                         (fun a => list_sum
                                     (map
                                        (fun c => c * (point_preimage_indicator rv_X c a))
                                        (nodup Req_EM_T frf_vals))).

  End Indicator.

  Section Pos.
    
    Class NonnegativeFunction
          (rv_X:Ts->R) : Prop :=
      nnf : forall (x:Ts), (0 <= rv_X x)%R.

    Class Rbar_NonnegativeFunction
          (rv_X:Ts->Rbar) : Prop :=
      Rbar_nnf : forall (x:Ts), (Rbar_le 0 (rv_X x)).

    Global Instance positive_Rbar_positive
           (rv_X:Ts->R)
           {nnf : NonnegativeFunction rv_X} :
      Rbar_NonnegativeFunction rv_X.

    Global Instance NonnegativeFunction_proper : Proper (rv_eq ==> iff) NonnegativeFunction.

    Global Instance NonnegativeFunction_le_proper : Proper (rv_le ==> impl) NonnegativeFunction.

    Global Instance nnfconst c (cpos:0<=c) : NonnegativeFunction (const c).
    
    Global Instance nnfconstinr (c : nat) : NonnegativeFunction (const (INR c)).

    Global Instance IndicatorRandomVariable_positive (rv_X:Ts->R)
           {irvx:IndicatorRandomVariable rv_X} :
      NonnegativeFunction rv_X.

    Global Instance positive_scale_nnf (c:posreal)
           (rv_X : Ts -> R)
           {nnf : NonnegativeFunction rv_X} :
      NonnegativeFunction (rvscale c rv_X).

     Instance scale_nneg_nnf c
           (rv_X : Ts -> R)
           {nnf : NonnegativeFunction rv_X} :
       0 <= c ->
      NonnegativeFunction (rvscale c rv_X).

    Global Instance rvplus_nnf (rv_X1 rv_X2 : Ts -> R)
           {rv1 : NonnegativeFunction rv_X1}
           {rv2 : NonnegativeFunction rv_X2} :
      NonnegativeFunction (rvplus rv_X1 rv_X2).

    Global Instance rvsum_pos (Xn : nat -> Ts -> R)
           {Xn_pos : forall n, NonnegativeFunction (Xn n)} :
      forall (n:nat), NonnegativeFunction (rvsum Xn n).

    Global Instance indicator_prod_pos
           (rv_X : Ts -> R)
           (pofrf : NonnegativeFunction rv_X)
           {P : pre_event Ts}
           (dec:forall x, {P x} + {~ P x}) :
      NonnegativeFunction (rvmult rv_X (EventIndicator dec)).

    Global Instance NonNegMult (f g : Ts -> R)
             {nnf : NonnegativeFunction f}
             {nng : NonnegativeFunction g} :
      NonnegativeFunction (rvmult g f).

    Global Instance EventIndicator_pos {P : pre_event Ts} (dec:forall x, {P x} + {~ P x})
      : NonnegativeFunction (EventIndicator dec).


    Global Instance rvscale_nnf (phival : posreal)
           (rv_X : Ts -> R)
           (pofrf : NonnegativeFunction rv_X) :
      NonnegativeFunction (rvscale phival rv_X).

    Global Instance nnfabs
           (rv_X : Ts -> R) :
      NonnegativeFunction (rvabs rv_X).

    Lemma rvabs_pos_eq (rv_X:Ts->R) {nnf:NonnegativeFunction rv_X} :
      rv_eq (rvabs rv_X) rv_X.


    Global Instance nnfsqr
           (rv_X : Ts -> R) :
      NonnegativeFunction (rvsqr rv_X).


    Global Instance nnflim
           (Xn : nat -> Ts -> R)
           (pofrf : forall n, NonnegativeFunction (Xn n)) :
      NonnegativeFunction (rvlim Xn).

    Global Instance rvpow_nnf
           (rv_X : Ts -> R)
           (k : nat)
           (nnf : NonnegativeFunction rv_X) :
      NonnegativeFunction (rvpow rv_X k).

    Global Instance rvpower_nnf
           (rv_X1 rv_X2 : Ts -> R) :
      NonnegativeFunction (rvpower rv_X1 rv_X2).
    
    Global Instance nnfchoice (c:Ts->bool) (rv_X1 rv_X2 : Ts -> R)
           {nnf1:NonnegativeFunction rv_X1}
           {nnf2:NonnegativeFunction rv_X2} :
      NonnegativeFunction (rvchoice c rv_X1 rv_X2).

    Global Instance nnfmin (rv_X1 rv_X2 : Ts -> R)
           {nnf1:NonnegativeFunction rv_X1}
           {nnf2:NonnegativeFunction rv_X2} :
      NonnegativeFunction (rvmin rv_X1 rv_X2).

    Global Instance nnfmax_l (rv_X1 rv_X2 : Ts -> R)
           {nnf1:NonnegativeFunction rv_X1} : NonnegativeFunction (rvmax rv_X1 rv_X2).

    Global Instance nnfmax_r (rv_X1 rv_X2 : Ts -> R)
           {nnf1:NonnegativeFunction rv_X2} : NonnegativeFunction (rvmax rv_X1 rv_X2).

    Global Instance positive_part_nnf
           (rv_X : Ts -> R) :
      NonnegativeFunction (pos_fun_part rv_X).

    
    Global Instance negative_part_nnf
           (rv_X : Ts -> R) :
      NonnegativeFunction (neg_fun_part rv_X).
    
  End Pos.

  Instance rv_fun_simple_R (x : Ts -> R) (f : R -> R)
           (rvx : RandomVariable dom borel_sa x)
           (frfx : FiniteRangeFunction x) :
    RandomVariable dom borel_sa (fun u => f (x u)).

  Lemma sa_le_ge_rv
        (rv_X : Ts -> R) {rv : RandomVariable dom borel_sa rv_X} x
    : sa_sigma (fun omega => rv_X omega >= x).

  Definition event_ge
             (rv_X : Ts -> R) {rv : RandomVariable dom borel_sa rv_X} x
    : event dom
    := @exist (pre_event Ts) _ _ (sa_le_ge_rv rv_X x).

  Lemma sa_le_le_rv
        (rv_X : Ts -> R) {rv : RandomVariable dom borel_sa rv_X} x
    : sa_sigma (fun omega => rv_X omega <= x).

  Definition event_le
             (rv_X : Ts -> R) {rv : RandomVariable dom borel_sa rv_X} x
    : event dom
    := @exist (pre_event Ts) _ _ (sa_le_le_rv rv_X x).

  Lemma sa_le_lt_rv
        (rv_X : Ts -> R) {rv : RandomVariable dom borel_sa rv_X} x
    : sa_sigma (fun omega => rv_X omega < x).

  Definition event_lt
             (rv_X : Ts -> R) {rv : RandomVariable dom borel_sa rv_X} x
    : event dom
    := @exist (pre_event Ts) _ _ (sa_le_lt_rv rv_X x).
  
  Lemma sa_le_gt_rv
        (rv_X : Ts -> R) {rv : RandomVariable dom borel_sa rv_X} x
    : sa_sigma (fun omega => rv_X omega > x).

  Definition event_gt
             (rv_X : Ts -> R) {rv : RandomVariable dom borel_sa rv_X} x
    : event dom
    := @exist (pre_event Ts) _ _ (sa_le_gt_rv rv_X x).

End RealRandomVariables.

Section MoreRealRandomVariable.
  
  Instance continuity_rv (g : R -> R) :
    continuity g ->
    RandomVariable borel_sa borel_sa g.

  Context {Ts:Type}.

  Lemma event_Rgt_sa (σ:SigmaAlgebra Ts) x1 x2
        {rv1:RandomVariable σ borel_sa x1}
        {rv2:RandomVariable σ borel_sa x2}
    : sa_sigma (fun x => x1 x > x2 x).


  Lemma event_Rge_sa (σ:SigmaAlgebra Ts) x1 x2
        {rv1:RandomVariable σ borel_sa x1}
        {rv2:RandomVariable σ borel_sa x2}
    : sa_sigma (fun x => x1 x >= x2 x).

  Definition event_Rge (σ:SigmaAlgebra Ts) x1 x2
             {rv1:RandomVariable σ borel_sa x1}
             {rv2:RandomVariable σ borel_sa x2} : event σ
    := exist _ _ (event_Rge_sa σ x1 x2).

  Definition event_Rgt (σ:SigmaAlgebra Ts) x1 x2
             {rv1:RandomVariable σ borel_sa x1}
             {rv2:RandomVariable σ borel_sa x2} : event σ
    := exist _ _ (event_Rgt_sa σ x1 x2).

  Lemma event_Rgt_dec (σ:SigmaAlgebra Ts) x1 x2
        {rv1:RandomVariable σ borel_sa x1}
        {rv2:RandomVariable σ borel_sa x2} :
    dec_event (event_Rgt σ x1 x2).

  Definition dec_sa_event_Rgt (σ:SigmaAlgebra Ts) x1 x2
             {rv1:RandomVariable σ borel_sa x1}
             {rv2:RandomVariable σ borel_sa x2}
    : dec_sa_event (σ:=σ)
    := {| dsa_event := event_Rgt σ x1 x2
          ; dsa_dec := event_Rgt_dec σ x1 x2
       |}.

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

  Lemma event_ge_pre_dec (σ:SigmaAlgebra Ts) x1 n
        {rv1:RandomVariable σ borel_sa x1} :
    dec_pre_event (event_ge σ x1 n).

  Definition dec_sa_event_ge (σ:SigmaAlgebra Ts) x1 n
             {rv1:RandomVariable σ borel_sa x1}
    : dec_sa_event (σ:=σ)
    := {| dsa_event := event_ge σ x1 n
          ; dsa_dec := event_ge_dec σ x1 n
       |}.

End MoreRealRandomVariable.

Section RbarRandomVariables.

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

  Lemma RealMeasurable_RbarMeasurable (f : Ts -> R) :
    RealMeasurable dom f <-> RbarMeasurable f.

  Lemma borel_Rbar_borel (f : Ts -> R) :
    RandomVariable dom borel_sa f <-> RandomVariable dom Rbar_borel_sa f.

  Global Instance Rbar_measurable_rv (rv_X:Ts->Rbar)
         {rm:RbarMeasurable rv_X}
    : RandomVariable dom Rbar_borel_sa rv_X.

  Global Instance rv_Rbar_measurable (rv_X : Ts -> Rbar)
         {rrv:RandomVariable dom Rbar_borel_sa rv_X}
    : RbarMeasurable rv_X.

  Global Instance RbarMeasurable_proper :
    Proper (rv_eq ==> iff) RbarMeasurable.

  Global Instance Rbar_rvchoice_rv
         (rv_C : Ts -> R) (rv_X1 rv_X2 : Ts -> Rbar)
         {rvc : RandomVariable dom borel_sa rv_C}
         {rv1 : RandomVariable dom Rbar_borel_sa rv_X1}
         {rv2 : RandomVariable dom Rbar_borel_sa rv_X2} :
    RandomVariable dom Rbar_borel_sa (Rbar_rvchoice (fun x => if Req_EM_T (rv_C x) 0 then false else true) rv_X1 rv_X2).

  Definition Rbar_finite_part (rv_X : Ts -> Rbar) : (Ts -> R) :=
    (fun x => real (rv_X x)).

  Instance Rbar_finite_part_meas (rv_X : Ts -> Rbar)
           (rv : RandomVariable dom Rbar_borel_sa rv_X) :
    RealMeasurable dom (Rbar_finite_part rv_X).

  Lemma sa_pinf_Rbar
        (f : Ts -> Rbar)
        (rv : RandomVariable dom Rbar_borel_sa f) :
    sa_sigma (fun x => (f x) = p_infty).

  Lemma sa_minf_Rbar
        (f : Ts -> Rbar)
        (rv : RandomVariable dom Rbar_borel_sa f) :
    sa_sigma (fun x => (f x) = m_infty).

  Lemma sa_finite_Rbar
        (f : Ts -> Rbar)
        (rv : RandomVariable dom Rbar_borel_sa f) :
    sa_sigma (fun x => is_finite (f x)).

  Global Instance Real_Rbar_rv (rv_X:Ts->R)
         {rv : RandomVariable dom borel_sa rv_X} :
    RandomVariable dom Rbar_borel_sa rv_X.

  Definition Rbar_rvlim (f : nat -> Ts -> Rbar) : (Ts -> Rbar) :=
    (fun omega => ELim_seq (fun n => f n omega)).

  Global Instance Rbar_rvlim_nnf
         (Xn : nat -> Ts -> Rbar)
         (pofrf : forall n, Rbar_NonnegativeFunction (Xn n)) :
    Rbar_NonnegativeFunction (Rbar_rvlim Xn).

  Lemma Rbar_rvlim_pos_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_rv_le (Xn n) (Rbar_rvlim Xn).

  Lemma is_Elim_seq_min (x : Rbar) :
    is_Elim_seq (fun n : nat => Rbar_min x (INR n)) x.

  Lemma ELim_seq_min (x : Rbar) :
    ELim_seq (fun n => Rbar_min x (INR n)) = x.
  
  Lemma rvlim_rvmin (f : Ts -> Rbar) :
    rv_eq (Rbar_rvlim (fun n => (fun x => Rbar_min (f x) (INR n)))) f.

  Definition Rbar_rvplus (rv_X1 rv_X2 : Ts -> Rbar) :=
    (fun omega => Rbar_plus (rv_X1 omega) (rv_X2 omega)).

  Definition Rbar_rvopp (rv_X : Ts -> Rbar) :=
    (fun omega => Rbar_opp (rv_X omega)).

  Instance Rbar_rvopp_measurable (f : Ts -> Rbar) :
    RbarMeasurable f ->
    RbarMeasurable (Rbar_rvopp f).

  Global Instance Rbar_rvopp_rv (f: Ts -> Rbar)
         {rv : RandomVariable dom Rbar_borel_sa f} :
    RandomVariable dom Rbar_borel_sa (Rbar_rvopp f).

  Definition Rbar_rvminus (rv_X1 rv_X2 : Ts -> Rbar) :=
    Rbar_rvplus rv_X1 (Rbar_rvopp rv_X2).

  Definition Rbar_sqr (x:Rbar)
    := match x with
       | Finite x' => Finite (Rsqr x')
       | p_infty => p_infty
       | m_infty => p_infty
       end.
  
  Definition Rbar_rvsqr (rv_X : Ts -> Rbar) :=
    (fun omega => Rbar_sqr (rv_X omega)).

  Definition Rbar_rvmult (x y:Ts->Rbar) omega :=
    Rbar_mult (x omega) (y omega).

  Global Instance pos_Rbar_plus (f g : Ts -> Rbar)
         {fpos : Rbar_NonnegativeFunction f}
         {gpos: Rbar_NonnegativeFunction g} :
    Rbar_NonnegativeFunction (Rbar_rvplus f g).

  
  Instance Rbar_div_pos_measurable (f : Ts -> Rbar) (c : posreal) :
    RbarMeasurable f ->
    RbarMeasurable (fun omega => Rbar_div_pos (f omega) c).

  Instance Rbar_inf_measurable (f : nat -> Ts -> Rbar) :
    (forall n, RbarMeasurable (f n)) ->
    RbarMeasurable (fun omega => Inf_seq (fun n => f n omega)).


  Instance Rbar_sup_measurable (f : nat -> Ts -> Rbar) :
    (forall n, RbarMeasurable (f n)) ->
    RbarMeasurable (fun omega => Sup_seq (fun n => f n omega)).

  Instance Rbar_lim_sup_measurable (f : nat -> Ts -> Rbar) :
    (forall n, RbarMeasurable (f n)) ->
    RbarMeasurable (fun omega => ELimSup_seq (fun n => f n omega)).
  
  Instance Rbar_lim_inf_measurable (f : nat -> Ts -> Rbar) :
    (forall n, RbarMeasurable (f n)) ->
    RbarMeasurable (fun omega => ELimInf_seq (fun n => f n omega)).

  Instance Rbar_real_measurable (f : Ts -> Rbar) :
    RbarMeasurable f ->
    RealMeasurable dom (fun x => real (f x)).

  Lemma Rbar_rvplus_minf (f g : Ts -> Rbar) :
    pre_event_equiv
      (fun omega : Ts => Rbar_plus (f omega) (g omega) = m_infty)
      (pre_event_union
         (pre_event_inter
            (fun omega => f omega = m_infty)
            (fun omega => g omega = m_infty))
         (pre_event_union
            (pre_event_inter
               (fun omega => f omega = m_infty)
               (fun omega => is_finite (g omega)))
            (pre_event_inter
               (fun omega => is_finite (f omega))
               (fun omega => g omega = m_infty) ))).

  Instance Rbar_plus_measurable (f g : Ts -> Rbar) :
    RbarMeasurable f -> RbarMeasurable g ->
    RbarMeasurable (Rbar_rvplus f g).

  Global Instance Rbar_rvplus_rv (rv_X1 rv_X2 : Ts -> Rbar)
         {rvx1 : RandomVariable dom Rbar_borel_sa rv_X1}
         {rvx2 : RandomVariable dom Rbar_borel_sa rv_X2} :
    RandomVariable dom Rbar_borel_sa (Rbar_rvplus rv_X1 rv_X2).

  Instance Rbar_minus_measurable (f g : Ts -> Rbar) :
    RbarMeasurable f -> RbarMeasurable g ->
    RbarMeasurable (Rbar_rvminus f g).

  Global Instance Rbar_rvminus_rv (rv_X1 rv_X2 : Ts -> Rbar)
         {rvx1 : RandomVariable dom Rbar_borel_sa rv_X1}
         {rvx2 : RandomVariable dom Rbar_borel_sa rv_X2} :
    RandomVariable dom Rbar_borel_sa (Rbar_rvminus rv_X1 rv_X2).
  
  Instance Rbar_lim_seq_measurable_pos (f : nat -> Ts -> Rbar) :
    (forall n, RbarMeasurable (f n)) ->
    (forall n, Rbar_NonnegativeFunction (f n)) ->
    RbarMeasurable (fun omega => ELim_seq (fun n => f n omega)).

  Definition Rbar_rvabs (rv_X : Ts -> Rbar) := fun omega => Rbar_abs (rv_X omega).

  Instance Rbar_Rabs_measurable (f : Ts -> Rbar) :
    RbarMeasurable f ->
    RbarMeasurable (Rbar_rvabs f).


  Global Instance power_abs_pos (rv_X : Ts -> Rbar) (p:R) :
    Rbar_NonnegativeFunction
      (fun omega => Rbar_power (Rbar_abs (rv_X omega)) p ).

  Definition Rbar_rvpower (rv_X1 : Ts -> Rbar) (n : R) :=
    fun omega => Rbar_power (rv_X1 omega) n.

  Instance Rbar_power_measurable (f : Ts -> Rbar) (n : R) :
    RbarMeasurable f ->
    RbarMeasurable (Rbar_rvpower f n).
  
  Global Instance Rbar_rvmult_meas (x y : Ts -> Rbar)
         {xrv:RbarMeasurable x}
         {yrv:RbarMeasurable y} :
    RbarMeasurable (Rbar_rvmult x y).
  
  Global Instance Rbar_rvmult_rv (x y : Ts -> Rbar)
         {xrv:RandomVariable dom Rbar_borel_sa x}
         {yrv:RandomVariable dom Rbar_borel_sa y} :
    RandomVariable dom Rbar_borel_sa (Rbar_rvmult x y).

  Global Instance Rbar_rvmult_nnf (x y : Ts -> Rbar)
         {xnnf:Rbar_NonnegativeFunction x}
         {ynnf:Rbar_NonnegativeFunction y} :
    Rbar_NonnegativeFunction (Rbar_rvmult x y).

  Global Instance Rbar_rvsqr_rv (x : Ts -> Rbar)
    {rv:RandomVariable dom Rbar_borel_sa x} :
    RandomVariable dom Rbar_borel_sa (Rbar_rvsqr x).

  Global Instance Rbar_rvsqr_nnf (x : Ts -> Rbar) :
    Rbar_NonnegativeFunction (Rbar_rvsqr x).

   Lemma sup_le_bound (f : nat -> Rbar) (B : Rbar) :
    (forall n, Rbar_le (f n) B) <-> Rbar_le (Sup_seq f) B.

  Global Instance Sup_seq_rv (f : nat -> Ts-> Rbar)
         {rv : forall n, RandomVariable dom Rbar_borel_sa (f n)} :
    RandomVariable dom Rbar_borel_sa (fun x => Sup_seq (fun n => f n x)).

  Global Instance Inf_seq_rv (f : nat -> Ts-> Rbar)
         {rv : forall n, RandomVariable dom Rbar_borel_sa (f n)} :
    RandomVariable dom Rbar_borel_sa (fun x => Inf_seq (fun n => f n x)).

  Global Instance Rbar_rvabs_nnf
         (rv_X : Ts -> Rbar) :
    Rbar_NonnegativeFunction (Rbar_rvabs rv_X).
  
  Global Instance Rbar_rvabs_rv
         (rv_X : Ts -> Rbar)
         {rv : RandomVariable dom Rbar_borel_sa rv_X} :
    RandomVariable dom Rbar_borel_sa (Rbar_rvabs rv_X).
  
  Global Instance Rbar_rvpower_rv (rv_X1 : Ts -> Rbar) (n:R)
           {rvx1 : RandomVariable dom Rbar_borel_sa rv_X1} :
    RandomVariable dom Rbar_borel_sa (Rbar_rvpower rv_X1 n).

    Lemma rvmin_INR_le (f : Ts -> R) :
    forall (n:nat),
      rv_le (rvmin f (const (INR n))) (rvmin f (const (INR (S n)))).

  Instance NonNeg_rvmin (f g : Ts -> R)
           {nnf: NonnegativeFunction f}
           {nng: NonnegativeFunction g} :
    NonnegativeFunction (rvmin f g).

  Instance NonNeg_INR (n : nat) :
    @NonnegativeFunction Ts (const (INR n)).


  Lemma Rbar_mult_pos_div_pos (x : Rbar) (c : posreal) :
    x = Rbar_mult_pos (Rbar_div_pos x c) c.

  Lemma Rbar_le_mult_pos_div_pos (x r : Rbar) (c : posreal) :
    Rbar_le (Rbar_mult_pos x c) r <-> Rbar_le x (Rbar_div_pos r c).

  Instance Rbar_mult_pos_measurable (domm :SigmaAlgebra Ts) (f : Ts -> Rbar) (c:posreal) :
    RbarMeasurable (dom := domm) f ->
    RbarMeasurable (dom := domm) (fun omega => Rbar_mult_pos (f omega) c).

  Lemma pos_fun_part_scale_pos_eq c f :
    0 < c ->
    rv_eq (fun x => nonneg (pos_fun_part (rvscale c f) x)) (rvscale c (fun x : Ts => pos_fun_part f x)).

  Lemma neg_fun_part_scale_pos_eq c f :
    0 < c ->
    rv_eq (fun x => nonneg (neg_fun_part (rvscale c f) x)) (rvscale c (fun x : Ts => neg_fun_part f x)).

  Lemma pos_fun_part_scale_neg_eq c f :
    0 < c ->
    rv_eq (fun x => nonneg (pos_fun_part (rvscale (- c) f) x)) (rvscale c (fun x : Ts => neg_fun_part f x)).

  Lemma neg_fun_part_scale_neg_eq c f :
    0 < c ->
    rv_eq (fun x => nonneg (neg_fun_part (rvscale (- c) f) x)) (rvscale c (fun x : Ts => pos_fun_part f x)).

  Lemma pos_fun_part_nneg_tri (x a:Ts->R) :
    rv_le (pos_fun_part (rvminus x a)) (rvplus (pos_fun_part x) (neg_fun_part a)).
    
  Lemma Rbar_rvlim_plus_min (f1 f2 : Ts -> R) :
    rv_eq
      (Rbar_rvlim
         (fun n : nat =>
            rvplus (rvmin f1 (const (INR n)))
                   (rvmin f2 (const (INR n)))))
      (Rbar_rvlim
         (fun n : nat =>
            rvmin (rvplus f1 f2) (const (INR n)))).

  Instance Rbar_rvlim_measurable (f : nat -> Ts -> Rbar) :
    (forall n, RbarMeasurable (f n)) ->
    RbarMeasurable (Rbar_rvlim f).

  Global Instance Rbar_rvlim_rv (f: nat -> Ts -> Rbar)
         {rv : forall n, RandomVariable dom Rbar_borel_sa (f n)} :
    RandomVariable dom Rbar_borel_sa (Rbar_rvlim f).

  Instance Rbar_lim_inf_rv (f : nat -> Ts -> Rbar) :
    (forall n, RandomVariable dom Rbar_borel_sa (f n)) ->
    RandomVariable dom Rbar_borel_sa (fun omega => ELimInf_seq (fun n => f n omega)).

  Global Instance Rmax_list_rv (l : list (Ts-> R))
         {rvl:forall x, In x l -> RandomVariable dom borel_sa x}
    :
    RandomVariable dom borel_sa (fun omega => Rmax_list (map (fun a => a omega) l)).

  
 Lemma event_Rbar_gt_sa x1 x2
        {rv1:RandomVariable dom Rbar_borel_sa x1}
        {rv2:RandomVariable dom Rbar_borel_sa x2}
    : sa_sigma (fun x => Rbar_gt (x1 x) (x2 x)).

   Definition event_Rbar_gt x1 x2
             {rv1:RandomVariable dom Rbar_borel_sa x1}
             {rv2:RandomVariable dom Rbar_borel_sa x2} : event dom
    := exist _ _ (event_Rbar_gt_sa x1 x2).

  Lemma event_Rbar_gt_dec x1 x2
        {rv1:RandomVariable dom Rbar_borel_sa x1}
        {rv2:RandomVariable dom Rbar_borel_sa x2} :
    dec_event (event_Rbar_gt x1 x2).

  Definition dec_sa_event_Rbar_gt x1 x2
             {rv1:RandomVariable dom borel_sa x1}
             {rv2:RandomVariable dom borel_sa x2}
    : dec_sa_event
    := {| dsa_event := event_Rbar_gt x1 x2
          ; dsa_dec := event_Rbar_gt_dec x1 x2
       |}.

End RbarRandomVariables.

Section rv_almost.

  Lemma almost_map_R_split
        {Ts:Type}
        {dom: SigmaAlgebra Ts}
        (prts: ProbSpace dom)
        {f:Ts->R} {P:R->Prop} :
    almost prts (fun x => P (f x)) ->
    exists f', almostR2 prts eq f f' /\
          (forall x, P (f' x)) /\
          (RandomVariable dom borel_sa f -> RandomVariable dom borel_sa f').

  Lemma almostR2_map_R_split
        {Ts:Type}
        {dom: SigmaAlgebra Ts}
        (prts: ProbSpace dom)
        {f1 f2:Ts->R} {RR:R->R->Prop} :
    almostR2 prts RR f1 f2 ->
    exists f1' f2', almostR2 prts eq f1 f1' /\
               almostR2 prts eq f2 f2' /\
               (forall x, RR (f1' x) (f2' x)) /\
               (RandomVariable dom borel_sa f1 -> RandomVariable dom borel_sa f1')
               /\ (RandomVariable dom borel_sa f2 -> RandomVariable dom borel_sa f2').

  Lemma almostR2_le_forall_split
        {Ts:Type}
        {dom: SigmaAlgebra Ts}
        (prts: ProbSpace dom)
        (f1 f2:nat -> Ts -> R) {RR:R->R->Prop}:
    (forall n:nat, almostR2 prts RR (f1 n) (f2 n)) ->
    exists (f1' f2':nat -> Ts -> R),
      (forall n, almostR2 prts eq (f1 n) (f1' n)) /\
      (forall n, almostR2 prts eq (f2 n) (f2' n)) /\
      (forall n x, RR (f1' n x) (f2' n x)) /\
      (forall n, RandomVariable dom borel_sa (f1 n) ->
            RandomVariable dom borel_sa (f1' n)) /\
      (forall n, RandomVariable dom borel_sa (f2 n) ->
            RandomVariable dom borel_sa (f2' n)).

    Lemma almostR2_le_forall_l_split
        {Ts:Type}
        {dom: SigmaAlgebra Ts}
        (prts: ProbSpace dom)
        (f1:nat -> Ts -> R) (f2:Ts->R) {RR:R->R->Prop}:
    (forall n:nat, almostR2 prts RR (f1 n) f2) ->
    exists (f1':nat -> Ts -> R) (f2':Ts->R),
      (forall n, almostR2 prts eq (f1 n) (f1' n)) /\
      almostR2 prts eq f2 f2' /\
      (forall n x, RR (f1' n x) (f2' x)) /\
      (forall n, RandomVariable dom borel_sa (f1 n) ->
            RandomVariable dom borel_sa (f1' n)) /\
      (RandomVariable dom borel_sa f2 ->
       RandomVariable dom borel_sa f2').

  Lemma almostR2_Rbar_le_forall_l_split
        {Ts:Type}
        {dom: SigmaAlgebra Ts}
        (prts: ProbSpace dom)
        (f1:nat -> Ts -> Rbar) (f2:Ts->Rbar) {RR:Rbar->Rbar->Prop}:
    (forall n:nat, almostR2 prts RR (f1 n) f2) ->
    exists (f1':nat -> Ts -> Rbar) (f2':Ts->Rbar),
      (forall n, almostR2 prts eq (f1 n) (f1' n)) /\
      almostR2 prts eq f2 f2' /\
      (forall n x, RR (f1' n x) (f2' x)) /\
      (forall n, RandomVariable dom Rbar_borel_sa (f1 n) ->
            RandomVariable dom Rbar_borel_sa (f1' n)) /\
      (RandomVariable dom Rbar_borel_sa f2 ->
       RandomVariable dom Rbar_borel_sa f2').

  Lemma almostR2_Rbar_le_fixup_forall_r_split
        {Ts:Type}
        {dom: SigmaAlgebra Ts}
        (prts: ProbSpace dom)
        (f1:Ts -> Rbar) (f2:nat -> Ts->Rbar) {RR:Rbar->Rbar->Prop} {RRrefl:Reflexive RR}:
    (forall n:nat, almostR2 prts RR f1 (f2 n)) ->
    exists (f2':nat->Ts->Rbar),
      (forall n, almostR2 prts eq (f2 n) (f2' n)) /\
      (forall n x, RR (f1 x) (f2' n x)) /\
      (forall n, RandomVariable dom Rbar_borel_sa f1 -> RandomVariable dom Rbar_borel_sa (f2 n) ->
            RandomVariable dom Rbar_borel_sa (f2' n)).

  Lemma almostR2_Rbar_le_forall_r_split
        {Ts:Type}
        {dom: SigmaAlgebra Ts}
        (prts: ProbSpace dom)
        (f1:Ts -> Rbar) (f2:nat -> Ts->Rbar) {RR:Rbar->Rbar->Prop}:
    (forall n:nat, almostR2 prts RR f1 (f2 n)) ->
    exists (f1':Ts->Rbar) (f2':nat -> Ts -> Rbar),
      almostR2 prts eq f1 f1' /\
      (forall n, almostR2 prts eq (f2 n) (f2' n)) /\
      (forall n x, RR (f1' x) (f2' n x)) /\
      (RandomVariable dom Rbar_borel_sa f1 ->
       RandomVariable dom Rbar_borel_sa f1') /\
      (forall n, RandomVariable dom Rbar_borel_sa (f2 n) ->
            RandomVariable dom Rbar_borel_sa (f2' n)).

  Lemma almostR2_Rbar_R_le_forall_l_split
        {Ts:Type}
        {dom: SigmaAlgebra Ts}
        (prts: ProbSpace dom)
        (f1:nat -> Ts -> Rbar) (f2:Ts->R) {RR:Rbar->R->Prop}:
    (forall n:nat, almostR2 prts RR (f1 n) f2) ->
    exists (f1':nat -> Ts -> Rbar) (f2':Ts->R),
      (forall n, almostR2 prts eq (f1 n) (f1' n)) /\
      almostR2 prts eq f2 f2' /\
      (forall n x, RR (f1' n x) (f2' x)) /\
      (forall n, RandomVariable dom Rbar_borel_sa (f1 n) ->
            RandomVariable dom Rbar_borel_sa (f1' n)) /\
      (RandomVariable dom borel_sa f2 ->
       RandomVariable dom borel_sa f2').

  Lemma almostR2_map_R_split_l_bounded
        {Ts:Type}
        {dom: SigmaAlgebra Ts}
        (prts: ProbSpace dom)
        {f1 f2 f3:Ts->R} {RR:R->R->Prop} :
    (forall x, RR (f3 x) (f2 x)) ->
    almostR2 prts RR f1 f2 ->
    exists f1', almostR2 prts eq f1 f1' /\
               (forall x, RR (f1' x) (f2 x)) /\
               (RandomVariable dom borel_sa f1 -> RandomVariable dom borel_sa f3 -> RandomVariable dom borel_sa f1').

  Lemma almostR2_map_R_split_l_refl
        {Ts:Type}
        {dom: SigmaAlgebra Ts}
        (prts: ProbSpace dom)
        {f1 f2:Ts->R} {RR:R->R->Prop} {RR_refl:Reflexive RR}:
    almostR2 prts RR f1 f2 ->
    exists f1', almostR2 prts eq f1 f1' /\
               (forall x, RR (f1' x) (f2 x)) /\
               (RandomVariable dom borel_sa f1 -> RandomVariable dom borel_sa f2 -> RandomVariable dom borel_sa f1').

  Lemma almostR2_map_R_split_l_const_bounded
        {Ts:Type}
        {dom: SigmaAlgebra Ts}
        (prts: ProbSpace dom)
        {f1 f2:Ts->R} {RR:R->R->Prop} (c:R):
    (forall x, RR c (f2 x)) ->
    almostR2 prts RR f1 f2 ->
    exists f1', almostR2 prts eq f1 f1' /\
               (forall x, RR (f1' x) (f2 x)) /\
               (RandomVariable dom borel_sa f1 -> RandomVariable dom borel_sa f1').

  Lemma almostR2_flip
        {Ts Td:Type}
        {dom: SigmaAlgebra Ts}
        (prts: ProbSpace dom)
        {f1 f2:Ts->Td} {RR:Td->Td->Prop} :
    almostR2 prts RR f1 f2 <->
    almostR2 prts (flip RR) f2 f1.


  Lemma almostR2_map_R_split_r_bounded
        {Ts:Type}
        {dom: SigmaAlgebra Ts}
        (prts: ProbSpace dom)
        {f1 f2 f3:Ts->R} {RR:R->R->Prop} :
    (forall x, RR (f1 x) (f3 x)) ->
    almostR2 prts RR f1 f2 ->
    exists f2', almostR2 prts eq f2 f2' /\
               (forall x, RR (f1 x) (f2' x)) /\
               (RandomVariable dom borel_sa f2 -> RandomVariable dom borel_sa f3 -> RandomVariable dom borel_sa f2').

  Lemma almostR2_map_R_split_r_refl
        {Ts:Type}
        {dom: SigmaAlgebra Ts}
        (prts: ProbSpace dom)
        {f1 f2:Ts->R} {RR:R->R->Prop} {RR_refl:Reflexive RR}:
    almostR2 prts RR f1 f2 ->
    exists f2', almostR2 prts eq f2 f2' /\
               (forall x, RR (f1 x) (f2' x)) /\
               (RandomVariable dom borel_sa f1 -> RandomVariable dom borel_sa f2 -> RandomVariable dom borel_sa f2').

  Lemma almostR2_map_R_split_r_const_bounded
        {Ts:Type}
        {dom: SigmaAlgebra Ts}
        (prts: ProbSpace dom)
        {f1 f2:Ts->R} {RR:R->R->Prop} (c:R):
    (forall x, RR (f1 x) c) ->
    almostR2 prts RR f1 f2 ->
    exists f2', almostR2 prts eq f2 f2' /\
               (forall x, RR (f1 x) (f2' x)) /\
               (RandomVariable dom borel_sa f2 -> RandomVariable dom borel_sa f2').

  Lemma almost_map_Rbar_split
        {Ts:Type}
        {dom: SigmaAlgebra Ts}
        (prts: ProbSpace dom)
        {f:Ts->Rbar} {P:Rbar->Prop} :
    almost prts (fun x => P (f x)) ->
    exists f', almostR2 prts eq f f' /\
          (forall x, P (f' x)) /\
          (RandomVariable dom Rbar_borel_sa f -> RandomVariable dom Rbar_borel_sa f').

  Lemma almostR2_map_Rbar_split_l_bounded
        {Ts:Type}
        {dom: SigmaAlgebra Ts}
        (prts: ProbSpace dom)
        {f1 f2 f3:Ts->Rbar} {RR:Rbar->Rbar->Prop} :
    (forall x, RR (f3 x) (f2 x)) ->
    almostR2 prts RR f1 f2 ->
    exists f1', almostR2 prts eq f1 f1' /\
               (forall x, RR (f1' x) (f2 x)) /\
             (RandomVariable dom Rbar_borel_sa f1 -> RandomVariable dom Rbar_borel_sa f3 -> RandomVariable dom Rbar_borel_sa f1') /\
               (forall x, f1' x = f1 x \/ f1' x = f3 x)
.


  Lemma almostR2_map_Rbar_split_l_refl
        {Ts:Type}
        {dom: SigmaAlgebra Ts}
        (prts: ProbSpace dom)
        {f1 f2:Ts->Rbar} {RR:Rbar->Rbar->Prop} {RR_refl:Reflexive RR}:
    almostR2 prts RR f1 f2 ->
    exists f1', almostR2 prts eq f1 f1' /\
               (forall x, RR (f1' x) (f2 x)) /\
             (RandomVariable dom Rbar_borel_sa f1 -> RandomVariable dom Rbar_borel_sa f2 -> RandomVariable dom Rbar_borel_sa f1') /\
             (forall x, f1' x = f1 x \/ f1' x = f2 x)
.

  Lemma almostR2_map_Rbar_split_l_const_bounded
        {Ts:Type}
        {dom: SigmaAlgebra Ts}
        (prts: ProbSpace dom)
        {f1 f2:Ts->Rbar} {RR:Rbar->Rbar->Prop} (c:Rbar):
    (forall x, RR c (f2 x)) ->
    almostR2 prts RR f1 f2 ->
    exists f1', almostR2 prts eq f1 f1' /\
               (forall x, RR (f1' x) (f2 x)) /\
             (RandomVariable dom Rbar_borel_sa f1 -> RandomVariable dom Rbar_borel_sa f1') /\
           (forall x, f1' x = f1 x \/ f1' x = c).

  Lemma almostR2_map_Rbar_split_r_bounded
        {Ts:Type}
        {dom: SigmaAlgebra Ts}
        (prts: ProbSpace dom)
        {f1 f2 f3:Ts->Rbar} {RR:Rbar->Rbar->Prop} :
    (forall x, RR (f1 x) (f3 x)) ->
    almostR2 prts RR f1 f2 ->
    exists f2', almostR2 prts eq f2 f2' /\
               (forall x, RR (f1 x) (f2' x)) /\
             (RandomVariable dom Rbar_borel_sa f2 -> RandomVariable dom Rbar_borel_sa f3 -> RandomVariable dom Rbar_borel_sa f2') /\
             (forall x, f2' x = f2 x \/ f2' x = f3 x).

  Lemma almostR2_map_Rbar_split_r_refl
        {Ts:Type}
        {dom: SigmaAlgebra Ts}
        (prts: ProbSpace dom)
        {f1 f2:Ts->Rbar} {RR:Rbar->Rbar->Prop} {RR_refl:Reflexive RR}:
    almostR2 prts RR f1 f2 ->
    exists f2', almostR2 prts eq f2 f2' /\
               (forall x, RR (f1 x) (f2' x)) /\
             (RandomVariable dom Rbar_borel_sa f1 -> RandomVariable dom Rbar_borel_sa f2 -> RandomVariable dom Rbar_borel_sa f2') /\
             (forall x, f2' x = f2 x \/ f2' x = f1 x).


  Lemma almostR2_map_Rbar_split_r_const_bounded
        {Ts:Type}
        {dom: SigmaAlgebra Ts}
        (prts: ProbSpace dom)
        {f1 f2:Ts->Rbar} {RR:Rbar->Rbar->Prop} (c:Rbar):
    (forall x, RR (f1 x) c) ->
    almostR2 prts RR f1 f2 ->
    exists f2', almostR2 prts eq f2 f2' /\
               (forall x, RR (f1 x) (f2' x)) /\
             (RandomVariable dom Rbar_borel_sa f2 -> RandomVariable dom Rbar_borel_sa f2') /\
             (forall x, f2' x = f2 x \/ f2' x = c).


  Lemma almostR2_seq_split
        {Ts:Type}
        {dom: SigmaAlgebra Ts}
        (prts: ProbSpace dom)
        {f:nat->Ts->R} {RR:R->R->Prop} :
    (forall n : nat, almostR2 prts RR (f n) (f (S n))) ->
    exists f':nat->Ts->R,
      (forall n, almostR2 prts eq (f n) (f' n)) /\
      (forall n x, RR (f' n x) (f' (S n) x)) /\
      (forall n, RandomVariable dom borel_sa (f n) -> RandomVariable dom borel_sa (f' n)).

    Lemma almostR2_Rbar_seq_split
        {Ts:Type}
        {dom: SigmaAlgebra Ts}
        (prts: ProbSpace dom)
        {f:nat->Ts->Rbar} {RR:Rbar->Rbar->Prop} :
    (forall n : nat, almostR2 prts RR (f n) (f (S n))) ->
    exists f':nat->Ts->Rbar,
      (forall n, almostR2 prts eq (f n) (f' n)) /\
      (forall n x, RR (f' n x) (f' (S n) x)) /\
      (forall n, RandomVariable dom Rbar_borel_sa (f n) -> RandomVariable dom Rbar_borel_sa (f' n)).
  
  Open Scope prob.
  Global Instance almostR2_eq_plus_proper
         {Ts:Type}
         {dom: SigmaAlgebra Ts}
         (prts: ProbSpace dom) : Proper (almostR2 prts eq ==> almostR2 prts eq ==> almostR2 prts eq) rvplus.

  Global Instance almostR2_eq_scale_proper
         {Ts:Type}
         {dom: SigmaAlgebra Ts}
         (prts: ProbSpace dom) : Proper (eq ==> almostR2 prts eq ==> almostR2 prts eq) rvscale.

  Global Instance almostR2_eq_opp_proper
         {Ts:Type}
         {dom: SigmaAlgebra Ts}
         (prts: ProbSpace dom) : Proper (almostR2 prts eq ==> almostR2 prts eq) rvopp.

  Global Instance almostR2_eq_minus_proper
         {Ts:Type}
         {dom: SigmaAlgebra Ts}
         (prts: ProbSpace dom) : Proper (almostR2 prts eq ==> almostR2 prts eq ==> almostR2 prts eq) rvminus.

  Lemma almostR2_eq_plus_inv {Ts:Type}
         {dom: SigmaAlgebra Ts}
         (prts: ProbSpace dom)
         {x y z} :
    almostR2 prts eq z (rvplus x y) ->
    exists x' y',
      almostR2 prts eq x x' /\
      almostR2 prts eq y y' /\
      rv_eq z (rvplus x' y').

  Lemma almostR2_eq_opp_inv{Ts:Type}
         {dom: SigmaAlgebra Ts}
         (prts: ProbSpace dom)
         {x z} :
    almostR2 prts eq z (rvopp x) ->
    exists x',
      almostR2 prts eq x x' /\
      rv_eq z (rvopp x').

  Global Instance almostR2_le_plus_proper
         {Ts:Type}
         {dom: SigmaAlgebra Ts}
         (prts: ProbSpace dom) : Proper (almostR2 prts Rle ==> almostR2 prts Rle ==> almostR2 prts Rle) rvplus.

  Global Instance almostR2_Rbar_le_plus_proper
         {Ts:Type}
         {dom: SigmaAlgebra Ts}
         (prts: ProbSpace dom) : Proper (almostR2 prts Rbar_le ==> almostR2 prts Rbar_le ==> almostR2 prts Rbar_le) Rbar_rvplus.

  Global Instance almostR2_le_lt_plus_proper
         {Ts:Type}
         {dom: SigmaAlgebra Ts}
         (prts: ProbSpace dom) : Proper (almostR2 prts Rle ==> almostR2 prts Rlt ==> almostR2 prts Rlt) rvplus.

  Global Instance almostR2_lt_le_plus_proper
         {Ts:Type}
         {dom: SigmaAlgebra Ts}
         (prts: ProbSpace dom) : Proper (almostR2 prts Rlt ==> almostR2 prts Rle ==> almostR2 prts Rlt) rvplus.

  Global Instance almostR2_eq_mult_proper
         {Ts:Type}
         {dom: SigmaAlgebra Ts}
         (prts: ProbSpace dom) : Proper (almostR2 prts eq ==> almostR2 prts eq ==> almostR2 prts eq) rvmult.

  Global Instance almostR2_eq_Rbar_mult_proper
         {Ts:Type}
         {dom: SigmaAlgebra Ts}
         (prts: ProbSpace dom) : Proper (almostR2 prts eq ==> almostR2 prts eq ==> almostR2 prts eq) Rbar_rvmult.

  Global Instance almostR2_sub
         {Ts Td:Type}
         {dom: SigmaAlgebra Ts}
         (prts: ProbSpace dom)
         (R:Td->Td->Prop)
         (f:(Ts->Td)->Ts->Td)
         (fpres: forall x y a, R (x a) (y a) -> R (f x a) (f y a))
    : Proper (almostR2 prts R ==> almostR2 prts R) f.

  Lemma almostR2_Rle_ge
         {Ts:Type}
         {dom: SigmaAlgebra Ts}
         (prts: ProbSpace dom) x y:
    almostR2 prts Rle x y -> almostR2 prts Rge y x.

  Lemma almostR2_Rge_le
         {Ts:Type}
         {dom: SigmaAlgebra Ts}
         (prts: ProbSpace dom) x y:
    almostR2 prts Rge x y -> almostR2 prts Rle y x.

  Lemma almostR2_eq_pow_abs_proper
        {Ts:Type}
        {dom: SigmaAlgebra Ts}
        (prts: ProbSpace dom)
        (x1 x2: Ts -> R)
        n
        (eqqx : almostR2 prts eq (rvabs x1) (rvabs x2)) :
    almostR2 prts eq (rvpow (rvabs x1) n) (rvpow (rvabs x2) n).

  Global Instance almostR2_eq_power_proper
         {Ts:Type}
         {dom: SigmaAlgebra Ts}
         (prts: ProbSpace dom) :
    Proper (almostR2 prts eq ==> eq ==> almostR2 prts eq) rvpower.

  Global Instance almostR2_eq_abs_proper
         {Ts:Type}
         {dom: SigmaAlgebra Ts}
         (prts: ProbSpace dom) :
    Proper (almostR2 prts eq ==> almostR2 prts eq) rvabs.

  Global Instance almostR2_eq_subr {Ts Td:Type}
         {dom: SigmaAlgebra Ts}
         (prts: ProbSpace dom) :
    subrelation (@rv_eq Ts Td) (almostR2 prts eq).

  Global Instance almostR2_le_subr {Ts:Type}
         {dom: SigmaAlgebra Ts}
         (prts: ProbSpace dom) :
    subrelation (@rv_le Ts) (almostR2 prts Rle).

  Global Instance rv_le_sub_eq {Ts:Type}: subrelation (@rv_eq Ts R) rv_le.

  Lemma almostR2_le_split {Ts:Type}
         {dom: SigmaAlgebra Ts}
         (prts: ProbSpace dom)
         x y :
    almostR2 prts Rle x y ->
    exists x', almostR2 prts eq x x' /\
          rv_le x' y /\
          (RandomVariable dom borel_sa x ->
           RandomVariable dom borel_sa y ->
           RandomVariable dom borel_sa x').

  Lemma almostR2_le_split_r {Ts:Type}
         {dom: SigmaAlgebra Ts}
         (prts: ProbSpace dom)
         x y :
    almostR2 prts Rle x y ->
    exists y', almostR2 prts eq y y' /\
          rv_le x y' /\
          (RandomVariable dom borel_sa x ->
           RandomVariable dom borel_sa y ->
           RandomVariable dom borel_sa y').

  
  Instance almostR2_eq_Rbar_plus_proper {Ts:Type}
         {dom: SigmaAlgebra Ts}
         (prts: ProbSpace dom)
          : Proper (almostR2 prts eq ==> almostR2 prts eq ==> almostR2 prts eq) Rbar_rvplus.

  Local Existing Instance Rbar_le_pre.
  
  Lemma almostR2_Rbar_le_split {Ts:Type}
         {dom: SigmaAlgebra Ts}
         (prts: ProbSpace dom)
         x y :
    almostR2 prts Rbar_le x y ->
    exists x', almostR2 prts eq x x' /\
          Rbar_rv_le x' y /\
          (RandomVariable dom Rbar_borel_sa x ->
           RandomVariable dom Rbar_borel_sa x').


  Lemma almostR2_Rbar_le_split_r {Ts:Type}
         {dom: SigmaAlgebra Ts}
         (prts: ProbSpace dom)
         x y :
    almostR2 prts Rbar_le x y ->
    exists y', almostR2 prts eq y y' /\
          Rbar_rv_le x y' /\
          (RandomVariable dom Rbar_borel_sa y ->
           RandomVariable dom Rbar_borel_sa y').

End rv_almost.

Section EventRestricted.

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

  Global Instance Restricted_NonnegativeFunction
         (e:event dom) (f : Ts -> R)
         (nnf: NonnegativeFunction f) :
    NonnegativeFunction (event_restricted_function e f).

  Global Instance Restricted_Rbar_NonnegativeFunction P (f : Ts -> Rbar)
         (nnf : Rbar_NonnegativeFunction f) :
    Rbar_NonnegativeFunction (event_restricted_function P f).

  Global Instance event_restricted_rv_le P : Proper (rv_le ==> rv_le) (event_restricted_function P).

  Global Instance event_restricted_Rbar_rv_le P : Proper (Rbar_rv_le ==> Rbar_rv_le) (event_restricted_function P).



  Global Instance lift_event_restricted_domain_fun_nnf {P} (f:event_restricted_domain P -> R) :
    NonnegativeFunction f ->
    NonnegativeFunction (lift_event_restricted_domain_fun 0 f).

  Global Instance lift_event_restricted_domain_fun_Rbar_nnf {P} (f:event_restricted_domain P -> Rbar) :
    Rbar_NonnegativeFunction f ->
    Rbar_NonnegativeFunction (lift_event_restricted_domain_fun (Finite 0) f).

  Lemma restrict_lift {P} (f:event_restricted_domain P -> R) :
    rv_eq (event_restricted_function P (lift_event_restricted_domain_fun 0 f)) f.


  Lemma restrict_lift_Rbar {P} (f:event_restricted_domain P -> Rbar) :
    rv_eq (event_restricted_function P (lift_event_restricted_domain_fun (Finite 0) f)) f.

End EventRestricted.

Section real_pullback.
  
  Lemma pullback_sa_plus_sub {Ts} (x1 x2 : Ts -> R) :
    sa_sub (pullback_sa borel_sa (rvplus x1 x2)) (union_sa (pullback_sa _ x1) (pullback_sa _ x2)).

  Lemma pullback_sa_minus_sub {Ts} (x1 x2 : Ts -> R) :
    sa_sub (pullback_sa borel_sa (rvminus x1 x2)) (union_sa (pullback_sa _ x1) (pullback_sa _ x2)).

  Lemma pullback_sa_mult_sub {Ts} (x1 x2 : Ts -> R) :
    sa_sub (pullback_sa borel_sa (rvmult x1 x2)) (union_sa (pullback_sa _ x1) (pullback_sa _ x2)).


  Lemma pullback_sa_plus_equiv {Ts} (x1 x2 : Ts -> R) :
    sa_equiv (union_sa (pullback_sa _ x1) (pullback_sa _ x2)) (union_sa (pullback_sa _ x1) (pullback_sa borel_sa (rvplus x1 x2))).

  Lemma history_pair_plus_equiv {Ts} (x : nat -> Ts -> R) :
    rv_eq (x 0%nat) (const 0) ->
    forall n,
      sa_equiv (filtration_history_sa (fun n => (x (S n))) n)
               (filtration_history_sa (fun n => rvplus (x n) (x (S n))) n).

  Lemma pullback_sa_rvscale_equiv {Ts} (c:R) (x : Ts -> R) : c <> 0 ->
    sa_equiv (pullback_sa borel_sa x) (pullback_sa borel_sa (rvscale c x)).

End real_pullback.
Section rv_expressible.

  Lemma event_measurable_iff_expressible {Ts : Type} {Td : Type}
        {dom : SigmaAlgebra Ts} {cod : SigmaAlgebra Td}
        (X : Ts -> Td) (A : event (pullback_sa cod X))
        {rv_X : RandomVariable dom cod X} :
    exists g : Td -> R,
      RandomVariable cod borel_sa g /\
      forall x,
         EventIndicator (classic_dec A) x = g (X x).

 Lemma event_measurable_iff_expressible' {Ts : Type} {Td : Type}
        {dom : SigmaAlgebra Ts} {cod : SigmaAlgebra Td}
        (X : Ts -> Td) (A : event (pullback_sa cod X))
        {rv_X : RandomVariable dom cod X} :
    { g : Td -> R |
      RandomVariable cod borel_sa g /\
      forall x,
        EventIndicator (classic_dec A) x = g (X x)}.

 Lemma pt_event_measurable_is_expressible {Ts : Type} {Td : Type}
        {dom : SigmaAlgebra Ts} {cod : SigmaAlgebra Td}
        (X : Ts -> Td) (Y : Ts -> R) (c : R)
        {rv_X : RandomVariable dom cod X}
        {rv_Y : RandomVariable (pullback_sa cod X) borel_sa Y} :
   exists (g : Td -> R),
      RandomVariable cod borel_sa g /\
      forall x,
        point_preimage_indicator Y c x = g (X x).
   
 Lemma pt_event_measurable_is_expressible' {Ts : Type} {Td : Type}
        {dom : SigmaAlgebra Ts} {cod : SigmaAlgebra Td}
        (X : Ts -> Td) (Y : Ts -> R) (c : R)
        {rv_X : RandomVariable dom cod X}
        {rv_Y : RandomVariable (pullback_sa cod X) borel_sa Y} :
   {g : Td -> R |
      RandomVariable cod borel_sa g /\
      forall x,
        point_preimage_indicator Y c x = g (X x)}.

  Lemma list_sum_rv {Ts} {dom} (f : R -> (Ts -> R)) (l : list R)
        {rv: forall (c:R), In c l -> RandomVariable dom borel_sa (f c)} :
    RandomVariable dom borel_sa (fun z => (list_sum (map (fun c => f c z) l))).

  Lemma frf_measurable_is_expressible {Ts : Type} {Td : Type}
        {dom : SigmaAlgebra Ts} {cod : SigmaAlgebra Td}
        (X : Ts -> Td) (Y : Ts -> R)
        {rv_X : RandomVariable dom cod X}
        {fr_Y : FiniteRangeFunction Y}
        {rv_y : RandomVariable (pullback_sa cod X) borel_sa Y} :
    exists g : Td -> R,
      RandomVariable cod borel_sa g /\
      forall x, Y x = g (X x).

    Lemma frf_measurable_is_expressible' {Ts : Type} {Td : Type}
        {dom : SigmaAlgebra Ts} {cod : SigmaAlgebra Td}
        (X : Ts -> Td) (Y : Ts -> R)
        {rv_X : RandomVariable dom cod X}
        {fr_Y : FiniteRangeFunction Y}
        {rv_y : RandomVariable (pullback_sa cod X) borel_sa Y} :
      { g : Td -> R |
        RandomVariable cod borel_sa g /\
        forall x, Y x = g (X x)}.

End rv_expressible.

Section adapted.
  Context {Ts:Type}.

  Global Instance is_adapted_const c (sas:nat->SigmaAlgebra Ts) :
    IsAdapted borel_sa (fun _ => const c) sas.

  Global Instance is_adapted_opp Y (sas:nat->SigmaAlgebra Ts) :
    IsAdapted borel_sa Y sas ->
    IsAdapted borel_sa (fun n => rvopp (Y n)) sas.

  Global Instance is_adapted_plus X Y (sas:nat->SigmaAlgebra Ts) :
    IsAdapted borel_sa X sas ->
    IsAdapted borel_sa Y sas ->
    IsAdapted borel_sa (fun n => rvplus (X n) (Y n)) sas.

  Global Instance is_adapted_minus X Y (sas:nat->SigmaAlgebra Ts) :
    IsAdapted borel_sa X sas ->
    IsAdapted borel_sa Y sas ->
    IsAdapted borel_sa (fun n => rvminus (X n) (Y n)) sas.

  Global Instance is_adapted_mult X Y (sas:nat->SigmaAlgebra Ts) :
    IsAdapted borel_sa X sas ->
    IsAdapted borel_sa Y sas ->
    IsAdapted borel_sa (fun n => rvmult (X n) (Y n)) sas.

  Global Instance is_adapted_abs Y (sas:nat->SigmaAlgebra Ts) :
    IsAdapted borel_sa Y sas ->
    IsAdapted borel_sa (fun n => rvabs (Y n)) sas.

End adapted.