Library probsa.probability.stochastic_order

(* -------------------------------- Coq-Proba ------------------------------- *)
From discprob.prob Require Export indep.

(* ---------------------------------- Prosa --------------------------------- *)
Require Export prosa.util.all.

(* --------------------------------- ProBsa --------------------------------- *)
From probsa.util Require Export bigop iota.
From probsa.probability Require Export conditional dominance_relation.

(* ---------------------------------- Main ---------------------------------- *)

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

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

  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.