Module FormalML.ProbTheory.ConditionalExpectation

Require Import Morphisms.
Require Import Equivalence.
Require Import Program.Basics.
Require Import Lra Lia.
Require Import Classical ClassicalChoice RelationClasses.

Require Import FunctionalExtensionality.
Require Import IndefiniteDescription ClassicalDescription.

Require Import hilbert.

Require Export RandomVariableLpR RandomVariableL2 OrthoProject.
Require Import quotient_space.
Require Import RbarExpectation.

Require Import Event.
Require Import Almost DVector.
Require Import utils.Utils.
Require Import List.
Require Import NumberIso.
Require Import PushNeg.

Set Bullet Behavior "Strict Subproofs".

Section is_cond_exp.

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

  
  Definition is_conditional_expectation
             (dom2 : SigmaAlgebra Ts)
             (f : Ts -> R)
             (ce : Ts -> Rbar)
             {rvf : RandomVariable dom borel_sa f}
             {rvce : RandomVariable dom2 Rbar_borel_sa ce}
    := forall P (dec:dec_pre_event P),
      sa_sigma (SigmaAlgebra := dom2) P ->
      Expectation (rvmult f (EventIndicator dec)) =
      Rbar_Expectation (Rbar_rvmult ce (EventIndicator dec)).
  
  Context {dom2 : SigmaAlgebra Ts}
          (sub : sa_sub dom2 dom).

  Theorem is_conditional_expectation_id
          (f : Ts -> R)
          {rvf : RandomVariable dom borel_sa f}
          {rvf2 : RandomVariable dom2 borel_sa f} :
    is_conditional_expectation dom2 f (fun x => Finite (f x)).

  Theorem is_conditional_expectation_Expectation
        (f : Ts -> R)
        (ce : Ts -> Rbar)
        {rvf : RandomVariable dom borel_sa f}
        {rvce : RandomVariable dom2 Rbar_borel_sa ce} :
    is_conditional_expectation dom2 f ce ->
    Expectation f = Rbar_Expectation ce.

  Lemma is_conditional_expectation_FiniteExpectation
        (f : Ts -> R)
        (ce : Ts -> Rbar)
        {rvf : RandomVariable dom borel_sa f}
        {rvce : RandomVariable dom2 Rbar_borel_sa ce} :
    is_conditional_expectation dom2 f ce ->
    IsFiniteExpectation prts f <-> Rbar_IsFiniteExpectation prts ce.

  Theorem is_conditional_expectation_proper
        (f1 f2 : Ts -> R)
        (ce1 ce2 : Ts -> Rbar)
        {rvf1 : RandomVariable dom borel_sa f1}
        {rvf2 : RandomVariable dom borel_sa f2}
        {rvce1 : RandomVariable dom2 Rbar_borel_sa ce1}
        {rvce2 : RandomVariable dom2 Rbar_borel_sa ce2}
    : almostR2 prts eq f1 f2 ->
      almostR2 prts eq ce1 ce2 ->
      is_conditional_expectation dom2 f1 ce1 ->
      is_conditional_expectation dom2 f2 ce2.

  
  Lemma is_conditional_expectation_nneg_le
        (f : Ts->R)
        (ce1 ce2 : Ts -> Rbar)
        {rvf : RandomVariable dom borel_sa f}
        {rvce1 : RandomVariable dom2 Rbar_borel_sa ce1}
        {rvce2 : RandomVariable dom2 Rbar_borel_sa ce2}
        {nnf : NonnegativeFunction f}
        {nnf1 : Rbar_NonnegativeFunction ce1}
        {nnf2 : Rbar_NonnegativeFunction ce2}
    : is_conditional_expectation dom2 f ce1 ->
      is_conditional_expectation dom2 f ce2 ->
      almostR2 (prob_space_sa_sub prts sub) Rbar_le ce1 ce2.

  Local Existing Instance Rbar_le_part.
  
  Theorem is_conditional_expectation_nneg_unique
        (f : Ts->R)
        (ce1 ce2 : Ts -> Rbar)
        {rvf : RandomVariable dom borel_sa f}
        {rvce1 : RandomVariable dom2 Rbar_borel_sa ce1}
        {rvce2 : RandomVariable dom2 Rbar_borel_sa ce2}
        {nnf : NonnegativeFunction f}
        {nnf1 : Rbar_NonnegativeFunction ce1}
        {nnf2 : Rbar_NonnegativeFunction ce2}
    : is_conditional_expectation dom2 f ce1 ->
      is_conditional_expectation dom2 f ce2 ->
      almostR2 (prob_space_sa_sub prts sub) eq ce1 ce2.

  Lemma is_conditional_expectation_almostfinite_le
        (f : Ts->R)
        (ce1 ce2 : Ts -> Rbar)
        {rvf : RandomVariable dom borel_sa f}
        {rvce1 : RandomVariable dom2 Rbar_borel_sa ce1}
        {rvce2 : RandomVariable dom2 Rbar_borel_sa ce2}
        (isf2:almost (prob_space_sa_sub prts sub) (fun a => is_finite (ce2 a))) :
    is_conditional_expectation dom2 f ce1 ->
    is_conditional_expectation dom2 f ce2 ->
    almostR2 (prob_space_sa_sub prts sub) Rbar_le ce1 ce2.

  Theorem is_conditional_expectation_almostfinite_unique
        (f : Ts->R)
        (ce1 ce2 : Ts -> Rbar)
        {rvf : RandomVariable dom borel_sa f}
        {rvce1 : RandomVariable dom2 Rbar_borel_sa ce1}
        {rvce2 : RandomVariable dom2 Rbar_borel_sa ce2}
        (isf1:almost (prob_space_sa_sub prts sub) (fun a => is_finite (ce1 a)))
        (isf2:almost (prob_space_sa_sub prts sub) (fun a => is_finite (ce2 a))) :
    is_conditional_expectation dom2 f ce1 ->
    is_conditional_expectation dom2 f ce2 ->
    almostR2 (prob_space_sa_sub prts sub) eq ce1 ce2.

  Theorem is_conditional_expectation_unique
        (f : Ts->R)
        (ce1 ce2 : Ts -> Rbar)
        {rvf : RandomVariable dom borel_sa f}
        {rvce1 : RandomVariable dom2 Rbar_borel_sa ce1}
        {rvce2 : RandomVariable dom2 Rbar_borel_sa ce2}
        {isfe:IsFiniteExpectation prts f} :
    is_conditional_expectation dom2 f ce1 ->
    is_conditional_expectation dom2 f ce2 ->
    almostR2 (prob_space_sa_sub prts sub) eq ce1 ce2.

  Existing Instance Rbar_rvmult_rv.

  Lemma Rbar_rvmult_assoc (a:Ts->Rbar) (b:Ts->Rbar) (c:Ts->Rbar) :
    rv_eq (Rbar_rvmult a (Rbar_rvmult b c)) (Rbar_rvmult (Rbar_rvmult a b) c).

  Lemma rvmult_rvscale c (a b:Ts->R) :
    rv_eq (rvmult (rvscale c a) b) (rvscale c (rvmult a b)).

  Theorem is_conditional_expectation_const (c:R)
    :
      is_conditional_expectation dom2 (const c) (const c).
  
  Lemma is_conditional_expectation_scale_nzero (c:R)
        (f : Ts -> R)
        (ce : Ts -> Rbar)
        {rv : RandomVariable dom borel_sa f}
        {rvce : RandomVariable dom2 Rbar_borel_sa ce}
    :
      c <> 0 ->
      is_conditional_expectation dom2 f ce ->
      is_conditional_expectation dom2 (rvscale c f) (Rbar_rvmult (const c) ce)
                                 (rvce:=Rbar_rvmult_rv _ _)
  .

  Corollary is_conditional_expectation_propere
            {f1 f2 : Ts -> R}
            (eq1:almostR2 prts eq f1 f2)
            {ce1 ce2 : Ts -> Rbar}
            (eq2:almostR2 prts eq ce1 ce2)
            (rvf1 : RandomVariable dom borel_sa f1)
            (rvf2 : RandomVariable dom borel_sa f2)
            (rvce1 : RandomVariable dom2 Rbar_borel_sa ce1)
            (rvce2 : RandomVariable dom2 Rbar_borel_sa ce2)
            :
      is_conditional_expectation dom2 f1 ce1 ->
      is_conditional_expectation dom2 f2 ce2.
    
  Theorem is_conditional_expectation_scale (c:R)
        (f : Ts -> R)
        (ce : Ts -> Rbar)
        {rv : RandomVariable dom borel_sa f}
        {rvce : RandomVariable dom2 Rbar_borel_sa ce}
    :
      is_conditional_expectation dom2 f ce ->
      is_conditional_expectation dom2 (rvscale c f) (Rbar_rvmult (const c) ce)
                                 (rvce:=Rbar_rvmult_rv _ _).
  
  Corollary is_conditional_expectation_scale_inv (c:R)
        (f : Ts -> R)
        (ce : Ts -> Rbar)
        {rv : RandomVariable dom borel_sa f}
        {rvce : RandomVariable dom2 Rbar_borel_sa ce}
    :
      c <> 0 ->
      is_conditional_expectation dom2 (rvscale c f) (Rbar_rvmult (const c) ce)
                                 (rvce:=Rbar_rvmult_rv _ _) ->
      is_conditional_expectation dom2 f ce.

  Corollary is_conditional_expectation_opp
        (f : Ts -> R)
        (ce : Ts -> Rbar)
        {rv : RandomVariable dom borel_sa f}
        {rvce : RandomVariable dom2 Rbar_borel_sa ce}
    :
      is_conditional_expectation dom2 f ce ->
      is_conditional_expectation dom2 (rvopp f) (Rbar_rvopp ce)
                                 (rvce:=Rbar_rvopp_rv _).

  Theorem is_conditional_expectation_plus
        (f1 f2 : Ts -> R)
        (ce1 ce2 : Ts -> Rbar)
        {rvf1 : RandomVariable dom borel_sa f1}
        {rvf2 : RandomVariable dom borel_sa f2}
        {isfe1:IsFiniteExpectation prts f1}
        {isfe2:IsFiniteExpectation prts f2}
        {rvce1 : RandomVariable dom2 Rbar_borel_sa ce1}
        {rvce2 : RandomVariable dom2 Rbar_borel_sa ce2}
    :
      is_conditional_expectation dom2 f1 ce1 ->
      is_conditional_expectation dom2 f2 ce2 ->
      is_conditional_expectation dom2 (rvplus f1 f2) (Rbar_rvplus ce1 ce2)
                                      (rvce:= Rbar_rvplus_rv _ _).

  Corollary is_conditional_expectation_minus
            (f1 f2 : Ts -> R)
            (ce1 ce2 : Ts -> Rbar)
            {rvf1 : RandomVariable dom borel_sa f1}
            {rvf2 : RandomVariable dom borel_sa f2}
            {isfe1:IsFiniteExpectation prts f1}
            {isfe2:IsFiniteExpectation prts f2}
            {rvce1 : RandomVariable dom2 Rbar_borel_sa ce1}
            {rvce2 : RandomVariable dom2 Rbar_borel_sa ce2}
    :
      is_conditional_expectation dom2 f1 ce1 ->
      is_conditional_expectation dom2 f2 ce2 ->
      is_conditional_expectation dom2 (rvminus f1 f2) (Rbar_rvminus ce1 ce2)
                                 (rvce:= Rbar_rvplus_rv _ _).
  
  Lemma Rbar_rvlim_almost_proper (f1 f2:nat->Ts->Rbar) :
    (forall n, almostR2 prts eq (f1 n) (f2 n)) ->
    almostR2 prts eq (Rbar_rvlim f1) (Rbar_rvlim f2).

  Global Instance rvmin_almost_proper : Proper (almostR2 prts eq ==> almostR2 prts eq ==> almostR2 prts eq) rvmin.

  Global Instance Rbar_rvplus_almost_proper {DOM:SigmaAlgebra Ts} (PRTS: ProbSpace DOM) : Proper (almostR2 PRTS eq ==> almostR2 PRTS eq ==> almostR2 PRTS eq) Rbar_rvplus.

  Global Instance Rbar_rvopp_almost_proper {DOM:SigmaAlgebra Ts} (PRTS: ProbSpace DOM) : Proper (almostR2 PRTS eq ==> almostR2 PRTS eq) Rbar_rvopp.

  Lemma sa_le_Rbar_ge_rv {domm}
        (rv_X : Ts -> Rbar) {rv : RandomVariable domm Rbar_borel_sa rv_X} x
    : sa_sigma (fun omega => Rbar_ge (rv_X omega) x).

  Definition event_Rbar_ge {domm}
             (rv_X : Ts -> Rbar) {rv : RandomVariable domm Rbar_borel_sa rv_X} x
    : event domm
    := @exist (pre_event Ts) _ _ (sa_le_Rbar_ge_rv rv_X x).

  Theorem is_conditional_expectation_isfe
        f ce
        {rvf:RandomVariable dom borel_sa f}
        {rvce:RandomVariable dom2 Rbar_borel_sa ce} :
    is_conditional_expectation dom2 f ce ->
    IsFiniteExpectation prts f ->
    Rbar_IsFiniteExpectation prts ce.

  Theorem is_conditional_expectation_nneg
        (f : Ts -> R)
        (ce : Ts -> Rbar)
        {rvf : RandomVariable dom borel_sa f}
        {rvce : RandomVariable dom2 Rbar_borel_sa ce}
        {nnf:NonnegativeFunction f}
    :
      is_conditional_expectation dom2 f ce ->
      almostR2 (prob_space_sa_sub prts sub) Rbar_le (const 0) ce.

  Lemma is_conditional_expectation_anneg
        (f : Ts -> R)
        (ce : Ts -> Rbar)
        {rvf : RandomVariable dom borel_sa f}
        {rvce : RandomVariable dom2 Rbar_borel_sa ce}
    :
      almostR2 prts Rle (const 0) f ->
      is_conditional_expectation dom2 f ce ->
      almostR2 (prob_space_sa_sub prts sub) Rbar_le (const 0) ce.

    Theorem is_conditional_expectation_ale
        (f1 : Ts -> R)
        (f2 : Ts -> R)
        (ce1 : Ts -> Rbar)
        (ce2 : Ts -> Rbar)
        {rvf1 : RandomVariable dom borel_sa f1}
        {rvce1 : RandomVariable dom2 Rbar_borel_sa ce1}
        {isfe1:IsFiniteExpectation prts f1}
        {rvf2 : RandomVariable dom borel_sa f2}
        {rvce2 : RandomVariable dom2 Rbar_borel_sa ce2}
        {isfe2:IsFiniteExpectation prts f2}
    :
      almostR2 prts Rle f1 f2 ->
      is_conditional_expectation dom2 f1 ce1 ->
      is_conditional_expectation dom2 f2 ce2 ->
      almostR2 (prob_space_sa_sub prts sub) Rbar_le ce1 ce2.

  Fixpoint list_Rbar_sum (l : list Rbar) : Rbar :=
    match l with
    | nil => 0
    | x :: xs => Rbar_plus x (list_Rbar_sum xs)
    end.

  Lemma list_Rbar_sum_const_mulR {A : Type} f (l : list A) :
    forall (r:R), list_Rbar_sum (map (fun x => Rbar_mult r (f x)) l) =
              Rbar_mult r (list_Rbar_sum (map (fun x => f x) l)).

  Lemma is_conditional_expectation_finexp
             (f : Ts -> R)
             (ce : Ts -> Rbar)
             {rvf : RandomVariable dom borel_sa f}
             {rvce : RandomVariable dom2 Rbar_borel_sa ce}
    : is_conditional_expectation dom2 f ce ->
      forall P (dec:dec_pre_event P),
        sa_sigma (SigmaAlgebra := dom2) P ->
        forall {isfef:IsFiniteExpectation prts (rvmult f (EventIndicator dec))}
          {isfece:Rbar_IsFiniteExpectation prts (Rbar_rvmult ce (EventIndicator dec))},
        FiniteExpectation prts (rvmult f (EventIndicator dec)) =
        Rbar_FiniteExpectation prts (Rbar_rvmult ce (EventIndicator dec)).

  Lemma is_conditional_expectation_isfe_finite_part
        {f : Ts -> R}
        {ce : Ts -> Rbar}
        {rvf : RandomVariable dom borel_sa f}
        {isfe:IsFiniteExpectation prts f}
        {rvce : RandomVariable dom2 Rbar_borel_sa ce}
    : is_conditional_expectation dom2 f ce ->
      is_conditional_expectation dom2 f (Rbar_finite_part ce).

  Lemma is_conditional_expectation_isfe_finite_part_b
        {f : Ts -> R}
        {ce : Ts -> Rbar}
        {rvf : RandomVariable dom borel_sa f}
        {isfe:Rbar_IsFiniteExpectation prts ce}
        {rvce : RandomVariable dom2 Rbar_borel_sa ce}
    : is_conditional_expectation dom2 f (Rbar_finite_part ce) ->
      is_conditional_expectation dom2 f ce.
  
  Lemma IsFiniteExpectation_factor_out_scale_indicator (g:Ts->R) (f:Ts->R)
        {rvg : RandomVariable dom borel_sa g}
        {rvf : RandomVariable dom borel_sa f}
        {isfe:IsFiniteExpectation prts f}
        (a:R) :
    IsFiniteExpectation prts (rvmult (scale_val_indicator g a) f).

  Lemma IsFiniteExpectation_factor_out_frf (g:Ts->R) (f:Ts->R)
        {rvg : RandomVariable dom borel_sa g}
        {rvf : RandomVariable dom borel_sa f}
        {isfe:IsFiniteExpectation prts f}
        {frfg : FiniteRangeFunction g} :
    IsFiniteExpectation prts (rvmult (fun x : Ts => g x) f).

  Lemma Rbar_IsFiniteExpectation_factor_out_frf (g:Ts->R) (f:Ts->Rbar)
        {rvg : RandomVariable dom borel_sa g}
        {rvf : RandomVariable dom Rbar_borel_sa f}
        {isfe:Rbar_IsFiniteExpectation prts f}
        {frfg : FiniteRangeFunction g} :
    Rbar_IsFiniteExpectation prts (Rbar_rvmult (fun x : Ts => g x) f).

  Lemma Rbar_FinExp_FinExp (f:Ts->Rbar)
        {rv:RandomVariable dom Rbar_borel_sa f}
        {isfe:Rbar_IsFiniteExpectation prts f}
        {isfe':IsFiniteExpectation prts (Rbar_finite_part f)}:
    Rbar_FiniteExpectation prts f =
    FiniteExpectation prts (Rbar_finite_part f).

  Lemma is_conditional_expectation_factor_out_frf
        (f g:Ts->R) (ce:Ts->Rbar)
        {frfg : FiniteRangeFunction g}
        {rvf : RandomVariable dom borel_sa f}
        {rvg : RandomVariable dom2 borel_sa g}
        {rvce : RandomVariable dom2 Rbar_borel_sa ce}
        {rvgf: RandomVariable dom borel_sa (rvmult g f)}
        {rvgce: RandomVariable dom2 Rbar_borel_sa (Rbar_rvmult g ce)} :
    IsFiniteExpectation prts f ->
    is_conditional_expectation dom2 f ce ->
    is_conditional_expectation dom2 (rvmult g f) (Rbar_rvmult g ce).

  Lemma frf_min (f : Ts -> R)
    {frf : FiniteRangeFunction f} :
    forall x, RList.MinRlist frf_vals <= f x.

  Lemma frf_max (f : Ts -> R)
    {frf : FiniteRangeFunction f} :
    forall x, f x <= RList.MaxRlist frf_vals.
  
  Lemma IsFiniteExpectation_mult_finite_range_pos (f g : Ts -> R)
    {frf : FiniteRangeFunction g} :
    NonnegativeFunction f ->
    IsFiniteExpectation prts f ->
    IsFiniteExpectation prts (rvmult f g).

  Lemma IsFiniteExpectation_mult_finite_range (f g : Ts -> R)
        {rvf : RandomVariable dom borel_sa f}
        {rvg : RandomVariable dom borel_sa g}
        {frf : FiniteRangeFunction g} :
    IsFiniteExpectation prts f ->
    IsFiniteExpectation prts (rvmult f g).

     
  Theorem is_conditional_expectation_factor_out_nneg_both
          (f g:Ts -> R)
          (ce : Ts -> R)
          {nnegf : NonnegativeFunction f}
          {nnegg : NonnegativeFunction g}
          {nnegce : NonnegativeFunction ce}
          {rvf : RandomVariable dom borel_sa f}
          {rvg : RandomVariable dom2 borel_sa g}
          {rvce : RandomVariable dom2 borel_sa ce}
          {rvgf: RandomVariable dom borel_sa (rvmult f g)} :
    IsFiniteExpectation prts f ->
    is_conditional_expectation dom2 f ce ->
    is_conditional_expectation dom2 (rvmult f g) (Rbar_rvmult g ce).

  Lemma IsFiniteExpectation_abs f
    {rv : RandomVariable dom borel_sa f} :
    IsFiniteExpectation prts f ->
    IsFiniteExpectation prts (rvabs f).
    
  Lemma is_cond_rle_abs f ce ace
          {rvf : RandomVariable dom borel_sa f}
          {rvce : RandomVariable dom2 Rbar_borel_sa ce}
          {rvace : RandomVariable dom2 Rbar_borel_sa ace} :
    IsFiniteExpectation prts f ->
    is_conditional_expectation dom2 f ce ->
    is_conditional_expectation dom2 (rvabs f) ace ->
    almostR2 prts Rbar_le (Rbar_rvabs ce) ace.


  
  Lemma Jensen (rv_X : Ts -> R) (phi : R -> R)
        {rv : RandomVariable dom borel_sa rv_X}
        {isfe : IsFiniteExpectation prts rv_X}
        {isfephi : IsFiniteExpectation prts (fun x => phi (rv_X x))} :
    (forall c x y, convex phi c x y) ->
    FiniteExpectation prts (fun x => phi (rv_X x)) >= phi (FiniteExpectation prts rv_X).


  Lemma is_condexp_Jensen_helper (rv_X ce phice: Ts -> R) (phi : R -> R) (a b : nat -> R)
        {rv : RandomVariable dom borel_sa rv_X}
        {rvphi : RandomVariable dom borel_sa (fun x => phi (rv_X x))}
        {rvce : RandomVariable dom2 borel_sa ce}
        {rvace : RandomVariable dom2 borel_sa phice}
        {isfe : IsFiniteExpectation prts rv_X}
        {isfephi : IsFiniteExpectation prts (fun x => phi (rv_X x))}
        (iscondce : is_conditional_expectation dom2 rv_X ce)
        (iscond_phice : is_conditional_expectation dom2 (fun x => phi (rv_X x)) phice) :
    (forall (x: R),
        is_sup_seq (fun n => (a n) * x + (b n)) (phi x)) ->
    almostR2 (prob_space_sa_sub prts sub) Rbar_le
      (fun x => phi (ce x)) phice.

  Lemma is_condexp_Jensen (rv_X ce phice: Ts -> R) (phi : R -> R)
        {rv : RandomVariable dom borel_sa rv_X}
        {rvphi : RandomVariable dom borel_sa (fun x => phi (rv_X x))}
        {rvce : RandomVariable dom2 borel_sa ce}
        {rvace : RandomVariable dom2 borel_sa phice}
        {isfe : IsFiniteExpectation prts rv_X}
        {isfephi : IsFiniteExpectation prts (fun x => phi (rv_X x))}
        (iscondce : is_conditional_expectation dom2 rv_X ce)
        (iscond_phice : is_conditional_expectation dom2 (fun x => phi (rv_X x)) phice) :
    (forall c x y, convex phi c x y) ->
    almostR2 (prob_space_sa_sub prts sub) Rbar_le
      (fun x => phi (ce x)) phice.

  Lemma is_condexp_Jensen_abs (rv_X ce ace : Ts -> R)
        {rv : RandomVariable dom borel_sa rv_X}
        {rvce : RandomVariable dom2 borel_sa ce}
        {rvace : RandomVariable dom2 borel_sa ace}
        {isfe : IsFiniteExpectation prts rv_X} :
    is_conditional_expectation dom2 rv_X ce ->
    is_conditional_expectation dom2 (rvabs rv_X) ace ->
    almostR2 (prob_space_sa_sub prts sub) Rle
             (rvabs ce) ace.

  Lemma Rbar_mult_le_compat_l (r r1 r2 : Rbar) :
    Rbar_le 0 r ->
    Rbar_le r1 r2 -> Rbar_le (Rbar_mult r r1) (Rbar_mult r r2).

  Lemma Rbar_mult_le_compat_r (r r1 r2 : Rbar) :
    Rbar_le 0 r ->
    Rbar_le r1 r2 -> Rbar_le (Rbar_mult r1 r) (Rbar_mult r2 r).

  Theorem is_conditional_expectation_factor_out_nneg
          (f g : Ts -> R)
          (ce ace : Ts -> R)
          {nnegg : NonnegativeFunction g}
          {nnegace : NonnegativeFunction ace}
          {rvf : RandomVariable dom borel_sa f}
          {rvg : RandomVariable dom2 borel_sa g}
          {rvce : RandomVariable dom2 borel_sa ce}
          {rvace : RandomVariable dom2 borel_sa ace}
          {rvgf: RandomVariable dom borel_sa (rvmult f g)}
          {rvgaf: RandomVariable dom borel_sa (rvmult (rvabs f) g)}
          {rvgce: RandomVariable dom2 borel_sa (rvmult g ce)} :
    IsFiniteExpectation prts f ->
    IsFiniteExpectation prts (rvmult f g) ->
    is_conditional_expectation dom2 f ce ->
    is_conditional_expectation dom2 (rvabs f) ace ->
    is_conditional_expectation dom2 (rvmult f g) (Rbar_rvmult g ce).


  Theorem is_conditional_expectation_factor_out
        (f g ce ace : Ts -> R)
        {nnegace : NonnegativeFunction ace}
        {rvf : RandomVariable dom borel_sa f}
        {rvg : RandomVariable dom2 borel_sa g}
        {rvce : RandomVariable dom2 borel_sa ce}
        {rvace : RandomVariable dom2 borel_sa ace}
        {rvgf: RandomVariable dom borel_sa (rvmult f g)} :
    IsFiniteExpectation prts f ->
    IsFiniteExpectation prts (rvmult f g) ->
    is_conditional_expectation dom2 f ce ->
    is_conditional_expectation dom2 (rvabs f) ace ->
    is_conditional_expectation dom2 (rvmult f g) (Rbar_rvmult g ce).

  Lemma is_conditional_expectation_monotone_convergence
        (f : Ts -> R )
        (ce : Ts -> Rbar )
        (fn : nat -> Ts -> R)
        (cen : nat -> Ts -> Rbar)
        (rvf : RandomVariable dom borel_sa f)
        {rvce : RandomVariable dom2 Rbar_borel_sa ce}
        (nnf: NonnegativeFunction f)
        (nnce: Rbar_NonnegativeFunction ce)
        (rvfn : forall n, RandomVariable dom borel_sa (fn n))
        (nnfn : forall n, NonnegativeFunction (fn n))
        (nncen : forall n, Rbar_NonnegativeFunction (cen n))
        (rvcen : forall n, RandomVariable dom2 Rbar_borel_sa (cen n))
    :
    (forall (n:nat), Rbar_rv_le (fn n) f) ->
    (forall (n:nat), rv_le (fn n) (fn (S n))) ->
    (forall (n:nat), Rbar_rv_le (cen n) ce) ->
    (forall (n:nat), Rbar_rv_le (cen n) (cen (S n))) ->
    (forall (omega:Ts), is_Elim_seq (fun n => fn n omega) (f omega)) ->
    (forall (omega:Ts), is_Elim_seq (fun n => cen n omega) (ce omega)) ->
    (forall (n:nat), is_conditional_expectation dom2 (fn n) (cen n)) ->
    is_conditional_expectation dom2 f ce.
  
  Lemma is_conditional_expectation_monotone_convergence_almost
        (f : Ts -> R )
        (ce : Ts -> Rbar )
        (fn : nat -> Ts -> R)
        (cen : nat -> Ts -> Rbar)
        (rvf : RandomVariable dom borel_sa f)
        {rvce : RandomVariable dom2 Rbar_borel_sa ce}
        (nnf: almostR2 prts Rle (const 0) f)
        (nnce: almostR2 (prob_space_sa_sub prts sub) Rbar_le (const 0) ce)
        (rvfn : forall n, RandomVariable dom borel_sa (fn n))
        (nnfn : forall n, almostR2 prts Rle (const 0) (fn n))
        (nncen : forall n, almostR2 (prob_space_sa_sub prts sub) Rbar_le (const 0) (cen n))
        (rvcen : forall n, RandomVariable dom2 Rbar_borel_sa (cen n))
    :
    (forall (n:nat), almostR2 prts Rle (fn n) f) ->
    (forall (n:nat), almostR2 prts Rle (fn n) (fn (S n))) ->
    (forall (n:nat), almostR2 (prob_space_sa_sub prts sub) Rbar_le (cen n) ce) ->
    (forall (n:nat), almostR2 (prob_space_sa_sub prts sub) Rbar_le (cen n) (cen (S n))) ->
    (almost prts (fun omega => is_Elim_seq (fun n => fn n omega) (f omega))) ->
    (almost (prob_space_sa_sub prts sub) (fun (omega:Ts) => is_Elim_seq (fun n => cen n omega) (ce omega))) ->
    (forall (n:nat), is_conditional_expectation dom2 (fn n) (cen n)) ->
    is_conditional_expectation dom2 f ce.
End is_cond_exp.

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

  Theorem is_conditional_expectation_tower
        (f ce1: Ts -> R)
        (ce2: Ts -> Rbar)
        {rvf : RandomVariable dom borel_sa f}
        {rvce1 : RandomVariable dom2 borel_sa ce1}
        {rvce1' : RandomVariable dom borel_sa ce1}
        {rvce2 : RandomVariable dom3 Rbar_borel_sa ce2}
:
    is_conditional_expectation prts dom2 f (fun x => ce1 x) ->
    is_conditional_expectation prts dom3 f ce2 ->
    is_conditional_expectation prts dom3 ce1 ce2.

End is_cond_exp_props.

Section cond_exp_l2.

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

  Definition conditional_expectation_L2q
             (x:LpRRVq prts 2)
    : {v : L2RRVq_PreHilbert prts
        | unique
            (fun v : L2RRVq_PreHilbert prts =>
               ortho_phi prts dom2 v /\
               norm (minus (G:=(PreHilbert.AbelianGroup (L2RRVq_PreHilbert prts))) x v) =
               Glb_Rbar (fun r : R => exists w : L2RRVq_PreHilbert prts,
                             ortho_phi prts dom2 w /\
                             r = norm (minus (G:=(PreHilbert.AbelianGroup (L2RRVq_PreHilbert prts)))x w)))
            v}.

  Let nneg2 : nonnegreal := bignneg 2 big2.
  Canonical nneg2.

  Definition conditional_expectation_L2 (f :LpRRV prts 2) :
    {v : LpRRV prts 2
      | RandomVariable dom2 borel_sa v /\
        LpRRVnorm prts (LpRRVminus prts f v) =
        Glb_Rbar (fun r : R => exists w : LpRRV prts 2,
                      RandomVariable dom2 borel_sa (LpRRV_rv_X prts w) /\
                      r = LpRRVnorm prts (LpRRVminus prts f w)) /\
        (forall w:LpRRV prts 2, RandomVariable dom2 borel_sa w -> L2RRVinner prts (LpRRVminus prts f v) (LpRRVminus prts w v) <= 0) /\
        (forall w:LpRRV prts 2, RandomVariable dom2 borel_sa w -> L2RRVinner prts v w = L2RRVinner prts (pack_LpRRV prts f) w) /\

        (forall z: LpRRV prts 2, RandomVariable dom2 borel_sa z ->
                            (LpRRVnorm prts (LpRRVminus prts f z) =
                             Glb_Rbar (fun r : R => exists w : LpRRV prts 2,
                                           RandomVariable dom2 borel_sa (LpRRV_rv_X prts w) /\
                                           r = LpRRVnorm prts (LpRRVminus prts f w))) -> LpRRV_eq prts z v) /\
        
        (forall z: LpRRV prts 2, RandomVariable dom2 borel_sa z ->
                            (forall w:LpRRV prts 2, RandomVariable dom2 borel_sa w -> L2RRVinner prts (LpRRVminus prts f z) (LpRRVminus prts w z) <= 0) -> LpRRV_eq prts z v) /\
        (forall z: LpRRV prts 2, RandomVariable dom2 borel_sa z ->
                            (forall w:LpRRV prts 2, RandomVariable dom2 borel_sa w -> L2RRVinner prts z w = L2RRVinner prts (pack_LpRRV prts f) w) -> LpRRV_eq prts z v)

    }.

  Definition conditional_expectation_L2fun (f : Ts -> R)
             {rv : RandomVariable dom borel_sa f}
             {isl : IsLp prts 2 f} :
    LpRRV prts 2
    := proj1_sig (conditional_expectation_L2 (pack_LpRRV prts f)).

  Instance conditional_expectation_L2fun_rv
           (f : Ts -> R)
           {rv : RandomVariable dom borel_sa f}
           {isl : IsLp prts 2 f} :
    RandomVariable dom2 borel_sa (conditional_expectation_L2fun f).

  Instance conditional_expectation_L2fun_L2
           (f : Ts -> R)
           {rv : RandomVariable dom borel_sa f}
           {isl : IsLp prts 2 f} :
    IsLp prts 2 (conditional_expectation_L2fun f).

  Lemma conditional_expectation_L2fun_eq
        (f : Ts -> R)
        {rv : RandomVariable dom borel_sa f}
        {isl : IsLp prts 2 f} :
    LpRRVnorm prts (LpRRVminus prts (pack_LpRRV prts f) (conditional_expectation_L2fun f)) =
    Glb_Rbar
      (fun r : R =>
         exists w : LpRRV prts 2,
           RandomVariable dom2 borel_sa w /\ r = LpRRVnorm prts (LpRRVminus prts (pack_LpRRV prts f) w)).

  Lemma conditional_expectation_L2fun_eq_finite
        (f : Ts -> R)
        {rv : RandomVariable dom borel_sa f}
        {isl : IsLp prts 2 f} :
    is_finite (Glb_Rbar
      (fun r : R =>
         exists w : LpRRV prts 2,
           RandomVariable dom2 borel_sa w /\ r = LpRRVnorm prts (LpRRVminus prts (pack_LpRRV prts f) w))).

  Lemma conditional_expectation_L2fun_eq1
        (f : Ts -> R)
        {rv : RandomVariable dom borel_sa f}
        {isl : IsLp prts 2 f} :
    (forall w:LpRRV prts 2, RandomVariable dom2 borel_sa w -> L2RRVinner prts (LpRRVminus prts (pack_LpRRV prts f) (conditional_expectation_L2fun f)) (LpRRVminus prts w (conditional_expectation_L2fun f)) <= 0).

  Lemma conditional_expectation_L2fun_eq2
        (f : Ts -> R)
        {rv : RandomVariable dom borel_sa f}
        {isl : IsLp prts 2 f} :
    (forall w:LpRRV prts 2, RandomVariable dom2 borel_sa w -> L2RRVinner prts (conditional_expectation_L2fun f) w = L2RRVinner prts (pack_LpRRV prts f) w).

  Lemma conditional_expectation_L2fun_eq3
        (f : Ts -> R)
        {rv : RandomVariable dom borel_sa f}
        {isl : IsLp prts 2 f} :
    is_conditional_expectation prts dom2 f (fun x => (conditional_expectation_L2fun f) x).

  Lemma conditional_expectation_L2fun_unique
        (f : Ts -> R)
        {rv : RandomVariable dom borel_sa f}
        {isl : IsLp prts 2 f}
        (z: LpRRV prts 2)
        {z_rv:RandomVariable dom2 borel_sa z} :
    (LpRRVnorm prts (LpRRVminus prts (pack_LpRRV prts f) z) =
     Glb_Rbar (fun r : R => exists w : LpRRV prts 2,
                   RandomVariable dom2 borel_sa (LpRRV_rv_X prts w) /\
                   r = LpRRVnorm prts (LpRRVminus prts (pack_LpRRV prts f) w))) ->
    LpRRV_eq prts z (conditional_expectation_L2fun f).

  Lemma conditional_expectation_L2fun_unique1
        (f : Ts -> R)
        {rv : RandomVariable dom borel_sa f}
        {isl : IsLp prts 2 f}
        (z: LpRRV prts 2)
        {z_rv:RandomVariable dom2 borel_sa z} :
    (forall w:LpRRV prts 2, RandomVariable dom2 borel_sa w -> L2RRVinner prts (LpRRVminus prts (pack_LpRRV prts f) z) (LpRRVminus prts w z) <= 0) -> LpRRV_eq prts z (conditional_expectation_L2fun f).

  Lemma conditional_expectation_L2fun_unique2
        (f : Ts -> R)
        {rv : RandomVariable dom borel_sa f}
        {isl : IsLp prts 2 f}
        (z: LpRRV prts 2)
        {z_rv:RandomVariable dom2 borel_sa z} :
    (forall w:LpRRV prts 2, RandomVariable dom2 borel_sa w -> L2RRVinner prts z w = L2RRVinner prts (pack_LpRRV prts f) w) -> LpRRV_eq prts z (conditional_expectation_L2fun f).

  Lemma conditional_expectation_L2fun_const
        (c : R) :
    LpRRV_eq prts
             (LpRRVconst prts c)
             (conditional_expectation_L2fun (const c)).

  Instance IsLp_min_const_nat (f : Ts -> R) (n : nat)
           {nneg : NonnegativeFunction f} :
    IsLp prts 2 (rvmin f (const (INR n))).

  Lemma conditional_expectation_L2fun_proper (f1 f2 : Ts -> R)
        {rv1 : RandomVariable dom borel_sa f1}
        {rv2 : RandomVariable dom borel_sa f2}
        {isl1 : IsLp prts 2 f1}
        {isl2 : IsLp prts 2 f2} :
    almostR2 prts eq f1 f2 ->
    LpRRV_eq prts
             (conditional_expectation_L2fun f1)
             (conditional_expectation_L2fun f2).

  Lemma conditional_expectation_L2fun_nonneg (f : Ts -> R)
        {rv : RandomVariable dom borel_sa f}
        {isl : IsLp prts 2 f}
        {nneg: NonnegativeFunction f} :
    almostR2 (prob_space_sa_sub prts sub) Rle (const 0) (conditional_expectation_L2fun f).
  
  Lemma conditional_expectation_L2fun_nonneg_prts (f : Ts -> R)
        {rv : RandomVariable dom borel_sa f}
        {isl : IsLp prts 2 f}
        {nneg: NonnegativeFunction f} :
    almostR2 prts Rle (const 0) (conditional_expectation_L2fun f).

  Local Existing Instance Rbar_le_pre.

  Lemma conditional_expectation_L2fun_plus f1 f2
        {rv1 : RandomVariable dom borel_sa f1}
        {rv2 : RandomVariable dom borel_sa f2}
        {isl1 : IsLp prts 2 f1}
        {isl2 : IsLp prts 2 f2} :
    LpRRV_eq prts
             (conditional_expectation_L2fun (rvplus f1 f2))
             (LpRRVplus prts (conditional_expectation_L2fun f1) (conditional_expectation_L2fun f2)).
  
End cond_exp_l2.

Section cond_exp2.

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

  Lemma conditional_expectation_L2fun_le (f1 f2 : Ts -> R)
        {rv1 : RandomVariable dom borel_sa f1}
        {rv2 : RandomVariable dom borel_sa f2}
        {isl1 : IsLp prts 2 f1}
        {isl2 : IsLp prts 2 f2} :
    rv_le f1 f2 ->
    almostR2 (prob_space_sa_sub prts sub) Rle (conditional_expectation_L2fun prts sub f1)
             (conditional_expectation_L2fun prts sub f2).

  Lemma conditional_expectation_L2fun_le_prts (f1 f2 : Ts -> R)
        {rv1 : RandomVariable dom borel_sa f1}
        {rv2 : RandomVariable dom borel_sa f2}
        {isl1 : IsLp prts 2 f1}
        {isl2 : IsLp prts 2 f2} :
    rv_le f1 f2 ->
    almostR2 prts Rle (conditional_expectation_L2fun prts sub f1)
             (conditional_expectation_L2fun prts sub f2).

  Local Existing Instance Rbar_le_pre.
  Local Existing Instance IsLp_min_const_nat.
  Local Existing Instance conditional_expectation_L2fun_rv.

  Definition NonNegConditionalExpectation (f : Ts -> R)
             {rv : RandomVariable dom borel_sa f}
             {nnf : NonnegativeFunction f} : Ts -> Rbar :=
    Rbar_rvlim (fun n => LpRRV_rv_X _ (conditional_expectation_L2fun prts sub (rvmin f (const (INR n))))).

  Lemma NonNegCondexp_almost_increasing (f : Ts -> R)
          {rv : RandomVariable dom borel_sa f}
        {nnf : NonnegativeFunction f} :
    almost (prob_space_sa_sub prts sub)
           (fun x =>
              forall n,
                conditional_expectation_L2fun prts sub (rvmin f (const (INR n))) x
                <= conditional_expectation_L2fun prts sub (rvmin f (const (INR (S n)))) x).

  Lemma NonNegCondexp_almost_increasing_prts (f : Ts -> R)
        {rv : RandomVariable dom borel_sa f}
        {nnf : NonnegativeFunction f} :
    almost prts
           (fun x =>
              forall n,
                conditional_expectation_L2fun prts sub (rvmin f (const (INR n))) x
                <= conditional_expectation_L2fun prts sub (rvmin f (const (INR (S n)))) x).

  Lemma almost_Rbar_rvlim_condexp_incr_indicator_rv (f : Ts -> R)
        {rv : RandomVariable dom borel_sa f}
        {nnf : NonnegativeFunction f}
        (E : event dom2) :
    ps_P (ProbSpace:=(prob_space_sa_sub prts sub)) E = 1 ->
    (forall x0 : Ts,
        E x0 ->
        forall n : nat,
          conditional_expectation_L2fun prts sub (rvmin f (const (INR n))) x0 <=
          conditional_expectation_L2fun prts sub (rvmin f (const (INR (S n)))) x0) ->
    (RandomVariable
       dom2 Rbar_borel_sa
       (Rbar_rvlim
          (fun n0 : nat =>
             rvmult (conditional_expectation_L2fun prts sub (rvmin f (const (INR n0))))
                    (EventIndicator (classic_dec E))))).

  Lemma NonNegCondexp_almost_nonneg (f : Ts -> R)
        {rv : RandomVariable dom borel_sa f}
        {nnf : NonnegativeFunction f} :
    almostR2 (prob_space_sa_sub prts sub) Rbar_le (const 0) (NonNegConditionalExpectation f).

  Lemma NonNegCondexp_almost_nonneg_prts (f : Ts -> R)
        {rv : RandomVariable dom borel_sa f}
        {nnf : NonnegativeFunction f} :
    almostR2 prts Rbar_le (const 0) (NonNegConditionalExpectation f).

  Lemma rvlim_rvmin_indicator (f : Ts -> R) (P:pre_event Ts) (dec:dec_pre_event P) :
    rv_eq (fun x=> Finite (rvmult f (EventIndicator dec) x))
          (Rbar_rvlim (fun n : nat => rvmult (rvmin f (const (INR n))) (EventIndicator dec))).
    
  Lemma NonNegCondexp_is_Rbar_condexp_almost0 (f : Ts -> R)
        {rv : RandomVariable dom borel_sa f}
        {nnf : NonnegativeFunction f} :
    exists (g : nat -> Ts -> R),
      (forall n, (NonnegativeFunction (g n)))
      /\ (forall n, (rv_le (g n) (g (S n))))
      /\ RandomVariable dom2 Rbar_borel_sa (Rbar_rvlim g)
      /\ exists (g_rv:forall n, RandomVariable dom2 borel_sa (g n)),
          (forall n, is_conditional_expectation prts dom2 (rvmin f (const (INR n))) (g n)).

  Lemma NonNegCondexp_is_Rbar_condexp_g (f : Ts -> R)
        {rv : RandomVariable dom borel_sa f}
        {nnf : NonnegativeFunction f} :
    exists (g : nat -> Ts -> R),
      Rbar_NonnegativeFunction (Rbar_rvlim g)
      /\ exists (g_rv : RandomVariable dom2 Rbar_borel_sa (Rbar_rvlim g)),
        is_conditional_expectation prts dom2 f (Rbar_rvlim g).