# Library prosa.util.superadditivity

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

Require Export prosa.util.nat prosa.util.rel prosa.util.list.

Require Export prosa.util.nat prosa.util.rel prosa.util.list.

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.

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

Finally, give a definition of subadditive function: f is subadditive
when it is subadditive at any point 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.

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

Lemma superadditive_standard_equivalence :

∀ f,

superadditive f ↔ superadditive_standard f.

End EquivalenceWithStandardDefinition.

∀ f,

superadditive f ↔ superadditive_standard f.

End EquivalenceWithStandardDefinition.

In the following section, we prove some useful facts about superadditivity.

Consider a function f.

First, we show that if f is superadditive in zero, then its value in zero must
also be zero.

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

Assume that f is superadditive.

First, we show that f must also be monotone.

Next, we prove that moving any factor m outside of the arguments
of f leads to a smaller or equal number.

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

... then, f will eventually grow larger than any number.

Lemma superadditive_unbounded:

∀ t, ∃ n', t ≤ f n'.

End NonZeroSuperadditiveFunctions.

End SuperadditiveFunctions.

End Facts.

∀ t, ∃ n', t ≤ f n'.

End NonZeroSuperadditiveFunctions.

End SuperadditiveFunctions.

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.

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

Consider a horizon h..

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.

Definition minimal_superadditive_extension :=

max0 [seq f a + f (h-a) | a <- index_iota 1 h].

End Definitions.

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

Consider a horizon 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.