In this section, we define and prove facts about superadditivity and superadditive functions. The definition of superadditivity presented here slightly differs from the standard one (f a + f b f (a + 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 a + f b f h.

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 + f b f (a + b).

Then, we prove that the two definitions are implied by each other.
f,
Proof.
split.
- moveSUPER a b.
by apply SUPER.
- moveSUPER h a b AB.
rewrite -AB.
by apply SUPER.
Qed.

End EquivalenceWithStandardDefinition.

Section Facts.

Consider a function f.
Variable f : nat nat.

First, we show that if f is superadditive in zero, then its value in zero must also be zero.
f 0 = 0.
Proof.
moveSUPER.
destruct (f 0) eqn:Fx; first by done.
specialize (SUPER 0 0 (addn0 0)).
apply /negP; rewrite -ltnNge.
by lia.
Qed.

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

First, we show that f must also be monotone.
monotone leq f.
Proof.
movex y LEQ.
apply leq_trans with (f x + f (y - x)).
- by lia.
by lia.
Qed.

Next, we prove that moving any factor m outside of the arguments of f leads to a smaller or equal number.
n m,
m × f n f (m × n).
Proof.
moven m.
elim: m⇒ [| m IHm]; first by lia.
rewrite !mulSnr.
apply leq_trans with (f (m × n) + f n).
Qed.

In the next section, we show that any superadditive function that is not the zero constant function (i.e., f x = 0 for any x) is forced to grow beyond any finite limit.

Assume that f is not the zero constant function ...
Hypothesis h_non_zero: n, f n > 0.

... then, f will eventually grow larger than any number.
t, n', t f n'.
Proof.
movet.
move: h_non_zero ⇒ [n LT_n].
(t × n).
apply leq_trans with (t × f n).
- by apply leq_pmulr.
Qed.

End Facts.

In this section, we present the define and prove facts about the minimal superadditive extension of superadditive functions. Given a prefix of a function, there are many ways to continue the function in order to maintain superadditivity. Among these possible extrapolations, there always exists a minimal one.
Consider a function f.
Variable f : nat nat.

First, we define what it means to find the minimal extension once a horizon is specified.
Section Definitions.

Consider a horizon h..
Variable h : nat.

Then, the minimal superadditive extension will be the maximum sum over the pairs that sum to h. Note that, in this formula, there are two important edge cases: both h=0 and h=1, the sequence of valid sums will be empty, so their maximum will be 0. In both cases, the extrapolation is nonetheless correct.
max0 [seq f a + f (h-a) | a <- index_iota 1 h].

End Definitions.

In the following section, we prove some facts about the minimal superadditive extension. Note that we currently do not prove that the implemented extension is minimal. However, we plan to add this fact in the future. The following discussion provides useful information on the subject, including its connection with Network Calculus: https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/127note_64177
Section Facts.

Consider a horizon h ...
Variable h : nat.

... and assume that we know f to be superadditive until h.

Moreover, consider a second function, f', which is equivalent to f in all of its points except for h, in which its value is exactly the superadditive extension of f in h.
Variable f' : nat nat.
Hypothesis h_f'_min_extension : t,
f' t =
if t == h
else f t.

First, we prove that f' is superadditive also in h.
Proof.
movea b SUM.
rewrite !h_f'_min_extension.
rewrite -SUM.
destruct a as [|a'] eqn:EQa; destruct b as [|b'] eqn:EQb ⇒ //=.
{ rewrite -!EQa -!EQb eq_refl //=.
apply in_max0_le.
apply /mapP; a.
- by rewrite mem_iota; lia.
- by have → : a + b - a = b by lia. }
Qed.

And finally, we prove that f' is superadditive until h.+1.
Proof.
movet LEQh a b SUM.
destruct (ltngtP t h) as [LT | GT | EQ].
- rewrite !h_f'_min_extension.
rewrite !ltn_eqF; try lia.