Library Algebra.binomial_compl

This file is part of the Coq Numerical Analysis library
Copyright (C) Boldo, Clément, Martin, Mayero, Mouhcine
This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the COPYING file for more details.

Brief description

Complements on the binomial coefficients (aka binomials).

Description

The binomials are defined in the Mathematical Components library, and denoted 'C n p, a positive number iff p n.
The present module adds:
  • a couple of properties about sums of binomials,
  • a way to structurally grant that a binomial is positive.

Predecessor of (nonzero) binomial

Taking 'C (m + n) m already structurally grants that m m + n, and the variant (pbinom m n).+1 also structurally grants that it is positive.

Usage

This module may be used through the import of Algebra.Algebra, or Algebra.Algebra_wDep, where it is exported.

From Requisite Require Import stdlib.

From Requisite Require Import ssr_wMC.
From mathcomp Require Import binomial.

From Coquelicot Require Import Hierarchy.
Close Scope R_scope.

From Subsets Require Import Subsets.
From Algebra Require Import Hierarchy_compl Monoid.

Section Binomial_compl.

Lemma binom_sym_alt :
   m n, 'C ((m + n)%coq_nat, m) = 'C ((m + n)%coq_nat, n).
Proof.
intros; rewrite plusE -bin_sub; [rewrite -addnBAC// subnn// | apply leq_addr].
Qed.

Lemma binom_rising_sum_l :
   m n,
    sum (fun i : 'I_n.+1'C ((m + i)%coq_nat, m)) =
      'C ((m.+1 + n)%coq_nat, m.+1).
Proof.
intros m n; induction n as [| n Hn].
rewrite sum_1 !Nat.add_0_r !binn; easy.
rewrite sum_ind_r; unfold widenF_S; simpl; rewrite Hn.
replace (m.+1 + n)%coq_nat with (m + n.+1)%coq_nat; auto with zarith.
Qed.

Lemma binom_rising_sum_r :
   m n,
    sum (fun i : 'I_n.+1'C ((m + i)%coq_nat, i)) =
      'C ((m.+1 + n)%coq_nat, n).
Proof.
intros; rewrite -binom_sym_alt -binom_rising_sum_l.
apply sum_ext; intros; apply eq_sym, binom_sym_alt.
Qed.

End Binomial_compl.

Section Pbinom_Def.

Definition pbinom (m n : nat) : nat := ('C ((m + n)%coq_nat, m)).-1.

End Pbinom_Def.

Section PbinomS_Facts.

Lemma pbinomS_eq : m n, (pbinom m n).+1 = 'C ((m + n)%coq_nat, m).
Proof.
intros; apply Nat.succ_pred, not_eq_sym, Nat.lt_neq; apply /ltP.
rewrite bin_gt0 plusE; apply leq_addr.
Qed.

Lemma pbinomS_pascal :
   m n, (pbinom m n.+1).+1 + (pbinom m.+1 n).+1 = (pbinom m.+1 n.+1).+1.
Proof. intros; rewrite !pbinomS_eq plusE addnC addSnnS; apply binS. Qed.

Lemma pbinomS_sym : m n, (pbinom m n).+1 = (pbinom n m).+1.
Proof.
intros; rewrite !pbinomS_eq plusE addnC -bin_sub;
    [rewrite addnK; easy | apply leq_addl].
Qed.

Lemma pbinomS_0_l : n, (pbinom 0 n).+1 = 1.
Proof. intros; rewrite pbinomS_eq plusE add0n; apply bin0. Qed.

Lemma pbinomS_0_r : m, (pbinom m 0).+1 = 1.
Proof. intros; rewrite pbinomS_eq plusE addn0; apply binn. Qed.

Lemma pbinomS_1_l : n, (pbinom 1 n).+1 = n.+1.
Proof. intros; rewrite pbinomS_eq plusE add1n; apply bin1. Qed.

Lemma pbinomS_1_r : m, (pbinom m 1).+1 = m.+1.
Proof. intros; rewrite pbinomS_eq plusE addn1; apply binSn. Qed.

Lemma pbinomS_leq :
   m n1 n2, n1 n2 (pbinom m n1).+1 (pbinom m n2).+1.
Proof.
intros; rewrite !pbinomS_eq plusE; apply leq_bin2l; rewrite leq_add2l; easy.
Qed.

Lemma pbinomS_monot :
   m n1 n2, (n1 n2)%coq_nat (pbinom m n1).+1 (pbinom m n2).+1.
Proof. move=>> /leP H; apply pbinomS_leq; easy. Qed.

Lemma pbinomS_monot_pred : m n, (pbinom m (n.-1)).+1 (pbinom m n).+1.
Proof.
intros m [| n]; [simpl; apply ltnSn | apply pbinomS_monot, Nat.le_pred_l].
Qed.

Lemma pbinomS_le :
   m n1 n2,
    (n1 n2)%coq_nat ((pbinom m n1).+1 (pbinom m n2).+1)%coq_nat.
Proof. intros; apply /leP; apply pbinomS_monot; easy. Qed.

Lemma pbinomS_gt_0 : m n, (0 < (pbinom m n).+1)%coq_nat.
Proof.
intros; apply /ltP; rewrite pbinomS_eq plusE bin_gt0; apply leq_addr.
Qed.

Lemma pbinomS_rising_sum_l :
   m n, sum (fun i : 'I_n.+1(pbinom m i).+1) = (pbinom m.+1 n).+1.
Proof.
intros; rewrite pbinomS_eq -binom_rising_sum_l.
apply sum_ext; intros; apply pbinomS_eq.
Qed.

Lemma pbinomS_rising_sum_r :
   m n, sum (fun i : 'I_n.+1(pbinom i m).+1) = (pbinom n m.+1).+1.
Proof.
intros; rewrite pbinomS_eq Nat.add_comm -binom_rising_sum_r.
apply sum_ext; intros; rewrite Nat.add_comm; apply pbinomS_eq.
Qed.

End PbinomS_Facts.

Section Pbinom_Facts.

Lemma pbinom_sym : m n, pbinom m n = pbinom n m.
Proof. intros; apply eq_add_S, pbinomS_sym. Qed.

Lemma pbinom_0_l : n, pbinom 0 n = 0.
Proof. intros; apply eq_add_S, pbinomS_0_l. Qed.

Lemma pbinom_0_r : m, pbinom m 0 = 0.
Proof. intros; apply eq_add_S, pbinomS_0_r. Qed.

Lemma pbinom_1_l : n, pbinom 1 n = n.
Proof. intros; apply eq_add_S, pbinomS_1_l. Qed.

Lemma pbinom_1_r : m, pbinom m 1 = m.
Proof. intros; apply eq_add_S, pbinomS_1_r. Qed.

Lemma pbinom_le :
   m n1 n2, (n1 n2)%coq_nat (pbinom m n1 pbinom m n2)%coq_nat.
Proof. intros; apply Nat.succ_le_mono, pbinomS_le; easy. Qed.

Lemma pbinom_leq : m n1 n2, n1 n2 pbinom m n1 pbinom m n2.
Proof. intros; apply /leP; apply pbinom_le; apply /leP; easy. Qed.

Lemma pbinom_ge_0 : m n, (0 pbinom m n)%coq_nat.
Proof. intros; apply Nat.lt_succ_r, pbinomS_gt_0. Qed.

End Pbinom_Facts.