From mathcomp Require Export ssreflect ssrbool eqtype ssrnat div seq path fintype bigop.

In this section, we define and prove facts about subadditivity and subadditive functions. The definition of subadditivity presented here slightly differs from the standard one (f (a + b) f a + f b for any a and b), but it is proven to be equivalent to it.

First, we define subadditivity as a point-wise property; i.e., f is subadditive at h if standard subadditivity holds for any pair (a,b) that sums to h.
a b,
a + b = h
f h f a + f b.

Second, we define the concept of partial subadditivity until a certain horizon h. This definition is useful when dealing with finite sequences.
x,
x < h

Finally, give a definition of subadditive function: f is subadditive when it is subadditive at any point h.
h,

In this section, we show that the proposed definition of subadditivity is equivalent to the standard one.
First, we give a standard definition of subadditivity.
a b,
f (a + b) f a + f b.

Then, we prove that the two definitions are implied by each other.
Section Facts.

Consider a function f.
Variable f : nat nat.

In this section, we show some of the properties of subadditive functions.