# Sums of natural numbers

Content created by Egbert Rijke, Fredrik Bakke and Jonathan Prieto-Cubides.

Created on 2022-02-10.

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.action-on-identifications-functions
open import foundation.constant-maps
open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.unit-type
open import foundation.universe-levels
open import foundation.whiskering-homotopies

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 ℕ → ℕ


### 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 =
( 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 =
( 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-ℕ!}