Library probsa.probability.conditional
Recall that a probability of an event A given an event B (ℙ[
A | B ]) is undefined if the probability of B is
zero. Therefore, our formalization of conditional probability
function expects as an argument a proof that event B has a
positive probability.
The purpose of the PosProb class is to provide a way to check if
the probability of an event defined by a predicate S is
positive. Specifically, it asserts that the probability of the set
{ω : Ω | S ω} according to measure μ is greater than zero.
This notion is defined as a typeclass to facilitate inference of
the implicit argument about positive probability of an event.
Class PosProb {Ω} (μ : measure Ω) (S : pred Ω) :=
pos_prob : ℙ<μ>{[ S ]} > 0.
Global Instance posprob_xpredT :
∀ Ω {μ : measure Ω}, PosProb μ xpredT.
Proof. by move ⇒ ? ?; rewrite /PosProb pr_xpredT; nra. Qed.
pos_prob : ℙ<μ>{[ S ]} > 0.
Global Instance posprob_xpredT :
∀ Ω {μ : measure Ω}, PosProb μ xpredT.
Proof. by move ⇒ ? ?; rewrite /PosProb pr_xpredT; nra. Qed.
Conditional Measure μ ↦ μ|S
In this section, we define a "conditional measure", which is a measure restricted to a subset of Ω.
... and a subset of Ω satisfying a predicate S; let us
further assume that the subset has positive probability.
Then, conditional measure "μ restricted on S" can be defined
as follows:
μ|S := λ ω ⇒ if (S ω) then μ ω / ℙ<μ>{[ S ]} else 0.
Definition pmf_restricted :=
fun ω:Ω ⇒ if S ω then pmf μ ω / ℙ<μ>{[ S ]} else 0.
Lemma pmf_nonnegative : ∀ ω, pmf_restricted ω ≥ 0.
Proof.
rewrite /pmf_restricted ⇒ ω; case: (S ω); last by apply Rle_refl.
by apply Rle_ge, Rle_mult_inv_pos; first (destruct μ; apply Rge_le).
Qed.
Lemma pmf_sums_to_1 : is_series (countable_sum pmf_restricted) 1.
Proof.
rewrite /pmf_restricted.
apply is_seriesC_ext with (a := fun ω:Ω ⇒ (if S ω then pmf μ ω else 0) / ℙ<μ>{[ S ]}).
{ by intros ω; case: (S ω); [reflexivity | apply Rmult_0_l]. }
replace 1%R with (ℙ<μ>{[ S ]} × /ℙ<μ>{[ S ]})%R; last first.
{ by apply Rinv_r, Rsqr_gt_0_0, Rmult_lt_0_compat. }
by apply is_seriesC_scal_r, Series_correct, pr_ex_series.
Qed.
fun ω:Ω ⇒ if S ω then pmf μ ω / ℙ<μ>{[ S ]} else 0.
Lemma pmf_nonnegative : ∀ ω, pmf_restricted ω ≥ 0.
Proof.
rewrite /pmf_restricted ⇒ ω; case: (S ω); last by apply Rle_refl.
by apply Rle_ge, Rle_mult_inv_pos; first (destruct μ; apply Rge_le).
Qed.
Lemma pmf_sums_to_1 : is_series (countable_sum pmf_restricted) 1.
Proof.
rewrite /pmf_restricted.
apply is_seriesC_ext with (a := fun ω:Ω ⇒ (if S ω then pmf μ ω else 0) / ℙ<μ>{[ S ]}).
{ by intros ω; case: (S ω); [reflexivity | apply Rmult_0_l]. }
replace 1%R with (ℙ<μ>{[ S ]} × /ℙ<μ>{[ S ]})%R; last first.
{ by apply Rinv_r, Rsqr_gt_0_0, Rmult_lt_0_compat. }
by apply is_seriesC_scal_r, Series_correct, pr_ex_series.
Qed.
Definition restrict : measure Ω :=
mkDistrib Ω pmf_restricted pmf_nonnegative pmf_sums_to_1.
Remark pmf_restricted_pred :
∀ ω, pmf_restricted ω > 0 → S ω.
Proof.
clear; intros; unfold pmf_restricted in ×.
destruct (S ω) eqn:Pω ⇒ //.
by apply Rlt_irrefl in H.
Qed.
End ConditionalMeasure.
mkDistrib Ω pmf_restricted pmf_nonnegative pmf_sums_to_1.
Remark pmf_restricted_pred :
∀ ω, pmf_restricted ω > 0 → S ω.
Proof.
clear; intros; unfold pmf_restricted in ×.
destruct (S ω) eqn:Pω ⇒ //.
by apply Rlt_irrefl in H.
Qed.
End ConditionalMeasure.
Conditional Probability and CDF
Conditional probability is defined using the notion of conditional measure.Definition pr_cond {Ω} (μ : measure Ω) (S : pred Ω) `{PosProb _ μ S} (P : pred Ω) : R :=
ℙ<restrict μ S>{[ P ]}.
Notation "'ℙ<' μ '>{[' A '|' B ']}'" := (pr_cond μ B A)
(at level 10, format "ℙ< μ >{[ A | B ]}") : probability_scope.
Notation "'ℙ<' μ , ρ '>{[' A '|' B ']}'" := (@pr_cond _ μ B ρ A)
(at level 10, only parsing, format "ℙ< μ , ρ >{[ A | B ]}") : probability_scope.
Definition cdf_cond {Ω} {μ : measure Ω} (B : pred Ω) `{PosProb _ μ B} (X : nrvar μ) (x : nat) :=
ℙ<μ>{[ X ⟨<=⟩ x | B ]}.
Notation "'𝔽<' μ '>{[' A '|' B ']}(' x ')'" := (@cdf_cond _ μ B _ A x)
(at level 10, format "𝔽< μ >{[ A | B ]}( x )") : probability_scope.
Notation "'𝔽<' μ , ρ '>{[' A '|' B ']}(' x ')'" := (@cdf_cond _ μ B ρ A x)
(at level 10, only parsing, format "𝔽< μ , ρ >{[ A | B ]}( x )") : probability_scope.
Notation "'𝔽<' μ , ρ '>{[' A '|' B ']}'" := (@cdf_cond _ μ B ρ A)
(at level 10, only parsing, format "𝔽< μ , ρ >{[ A | B ]}") : probability_scope.
Equivalence to Textbook Definition
In this section, we prove that the measure-based definition (μ|S := ...) of conditional probability coincides with the axiomatic definition ℙ{[A | B]} = ℙ{[ A ∩ B ]} / ℙ{[ B ]}.
Section AxiomaticConditionalProbability.
Context {Ω} (μ : measure Ω).
Context (A : pred Ω) (B : pred Ω) `{PosProb _ μ B}.
Lemma pr_cond_axiomatic :
ℙ<μ>{[ A | B ]} = ℙ<μ>{[ A ∩ B ]} / ℙ<μ>{[ B ]}.
Proof.
rewrite /pr_cond {1}/pr /restrict /pmf_restricted.
erewrite SeriesC_ext; first last.
{ instantiate (1 := (fun ω:Ω ⇒ (if A ω && B ω then pmf μ ω else 0) / ℙ<μ>{[ B ]})).
move ⇒ ω //=; destruct (A ω), (B ω); first by done.
all: by rewrite /Rdiv Rmult_0_l.
}
by rewrite /Rdiv SeriesC_scal_r.
Qed.
Lemma pr_cond_axiomatic' :
ℙ<μ>{[ A ∩ B ]} = ℙ<μ>{[ B ]} × ℙ<μ>{[ A | B ]}.
Proof.
rewrite pr_cond_axiomatic.
rewrite -Rmult_assoc Rinv_r_simpl_m; first reflexivity.
move: (H); unfold PosProb ⇒ POS Z; rewrite Z in POS.
by apply Rgt_irrefl in POS.
Qed.
End AxiomaticConditionalProbability.
Context {Ω} (μ : measure Ω).
Context (A : pred Ω) (B : pred Ω) `{PosProb _ μ B}.
Lemma pr_cond_axiomatic :
ℙ<μ>{[ A | B ]} = ℙ<μ>{[ A ∩ B ]} / ℙ<μ>{[ B ]}.
Proof.
rewrite /pr_cond {1}/pr /restrict /pmf_restricted.
erewrite SeriesC_ext; first last.
{ instantiate (1 := (fun ω:Ω ⇒ (if A ω && B ω then pmf μ ω else 0) / ℙ<μ>{[ B ]})).
move ⇒ ω //=; destruct (A ω), (B ω); first by done.
all: by rewrite /Rdiv Rmult_0_l.
}
by rewrite /Rdiv SeriesC_scal_r.
Qed.
Lemma pr_cond_axiomatic' :
ℙ<μ>{[ A ∩ B ]} = ℙ<μ>{[ B ]} × ℙ<μ>{[ A | B ]}.
Proof.
rewrite pr_cond_axiomatic.
rewrite -Rmult_assoc Rinv_r_simpl_m; first reflexivity.
move: (H); unfold PosProb ⇒ POS Z; rewrite Z in POS.
by apply Rgt_irrefl in POS.
Qed.
End AxiomaticConditionalProbability.
First, we prove that the probability over a restricted measure
can be "folded" back to conditional probability...
Lemma fold_prob_to_cond_prob :
∀ {Ω} (μ : measure Ω) (A B : pred Ω) (ρ : PosProb μ B),
ℙ<@restrict _ μ B ρ>{[ A ]} = ℙ<μ, ρ>{[ A | B ]}.
Proof. by rewrite/pr_cond. Qed.
∀ {Ω} (μ : measure Ω) (A B : pred Ω) (ρ : PosProb μ B),
ℙ<@restrict _ μ B ρ>{[ A ]} = ℙ<μ, ρ>{[ A | B ]}.
Proof. by rewrite/pr_cond. Qed.
... and show a similar folding lemma for conditional CDF.
Lemma fold_prob_to_cond_cdf :
∀ {Ω} (μ : measure Ω) (B : pred Ω) (X : nrvar μ) (c : nat) `{PosProb Ω μ B},
ℙ<restrict μ B>{[ X ⟨<=⟩ c ]} = 𝔽<μ,_>{[ X | B ]}(c).
Proof. by rewrite /cdf_cond /pr_cond. Qed.
∀ {Ω} (μ : measure Ω) (B : pred Ω) (X : nrvar μ) (c : nat) `{PosProb Ω μ B},
ℙ<restrict μ B>{[ X ⟨<=⟩ c ]} = 𝔽<μ,_>{[ X | B ]}(c).
Proof. by rewrite /cdf_cond /pr_cond. Qed.
We prove that the probability of an event P conditioned on an
event that is always true xpredT is equal to the probability
of P.
Lemma pr_cond_xpredT :
∀ {Ω} (μ : measure Ω) (P : pred Ω) `{PosProb _ μ xpredT},
ℙ<μ,_>{[ P | xpredT ]} = ℙ<μ>{[ P ]}.
Proof.
move ⇒ Ω μ P POS; rewrite /pr_cond /pr.
apply SeriesC_ext ⇒ ω.
case (P ω); last by done.
destruct μ ⇒ //=.
by rewrite /pmf_restricted pr_xpredT Rdiv_1.
Qed.
Lemma cdf_cond_xpredT :
∀ {Ω} (μ : measure Ω) (P : nrvar μ) (ρ : PosProb _ _) (x : nat),
𝔽<μ,ρ>{[ P | xpredT ]}(x) = 𝔽<μ>{[ P ]}(x).
Proof. by intros; rewrite /cdf_cond /cdf pr_cond_xpredT. Qed.
Lemma pr_cond_xpred1 :
∀ {Ω} (μ : measure Ω) (P : pred Ω) (ω0 : Ω) (ρ : PosProb _ _),
ℙ<μ>{[ P | xpred1 ω0 ]} = I[ P ω0 ].
Proof.
intros *; rewrite pr_cond_axiomatic.
case Pω0: (P ω0); unfold "∩", pred.pred_intersection.
{ erewrite pr_eq_pred with (Q := eq_op^~ ω0); first last.
{ intros ω1; rewrite !unfold_in.
case EQ : (ω1 == ω0).
{ by move: EQ ⇒ /eqP EQ; subst;rewrite Pω0. }
{ by rewrite andb_false_r. }
}
rewrite /Rdiv -Rinv_r_sym; first by done.
by move: ρ; rewrite /PosProb; nra.
}
{ erewrite pr_eq_pred with (Q := xpred0); first last.
{ intros ω1; rewrite !unfold_in.
case EQ : (ω1 == ω0).
{ by move: EQ ⇒ /eqP EQ; subst;rewrite Pω0. }
{ by rewrite andb_false_r. }
}
by move: ρ; rewrite /PosProb pr_xpred0 //=; nra.
}
Qed.
∀ {Ω} (μ : measure Ω) (P : pred Ω) `{PosProb _ μ xpredT},
ℙ<μ,_>{[ P | xpredT ]} = ℙ<μ>{[ P ]}.
Proof.
move ⇒ Ω μ P POS; rewrite /pr_cond /pr.
apply SeriesC_ext ⇒ ω.
case (P ω); last by done.
destruct μ ⇒ //=.
by rewrite /pmf_restricted pr_xpredT Rdiv_1.
Qed.
Lemma cdf_cond_xpredT :
∀ {Ω} (μ : measure Ω) (P : nrvar μ) (ρ : PosProb _ _) (x : nat),
𝔽<μ,ρ>{[ P | xpredT ]}(x) = 𝔽<μ>{[ P ]}(x).
Proof. by intros; rewrite /cdf_cond /cdf pr_cond_xpredT. Qed.
Lemma pr_cond_xpred1 :
∀ {Ω} (μ : measure Ω) (P : pred Ω) (ω0 : Ω) (ρ : PosProb _ _),
ℙ<μ>{[ P | xpred1 ω0 ]} = I[ P ω0 ].
Proof.
intros *; rewrite pr_cond_axiomatic.
case Pω0: (P ω0); unfold "∩", pred.pred_intersection.
{ erewrite pr_eq_pred with (Q := eq_op^~ ω0); first last.
{ intros ω1; rewrite !unfold_in.
case EQ : (ω1 == ω0).
{ by move: EQ ⇒ /eqP EQ; subst;rewrite Pω0. }
{ by rewrite andb_false_r. }
}
rewrite /Rdiv -Rinv_r_sym; first by done.
by move: ρ; rewrite /PosProb; nra.
}
{ erewrite pr_eq_pred with (Q := xpred0); first last.
{ intros ω1; rewrite !unfold_in.
case EQ : (ω1 == ω0).
{ by move: EQ ⇒ /eqP EQ; subst;rewrite Pω0. }
{ by rewrite andb_false_r. }
}
by move: ρ; rewrite /PosProb pr_xpred0 //=; nra.
}
Qed.
Notice that the value of conditional probability does not
change depending on the accompanying proof. Hence, one can
switch between different proofs without changing the value.
Lemma cond_prob_posprob_irrelevance :
∀ {Ω} (μ : measure Ω) (A B : pred Ω) (ρ1 ρ2 : PosProb μ B),
ℙ<μ, ρ1>{[ A | B ]} = ℙ<μ, ρ2>{[ A | B ]}.
Proof. by done. Qed.
∀ {Ω} (μ : measure Ω) (A B : pred Ω) (ρ1 ρ2 : PosProb μ B),
ℙ<μ, ρ1>{[ A | B ]} = ℙ<μ, ρ2>{[ A | B ]}.
Proof. by done. Qed.
We prove a similar lemma for conditional CDF.
Lemma cond_cdf_posprob_irrelevance :
∀ {Ω} (μ : measure Ω) (A : nrvar μ) (B : pred Ω) (x : nat) (ρ1 ρ2 : PosProb μ B),
𝔽<μ, ρ1>{[ A | B ]}(x) = 𝔽<μ, ρ2>{[ A | B ]}(x).
Proof. by done. Qed.
Lemma pr_cond_eq_pred :
∀ {Ω} (μ : measure Ω) (P Q B : pred Ω) (ρ1 ρ2 : PosProb μ B),
(∀ ω, B ω → P ω ↔ Q ω) →
ℙ<μ, ρ1>{[ P | B ]} = ℙ<μ, ρ2>{[ Q | B ]}.
Proof.
intros × EQUIV; rewrite /pr_cond /pr /restrict /pmf_restricted.
apply SeriesC_ext ⇒ ω ⇒ //=.
destruct (B _) eqn:BP, P eqn:PP, Q eqn:QP; try done.
- by specialize (EQUIV ω BP); apply EQUIV in PP; rewrite PP in QP.
- by specialize (EQUIV ω BP); apply EQUIV in QP; rewrite QP in PP.
Qed.
Lemma pr_cond_eq_cond :
∀ {Ω} (μ : measure Ω) (P B C : pred Ω) (ρ1 : PosProb μ B) (ρ2 : PosProb μ C),
(∀ ω, B ω = C ω) →
ℙ<μ, ρ1>{[ P | B ]} = ℙ<μ, ρ2>{[ P | C ]}.
Proof.
intros × EQ; apply SeriesC_ext ⇒ ω.
destruct P; last by done.
rewrite /restrict /pmf_restricted //= EQ; case: (C ω); last by done.
rewrite /Rdiv; apply Rmult_eq_compat_l; clear ω.
have L : ∀ a b, a = b → / a = / b by clear; intros; subst b.
by apply L, pr_eq_pred ⇒ ω; rewrite !unfold_in.
Qed.
Lemma cdf_cond_eq_cond :
∀ {Ω} (μ : measure Ω) (P : nrvar μ) (B C : pred Ω) (x : nat) ρ1 ρ2,
(∀ ω, B ω = C ω) →
𝔽<μ, ρ1>{[ P | B ]}(x) = 𝔽<μ, ρ2>{[ P | C ]}(x).
Proof.
unfold cdf_cond; intros.
by apply pr_cond_eq_cond.
Qed.
Lemma pr_cond_eq_pred_0 :
∀ {Ω} (μ : measure Ω) (A B : pred Ω) ρ,
(∀ ω, B ω → ~~ A ω) →
ℙ<μ, ρ>{[ A | B ]} = 0.
Proof.
intros × NE; apply pr_zero ⇒ ω POS.
apply/negP/negP; apply: NE.
by apply pmf_restricted_pred in POS.
Qed.
Lemma pr_cond_mono_pred :
∀ {Ω} (μ : measure Ω) (P Q C : pred Ω) ρ1 ρ2,
(∀ ω : Ω, C ω → P ω → Q ω) →
ℙ<μ, ρ1>{[ P | C ]} ≤ ℙ<μ, ρ2>{[ Q | C ]}.
Proof.
intros × IMP.
erewrite cond_prob_posprob_irrelevance; rewrite /pr_cond; apply pr_mono_pred_pos.
move⇒ ω POS Pω; apply IMP ⇒ //.
by apply pmf_restricted_pred in POS.
Qed.
∀ {Ω} (μ : measure Ω) (A : nrvar μ) (B : pred Ω) (x : nat) (ρ1 ρ2 : PosProb μ B),
𝔽<μ, ρ1>{[ A | B ]}(x) = 𝔽<μ, ρ2>{[ A | B ]}(x).
Proof. by done. Qed.
Lemma pr_cond_eq_pred :
∀ {Ω} (μ : measure Ω) (P Q B : pred Ω) (ρ1 ρ2 : PosProb μ B),
(∀ ω, B ω → P ω ↔ Q ω) →
ℙ<μ, ρ1>{[ P | B ]} = ℙ<μ, ρ2>{[ Q | B ]}.
Proof.
intros × EQUIV; rewrite /pr_cond /pr /restrict /pmf_restricted.
apply SeriesC_ext ⇒ ω ⇒ //=.
destruct (B _) eqn:BP, P eqn:PP, Q eqn:QP; try done.
- by specialize (EQUIV ω BP); apply EQUIV in PP; rewrite PP in QP.
- by specialize (EQUIV ω BP); apply EQUIV in QP; rewrite QP in PP.
Qed.
Lemma pr_cond_eq_cond :
∀ {Ω} (μ : measure Ω) (P B C : pred Ω) (ρ1 : PosProb μ B) (ρ2 : PosProb μ C),
(∀ ω, B ω = C ω) →
ℙ<μ, ρ1>{[ P | B ]} = ℙ<μ, ρ2>{[ P | C ]}.
Proof.
intros × EQ; apply SeriesC_ext ⇒ ω.
destruct P; last by done.
rewrite /restrict /pmf_restricted //= EQ; case: (C ω); last by done.
rewrite /Rdiv; apply Rmult_eq_compat_l; clear ω.
have L : ∀ a b, a = b → / a = / b by clear; intros; subst b.
by apply L, pr_eq_pred ⇒ ω; rewrite !unfold_in.
Qed.
Lemma cdf_cond_eq_cond :
∀ {Ω} (μ : measure Ω) (P : nrvar μ) (B C : pred Ω) (x : nat) ρ1 ρ2,
(∀ ω, B ω = C ω) →
𝔽<μ, ρ1>{[ P | B ]}(x) = 𝔽<μ, ρ2>{[ P | C ]}(x).
Proof.
unfold cdf_cond; intros.
by apply pr_cond_eq_cond.
Qed.
Lemma pr_cond_eq_pred_0 :
∀ {Ω} (μ : measure Ω) (A B : pred Ω) ρ,
(∀ ω, B ω → ~~ A ω) →
ℙ<μ, ρ>{[ A | B ]} = 0.
Proof.
intros × NE; apply pr_zero ⇒ ω POS.
apply/negP/negP; apply: NE.
by apply pmf_restricted_pred in POS.
Qed.
Lemma pr_cond_mono_pred :
∀ {Ω} (μ : measure Ω) (P Q C : pred Ω) ρ1 ρ2,
(∀ ω : Ω, C ω → P ω → Q ω) →
ℙ<μ, ρ1>{[ P | C ]} ≤ ℙ<μ, ρ2>{[ Q | C ]}.
Proof.
intros × IMP.
erewrite cond_prob_posprob_irrelevance; rewrite /pr_cond; apply pr_mono_pred_pos.
move⇒ ω POS Pω; apply IMP ⇒ //.
by apply pmf_restricted_pred in POS.
Qed.
This is a technical lemma that can be skipped. Intuitively, it
states that if we consider only those outcomes in the product
space where the first component belongs to B (i.e., product
measure is restricted to λ ω ⇒ B ω.1), then the probability of
A under this restricted measure is the same as the probability
of A under the original product measure, but with the first
measure restricted to B.
Lemma distribution_of_prod_restrict :
∀ {Ω1} {Ω2} (μ1 : measure Ω1) (μ2 : measure Ω2) (B : pred Ω1) (A : pred (Ω1 × Ω2))
{ρ12 : PosProb (distrib_prod μ1 μ2) (λ ω, B ω.1)} {ρ1 : PosProb μ1 B},
ℙ< restrict (distrib_prod μ1 μ2) (fun ω ⇒ B ω.1) >{[ A ]}
= ℙ< distrib_prod (restrict μ1 B) (μ2) >{[ A ]}.
Proof.
intros; apply pr_eq_measure ⇒ [[ω1 ω2]].
rewrite /restrict /distrib_prod /pmf_restricted /prod_pmf ⇒ //=.
destruct (B _); last by nra.
rewrite /Rdiv !Rmult_assoc; apply Rmult_eq_compat_l.
rewrite Rmult_comm; apply Rmult_eq_compat_r.
by rewrite pair_marginal1.
Qed.
Lemma pr_joint_pred_eq :
∀ {Ω1} {Ω2} (μ1 : measure Ω1) (μ2 : measure Ω2) A A1 A2,
(∀ ω, A ω = A1 ω.1 && A2 ω.2) →
ℙ<distrib_prod μ1 μ2>{[ A ]} = ℙ<μ1>{[ A1 ]} × ℙ<μ2>{[ A2 ]}.
Proof.
intros × EQ.
erewrite pr_eq_pred with (Q := fun ω ⇒ A1 ω.1 && A2 ω.2).
- by apply pair_joint_pred.
- by intros [ω c]; rewrite !unfold_in EQ.
Qed.
Lemma pr_cond_joint_pred_eq_cond_eq :
∀ {Ω1} {Ω2} (μ1 : measure Ω1) (μ2 : measure Ω2)
A A1 A2 B B1 B2 ρ ρ1 ρ2,
(∀ ω, A ω = A1 ω.1 && A2 ω.2) →
(∀ ω, B ω = B1 ω.1 && B2 ω.2) →
ℙ<distrib_prod μ1 μ2, ρ>{[ A | B ]} = ℙ<μ1, ρ1>{[ A1 | B1 ]} × ℙ<μ2, ρ2>{[ A2 | B2 ]}.
Proof.
intros × EQ1 EQ2; rewrite !/pr_cond; unfold PosProb in ×.
erewrite pr_eq_pred with (Q := fun ω ⇒ A1 ω.1 && A2 ω.2); first last.
{ by intros [ω c]; rewrite !unfold_in EQ1. }
rewrite [in X in X = _]fold_prob_to_cond_prob.
unshelve erewrite pr_cond_eq_cond with (C := fun ω ⇒ B1 ω.1 && B2 ω.2);
[ rewrite /PosProb pair_joint_pred; nra | | done ].
rewrite /pr_cond; erewrite pr_eq_measure; first by apply pair_joint_pred.
intros [ω1 ω2]; rewrite //= /pmf_restricted pair_joint_pred /prod_pmf /= /pmf_restricted //=.
destruct (B1 ω1), (B2 ω2) ⇒ //=; try nra.
rewrite /Rdiv !Rmult_assoc //=.
apply Rmult_eq_compat_l.
by rewrite Rmult_comm Rinv_mult_distr; nra.
Qed.
Lemma cdf_cond_marginal11 :
∀ {Ω1} {Ω2} (μ1 : measure Ω1) (μ2 : measure Ω2)
(A : nrvar (distrib_prod μ1 μ2)) (A' : nrvar μ1) (B : pred _) ρ1 ρ2 x,
(∀ ω, A ω = A' ω.1) →
𝔽<distrib_prod μ1 μ2, ρ1>{[ A | fun ω ⇒ B ω.1 ]}(x) = 𝔽<μ1, ρ2>{[ A' | B ]}(x).
Proof.
clear; intros × EQ; rewrite /cdf_cond /pr_cond distribution_of_prod_restrict.
erewrite pr_eq_pred with (Q := (fun ω ⇒ A' ω.1 ≤ x)%nat); first last.
{ by intros []; rewrite !unfold_in EQ. }
erewrite pr_eq_pred; first by erewrite pair_marginal1; reflexivity.
by move ⇒ [ω1 ω2]; rewrite !unfold_in.
Qed.
Lemma cdf_cond_marginal21 :
∀ {Ω1} {Ω2} (μ1 : measure Ω1) (μ2 : measure Ω2)
(A : nrvar (distrib_prod μ1 μ2)) (A' : nrvar μ2) B ρ1 ρ2 x,
(∀ ω, A ω = A' ω.2) →
𝔽<distrib_prod μ1 μ2, ρ1>{[ A | fun ω ⇒ B ω.1 ]}(x) = 𝔽<μ2, ρ2>{[ A' | xpredT ]}(x).
Proof.
clear; intros × EQ.
have ρ3 : PosProb μ1 B by rewrite /PosProb pair_marginal1 in ρ1.
rewrite /cdf_cond /pr_cond distribution_of_prod_restrict.
erewrite pr_eq_pred with (Q := (fun ω ⇒ A' ω.2 ≤ x)%nat); first last.
{ by intros []; rewrite !unfold_in EQ. }
erewrite pr_eq_pred.
{ erewrite pair_marginal2.
rewrite fold_prob_to_cond_prob pr_cond_xpredT.
reflexivity.
}
by move ⇒ [ω1 ω2]; rewrite !unfold_in.
Qed.
End BasicLemmas.
∀ {Ω1} {Ω2} (μ1 : measure Ω1) (μ2 : measure Ω2) (B : pred Ω1) (A : pred (Ω1 × Ω2))
{ρ12 : PosProb (distrib_prod μ1 μ2) (λ ω, B ω.1)} {ρ1 : PosProb μ1 B},
ℙ< restrict (distrib_prod μ1 μ2) (fun ω ⇒ B ω.1) >{[ A ]}
= ℙ< distrib_prod (restrict μ1 B) (μ2) >{[ A ]}.
Proof.
intros; apply pr_eq_measure ⇒ [[ω1 ω2]].
rewrite /restrict /distrib_prod /pmf_restricted /prod_pmf ⇒ //=.
destruct (B _); last by nra.
rewrite /Rdiv !Rmult_assoc; apply Rmult_eq_compat_l.
rewrite Rmult_comm; apply Rmult_eq_compat_r.
by rewrite pair_marginal1.
Qed.
Lemma pr_joint_pred_eq :
∀ {Ω1} {Ω2} (μ1 : measure Ω1) (μ2 : measure Ω2) A A1 A2,
(∀ ω, A ω = A1 ω.1 && A2 ω.2) →
ℙ<distrib_prod μ1 μ2>{[ A ]} = ℙ<μ1>{[ A1 ]} × ℙ<μ2>{[ A2 ]}.
Proof.
intros × EQ.
erewrite pr_eq_pred with (Q := fun ω ⇒ A1 ω.1 && A2 ω.2).
- by apply pair_joint_pred.
- by intros [ω c]; rewrite !unfold_in EQ.
Qed.
Lemma pr_cond_joint_pred_eq_cond_eq :
∀ {Ω1} {Ω2} (μ1 : measure Ω1) (μ2 : measure Ω2)
A A1 A2 B B1 B2 ρ ρ1 ρ2,
(∀ ω, A ω = A1 ω.1 && A2 ω.2) →
(∀ ω, B ω = B1 ω.1 && B2 ω.2) →
ℙ<distrib_prod μ1 μ2, ρ>{[ A | B ]} = ℙ<μ1, ρ1>{[ A1 | B1 ]} × ℙ<μ2, ρ2>{[ A2 | B2 ]}.
Proof.
intros × EQ1 EQ2; rewrite !/pr_cond; unfold PosProb in ×.
erewrite pr_eq_pred with (Q := fun ω ⇒ A1 ω.1 && A2 ω.2); first last.
{ by intros [ω c]; rewrite !unfold_in EQ1. }
rewrite [in X in X = _]fold_prob_to_cond_prob.
unshelve erewrite pr_cond_eq_cond with (C := fun ω ⇒ B1 ω.1 && B2 ω.2);
[ rewrite /PosProb pair_joint_pred; nra | | done ].
rewrite /pr_cond; erewrite pr_eq_measure; first by apply pair_joint_pred.
intros [ω1 ω2]; rewrite //= /pmf_restricted pair_joint_pred /prod_pmf /= /pmf_restricted //=.
destruct (B1 ω1), (B2 ω2) ⇒ //=; try nra.
rewrite /Rdiv !Rmult_assoc //=.
apply Rmult_eq_compat_l.
by rewrite Rmult_comm Rinv_mult_distr; nra.
Qed.
Lemma cdf_cond_marginal11 :
∀ {Ω1} {Ω2} (μ1 : measure Ω1) (μ2 : measure Ω2)
(A : nrvar (distrib_prod μ1 μ2)) (A' : nrvar μ1) (B : pred _) ρ1 ρ2 x,
(∀ ω, A ω = A' ω.1) →
𝔽<distrib_prod μ1 μ2, ρ1>{[ A | fun ω ⇒ B ω.1 ]}(x) = 𝔽<μ1, ρ2>{[ A' | B ]}(x).
Proof.
clear; intros × EQ; rewrite /cdf_cond /pr_cond distribution_of_prod_restrict.
erewrite pr_eq_pred with (Q := (fun ω ⇒ A' ω.1 ≤ x)%nat); first last.
{ by intros []; rewrite !unfold_in EQ. }
erewrite pr_eq_pred; first by erewrite pair_marginal1; reflexivity.
by move ⇒ [ω1 ω2]; rewrite !unfold_in.
Qed.
Lemma cdf_cond_marginal21 :
∀ {Ω1} {Ω2} (μ1 : measure Ω1) (μ2 : measure Ω2)
(A : nrvar (distrib_prod μ1 μ2)) (A' : nrvar μ2) B ρ1 ρ2 x,
(∀ ω, A ω = A' ω.2) →
𝔽<distrib_prod μ1 μ2, ρ1>{[ A | fun ω ⇒ B ω.1 ]}(x) = 𝔽<μ2, ρ2>{[ A' | xpredT ]}(x).
Proof.
clear; intros × EQ.
have ρ3 : PosProb μ1 B by rewrite /PosProb pair_marginal1 in ρ1.
rewrite /cdf_cond /pr_cond distribution_of_prod_restrict.
erewrite pr_eq_pred with (Q := (fun ω ⇒ A' ω.2 ≤ x)%nat); first last.
{ by intros []; rewrite !unfold_in EQ. }
erewrite pr_eq_pred.
{ erewrite pair_marginal2.
rewrite fold_prob_to_cond_prob pr_cond_xpredT.
reflexivity.
}
by move ⇒ [ω1 ω2]; rewrite !unfold_in.
Qed.
End BasicLemmas.