Library probsa.rt.analysis.arrivals

From prosa.model Require Import task.arrival.curves.
From prosa.analysis Require Export facts.behavior.arrivals.

From probsa.probability Require Export law_of_total_prob.
From probsa.rt.model Require Export events.

Local Open Scope nat_scope.

Section PrArrivalLemmas.

Consider a system that is described by a sample space Ω and a probability measure μ.

Variables (Ω : _) (μ : measure Ω).

Consider any type of tasks and their jobs.

  Context {Task : TaskType}
          {α : MaxArrivals Task}.

  Context {Job : finType}
          {job_cost : JobCostRV Job Ω μ}
          {job_arrival : JobArrivalRV Job Ω μ}
          {job_task : JobTask Job Task}.

Consider an arbitrary task set ts...

Variable ts : seq Task.

... and a task tsk ∈ ts.

Variable tsk : Task.
Hypothesis H_tsk_in_ts : tsk \in ts.

Let ξpart denote a partition of Ω into sets corresponding to different arrival sequences...

Let ξpart := partition_on_ξ μ : Ω_partition.

... and let ξ denote a positive-probability element of such a partition.

  Variable ξ : I ξpart.
  Context {ρ : PosProb μ (ξpart ◁{ξ })}.

  Lemma pr_arrivals_between_eq :
    ∀ (t1 t2 : instant) (ω1 ω2 : Ω),
      ξpart ◁{ξ } ω1 →
      ξpart ◁{ξ } ω2 →
      pr_arrivals_between t1 t2 ω1 = pr_arrivals_between t1 t2 ω2.

  Lemma pr_arrivals_task_between_eq :
    ∀ (t1 t2 : instant) (ω1 ω2 : Ω),
      ξpart ◁{ξ } ω1 →
      ξpart ◁{ξ } ω2 →
      pr_arrivals_task_between tsk t1 t2 ω1 = pr_arrivals_task_between tsk t1 t2 ω2.

  Lemma pr_arrivals_between_fixed_in_partition :
    ∀ (t1 t2 : instant),
    ∃ (jobs : seq Job ), ∀ (ω : Ω),
      ξpart ◁{ξ } ω →
      [seq x <- arrivals_between (arr_seq ω) t1 t2 | job_of_task tsk x] = jobs.

  Hypothesis H_respects_arrival_curve :
    ∀ ω, taskset_respects_max_arrivals (arr_seq ω) ts.

  Hypothesis H_valid_arrival_curve :
    valid_taskset_arrival_curve ts α.

  Lemma pr_arrivals_task_between_respect_arrival_curve :
    ∀ (t1 t2 : instant) (ω : Ω),
      size (pr_arrivals_task_between tsk t1 t2 ω) ≤ α tsk (t2 - t1).
  Corollary pr_arrivals_task_between_respect_arrival_curve_mid :
    ∀ (t1 t2 A : instant) (ω : Ω),
      size (pr_arrivals_task_between tsk (A - t1) (A + t2) ω) ≤ α tsk (t1 + t2).
End PrArrivalLemmas.