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.

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.

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).

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.

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

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.

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.
End SumOverPartitions.