proposition: Lemma Dade_Ind_expansion B g : B \in calP -> [/\ g \notin Atau -> ('Ind[G, 'M(B)] 'aa_B) g = 0 & {in A, forall a, g \in dd1 a -> ('Ind[G, 'M(B)] 'aa_B) g = (aa a / #|'M(B)|%:R) * \sum_(b in 'N_L(B) :&: a ^: L) #|calA g ('H(B) :* b)|%:R}].
proof: Proof. move=> dB; set LHS := 'Ind _ g. have defMB := Dade_set_sdprod dB; have [_ mulHNB nHNB tiHNB] := sdprodP defMB. have [sHMB sNMB] := mulG_sub mulHNB. have{LHS} ->: LHS = #|'M(B)|%:R^-1 * \sum_(x in calA g 'M(B)) 'aa_B (g ^ x). rewrite {}/LHS cfIndE ?sMG //; congr (_ * _). rewrite (bigID [pred x | g ^ x \in 'M(B)]) /= addrC big1 ?add0r => [|x]. by apply: eq_bigl => x; rewrite inE. by case/andP=> _ notMgx; rewrite cfun0. pose fBg x := remgr 'H(B) 'N_L(B) (g ^ x). pose supp_aBg := [pred b in A | g \in dd1 b]. have supp_aBgP: {in calA g 'M(B), forall x, ~~ supp_aBg (fBg x) -> 'aa_B (g ^ x)%g = 0}. - move=> x /setIdP[]; set b := fBg x => Gx MBgx notHGx; rewrite rDadeE // MBgx. have Nb: b \in 'N_L(B) by rewrite mem_remgr ?mulHNB. have Cb: b \in 'C_L[b] by rewrite inE cent1id; have [-> _] := setIP Nb. rewrite (cfun_on0 CFaa) // -/(fBg x) -/b; apply: contra notHGx => Ab. have nHb: b \in 'N('H(B)) by rewrite (subsetP nHNB). have [sBA /set0Pn[a Ba]] := setIdP dB; have Aa := subsetP sBA a Ba. have [|/= partHBb _] := partition_cent_rcoset nHb. rewrite (coprime_dvdr (order_dvdG Cb)) //= ['H(B)](bigD1 a) //=. by rewrite (coprimeSg (subsetIl _ _)) ?coHL. have Hb_gx: g ^ x \in 'H(B) :* b by rewrite mem_rcoset mem_divgr ?mulHNB. have [defHBb _ _] := and3P partHBb; rewrite -(eqP defHBb) in Hb_gx. case/bigcupP: Hb_gx => Cy; case/imsetP=> y HBy ->{Cy} Cby_gx. have sHBa: 'H(B) \subset H a by rewrite bigcap_inf. have sHBG: 'H(B) \subset G := subset_trans sHBa (sHG a). rewrite Ab -(memJ_conjg _ x) class_supportGidr // -(conjgKV y (g ^ x)). rewrite imset2_f // ?(subsetP sHBG) {HBy}// -mem_conjg. apply: subsetP Cby_gx; rewrite {y}conjSg mulSg //. have [nsHb _ defCb _ _] := sdprod_context (defCA Ab). have [hallHb _] := coprime_mulGp_Hall defCb (pi'H b) (piCL Ab). rewrite (sub_normal_Hall hallHb) ?setSI // (pgroupS _ (pi'H a)) //=. by rewrite subIset ?sHBa. split=> [notHGg | a Aa Hag]. rewrite big1 ?mulr0 // => x; move/supp_aBgP; apply; set b := fBg x. by apply: contra notHGg; case/andP=> Ab Hb_x; apply/bigcupP; exists b. rewrite -mulrA mulrCA; congr (_ * _); rewrite big_distrr /=. set nBaL := _ :&: _; rewrite (bigID [pred x | fBg x \in nBaL]) /= addrC. rewrite big1 ?add0r => [|x /andP[calAx not_nBaLx]]; last first. apply: supp_aBgP => //; apply: contra not_nBaLx. set b := fBg x => /andP[Ab Hb_g]; have [Gx MBx] := setIdP calAx. rewrite inE mem_remgr ?mulHNB //; apply/imsetP/Dade_support1_TI => //. by apply/pred0Pn; exists g; apply/andP. rewrite (partition_big fBg (mem nBaL)) /= => [|x]; last by case/andP. apply: eq_bigr => b; case/setIP=> Nb aLb; rewrite mulr_natr -sumr_const. apply: eq_big => x; rewrite ![x \in _]inE -!andbA. apply: andb_id2l=> Gx; apply/and3P/idP=> [[Mgx _] /eqP <- | HBb_gx]. by rewrite mem_rcoset mem_divgr ?mulHNB. suffices ->: fBg x = b. by rewrite inE Nb (subsetP _ _ HBb_gx) // -mulHNB mulgS ?sub1set. by rewrite /fBg; have [h Hh ->] := rcosetP HBb_gx; apply: remgrMid. move/and4P=> [_ Mgx _ /eqP def_fx]. rewrite rDadeE // Mgx -/(fBg x) def_fx; case/imsetP: aLb => y Ly ->. by rewrite cfunJ // (subsetP sAL). Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice) mathcomp(fintype tuple finfun bigop prime ssralg poly finset center) mathcomp(fingroup morphism perm automorphism quotient action zmodp) mathcomp(gfunctor gproduct cyclic pgroup frobenius ssrnum) mathcomp(matrix mxalgebra mxrepresentation vector algC classfun character) mathcomp(inertia vcharacter) odd_order(PFsection1)