Reference · Finite sums

rainbow.math.sums.wspt-permutation

Finite sumssrc/rainbow/math/sums/wspt_permutation.clj0 definitions, 4 theorems

WSPT optimality over all permutation matrices, with positive processing times. Pairwise and prefix quantities use the existing expr-sum-value throughout.

signed/wspt-permutation-diagonal-invariant :
  (wp-X : ℕ → ℕ → ℚ) (wp-P wp-W : ℕ → ℚ) (wp-n : ℕ)
  (wp-permutation : proposition/conjunction (∀ (pi-row : ℕ), ∀ (pi-rb : nat/strict-below pi-row wp-n), ∀ (pi-col : ℕ), ∀ (pi-cb : nat/strict-below pi-col wp-n), proposition/disjunction (wp-X pi-row pi-col = 0) (wp-X pi-row pi-col = 1)) (conjunction))
  → signed/expr-sum-value (fun tr-diag => (fun tr-p => fun tr-w => (fun pi-position => signed/expr-sum-value (fun pi-job => (fun pi-job₁ => …⟨1⟩ …⟨1⟩ …⟨1⟩) pi-job · wp-P pi-job) wp-n) tr-p · (fun pi-position => signed/expr-sum-value (fun pi-job => (fun pi-job₁ => …⟨1⟩ …⟨1⟩ …⟨1⟩) pi-job · wp-W pi-job) wp-n) tr-w) tr-diag tr-diag) wp-n = signed/expr-sum-value (fun tr-diag => (fun tr-p => fun tr-w => wp-P tr-p · wp-W tr-w) tr-diag tr-diag) wp-n
  where conjunction := proposition/conjunction (∀ (idx : ℕ), ∀ (bound : nat/strict-below idx wp-n), signed/expr-sum-value (fun rj => wp-X idx rj) wp-n = 1) (∀ (idx : ℕ), ∀ (bound : nat/strict-below idx wp-n), signed/expr-sum-value (fun ci => wp-X ci idx) wp-n = 1)

signed/wspt-permutation-pair-sum-invariant :
  (wp-X : ℕ → ℕ → ℚ) (wp-P wp-W : ℕ → ℚ) (wp-n : ℕ)
  (wp-permutation : proposition/conjunction (∀ (pi-row : ℕ), ∀ (pi-rb : nat/strict-below pi-row wp-n), ∀ (pi-col : ℕ), ∀ (pi-cb : nat/strict-below pi-col wp-n), proposition/disjunction (wp-X pi-row pi-col = 0) (wp-X pi-row pi-col = 1)) (conjunction))
  → signed/expr-sum-value (fun tr-outer => signed/expr-sum-value (fun tr-col => (fun pb-i => fun pb-j => signed/min ((fun pi-position => signed/expr-sum-value (fun pi-job => …⟨9⟩ · …⟨3⟩) wp-n) pb-i · (fun pi-position => signed/expr-sum-value (fun pi-job => …⟨9⟩ · …⟨3⟩) wp-n) pb-j) ((fun pi-position => signed/expr-sum-value (fun pi-job => …⟨9⟩ · …⟨3⟩) wp-n) pb-j · (fun pi-position => signed/expr-sum-value (fun pi-job => …⟨9⟩ · …⟨3⟩) wp-n) pb-i)) tr-outer tr-col) wp-n) wp-n = signed/expr-sum-value (fun tr-outer => signed/expr-sum-value (fun tr-col => (fun pb-i => fun pb-j => signed/min (wp-P pb-i · wp-W pb-j) (wp-P pb-j · wp-W pb-i)) tr-outer tr-col) wp-n) wp-n
  where conjunction := proposition/conjunction (∀ (idx : ℕ), ∀ (bound : nat/strict-below idx wp-n), signed/expr-sum-value (fun rj => wp-X idx rj) wp-n = 1) (∀ (idx : ℕ), ∀ (bound : nat/strict-below idx wp-n), signed/expr-sum-value (fun ci => wp-X ci idx) wp-n = 1)

signed/wspt-permutation-processing-positive :
  (wp-X : ℕ → ℕ → ℚ) (wp-P : ℕ → ℚ) (wp-n : ℕ)
  (wp-permutation : proposition/conjunction (∀ (pi-row : ℕ), ∀ (pi-rb : nat/strict-below pi-row wp-n), ∀ (pi-col : ℕ), ∀ (pi-cb : nat/strict-below pi-col wp-n), proposition/disjunction (wp-X pi-row pi-col = 0) (wp-X pi-row pi-col = 1)) (conjunction))
  (wp-positive : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx wp-n), 0 < wp-P idx)
  (idx : ℕ) (bound : nat/strict-below idx wp-n)
  → 0 < (fun pi-position => signed/expr-sum-value (fun pi-job => (fun pi-job₁ => wp-X pi-job₁ pi-position) pi-job · wp-P pi-job) wp-n) idx
  where conjunction := proposition/conjunction (∀ (idx : ℕ), ∀ (bound : nat/strict-below idx wp-n), signed/expr-sum-value (fun rj => wp-X idx rj) wp-n = 1) (∀ (idx : ℕ), ∀ (bound : nat/strict-below idx wp-n), signed/expr-sum-value (fun ci => wp-X ci idx) wp-n = 1)

