Module mathcomp.analysis.probability_theory.independence

From HB Require Import structures.
From mathcomp Require Import boot order interval_inference.
From mathcomp Require Import ssralg poly ssrnum ssrint interval finmap.
From mathcomp Require Import boolp classical_sets functions cardinality fsbigop.
From mathcomp Require Import reals.
From mathcomp Require Import ereal topology normedtype sequences.
From mathcomp Require Import exp numfun lebesgue_measure lebesgue_integral.
From mathcomp Require Import esum measure exp numfun lebesgue_measure.
From mathcomp Require Import measurable_realfun lebesgue_integral kernel.
From mathcomp Require Import hoelder random_variable.


Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Import Order.TTheory GRing.Theory Num.Def Num.Theory.
Import numFieldTopology.Exports.

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

Section independent_events.
Context {

RSource code

: realType}

dSource code

{

TSource code

: measurableType d} (

PSource code

: probability T R)
  {

I0Source code

: choiceType}.
Local Open Scope ereal_scope.

Definition

independent_events

---

Source code

 (

ISource code

: set I0) (

ESource code

: I0 -> set T) :=
  forall

JSource code

: {fset I0}, [set` J] `<=` I ->
    P (\bigcap_(

iSource code

in [set` J]) E i) = \prod_(

iSource code

<- J) P (E i).

End independent_events.

Section mutual_independence.
Context {

RSource code

: realType}

dSource code

{

TSource code

: measurableType d} (

PSource code

: probability T R)
  {

I0Source code

: choiceType}.
Local Open Scope ereal_scope.

Definition

mutual_independence

---

Source code

 (

ISource code

: set I0) (

FSource code

: I0 -> set_system T) :=
  forall

JSource code

: {fset I0}, [set` J] `<=` I ->
    forall

ESource code

, (forall

iSource code

, i \in J -> E i \in F i) ->
      P (\big[setI/setT]_(

jSource code

<- J) E j) = \prod_(

jSource code

<- J) P (E j).

Lemma

eq_mutual_independenceSource code

 (

ISource code

: set I0) (

FSource code

F'Source code

: I0 -> set_system T) :
  (forall

iSource code

, I i -> F i = F' i) ->
  mutual_independence I F -> mutual_independence I F'.

Proof.

move=> FF' + J JI E EF'; apply => // i iJ.
by rewrite FF' ?EF'//; exact: JI.
Qed.

End mutual_independence.

Section independence.
Context {

RSource code

: realType}

dSource code

{

TSource code

: measurableType d} (

PSource code

: probability T R).
Local Open Scope ereal_scope.

Definition

independence2

---

Source code

 (

FSource code

GSource code

: set_system T) :=
  forall

ASource code

BSource code

, A \in F -> B \in G -> P (A `&` B) = P A * P B.

Lemma

independence2PSource code

 (

FSource code

GSource code

: set_system T) : independence2 F G <->
  mutual_independence P [set: bool] (fun

bSource code

=> if b then F else G).

Proof.

split=> indeF.
  move=> J Jbool E EF.
  have [/eqP Jtrue|/eqP Jfalse| |] := set_bool [set` J].
  - by rewrite -bigcap_fset Jtrue bigcap_set1 fsbig_seq ?Jtrue ?fsbig_set1.
  - by rewrite -bigcap_fset Jfalse bigcap_set1 fsbig_seq// ?Jfalse fsbig_set1.
  - by rewrite set_seq_eq0 => /eqP ->; rewrite !big_nil probability_setT.
  - rewrite setT_bool => /eqP {}Jbool.
    rewrite -bigcap_fset Jbool bigcap_setU1 bigcap_set1.
    rewrite indeF.
    + by rewrite EF// -(set_fsetK J) Jbool in_fset_set// !inE/=; left.
    + by rewrite EF// -(set_fsetK J) Jbool in_fset_set// !inE/=; right.
    + rewrite -(set_fsetK J) Jbool fset_setU1//= fset_set1 big_fsetU1 ?inE//=.
      by rewrite big_seq_fset1.
move=> A B AF BG.
move: indeF => /(_ [fset true; false]%fset _ (fun

bSource code

=> if b then A else B)).
do 2 rewrite big_fsetU1/= ?inE//= big_seq_fset1.
by apply => // -[].
Qed.

End independence.

Section mutual_independence_properties.
Context {

RSource code

: realType}

dSource code

{

TSource code

: measurableType d} (

PSource code

: probability T R).
Local Open Scope ereal_scope.

Lemma

mutual_independence_fsetSource code

