Library prosa.util.subadditivity


(* ----------------------------------[ coqtop ]---------------------------------

Welcome to Coq 8.13.0 (January 2021)

----------------------------------------------------------------------------- *)

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.
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 :=
    ∀ 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 :=
    ∀ 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 :=
    ∀ 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 :=
      ∀ a b,
         f (a + b) ≤ f a + f b.

Then, we prove that the two definitions are implied by each other.
    Lemma subadditive_standard_equivalence :
      ∀ f,
        subadditive f ↔ subadditive_standard f.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 34)
  
  ============================
  forall f : nat -> nat, subadditive f <-> subadditive_standard f

----------------------------------------------------------------------------- *)

    Proof.
      split.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 37)
  
  f : nat -> nat
  ============================
  subadditive f -> subadditive_standard f

subgoal 2 (ID 38) is:
 subadditive_standard f -> subadditive f

----------------------------------------------------------------------------- *)

      - move⇒ SUB a b.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 42)
  
  f : nat -> nat
  SUB : subadditive f
  a, b : nat
  ============================
  f (a + b) <= f a + f b

subgoal 2 (ID 38) is:
 subadditive_standard f -> subadditive f

----------------------------------------------------------------------------- *)

        by apply SUB.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 38)
  
  f : nat -> nat
  ============================
  subadditive_standard f -> subadditive f

----------------------------------------------------------------------------- *)

      - move⇒ SUB h a b AB.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 50)
  
  f : nat -> nat
  SUB : subadditive_standard f
  h, a, b : nat
  AB : a + b = h
  ============================
  f h <= f a + f b

----------------------------------------------------------------------------- *)

        rewrite -AB.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 52)
  
  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.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

    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.
      Lemma subadditive_leq_mul:
        ∀ n m,
          0 < m →
          f (m × n) ≤ m × f n.

(* ----------------------------------[ coqtop ]---------------------------------

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

----------------------------------------------------------------------------- *)

      Proof.
        move⇒ n [// | m] _.

(* ----------------------------------[ coqtop ]---------------------------------

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

----------------------------------------------------------------------------- *)

        elim: m ⇒ [ | m IHm]; first by rewrite !mul1n.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 78)
  
  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

----------------------------------------------------------------------------- *)

        rewrite mulSnr [X in _ ≤ X]mulSnr.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 104)
  
  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

----------------------------------------------------------------------------- *)

        move: IHm; rewrite -(leq_add2r (f n)).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 110)
  
  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.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

      Qed.

    End SubadditiveFunctions.

  End Facts.

End Subadditivity.