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) ω.
Local Proposition addrv_eq_decomposition :
∀ t,
ℙ<μ>{[ X ⟨+⟩ Y ⟨=⟩ t ]}
= ∑_{0 ≤ i ≤ t} ℙ<μ>{[ X ⟨=⟩ i ]} × ℙ<μ>{[ Y ⟨=⟩ (t - i)%N ]}.
Local Proposition addrv_leq_decomposition :
∀ t,
ℙ<μ>{[ X ⟨+⟩ Y ⟨<=⟩ t ]}
= ∑_{0 ≤ i ≤ t} ∑_{0 ≤ j ≤ t - i} ℙ<μ>{[ X ⟨=⟩ i ]} × ℙ<μ>{[ Y ⟨=⟩ j ]}.
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 ]}.
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 ]}).
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 ]}.
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 ]}).
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 ]}).
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 ]}.
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 ]}).
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 ]}.
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 ]}.
End AddrvRespectsStochasticOrderHelpers.
Context {Ω} {μ : measure Ω}.
Variables (X Y : nrvar μ).
Hypothesis H_independent : indep2 X Y.
Lemma addrv_comm :
∀ ω, (X ⟨+⟩ Y) ω = (Y ⟨+⟩ X) ω.
Local Proposition addrv_eq_decomposition :
∀ t,
ℙ<μ>{[ X ⟨+⟩ Y ⟨=⟩ t ]}
= ∑_{0 ≤ i ≤ t} ℙ<μ>{[ X ⟨=⟩ i ]} × ℙ<μ>{[ Y ⟨=⟩ (t - i)%N ]}.
Local Proposition addrv_leq_decomposition :
∀ t,
ℙ<μ>{[ X ⟨+⟩ Y ⟨<=⟩ t ]}
= ∑_{0 ≤ i ≤ t} ∑_{0 ≤ j ≤ t - i} ℙ<μ>{[ X ⟨=⟩ i ]} × ℙ<μ>{[ Y ⟨=⟩ j ]}.
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 ]}.
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 ]}).
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 ]}.
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 ]}).
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 ]}).
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 ]}.
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 ]}).
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 ]}.
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 ]}.
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'.
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.
End StochasticDominationSum.
∀ {Ω Ω'} {μ : measure Ω} {μ' : measure Ω'}
(X Y : nrvar μ) (X' Y' : nrvar μ'),
indep2 X Y → indep2 X' Y' →
X ⪯ X' → Y ⪯ Y' → X ⟨+⟩ Y ⪯ X' ⟨+⟩ Y'.
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.
End StochasticDominationSum.