Sums of natural numbers

module elementary-number-theory.sums-of-natural-numbers where
Imports
open import elementary-number-theory.addition-natural-numbers
open import elementary-number-theory.multiplication-natural-numbers
open import elementary-number-theory.natural-numbers
open import elementary-number-theory.strict-inequality-natural-numbers

open import foundation.constant-maps
open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.functions
open import foundation.homotopies
open import foundation.identity-types
open import foundation.unit-type
open import foundation.universe-levels

open import lists.lists

open import univalent-combinatorics.counting
open import univalent-combinatorics.standard-finite-types

Idea

The values of a map f : X → ℕ out of a finite type X can be summed up.

Definition

Sums of lists of natural numbers

sum-list-ℕ : list   
sum-list-ℕ = fold-list 0 add-ℕ

Sums of natural numbers indexed by a standard finite type

sum-Fin-ℕ : (k : )  (Fin k  )  
sum-Fin-ℕ zero-ℕ f = zero-ℕ
sum-Fin-ℕ (succ-ℕ k) f = (sum-Fin-ℕ k  x  f (inl x))) +ℕ (f (inr star))

Sums of natural numbers indexed by a type equipped with a counting

sum-count-ℕ : {l : Level} {A : UU l} (e : count A)  (f : A  )  
sum-count-ℕ (pair k e) f = sum-Fin-ℕ k (f  (map-equiv e))

Bounded sums of natural numbers

bounded-sum-ℕ : (u : )  ((x : )  le-ℕ x u  )  
bounded-sum-ℕ zero-ℕ f = zero-ℕ
bounded-sum-ℕ (succ-ℕ u) f =
  add-ℕ
    ( bounded-sum-ℕ u  x H  f x (preserves-le-succ-ℕ x u H)))
    ( f u (succ-le-ℕ u))

Properties

Sums are invariant under homotopy

abstract
  htpy-sum-Fin-ℕ :
    (k : ) {f g : Fin k  } (H : f ~ g)  sum-Fin-ℕ k f  sum-Fin-ℕ k g
  htpy-sum-Fin-ℕ zero-ℕ H = refl
  htpy-sum-Fin-ℕ (succ-ℕ k) H =
    ap-add-ℕ
      ( htpy-sum-Fin-ℕ k  x  H (inl x)))
      ( H (inr star))

abstract
  htpy-sum-count-ℕ :
    {l : Level} {A : UU l} (e : count A) {f g : A  } (H : f ~ g) 
    sum-count-ℕ e f  sum-count-ℕ e g
  htpy-sum-count-ℕ (pair k e) H = htpy-sum-Fin-ℕ k (H ·r (map-equiv e))

Summing up the same value m times is multiplication by m

abstract
  constant-sum-Fin-ℕ :
    (m n : )  sum-Fin-ℕ m (const (Fin m)  n)  m *ℕ n
  constant-sum-Fin-ℕ zero-ℕ n = refl
  constant-sum-Fin-ℕ (succ-ℕ m) n = ap (_+ℕ n) (constant-sum-Fin-ℕ m n)

abstract
  constant-sum-count-ℕ :
    {l : Level} {A : UU l} (e : count A) (n : ) 
    sum-count-ℕ e (const A  n)  (number-of-elements-count e) *ℕ n
  constant-sum-count-ℕ (pair m e) n = constant-sum-Fin-ℕ m n

Each of the summands is less than or equal to the total sum

-- leq-sum-Fin-ℕ :
--   {k : ℕ} (f : Fin k → ℕ) (x : Fin k) → leq-ℕ (f x) (sum-Fin-ℕ f)
-- leq-sum-Fin-ℕ {succ-ℕ k} f x = {!leq-add-ℕ!}