proposition: Lemma Formula1 : (hook_length_prod p)%:Q / (hook_length_prod p')%:Q = ( \prod_(0 <= i < Alpha) (1 + ((hook_length p (i, Beta) )%:Q - 1)^-1) ) * ( \prod_(0 <= j < Beta) (1 + ((hook_length p (Alpha, j))%:Q - 1)^-1) ).
proof: Proof. Proof using Hpartc'. rewrite /hook_length_prod /= !big_box_skew /= . rewrite -{1}Hp -(perm_big _ (box_in_incr_nth _ _)) /= big_cons. rewrite !PoszM /= !intrM /=. rewrite !(big_morph Posz PoszM (id1 := Posz 1%N)) //=. rewrite !(big_morph intr (@intrM _) (id1 := 1)) //=. rewrite -mulrA. rewrite -HBeta' (corner_hook_length1 (intpartP p) Hcorn) mul1r. rewrite -prodf_div /=. rewrite (bigID (fun i => i.1 == Alpha)) /=. rewrite mulrC (bigID (fun i => i.2 == Beta)) /= mulrC mulrA. rewrite [RHS]mulrC -[RHS]mulr1; congr (_ * _ * _). - exact: prod_hook_length_quot_row. - have Hpartconj := is_part_conj (intpartP p). have Hcornconj := corner_box_conj_part (intpartP p) Hcorn. have Hconj' : (decr_nth (conj_part p) Beta) = conj_part p'. rewrite -Hp conj_part_incr_nth //; last exact: add_corner_decr_nth. rewrite -HBeta' incr_nthK //. apply (is_part_incr_nth Hpartc'). rewrite HBeta'; apply (is_add_corner_conj_part Hpart'). exact: add_corner_decr_nth. transitivity (\prod_(0 <= j < Alpha) (1 + ((hook_length (conj_part p) (Beta, j))%:Q - 1)^-1)); first last. by apply eq_bigr => i _; rewrite hook_length_conj_part. rewrite -(prod_hook_length_quot_row Hpartconj Hcornconj) Hconj'. pose swap i : nat * nat := (i.2, i.1). have swap_inj : injective swap by apply (can_inj (g := swap)) => [] [r c]. rewrite -[RHS]big_filter; set F := (X in \prod_(i <- _) X i). rewrite -[X in \prod_(i <- X) _]map_id. rewrite (eq_map (g := swap \o swap)); last by move=> [r c]. rewrite map_comp big_map. transitivity (\prod_(i <- enum_box_in p' | (i.1 != Alpha) && (i.2 == Beta)) F (swap i)). apply eq_bigr => [[r c]] _. by rewrite /swap {}/F /= !hook_length_conj_part. rewrite -big_filter; apply: perm_big => {F}. apply uniq_perm. + by apply filter_uniq; apply: enum_box_in_uniq. + rewrite (map_inj_uniq swap_inj). by apply filter_uniq; apply: enum_box_in_uniq. + move=> [r c] /=. rewrite -/(swap (c, r)) (mem_map swap_inj) !mem_filter /=. rewrite !mem_enum_box_in !unfold_in /= -!/(in_shape _ (_, _)). rewrite -in_conj_part //. case: (boolP (in_shape p' (r, c))) => Hrc; last by rewrite !andbF. case: (c =P Beta) => /= Hc; last by rewrite !andbF. rewrite !andbT. move: Hrc; rewrite /in_shape Hc HBeta'. by rewrite ltnNge; apply contra => /eqP ->. - rewrite big_seq_cond; apply big1 => [[r c]] /= /and3P[]. rewrite mem_enum_box_in unfold_in => Hrc Hr Hc. rewrite -Hp hook_length_incr_nth. + by rewrite divff // intr_eq0. + exact: is_part_decr_nth. + exact: add_corner_decr_nth. + exact: Hrc. + by rewrite eq_sym. + move: Hc; rewrite eq_sym HBeta -Hp. by rewrite nth_incr_nth eq_refl add1n. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure