Library mathcomp_eulerian.qeul

From mathcomp Require Import all_ssreflect fingroup perm ssrint ssralg poly.
From mathcomp_eulerian Require Import ordinal_reindex perm_compress
                                       descent eulerian beta inversions
                                       foata qfact.

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

Import GRing.Theory.

Open Scope ring_scope.


Notation qpow k := (('X ^+ k : {poly int})%:P : {poly {poly int}}).


Definition q_eul_pol (n : nat) : {poly {poly int}} :=
  \sum_(σ : {perm 'I_n.+1}) qpow (maj σ) × 'X^(des σ).


Theorem q_eul_pol_t1 n :
  (q_eul_pol n).[1] = q_fact n.
Proof.
rewrite /q_eul_pol horner_sum.
rewrite -[RHS]maj_q_fact.
apply: eq_bigr ⇒ σ _.
rewrite hornerM hornerXn expr1n mulr1.
by rewrite hornerC.
Qed.


Definition eul_pol (n : nat) : {poly int} :=
  \sum_(k < n.+1) (eulerian n k)%:R × 'X^k.

Lemma sum_des_eq_eul_pol n :
  \sum_(σ : {perm 'I_n.+1}) 'X^(des σ) = eul_pol n :> {poly int}.
Proof.
rewrite /eul_pol.
pose F (s : {perm 'I_n.+1}) : 'I_n.+1 := Ordinal (leq_ltn_trans (des_le s) (ltnSn n)).
rewrite (partition_big F xpredT) //=.
apply: eq_bigr ⇒ k _.
rewrite /eulerian.
under eq_bigl ⇒ s do rewrite -val_eqE /F /=.
rewrite -sum1dep_card natr_sum big_distrl /=.
apply: eq_bigr ⇒ s /eqP Hs.
by rewrite Hs mul1r.
Qed.


Definition q1_subst : {poly {poly int}} → {poly int} :=
  map_poly (horner_eval (1 : int)).

Theorem q_eul_pol_q1 n :
  q1_subst (q_eul_pol n) = eul_pol n.
Proof.
rewrite /q_eul_pol /q1_subst.
rewrite (raddf_sum (map_poly (horner_eval (1 : int)))) /=.
rewrite -sum_des_eq_eul_pol.
apply: eq_bigr ⇒ σ _.
rewrite rmorphM /= map_polyXn map_polyC /=.
rewrite /horner_eval hornerXn expr1n.
by rewrite mul1r.
Qed.