Library probsa.probability.stochastic_order
From discprob.prob Require Export indep.
Require Export prosa.util.all.
From probsa.util Require Export bigop iota.
From probsa.probability Require Export conditional dominance_relation independence.
Require Export prosa.util.all.
From probsa.util Require Export bigop iota.
From probsa.probability Require Export conditional dominance_relation independence.
Remark: This file is not needed for the proof of the theorem about
adequacy of the axiomatic pWCET.
Section BasicLemmas.
Context {Ω} {μ : measure Ω}.
Variables (X Y : nrvar μ).
Hypothesis H_independent : indep2 X Y.
Lemma addrv_comm :
∀ ω, (X ⟨+⟩ Y) ω = (Y ⟨+⟩ X) ω.
Proof. by intros *; rewrite //= addnC. Qed.
Local Proposition addrv_eq_decomposition :
∀ t,
ℙ<μ>{[ X ⟨+⟩ Y ⟨=⟩ t ]}
= ∑_{0 ≤ i ≤ t} ℙ<μ>{[ X ⟨=⟩ i ]} × ℙ<μ>{[ Y ⟨=⟩ (t - i)%N ]}.
Proof.
intros s; unfold "⟨=⟩", nrvar_nat_pred_eqop.
rewrite (@pr_eq_pred'
_ _ _ (fun ω ⇒ has (fun i ⇒ (X ω == i) && (Y ω == s - i)) (index_iota 0 s.+1)))%nat; last first.
{ intros ω; split; [move ⇒ /eqP EQ | intros EQ].
- apply/hasP; ∃ (X ω).
rewrite mem_iota add0n ltnS -EQ; apply/andP; split ⇒ //.
+ by rewrite leq_addr.
+ apply/andP; split; first by done.
by rewrite -EQ //= addKn.
- move: EQ ⇒ /hasP [i IN /andP [/eqP EQ1 /eqP EQ2]].
rewrite //= EQ1 EQ2.
move: IN; rewrite mem_iota add0n ltnS ⇒ /andP [_ LE].
by rewrite subnKC.
}
rewrite union_disj_eq_sum_prob.
- apply eq_bigr ⇒ i _.
by rewrite H_independent.
- by intros *; move ⇒ /andP [/eqP → _] /andP [/eqP → _].
Qed.
Local Proposition addrv_leq_decomposition :
∀ t,
ℙ<μ>{[ X ⟨+⟩ Y ⟨<=⟩ t ]}
= ∑_{0 ≤ i ≤ t} ∑_{0 ≤ j ≤ t - i} ℙ<μ>{[ X ⟨=⟩ i ]} × ℙ<μ>{[ Y ⟨=⟩ j ]}.
Proof.
induction t.
- rewrite !big_nat1 -H_independent; unfold "⟨<=⟩", rvar_nat_pred_leqop.
apply pr_eq_pred' ⇒ ω //=; split; intros EQ.
+ by move: EQ; rewrite leqn0 addn_eq0.
+ by move: EQ ⇒ /andP [/eqP → /eqP ->].
- rewrite big_nat_recr //=.
rewrite subnn big_nat1.
erewrite eq_big_seq; last first.
{ intros i; rewrite mem_iota add0n ltnS ⇒ /andP [_ LEi].
rewrite subSn; last by done.
by rewrite big_nat_recr //=.
}
rewrite //= bigsum_add -IHt.
have EQ := cdf_succ_to_cdf_preq.
unfold cdf in EQ.
rewrite EQ; clear IHt.
rewrite Rplus_assoc; apply Rplus_eq_compat_l.
rewrite addrv_eq_decomposition.
rewrite big_nat_recr //= subnn; apply Rplus_eq_compat_r.
rewrite big_seq [in X in _ = X]big_seq; apply eq_bigr ⇒ i INi.
move: INi; rewrite mem_iota add0n ltnS ⇒ /andP [_ LEi].
by rewrite subSn.
Qed.
End BasicLemmas.
Section StochasticDomination.
Section AddrvRespectsStochasticOrderHelpers.
Context {Ω Ω'} {μ : measure Ω} {μ' : measure Ω'}.
Variables (t : nat) (X Y : nrvar μ) (X' Y' : nrvar μ').
Hypothesis H_dominates_X : X ⪯ X'.
Hypothesis H_dominates_Y : Y ⪯ Y'.
Hypothesis H_independent : indep2 X Y.
Hypothesis H_independent' : indep2 X' Y'.
Local Proposition addrv_respects_stochastic_order_step_1 :
ℙ<μ>{[ X ⟨+⟩ Y ⟨<=⟩ t ]}
= ∑_{0 ≤ i ≤ t} ∑_{0 ≤ j ≤ t} I[i + j ≤ t] × ℙ<μ>{[ X ⟨=⟩ i ]} × ℙ<μ>{[ Y ⟨=⟩ j ]}.
Proof.
rewrite addrv_leq_decomposition //.
rewrite big_seq [in X in _ = X]big_seq; apply eq_bigr ⇒ i INi.
symmetry; erewrite eq_big_seq; [symmetry | ]; last first.
{ intros j INj; move: INi; rewrite mem_iota add0n ltnS ⇒ /andP [_ LEi].
erewrite Rmult_assoc, Rmult_comm, Rmult_assoc; apply Rmult_eq_compat_l.
by rewrite Rmult_comm -leq_subRL; first reflexivity. }
rewrite bigsum_distr bigsum_distr; apply Rmult_eq_compat_l.
by apply bigsum_upper_bound_to_indicator; ssrlia.
Qed.
Local Proposition addrv_respects_stochastic_order_step_2 :
∑_{0 ≤ i ≤ t} ∑_{0 ≤ j ≤ t} I[i + j ≤ t] × ℙ<μ>{[ X ⟨=⟩ i ]} × ℙ<μ>{[ Y ⟨=⟩ j ]}
= ∑_{0 ≤ j ≤ t} ℙ<μ>{[ Y ⟨=⟩ j ]} × (∑_{0 ≤ i ≤ t} I[i ≤ t - j] × ℙ<μ>{[ X ⟨=⟩ i ]}).
Proof.
rewrite exchange_big //=.
rewrite big_seq [in X in _ = X]big_seq; apply eq_bigr ⇒ i IN1.
rewrite -bigsum_distr.
rewrite big_seq [in X in _ = X]big_seq; apply eq_bigr ⇒ j IN2.
rewrite !Rmult_assoc [in X in _ = X]Rmult_comm -!Rmult_assoc.
apply Rmult_eq_compat_r, Rmult_eq_compat_r.
destruct (j + i ≤ t)%nat eqn:LE1.
- by apply leq_subRL_impl in LE1; rewrite LE1.
- move: IN1; rewrite mem_iota add0n ltnS ⇒ /andP [_ LE3].
move: IN2; rewrite mem_iota add0n ltnS ⇒ /andP [_ LE4].
by destruct (j ≤ t - i)%nat eqn:LE2; [ssrlia | reflexivity].
Qed.
Local Proposition addrv_respects_stochastic_order_step_3a :
∀ j,
∑_{0 ≤ i ≤ t} I[i ≤ t - j] × ℙ<μ>{[ X ⟨=⟩ i ]}
≥ ∑_{0 ≤ i ≤ t} I[i ≤ t - j] × ℙ<μ'>{[ X' ⟨=⟩ i ]}.
Proof.
intros.
erewrite <-cdf_to_sum_of_indicators; last by ssrlia.
erewrite <-cdf_to_sum_of_indicators; last by ssrlia.
by done.
Qed.
Local Proposition addrv_respects_stochastic_order_step_3 :
∑_{0 ≤ j ≤ t} ℙ<μ>{[ Y ⟨=⟩ j ]} × (∑_{0 ≤ i ≤ t} I[i ≤ t - j] × ℙ<μ>{[ X ⟨=⟩ i ]})
≥ ∑_{0 ≤ j ≤ t} ℙ<μ>{[ Y ⟨=⟩ j ]} × (∑_{0 ≤ i ≤ t} I[i ≤ t - j] × ℙ<μ'>{[ X' ⟨=⟩ i ]}).
Proof.
apply Rle_ge, Rle_bigr ⇒ i _.
by apply Rmult_le_compat_l;
[ apply Rge_le, ge_pr_0
| apply Rge_le, addrv_respects_stochastic_order_step_3a].
Qed.
Local Proposition addrv_respects_stochastic_order_step_4 :
∑_{0 ≤ j ≤ t} ℙ<μ>{[ Y ⟨=⟩ j ]} × (∑_{0 ≤ i ≤ t} I[i ≤ t - j] × ℙ<μ'>{[ X' ⟨=⟩ i ]})
= ∑_{0 ≤ i ≤ t} ℙ<μ'>{[ X' ⟨=⟩ i ]} × (∑_{0 ≤ j ≤ t} I[j ≤ t - i] × ℙ<μ>{[ Y ⟨=⟩ j ]}).
Proof.
set F2 := ( fun j ⇒ ∑_{0 ≤ i ≤ t} I[i ≤ t - j] × ℙ<μ'>{[ X' ⟨=⟩ i ]} × ℙ<μ>{[ Y ⟨=⟩ j ]} )%R.
rewrite (eq_big_seq F2); unfold F2; clear F2; last first.
{ intros j INj; rewrite -bigsum_distr.
by apply eq_big_seq ⇒ i INi; rewrite Rmult_comm. }
rewrite exchange_big //=.
apply eq_big_seq ⇒ i INi.
rewrite -bigsum_distr; apply eq_big_seq ⇒ j INj.
rewrite Rmult_assoc Rmult_comm Rmult_assoc; apply Rmult_eq_compat_l.
rewrite Rmult_comm; apply Rmult_eq_compat_r.
move: INi; rewrite mem_iota add0n ltnS ⇒ /andP [_ LEi].
move: INj; rewrite mem_iota add0n ltnS ⇒ /andP [_ LEj].
by rewrite !leq_subRL // addnC.
Qed.
Local Proposition addrv_respects_stochastic_order_step_5a :
∀ i,
∑_{0 ≤ j ≤ t} I[j ≤ t - i] × ℙ<μ>{[ Y ⟨=⟩ j ]}
≥ ∑_{0 ≤ j ≤ t} I[j ≤ t - i] × ℙ<μ'>{[ Y' ⟨=⟩ j ]}.
Proof.
intros.
erewrite <-cdf_to_sum_of_indicators; last by ssrlia.
erewrite <-cdf_to_sum_of_indicators; last by ssrlia.
by done.
Qed.
Local Proposition addrv_respects_stochastic_order_step_5 :
∑_{0 ≤ i ≤ t} ℙ<μ'>{[ X' ⟨=⟩ i ]} × (∑_{0 ≤ j ≤ t} I[j ≤ t - i] × ℙ<μ>{[ Y ⟨=⟩ j ]})
≥ ∑_{0 ≤ i ≤ t} ℙ<μ'>{[ X' ⟨=⟩ i ]} × (∑_{0 ≤ j ≤ t} I[j ≤ t - i] × ℙ<μ'>{[ Y' ⟨=⟩ j ]}).
Proof.
apply Rle_ge, Rle_bigr ⇒ i _.
by apply Rmult_le_compat_l;
[ apply Rge_le, ge_pr_0
| apply Rge_le, addrv_respects_stochastic_order_step_5a].
Qed.
Local Proposition addrv_respects_stochastic_order_step_6 :
∑_{0 ≤ i ≤ t} ℙ<μ'>{[ X' ⟨=⟩ i ]} × (∑_{0 ≤ j ≤ t} I[j ≤ t - i] × ℙ<μ'>{[ Y' ⟨=⟩ j ]})
= ∑_{0 ≤ i ≤ t} ∑_{0 ≤ j ≤ t} I[j ≤ t - i] × ℙ<μ'>{[ X' ⟨=⟩ i ]} × ℙ<μ'>{[ Y' ⟨=⟩ j ]}.
Proof.
symmetry.
rewrite big_seq [in X in _ = X]big_seq; apply eq_bigr ⇒ i IN1.
rewrite -bigsum_distr.
rewrite big_seq [in X in _ = X]big_seq; apply eq_bigr ⇒ j IN2.
rewrite -Rmult_assoc; apply Rmult_eq_compat_r.
by rewrite Rmult_comm.
Qed.
Local Proposition addrv_respects_stochastic_order_step_7 :
∑_{0 ≤ i ≤ t} ∑_{0 ≤ j ≤ t} I[j ≤ t - i] × ℙ<μ'>{[ X' ⟨=⟩ i ]} × ℙ<μ'>{[ Y' ⟨=⟩ j ]}
= ℙ<μ'>{[ X' ⟨+⟩ Y' ⟨<=⟩ t ]}.
Proof.
symmetry; rewrite addrv_leq_decomposition //.
rewrite big_seq [in X in _ = X]big_seq; apply eq_bigr ⇒ i INi.
symmetry; erewrite eq_big_seq; [symmetry | ]; last first.
{ intros j INj; move: INi; rewrite mem_iota add0n ltnS ⇒ /andP [_ LEi].
erewrite Rmult_assoc, Rmult_comm, Rmult_assoc; apply Rmult_eq_compat_l.
by rewrite Rmult_comm; first reflexivity. }
rewrite bigsum_distr bigsum_distr; apply Rmult_eq_compat_l.
by apply bigsum_upper_bound_to_indicator; ssrlia.
Qed.
End AddrvRespectsStochasticOrderHelpers.
Context {Ω} {μ : measure Ω}.
Variables (X Y : nrvar μ).
Hypothesis H_independent : indep2 X Y.
Lemma addrv_comm :
∀ ω, (X ⟨+⟩ Y) ω = (Y ⟨+⟩ X) ω.
Proof. by intros *; rewrite //= addnC. Qed.
Local Proposition addrv_eq_decomposition :
∀ t,
ℙ<μ>{[ X ⟨+⟩ Y ⟨=⟩ t ]}
= ∑_{0 ≤ i ≤ t} ℙ<μ>{[ X ⟨=⟩ i ]} × ℙ<μ>{[ Y ⟨=⟩ (t - i)%N ]}.
Proof.
intros s; unfold "⟨=⟩", nrvar_nat_pred_eqop.
rewrite (@pr_eq_pred'
_ _ _ (fun ω ⇒ has (fun i ⇒ (X ω == i) && (Y ω == s - i)) (index_iota 0 s.+1)))%nat; last first.
{ intros ω; split; [move ⇒ /eqP EQ | intros EQ].
- apply/hasP; ∃ (X ω).
rewrite mem_iota add0n ltnS -EQ; apply/andP; split ⇒ //.
+ by rewrite leq_addr.
+ apply/andP; split; first by done.
by rewrite -EQ //= addKn.
- move: EQ ⇒ /hasP [i IN /andP [/eqP EQ1 /eqP EQ2]].
rewrite //= EQ1 EQ2.
move: IN; rewrite mem_iota add0n ltnS ⇒ /andP [_ LE].
by rewrite subnKC.
}
rewrite union_disj_eq_sum_prob.
- apply eq_bigr ⇒ i _.
by rewrite H_independent.
- by intros *; move ⇒ /andP [/eqP → _] /andP [/eqP → _].
Qed.
Local Proposition addrv_leq_decomposition :
∀ t,
ℙ<μ>{[ X ⟨+⟩ Y ⟨<=⟩ t ]}
= ∑_{0 ≤ i ≤ t} ∑_{0 ≤ j ≤ t - i} ℙ<μ>{[ X ⟨=⟩ i ]} × ℙ<μ>{[ Y ⟨=⟩ j ]}.
Proof.
induction t.
- rewrite !big_nat1 -H_independent; unfold "⟨<=⟩", rvar_nat_pred_leqop.
apply pr_eq_pred' ⇒ ω //=; split; intros EQ.
+ by move: EQ; rewrite leqn0 addn_eq0.
+ by move: EQ ⇒ /andP [/eqP → /eqP ->].
- rewrite big_nat_recr //=.
rewrite subnn big_nat1.
erewrite eq_big_seq; last first.
{ intros i; rewrite mem_iota add0n ltnS ⇒ /andP [_ LEi].
rewrite subSn; last by done.
by rewrite big_nat_recr //=.
}
rewrite //= bigsum_add -IHt.
have EQ := cdf_succ_to_cdf_preq.
unfold cdf in EQ.
rewrite EQ; clear IHt.
rewrite Rplus_assoc; apply Rplus_eq_compat_l.
rewrite addrv_eq_decomposition.
rewrite big_nat_recr //= subnn; apply Rplus_eq_compat_r.
rewrite big_seq [in X in _ = X]big_seq; apply eq_bigr ⇒ i INi.
move: INi; rewrite mem_iota add0n ltnS ⇒ /andP [_ LEi].
by rewrite subSn.
Qed.
End BasicLemmas.
Section StochasticDomination.
Section AddrvRespectsStochasticOrderHelpers.
Context {Ω Ω'} {μ : measure Ω} {μ' : measure Ω'}.
Variables (t : nat) (X Y : nrvar μ) (X' Y' : nrvar μ').
Hypothesis H_dominates_X : X ⪯ X'.
Hypothesis H_dominates_Y : Y ⪯ Y'.
Hypothesis H_independent : indep2 X Y.
Hypothesis H_independent' : indep2 X' Y'.
Local Proposition addrv_respects_stochastic_order_step_1 :
ℙ<μ>{[ X ⟨+⟩ Y ⟨<=⟩ t ]}
= ∑_{0 ≤ i ≤ t} ∑_{0 ≤ j ≤ t} I[i + j ≤ t] × ℙ<μ>{[ X ⟨=⟩ i ]} × ℙ<μ>{[ Y ⟨=⟩ j ]}.
Proof.
rewrite addrv_leq_decomposition //.
rewrite big_seq [in X in _ = X]big_seq; apply eq_bigr ⇒ i INi.
symmetry; erewrite eq_big_seq; [symmetry | ]; last first.
{ intros j INj; move: INi; rewrite mem_iota add0n ltnS ⇒ /andP [_ LEi].
erewrite Rmult_assoc, Rmult_comm, Rmult_assoc; apply Rmult_eq_compat_l.
by rewrite Rmult_comm -leq_subRL; first reflexivity. }
rewrite bigsum_distr bigsum_distr; apply Rmult_eq_compat_l.
by apply bigsum_upper_bound_to_indicator; ssrlia.
Qed.
Local Proposition addrv_respects_stochastic_order_step_2 :
∑_{0 ≤ i ≤ t} ∑_{0 ≤ j ≤ t} I[i + j ≤ t] × ℙ<μ>{[ X ⟨=⟩ i ]} × ℙ<μ>{[ Y ⟨=⟩ j ]}
= ∑_{0 ≤ j ≤ t} ℙ<μ>{[ Y ⟨=⟩ j ]} × (∑_{0 ≤ i ≤ t} I[i ≤ t - j] × ℙ<μ>{[ X ⟨=⟩ i ]}).
Proof.
rewrite exchange_big //=.
rewrite big_seq [in X in _ = X]big_seq; apply eq_bigr ⇒ i IN1.
rewrite -bigsum_distr.
rewrite big_seq [in X in _ = X]big_seq; apply eq_bigr ⇒ j IN2.
rewrite !Rmult_assoc [in X in _ = X]Rmult_comm -!Rmult_assoc.
apply Rmult_eq_compat_r, Rmult_eq_compat_r.
destruct (j + i ≤ t)%nat eqn:LE1.
- by apply leq_subRL_impl in LE1; rewrite LE1.
- move: IN1; rewrite mem_iota add0n ltnS ⇒ /andP [_ LE3].
move: IN2; rewrite mem_iota add0n ltnS ⇒ /andP [_ LE4].
by destruct (j ≤ t - i)%nat eqn:LE2; [ssrlia | reflexivity].
Qed.
Local Proposition addrv_respects_stochastic_order_step_3a :
∀ j,
∑_{0 ≤ i ≤ t} I[i ≤ t - j] × ℙ<μ>{[ X ⟨=⟩ i ]}
≥ ∑_{0 ≤ i ≤ t} I[i ≤ t - j] × ℙ<μ'>{[ X' ⟨=⟩ i ]}.
Proof.
intros.
erewrite <-cdf_to_sum_of_indicators; last by ssrlia.
erewrite <-cdf_to_sum_of_indicators; last by ssrlia.
by done.
Qed.
Local Proposition addrv_respects_stochastic_order_step_3 :
∑_{0 ≤ j ≤ t} ℙ<μ>{[ Y ⟨=⟩ j ]} × (∑_{0 ≤ i ≤ t} I[i ≤ t - j] × ℙ<μ>{[ X ⟨=⟩ i ]})
≥ ∑_{0 ≤ j ≤ t} ℙ<μ>{[ Y ⟨=⟩ j ]} × (∑_{0 ≤ i ≤ t} I[i ≤ t - j] × ℙ<μ'>{[ X' ⟨=⟩ i ]}).
Proof.
apply Rle_ge, Rle_bigr ⇒ i _.
by apply Rmult_le_compat_l;
[ apply Rge_le, ge_pr_0
| apply Rge_le, addrv_respects_stochastic_order_step_3a].
Qed.
Local Proposition addrv_respects_stochastic_order_step_4 :
∑_{0 ≤ j ≤ t} ℙ<μ>{[ Y ⟨=⟩ j ]} × (∑_{0 ≤ i ≤ t} I[i ≤ t - j] × ℙ<μ'>{[ X' ⟨=⟩ i ]})
= ∑_{0 ≤ i ≤ t} ℙ<μ'>{[ X' ⟨=⟩ i ]} × (∑_{0 ≤ j ≤ t} I[j ≤ t - i] × ℙ<μ>{[ Y ⟨=⟩ j ]}).
Proof.
set F2 := ( fun j ⇒ ∑_{0 ≤ i ≤ t} I[i ≤ t - j] × ℙ<μ'>{[ X' ⟨=⟩ i ]} × ℙ<μ>{[ Y ⟨=⟩ j ]} )%R.
rewrite (eq_big_seq F2); unfold F2; clear F2; last first.
{ intros j INj; rewrite -bigsum_distr.
by apply eq_big_seq ⇒ i INi; rewrite Rmult_comm. }
rewrite exchange_big //=.
apply eq_big_seq ⇒ i INi.
rewrite -bigsum_distr; apply eq_big_seq ⇒ j INj.
rewrite Rmult_assoc Rmult_comm Rmult_assoc; apply Rmult_eq_compat_l.
rewrite Rmult_comm; apply Rmult_eq_compat_r.
move: INi; rewrite mem_iota add0n ltnS ⇒ /andP [_ LEi].
move: INj; rewrite mem_iota add0n ltnS ⇒ /andP [_ LEj].
by rewrite !leq_subRL // addnC.
Qed.
Local Proposition addrv_respects_stochastic_order_step_5a :
∀ i,
∑_{0 ≤ j ≤ t} I[j ≤ t - i] × ℙ<μ>{[ Y ⟨=⟩ j ]}
≥ ∑_{0 ≤ j ≤ t} I[j ≤ t - i] × ℙ<μ'>{[ Y' ⟨=⟩ j ]}.
Proof.
intros.
erewrite <-cdf_to_sum_of_indicators; last by ssrlia.
erewrite <-cdf_to_sum_of_indicators; last by ssrlia.
by done.
Qed.
Local Proposition addrv_respects_stochastic_order_step_5 :
∑_{0 ≤ i ≤ t} ℙ<μ'>{[ X' ⟨=⟩ i ]} × (∑_{0 ≤ j ≤ t} I[j ≤ t - i] × ℙ<μ>{[ Y ⟨=⟩ j ]})
≥ ∑_{0 ≤ i ≤ t} ℙ<μ'>{[ X' ⟨=⟩ i ]} × (∑_{0 ≤ j ≤ t} I[j ≤ t - i] × ℙ<μ'>{[ Y' ⟨=⟩ j ]}).
Proof.
apply Rle_ge, Rle_bigr ⇒ i _.
by apply Rmult_le_compat_l;
[ apply Rge_le, ge_pr_0
| apply Rge_le, addrv_respects_stochastic_order_step_5a].
Qed.
Local Proposition addrv_respects_stochastic_order_step_6 :
∑_{0 ≤ i ≤ t} ℙ<μ'>{[ X' ⟨=⟩ i ]} × (∑_{0 ≤ j ≤ t} I[j ≤ t - i] × ℙ<μ'>{[ Y' ⟨=⟩ j ]})
= ∑_{0 ≤ i ≤ t} ∑_{0 ≤ j ≤ t} I[j ≤ t - i] × ℙ<μ'>{[ X' ⟨=⟩ i ]} × ℙ<μ'>{[ Y' ⟨=⟩ j ]}.
Proof.
symmetry.
rewrite big_seq [in X in _ = X]big_seq; apply eq_bigr ⇒ i IN1.
rewrite -bigsum_distr.
rewrite big_seq [in X in _ = X]big_seq; apply eq_bigr ⇒ j IN2.
rewrite -Rmult_assoc; apply Rmult_eq_compat_r.
by rewrite Rmult_comm.
Qed.
Local Proposition addrv_respects_stochastic_order_step_7 :
∑_{0 ≤ i ≤ t} ∑_{0 ≤ j ≤ t} I[j ≤ t - i] × ℙ<μ'>{[ X' ⟨=⟩ i ]} × ℙ<μ'>{[ Y' ⟨=⟩ j ]}
= ℙ<μ'>{[ X' ⟨+⟩ Y' ⟨<=⟩ t ]}.
Proof.
symmetry; rewrite addrv_leq_decomposition //.
rewrite big_seq [in X in _ = X]big_seq; apply eq_bigr ⇒ i INi.
symmetry; erewrite eq_big_seq; [symmetry | ]; last first.
{ intros j INj; move: INi; rewrite mem_iota add0n ltnS ⇒ /andP [_ LEi].
erewrite Rmult_assoc, Rmult_comm, Rmult_assoc; apply Rmult_eq_compat_l.
by rewrite Rmult_comm; first reflexivity. }
rewrite bigsum_distr bigsum_distr; apply Rmult_eq_compat_l.
by apply bigsum_upper_bound_to_indicator; ssrlia.
Qed.
End AddrvRespectsStochasticOrderHelpers.
Consider two probability spaces (Ω,μ) and (Ω',μ') and four
random variables X Y : Ω → nat and X' Y' : Ω' → nat. If X and
Y are independent, X' and Y' are independent, and
furthermore, X is stochastically dominated by X' and Y is
stochastically dominated by Y', then the sum of X and Y is
stochastically dominated by the sum of X' and Y'.
Theorem addrv_respects_stochastic_order :
∀ {Ω Ω'} {μ : measure Ω} {μ' : measure Ω'}
(X Y : nrvar μ) (X' Y' : nrvar μ'),
indep2 X Y → indep2 X' Y' →
X ⪯ X' → Y ⪯ Y' → X ⟨+⟩ Y ⪯ X' ⟨+⟩ Y'.
Proof.
intros × IND1 IND2 LEX LEY n; rewrite /cdf.
erewrite addrv_respects_stochastic_order_step_1; eauto 2.
erewrite addrv_respects_stochastic_order_step_2; eauto 2.
erewrite addrv_respects_stochastic_order_step_3; eauto 2.
erewrite addrv_respects_stochastic_order_step_4; eauto 2.
erewrite addrv_respects_stochastic_order_step_5; eauto 2.
erewrite addrv_respects_stochastic_order_step_6; eauto 2.
erewrite addrv_respects_stochastic_order_step_7; eauto 2.
by apply Rle_ge, Rge_refl.
Qed.
End StochasticDomination.
Section StochasticDominationSum.
Context {Ω1} {μ1 : measure Ω1} {X1 : eqType}.
Variable (F1 : X1 → nrvar μ1) (xs1 : seq X1).
Hypothesis H_independent1 : independent [seq F1 x | x <- xs1].
Context {Ω2} {μ2 : measure Ω2} {X2 : eqType}.
Variable (F2 : X2 → nrvar μ2) (xs2 : seq X2).
Hypothesis H_independent2 : independent [seq F2 x | x <- xs2].
Hypothesis H_eq_size : size xs1 = size xs2.
Hypothesis H_xs2_doms_xs1 : ∀ x y, (x, y) \in zip xs1 xs2 → F1 x ⪯ F2 y.
Lemma sumrv_respects_stochastic_order :
∑[rv]_{ x <- xs1 } F1 x ⪯ ∑[rv]_{ x <- xs2 } F2 x.
Proof.
move: xs2 H_eq_size H_independent2 H_xs2_doms_xs1.
clear H_eq_size H_independent2 H_xs2_doms_xs1.
induction xs1 as [ | y1 ys1].
{ move ⇒ []; last by done.
rewrite !big_nil; intros _ ? ? ?.
by rewrite /cdf !pr_xpredT_ext; first apply Rle_refl.
}
intros [ | y2 ys2]; first by done.
intros SIZE H_independent2 H_dom; simpl in SIZE; apply eq_add_S in SIZE.
rewrite !big_cons; apply addrv_respects_stochastic_order.
{ by apply: indep2_sum_cons; apply H_independent1. }
{ by apply: indep2_sum_cons; apply H_independent2. }
{ by apply H_dom; simpl; rewrite in_cons eq_refl orTb. }
{ apply IHys1.
{ by apply: independent_tl; eassumption. }
{ by done. }
{ by apply: independent_tl; eassumption. }
{ by intros; apply H_dom; rewrite in_cons H orbT. }
}
Qed.
End StochasticDominationSum.
∀ {Ω Ω'} {μ : measure Ω} {μ' : measure Ω'}
(X Y : nrvar μ) (X' Y' : nrvar μ'),
indep2 X Y → indep2 X' Y' →
X ⪯ X' → Y ⪯ Y' → X ⟨+⟩ Y ⪯ X' ⟨+⟩ Y'.
Proof.
intros × IND1 IND2 LEX LEY n; rewrite /cdf.
erewrite addrv_respects_stochastic_order_step_1; eauto 2.
erewrite addrv_respects_stochastic_order_step_2; eauto 2.
erewrite addrv_respects_stochastic_order_step_3; eauto 2.
erewrite addrv_respects_stochastic_order_step_4; eauto 2.
erewrite addrv_respects_stochastic_order_step_5; eauto 2.
erewrite addrv_respects_stochastic_order_step_6; eauto 2.
erewrite addrv_respects_stochastic_order_step_7; eauto 2.
by apply Rle_ge, Rge_refl.
Qed.
End StochasticDomination.
Section StochasticDominationSum.
Context {Ω1} {μ1 : measure Ω1} {X1 : eqType}.
Variable (F1 : X1 → nrvar μ1) (xs1 : seq X1).
Hypothesis H_independent1 : independent [seq F1 x | x <- xs1].
Context {Ω2} {μ2 : measure Ω2} {X2 : eqType}.
Variable (F2 : X2 → nrvar μ2) (xs2 : seq X2).
Hypothesis H_independent2 : independent [seq F2 x | x <- xs2].
Hypothesis H_eq_size : size xs1 = size xs2.
Hypothesis H_xs2_doms_xs1 : ∀ x y, (x, y) \in zip xs1 xs2 → F1 x ⪯ F2 y.
Lemma sumrv_respects_stochastic_order :
∑[rv]_{ x <- xs1 } F1 x ⪯ ∑[rv]_{ x <- xs2 } F2 x.
Proof.
move: xs2 H_eq_size H_independent2 H_xs2_doms_xs1.
clear H_eq_size H_independent2 H_xs2_doms_xs1.
induction xs1 as [ | y1 ys1].
{ move ⇒ []; last by done.
rewrite !big_nil; intros _ ? ? ?.
by rewrite /cdf !pr_xpredT_ext; first apply Rle_refl.
}
intros [ | y2 ys2]; first by done.
intros SIZE H_independent2 H_dom; simpl in SIZE; apply eq_add_S in SIZE.
rewrite !big_cons; apply addrv_respects_stochastic_order.
{ by apply: indep2_sum_cons; apply H_independent1. }
{ by apply: indep2_sum_cons; apply H_independent2. }
{ by apply H_dom; simpl; rewrite in_cons eq_refl orTb. }
{ apply IHys1.
{ by apply: independent_tl; eassumption. }
{ by done. }
{ by apply: independent_tl; eassumption. }
{ by intros; apply H_dom; rewrite in_cons H orbT. }
}
Qed.
End StochasticDominationSum.