Bounded sums of arithmetic functions

module elementary-number-theory.bounded-sums-arithmetic-functions where
Imports
open import elementary-number-theory.arithmetic-functions
open import elementary-number-theory.natural-numbers
open import elementary-number-theory.nonzero-natural-numbers

open import foundation.coproduct-types
open import foundation.decidable-propositions
open import foundation.decidable-types
open import foundation.functions
open import foundation.universe-levels

open import ring-theory.rings

Idea

Given a decidable predicate P on the nonzero natural numbers, and a map f from the nonzero natural numbers in P into a ring R, the bounded sum is a summation of the values of f up to an upper bound b.

Definition

module _
  {l : Level} (R : Ring l)
  where

  restricted-arithmetic-function-Ring :
    {l' : Level} (P : nonzero-ℕ  Decidable-Prop l')  UU (l  l')
  restricted-arithmetic-function-Ring P =
    (x : nonzero-ℕ)  type-Decidable-Prop (P x)  type-Ring R

  shift-arithmetic-function-Ring :
    type-arithmetic-functions-Ring R  type-arithmetic-functions-Ring R
  shift-arithmetic-function-Ring f = f  succ-nonzero-ℕ

  shift-restricted-arithmetic-function-Ring :
    {l' : Level} (P : nonzero-ℕ  Decidable-Prop l') 
    restricted-arithmetic-function-Ring P 
    restricted-arithmetic-function-Ring (P  succ-nonzero-ℕ)
  shift-restricted-arithmetic-function-Ring P f = f  succ-nonzero-ℕ

  case-one-bounded-sum-arithmetic-function-Ring :
    {l' : Level}  (P : Decidable-Prop l') 
    is-decidable (type-Decidable-Prop P) 
    (type-Decidable-Prop P  type-Ring R)  type-Ring R
  case-one-bounded-sum-arithmetic-function-Ring P (inl x) f = f x
  case-one-bounded-sum-arithmetic-function-Ring P (inr x) f =
    zero-Ring R

  bounded-sum-arithmetic-function-Ring :
    (b : ) {l' : Level} (P : nonzero-ℕ  Decidable-Prop l')
    (f : restricted-arithmetic-function-Ring P)  type-Ring R
  bounded-sum-arithmetic-function-Ring zero-ℕ P f = zero-Ring R
  bounded-sum-arithmetic-function-Ring (succ-ℕ zero-ℕ) P f =
    case-one-bounded-sum-arithmetic-function-Ring
      ( P one-nonzero-ℕ)
      ( is-decidable-Decidable-Prop (P one-nonzero-ℕ))
      ( f one-nonzero-ℕ)
  bounded-sum-arithmetic-function-Ring (succ-ℕ (succ-ℕ b)) P f =
    add-Ring R
      ( case-one-bounded-sum-arithmetic-function-Ring
        ( P one-nonzero-ℕ)
        ( is-decidable-Decidable-Prop (P one-nonzero-ℕ))
        ( f one-nonzero-ℕ))
      ( bounded-sum-arithmetic-function-Ring
        ( succ-ℕ b)
        ( P  succ-nonzero-ℕ)
        ( f  succ-nonzero-ℕ))