Built with Alectryon, running Coq+SerAPI v8.15.0+0.15.0. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use instead of Ctrl.
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "_ + _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ - _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ >= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ > _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ * _" was already used in scope nat_scope. [notation-overridden,parsing]
(** 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. *) Section Subadditivity. (** 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]. *) Definition subadditive_at f h := forall 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. *) Definition subadditive_until f h := forall x, x < h -> subadditive_at f x. (** Finally, give a definition of subadditive function: [f] is subadditive when it is subadditive at any point [h].*) Definition subadditive f := forall h, subadditive_at f h. (** In this section, we show that the proposed definition of subadditivity is equivalent to the standard one. *) Section EquivalenceWithStandardDefinition. (** First, we give a standard definition of subadditivity. *) Definition subadditive_standard f := forall a b, f (a + b) <= f a + f b. (** Then, we prove that the two definitions are implied by each other. *)

forall f : nat -> nat, subadditive f <-> subadditive_standard f

forall f : nat -> nat, subadditive f <-> subadditive_standard f
f: nat -> nat

subadditive f -> subadditive_standard f
f: nat -> nat
subadditive_standard f -> subadditive f
f: nat -> nat

subadditive f -> subadditive_standard f
f: nat -> nat
subadditive_standard f -> subadditive f
f: nat -> nat
SUB: subadditive f
a, b: nat

f (a + b) <= f a + f b
f: nat -> nat
subadditive_standard f -> subadditive f
f: nat -> nat

subadditive_standard f -> subadditive f
f: nat -> nat

subadditive_standard f -> subadditive f
f: nat -> nat
SUB: subadditive_standard f
h, a, b: nat
AB: a + b = h

f h <= f a + f b
f: nat -> nat
SUB: subadditive_standard f
h, a, b: nat
AB: a + b = h

f (a + b) <= f a + f b
by apply SUB. Qed. End EquivalenceWithStandardDefinition. (** In the following section, we prove some useful facts about subadditivity. *) Section Facts. (** Consider a function [f]. *) Variable f : nat -> nat. (** In this section, we show some of the properties of subadditive functions. *) Section SubadditiveFunctions. (** Assume that [f] is subadditive. *) Hypothesis h_subadditive : subadditive f. (** Then, we prove that moving any non-zero factor [m] outside of the arguments of [f] leads to a bigger or equal number. *)
f: nat -> nat
h_subadditive: subadditive f

forall n m : nat, 0 < m -> f (m * n) <= m * f n
f: nat -> nat
h_subadditive: subadditive f

forall n m : nat, 0 < m -> f (m * n) <= m * f n
f: nat -> nat
h_subadditive: subadditive f
n, m: nat

f (m.+1 * n) <= m.+1 * f n
f: nat -> nat
h_subadditive: subadditive f
n, m: nat
IHm: f (m.+1 * n) <= m.+1 * f n

f (m.+2 * n) <= m.+2 * f n
f: nat -> nat
h_subadditive: subadditive f
n, m: nat
IHm: f (m.+1 * n) <= m.+1 * f n

f (m.+1 * n + n) <= m.+1 * f n + f n
f: nat -> nat
h_subadditive: subadditive f
n, m: nat

f (m.+1 * n) + f n <= m.+1 * f n + f n -> f (m.+1 * n + n) <= m.+1 * f n + f n
exact /leq_trans/h_subadditive. Qed. End SubadditiveFunctions. End Facts. End Subadditivity.