proposition: Lemma FTtypeP_compl_ker_ratio_lb : m * (p ^ q.-1)%:R / q%:R < u%:R / c%:R.
proof: Proof. have [tau1 cohS cohSmu] := FTtypeP_coherence maxS StypeP. pose lam1 := tau1 lambda; pose eta10 := eta_ #1 0. pose H1G := class_support H^# G; pose K1G := class_support K^# G. pose G0 := ~: (class_support H G :|: class_support K G). pose invJ (f : gT -> algC) := forall y x, f (x ^ y) = f x. pose nm2 (chi : 'CF(G)) x := `|chi x| ^+ 2; pose g : algC := #|G|%:R. have injJnm2 chi: invJ (nm2 chi) by move=> y x; rewrite /nm2 cfunJ ?inE. have nm2_dirr chi: chi \in dirr G -> g^-1 <= nm2 chi 1%g / g. case/dIrrP=> d ->; rewrite -{1}[g^-1]mul1r ler_pM2r ?invr_gt0 ?gt0CG //. rewrite expr_ge1 ?normr_ge0 // cfunE normrMsign. by rewrite irr1_degree normr_nat ler1n irr_degree_gt0. pose mean (F M : {set gT}) (f : gT -> algC) := (\sum_(x in F) f x) / #|M|%:R. have meanTI M (F := 'F(gval M)^#) (FG := class_support F G) f: M \in 'M -> normedTI F G M -> invJ f -> mean FG G f = mean F M f. - move=> maxM /and3P[ntF tiF /eqP defN] fJ; apply: canLR (mulfK (neq0CG _)) _. rewrite (set_partition_big _ (partition_class_support ntF tiF)) /=. rewrite mulrAC -mulrA -natf_indexg ?subsetT //=. have ->: #|G : M| = #|F :^: G| by rewrite card_conjugates defN. rewrite mulr_natr -sumr_const; apply: eq_bigr => _ /imsetP[y _ ->]. by rewrite (big_imset _ (in2W (conjg_inj _))) (eq_bigr _ (in1W (fJ y))). have{meanTI} meanG f : invJ f -> mean G G f = f 1%g / g + mean H^# S f + mean K^# T f + mean G0 G f. - have type24 maxM := compl_of_typeII_IV maxM _ (FTtype5_exclusion maxM). have tiH: normedTI H^# G S by have/type24[] := StypeP. have{type24} tiK: normedTI K^# G T by have/type24[] := TtypeP. move=> fJ; rewrite -!meanTI // {1}/mean (big_setD1 1%g) // (big_setID H1G) /=. rewrite [in rhs in _ + (_ + rhs)](big_setID K1G) /= -/g -!mulrDl !addrA. congr ((_ + _ + _ + _) / g); rewrite ?(setIidPr _) // /H1G /K1G. + by rewrite class_supportEr -cover_imset -class_supportD1 setSD ?subsetT. + rewrite subsetD -setI_eq0 setIC tiHK eqxx andbT. by rewrite class_supportEr -cover_imset -class_supportD1 setSD ?subsetT. rewrite !class_supportEr -!cover_imset -!class_supportD1. apply: eq_bigl => x; rewrite !inE andbT -!negb_or orbCA orbA orbC. by case: (x =P 1%g) => //= ->; rewrite mem_class_support ?group1. have lam1_ub: mean G0 G (nm2 lam1) <= lambda 1%g ^+ 2 / #|S|%:R - g^-1. have [[Itau1 Ztau1] _] := cohS. have{Itau1} n1lam1: '[lam1] = 1 by rewrite Itau1 ?mem_zchar ?irrWnorm. have{Ztau1} Zlam1: lam1 \in 'Z[irr G] by rewrite Ztau1 ?mem_zchar. rewrite -lerN2 opprB -(lerD2l '[lam1]) {1}n1lam1 addrCA. rewrite (cfnormE (cfun_onG _)) (mulrC g^-1) [_ / g](meanG (nm2 _)) // addrK. rewrite -addrA lerD ?nm2_dirr //; first by rewrite dirrE Zlam1 n1lam1 /=. rewrite ler_wpDr ?divr_ge0 ?ler0n //. by apply: sumr_ge0 => x _; rewrite exprn_ge0 ?normr_ge0. rewrite ler_pdivlMr ?gt0CG // mulrBl mul1r divfK ?neq0CG //. by rewrite (FTtypeP_sum_Ind_Fitting_lb StypeP). pose ub_lam1 : algC := (#|T^`(1)%g|%:R - (v ^ 2)%:R - #|Q|.-1%:R) / #|T|%:R. have [_ D_1 Dv] := T_Galois. have defK : K = Q by have [<-] := typeP_context TtypeP; rewrite D_1 dprodg1. have eta10_ub: mean G0 G (nm2 (eta_ #1 0)) <= #|G0|%:R / g - ub_lam1. rewrite -lerN2 opprB -(lerD2l '[eta_ #1 0]) {2}(cfnormE (cfun_onG _)). rewrite (mulrC g^-1) [_ / g in rhs in _ <= rhs](meanG (nm2 _)) // addrK. have ->: '[eta_ #1 0] = mean G G (fun _ => 1). by rewrite /mean sumr_const cfdot_cycTIiso eqxx divff ?neq0CG. rewrite meanG // [in lhs in lhs <= _]/mean !sumr_const addrACA subrr addr0. rewrite [lhs in lhs <= _]addrAC -addrA -mulrDl (cardsD1 1%g Q) group1 -defK. rewrite mul1r subrK ?lerD ?ler_pM2r ?invr_gt0 ?gt0CG //. - by rewrite nm2_dirr ?cycTIiso_dirr. - exact: (FTtypeP_sum_cycTIiso10_lb _ StypeP). congr (_ <= _): (FTtypeP_sum_cycTIiso01_lb maxT TtypeP). by apply: eq_bigr => x _; congr (nm2 _ x); apply: cycTIisoC. have: ub_lam1 < lambda 1%g ^+ 2 / #|S|%:R. rewrite -[_ / _](subrK g^-1) ltr_pwDr ?invr_gt0 ?gt0CG //. rewrite -(lerD2r (#|G0|%:R / g)) -lerBrDl -addrA. apply: le_trans (lerD lam1_ub eta10_ub). rewrite -mulrDl -big_split /= ler_pM2r ?invr_gt0 ?gt0CG //. exact: FTtypeP_sum_nonFitting_lb. rewrite calHuq // -/u -(sdprod_card defS) -/q -(sdprod_card defPU) oU mulnC. rewrite mulnCA mulnAC !natrM !invfM expr2 !mulrA !mulfK ?neq0CG ?neq0CiG //. rewrite mulrAC ltr_pdivlMr ?ltr_pdivrMr ?gt0CG //. congr (_ < _); last by rewrite -mulrA mulrC. have [_ [_ ->] _ _ _] := Sfacts; rewrite -/p -/q. rewrite -{1}(ltn_predK qgt2) expnS natrM mulrA; congr (_ * _). have /sdprod_card oT: T^`(1) ><| W2 = T by have [[]] := TtypeP. rewrite /ub_lam1 -{}oT natrM invfM mulrA divfK ?mulrBl ?divff ?neq0CG //. have /sdprod_card <-: Q ><| V = T^`(1)%g by have [_ []] := TtypeP. have ->: #|V| = v by rewrite /v D_1 indexg1. rewrite mulnC !natrM invfM mulrA mulfK ?neq0CiG //. have [_ [_ oQ] _ _ _] := FTtypeP_facts maxT TtypeP; rewrite -/p -/q /= in oQ. rewrite Dv natf_div ?dvdn_pred_predX // oQ. rewrite invfM invrK -mulrA -subn1 mulVKf ?gt_eqF ?ltr0n //; last first. by rewrite subn_gt0 -(exp1n p) ltn_exp2r ltnW // ltnW. rewrite -oQ natrB ?cardG_gt0 // !mulrBl mul1r mulrC mulKf ?neq0CG // -invfM. by rewrite -natrM oQ opprD opprK addrA addrAC. 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)