proposition: Lemma Cauchy_symm_symh : Cauchy_kernel d = \sum_(la : 'P_d) ('h[la] : polY) *: ('m[la] : polXY).
proof: Proof. apply/mpolyP => mon. case/altP: (mdeg mon =P d) => Hdeg; first last. rewrite (dhomog_nemf_coeff (Cauchy_kernel_dhomog d) Hdeg). rewrite linear_sum /= big1 ?mcoeff0 // => la _. rewrite mcoeffZ. case: (ssrnat.leqP (size la) m) => [Hi | /symm_oversize ->]. - rewrite mcoeff_symm //. suff /negbTE -> : ~~ perm_eq (mpart (n := m) la) mon by rewrite mulr0. apply/negP => /perm_sumn. rewrite sumn_mpart // sumn_intpartn sumnE -/(mdeg _) => Hd. by rewrite -Hd eq_refl in Hdeg. - by rewrite mcoeff0 mulr0. have Hpm : is_part_of_n d (partm mon). by rewrite /= intpartP andbT sumn_partm Hdeg. pose pm := IntPartN Hpm. suff -> : (Cauchy_kernel d)@_mon = 'h[pm]. rewrite (bigID (fun mu : 'P_d => (size mu <= m)%N)) /=. rewrite linearD ![in RHS]linear_sum /=. rewrite addrC big1 ?add0r; first last. by move=> la; rewrite -ltnNge => /symm_oversize ->; rewrite !raddf0. rewrite (bigD1 pm) ?size_partm //= ?big1 ?addr0; first last. move=> la /andP[Hszla Hla]. rewrite mcoeffZ mcoeff_symm //. suff /negbTE -> : ~~ perm_eq (mpart (n := m) la) mon by rewrite mulr0. apply/negP => /perm_partm/(congr1 val)/=. rewrite mpartK // => Heq. by move: Hla; rewrite /eq_op /= Heq eq_refl. by rewrite mcoeffZ mcoeff_symm ?size_partm // perm_sym partm_permK mulr1. rewrite /Cauchy_kernel /prod_symh /prod_gen {1}/symh /= rmorph_prod /=. rewrite rmorph_sum raddf_sum /= partmE; apply esym. transitivity (\prod_(i <- mon) sympol 'h_i : polY ). rewrite [RHS](bigID (fun i => i == 0%N)) /=. rewrite [in RHS]big1 ?mul1r; first last => [i /eqP ->|]. exact: (congr1 val (symh0 n R)). rewrite /= -[RHS]big_filter; apply: perm_big. by rewrite perm_sort. rewrite {Hpm pm} /= big_tuple; symmetry. rewrite (bigID (fun mZ : 'X_{1.. _ < _} => monX mZ == mon)) /=. rewrite addrC big1 ?add0r; first last. move=> i /andP[_ /negbTE Hneq]. rewrite evalXY_XE -rmorph_prod /= polyXY_scale. by rewrite linearZ /= /polX_XY map_mpolyX mcoeffX Hneq mulr0. under eq_bigl=> i do [rewrite andb_idl; last by move=> /eqP; rewrite -{3}Hdeg => <-; rewrite mdeg_monX]. under [LHS]eq_bigr => mz Hmz. rewrite evalXY_XE -rmorph_prod /= polyXY_scale. by rewrite linearZ /= /polX_XY map_mpolyX mcoeffX Hmz mulr1 over. under [RHS]eq_bigr => i _ do [rewrite (@symh_pol_any _ _ d.+1) //; last by rewrite ltnS -Hdeg /mdeg big_tuple (bigD1 i) // leq_addr]. rewrite bigA_distr_big_dep => /=. rewrite (reindex (famY (d := d))) /=; last exact: famY_bij. apply eq_big => [mz | mz /eqP Hmz]. - apply/eqP/familyP => [/= Hmon i | Hfam]. + by rewrite unfold_in ffunE /= mdeg_tnth_monsY Hmon. + apply/mnmP => i. have := Hfam i; rewrite unfold_in /= !mnm_tnth => /eqP <-. rewrite ffunE /= !tnth_mktuple mdegE. by apply eq_bigr => j _; rewrite mnmE. - by apply eq_bigr => i _; rewrite ffunE /= !tnth_mktuple. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssrint rat ssralg ssrnum algC matrix vector) mathcomp(mpoly) tools partition ordtype antisym Schur_mpoly Schur_altdef sympoly homogsym permcent