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).

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

  Definition IsFiniteExpectation_dec (f: Ts -> R) :
    {IsFiniteExpectation prts f} + {~ IsFiniteExpectation prts f}.
  
  Lemma NonNegCondexp'' (f : Ts -> R)
        {rv : RandomVariable dom borel_sa f}
        {nnf : NonnegativeFunction f} :
    { g : Ts -> Rbar |
      Rbar_NonnegativeFunction g /\
      (RandomVariable dom2 borel_sa f -> g = (fun x => Finite (f x)))
      /\ (IsFiniteExpectation prts f -> exists gr, g = fun x => Finite (gr x))
      /\ exists (g_rv : RandomVariable dom2 Rbar_borel_sa g),
          is_conditional_expectation prts dom2 f g }.

  Definition NonNegCondexp (f : Ts -> R)
             {rv : RandomVariable dom borel_sa f}
             {nnf : NonnegativeFunction f} : Ts -> Rbar
    := proj1_sig (NonNegCondexp'' f).

  Global Instance NonNegCondexp_nneg (f : Ts -> R)
         {rv : RandomVariable dom borel_sa f}
         {nnf : NonnegativeFunction f} :
    Rbar_NonnegativeFunction (NonNegCondexp f).

  Global Instance NonNegCondexp_rv (f : Ts -> R)
         {rv : RandomVariable dom borel_sa f}
         {nnf : NonnegativeFunction f} :
    RandomVariable dom2 Rbar_borel_sa (NonNegCondexp f).

  Lemma NonNegCondexp_cond_exp (f : Ts -> R)
        {rv : RandomVariable dom borel_sa f}
        {nnf : NonnegativeFunction f} :
    is_conditional_expectation prts dom2 f (NonNegCondexp f).

  Lemma NonNegCondexp_finite (f : Ts -> R)
          {rv : RandomVariable dom borel_sa f}
          {nnf : NonnegativeFunction f}
          {rvce : RandomVariable dom2 Rbar_borel_sa (NonNegCondexp f)}
          {isfe:IsFiniteExpectation prts f} :
      exists gr, NonNegCondexp f = fun x => Finite (gr x).

  Lemma NonNegCondexp_id (f : Ts -> R)
        {rv : RandomVariable dom borel_sa f}
        {rv2 : RandomVariable dom2 borel_sa f}
        {nnf : NonnegativeFunction f}
        {rvce : RandomVariable dom2 Rbar_borel_sa (NonNegCondexp f)} :
    NonNegCondexp f = (fun x => Finite (f x)).

  Lemma conditional_expectation_L2fun_cond_exp
        (f : Ts -> R)
        {rv : RandomVariable dom borel_sa f} {isl : IsLp prts 2 f} :
    is_conditional_expectation prts dom2 f (LpRRV_rv_X _ (conditional_expectation_L2fun prts sub f)).

  Lemma NonNegCondexp_ext (f1 f2 : Ts -> R)
        {rv1 : RandomVariable dom borel_sa f1}
        {rv2 : RandomVariable dom borel_sa f2}
        {nnf1 : NonnegativeFunction f1}
        {nnf2 : NonnegativeFunction f2} :
    rv_eq f1 f2 ->
    rv_eq (NonNegCondexp f1) (NonNegCondexp f2).

  Definition ConditionalExpectation (f : Ts -> R)
             {rv : RandomVariable dom borel_sa f} : Ts -> Rbar :=
    Rbar_rvminus (NonNegCondexp (pos_fun_part f))
                 (NonNegCondexp (neg_fun_part f)).

  Lemma Condexp_nneg_simpl (f : Ts -> R)
        {rv : RandomVariable dom borel_sa f}
        {nnf : NonnegativeFunction f} :
    rv_eq (ConditionalExpectation f) (NonNegCondexp f).

  Lemma ConditionalExpectation_ext (f1 f2 : Ts -> R)
        {rv1 : RandomVariable dom borel_sa f1}
        {rv2 : RandomVariable dom borel_sa f2} :
    rv_eq f1 f2 ->
    rv_eq (ConditionalExpectation f1) (ConditionalExpectation f2).

  Global Instance Condexp_rv (f : Ts -> R)
         {rv : RandomVariable dom borel_sa f} :
    RandomVariable dom2 Rbar_borel_sa (ConditionalExpectation f).

  Lemma Condexp_cond_exp_nneg (f : Ts -> R)
        {rv : RandomVariable dom borel_sa f}
        {isfe:NonnegativeFunction f}
    :
      is_conditional_expectation prts dom2 f (ConditionalExpectation f).
  
  Theorem Condexp_cond_exp (f : Ts -> R)
        {rv : RandomVariable dom borel_sa f}
        {isfe:IsFiniteExpectation prts f}
    :
      is_conditional_expectation prts dom2 f (ConditionalExpectation f).

  Global Instance Condexp_nneg (f : Ts -> R)
         {rv : RandomVariable dom borel_sa f}
         {nnf : NonnegativeFunction f} :
    Rbar_NonnegativeFunction (ConditionalExpectation f).

  Theorem Condexp_id (f : Ts -> R)
        {rv : RandomVariable dom borel_sa f}
        {rv2 : RandomVariable dom2 borel_sa f} :
    rv_eq (ConditionalExpectation f) (fun x => Finite (f x)).

  Corollary Condexp_const c :
    rv_eq (ConditionalExpectation (const c)) (const (Finite c)).

  Theorem Condexp_finite (f : Ts -> R)
          {rv : RandomVariable dom borel_sa f}
          {isfe:IsFiniteExpectation prts f} :
      exists gr, ConditionalExpectation f = fun x => Finite (gr x).

  Theorem Condexp_is_finite (f : Ts -> R)
          {rv : RandomVariable dom borel_sa f}
          {isfe:IsFiniteExpectation prts f} :
    forall x, is_finite (ConditionalExpectation f x).

  Lemma Condexp_Expectation (f : Ts -> R)
        {rv : RandomVariable dom borel_sa f}
        {isfe:IsFiniteExpectation prts f}
    :
      Expectation f =
      Rbar_Expectation (ConditionalExpectation f).

    Global Instance Condexp_Rbar_isfe (f : Ts -> R)
           {rv : RandomVariable dom borel_sa f}
           {isfe:IsFiniteExpectation prts f}
      : Rbar_IsFiniteExpectation prts (ConditionalExpectation f).

  Lemma NonNegCondexp_proper (f1 f2 : Ts -> R)
        {rv1 : RandomVariable dom borel_sa f1}
        {rv2 : RandomVariable dom borel_sa f2}
        {nnf1 : NonnegativeFunction f1}
        {nnf2 : NonnegativeFunction f2} :
    almostR2 prts eq f1 f2 ->
    almostR2 (prob_space_sa_sub prts sub) eq
             (NonNegCondexp f1)
             (NonNegCondexp f2).

  Lemma Condexp_proper (f1 f2 : Ts -> R)
        {rv1 : RandomVariable dom borel_sa f1}
        {rv2 : RandomVariable dom borel_sa f2} :
    almostR2 prts eq f1 f2 ->
    almostR2 (prob_space_sa_sub prts sub) eq
             (ConditionalExpectation f1)
             (ConditionalExpectation f2).

  Lemma Condexp_ale (f1 f2 : Ts -> R)
        {rv1 : RandomVariable dom borel_sa f1}
        {rv2 : RandomVariable dom borel_sa f2}
        {isfe1:IsFiniteExpectation prts f1}
        {isfe2:IsFiniteExpectation prts f2}

    :
    almostR2 prts Rle f1 f2 ->
    almostR2 (prob_space_sa_sub prts sub) Rbar_le
             (ConditionalExpectation f1)
             (ConditionalExpectation f2).

  Lemma Condexp_scale c (f : Ts -> R)
        {rv : RandomVariable dom borel_sa f}
        {isfe:IsFiniteExpectation prts f}
    :
    almostR2 (prob_space_sa_sub prts sub) eq
             (ConditionalExpectation (rvscale c f))
             (Rbar_rvmult (const (Finite c)) (ConditionalExpectation f)).

  Lemma Condexp_opp (f : Ts -> R)
        {rv : RandomVariable dom borel_sa f}
        {isfe:IsFiniteExpectation prts f}
    :
    almostR2 (prob_space_sa_sub prts sub) eq
             (ConditionalExpectation (rvopp f))
             (Rbar_rvopp (ConditionalExpectation f)).

  Lemma Condexp_plus (f1 f2 : Ts -> R)
        {rv1 : RandomVariable dom borel_sa f1}
        {rv2 : RandomVariable dom borel_sa f2}
        {isfe1:IsFiniteExpectation prts f1}
        {isfe2:IsFiniteExpectation prts f2}
    :
    almostR2 (prob_space_sa_sub prts sub) eq
             (ConditionalExpectation (rvplus f1 f2))
             (Rbar_rvplus (ConditionalExpectation f1) (ConditionalExpectation f2)).

  Lemma Condexp_minus (f1 f2 : Ts -> R)
        {rv1 : RandomVariable dom borel_sa f1}
        {rv2 : RandomVariable dom borel_sa f2}
        {isfe1:IsFiniteExpectation prts f1}
        {isfe2:IsFiniteExpectation prts f2}
    :
    almostR2 (prob_space_sa_sub prts sub) eq
             (ConditionalExpectation (rvminus f1 f2))
             (Rbar_rvminus (ConditionalExpectation f1) (ConditionalExpectation f2)).

  Theorem Condexp_factor_out
        (f g : Ts -> R)
        {rvf : RandomVariable dom borel_sa f}
        {rvg : RandomVariable dom2 borel_sa g}
        {rvgf: RandomVariable dom borel_sa (rvmult f g)}
        {isfef: IsFiniteExpectation prts f}
        {isfefg:IsFiniteExpectation prts (rvmult f g)} :
    almostR2 (prob_space_sa_sub prts sub) eq
             (ConditionalExpectation (rvmult f g))
             (Rbar_rvmult g (ConditionalExpectation f)).

  Lemma Condexp_L2 (f : Ts -> R)
          {rv : RandomVariable dom borel_sa f}
          {isfe:IsFiniteExpectation prts f}
          {islp : IsLp prts 2 f}
    :
      almostR2 (prob_space_sa_sub prts sub) eq
               (ConditionalExpectation f)
               (fun x => conditional_expectation_L2fun prts sub f x).

  Lemma Condexp_L2_inner
        (f : Ts -> R)
        {frv : RandomVariable dom borel_sa f}
        {fisl : IsLp prts 2 f}
        (w : Ts -> R)
        {wrv:RandomVariable dom2 borel_sa w}
        {wisl:IsLp prts 2 w} :
    Rbar_Expectation (Rbar_rvmult (ConditionalExpectation f) w) =
    Expectation (rvmult f w).

  Lemma L2_min_dist_finite
        (f : Ts -> R)
        {rv : RandomVariable dom borel_sa f}
        {isl : IsLp prts 2 f} :
    is_finite (Glb_Rbar
      (fun r : R =>
         exists w : Ts -> R,
           RandomVariable dom2 borel_sa w /\ IsLp prts 2 w /\
           Some (Finite r) = lift (fun x => Rbar_power x (/ 2)) (Expectation (rvsqr (rvminus f w))))).

  Lemma Condexp_L2_min_dist
        (f : Ts -> R)
        {rv : RandomVariable dom borel_sa f}
        {isl : IsLp prts 2 f} :
    lift (fun x => Rbar_power x (/ 2))
         (Rbar_Expectation (Rbar_rvsqr (Rbar_rvminus f (ConditionalExpectation f))))
    =
    Some (Glb_Rbar
      (fun r : R =>
         exists w : Ts -> R,
           RandomVariable dom2 borel_sa w /\ IsLp prts 2 w /\
           Some (Finite r) = lift (fun x => Rbar_power x (/ 2)) (Expectation (rvsqr (rvminus f w))))).

  Lemma Condexp_monotone_convergence
        (f : Ts -> R)
        (fn : nat -> Ts -> R)
        {rvf : RandomVariable dom borel_sa f}
        {rvfn : forall n, RandomVariable dom borel_sa (fn n)}
        (nnf: almostR2 prts Rle (const 0) f)
        (nnfn : forall n, almostR2 prts Rle (const 0) (fn n))
        (fbound:forall (n:nat), almostR2 prts Rle (fn n) f)
        (fincr:forall (n:nat), almostR2 prts Rle (fn n) (fn (S n)))
        {isfef:IsFiniteExpectation prts f}
        {isfefn:forall n, IsFiniteExpectation prts (fn n)}
        (flim:almost prts (fun omega => is_Elim_seq (fun n => fn n omega) (f omega))) :
    almost (prob_space_sa_sub prts sub)
           (fun omega => is_Elim_seq (fun n => ConditionalExpectation (fn n) omega) (ConditionalExpectation f omega)).
  
