proposition: Lemma Dade_expansion : aa^\tau = - \sum_(B in calB) (- 1) ^+ #|B| *: 'Ind[G, 'M(B)] 'aa_B.
proof: Proof. apply/cfunP=> g; rewrite !cfunElock sum_cfunE. pose n1 (B : {set gT}) : algC := (-1) ^+ #|B| / #|L : 'N_L(B)|%:R. pose aa1 B := ('Ind[G, 'M(B)] 'aa_B) g. have dBJ: {acts L, on calP | 'Js}. move=> x Lx /= B; rewrite !inE -!cards_eq0 cardJg. by rewrite -{1}(normsP nAL x Lx) conjSg. transitivity (- (\sum_(B in calP) n1 B * aa1 B)); last first. congr (- _); rewrite {1}(partition_big_imset (fun B => repr (B :^: L))) /=. apply: eq_bigr => B /imsetP[B1 dB1 defB]. have B1L_B: B \in B1 :^: L by rewrite defB (mem_repr B1) ?orbit_refl. have{dB1} dB1L: {subset B1 :^: L <= calP}. by move=> _ /imsetP[x Lx ->]; rewrite dBJ. have dB: B \in calP := dB1L B B1L_B. rewrite (eq_bigl (mem (B :^: L))) => [|B2 /=]; last first. apply/andP/idP=> [[_ /eqP <-] | /orbit_trans/(_ B1L_B)-B1L_B2]. by rewrite orbit_sym (mem_repr B2) ?orbit_refl. by rewrite [B2 :^: L](orbit_eqP B1L_B2) -defB dB1L. rewrite (eq_bigr (fun _ => n1 B * aa1 B)) => [|_ /imsetP[x Lx ->]]. rewrite cfunE sumr_const -mulr_natr mulrAC card_orbit astab1Js divfK //. by rewrite pnatr_eq0 -lt0n indexg_gt0. rewrite /aa1 Dade_Ind_restr_J //; congr (_ * _). by rewrite /n1 cardJg -{1 2}(conjGid Lx) normJ -conjIg indexJg. case: pickP => /= [a /andP[Aa Ha_g] | notHAg]; last first. rewrite big1 ?oppr0 // /aa1 => B dB. have [->] := Dade_Ind_expansion g dB; first by rewrite mulr0. by apply/bigcupP=> [[a Aa Ha_g]]; case/andP: (notHAg a). pose P_ b := [set B in calP | b \in 'N_L(B)]. pose aa2 B b : algC := #|calA g ('H(B) :* b)|%:R. pose nn2 (B : {set gT}) : algC := (-1) ^+ #|B| / #|'H(B)|%:R. pose sumB b := \sum_(B in P_ b) nn2 B * aa2 B b. transitivity (- aa a / #|L|%:R * \sum_(b in a ^: L) sumB b); last first. rewrite !mulNr; congr (- _). rewrite (exchange_big_dep (mem calP)) => [|b B _] /=; last by case/setIdP. rewrite big_distrr /aa1; apply: eq_bigr => B dB; rewrite -big_distrr /=. have [_ /(_ a) -> //] := Dade_Ind_expansion g dB; rewrite !mulrA. congr (_ * _); last by apply: eq_bigl => b; rewrite inE dB /= andbC -in_setI. rewrite -mulrA mulrCA -!mulrA; congr (_ * _). rewrite -invfM mulrCA -invfM -!natrM; congr (_ / _%:R). rewrite -(sdprod_card (Dade_set_sdprod dB)) mulnA mulnAC; congr (_ * _)%N. by rewrite mulnC Lagrange ?subsetIl. rewrite (eq_bigr (fun _ => sumB a)) /= => [|_ /imsetP[x Lx ->]]; last first. rewrite {1}/sumB (reindex_inj (@conjsg_inj _ x)) /=. symmetry; apply: eq_big => B. rewrite ![_ \in P_ _]inE dBJ //. by rewrite -{2}(conjGid Lx) normJ -conjIg memJ_conjg. case/setIdP=> dB Na; have [sBA _] := setIdP dB. have defHBx: 'H(B :^ x) = 'H(B) :^ x. rewrite /'H(_) (big_imset _ (in2W (conjg_inj x))) -bigcapJ /=. by apply: eq_bigr => b Bb; rewrite DadeJ ?(subsetP sBA). rewrite /nn2 /aa2 defHBx !cardJg; congr (_ * _%:R). rewrite -(card_rcoset _ x); apply: eq_card => y. rewrite !(inE, mem_rcoset, mem_conjg) conjMg conjVg conjgK -conjgM. by rewrite groupMr // groupV (subsetP sLG). rewrite sumr_const mulrC [sumB a](bigD1 [set a]) /=; last first. by rewrite 3!inE cent1id sub1set Aa -cards_eq0 cards1 (subsetP sAL). rewrite -[_ *+ _]mulr_natr -mulrA mulrDl -!mulrA ['H(_)]big_set1 cards1. have ->: aa2 [set a] a = #|'C_G[a]|%:R. have [u x Ha_ux Gx def_g] := imset2P Ha_g. rewrite -(card_lcoset _ x^-1); congr _%:R; apply: eq_card => y. rewrite ['H(_)]big_set1 mem_lcoset invgK inE def_g -conjgM. rewrite -(groupMl y Gx) inE; apply: andb_id2l => Gxy. by have [_ _ -> //] := normedTI_memJ_P (Dade_cover_TI Aa); rewrite inE Gxy. rewrite mulN1r mulrC mulrA -natrM -(sdprod_card (defCA Aa)). rewrite -mulnA card_orbit astab1J Lagrange ?subsetIl // mulnC natrM. rewrite mulrAC mulfK ?neq0CG // mulrC divfK ?neq0CG // opprK. rewrite (bigID [pred B : {set gT} | a \in B]) /= mulrDl addrA. apply: canRL (subrK _) _; rewrite -mulNr -sumrN; congr (_ + _ * _). symmetry. rewrite (reindex_onto (fun B => a |: B) (fun B => B :\ a)) /=; last first. by move=> B; case/andP=> _; apply: setD1K. symmetry; apply: eq_big => B. rewrite setU11 andbT -!andbA; apply/and3P/and3P; case. do 2![case/setIdP] => sBA ntB /setIP[La nBa] _ notBa. rewrite 3!inE subUset sub1set Aa sBA La setU1K // -cards_eq0 cardsU1 notBa. rewrite -sub1set normsU ?sub1set ?cent1id //= eq_sym eqEcard subsetUl /=. by rewrite cards1 cardsU1 notBa ltnS leqn0 cards_eq0. do 2![case/setIdP] => /subUsetP[_ sBA] _ /setIP[La]. rewrite inE conjUg (normP (cent1id a)) => /subUsetP[_ sBa_aB]. rewrite eq_sym eqEcard subsetUl cards1 (cardsD1 a) setU11 ltnS leqn0 /=. rewrite cards_eq0 => notB0 /eqP defB. have notBa: a \notin B by rewrite -defB setD11. split=> //; last by apply: contraNneq notBa => ->; apply: set11. rewrite !inE sBA La -{1 3}defB notB0 subsetD1 sBa_aB. by rewrite mem_conjg /(a ^ _) invgK mulgA mulgK. do 2![case/andP] => /setIdP[dB Na] _ notBa. suffices ->: aa2 B a = #|'H(B) : 'H(a |: B)|%:R * aa2 (a |: B) a. rewrite /nn2 cardsU1 notBa exprS mulN1r !mulNr; congr (- _). rewrite !mulrA; congr (_ * _); rewrite -!mulrA; congr (_ * _). apply: canLR (mulKf (neq0CG _)) _; apply: canRL (mulfK (neq0CG _)) _ => /=. by rewrite -natrM mulnC Lagrange //= Dade_setU1 ?subsetIl. rewrite /aa2 Dade_setU1 //= -natrM; congr _%:R. have defMB := Dade_set_sdprod dB; have [_ mulHNB nHNB tiHNB] := sdprodP defMB. have [sHMB sNMB] := mulG_sub mulHNB; have [La nBa] := setIP Na. have nHa: a \in 'N('H(B)) by rewrite (subsetP nHNB). have Ca: a \in 'C_L[a] by rewrite inE cent1id La. have [|/= partHBa nbHBa] := partition_cent_rcoset nHa. have [sBA] := setIdP dB; case/set0Pn=> b Bb; have Ab := subsetP sBA b Bb. rewrite (coprime_dvdr (order_dvdG Ca)) //= ['H(B)](bigD1 b) //=. by rewrite (coprimeSg (subsetIl _ _)) ?coHL. pose pHBa := mem ('H(B) :* a). rewrite -sum1_card (partition_big (fun x => g ^ x) pHBa) /= => [|x]; last first. by case/setIdP=> _ ->. rewrite (set_partition_big _ partHBa) /= -nbHBa -sum_nat_const. apply: eq_bigr => _ /imsetP[x Hx ->]. rewrite (big_imset _ (in2W (conjg_inj x))) /=. rewrite -(card_rcoset _ x) -sum1_card; symmetry; set HBaa := 'C_(_)[a] :* a. rewrite (partition_big (fun y => g ^ (y * x^-1)) (mem HBaa)); last first. by move=> y; rewrite mem_rcoset => /setIdP[]. apply: eq_bigr => /= u Ca_u; apply: eq_bigl => z. rewrite -(canF_eq (conjgKV x)) -conjgM; apply: andb_id2r; move/eqP=> def_u. have sHBG: 'H(B) \subset G. have [sBA /set0Pn[b Bb]] := setIdP dB; have Ab := subsetP sBA b Bb. by rewrite (bigcap_min b) ?sHG. rewrite mem_rcoset !inE groupMr ?groupV ?(subsetP sHBG x Hx) //=. congr (_ && _); have [/eqP defHBa _ _] := and3P partHBa. symmetry; rewrite def_u Ca_u -defHBa -(mulgKV x z) conjgM def_u -/HBaa. by rewrite cover_imset -class_supportEr imset2_f. 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)