Additivity theory

If everybody is happy with the current structure and code, I will comment it so that we can do a round of polish.

added 1 commit

9c864f2a - Merged export statements

Compare with previous version

Thanks, @mmaida!

Pinging @sophie @mlesourd @proux — this may be of interest to you as well.

Thanks. Pinging @Mbodin @fradet and @ptorrx too.

added 1 commit

17449ec5 - Fixed imports

Compare with previous version

FYI I also have a lot of code related to delta-min functions ready. If somebody is interested I might make a MR with that as well in the next weeks.

Noted, thanks. We had quite a few results on super and subadditive theories in another branch, so I'll be interested in looking at similarities and differences in your definitions, theorems and proofs.

I guess the only "major" comment from me is that it would be nice to add the standard definitions of subadditivity and superadditivity (even thought it is not useful at this point).

That is, f is subadditive := \forall x y, f (x + y) <= f x + f y.