Reference · Finite sums

rainbow.math.sums.triangular

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

Triangular decomposition for the existing finite sums; prefix completion costs. Pure algebra, with no schedule or permutation assumptions.

Depends onmath.sums.flow-cut

signed/expr-sum-square-successor :
  (tr-matrix : ℕ → ℕ → ℚ) (tr-size : ℕ)
  → signed/expr-sum-value (fun tr-outer => signed/expr-sum-value (fun tr-col => tr-matrix tr-outer tr-col) (data/succ tr-size)) (data/succ tr-size) = signed/expr-sum-value (fun tr-outer => signed/expr-sum-value (fun tr-col => tr-matrix tr-outer tr-col) tr-size) tr-size + signed/expr-sum-value (fun tr-col => tr-matrix tr-size tr-col) tr-size + (signed/expr-sum-value (fun tr-row => tr-matrix tr-row tr-size) tr-size + tr-matrix tr-size tr-size)

signed/expr-sum-square-triangular-decomposition :
  (tr-matrix : ℕ → ℕ → ℚ) (tr-size : ℕ)
  → signed/expr-sum-value (fun tr-outer => signed/expr-sum-value (fun tr-col => tr-matrix tr-outer tr-col) tr-size) tr-size = signed/expr-sum-value (fun tr-later => signed/expr-sum-value (fun tr-row => tr-matrix tr-row tr-later) tr-later) tr-size + signed/expr-sum-value (fun tr-later => signed/expr-sum-value (fun tr-row => (fun tr-a => fun tr-b => tr-matrix tr-b tr-a) tr-row tr-later) tr-later) tr-size + signed/expr-sum-value (fun tr-diag => tr-matrix tr-diag tr-diag) tr-size

signed/expr-sum-symmetric-triangular :
  (tr-matrix : ℕ → ℕ → ℚ) (tr-size : ℕ)
  (tr-symmetric : ∀ (tr-i : ℕ), ∀ (tr-ib : nat/strict-below tr-i tr-size), ∀ (tr-j : ℕ), ∀ (tr-jb : nat/strict-below tr-j tr-size), tr-matrix tr-i tr-j = tr-matrix tr-j tr-i)
  → signed/expr-sum-value (fun tr-outer => signed/expr-sum-value (fun tr-col => tr-matrix tr-outer tr-col) tr-size) tr-size = value + value + signed/expr-sum-value (fun tr-diag => tr-matrix tr-diag tr-diag) tr-size
  where value := signed/expr-sum-value (fun tr-later => signed/expr-sum-value (fun tr-row => tr-matrix tr-row tr-later) tr-later) tr-size

signed/expr-sum-prefix-completion-cost :
  (tr-times tr-weights : ℕ → ℚ) (tr-size : ℕ)
  → signed/expr-sum-value (fun tr-position => tr-weights tr-position · signed/expr-sum-value tr-times (data/succ tr-position)) tr-size = signed/expr-sum-value (fun tr-later => signed/expr-sum-value (fun tr-row => (fun tr-p => fun tr-w => tr-times tr-p · tr-weights tr-w) tr-row tr-later) tr-later) tr-size + signed/expr-sum-value (fun tr-diag => (fun tr-p => fun tr-w => tr-times tr-p · tr-weights tr-w) tr-diag tr-diag) tr-size