proposition: Lemma FTtypeP_sum_nonFitting_lb : \sum_(x in G0) (`|tau1 lambda x| ^+ 2 + `|eta_ #1 0 x| ^+ 2) >= #|G0|%:R.
proof: Proof. pose A (xi : 'CF(G)) := [set x in G0 | xi x != 0]. suffices A_ub xi: xi \in dirr G -> #|A xi|%:R <= \sum_(x in G0) `|xi x| ^+ 2. apply: le_trans (_ : (#|A (tau1 lambda)| + #|A (eta_ #1 0)|)%:R <= _). rewrite leC_nat -cardsUI /A !setIdE -setIUr (leq_trans _ (leq_addr _ _)) //. rewrite subset_leq_card // subsetIidl. by apply/subsetP=> x /cover_G0/orP; rewrite !inE. rewrite natrD big_split lerD ?A_ub ?cycTIiso_dirr //. have [[[Itau1 Ztau1] _] [Ilam _]] := (cohS, andP irrHlam). by rewrite dirrE Ztau1 ?Itau1 ?mem_zchar //= irrWnorm. case/dirrP=> d [t Dxi]; rewrite (big_setID [set x | xi x != 0]) /= addrC. rewrite -setIdE -/(A _) big1 ?add0r => [|x]; last first. by rewrite !inE negbK => /andP[/eqP-> _]; rewrite normr0 expr0n. rewrite -sum1_card !(partition_big_imset (@cycle _)) /= natr_sum. apply: ler_sum => _ /imsetP[x Ax ->]. pose B := [pred y | generator <[x]> y]; pose phi := 'Res[<[x]>] 'chi_t. have defA: [pred y in A xi | <[y]> == <[x]>] =i B. move=> y; rewrite inE /= eq_sym andb_idl // !inE => eq_xy. have LGxy L (LG := class_support L G): x \notin LG -> y \notin LG. rewrite /LG class_supportEr; apply: contra => /bigcupP[g Gg Lg_y]. apply/bigcupP; exists g => //; move: Lg_y. by rewrite -!cycle_subG (eqP eq_xy). move: Ax; rewrite !inE !negb_or -andbA => /and3P[/LGxy-> /LGxy->]. apply: contraNneq => chi_y_0. have [k co_k_y ->]: exists2 k, coprime k #[y] & x = (y ^+ k)%g. have Yx: generator <[y]> x by rewrite [generator _ _]eq_sym. have /cycleP[k Dx] := cycle_generator Yx; exists k => //. by rewrite coprime_sym -generator_coprime -Dx. have Zxi: xi \in 'Z[irr G] by rewrite Dxi rpredZsign irr_vchar. have [uu <- // _] := make_pi_cfAut [group of G] co_k_y. by rewrite cfunE chi_y_0 rmorph0. have resB: {in B, forall y, `|xi y| ^+ 2 = `|phi y| ^+ 2}. move=> y /cycle_generator Xy. by rewrite Dxi cfunE normrMsign cfResE ?subsetT. rewrite !(eq_bigl _ _ defA) sum1_card (eq_bigr _ resB). apply: sum_norm2_char_generators => [|y By]. by rewrite cfRes_char ?irr_char. rewrite -normr_eq0 -sqrf_eq0 -resB // sqrf_eq0 normr_eq0. by move: By; rewrite -defA !inE -andbA => /and3P[]. 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)