Done the proofs of Pieri_(elementary|complete)

Author: hivert

LRrule/Schur.v

@@ -288,6 +288,12 @@ Qed.
 Definition colpartn d : intpartn d := IntPartN (colpartnP d).
 Definition elementary d : {mpoly R[n]} := Schur (colpartn d).
 
+Lemma conj_rowpartn d : conj_intpartn (rowpartn d) = colpartn d.
+Proof. apply val_inj => /=; rewrite /rowpart /colpart; by case: d. Qed.
+Lemma conj_colpartn d : conj_intpartn (colpartn d) = rowpartn d.
+Proof. rewrite -[RHS]conj_intpartnK; by rewrite conj_rowpartn. Qed.
+
+
 (* Noncommutative lifting of Schur *)
 Lemma Schur_freeSchurE d (Q : stdtabn d) :
   Schur (shape_deg Q) = polyset R (freeSchur Q).
@@ -702,6 +708,7 @@ End Coeffs.
 
 End FinSets.
 
+
 Section Conj.
 
 Variables d1 d2 : nat.

LRrule/partition.v

@@ -760,6 +760,16 @@ Section SkewShape.
     move: Heq => /eqP; by rewrite H0 eqn_add2l => /eqP/(Hrec Hincl) ->.
   Qed.
 
+  Lemma included_conj_part inner outer :
+    is_part inner -> is_part outer ->
+    included inner outer -> included (conj_part inner) (conj_part outer).
+  Proof.
+    move=> Hinn Hout /includedP [] Hsz Hincl.
+    apply/includedP; split; first by rewrite !size_conj_part // -!nth0; exact: Hincl.
+    move=> i.
+    rewrite -conj_leqE //; apply (leq_trans (Hincl _)); by rewrite conj_leqE.
+  Qed.
+
   Fixpoint diff_shape inner outer :=
     if inner is inn0 :: inn then
       if outer is out0 :: out then
@@ -877,16 +887,18 @@ Canonical intpart_countType := Eval hnf in CountType intpart intpart_countMixin.
 Lemma intpartP (p : intpart) : is_part p.
 Proof. by case: p. Qed.
 
+Hint Resolve intpartP.
+
 Canonical conj_intpart p := IntPart (is_part_conj (intpartP p)).
 
 Lemma conj_intpartK : involutive conj_intpart.
-Proof.  move=> p; apply: val_inj => /=; by rewrite conj_partK; last by apply: intpartP. Qed.
+Proof. move=> p; apply: val_inj => /=; by rewrite conj_partK. Qed.
 
 Lemma intpart_sum_inj (s t : intpart) :
   (forall k, part_sum s k = part_sum t k) -> s = t.
 Proof.
   move=> H; apply: val_inj => /=.
-  apply: part_sum_inj; last exact H; by apply: intpartP.
+  by apply: part_sum_inj; last exact H.
 Qed.
 
 
@@ -1042,7 +1054,7 @@ Canonical intpartn_subFinType := Eval hnf in [subFinType of intpartn].
 
 Lemma intpartnP (p : intpartn) : is_part p.
 Proof. by case: p => /= p /andP []. Qed.
-
+Hint Resolve intpartnP.
 Definition intpart_of_intpartn (p : intpartn) := IntPart (intpartnP p).
 Coercion intpart_of_intpartn : intpartn >-> intpart.
 
@@ -1059,6 +1071,9 @@ Proof.
 Qed.
 Canonical conj_intpartn (sh : intpartn) := IntPartN (conj_intpartnP sh).
 
+Lemma conj_intpartnK : involutive conj_intpartn.
+Proof. move=> p; apply: val_inj => /=; by rewrite conj_partK. Qed.
+
 End PartOfn.
 
 Fixpoint intpartnsk_nb sm sz mx : nat :=

LRrule/skewtab.v

@@ -322,13 +322,136 @@ Section Dominate.
     else if outer is out0 :: out then out == [::]
          else true.
 