signed/wspt-permutation-cost-optimal :
  (wp-P wp-W : ℕ → ℚ) (wp-X wp-Y : ℕ → ℕ → ℚ) (wp-count-predecessor : ℕ)
  (wp-positive : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx (data/succ wp-count-predecessor)), 0 < wp-P idx)
  (wp-X-permutation : proposition/conjunction (∀ (pi-row : ℕ), ∀ (pi-rb : nat/strict-below pi-row (data/succ wp-count-predecessor)), ∀ (pi-col : ℕ), ∀ (pi-cb : nat/strict-below pi-col (data/succ wp-count-predecessor)), proposition/disjunction (wp-X pi-row pi-col = 0) (wp-X pi-row pi-col = 1)) (conjunction))
  (wp-adjacent : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx wp-count-predecessor), (fun pi-position => signed/expr-sum-value (fun pi-job => (fun pi-job₁ => wp-X pi-job₁ pi-position) pi-job · wp-W pi-job) (data/succ wp-count-predecessor)) (data/succ idx) · (fun pi-position => signed/expr-sum-value (fun pi-job => (fun pi-job₁ => wp-X pi-job₁ pi-position) pi-job · wp-P pi-job) (data/succ wp-count-predecessor)) idx ≤ (fun pi-position => signed/expr-sum-value (fun pi-job => (fun pi-job₁ => wp-X pi-job₁ pi-position) pi-job · wp-W pi-job) (data/succ wp-count-predecessor)) idx · (fun pi-position => signed/expr-sum-value (fun pi-job => (fun pi-job₁ => wp-X pi-job₁ pi-position) pi-job · wp-P pi-job) (data/succ wp-count-predecessor)) (data/succ idx))
  (wp-Y-permutation : proposition/conjunction (∀ (pi-row : ℕ), ∀ (pi-rb : nat/strict-below pi-row (data/succ wp-count-predecessor)), ∀ (pi-col : ℕ), ∀ (pi-cb : nat/strict-below pi-col (data/succ wp-count-predecessor)), proposition/disjunction (wp-Y pi-row pi-col = 0) (wp-Y pi-row pi-col = 1)) (conjunction₁))
  → signed/expr-sum-value (fun tr-position => (fun pi-position => signed/expr-sum-value (fun pi-job => (fun pi-job₁ => wp-X pi-job₁ pi-position) pi-job · wp-W pi-job) (data/succ wp-count-predecessor)) tr-position · signed/expr-sum-value (fun pi-position => signed/expr-sum-value (fun pi-job => (fun pi-job₁ => wp-X pi-job₁ pi-position) pi-job · wp-P pi-job) (data/succ wp-count-predecessor)) (data/succ tr-position)) (data/succ wp-count-predecessor) ≤ signed/expr-sum-value (fun tr-position => (fun pi-position => signed/expr-sum-value (fun pi-job => (fun pi-job₁ => wp-Y pi-job₁ pi-position) pi-job · wp-W pi-job) (data/succ wp-count-predecessor)) tr-position · signed/expr-sum-value (fun pi-position => signed/expr-sum-value (fun pi-job => (fun pi-job₁ => wp-Y pi-job₁ pi-position) pi-job · wp-P pi-job) (data/succ wp-count-predecessor)) (data/succ tr-position)) (data/succ wp-count-predecessor)
  where conjunction := proposition/conjunction (∀ (idx : ℕ), ∀ (bound : nat/strict-below idx (data/succ wp-count-predecessor)), signed/expr-sum-value (fun rj => wp-X idx rj) (data/succ wp-count-predecessor) = 1) (∀ (idx : ℕ), ∀ (bound : nat/strict-below idx (data/succ wp-count-predecessor)), signed/expr-sum-value (fun ci => wp-X ci idx) (data/succ wp-count-predecessor) = 1)
  where conjunction₁ := proposition/conjunction (∀ (idx : ℕ), ∀ (bound : nat/strict-below idx (data/succ wp-count-predecessor)), signed/expr-sum-value (fun rj => wp-Y idx rj) (data/succ wp-count-predecessor) = 1) (∀ (idx : ℕ), ∀ (bound : nat/strict-below idx (data/succ wp-count-predecessor)), signed/expr-sum-value (fun ci => wp-Y ci idx) (data/succ wp-count-predecessor) = 1)