proposition: Lemma Dade_cover_inequality (chi : 'CF(G)) (G0 := G :\: \bigcup_i Atau i) : '[chi] = 1 -> #|G|%:R^-1 * (\sum_(g in G0) `|chi g| ^+ 2 - #|G0|%:R) + \sum_i ('[chi^\rho]_(L i) - #|A i|%:R / #|L i|%:R) <= 0.
proof: Proof. move=> Nchi1; set vG := _^-1; rewrite sumrB /= addrCA mulrBr -addrA. pose F (xi : 'CF(G)) (B : {set gT}) := vG * \sum_(g in B) `|xi g| ^+ 2. have sumF xi: F xi G0 + \sum_i F xi (Atau i) = '[xi]. rewrite (cfnormE (cfun_onG _)) -mulr_sumr -mulrDr; congr (_ * _). rewrite -partition_disjoint_bigcup //=; set U_A := \bigcup_i _. have sUG: U_A \subset G by apply/bigcupsP=> i _; apply: Dade_support_sub. by rewrite -(setIidPr sUG) addrC -big_setID. have ->: \sum_i #|A i|%:R / #|L i|%:R = \sum_i F 1 (Atau i). apply: eq_bigr => i _; apply/eqP; rewrite /F. have [[/andP[sAL nAL] _ _ _ _] sHG] := (ddA i, Dade_signalizer_sub (ddA i)). rewrite -{1}[A i]setIid -cfdot_cfuni /normal ?sAL // -(invDade_cfun1 (ddA i)). rewrite leC_cfnorm_invDade_support; apply/forall_inP=> a Aa. by apply/forall_inP=> x Hx; rewrite !cfun1E groupMl // (subsetP (sHG a)). have ->: vG * #|G0|%:R = F 1 G0. congr (_ * _); rewrite -sumr_const; apply: eq_bigr => x /setDP[Gx _]. by rewrite cfun1E Gx normr1 expr1n. rewrite -opprD sumF cfnorm1 -Nchi1 -sumF opprD addNKr -oppr_ge0 opprB -sumrB. by rewrite sumr_ge0 // => i _; rewrite subr_ge0 leC_cfnorm_invDade_support. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop order prime ssralg poly finset center) mathcomp(fingroup morphism perm automorphism quotient action zmodp) mathcomp(gfunctor gproduct cyclic pgroup commutator nilpotent frobenius) mathcomp(matrix mxalgebra mxrepresentation) odd_order(BGsection3) mathcomp(vector ssrnum algC classfun character inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection4 PFsection5 PFsection6)