proposition: Lemma FTtypeP_sum_cycTIiso10_lb : \sum_(x in H^#) `|eta10 x| ^+ 2 >= #|H^#|%:R.
proof: Proof. pose mu1 := mu_ #1; have S1mu1: mu1 \in calS1 by rewrite S1mu ?Iirr1_neq0. have Zeta10: eta10 \in 'Z[irr G] by rewrite cycTIiso_vchar. have [tau1 cohS [b _ Dtau1]] := FTtypeP_coherence. have{b Dtau1} oS1eta10: {in calS1, forall zeta, '[tau1 zeta, eta10] = 0}. move=> zeta /S1cases[[j nz_j ->] | /o_tau1_eta-> //]. rewrite Dtau1 // cfdotZl cfdot_suml big1 ?mulr0 // => i _. by rewrite cfdot_cycTIiso signW2_eq0 (negPf nz_j) andbF. have [_ /oS1eta10//|alpha [Zalpha kerPalpha]] := calS1_split1 cohS S1mu1 Zeta10. rewrite {}oS1eta10 // expr0n mulr0 !mul0r subrr add0r => [[Deta10 -> ub_alpha]]. have{} Deta10: {in H^#, eta10 =1 alpha}. by move=> x /Deta10; rewrite !mul0r add0r. set a1_2 := alpha 1%g ^+ 2 in ub_alpha. have Dsum_alpha: \sum_(x in H^#) `|alpha x| ^+ 2 = #|H|%:R * '[alpha] - a1_2. rewrite (cfnormE (cfun_onG _)) mulVKf ?neq0CG // (big_setD1 _ (group1 H)) /=. by rewrite addrC Cint_normK ?addKr ?Cint_vchar1. have [/mulG_sub[sPH _] [_ _ _ [_ _ sW2P _ _] _]] := (dprodW defH, StypeP). have nz_alpha: alpha != 0. have [[x W2x ntx] [y W1y nty]] := (trivgPn _ ntW2, trivgPn _ ntW1). have [eps pr_eps] := C_prim_root_exists (prime_gt0 pr_q). have [_ mulW12 cW12 tiW12] := dprodP defW. have [sW1W sW2W] := mulG_sub mulW12. 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 eta10x: (eta10 x == eta10 (y * x)%g %[mod 1 - eps])%A. by rewrite eqAmod_sym (vchar_ker_mod_prim pr_eps) ?in_setT. have eta10xy: (eta10 (y * x)%g == 1 %[mod 1 - eps])%A. rewrite cycTIiso_restrict; last first. rewrite !inE -mulW12 mem_mulg // andbT groupMl ?groupMr // -[_ || _]andTb. by rewrite andb_orr -{1}W2x -W1y andbC -!in_setI tiW12 !inE (negPf ntx). have {2}<-: w_ #1 0 x = 1. rewrite -[x]mul1g /w_ dprod_IirrE cfDprodE // irr0 cfun1E W2x mulr1. by rewrite lin_char1 ?irr_cyclic_lin. rewrite (vchar_ker_mod_prim pr_eps) ?(subsetP sW1W y) ?(subsetP sW2W) //. by rewrite irr_vchar. have: (alpha x == 1 %[mod 1 - eps])%A. rewrite -Deta10; last by rewrite !inE ntx (subsetP sPH) ?(subsetP sW2P). exact: eqAmod_trans eta10x eta10xy. apply: contraTneq => ->; rewrite cfunE eqAmod_sym. apply/negP=> /(int_eqAmod_prime_prim pr_eps pr_q (rpred1 _))/idPn[]. by rewrite (dvdC_nat q 1) -(subnKC qgt2). apply: wlog_neg => suma_lt_H. suffices{ub_alpha} lb_a1_2: a1_2 >= #|H^#|%:R. have Pgt2: (2 < #|P|)%N by apply: leq_trans (subset_leq_card sW2P). apply: le_trans (le_trans lb_a1_2 _) ub_alpha. rewrite ler_pMl ?(lt_le_trans _ lb_a1_2) ?ler1n ?ltr0n //. by rewrite -(subnKC Pgt2). have:= leq_trans (ltnW Pgt2) (subset_leq_card sPH). by rewrite [in X in X -> _](cardsD1 1%g) group1. have /CnatP[n Dn]: '[alpha] \in Cnat by rewrite Cnat_cfnorm_vchar. have /CnatP[m Dm]: a1_2 \in Cnat by rewrite Cnat_exp_even ?Cint_vchar1. rewrite Dm leC_nat leqNgt; apply: contra suma_lt_H => a1_2_lt_H. rewrite {1}Dsum_alpha Dn Dm -natrM lerBrDl (cardsD1 1%g H) group1 /=. case Dn1: n => [|[|n1]]; first by rewrite -cfnorm_eq0 Dn Dn1 eqxx in nz_alpha. have /dirrP[b [i Dalpha]]: alpha \in dirr H by rewrite dirrE Zalpha Dn Dn1 /=. rewrite -Dm /a1_2 Dalpha cfunE exprMn sqrr_sign mul1r muln1 mulrS lerD2r. by rewrite lin_char1 ?expr1n //; apply/char_abelianP. rewrite -natrD leC_nat -add2n mulnDr (addnC 1%N) mulnDl -addnA. by apply: leq_trans (leq_addr _ _); rewrite muln2 -addnn leq_add2r ltnW. 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)