Library mathcomp_eulerian.cycles

From mathcomp Require Import all_ssreflect fingroup perm.
From mathcomp_eulerian Require Import ordinal_reindex perm_compress descent.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.


Definition cycle_count {T : finType} (s : {perm T}) : nat := #|porbits s|.


Definition stirling_c (n k : nat) : nat :=
  #|[set s : {perm 'I_n} | cycle_count s == k]|.


Section CycleBasic.

Lemma cycle_count_le {T : finType} (s : {perm T}) :
  cycle_count s ≤ #|T|.
Proof.
rewrite /cycle_count /porbits.
exact: leq_imset_card.
Qed.

Lemma porbit_id_singleton (T : finType) (x : T) :
  porbit (1 : {perm T}) x = [set x].
Proof.
apply/setP⇒ y; rewrite !inE.
apply/porbitP/eqP.
- by case⇒ i ->; rewrite expg1n perm1.
- by move⇒ ->; ∃ 0; rewrite expg1n perm1.
Qed.

Lemma cycle_count_id (T : finType) :
  cycle_count (1 : {perm T}) = #|T|.
Proof.
rewrite /cycle_count /porbits.
rewrite -[in RHS](card_imset [pred x : T | true] set1_inj).
apply: eq_card ⇒ P; apply/imsetP/imsetP.
- case⇒ x _ →.
  by ∃ x; rewrite ?inE //; rewrite porbit_id_singleton.
- case⇒ x _ →.
  by ∃ x ⇒ //; rewrite porbit_id_singleton.
Qed.

End CycleBasic.



Lemma stirling_c_row_sum n :
  \sum_(k < n.+1) stirling_c n k = #|{perm 'I_n}|.
Proof.
rewrite /stirling_c -sum1_card.
rewrite (partition_big (fun s : {perm 'I_n} ⇒ inord (cycle_count s) : 'I_n.+1)
                       xpredT) //=.
apply: eq_bigr ⇒ k _; rewrite -sum1_card; apply: eq_bigl ⇒ s; rewrite inE.
rewrite -val_eqE /= inordK //.
have := cycle_count_le s.
by rewrite card_ord.
Qed.

Lemma stirling_c_row_sum_fact n :
  \sum_(k < n.+1) stirling_c n k = n`!.
Proof. by rewrite stirling_c_row_sum card_Sn. Qed.