End cond_exp2.

Section 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 Condexp_tower
        (f ce: Ts -> R)
        {rvf : RandomVariable dom borel_sa f}
        {isfe: IsFiniteExpectation prts f}
        {rvce : RandomVariable dom2 borel_sa ce}
        {rvce' : RandomVariable dom borel_sa ce}
    :
      almostR2 (prob_space_sa_sub prts sub) eq
               (ConditionalExpectation prts sub f) (fun x => ce x) ->
      almostR2 (prob_space_sa_sub prts (transitivity sub2 sub)) eq
               (ConditionalExpectation prts (transitivity sub2 sub) ce)
               (ConditionalExpectation prts (transitivity sub2 sub) f).

End cond_exp_props.

Section fin_cond_exp.

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


  Definition FiniteConditionalExpectation
             (f : Ts -> R)
             {rv : RandomVariable dom borel_sa f}
             {isfe:IsFiniteExpectation prts f} : Ts -> R.

  Lemma FiniteConditionalExpectation_ext (f1 f2 : Ts -> R)
        {rv1 : RandomVariable dom borel_sa f1}
        {rv2 : RandomVariable dom borel_sa f2}
        {isfe1:IsFiniteExpectation prts f1}
        {isfe2:IsFiniteExpectation prts f2}
    : rv_eq f1 f2 ->
      rv_eq (FiniteConditionalExpectation f1) (FiniteConditionalExpectation f2).

  Lemma FiniteCondexp_eq
             (f : Ts -> R)
             {rv : RandomVariable dom borel_sa f}
             {isfe:IsFiniteExpectation prts f} :
    ConditionalExpectation prts sub f = fun x => (Finite (FiniteConditionalExpectation f x)).
  
    Global Instance FiniteCondexp_rv (f : Ts -> R)
         {rv : RandomVariable dom borel_sa f}
         {isfe:IsFiniteExpectation prts f} :
    RandomVariable dom2 borel_sa (FiniteConditionalExpectation f).

    Instance FiniteCondexp_rv' (f : Ts -> R)
           {rv : RandomVariable dom borel_sa f}
           {isfe:IsFiniteExpectation prts f} :
      RandomVariable dom borel_sa (FiniteConditionalExpectation f).
    
  Lemma FiniteCondexp_is_cond_exp (f : Ts -> R)
        {rv : RandomVariable dom borel_sa f}
        {isfe:IsFiniteExpectation prts f}
    :
      is_conditional_expectation prts dom2 f (FiniteConditionalExpectation f).

  Theorem FiniteCondexp_cond_exp (f : Ts -> R)
        {rv : RandomVariable dom borel_sa f}
        {isfe:IsFiniteExpectation prts f}
        {P:pre_event Ts}
        (dec:dec_pre_event P)
        (saP:sa_sigma (SigmaAlgebra := dom2) P) :
    Expectation (rvmult f (EventIndicator dec)) =
    Expectation (rvmult (FiniteConditionalExpectation f) (EventIndicator dec)).

  Corollary FiniteCondexp_cond_exp_classic (f : Ts -> R)
        {rv : RandomVariable dom borel_sa f}
        {isfe:IsFiniteExpectation prts f}
        {P:pre_event Ts}
        (saP:sa_sigma (SigmaAlgebra := dom2) P) :
    Expectation (rvmult f (EventIndicator (classic_dec P))) =
    Expectation (rvmult (FiniteConditionalExpectation f) (EventIndicator (classic_dec P))).

  Corollary FiniteCondexp_cond_exp_event (f : Ts -> R)
        {rv : RandomVariable dom borel_sa f}
        {isfe:IsFiniteExpectation prts f}
        {P:event dom2}
        (dec:dec_event P) :
    Expectation (rvmult f (EventIndicator dec)) =
    Expectation (rvmult (FiniteConditionalExpectation f) (EventIndicator dec)).

  Corollary FiniteCondexp_cond_exp_event_classic (f : Ts -> R)
        {rv : RandomVariable dom borel_sa f}
        {isfe:IsFiniteExpectation prts f}
        (P:event dom2) :
    Expectation (rvmult f (EventIndicator (classic_dec P))) =
    Expectation (rvmult (FiniteConditionalExpectation f) (EventIndicator (classic_dec P))).

  Global Instance FiniteCondexp_nneg (f : Ts -> R)
         {rv : RandomVariable dom borel_sa f}
         {isfe:IsFiniteExpectation prts f}
         {nnf : NonnegativeFunction f} :
    NonnegativeFunction (FiniteConditionalExpectation f).

  Theorem FiniteCondexp_id (f : Ts -> R)
          {rv : RandomVariable dom borel_sa f}
          {rv2 : RandomVariable dom2 borel_sa f}
          {isfe:IsFiniteExpectation prts f}
    :
      rv_eq (FiniteConditionalExpectation f) f.

  Corollary FiniteCondexp_const c :
    rv_eq (FiniteConditionalExpectation (const c)) (const c).

  Theorem FiniteCondexp_Expectation (f : Ts -> R)
          {rv : RandomVariable dom borel_sa f}
          {isfe:IsFiniteExpectation prts f}
    :
      Expectation (FiniteConditionalExpectation f) =
      Expectation f.

  Global Instance FiniteCondexp_isfe (f : Ts -> R)
          {rv : RandomVariable dom borel_sa f}
          {isfe:IsFiniteExpectation prts f}
    : IsFiniteExpectation prts (FiniteConditionalExpectation f).

  Global Instance FiniteCondexp_isfe2 (f : Ts -> R)
          {rv : RandomVariable dom borel_sa f}
          {isfe:IsFiniteExpectation prts f}
    : IsFiniteExpectation (prob_space_sa_sub prts sub) (FiniteConditionalExpectation f).

  Theorem FiniteCondexp_FiniteExpectation (f : Ts -> R)
          {rv : RandomVariable dom borel_sa f}
          {isfe:IsFiniteExpectation prts f}
          {isfe':IsFiniteExpectation prts (FiniteConditionalExpectation f)}
    :
      FiniteExpectation prts (FiniteConditionalExpectation f) =
      FiniteExpectation prts f.

  Theorem FiniteCondexp_FiniteExpectation_sub (f : Ts -> R)
          {rv : RandomVariable dom borel_sa f}
          {isfe:IsFiniteExpectation prts f}
          {isfe':IsFiniteExpectation prts (FiniteConditionalExpectation f)}
    :
      FiniteExpectation (prob_space_sa_sub prts sub) (FiniteConditionalExpectation f) =
      FiniteExpectation prts f.

  Theorem FiniteCondexp_proper (f1 f2 : Ts -> R)
        {rv1 : RandomVariable dom borel_sa f1}
        {rv2 : RandomVariable dom borel_sa f2}
        {isfe1:IsFiniteExpectation prts f1}
        {isfe2:IsFiniteExpectation prts f2}:
    almostR2 prts eq f1 f2 ->
    almostR2 (prob_space_sa_sub prts sub) eq
             (FiniteConditionalExpectation f1)
             (FiniteConditionalExpectation f2).
    
  Lemma FiniteCondexp_ale (f1 f2 : Ts -> R)
        {rv1 : RandomVariable dom borel_sa f1}
        {rv2 : RandomVariable dom borel_sa f2}
        {isfe1:IsFiniteExpectation prts f1}
        {isfe2:IsFiniteExpectation prts f2} :
    almostR2 prts Rle f1 f2 ->
    almostR2 (prob_space_sa_sub prts sub) Rle
             (FiniteConditionalExpectation f1)
             (FiniteConditionalExpectation f2).

  Lemma FiniteCondexp_scale c (f : Ts -> R)
        {rv : RandomVariable dom borel_sa f}
        {isfe:IsFiniteExpectation prts f} :
    almostR2 (prob_space_sa_sub prts sub) eq
             (FiniteConditionalExpectation (rvscale c f))
             (rvscale c (FiniteConditionalExpectation f)).

  Lemma FiniteCondexp_opp (f : Ts -> R)
        {rv : RandomVariable dom borel_sa f}
        {isfe:IsFiniteExpectation prts f} :
    almostR2 (prob_space_sa_sub prts sub) eq
             (FiniteConditionalExpectation (rvopp f))
             (rvopp (FiniteConditionalExpectation f)).

  Lemma FiniteCondexp_plus (f1 f2 : Ts -> R)
        {rv1 : RandomVariable dom borel_sa f1}
        {rv2 : RandomVariable dom borel_sa f2}
        {isfe1:IsFiniteExpectation prts f1}
        {isfe2:IsFiniteExpectation prts f2} :
    almostR2 (prob_space_sa_sub prts sub) eq
             (FiniteConditionalExpectation (rvplus f1 f2))
             (rvplus (FiniteConditionalExpectation f1) (FiniteConditionalExpectation f2)).

  Lemma FiniteCondexp_minus (f1 f2 : Ts -> R)
        {rv1 : RandomVariable dom borel_sa f1}
        {rv2 : RandomVariable dom borel_sa f2}
        {isfe1:IsFiniteExpectation prts f1}
        {isfe2:IsFiniteExpectation prts f2} :
    almostR2 (prob_space_sa_sub prts sub) eq
             (FiniteConditionalExpectation (rvminus f1 f2))
             (rvminus (FiniteConditionalExpectation f1) (FiniteConditionalExpectation f2)).

  Lemma FiniteCondexp_Jensen (rv_X : Ts -> R) (phi : R -> R)
        {rv : RandomVariable dom borel_sa rv_X}
        {rvphi : RandomVariable dom borel_sa (fun x => phi (rv_X x))}
        {isfe : IsFiniteExpectation prts rv_X}
        {isfephi : IsFiniteExpectation prts (fun x => phi (rv_X x))} :
    (forall c x y, convex phi c x y) ->
    almostR2 (prob_space_sa_sub prts sub) Rle
      (fun x => phi ((FiniteConditionalExpectation rv_X) x))
      (FiniteConditionalExpectation (fun x => phi (rv_X x))).

  Lemma FiniteCondexp_abs (f: Ts -> R)
        {rv : RandomVariable dom borel_sa f}
        {isfe : IsFiniteExpectation prts f}
        {isfeabs : IsFiniteExpectation prts (rvabs f)} :
    almostR2 (prob_space_sa_sub prts sub) Rle
             (rvabs (FiniteConditionalExpectation f))
             (FiniteConditionalExpectation (rvabs f)).

  Theorem FiniteCondexp_factor_out
        (f g : Ts -> R)
        {rvf : RandomVariable dom borel_sa f}
        {rvg : RandomVariable dom2 borel_sa g}
        {rvgf: RandomVariable dom borel_sa (rvmult f g)}
        {isfef: IsFiniteExpectation prts f}
        {isfefg:IsFiniteExpectation prts (rvmult f g)} :
    almostR2 (prob_space_sa_sub prts sub) eq
             (FiniteConditionalExpectation (rvmult f g))
             (rvmult g (FiniteConditionalExpectation f)).
    
    Theorem FiniteCondexp_factor_out_l
            (f g : Ts -> R)
            {rvf : RandomVariable dom borel_sa f}
            {rvg : RandomVariable dom2 borel_sa g}
            {rvgf: RandomVariable dom borel_sa (rvmult g f)}
            {isfef: IsFiniteExpectation prts f}
            {isfefg:IsFiniteExpectation prts (rvmult g f)} :
      almostR2 (prob_space_sa_sub prts sub) eq
               (FiniteConditionalExpectation (rvmult g f))
               (rvmult g (FiniteConditionalExpectation f)).
    
    Lemma FiniteCondexp_factor_out_zero
        (f g : Ts -> R)
        {rvf : RandomVariable dom borel_sa f}
        {rvg : RandomVariable dom2 borel_sa g}
        {isfef: IsFiniteExpectation prts f}
        {isfefg:IsFiniteExpectation prts (rvmult f g)} :
    almostR2 prts eq (FiniteConditionalExpectation f) (const 0) ->
    FiniteExpectation prts (rvmult f g) = 0.
      
  Lemma FiniteCondexp_factor_out_zero_swapped
        (f g : Ts -> R)
        {rvf : RandomVariable dom borel_sa f}
        {rvg : RandomVariable dom2 borel_sa g}
        {isfef: IsFiniteExpectation prts f}
        {isfefg:IsFiniteExpectation prts (rvmult g f)} :
     almostR2 prts eq (FiniteConditionalExpectation f) (const 0) ->
    FiniteExpectation prts (rvmult g f) = 0.
  
  Lemma SimpleCondexp_factor_out_zero
        (f g : Ts -> R)
        {rvf : RandomVariable dom borel_sa f}
        {rvg : RandomVariable dom2 borel_sa g}
        {rvgf : RandomVariable dom borel_sa (rvmult g f)}
        {frf : FiniteRangeFunction f}
        {frg : FiniteRangeFunction g} :
     almostR2 prts eq (ConditionalExpectation prts sub f) (const 0) ->
    SimpleExpectation (rvmult g f) = 0.

  Lemma IsLp_almost_bounded n rv_X1 rv_X2
        (rle:almostR2 prts Rle (rvpower (rvabs rv_X1) (const n)) rv_X2)
        {rv1:RandomVariable dom borel_sa (rvpower (rvabs rv_X1) (const n))}
        {rv2:RandomVariable dom borel_sa rv_X2}
        {islp:IsFiniteExpectation prts rv_X2}
    :
      IsLp prts n rv_X1.

  Instance FiniteCondexp_Lp_sub {p} (pbig:1<=p)
        (f : Ts -> R)
        {frv : RandomVariable dom borel_sa f}
        {isfe: IsFiniteExpectation prts f}
        {isl : IsLp prts p f} :
    IsLp prts p (FiniteConditionalExpectation f).
  
  Instance FiniteCondexp_Lp {p} (pbig:1<=p)
        (f : Ts -> R)
        {frv : RandomVariable dom borel_sa f}
        {isfe: IsFiniteExpectation prts f}
        {isl : IsLp prts p f} :
    IsLp (prob_space_sa_sub prts sub) p (FiniteConditionalExpectation f).

  Lemma FiniteCondexp_Lp_contractive {p} (pbig:1<=p)
        (f : Ts -> R)
        {frv : RandomVariable dom borel_sa f}
        {isfe: IsFiniteExpectation prts f}
        {isl : IsLp prts p f} :
    FiniteExpectation (prob_space_sa_sub prts sub) (rvpower (rvabs (FiniteConditionalExpectation f)) (const p)) (isfe:=FiniteCondexp_Lp pbig f) <=
    FiniteExpectation prts (rvpower (rvabs f) (const p)).

  Lemma FiniteCondexp_Lp_norm_contractive {p} (pbig:1<=p)
        (f : Ts -> R)
        {frv : RandomVariable dom borel_sa f}
        {isfe: IsFiniteExpectation prts f}
        {isl : IsLp prts p f} :
    power (FiniteExpectation (prob_space_sa_sub prts sub) (rvpower (rvabs (FiniteConditionalExpectation f)) (const p)) (isfe:=FiniteCondexp_Lp pbig f)) (/ p) <=
    power (FiniteExpectation prts (rvpower (rvabs f) (const p))) (/ p).

  Lemma FiniteCondexp_L2_inner
        (f : Ts -> R)
        {frv : RandomVariable dom borel_sa f}
        {fisl : IsLp prts 2 f}
        (w : Ts -> R)
        {wrv:RandomVariable dom2 borel_sa w}
        {wisl:IsLp prts 2 w} :
    Expectation (rvmult (FiniteConditionalExpectation f) w) =
    Expectation (rvmult f w).

  Lemma FiniteCondexp_L2_proj
        (f : Ts -> R)
        {frv : RandomVariable dom borel_sa f}
        {fisl : IsLp prts 2 f}
        (w : Ts -> R)
        {wrv:RandomVariable dom2 borel_sa w}
        {wisl:IsLp prts 2 w} :
    Expectation (rvmult w (rvminus f (FiniteConditionalExpectation f))) = Some (Finite 0).

  Instance FiniteCondexp_L2_min_dist_isfe
        (f : Ts -> R)
        {rv : RandomVariable dom borel_sa f}
        {isl : IsLp prts 2 f} :
    IsFiniteExpectation prts (rvsqr (rvminus f (FiniteConditionalExpectation f))).

  Lemma FiniteCondexp_L2_min_dist
        (f : Ts -> R)
        {rv : RandomVariable dom borel_sa f}
        {isl : IsLp prts 2 f} :
    Finite (power
      (FiniteExpectation prts (rvsqr (rvminus f (FiniteConditionalExpectation f))))
      (/ 2))
    =
     (Glb_Rbar
      (fun r : R =>
         exists w : Ts -> R,
           RandomVariable dom2 borel_sa w /\ IsLp prts 2 w /\
           Some (Finite r) = lift (fun x => Rbar_power x (/ 2)) (Expectation (rvsqr (rvminus f w))))).

  Lemma Glb_Rbar_pos (rset : R -> Prop) :
    (forall (r:R), rset r -> 0 <= r) ->
    Rbar_le 0 (Glb_Rbar rset).

  Lemma finite_Glb_Rbar_pos (rset : R -> Prop) :
    (forall (r:R), rset r -> 0 <= r) ->
    (exists (r1 : R), rset r1) ->
    is_finite (Glb_Rbar rset).


  Lemma glb_sqrt (rset : R -> Prop) :
    (forall (r:R), rset r -> 0 <= r) ->
    (exists (r1 : R), rset r1) ->
    (Finite (sqrt (Glb_Rbar rset))) =
    Glb_Rbar (fun r => exists r0, rset r0 /\ r = sqrt r0).

  Lemma glb_power_half (rset : R -> Prop) :
    (forall (r:R), rset r -> 0 <= r) ->
    (exists (r1 : R), rset r1) ->
    (Rbar_power (Glb_Rbar rset) (/2)) =
    Glb_Rbar (fun r => exists r0, rset r0 /\ r = power r0 (/2)).

    Lemma FiniteCondexp_L2_min_dist_alt
        (f : Ts -> R)
        {rv : RandomVariable dom borel_sa f}
        {isl : IsLp prts 2 f} :
    Finite (FiniteExpectation prts (rvsqr (rvminus f (FiniteConditionalExpectation f))))
    =
     (Glb_Rbar
      (fun r : R =>
         exists w : Ts -> R,
           RandomVariable dom2 borel_sa w /\ IsLp prts 2 w /\
           Some (Finite r) = lift (fun x => x) (Expectation (rvsqr (rvminus f w))))).

    Lemma FiniteCondexp_monotone_convergence
        (f : Ts -> R)
        (fn : nat -> Ts -> R)
        {rvf : RandomVariable dom borel_sa f}
        {rvfn : forall n, RandomVariable dom borel_sa (fn n)}
        {isfef:IsFiniteExpectation prts f}
        {isfefn:forall n, IsFiniteExpectation prts (fn n)}
        (nnf: almostR2 prts Rle (const 0) f)
        (nnfn : forall n, almostR2 prts Rle (const 0) (fn n))
        (fbound:forall (n:nat), almostR2 prts Rle (fn n) f)
        (fincr:forall (n:nat), almostR2 prts Rle (fn n) (fn (S n)))
        (flim:almost prts (fun omega => is_Elim_seq (fun n => fn n omega) (f omega))) :
    almost (prob_space_sa_sub prts sub)
           (fun omega => is_Elim_seq (fun n => FiniteConditionalExpectation (fn n) omega) (FiniteConditionalExpectation f omega)).

End fin_cond_exp.

Section fin_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).

  Lemma FiniteCondexp_tower'
        (f: Ts -> R)
        {rvf : RandomVariable dom borel_sa f}
        {isfe: IsFiniteExpectation prts f}
        {rv:RandomVariable dom borel_sa (FiniteConditionalExpectation prts sub f)}
    :
      almostR2 (prob_space_sa_sub prts (transitivity sub2 sub))
               eq
               (FiniteConditionalExpectation
                  prts
                  (transitivity sub2 sub)
                  (FiniteConditionalExpectation prts sub f))
               (FiniteConditionalExpectation prts (transitivity sub2 sub) f).

  Theorem FiniteCondexp_tower
        (f: Ts -> R)
        {rvf : RandomVariable dom borel_sa f}
        {isfe: IsFiniteExpectation prts f}
    :
      almostR2 (prob_space_sa_sub prts (transitivity sub2 sub))
               eq
               (FiniteConditionalExpectation
                  prts
                  (transitivity sub2 sub)
                  (rv:=RandomVariable_sa_sub sub _ (rv_x:=FiniteCondexp_rv prts sub f))
                  (FiniteConditionalExpectation prts sub f))
               (FiniteConditionalExpectation prts (transitivity sub2 sub) f).

End fin_cond_exp_props.

Section lp_cond_exp.
  
    Context {Ts:Type}
          {dom: SigmaAlgebra Ts}
          (prts: ProbSpace dom)
          {dom2 : SigmaAlgebra Ts}
          (sub : sa_sub dom2 dom)
          {p} (pbig:1<=p).

    Lemma dec_event_sa_sub {P:event dom2}
          (dec:dec_event P) : dec_event (event_sa_sub sub P).

    Lemma EventIndicator_sa_sub {P:event dom2}
          (dec:dec_event P) :
      rv_eq (EventIndicator (dec_event_sa_sub dec)) (EventIndicator dec).

    Definition LpRRVcondexp (f:LpRRV prts p) : LpRRV (prob_space_sa_sub prts sub) p
      := pack_LpRRV (prob_space_sa_sub prts sub) (FiniteConditionalExpectation
                            prts sub f
                            (rv:=LpRRV_rv _ f)
                            (isfe:=IsLp_Finite prts p f pbig
                                               (rrv:=LpRRV_rv _ _)
                                               (lp:=LpRRV_lp _ _)
                                                  ))
                     (rv:=(FiniteCondexp_rv prts sub f))
                     (lp:=FiniteCondexp_Lp prts sub pbig f).

    Global Instance LpRRV_condexp_sproper : Proper (LpRRV_seq ==> LpRRV_seq) LpRRVcondexp.

    Global Instance LpRRV_condexp_proper :
      Proper (LpRRV_eq prts ==>
                       LpRRV_eq (prob_space_sa_sub prts sub)) LpRRVcondexp.

    Theorem LpRRV_condexp_event (f : LpRRV prts p)
        {P:event dom2}
        (dec:dec_event P) :
      Expectation (LpRRVindicator prts pbig (dec_event_sa_sub dec) f) =
      Expectation (LpRRVindicator (prob_space_sa_sub prts sub) pbig dec (LpRRVcondexp f)).

    Corollary LpRRV_condexp_event_classic (f : LpRRV prts p) (P:event dom2) :
      Expectation (LpRRVindicator prts pbig (dec_event_sa_sub (classic_dec P)) f) =
      Expectation (LpRRVindicator (prob_space_sa_sub prts sub) pbig (classic_dec P) (LpRRVcondexp f)).

    Global Instance LpRRV_condexp_nneg (f : LpRRV prts p)
         {nnf : NonnegativeFunction f} :
    NonnegativeFunction (LpRRVcondexp f).

  Lemma LpRRV_condexp_id
         (f : LpRRV prts p)
         {rv2 : RandomVariable dom2 borel_sa f} :
    LpRRV_seq (LpRRVcondexp f) (LpRRV_sa_sub_f prts sub p f).

  Lemma LpRRV_condexp_id'
         (f : LpRRV (prob_space_sa_sub prts sub) p) :
    LpRRV_seq (LpRRVcondexp (LpRRV_sa_sub _ _ _ f)) f.

  Corollary LpRRV_condexp_const c :
    LpRRV_seq (LpRRVcondexp (LpRRVconst _ c)) (LpRRVconst _ c).

  Theorem LpRRV_condexp_Expectation (f : LpRRV prts p)
    :
      Expectation (LpRRVcondexp f) =
      Expectation f.

  Lemma LpRRV_condexp_ale (f1 f2:LpRRV prts p):
    almostR2 prts Rle f1 f2 ->
    almostR2 (prob_space_sa_sub prts sub) Rle
             (LpRRVcondexp f1)
             (LpRRVcondexp f2).

  Lemma LpRRV_condexp_scale c (f : LpRRV prts p) :
    LpRRV_eq (prob_space_sa_sub prts sub)
             (LpRRVcondexp (LpRRVscale _ c f))
             (LpRRVscale _ c (LpRRVcondexp f)).

  Lemma LpRRV_condexp_opp (f : LpRRV prts p) :
    LpRRV_eq (prob_space_sa_sub prts sub)
             (LpRRVcondexp (LpRRVopp _ f))
             (LpRRVopp _ (LpRRVcondexp f)).

  Lemma LpRRV_condexp_plus (f1 f2 : LpRRV prts p) :
    LpRRV_eq (prob_space_sa_sub prts sub)
             (LpRRVcondexp (LpRRVplus _ f1 f2 (p:=bignneg _ pbig)))
             (LpRRVplus _ (LpRRVcondexp f1) (LpRRVcondexp f2) (p:=bignneg _ pbig)).

  Lemma LpRRV_condexp_minus (f1 f2 : LpRRV prts p) :
    LpRRV_eq (prob_space_sa_sub prts sub)
             (LpRRVcondexp (LpRRVminus _ f1 f2 (p:=bignneg _ pbig)))
             (LpRRVminus _ (LpRRVcondexp f1) (LpRRVcondexp f2) (p:=bignneg _ pbig)).

  Lemma LpRRV_condexp_Jensen (f : LpRRV prts p) (phi : R -> R)
        {rvphi : RandomVariable dom borel_sa (fun x => phi (f x))}
        {isfephi : IsLp prts p (fun x => phi (f x))} :
    (forall c x y, convex phi c x y) ->
    almostR2 (prob_space_sa_sub prts sub) Rle
      (fun x => phi ((LpRRVcondexp f) x))
      (LpRRVcondexp (pack_LpRRV _ (fun x => phi (f x)))).

  Theorem LpRRV_condexp_factor_out
          (f : LpRRV prts p)
          (g : LpRRV (prob_space_sa_sub prts sub) p)
          {rvfg:RandomVariable dom borel_sa (rvmult f g)}
        {isfef: IsFiniteExpectation prts f}
        {isfefg:IsLp prts p (rvmult f g)} :
    almostR2 (prob_space_sa_sub prts sub) eq
             (LpRRVcondexp (pack_LpRRV _ (rvmult f g)))
             (rvmult g (LpRRVcondexp f)).

  Lemma LpRRV_condexp_contract (f:LpRRV prts p) :
    LpRRVnorm (prob_space_sa_sub prts sub) (LpRRVcondexp f) <= LpRRVnorm prts f.

End lp_cond_exp.

Section condexp.
  Lemma is_condexp_expectation_sa_sub_proper {Ts:Type}
          {dom: SigmaAlgebra Ts}
          (prts: ProbSpace dom)
          {dom2 dom2' : SigmaAlgebra Ts}
          (sub : sa_sub dom2 dom)
          (sub' : sa_sub dom2' dom)
          (sub_sub:sa_sub dom2' dom2)
          (f : Ts -> R)
          {rvf : RandomVariable dom borel_sa f}
          (ce : Ts -> Rbar)
          {rvce : RandomVariable dom2 Rbar_borel_sa ce}
          {rvce' : RandomVariable dom2' Rbar_borel_sa ce} :
    is_conditional_expectation prts dom2 f ce ->
    is_conditional_expectation prts dom2' f ce.

  Lemma NonNegCondexp_sa_proper {Ts:Type}
        {dom: SigmaAlgebra Ts}
        (prts: ProbSpace dom)
        {dom2 dom2' : SigmaAlgebra Ts}
        (sub : sa_sub dom2 dom)
        (sub' : sa_sub dom2' dom)
        (sub_equiv:sa_equiv dom2 dom2')
        (f : Ts -> R)
        {rv : RandomVariable dom borel_sa f}
        {nnf:NonnegativeFunction f} :
    almostR2 (prob_space_sa_sub prts sub) eq
             (NonNegCondexp prts sub f)
             (NonNegCondexp prts sub' f).

  Lemma Condexp_sa_proper {Ts:Type}
        {dom: SigmaAlgebra Ts}
        (prts: ProbSpace dom)
        {dom2 dom2' : SigmaAlgebra Ts}
        (sub : sa_sub dom2 dom)
        (sub' : sa_sub dom2' dom)
        (sub_equiv:sa_equiv dom2 dom2')
        (f : Ts -> R)
        {rvf : RandomVariable dom borel_sa f} :
    almostR2 (prob_space_sa_sub prts sub) eq
             (ConditionalExpectation prts sub f)
             (ConditionalExpectation prts sub' f).

  Lemma Condexp_all_proper {Ts:Type}
        {dom: SigmaAlgebra Ts}
        (prts: ProbSpace dom)
        {dom2 dom2' : SigmaAlgebra Ts}
        (sub : sa_sub dom2 dom)
        (sub' : sa_sub dom2' dom)
        (sub_equiv:sa_equiv dom2 dom2')
        (f1 f2 : Ts -> R)
        {rvf1 : RandomVariable dom borel_sa f1}
        {rvf2 : RandomVariable dom borel_sa f2} :
      almostR2 prts eq f1 f2 ->
    almostR2 (prob_space_sa_sub prts sub) eq
             (ConditionalExpectation prts sub f1)
             (ConditionalExpectation prts sub' f2).

  Lemma FiniteCondexp_all_proper {Ts:Type}
          {dom: SigmaAlgebra Ts}
          (prts: ProbSpace dom)
          {dom2 dom2' : SigmaAlgebra Ts}
          (sub : sa_sub dom2 dom)
          (sub' : sa_sub dom2' dom)
          (sub_equiv:sa_equiv dom2 dom2')
          (f1 f2 : Ts -> R)
          {rv1 : RandomVariable dom borel_sa f1}
          {rv2 : RandomVariable dom borel_sa f2}
          {isfe1:IsFiniteExpectation prts f1}
          {isfe2:IsFiniteExpectation prts f2} :
    almostR2 prts eq f1 f2 ->
    almostR2 (prob_space_sa_sub prts sub) eq
             (FiniteConditionalExpectation prts sub f1)
             (FiniteConditionalExpectation prts sub' f2).

End condexp.