proposition: Lemma FTtypeP_sum_cycTIiso01_lb : \sum_(x in H^#) `|eta01 x| ^+ 2 >= #|PU|%:R - (u ^ 2)%:R.
proof: Proof. have [tau1 cohS [b _ Dtau1]] := FTtypeP_coherence. have Zeta01: eta01 \in 'Z[irr G] by rewrite cycTIiso_vchar. pose j1 := signW2 b #1; pose d : algC := (-1) ^+ b; pose mu1 := mu_ j1. have nzj1: j1 != 0 by [rewrite signW2_eq0 ?Iirr1_neq0]; have S1mu1 := S1mu nzj1. have o_mu_eta01 j: j != 0 -> '[tau1 (mu_ j), eta01] = d *+ (j == j1). move/Dtau1->; rewrite -/d cfdotZl cfdot_suml big_ord_recl /=. rewrite cfdot_cycTIiso andTb (inv_eq (signW2K b)). by rewrite big1 ?addr0 ?mulr_natr // => i _; rewrite cfdot_cycTIiso. have [zeta | alpha [Zalpha kerPalpha [_]]] := calS1_split1 cohS S1mu1 Zeta01. case/S1cases=> [[j nz_j ->] | /o_tau1_eta-> //]. by rewrite o_mu_eta01 // (inj_eq (prTIred_inj _)) => /negPf->. rewrite o_mu_eta01 // eqxx mulrb => -> lb_alpha. rewrite -lerBlDl cfnorm_prTIred -/q mulrAC sqrr_sign mul1r. rewrite mu1uq // natrM exprMn (mulrAC _ q%:R) (mulrA _ q%:R) !mulfK ?neq0CG //. rewrite natrX -(sdprod_card defS) natrM -mulrBl mulfK ?neq0CG //. rewrite addrC opprB subrK mulrACA; apply: le_trans lb_alpha. apply: le_trans (P1_int2_lb _) _; first by rewrite rpredMsign Cint_vchar1. by rewrite exprMn sqrr_sign mul1r lexx. 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)