+  Fixpoint vb_strip inner outer :=
+    if outer is out0 :: out then
+      if inner is inn0 :: inn then
+        (inn0 <= out0 <= inn0.+1) && (vb_strip inn out)
+      else (out0 == 1) && (vb_strip [::] out)
+    else inner == [::].
+
   Lemma hb_strip_included inner outer :
     hb_strip inner outer -> included inner outer.
   Proof.
     elim: inner outer => [| inn0 inn IHinn] [| out0 out] //=.
     by move=> /andP [] /andP [] _ -> /IHinn ->.
   Qed.
 
+  Lemma vb_strip_included inner outer :
+    vb_strip inner outer -> included inner outer.
+  Proof.
+    elim: inner outer => [| inn0 inn IHinn] [| out0 out] //=.
+    by move=> /andP [] /andP [] -> _ /IHinn ->.
+  Qed.
+
+  Lemma hb_stripP inner outer :
+    is_part inner -> is_part outer ->
+    reflect
+      (forall i, nth 0 outer i.+1 <= nth 0 inner i <= nth 0 outer i)
+      (hb_strip inner outer).
+  Proof.
+    move=> Hinn Hout; apply (iffP idP).
+    - elim: inner outer {Hinn Hout} => [| inn0 inn IHinn] /= [| out0 out] //=.
+        move=> /eqP -> i; by rewrite leqnn /= nth_default.
+      move=> /andP [] H0 /IHinn{IHinn}Hrec [//= | i]; exact: Hrec.
+    - elim: inner Hinn outer Hout => [| inn0 inn IHinn] Hinn /= [| out0 out] Hout //= H.
+      + have:= H 0 => /andP []; rewrite nth_nil leqn0 => /eqP {H} H _.
+        have:= part_head_non0 (is_part_tl Hout).
+        rewrite -nth0; by case: out H {Hout} => [//=| out1 out'] /= ->.
+      + have:= part_head_non0 Hinn; have:= H 0.
+        by rewrite /= leqn0 => ->.
+      + have := H 0; rewrite nth0 /= => -> /=.
+        apply (IHinn (is_part_tl Hinn) _ (is_part_tl Hout)) => i.
+        exact: H i.+1.
+  Qed.
+
+  Lemma vb_stripP inner outer :
+    is_part inner -> is_part outer ->
+    reflect
+      (forall i, nth 0 inner i <= nth 0 outer i <= (nth 0 inner i).+1)
+      (vb_strip inner outer).
+  Proof.
+    move=> Hinn Hout; apply (iffP idP) => [Hstrip|].
+    - elim: outer inner Hstrip Hout Hinn =>
+        [//= | out0 out IHout] [| inn0 inn] /=.
+      + move=> _ _ _ i; by rewrite nth_default.
+      + by move => /eqP.
+      + move=> /andP [] /eqP -> {out0 IHout} H _ _ [|i] //=.
+        elim: out H i => [//= | out1 out IHout] /=.
+          move=> _ i; by rewrite nth_default.
+        move=> /andP [] /eqP -> /IHout{IHout} Hrec; by case.
+      + by move=> /andP [] H0 /IHout{IHout}Hrec
+                  /andP [] Hout /Hrec{Hrec}Hrec
+                  /andP [] Hinn /Hrec{Hrec}Hrec [|i] //=.
+    - elim: outer inner Hout Hinn => [//= | out0 out IHout].
+      + case => [//= | inn0 inn] _ /= /andP [] Habs Hinn H; exfalso.
+        have {H} := H 0 => /= /andP []; rewrite leqn0 => /eqP Hinn0 _.
+        subst inn0; move: Habs Hinn; by rewrite leqn0 => /part_head0F ->.
+      + move=> inner Hpart; have:= part_head_non0 Hpart => /=.
+        rewrite -lt0n eqn_leq => H0out.
+        case: inner => [_ | inn0 inn]/=.
+          move=> {IHout} H; rewrite H0out.
+          have:= H 0 => /= -> /=.
+          have {H} /= Hout i := H i.+1.
+          move: Hpart => /= /andP [] _.
+          elim: out Hout => [//= | out1 out IHout] H Hpart.
+          have:= part_head_non0 Hpart => /=.
+          rewrite -lt0n eqn_leq => ->.
+          have:= H 0 => /= -> /=.
+          apply: IHout; last exact: (is_part_tl Hpart).
+          move=> i; exact: H i.+1.
+      + move: Hpart => /andP [] H0 /IHout{IHout}Hrec
+                       /andP [] _  /Hrec{Hrec}Hrec H.
+        have := H 0 => /= -> /=.
+        apply Hrec => i.
+        exact: H i.+1.
+  Qed.
+
+  Lemma vb_strip_conj inner outer :
+    is_part inner -> is_part outer ->
+    vb_strip inner outer -> hb_strip (conj_part inner) (conj_part outer).
+  Proof.
+    move=> Hinn Hout; have Hcinn := is_part_conj Hinn; have Hcout := is_part_conj Hout.
+    move => /(vb_stripP Hinn Hout) H.
+    apply/(hb_stripP Hcinn Hcout) => i; rewrite -!conj_leqE //; apply/andP; split.
+    + have {H} := H (nth 0 (conj_part inner) i) => /andP [] _ /leq_trans; apply.
+      by rewrite ltnS conj_leqE.
+    + have {H} := H (nth 0 (conj_part outer) i) => /andP [] /leq_trans H _; apply H.
+      by rewrite conj_leqE.
+  Qed.
+
+  Lemma hb_strip_conj inner outer :
+    is_part inner -> is_part outer ->
+    hb_strip inner outer -> vb_strip (conj_part inner) (conj_part outer).
+  Proof.
+    move=> Hinn Hout; have Hcinn := is_part_conj Hinn; have Hcout := is_part_conj Hout.
+    move => /(hb_stripP Hinn Hout) H.
+    apply/(vb_stripP Hcinn Hcout) => i; rewrite -!conj_leqE //; apply/andP; split.
+    + have {H} := H (nth 0 (conj_part outer) i) => /andP [] _ /leq_trans; apply.
+      by rewrite conj_leqE.
+    + have {H} := H (nth 0 (conj_part inner) i) => /andP [] /leq_trans H _; apply H.
+      by rewrite conj_leqE.
+  Qed.
+
+  Lemma hb_strip_conjE inner outer :
+    is_part inner -> is_part outer ->
+    hb_strip (conj_part inner) (conj_part outer) = vb_strip inner outer.
+  Proof.
+    move=> Hinn Hout; apply (sameP idP); apply (iffP idP).
+    - exact: vb_strip_conj.
+    - rewrite -{2}(conj_partK Hinn) -{2}(conj_partK Hout).
+      exact: hb_strip_conj (is_part_conj Hinn) (is_part_conj Hout).
+  Qed.
+
+  Lemma vb_strip_conjE inner outer :
+    is_part inner -> is_part outer ->
+    vb_strip (conj_part inner) (conj_part outer) = hb_strip inner outer.
+  Proof.
+    move=> Hinn Hout; apply (sameP idP); apply (iffP idP).
+    - exact: hb_strip_conj.
+    - rewrite -{2}(conj_partK Hinn) -{2}(conj_partK Hout).
+      exact: vb_strip_conj (is_part_conj Hinn) (is_part_conj Hout).
+  Qed.
+
   Lemma row_dominate u v :
     is_row (u ++ v) -> dominate u v -> u = [::].
   Proof.

LRrule/therule.v

@@ -602,21 +602,13 @@ Proof.
   * exfalso; by case: (evalseq y) y0 Heval => [| a [| l0 l]] [|y0].
 Qed.
 
-Theorem Pieri_row (P1 : intpartn d1) :
-  Schur P1 * complete d2 = \sum_(P : intpartn (d1 + d2) | hb_strip P1 P) Schur P.
+Theorem LRyam_coeff_Pieri_row (P1 : intpartn d1) (P : intpartn (d1 + d2)) :
+  included P1 P -> LRyam_coeff P1 (rowpartn d2) P = hb_strip P1 P.
 Proof.
-  rewrite /Schur.complete LRtab_coeffP.
-  rewrite [LHS]big_mkcond [RHS]big_mkcond /=.
-  apply eq_bigr => p _.
-  case: (boolP (included P1 p)) => Hincl; first last.
-    suff /negbTE -> : ~~ hb_strip P1 p by [].
-    move: Hincl; apply contra; exact: hb_strip_included.
-  suff -> : LRyam_coeff P1 (rowpartn d2) p = hb_strip P1 p.
-    case: (hb_strip P1 p); by rewrite /= ?mulr1n ?mulr0n.
-  rewrite /LRyam_coeff /LRyam_set.
+  rewrite /LRyam_coeff /LRyam_set => Hincl.
   rewrite /is_skew_reshape_tableau.
   set LRset := (X in #|pred_of_set X|).
-  case: (boolP (hb_strip P1 p)) => Hstrip /=.
+  case: (boolP (hb_strip P1 P)) => Hstrip /=.
   - suff -> : LRset = [set yamrow] by rewrite cards1.
     rewrite -setP => y; rewrite !inE {LRset}.
     case: y => y Hy /=.
@@ -644,6 +636,44 @@ Proof.
     by rewrite Hincl Hskew.
 Qed.
 
+Theorem Pieri_row (P1 : intpartn d1) :
+  Schur P1 * complete d2 = \sum_(P : intpartn (d1 + d2) | hb_strip P1 P) Schur P.
+Proof.
+  rewrite /Schur.complete LRtab_coeffP.
+  rewrite [LHS]big_mkcond [RHS]big_mkcond /=.
+  apply eq_bigr => p _.
+  case: (boolP (included P1 p)) => Hincl; first last.
+    suff /negbTE -> : ~~ hb_strip P1 p by [].
+    move: Hincl; apply contra; exact: hb_strip_included.
+  rewrite (LRyam_coeff_Pieri_row Hincl).
+  case: (hb_strip P1 p); by rewrite /= ?mulr1n ?mulr0n.
+Qed.
+
+Theorem LRyam_coeff_Pieri_col (P1 : intpartn d1) (P : intpartn (d1 + d2)) :
+  included P1 P -> LRyam_coeff P1 (colpartn d2) P = vb_strip P1 P.
+Proof.
+  move=> Hincl.
+  have Hinclc : included (conj_intpartn P1) (conj_intpartn P).
+    exact: included_conj_part.
+  rewrite -conj_rowpartn -{1}(conj_intpartnK P1) -{1}(conj_intpartnK P).
+  rewrite -LR_coeff_yamP; last by rewrite !conj_intpartnK.
+  rewrite -LRtab_coeff_conj (LR_coeff_yamP _ Hinclc) (LRyam_coeff_Pieri_row Hinclc).
+  by rewrite /= hb_strip_conjE.
+Qed.
+
+Theorem Pieri_col (P1 : intpartn d1) :
+  Schur P1 * elementary d2 = \sum_(P : intpartn (d1 + d2) | vb_strip P1 P) Schur P.
+Proof.
+  rewrite /Schur.elementary LRtab_coeffP.
+  rewrite [LHS]big_mkcond [RHS]big_mkcond /=.
+  apply eq_bigr => p _.
+  case: (boolP (included P1 p)) => Hincl; first last.
+    suff /negbTE -> : ~~ vb_strip P1 p by [].
+    move: Hincl; apply contra; exact: vb_strip_included.
+  rewrite (LRyam_coeff_Pieri_col Hincl).
+  case: (vb_strip P1 p); by rewrite /= ?mulr1n ?mulr0n.
+Qed.
+
 End Pieri.
 
 End LR.