Reference · Finite sums

rainbow.math.sums.wspt-pair-bound

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

Pairwise lower bound for a prefix completion objective, exact for sorted pairs. Generic finite sequences only; the permutation bridge is separate.

signed/wspt-min-respects-equivalence :
  (pb-a pb-b pb-c pb-d : ℚ)
  (pb-ac : pb-a = pb-c)
  (pb-bd : pb-b = pb-d)
  → signed/min pb-a pb-b = signed/min pb-c pb-d

signed/wspt-pair-expression-decomposition :
  (pb-times pb-weights : ℕ → ℚ) (pb-size : ℕ)
  → value₁ + signed/expr-sum-value (fun tr-outer => signed/expr-sum-value (fun tr-col => (fun pb-i => fun pb-j => signed/min (pb-times pb-i · pb-weights pb-j) (pb-times pb-j · pb-weights pb-i)) tr-outer tr-col) pb-size) pb-size = value + value₁ + (value + value₁)
  where value := signed/expr-sum-value (fun tr-later => signed/expr-sum-value (fun tr-row => (fun pb-i => fun pb-j => signed/min (pb-times pb-i · pb-weights pb-j) (pb-times pb-j · pb-weights pb-i)) tr-row tr-later) tr-later) pb-size
  where value₁ := signed/expr-sum-value (fun tr-diag => (fun tr-p => fun tr-w => pb-times tr-p · pb-weights tr-w) tr-diag tr-diag) pb-size

signed/wspt-pair-expression-lower-bound :
  (pb-times pb-weights : ℕ → ℚ) (pb-size : ℕ)
  → signed/expr-sum-value (fun tr-diag => (fun tr-p => fun tr-w => pb-times tr-p · pb-weights tr-w) tr-diag tr-diag) pb-size + signed/expr-sum-value (fun tr-outer => signed/expr-sum-value (fun tr-col => (fun pb-i => fun pb-j => signed/min (pb-times pb-i · pb-weights pb-j) (pb-times pb-j · pb-weights pb-i)) tr-outer tr-col) pb-size) pb-size ≤ value + value
  where value := signed/expr-sum-value (fun tr-position => pb-weights tr-position · signed/expr-sum-value pb-times (data/succ tr-position)) pb-size

signed/wspt-sorted-attains-pair-expression :
  (pb-times pb-weights : ℕ → ℚ) (pb-size : ℕ)
  (pb-ordered : ∀ (pb-later : ℕ), ∀ (pb-later-bound : nat/strict-below pb-later pb-size), ∀ (pb-earlier : ℕ), ∀ (pb-earlier-bound : nat/strict-below pb-earlier pb-later), pb-times pb-earlier · pb-weights pb-later ≤ pb-times pb-later · pb-weights pb-earlier)
  → signed/expr-sum-value (fun tr-diag => (fun tr-p => fun tr-w => pb-times tr-p · pb-weights tr-w) tr-diag tr-diag) pb-size + signed/expr-sum-value (fun tr-outer => signed/expr-sum-value (fun tr-col => (fun pb-i => fun pb-j => signed/min (pb-times pb-i · pb-weights pb-j) (pb-times pb-j · pb-weights pb-i)) tr-outer tr-col) pb-size) pb-size = value + value
  where value := signed/expr-sum-value (fun tr-position => pb-weights tr-position · signed/expr-sum-value pb-times (data/succ tr-position)) pb-size