# Bounded sums of arithmetic functions

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

Created on 2022-03-23.

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.function-types
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 =