Library probsa.util.bigop

From probsa.util Require Export notation.

Lemma bigsum_distr :
  ∀ (t1 t2 : nat) (f : nat → R) (c : R),
    ∑_{t1 ≤ i ≤ t2 } c × f i = c × ∑_{t1 ≤ i ≤ t2 } f i.
Proof.
  intros; have [LE|LT] := leqP t1 t2; last first.
  { by rewrite !big_geq; try assumption; nra. }
  have EQ: ∃ δ , (t2 = t1 + δ)%nat; [by ∃ (t2 - t1)%nat; rewrite subnKC | ].
  elim: EQ ⇒ [δ EQ]; subst t2; clear LE.
  induction δ.
  - by rewrite addn0 !big_nat1.
  - rewrite !addnS big_nat_recr //= ?IHδ; clear IHδ; last by rewrite ltnW //= ltnS leq_addr.
    rewrite !big_nat_recr //=; try rewrite ltnW //= ltnS; try by rewrite leq_addr.
    by nra.
Qed.

Lemma bigsum_add :
  ∀ (t1 t2 : nat) (f g : nat → R),
    ∑_{t1 ≤ i ≤ t2 } (f i + g i ) = ∑_{t1 ≤ i ≤ t2 } f i + ∑_{t1 ≤ i ≤ t2 } g i.
Proof.
  intros; have [LE|LT] := leqP t1 t2; last first.
  { by rewrite !big_geq; try assumption; nra. }
  have EQ: ∃ δ , (t2 = t1 + δ)%nat; [by ∃ (t2 - t1)%nat; rewrite subnKC | ].
  elim: EQ ⇒ [δ EQ]; subst t2; clear LE.
  induction δ.
  - by rewrite addn0 !big_nat1.
  - rewrite !addnS big_nat_recr //= ?IHδ; clear IHδ; last by rewrite ltnW //= ltnS leq_addr.
    rewrite !big_nat_recr //=; try rewrite ltnW //= ltnS; try by rewrite leq_addr.
    by nra.
Qed.

Lemma bigD1_seq_pred :
  ∀ (R : Type) (idx : R) (op : Monoid.com_law idx) (I : eqType) (r : seq I) (P : pred I) (j : I) (F : I → R ),
    P j →
    (j \in r ) →
    uniq r →
    \big[op/idx]_(i <- r | P i) F i
    = op (F j) (\big[op/idx]_(i <- r | (P i ) && (i != j )) F i).
Proof.
  move ⇒ ? ? ? ? ? ? j ? Pj ×.
  by rewrite big_mkcondl big_mkcond (bigD1_seq j) // Pj //.
Qed.

Lemma foldr_big :
  ∀ {T : eqType} (op : T → T → T) (e : T) (xs : seq T),
    fold_right op e xs = \big[op/e]_( x <- xs ) x.
Proof.
  induction xs; first by rewrite big_nil.
  by rewrite big_cons //= IHxs.
Qed.

In this section, we relate the sum of items with the sum over partitions of those items.

Section SumOverPartitions.

Consider an item type X and a partition type Y.

Variable X Y : eqType.

x_to_y is the mapping from an item to the partition it is contained in.

Variable x_to_y : X → Y.

Consider f, a function from X to nat.

Variable f : X → nat.

Consider an arbitrary predicate P on X.

Variable P : pred X.

Consider a sequence of items xs and a sequence of partitions ys.

Variable xs : seq X.
Variable ys : seq Y.

We assume that any item in xs has its corresponding partition in the sequence of partitions ys.

Hypothesis H_no_partition_missing : ∀ x, x \in xs → P x → x_to_y x \in ys.

Consider the sum of f x over all x in a given partition y.

Let sum_of_partition y := \sum_(x <- xs | P x && (x_to_y x == y )) f x.

We prove that summation of f x over all x is less than or equal to the summation of sum_of_partition over all partitions.

  Lemma sum_over_partitions_le :
    (\sum_(x <- xs | P x) f x
     ≤ \sum_(y <- ys) sum_of_partition y)%nat.
  Proof.
    rewrite /sum_of_partition.
    induction xs as [| x' xs' LE_TAIL]; first by rewrite big_nil.
    have P_HOLDS: ∀ i j, true → P j && (x_to_y j== i ) → P j by move⇒ ??? /andP [P_HOLDS _].
    have IN_ys: ∀ x : X, x \in xs' → P x → x_to_y x \in ys
            by move⇒ ??; apply H_no_partition_missing ⇒ //; rewrite in_cons; apply /orP; right.
    move: LE_TAIL; rewrite (exchange_big_dep P) ⇒ //= LE_TAIL.
    rewrite (exchange_big_dep P) //= !big_cons.
    case PX: (P x') ⇒ //=.
    { apply leq_add ⇒ //.
      { rewrite big_const_seq iter_addn_0.
        apply leq_pmulr; rewrite -has_count.
        apply /hasP; eapply ex_intro2 ⇒ //.
        apply H_no_partition_missing ⇒ //.
        exact: mem_head. }
      { by apply LE_TAIL. }
    }
    { by apply LE_TAIL. }
  Qed.

End SumOverPartitions.