Reference · Finite sums

rainbow.math.sums.value-algebra

Finite sumssrc/rainbow/math/sums/value_algebra.clj0 definitions, 11 theorems

Finite-sum algebra for the existing signed/expr-sum-value. All regrouping uses signed/equivalent (Grothendieck equality), never equality of raw pairs. Bounds and congruences require hypotheses only below the finite bound.

Depends onmath.checksmath.rational.signed.map-sum-algebramath.rational.signed.distributivemath.rational.signed.equivalence-lawsmath.rational.signed.fubinimath.rational.signed.pointwise-order

signed/expr-sum-value-as-map-sum :
  (F : ℕ → ℚ) (n : ℕ)
  → signed/expr-sum-value F n = Σ j∈list/nat-range n, F j

signed/expr-sum-bounds-as-list :
  (F G : ℕ → ℚ) (n : ℕ)
  (H : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), F idx ≤ G idx)
  → ∀ i ∈ list/nat-range n, F i ≤ G i

signed/expr-sum-value-zero :
  (n : ℕ)
  → signed/expr-sum-value (fun x₂ => 0) n = 0

signed/expr-sum-value-add :
  (F G : ℕ → ℚ) (n : ℕ)
  → signed/expr-sum-value (fun i => F i + G i) n = signed/expr-sum-value F n + signed/expr-sum-value G n

signed/expr-sum-value-scale-right :
  (F : ℕ → ℚ) (c : ℚ) (n : ℕ)
  → signed/expr-sum-value F n · c = signed/expr-sum-value (fun i => F i · c) n

signed/expr-sum-value-monotone-below :
  (F G : ℕ → ℚ) (n : ℕ)
  (H : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), F idx ≤ G idx)
  → signed/expr-sum-value F n ≤ signed/expr-sum-value G n

signed/expr-sum-value-respects-equivalence-below :
  (F G : ℕ → ℚ) (n : ℕ)
  (H : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), F idx = G idx)
  → signed/expr-sum-value F n = signed/expr-sum-value G n

signed/expr-sum-value-scale-left :
  (F : ℕ → ℚ) (c : ℚ) (n : ℕ)
  → c · signed/expr-sum-value F n = signed/expr-sum-value (fun i => c · F i) n

signed/expr-sum-value-weighted-monotone-left :
  (W F G : ℕ → ℚ) (n : ℕ)
  (hw : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), 0 ≤ W idx)
  (hfg : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), F idx ≤ G idx)
  → signed/expr-sum-value (fun i => W i · F i) n ≤ signed/expr-sum-value (fun i => W i · G i) n

signed/expr-sum-value-weighted-monotone-right :
  (W F G : ℕ → ℚ) (n : ℕ)
  (hw : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), 0 ≤ W idx)
  (hfg : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), F idx ≤ G idx)
  → signed/expr-sum-value (fun i => F i · W i) n ≤ signed/expr-sum-value (fun i => G i · W i) n

signed/expr-sum-value-swap :
  (F : ℕ → ℕ → ℚ) (n m : ℕ)
  → signed/expr-sum-value (fun i => signed/expr-sum-value (fun j => F i j) n) m = signed/expr-sum-value (fun j => signed/expr-sum-value (fun i => F i j) m) n