proposition: Lemma invDade_seqInd_sum : perm_eq calT (xi0 :: S) -> is_invDade_seqInd_sum.
proof: Proof. move=> defT; pose chi0 := \sum_(xi <- S) (c xi)^* / '[xi] *: xi. have Txi0: xi0 \in calT by rewrite (perm_mem defT) mem_head. have sST : {subset S <= calT}. by move=> xi Sxi; rewrite (perm_mem defT) mem_behead. have nz_xi01 : xi0 1%g != 0 by apply: seqInd1_neq0 Txi0. have part_a: {in A, chi^\rho =1 chi0}. pose phi := (chi^\rho - chi0) * '1_A. have Aphi : phi \in 'CF(L, A) := mul_cfuni_on A _. suffices: '[phi, chi^\rho - chi0] == 0; last clearbody phi. rewrite -(eq_cfdotr Aphi (eq_mul_cfuni _ nsAL)) cfnorm_eq0 => /eqP phi0. by move=> x Ax; rewrite -[chi0]add0r -phi0 cfunE eq_mul_cfuni ?cfunE ?subrK. have{Aphi} [Hphi phi1]: phi \in 'CF(L, H) /\ phi 1%g = 0. by move: Aphi; rewrite cfun_onD1 => /andP[-> /eqP]. have{Hphi} def_phi: phi = e^-1 *: 'Ind ('Res[H] phi). apply/cfunP=> y; have [Hy | notHy] := boolP (y \in H); last first. by rewrite cfunE !(cfun_on0 _ notHy) ?mulr0 ?cfInd_normal. rewrite cfunE cfIndE // mulrA -invfM eh. apply: (canRL (mulKf nzL)); rewrite mulr_natl -sumr_const. by apply: eq_bigr => z Lz; rewrite cfResE ?memJ_norm ?cfunJ ?(subsetP nHL). have{def_phi} Tphi: phi \in <<calT>>%VS. rewrite def_phi memvZ // ['Res _]cfun_sum_cfdot linear_sum. apply: memv_suml => i _; rewrite linearZ memvZ ?memv_span //=. by apply/seqIndP; exists i; rewrite ?inE. have{Tphi} [z def_phi _] := free_span (seqInd_free nsHL _) Tphi. have {phi def_phi phi1} ->: phi = \sum_(xi <- S) z xi *: psi xi. rewrite def_phi (perm_big _ defT) !big_cons /= 2!cfunE in phi1 *. rewrite (canRL (mulfK nz_xi01) (canRL (addrK _) phi1)) add0r addrC mulNr. rewrite sum_cfunE mulr_suml scaleNr scaler_suml -sumrB. by apply: eq_bigr => xi _; rewrite cfunE -mulrA -scalerA -scalerBr. rewrite cfdot_suml big1_seq //= => xi Sxi; have Txi := sST xi Sxi. rewrite cfdotZl cfdotBr -invDade_reciprocity -/(c xi); last first. rewrite cfun_onD1 !cfunE divfK // subrr eqxx andbT. by rewrite memvB ?memvZ //= ((seqInd_on _) setT). have [oSS /orthoPl o_xi0S]: pairwise_orthogonal S /\ orthogonal xi0 S. have:= seqInd_orthogonal nsHL setT; rewrite (eq_pairwise_orthogonal defT). by rewrite /= -cat1s pairwise_orthogonal_cat => /and3P[]. rewrite cfdotBl cfdotC cfproj_sum_orthogonal {oSS}// cfdotZl cfdot_sumr. rewrite big1_seq ?mulr0 => [|mu Smu]; last by rewrite cfdotZr o_xi0S ?mulr0. by rewrite subr0 divfK ?(cfnorm_seqInd_neq0 _ Txi) // conjCK subrr mulr0. split=> [x /part_a-> | ]. by rewrite sum_cfunE; apply: eq_bigr => ?; rewrite cfunE. rewrite (cfdotEl _ (invDade_on ddA _)) mulrC mulr_suml. pose F xi mu x := uc c xi mu * (xi x * (mu x)^*) / #|L|%:R. transitivity (\sum_(x in A) \sum_(xi <- S) \sum_(mu <- S) F xi mu x). apply: eq_bigr => x Ax; rewrite part_a // sum_cfunE -mulrA mulr_suml. apply: eq_bigr => xi _; rewrite mulrA -mulr_suml rmorph_sum; congr (_ * _). rewrite mulr_sumr; apply: eq_bigr => mu _; rewrite !cfunE (cfdotC mu). rewrite -{1}[mu x]conjCK -fmorph_div -rmorphM/= conjCK -3!mulrA 2!(mulrCA _^-1). by rewrite (mulrA _^-1) -invfM 2!(mulrCA (xi x)) mulrA 2!(mulrA _^*). rewrite exchange_big; apply: eq_bigr => xi _; rewrite exchange_big /=. apply: eq_big_seq => mu Smu; have Tmu := sST mu Smu. rewrite /u eh (cfdotEr _ (seqInd_on nsHL Tmu)) (mulrC _^-1) -mulrBl mulrA. rewrite -mulr_suml -mulr_sumr (big_setD1 1%g (group1 H)) /=; congr (_ * _ * _). by rewrite addrC conj_Cnat ?addKr // (Cnat_seqInd1 Tmu). Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop order prime ssralg poly finset center) mathcomp(fingroup morphism perm automorphism quotient action zmodp) mathcomp(gfunctor gproduct cyclic pgroup commutator nilpotent frobenius) mathcomp(matrix mxalgebra mxrepresentation) odd_order(BGsection3) mathcomp(vector ssrnum algC classfun character inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection4 PFsection5 PFsection6)