{

I0Source code

: choiceType} (

ISource code

: {fset I0})
    (

FSource code

: I0 -> set_system T) :
  (forall

iSource code

, i \in I -> (F i) [set: T]) ->
  mutual_independence P [set` I] F <->
  forall

ESource code

, (forall

iSource code

, i \in I -> E i \in F i) ->
      P (\big[setI/setT]_(

jSource code

<- I) E j) = \prod_(

jSource code

<- I) P (E j).

Proof.

move=> mF; split=> [indeF E EF|indeF]; first exact: indeF.
move=> J JI E EF.
pose E'

iSource code

:= if i \in J then E i else [set: T].
have /indeF : forall

iSource code

, i \in I -> E' i \in F i.
  move=> i iI; rewrite /E'; case: ifPn => [|iJ]; first exact: EF.
  by rewrite inE; apply mF.
move/fsubsetP : (JI) => /(big_fset_incl _) <- /=.
  by move=> j jI jJ; rewrite /E' (negbTE jJ).
move/fsubsetP : (JI) => /(big_fset_incl _) <- /=.
  by move=> j jI jJ; rewrite /E' (negbTE jJ); rewrite probability_setT.
rewrite big_seq [in X in X = _ -> _](eq_bigr E).
  by move=> i iJ; rewrite /E' iJ.
rewrite -big_seq => ->.
by rewrite !big_seq; apply: eq_bigr => i iJ; rewrite /E' iJ.
Qed.

Lemma

mutual_independence_finiteSSource code

{

I0Source code

: choiceType} (

ISource code

: set I0)
    (

FSource code

: I0 -> set_system T) :
  mutual_independence P I F <->
  (forall

JSource code

: {fset I0}%fset, [set` J] `<=` I ->
    mutual_independence P [set` J] F).

Proof.

split=> [indeF J JI K KJ E EF|indeF]; first by apply: indeF => // i /KJ /JI.
by move=> J JI E EF; exact: (indeF _ JI).
Qed.

Theorem

mutual_independence_finite_g_sigmaSource code

{

I0Source code

: choiceType} (

ISource code

: set I0)
    (

FSource code

: I0 -> set_system T) :
  (forall

iSource code

, i \in I -> F i `<=` d.-measurable) ->
  (forall

iSource code

, i \in I -> setI_closed (F i `|` [set set0])) ->
  mutual_independence P I F <-> mutual_independence P I (fun

iSource code

=> <<s F i>>).

Proof.

move=> mF IF0; split=> indeF; last first.
  move=> J JI E EF; apply: indeF => // i iJ; rewrite inE.
  by apply: sub_gen_smallest; exact/set_mem/EF.
move=> K KI E EF.
suff: forall

JSource code

J'Source code

: {fset I0}%fset, (J `<=` J')%fset -> [set` J'] `<=` I ->
  forall

ESource code

, (forall

iSource code

, i \in J -> E i \in <<s F i >>) ->
            (forall

iSource code

, i \in [set` J'] `\` [set` J] -> E i \in F i) ->
    P (\big[setI/setT]_(

jSource code

<- J') E j) = \prod_(

jSource code

<- J') P (E j).
  move=> /(_ K K (@fsubset_refl _ _) KI E); apply.
  - by move=> i iK; exact: EF.
  - by move=> i; rewrite setDv inE.
move=> {E EF K KI}.
apply: finSet_rect => K ih J' KJ' J'I E EsF EF.
have [K0|/fset0Pn[j jK]] := eqVneq K fset0.
  apply indeF => // i iJ'.
  by apply: EF; rewrite !inE; split => //=; rewrite K0 inE.
pose J := (K `\ j)%fset.
have jI : j \in I by apply/mem_set/J'I => /=; move/fsubsetP : KJ'; exact.
have JK : (J `<` K)%fset by rewrite fproperD1.
have JjJ' : (j |` J `<=` J')%fset by apply: fsubset_trans KJ'; rewrite fsetD1K.
have JJ' : (J `<=` J')%fset by apply: fsubset_trans JjJ'; exact: fsubsetU1.
have J'mE i : i \in J' -> d.-measurable (E i).
  move=> iJ'.
  suff: <<s F i>> (E i).
    apply: smallest_sub => //.
      exact: sigma_algebra_measurable.
    apply: mF.
    by apply/mem_set/J'I => /=.
  have [iK|iK] := boolP (i \in K).
    by apply/set_mem; rewrite EsF.
  have /set_mem : E i \in F i.
    by rewrite EF// !inE/=; split => //; exact/negP.
  by move/sub_sigma_algebra => /(_ setT).
have mmu : measurable (\big[setI/[set: T]]_(

j0Source code

<- (J' `\ j)%fset) (E j0)).
  rewrite big_seq; apply: bigsetI_measurable => i /[!inE] /andP[_ iJ'].
  exact: J'mE.
pose mu0

ASource code

:= P (A `&` \big[setI/[set: T]]_(

j0Source code

<- (J' `\ j)%fset) (E j0)).
pose mu := [the {finite_measure set _ -> \bar _} of mrestr P mmu].
pose nu0

ASource code

:= P A * \prod_(

j0Source code

<- (J' `\ j)%fset) P (E j0).
have nuk : (0 <= fine (\prod_(

j0Source code

<- (J' `\ j)%fset) P (E j0)))%R.
  by rewrite fine_ge0// prode_ge0.
pose nu := [the measure _ _ of mscale (NngNum nuk) P].
have nuEj A : nu A = P A * \prod_(

j0Source code

<- (J' `\ j)%fset) P (E j0).
  rewrite /nu/= /mscale muleC/= fineK// big_seq.
  rewrite prode_fin_num// => i /[!inE]/= /andP[ij iJ'].
  by rewrite fin_num_measure//; exact: J'mE.
have JJ'j : (J `<=` J' `\ j)%fset by exact: fsetSD.
have J'jI : [set` (J' `\ j)%fset] `<=` I.
  by apply: subset_trans J'I; apply/fsubsetP; exact: fsubsetDl.
have jJ' : j \in J' by move/fsubsetP : JjJ'; apply; rewrite !inE eqxx.
have Fjmunu A : (F j `|` [set set0; setT]) A -> mu A = nu A.
  move=> [FjA|[->|->]].
  - rewrite nuEj.
    pose E'

iSource code

:= if i == j then A else E i.
    transitivity (P (\big[setI/[set: T]]_(

jSource code

<- J') E' j)).
      rewrite [in RHS](big_fsetD1 j)//= {1}/E' eqxx//; congr (P (_ `&` _)).
      rewrite !big_seq; apply: eq_bigr => i /[!inE] /andP[ij _].
      by rewrite /E' (negbTE ij).
    transitivity (\prod_(

jSource code

<- J') P (E' j)); last first.
      rewrite [in LHS](big_fsetD1 j)//= {1}/E' eqxx//; congr (P _ * _).
      rewrite !big_seq; apply: eq_bigr => i /[!inE] /andP[ij _].
      by rewrite /E' (negbTE ij).
    apply: (ih _ JK _ JJ' J'I).
    + move=> i iJ.
      rewrite /E'; case: ifPn => [/eqP ->|ij].
        by rewrite inE; exact: sub_sigma_algebra.
      rewrite EsF//.
      by move/fproper_sub : JK => /fsubsetP; apply.
    + move=> i.
      rewrite ![in X in X -> _]inE /= ![in X in X -> _]inE => -[] iJ' /negP.
      rewrite negb_and negbK => /predU1P[ij|iK].
        by rewrite /E' ij eqxx inE.
      rewrite /E' ifF//.
        apply/negP => /eqP ij.
        by rewrite ij jK in iK.
      by rewrite EF// !inE/=; split => //; exact/negP.
  - by rewrite !measure0.
  - rewrite /mu /= /mrestr /= nuEj setTI probability_setT mul1e.
    apply: (ih _ JK _ JJ'j J'jI).
    + move=> i iJ.
      rewrite EsF//.
      by move/fproper_sub : JK => /fsubsetP; apply.
    + move=> i.
      rewrite ![in X in X -> _]inE /= ![in X in X -> _]inE => -[].
      move=> /andP[-> iJ'] iK.
      by rewrite EF// !inE.
have sFjmunu A : <<s F j >> A -> mu A = nu A.
  move=> sFjA.
  apply: (@g_sigma_algebra_finite_measure_unique _ _ _ (F j `|` [set set0])).
  - move=> B /= [|->//].
    move: B.
    exact: mF.
  - exact: IF0.
  - rewrite /mu/= /mrestr/= nuEj setTI probability_setT mul1e.
    apply: (ih _ JK _ JJ'j J'jI).
    + move=> i iJ.
      rewrite EsF//.
      by move/fproper_sub : JK => /fsubsetP; apply.
    + move=> i.
      rewrite ![in X in X -> _]inE /= ![in X in X -> _]inE => -[].
      move=> /andP[ij iJ'].
      rewrite ij/= => iK.
      by rewrite EF// !inE.
  - move=> B FjB; apply: Fjmunu.
    case: FjB => [|->//]; first by left.
    by right; left.
  - by move: sFjA; exact: sub_smallest2r.
rewrite [in LHS](big_fsetD1 j)//= [in RHS](big_fsetD1 j)//=.
have /sFjmunu : <<s F j >> (E j) by apply/set_mem; rewrite EsF.
by rewrite /mu/= /mrestr/= nuEj.
Qed.

#[local] Definition

f

---

Source code

 (

K0Source code

: choiceType) (

KSource code

: {fset K0})
  (

I0Source code

: pointedType) (

FSource code

: I0 -> set_system T)

ESource code

I_Source code

  (

EFSource code

: forall

kSource code

, k \in K -> E k \in \bigcup_(

iSource code

in I_ k) F i)

kSource code

:=
  if pselect (k \in K) is left kK then
     sval (cid2 (set_mem (EF _ kK)))
   else
     point.

#[local] Lemma

f_propSource code

 (

K0Source code

: choiceType) (

KSource code

: {fset K0})
    (

I0Source code

: pointedType) (

FSource code

: I0 -> set_system T)

ESource code

I_Source code

    (

EFSource code

: forall

kSource code

, k \in K -> E k \in \bigcup_(

iSource code

in I_ k) F i)

kSource code

:
  k \in K -> E k \in F (f EF k).

Proof.

move=> kK; rewrite /f; case: pselect => [kK_/=|//].
by case: cid2 => // i/= ? /mem_set.
Qed.

#[local] Lemma

f_injSource code

 (

K0Source code

: choiceType) (

KSource code

K'Source code

: {fset K0})
  (

K'KSource code

: [set` K'] `<=` [set` K]) (

I0Source code

: pointedType) (

FSource code

: I0 -> set_system T)
  

ESource code

I_Source code

 (

EFSource code

: forall

kSource code

, k \in K' -> E k \in \bigcup_(

iSource code

in I_ k) F i)
  (

KISource code

: trivIset [set` K] I_)

k1Source code

k2Source code

:
  k1 \in K' -> k2 \in K'-> k1 != k2 ->
  ([fset f EF k1] `&` [fset f EF k2] = fset0)%fset.

Proof.

move=> k1K' k2K' k1k2; apply/eqP; rewrite -fsubset0.
apply/fsubsetP => i /[!inE] /andP[].
rewrite /f; case: pselect => // k1K'_.
case: cid2 => // i' i'k1 Fi' /eqP ->{i}.
case: pselect => // k2K'_.
case: cid2 => // j ik2 FjEk2 /eqP/= i'j.
rewrite -{j}i'j in ik2 FjEk2 *.
move/trivIsetP : KI => /(_ _ _ (K'K _ k1K') (K'K _ k2K') k1k2).
by move/seteqP => [+ _] => /(_ i')/=; rewrite -falseE; exact.
Qed.

#[local] Definition

g

---

Source code

 (

K0Source code

: pointedType) (

K'Source code

: {fset K0})
    (

I0Source code

: Type) (

I_Source code

: K0 -> set I0) (

iSource code

: I0) : K0 :=
  if pselect (exists2

kSource code

, k \in K' & i \in I_ k) is left e then
    sval (cid2 e)
  else
    point.

#[local] Lemma

gfSource code

 (

K0Source code

I0Source code

: pointedType) (

FSource code

: I0 -> set_system T)
  (

KSource code

K'Source code

: {fset K0}) (

K'KSource code

: [set` K'] `<=` [set` K])
  

ESource code

I_Source code

 (

EFSource code

: forall

kSource code

, k \in K' -> E k \in \bigcup_(

iSource code

in I_ k) F i)
  (

KISource code

: trivIset [set` K] (fun

iSource code

=> I_ i))

iSource code

: i \in K' -> g K I_ (f EF i) = i.

Proof.

move=> iK'; rewrite /f; case: pselect => // iK'_.
case: cid2 => // j jIi FjEi.
rewrite /g; case: pselect => // k'; last first.
  exfalso; apply: k'.
  by exists i => //; [exact: K'K|exact/mem_set].
case: cid2 => //= k'' k''K jIk'.
apply/eqP/negP => /negP k'i.
move/trivIsetP : KI => /(_ k'' i) /= /(_ k''K (K'K _ iK') k'i)/= /eqP.
apply/negP/set0P; exists j; split => //.
exact/set_mem.
Qed.

Lemma

mutual_independence_bigcupSource code

 (

K0Source code

I0Source code

: pointedType) (

KSource code

: {fset K0})
    (

I_Source code

: K0 -> set I0) (

ISource code

: set I0) (

FSource code

: I0 -> set_system T) :
  trivIset [set` K] (fun

iSource code

=> I_ i) ->
  (forall

kSource code

, k \in K -> I_ k `<=` I) ->
  mutual_independence P I F ->
  mutual_independence P [set` K] (fun

kSource code

=> \bigcup_(

iSource code

in I_ k) F i).

Proof.

move=> KI I_I PIF K' K'K E EF.
pose f' := f EF.
pose g' := g K I_.
pose J' := (\bigcup_(

kSource code

<- K') [fset f' k])%fset.
pose E' := E \o g'.
suff: P (\big[setI/[set: T]]_(

jSource code

<- J') E' j) = \prod_(

jSource code

<- J') P (E' j).
  move=> suf.
  transitivity (P (\big[setI/[set: T]]_(

jSource code

<- J') E' j)).
    congr (P _).
    apply/seteqP; split=> [t|].
      rewrite -!bigcap_fset => L j => /bigfcupP[k] /[!andbT] kK'.
      rewrite !inE => /eqP ->{j}.
      apply: L => //=.
      by rewrite /g' /f' gf.
    move=> t.
    rewrite -!bigcap_fset => L j/= jK'.
    have /= := L (f' j).
    rewrite /E' /g' /f'/= gf//.
    by apply; apply/bigfcupP; exists j;[rewrite jK'|rewrite inE].
  rewrite suf partition_disjoint_bigfcup//=.
    move=> k1 k2 k1K' k2K' k1k2 /=.
    by rewrite -fsetI_eq0 -fsubset0 (f_inj K'K).
  rewrite [LHS]big_seq [RHS]big_seq; apply: eq_big => // k kK'.
  by rewrite big_seq_fset1 /E' /g' /f' /= gf.
apply: PIF.
- move=> i/= /bigfcupP[k] /[!andbT] kK' /[!inE] /eqP ->.
  apply: (I_I k) => /=; first exact: K'K.
  by rewrite /f' /f; case: pselect => // kK'_; case: cid2.
- move=> i /bigfcupP[k'] /[!andbT] k'K /[!inE] /eqP ->{i}.
  by rewrite /E' /g' /f'/= gf//; exact/set_mem/f_prop.
Qed.

End mutual_independence_properties.

Section independent_RVs.
Context {

RSource code

: realType}

dSource code

 (

TSource code

: measurableType d).
Context {

I0Source code

: choiceType}.
Context {

d'Source code

: I0 -> _} (

T'Source code

: forall

iSource code

: I0, measurableType (d' i)).
Variable

PSource code

: probability T R.

Definition

independent_RVs

---

Source code

 (

ISource code

: set I0)
  (

XSource code

: forall

iSource code

: I0, {mfun T >-> T' i}) : Prop :=
  mutual_independence P I (fun

iSource code

=> g_sigma_algebra_preimage (X i)).

End independent_RVs.

Section independent_RVs_properties.
Context {

RSource code

: realType}

dSource code

d'Source code

 (

TSource code

: measurableType d) (

T'Source code

: measurableType d').
Variable

PSource code

: probability T R.

Lemma

independent_RVsD1Source code

 (

ISource code

: {fset nat})

i0Source code

 (

XSource code

: {RV P >-> T'}^nat) :
  independent_RVs P [set` I] X -> independent_RVs P [set` (I `\ i0)%fset] X.

Proof.

move=> PIX; move=> /= J JIi0 E EK.
by apply: PIX => //= x /JIi0 /=; rewrite !inE => /andP[].
Qed.

End independent_RVs_properties.

Section independent_generators.
Context {

RSource code

: realType}

dSource code

 (

TSource code

: measurableType d).
Context {

I0Source code

: choiceType}.
Context {

d'Source code

: I0 -> _} (

T'Source code

: forall

iSource code

: I0, measurableType (d' i)).
Variable

PSource code

: probability T R.

Theorem

independent_generatorsSource code

 (

ISource code

: set I0)
    (

FSource code

: forall

iSource code

: I0, set_system (T' i)) (

XSource code

: forall

iSource code

, {RV P >-> T' i}) :
  (forall

iSource code

, i \in I -> setI_closed (F i)) ->
  (forall

iSource code

, i \in I -> F i `<=` @measurable _ (T' i)) ->
  (forall

iSource code

, i \in I -> @measurable _ (T' i) = <<s F i>>) ->
  mutual_independence P I (fun

iSource code

=> preimage_set_system setT (X i) (F i)) ->
  independent_RVs P I X.

Proof.

move=> IF FA AsF indeX1.
have closed_preimage i : I i ->
    setI_closed (preimage_set_system setT (X i) (F i)).
  move=> Ii A B [A' FiA']; rewrite setTI => <-{A}.
  move=> [B' FiB']; rewrite setTI => <-{B}.
  rewrite /preimage_set_system/=; exists (A' `&` B').
    by apply: IF => //; exact/mem_set.
  by rewrite setTI.
have gen_preimage i : I i ->
    <<s preimage_set_system setT (X i) (F i) >> =
    g_sigma_algebra_preimage (X i).
  move=> Ii.
  rewrite /g_sigma_algebra_preimage AsF; first exact/mem_set.
  by rewrite -g_sigma_preimageE.
rewrite /independent_RVs.
suff: mutual_independence P I
    (fun

iSource code

=> <<s preimage_set_system setT (X i) (F i) >>).
  exact: eq_mutual_independence.
apply: (mutual_independence_finite_g_sigma _ _ _).1 indeX1.
- move=> i iI _ [B FiB <-]; apply: measurable_funPT => //.
  by apply: FA FiB.
- move=> i Ii; apply: setI_closed_set0.
  exact/closed_preimage/set_mem.
Qed.

End independent_generators.

Section independent_RVs2.
Context {

RSource code

: realType} {

dSource code

d'Source code

} {

TSource code

: measurableType d} {

T'Source code

: measurableType d'}
 (

PSource code

: probability T R).

Definition

independent_RVs2

---

Source code

 (

XSource code

YSource code

: {mfun T >-> T'}) :=
  independent_RVs P [set: bool] (fun

bSource code

=> if b then Y else X).

End independent_RVs2.

Section independent_RVs2_properties.
Context {

RSource code

: realType} {

dSource code

d'Source code

} {

TSource code

: measurableType d} {

T'Source code

: measurableType d'}
  (

PSource code

: probability T R).
Local Open Scope ring_scope.

Import MeasurableR.

Lemma

independent_RVs2_compSource code

 (

XSource code

YSource code

: {RV P >-> R}) (

fSource code

gSource code

: {mfun R >-> R}) :
  independent_RVs2 P X Y -> independent_RVs2 P (f \o X) (g \o Y).

Proof.

move=> + J _ E JE; apply => //= i iJ; have := JE _ iJ.
by move: i {iJ} =>[|]//=; rewrite !inE => Eg;
  exact: g_sigma_algebra_preimage_comp Eg.
Qed.

Lemma

independent_RVs2_funrposnegSource code

 (

XSource code

YSource code

: {RV P >-> R}) :
  independent_RVs2 P X Y -> independent_RVs2 P X^\+ Y^\-.

Proof.

move=> + J J2 E JE; apply => //= i iJ; have := JE _ iJ.
move/J2 : iJ; move: i => [|] _; rewrite !inE .
- apply: (g_sigma_algebra_preimage_comp (fun

xSource code

: R => maxr (- x) 0)%R).
  exact: measurable_funrneg.
- apply: (g_sigma_algebra_preimage_comp (fun

xSource code

: R => maxr x 0)%R) => //.
  exact: measurable_funrpos.
Qed.

Lemma

independent_RVs2_funrnegposSource code

 (

XSource code

YSource code

: {RV P >-> R}) :
  independent_RVs2 P X Y -> independent_RVs2 P X^\- Y^\+.

Proof.

move=> + J J2 E JE; apply => //= i iJ; have := JE _ iJ.
move/J2 : iJ; move: i => [|]// _; rewrite !inE.
- apply: (g_sigma_algebra_preimage_comp (fun

xSource code

: R => maxr x 0)%R).
  exact: measurable_funrpos.
- apply: (g_sigma_algebra_preimage_comp (fun

xSource code

: R => maxr (- x) 0)%R).
  exact: measurable_funrneg.
Qed.

Lemma

independent_RVs2_funrnegnegSource code

 (

XSource code

YSource code

: {RV P >-> R}) :
  independent_RVs2 P X Y -> independent_RVs2 P X^\- Y^\-.

Proof.

move=> + J J2 E JE; apply => //= i iJ; have := JE _ iJ.
move/J2 : iJ; move: i => [|]// _; rewrite !inE.
- apply: (g_sigma_algebra_preimage_comp (fun

xSource code

: R => maxr (- x) 0)%R).
  exact: measurable_funrneg.
- apply: (g_sigma_algebra_preimage_comp (fun

xSource code

: R => maxr (- x) 0)%R).
  exact: measurable_funrneg.
Qed.

Lemma

independent_RVs2_funrposposSource code

 (

XSource code

YSource code

: {RV P >-> R}) :
  independent_RVs2 P X Y -> independent_RVs2 P X^\+ Y^\+.

Proof.

move=> + J J2 E JE; apply => //= i iJ; have := JE _ iJ.
move/J2 : iJ; move: i => [|]// _; rewrite !inE.
- apply: (g_sigma_algebra_preimage_comp (fun

xSource code

: R => maxr x 0)%R).
  exact: measurable_funrpos.
- apply: (g_sigma_algebra_preimage_comp (fun

xSource code

: R => maxr x 0)%R).
  exact: measurable_funrpos.
Qed.

End independent_RVs2_properties.

Section pairRV.
Context

dSource code

d'Source code

{

TSource code

: measurableType d} {

T'Source code

: measurableType d'} {

RSource code

: realType}
  (

PSource code

: probability T R).

Definition

pairRV

mutual_independence : forall {R : realType} [d : measure_display] {T : measurableType d}, probability T R -> forall {I0 : choiceType}, set I0 -> (I0 -> set_system T) -> Prop mutual_independence is not universe polymorphic Arguments mutual_independence {R} [d]%_measure_display_scope {T} P {I0} I%_classical_set_scope F%_function_scope mutual_independence is transparent Expands to: Constant mathcomp.analysis.probability_theory.independence.mutual_independence Declared in library mathcomp.analysis.probability_theory.independence, line 57, characters 11-30

---

Source code

 (

XSource code

YSource code

: {RV P >-> T'}) : T * T -> T' * T' :=
  (fun

xSource code

=> (X x.1, Y x.2)).

Let

measurable_pairMSource code

 (

XSource code

YSource code

: {RV P >-> T'}) : measurable_fun setT (pairRV X Y).

Proof.

rewrite /pairRV.
apply/measurable_fun_pairP; split => //=.
- rewrite [X in measurable_fun _ X](_ : _ = X \o fst)//.
  exact/measurableT_comp.
- rewrite [X in measurable_fun _ X](_ : _ = Y \o snd)//.
  exact/measurableT_comp.
Qed.

HBSource code

.

instanceSource code

DefinitionSource code

_Source code

 (

XSource code

YSource code

:Source code

{RVSource code

P >-> T'}) :=
  @isMeasurableFun.Build _ _ _ _ (pairRV X Y) (measurable_pairM X Y).

End pairRV.

Section independent_RVs2_properties_realType.
Context {

RSource code

: realType} {

dSource code

} {

TSource code

: measurableType d} (

PSource code

: probability T R).
Local Open Scope ereal_scope.

Import MeasurableR.

Lemma

independent_RVs2_setI_preimageSource code

 (

XSource code

YSource code

: {mfun T >-> R}) (

A1Source code

A2Source code

: set R) :
  measurable A1 -> measurable A2 ->
  independent_RVs2 P X Y ->
  P (X @^-1` A1 `&` Y @^-1` A2) = P (X @^-1` A1) * P (Y @^-1` A2).

Proof.

move=> mA1 mA2.
rewrite /independent_RVs2 /independent_RVs /mutual_independence /=.
move/(_ [fset false; true]%fset (@subsetT _ _)
  (fun

bSource code

=> if b then Y @^-1` A2 else X @^-1` A1)).
rewrite !big_fsetU1 ?inE//= !big_seq_fset1/=.
apply => -[|] /= _; rewrite !inE; rewrite /g_sigma_algebra_preimage.
by exists A2 => //; rewrite setTI.
by exists A1 => //; rewrite setTI.
Qed.

Lemma

independent_RVs2_product_measure1Source code

 (

XSource code

YSource code

: {RV P >-> R}) (

A1Source code

A2Source code

: set R) :
  measurable A1 -> measurable A2 ->
  independent_RVs2 P X Y ->
  (P \x P) (pairRV X Y @^-1` (A1 `*` A2)) = P (X @^-1` A1 `&` Y @^-1` A2).

Proof.

move=> mA1 mA2 iPXY.
rewrite (_ : (pairRV X Y @^-1` _) = (X @^-1` A1) `*` (Y @^-1` A2)).
  by apply/seteqP; split => [[x1 x2]|[x1 x2]].
rewrite product_measure1E; [exact: measurable_funPTI..|].
by rewrite independent_RVs2_setI_preimage.
Qed.

End independent_RVs2_properties_realType.

Section product_expectation_over_product_measure.
Context {

RSource code

: realType} {

dSource code

} {

TSource code

: measurableType d} (

PSource code

: probability T R).
Local Open Scope ereal_scope.

Import MeasurableR.

Lemma

independent_Lfun1_expectation_product_measure_ltySource code

 (

XSource code

YSource code

: {RV P >-> R}) :
  independent_RVs2 P X Y ->
  (X : _ -> _) \in Lfun P 1 -> (Y : _ -> _) \in Lfun P 1 ->
  'E_((P \x P) : probability (T * T)%type R)
     [(fun

xSource code

=> `|X x.1 * Y x.2|)%R] < +oo.

Proof.

move=> indeXY iX iY.
rewrite unlock [ltLHS](_ : _ =
    \int[distribution (P \x P) (pairRV X Y)%R]_

xSource code

`|x.1 * x.2|%:E).
  rewrite ge0_integral_distribution//=.
  apply/measurable_EFinP => //=.
  by apply/measurableT_comp => //=; exact/measurable_funM.
rewrite [ltLHS](_ : _ =
    \int[distribution P X \x distribution P Y]_

xSource code

`|x.1 * x.2|%:E).
  apply: eq_measure_integral => // A mA _.
  apply/esym. (* NB: don't simpl here! *)
  apply: product_measure_unique => //= A1 A2 mA1 mA2.
  by rewrite independent_RVs2_product_measure1// independent_RVs2_setI_preimage.
rewrite fubini_tonelli1//=.
  apply/measurable_EFinP => /=; apply/measurableT_comp => //=.
  exact/measurable_funM.
rewrite /fubini_F/=.
rewrite [ltLHS](_ : _ = (\int[distribution P X]_

xSource code

`|x|%:E) *
                        \int[distribution P Y]_

ySource code

`|y|%:E).
  rewrite -ge0_integralZr//=.
    exact/measurable_EFinP.
    exact: integral_ge0.
  apply: eq_integral => x _.
  rewrite -ge0_integralZl//=.
    exact/measurable_EFinP.
  by under eq_integral do rewrite normrM.
rewrite ge0_integral_distribution//=; first exact/measurable_EFinP.
rewrite ge0_integral_distribution//=; first exact/measurable_EFinP.
rewrite lte_mul_pinfty//.
- exact: integral_ge0.
- apply: integrable_fin_num => //=.
  by move/Lfun1_integrable : iX => /integrable_abse.
- apply: integrable_lty => //.
  by move/Lfun1_integrable : iY => /integrable_abse.
Qed.

End product_expectation_over_product_measure.

Section expectationM.
Context {

RSource code

: realType} {

dSource code

} {

TSource code

: measurableType d} (

PSource code

: probability T R).
Local Open Scope ereal_scope.

Import HBNNSimple.
Import MeasurableR.

#[local] Lemma

expectationM_nnsfunSource code

 (

fSource code

gSource code

: {nnsfun T >-> R}) :
  (forall

ySource code

y'Source code

, y \in range f -> y' \in range g ->
    P (f @^-1` [set y] `&` g @^-1` [set y']) =
    P (f @^-1` [set y]) * P (g @^-1` [set y'])) ->
  'E_P [f \* g] = 'E_P [f] * 'E_P [g].

Proof.

move=> fg; transitivity
    ('E_P [(fun

xSource code

=> (\sum_(

ySource code

\in range f) y * \1_(f @^-1` [set y]) x)%R)
        \* (fun

xSource code

=> (\sum_(

ySource code

\in range g) y * \1_(g @^-1` [set y]) x)%R)]).
  by congr ('E_P [_]); apply/funext => t/=; rewrite (fimfunE f) (fimfunE g).
transitivity ('E_P [(fun

xSource code

=> (\sum_(

ySource code

\in range f) \sum_(

y'Source code

\in range g) y * y'
                    * \1_(f @^-1` [set y] `&` g @^-1` [set y']) x)%R)]).
  congr ('E_P [_]); apply/funext => t/=.
  rewrite mulr_fsuml; apply: eq_fsbigr => y yf; rewrite mulr_fsumr.
  by apply: eq_fsbigr => y' y'g; rewrite indicI mulrCA !mulrA (mulrC y').
rewrite unlock.
under eq_integral do rewrite -fsumEFin//.
transitivity (\sum_(

ySource code

\in range f) (\sum_(

y'Source code

\in range g)
  ((y * y')%:E * \int[P]_

wSource code

 (\1_(f @^-1` [set y] `&` g @^-1` [set y']) w)%:E))).
  rewrite ge0_integral_fsum//=.
  - move=> r; under eq_fun do rewrite -fsumEFin//.
    apply: emeasurable_fsum => // s.
    apply/measurable_EFinP/measurable_funM => //.
    exact/measurable_indic/measurableI.
  - move=> r t _; rewrite lee_fin sumr_ge0 // => s _; rewrite -lee_fin.
    by rewrite indicI/= indicE -mulrACA EFinM mule_ge0// nnfun_muleindic_ge0.
  apply: eq_fsbigr => y yf.
  under eq_integral do rewrite -fsumEFin//.
  rewrite ge0_integral_fsum//=.
  - move=> r; apply/measurable_EFinP; apply: measurable_funM => //.
    exact/measurable_indic/measurableI.
  - move=> r t _.
    by rewrite indicI/= indicE -mulrACA EFinM mule_ge0// nnfun_muleindic_ge0.
  apply: eq_fsbigr => y' y'g.
  under eq_integral do rewrite EFinM.
  by rewrite integralZl//; exact/integrable_indic/measurableI.
transitivity (\sum_(

ySource code

\in range f) (\sum_(

y'Source code

\in range g)
  ((y * y')%:E * ((\int[P]_

wSource code

 (\1_(f @^-1` [set y]) w)%:E) *
                  \int[P]_

wSource code

 (\1_(g @^-1` [set y']) w)%:E)))).
  apply: eq_fsbigr => y fy; apply: eq_fsbigr => y' gy'; congr *%E.
  transitivity ('E_P[\1_(f @^-1` [set y] `&` g @^-1` [set y'])]).
    by rewrite unlock.
  transitivity ('E_P[\1_(f @^-1` [set y])] * 'E_P[\1_(g @^-1` [set y'])]);
    last by rewrite unlock.
  rewrite expectation_indic//; first exact: measurableI.
  by rewrite !expectation_indic//; exact: fg.
transitivity (
    (\sum_(

ySource code

\in range f) (y%:E * (\int[P]_

wSource code

 (\1_(f @^-1` [set y]) w)%:E))) *
    (\sum_(

y'Source code

\in range g) (y'%:E * \int[P]_

wSource code

 (\1_(g @^-1` [set y']) w)%:E))).
  transitivity (\sum_(

ySource code

\in range f) (\sum_(

y'Source code

\in range g)
      (y'%:E * \int[P]_

wSource code

 (\1_(g @^-1` [set y']) w)%:E)) *
        (y%:E * \int[P]_

wSource code

 (\1_(f @^-1` [set y]) w)%:E)); last first.
    rewrite !fsbig_finite//= ge0_sume_distrl//.
      move=> r _; rewrite -integralZl//; first exact: integrable_indic.
      by apply: integral_ge0 => t _; rewrite nnfun_muleindic_ge0.
    by apply: eq_bigr => r _; rewrite muleC.
  apply: eq_fsbigr => y fy.
  rewrite !fsbig_finite//= ge0_sume_distrl//.
    move=> r _; rewrite -integralZl//; first exact: integrable_indic.
    by apply: integral_ge0 => t _; rewrite nnfun_muleindic_ge0.
  apply: eq_bigr => r _; rewrite (mulrC y) EFinM.
  by rewrite [X in _ * X]muleC muleACA.
suff: forall

hSource code

: {nnsfun T >-> R},
    (\sum_(

ySource code

\in range h) (y%:E * \int[P]_

wSource code

 (\1_(h @^-1` [set y]) w)%:E)%E)%R
    = \int[P]_

wSource code

 (h w)%:E.
  by move=> suf; congr *%E; rewrite suf.
move=> h.
apply/esym.
under eq_integral do rewrite (fimfunE h) -fsumEFin//.
rewrite ge0_integral_fsum//.
- by move=> r; exact/measurable_EFinP/measurable_funM.
- by move=> r t _; rewrite lee_fin -lee_fin nnfun_muleindic_ge0.
by apply: eq_fsbigr => y fy; rewrite -integralZl//; exact/integrable_indic.
Qed.

Lemma

ge0_independent_expectationMSource code

 (

XSource code

YSource code

: {RV P >-> R}) :
  independent_RVs2 P X Y ->
  'E_P[X] *? 'E_P[Y] ->
  (forall

tSource code

, 0 <= X t)%R -> (forall

tSource code

, 0 <= Y t)%R ->
  'E_P [X * Y] = 'E_P [X] * 'E_P [Y].

Proof.

move=> indeXY defXY X0 Y0.
have mX : measurable_fun setT (EFin \o X) by exact/measurable_EFinP.
have mY : measurable_fun setT (EFin \o Y) by exact/measurable_EFinP.
pose X_ := nnsfun_approx measurableT mX.
pose Y_ := nnsfun_approx measurableT mY.
have EXY : 'E_P[X_ n \* Y_ n] @[

nSource code

--> \oo] --> 'E_P [X * Y].
  rewrite unlock; have -> : \int[P]_

wSource code

 ((X * Y) w)%:E =
      \int[P]_

xSource code

limn (fun

nSource code

=> (EFin \o (X_ n \* Y_ n)%R) x).
    apply: eq_integral => t _; apply/esym/cvg_lim => //=.
    rewrite fctE EFinM; under eq_fun do rewrite EFinM.
    by apply: cvgeM; [rewrite mule_def_fin//|
      apply: cvg_nnsfun_approx => //= x _; rewrite lee_fin..].
  apply: cvg_monotone_convergence => //.
  - by move=> n; apply/measurable_EFinP; exact: measurable_funM.
  - by move=> n t _; rewrite lee_fin.
  - move=> t _ m n mn.
    by rewrite lee_fin/= ler_pM//; exact/lefP/nd_nnsfun_approx.
have EX : 'E_P[X_ n] @[

nSource code

--> \oo] --> 'E_P [X].
  rewrite unlock.
  have -> : \int[P]_

wSource code

 (X w)%:E = \int[P]_

xSource code

limn (fun

nSource code

=> (EFin \o X_ n) x).
    by apply: eq_integral => t _; apply/esym/cvg_lim => //=;
      apply: cvg_nnsfun_approx => // x _; rewrite lee_fin.
 apply: cvg_monotone_convergence => //.
  - by move=> n; exact/measurable_EFinP.
  - by move=> n t _; rewrite lee_fin.
  - by move=> t _ m n mn; rewrite lee_fin/=; exact/lefP/nd_nnsfun_approx.
have EY : 'E_P[Y_ n] @[

nSource code

--> \oo] --> 'E_P [Y].
  rewrite unlock.
  have -> : \int[P]_

wSource code

 (Y w)%:E = \int[P]_

xSource code

limn (fun

nSource code

=> (EFin \o Y_ n) x).
    by apply: eq_integral => t _; apply/esym/cvg_lim => //=;
      apply: cvg_nnsfun_approx => // x _; rewrite lee_fin.
 apply: cvg_monotone_convergence => //.
  - by move=> n; exact/measurable_EFinP.
  - by move=> n t _; rewrite lee_fin.
  - by move=> t _ m n mn; rewrite lee_fin/=; exact/lefP/nd_nnsfun_approx.
have {EX EY}EXY' : 'E_P[X_ n] * 'E_P[Y_ n] @[

nSource code

--> \oo] --> 'E_P[X] * 'E_P[Y].
  apply: cvgeM => //.
suff : forall

nSource code

, 'E_P[X_ n \* Y_ n] = 'E_P[X_ n] * 'E_P[Y_ n].
  by move=> suf; apply: (cvg_unique _ EXY) => //=; under eq_fun do rewrite suf.
move=> n; apply: expectationM_nnsfun => x y xX_ yY_.
suff : P (\big[setI/setT]_(

jSource code

<- [fset false; true]%fset)
    [eta fun=> set0 with 0%N |-> X_ n @^-1` [set x],
                       1%N |-> Y_ n @^-1` [set y]] j) =
   \prod_(

jSource code

<- [fset false; true]%fset)
      P ([eta fun=> set0 with 0%N |-> X_ n @^-1` [set x],
                            1%N |-> Y_ n @^-1` [set y]] j).
  by rewrite !big_fsetU1/= ?inE//= !big_seq_fset1/=.
move: indeXY; apply => // i.
pose AX := dyadic_approx setT (EFin \o X).
pose AY := dyadic_approx setT (EFin \o Y).
pose BX := integer_approx setT (EFin \o X).
pose BY := integer_approx setT (EFin \o Y).
have mA (

ZSource code

: {RV P >-> R})

mSource code

kSource code

: (k < m * 2 ^ m)%N ->
    g_sigma_algebra_preimage Z (dyadic_approx setT (EFin \o Z) m k).
  move=> mk; rewrite /g_sigma_algebra_preimage /dyadic_approx mk setTI.
  rewrite /preimage_set_system/=; exists [set` dyadic_itv R m k] => //.
  rewrite setTI/=; apply/seteqP; split => z/=.
    by rewrite inE/= => Zz; exists (Z z).
  by rewrite inE/= => -[r rmk] [<-].
have mB (

ZSource code

: {RV P >-> R})

kSource code

:
    g_sigma_algebra_preimage Z (integer_approx setT (EFin \o Z) k).
  rewrite /g_sigma_algebra_preimage /integer_approx setTI /preimage_set_system/=.
  by exists `[k%:R, +oo[%classic => //; rewrite setTI preimage_itvcy.
have m1A (

ZSource code

: {RV P >-> R}) : forall

kSource code

, (k < n * 2 ^ n)%N ->
    measurable_fun setT
    (\1_(dyadic_approx setT (EFin \o Z) n k) : g_sigma_algebra_preimageType Z -> R).
  move=> k kn.
  exact/(@measurable_indicP _ (g_sigma_algebra_preimageType Z))/mA.
rewrite !inE => /orP[|]/eqP->{i} //=.
- have : @measurable_fun _ _ (g_sigma_algebra_preimageType X) _ setT (X_ n).
    rewrite nnsfun_approxE//; apply: measurable_funD => //=.
      apply: measurable_sum => //= k'; apply: measurable_funM => //.
      by apply: measurable_indic; exact: mA.
    apply: measurable_funM => //.
    by apply: measurable_indic; exact: mB.
  rewrite /measurable_fun => /(_ measurableT _ (measurable_set1 x)).
  by rewrite setTI.
- have : @measurable_fun _ _ (g_sigma_algebra_preimageType Y) _ setT (Y_ n).
    rewrite nnsfun_approxE//; apply: measurable_funD => //=.
      apply: measurable_sum => //= k'; apply: measurable_funM => //.
      by apply: measurable_indic; exact: mA.
    by apply: measurable_funM => //; apply: measurable_indic; exact: mB.
  by move=> /(_ measurableT [set y] (measurable_set1 y)); rewrite setTI.
Qed.

End expectationM.

Section product_expectation.
Context {

RSource code

: realType} {

dSource code

} {

TSource code

: measurableType d} (

PSource code

: probability T R).
Local Open Scope ereal_scope.

Import HBNNSimple.
Import MeasurableR.

Lemma

independent_Lfun1_expectationM_ltySource code

 (

XSource code

YSource code

: {RV P >-> R}) :
  independent_RVs2 P X Y ->
  (X : _ -> _) \in Lfun P 1 -> (Y : _ -> _) \in Lfun P 1 ->
  `|'E_P [X * Y]| < +oo.

Proof.

move=> indeXY iX iY.
apply: (@le_lt_trans _ _ 'E_P[(@normr _ _ \o X) * (@normr _ _ \o Y)]).
  rewrite unlock/= (le_trans (le_abse_integral _ _ _))//.
    apply/measurable_EFinP/measurable_funM.
      by move/Lfun1_integrable : iX => /measurable_int/measurable_EFinP.
    by move/Lfun1_integrable : iY => /measurable_int/measurable_EFinP.
  apply: ge0_le_integral => //=.
  - by apply/measurable_EFinP; exact/measurableT_comp.
  - by apply/measurable_EFinP; apply/measurable_funM; exact/measurableT_comp.
  - by move=> t _; rewrite lee_fin/= normrM.
rewrite ge0_independent_expectationM//=.
- exact: independent_RVs2_comp.
- apply: mule_def_fin; rewrite unlock integrable_fin_num//.
  + by move/Lfun_norm : iX => /Lfun1_integrable.
  + by move/Lfun_norm : iY => /Lfun1_integrable.
- rewrite lte_mul_pinfty//.
  + by rewrite expectation_ge0/=.
  + rewrite expectation_fin_num//=.
    by move: iX => /Lfun_norm.
  + move : iY => /Lfun1_integrable/integrableP[_].
    by rewrite unlock.
Qed.

Lemma

independent_Lfun1MSource code

 (

XSource code

YSource code

: {RV P >-> R}) :
  independent_RVs2 P X Y ->
  (X : _ -> _) \in Lfun P 1 -> (Y : _ -> _) \in Lfun P 1 ->
  (X \* Y)%R \in Lfun P 1.

Proof.

move=> indeXY iX iY.
apply/Lfun1_integrable.
apply/integrableP; split => //.
  move/Lfun1_integrable : iX => /integrableP[iX _].
  move/Lfun1_integrable : iY => /integrableP[iY _].
  exact/measurable_EFinP/measurable_funM/measurable_EFinP.
have := independent_Lfun1_expectationM_lty indeXY iX iY.
rewrite unlock => /abse_integralP; apply => //.
exact/measurable_EFinP/measurable_funM.
Qed.

Lemma

independent_expectationMSource code

 (

XSource code

YSource code

: {RV P >-> R}) :
  independent_RVs2 P X Y ->
  (X : _ -> _) \in Lfun P 1 -> (Y : _ -> _) \in Lfun P 1 ->
  'E_P [X * Y] = 'E_P [X] * 'E_P [Y].

Proof.

move=> XY iX iY.
transitivity ('E_P[(X^\+ - X^\-) * (Y^\+ - Y^\-)]).
  by congr ('E_P[_]); apply/funext => /= t; rewrite !funrposBneg.
have ? : X^\-%R \in Lfun P 1.
  apply/Lfun1_integrable; rewrite -funerneg; apply/integrable_funeneg => //.
  exact/Lfun1_integrable.
have ? : X^\-%R \in Lfun P 1.
  apply/Lfun1_integrable; rewrite -funerneg; apply/integrable_funeneg => //.
  exact/Lfun1_integrable.
have ? : X^\+%R \in Lfun P 1.
  apply/Lfun1_integrable; rewrite -funerpos; apply/integrable_funepos => //.
  exact/Lfun1_integrable.
have ? : Y^\+%R \in Lfun P 1.
  apply/Lfun1_integrable; rewrite -funerpos; apply/integrable_funepos => //.
  exact/Lfun1_integrable.
have ? : Y^\-%R \in Lfun P 1.
  apply/Lfun1_integrable; rewrite -funerneg; apply/integrable_funeneg => //.
  exact/Lfun1_integrable.
have ? : (X^\+ \* Y^\+)%R \in Lfun P 1.
  by apply: independent_Lfun1M => //=; exact: independent_RVs2_funrpospos.
have ? : (X^\- \* Y^\+)%R \in Lfun P 1.
  by apply: independent_Lfun1M => //=; exact: independent_RVs2_funrnegpos.
have ? : (X^\+ \* Y^\-)%R \in Lfun P 1.
  by apply: independent_Lfun1M => //=; exact: independent_RVs2_funrposneg.
have ? : (X^\- \* Y^\-)%R \in Lfun P 1.
  by apply: independent_Lfun1M => //=; exact: independent_RVs2_funrnegneg.
transitivity ('E_P[X^\+ * Y^\+] - 'E_P[X^\- * Y^\+]
              - 'E_P[X^\+ * Y^\-] + 'E_P[X^\- * Y^\-]).
  rewrite mulrDr !mulrDl -!expectationB//=; first by rewrite rpredB.
  rewrite -expectationD//=; first by rewrite !rpredB.
  congr ('E_P[_]); apply/funext => t/=.
  by rewrite !fctE !(mulNr,mulrN,opprK,addrA).
rewrite [in LHS]ge0_independent_expectationM//=.
  exact: independent_RVs2_funrpospos.
  by rewrite mule_def_fin// expectation_fin_num.
rewrite [in LHS]ge0_independent_expectationM//=.
  exact: independent_RVs2_funrnegpos.
  by rewrite mule_def_fin// expectation_fin_num.
rewrite [in LHS]ge0_independent_expectationM//=.
  exact: independent_RVs2_funrposneg.
  by rewrite mule_def_fin// expectation_fin_num.
rewrite [in LHS]ge0_independent_expectationM//=.
  exact: independent_RVs2_funrnegneg.
  by rewrite mule_def_fin// expectation_fin_num.
transitivity ('E_P[X^\+ - X^\-] * 'E_P[Y^\+ - Y^\-]); last first.
  by rewrite !funrposBneg.
rewrite -addeA -addeACA -muleBr.
  by rewrite expectation_fin_num.
  by rewrite fin_num_adde_defr// expectation_fin_num.
rewrite -oppeB.
  by rewrite fin_num_adde_defr// fin_numM// expectation_fin_num.
rewrite -muleBr.
  by rewrite expectation_fin_num.
  by rewrite fin_num_adde_defr// expectation_fin_num.
rewrite -muleBl.
- by rewrite fin_numB// !expectation_fin_num.
- by rewrite fin_num_adde_defr// expectation_fin_num.
- by rewrite -!expectationB.
Qed.

End product_expectation.