proposition: Lemma FTtypeP_sum_Ind_Fitting_lb (tau1 : {additive _ -> _}) lambda : coherent_with calS S^# tau tau1 -> lambda \in irrIndH -> lambda \in calS -> \sum_(x in H^#) `|tau1 lambda x| ^+ 2 >= #|S|%:R - lambda 1%g ^+ 2.
proof: Proof. move=> cohS /andP[Ilam Hlam] Slam; have [[Itau1 Ztau1] _] := cohS. have Zlam1: tau1 lambda \in 'Z[irr G] by rewrite Ztau1 ?mem_zchar. have S1lam: lambda \in calS1. have [[s kerP's Ds] [r _ Dr]] := (seqIndP Slam, seqIndP Hlam). rewrite Dr mem_seqInd ?gFnormal ?normal1 // !inE !sub1G !andbT in kerP's *. rewrite -(sub_cfker_Ind_irr r (gFsub _ _) (gFnorm _ _)) /= -Dr. by rewrite Ds sub_cfker_Ind_irr ?gFsub ?gFnorm. have [|alpha [Zalpha kerPalpha]] := calS1_split1 cohS S1lam Zlam1. move=> zeta S1zeta lam'zeta; rewrite Itau1 ?sS1S //. suffices: pairwise_orthogonal calS1 by case/pairwise_orthogonalP=> _ ->. by rewrite seqInd_orthogonal ?gFnormal. rewrite Itau1 ?mem_zchar // irrWnorm // expr1n !divr1 mul1r => [[Dlam ->]]. rewrite mulr1 -lerBlDl addrC opprB subrK calHuq //; apply: le_trans. have [[x W2x ntx] [y W1y nty]] := (trivgPn _ ntW2, trivgPn _ ntW1). have [_ _ _ [_ _ sW2P _ _] _] := StypeP; have Px := subsetP sW2P x W2x. have [eps pr_eps] := C_prim_root_exists (prime_gt0 pr_q). have{y W1y W2x nty} lamAmod: (tau1 lambda x == lambda x %[mod 1 - eps])%A. have [_ /mulG_sub[_ sW1S] _ tiPUW1] := sdprodP defS. have [_ /mulG_sub[sW1W sW2W] cW12 _] := dprodP defW. have /mulG_sub[sPPU _] := sdprodW defPU. have [o_y cxy]: #[y] = q /\ x \in 'C[y]. split; last by apply/cent1P; red; rewrite (centsP cW12). by apply: nt_prime_order => //; apply/eqP; rewrite -order_dvdn order_dvdG. have lam1yx: (tau1 lambda (y * x)%g == tau1 lambda x %[mod 1 - eps])%A. by rewrite (vchar_ker_mod_prim pr_eps) ?in_setT. have [Sx Sy] := (subsetP (gFsub _ _) x Px, subsetP sW1S y W1y). have PUx := subsetP sPPU x Px. have lam_yx: (lambda (y * x)%g == lambda x %[mod 1 - eps])%A. by rewrite (vchar_ker_mod_prim pr_eps) ?char_vchar ?(seqInd_char Slam). apply: eqAmod_trans lam_yx; rewrite eqAmod_sym; apply: eqAmod_trans lam1yx. have PUlam: lambda \in 'CF(S, PU) by rewrite (seqInd_on _ Slam) ?gFnormal. have PU'yx: (y * x)%g \notin PU. by rewrite groupMr //= -[y \in PU]andbT -W1y -in_setI tiPUW1 !inE. rewrite (cfun_on0 PUlam PU'yx) (ortho_cycTIiso_vanish pddS) //. apply/orthoPl=> _ /mapP[_ /(cycTIirrP defW)[i [j ->]] ->]. by rewrite (coherent_ortho_cycTIiso StypeP sSS0). rewrite !inE (groupMl x (subsetP sW1W y _)) // (subsetP sW2W) // andbT. rewrite groupMl // -[x \in _]andTb -PUx -in_setI tiPUW1 !inE negb_or ntx /=. by rewrite (contra _ PU'yx) // => /(subsetP sW2P)/(subsetP sPPU). have{x ntx Px lamAmod} alphaAmod: (alpha 1%g == 0 %[mod 1 - eps])%A. have Hx: x \in H by have/mulG_sub[/subsetP->] := dprodW defH. have:= lamAmod; rewrite -[lambda x]addr0 Dlam ?inE ?ntx // mul1r eqAmodDl. rewrite cfker1 // [alpha]cfun_sum_constt (subsetP (cfker_sum _ _ _)) //. rewrite !inE Hx (subsetP _ x Px) //; apply/bigcapsP=> i /kerPalpha. by rewrite !inE => /subset_trans-> //; apply: cfker_scale. have /dvdCP[b Zb ->]: (q %| alpha 1%g)%C. by rewrite (int_eqAmod_prime_prim pr_eps) // Cint_vchar1. rewrite natrM mulrACA exprMn !mulrA 2?ler_pM2r ?gt0CG //. by rewrite -[_ * b * b]mulrA P1_int2_lb. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop order prime binomial ssralg poly finset) mathcomp(fingroup morphism perm automorphism quotient action finalg zmodp) mathcomp(gfunctor gproduct center cyclic commutator gseries nilpotent) mathcomp(pgroup sylow hall abelian maximal frobenius) mathcomp(matrix mxalgebra mxrepresentation mxabelem vector) odd_order(BGsection1 BGsection3 BGsection7) odd_order(BGsection14 BGsection15 BGsection16) mathcomp(ssrnum rat algC cyclotomic algnum) mathcomp(classfun character integral_char inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3 PFsection4) odd_order(PFsection5 PFsection6 PFsection7 PFsection8 PFsection9) odd_order(PFsection10 PFsection11 PFsection12)