Reference · Finite sums

rainbow.math.sums.earliest-schedule

Finite sumssrc/rainbow/math/sums/earliest_schedule.clj1 definitions, 6 theorems

The earliest-start recurrence preserves feasibility whenever any window schedule exists.

Depends onmath.sums.nonblockingmath.nat.at-most-cancellationalgorithms.proofs.graph.walk-shorten

signed/earliest-window-start :
  (x₁ x₂ : ℕ → ℚ) (x₃ : ℕ)
  → ℚ

signed/maximum-at-least-left :
  (x y : ℚ)
  → x ≤ data/Bool.rec (fun x₄ => ℚ) x y (signed/decide-at-most x y)

signed/maximum-at-least-right :
  (x y : ℚ)
  → y ≤ data/Bool.rec (fun x₄ => ℚ) x y (signed/decide-at-most x y)

signed/maximum-below-common-upper :
  (x y z : ℚ)
  (left : x ≤ z)
  (right : y ≤ z)
  → data/Bool.rec (fun x₄ => ℚ) x y (signed/decide-at-most x y) ≤ z

signed/earliest-start-above-opening :
  (A D : ℕ → ℚ) (k : ℕ)
  → A k ≤ signed/earliest-window-start A D k

signed/earliest-start-no-later-than-feasible :
  (A D T : ℕ → ℚ) (q : ℕ)
  (lower : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx (data/succ q)), A idx ≤ T idx)
  (progress : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx q), T idx + D idx ≤ T (data/succ idx))
  (k : ℕ) (bound : nat/strict-below k (data/succ q))
  → signed/earliest-window-start A D k ≤ T k

signed/earliest-start-preserves-feasibility :
  (A B D T : ℕ → ℚ) (q : ℕ)
  (feasible : proposition/conjunction (∀ (idx : ℕ), ∀ (bound : nat/strict-below idx (data/succ q)), A idx ≤ T idx) (conjunction₁))
  → proposition/conjunction (∀ (idx : ℕ), ∀ (bound : nat/strict-below idx (data/succ q)), A idx ≤ (fun position17217 => signed/earliest-window-start A D position17217) idx) (conjunction)
  where conjunction := proposition/conjunction (∀ (idx : ℕ), ∀ (bound : nat/strict-below idx (data/succ q)), (fun position17217 => signed/earliest-window-start A D position17217) idx ≤ B idx) (∀ (idx : ℕ), ∀ (bound : nat/strict-below idx q), (fun position17217 => signed/earliest-window-start A D position17217) idx + D idx ≤ (fun position17217 => signed/earliest-window-start A D position17217) (data/succ idx))
  where conjunction₁ := proposition/conjunction (∀ (idx : ℕ), ∀ (bound : nat/strict-below idx (data/succ q)), T idx ≤ B idx) (∀ (idx : ℕ), ∀ (bound : nat/strict-below idx q), T idx + D idx ≤ T (data/succ idx))