Sums of natural numbers

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

Created on 2022-02-10.
Last modified on 2024-04-11.

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-composition

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-ℕ!}

Recent changes