proposition: Lemma coherent_Frobenius_bound : exists i, let e := e_ i in let h := h_ i in (e - 1) * ((h - 2%:R * e - 1) / (e * h) + 2%:R / (h * (h + 2%:R))) <= (#|G0|%:R - 1) / #|G|%:R.
proof: Proof. have [sLG solL frobL] := all_and3 frobeniusL_G. have oddL i := oddSg (sLG i) oddG. have /all_and2[nsHL ntH] i: H i <| L i /\ H i :!=: 1%g. by case/Frobenius_context: (frobL i) => /sdprod_context[]. have sHL i: H i \subset L i by case/andP: (nsHL i). pose DH i := @Dade_signalizer gT G (L i) (A i). have /fin_all_exists[ddA DH1] i: exists dd, {in A i, forall a, DH i dd a = 1%G}. have /Dade_normedTI_P[|ddAi _] := normedTI_A i; last by exists ddAi. by apply: normedTI_Dade => //; rewrite setSD // (subset_trans (sHL i)). pose tau i := Dade (ddA i); pose rho i := invDade (ddA i). pose Atau i := Dade_support (ddA i). have defAtau i: Atau i = class_support (A i) G. rewrite class_supportEl; apply: eq_bigr => x Ax. by rewrite /Dade_support1 -/(DH i) DH1 // mul1g class_support_set1l. have disjoint_Atau i j : i != j -> [disjoint Atau i & Atau j]. move=> neq_ij; rewrite !defAtau !class_supportEr -setI_eq0 big_distrlr /=. rewrite pair_big big1 // => [[x y] _] /=; apply/eqP. by rewrite !conjD1g -setDIl setD_eq0 coprime_TIg // !cardJg card_coprime. have{defAtau} defG0: G0 = G :\: \bigcup_i Atau i. by congr (_ :\: _); apply: eq_bigr => i; rewrite defAtau. pose S i := seqIndD (H i) (L i) (H i) 1. have irrS i: {subset S i <= irr (L i)}. move=> _ /seqIndC1P[t nz_t ->]; rewrite irr_induced_Frobenius_ker //. exact: FrobeniusWker (frobL i). have /fin_all_exists[r lin_r] i: exists r, 'chi_r \in S i /\ 'chi_r 1%g = e_ i. have lt1Hi: [1] \proper H i by rewrite proper1G. have solHi := solvableS (sHL i) (solL i). have [xi Sxi lin_xi] := exists_linInd (nsHL i) solHi lt1Hi (normal1 _). by have /irrP[r def_xi] := irrS i xi Sxi; exists r; rewrite -def_xi. have{lin_r} [Sr r1] := all_and2 lin_r. have ntS i: (size (S i) > 1)%N by apply: seqInd_nontrivial (Sr i). have /fin_all_exists[nu cohS] i: coherent (S i) (L i)^# 'Ind[G, L i]. have [[[frobLi tiAiL] sLiG] oddLi] := (frobL i, normedTI_A i, sLG i, oddL i). have [defLi ntHi ntEi _ _] := Frobenius_context frobLi. have{ntEi} nilHi: nilpotent (H i) by apply: (Frobenius_sol_kernel_nil frobLi). exact: Sibley_coherence (or_introl _ frobLi). have{cohS} [/all_and2[Inu Znu] nu_Ind] := all_and2 cohS. have{DH DH1 nu_Ind} cohS i: coherent_with (S i) (L i)^# (tau i) (nu i). split=> // phi Sphi; rewrite /tau nu_Ind ?Dade_Ind //. by rewrite (@zchar_on _ _ (S i)) -?zcharD1_seqInd. have n1S i xi: xi \in S i -> '[xi] = 1. by case/irrS/irrP=> t ->; rewrite cfnorm_irr. have n1Snu i xi: xi \in S i -> '[nu i xi] = 1. by move=> Sxi; rewrite Inu ?n1S ?seqInd_zcharW. have o_nu i j: i != j -> {in S i & S j, forall xi xj, '[nu i xi, nu j xj] = 0}. move/disjoint_Atau/disjoint_coherent_ortho=> o_ij xi xj Sxi Sxj. by rewrite o_ij ?irrS //; apply: cohS. have /all_and2[nze nzh] i: e_ i != 0 /\ h_ i != 0 by rewrite neq0CiG neq0CG. have h_gt1 i: 1 < h_ i by rewrite ltr1n cardG_gt1. have eh i: e_ i * h_ i = #|L i|%:R by rewrite -natrM mulnC Lagrange. have def_h1 i: h_ i - 1 = #|A i|%:R. by rewrite /h_ (cardsD1 1%g) group1 addnC natrD addrK. have [i1 min_i1]: {i1 | forall i, i != i1 -> h_ i1 + 2%:R <= h_ i}. exists [arg min_(i < Ordinal k_ge2) #|H i|]. case: fintype.arg_minnP => // i1 _ min_i1. have oddH i: #|H i| = #|H i|./2.*2.+1. by rewrite -{1}[#|H i|]odd_double_half (oddSg (sHL i)). move=> i neq_i; rewrite -natrD ler_nat (oddH i) oddH addn2 -doubleS ltnS. rewrite leq_double ltn_neqAle andbC half_leq ?min_i1 //=. apply: contraTneq (card_coprime neq_i) => eqHii1. by rewrite oddH -eqHii1 -oddH /coprime gcdnn -trivg_card1. exists i1 => e h; set lhs := (e - 1) * _. have nzh2: h + 2%:R != 0 by rewrite -natrD addnC pnatr_eq0. have{lhs} ->: lhs = 1 - e / h - (h - 1) / (e * h) - (e - 1) / (h + 2%:R). rewrite {}/lhs -{2}(addrK h 2%:R) !invfM (mulrBl _ _ h) mulVKf ?nzh //. rewrite addrCA (addrC _ h) mulrCA mulrA addrA mulrBr; congr (_ - _). rewrite mulfK // mulrDr addrAC addrC mulrC mulrBl -mulrA mulVKf ?nze //. rewrite mulrC mulrBr mulrBl mul1r addrAC addrC addrA; congr (_ - _). rewrite mulrCA mulVKf ?nze // addrCA mulrCA mulr_natl opprD addNKr. by rewrite !mulrBl opprB addrA subrK divff ?nzh. pose beta i := tau i ('Ind[L i, H i] 1 - 'chi_(r i)). have betaP i := Dade_Ind1_sub_lin (cohS i) (ntS i) (mem_irr _) (Sr i) (r1 i). pose chi i := nu i 'chi_(r i); pose c i j := '[beta i, chi j]. have:= betaP i1; rewrite -/(S _) -/(tau _) -/(beta _) -/(chi _) -/(e_ _) -/e. move=> [[oSnu1 o_beta1 Zbeta1] [Gamma [oSnuGamma oGamma1] [a Za def_beta1]]]. have [_ lt_e_h2] := e_bounds i1; rewrite -/(rho _) -/(h_ _) -/h. case/(_ lt_e_h2)=> min_rho1 maxGamma _ {lt_e_h2}. pose calB := [set i | (i != i1) && (c i i1 == 0)]. pose sumB := \sum_(i in calB) (h_ i - 1) / (e_ i * h_ i). suffices{min_rho1} sumB_max: sumB <= (e - 1) / (h + 2%:R). rewrite -subr_ge0 opprB addrCA -[_ / _ - _]opprB subr_ge0. apply: le_trans sumB_max. rewrite -subr_ge0 opprB addrCA -(opprB _ sumB) subr_ge0. have Zchi1: chi i1 \in 'Z[irr G] by rewrite Znu ?seqInd_zcharW ?Sr. have [eps [t def_chi1]] := vchar_norm1P Zchi1 (n1Snu i1 'chi_(r i1) (Sr i1)). pose sumG0 := \sum_(g in G0) `|'chi_t g| ^+ 2. apply: (le_trans (y := (#|G0|%:R - sumG0) / #|G|%:R)); last first. rewrite ler_pM2r ?invr_gt0 ?gt0CG // lerD2l lerN2. rewrite [sumG0](bigD1 1%g) /=; last first. rewrite !inE group1 andbT; apply/bigcupP=> [[i _]]. by rewrite class_supportEr => /bigcupP[x _]; rewrite conjD1g !inE eqxx. rewrite -[1]addr0 lerD ?sumr_ge0 // => [|x _]; last first. by rewrite -normrX normr_ge0. have Zchit1: 'chi_t 1%g \in Cint by rewrite CintE Cnat_irr1. by rewrite expr_ge1 ?normr_ge0 // norm_Cint_ge1 ?irr1_neq0. pose ea i : algC := #|(H i)^#|%:R / #|L i|%:R. apply: (le_trans (y := \sum_i ('[rho i 'chi_t] - ea i))); last first. rewrite -subr_ge0 -opprB oppr_ge0 -mulNr opprB addrC mulrC. by rewrite /sumG0 defG0 Dade_cover_inequality ?cfnorm_irr. rewrite (bigID (mem calB)) /= addrC lerD //. rewrite -subr_ge0 opprK -big_split sumr_ge0 //= => i _. by rewrite def_h1 eh subrK cfnorm_ge0. rewrite (bigD1 i1) ?inE ?eqxx ?andbF //= -lerBlDl. rewrite (le_trans (y := 0)) //. rewrite opprB /ea -def_h1 -eh -/h -/e addrA subrK subr_le0. by rewrite -(cfnorm_sign eps) -linearZ -def_chi1. rewrite sumr_ge0 // => i; rewrite inE /c andbC => /andP[neq_i]. rewrite neq_i subr_ge0 def_chi1 cfdotZr mulf_eq0 => /norP[_ not_o_beta_chi]. have [[_ _ Zbeta_i] _ /(_ _ (mem_irr t))[|_ ->]] := betaP i. apply/orthoPr=> _ /mapP[xi Sxi ->]; rewrite -['chi_t](signrZK eps). by rewrite -def_chi1 cfdotZr o_nu ?mulr0 ?Sr. rewrite -[ea i]mulr1 /ea ler_wpM2l ?mulr_ge0 ?invr_ge0 ?ler0n //. by rewrite -/(tau i) -/(beta i) sqr_Cint_ge1 ?Cint_cfdot_vchar_irr. rewrite -(mulfK nzh2 sumB) -{2 3}natrD ler_wpM2r ?invr_ge0 ?ler0n //. apply: le_trans maxGamma; rewrite mulr_suml. pose phi i : 'CF(G) := \sum_(xi <- S i) xi 1%g / e_ i / '[xi] *: nu i xi. have o_phi_nu i j xi: i != j -> xi \in S j -> '[phi i, nu j xi] = 0. move/o_nu=> o_ij Sxi; rewrite cfdot_suml big1_seq //= => pi Spi. by rewrite cfdotZl o_ij ?mulr0. have o_phi i j: i != j -> '[phi i, phi j] = 0. move/o_phi_nu=> o_ij; rewrite cfdot_sumr big1_seq // => xi Sxi. by rewrite cfdotZr o_ij ?mulr0. pose X : 'CF(G) := \sum_(i in calB) c i1 i *: phi i; pose Gamma1 := Gamma - X. have ->: Gamma = Gamma1 + X by rewrite subrK. have{betaP def_beta1} /cfnormDd->: '[Gamma1, X] = 0. rewrite cfdot_sumr big1 // => i Bi; have [neq_i _] := setIdP Bi. rewrite cfdotZr cfdot_sumr big1_seq ?mulr0 //= => xi Sxi. apply/eqP; rewrite cfdotZr cfdotBl mulf_eq0; apply/pred2P; right. rewrite cfdot_suml (bigD1 i) ?big1 //= => [|j /andP[_ neq_j]]; last first. by rewrite cfdotZl o_phi_nu ?mulr0. rewrite cfdotZl (cfproj_sum_orthogonal (Inu i)) ?seqInd_orthogonal //. rewrite n1S // divr1 mulr1 addr0 mulrC -(canLR (addKr _) def_beta1). rewrite !(cfdotDl, cfdotNl) cfdotZl o_nu ?o_phi_nu ?Sr 1?eq_sym // mulr0. have[[/orthoPr oSnui_1 _ _] _ _] := betaP i; rewrite -/(S i) in oSnui_1. rewrite cfdotC oSnui_1 ?map_f // conjC0 !(add0r, oppr0). have Nxie: xi 1%g / e_ i \in Cnat by apply: dvd_index_seqInd1 _ Sxi. rewrite -(conj_Cnat Nxie) // -cfdotZr -raddfZ_Cnat // -!raddfB /=. have [_ Dnu] := cohS i. rewrite Dnu ?zcharD1_seqInd ?seqInd_sub_lin_vchar ?Sr ?r1 //. by rewrite disjoint_Dade_ortho ?disjoint_Atau 1?eq_sym. rewrite -subr_ge0 cfdot_sumr -addrA -sumrB addr_ge0 ?cfnorm_ge0 //. rewrite sumr_ge0 // => i Bi; have [neq_i ci1_0] := setIdP Bi. have n_phi: '[phi i] = (h_ i - 1) / e_ i. rewrite (cfnorm_sum_orthogonal (Inu i)) ?seqInd_orthogonal //. rewrite -[_ - 1](mulKf (nze i)) -sum_seqIndC1_square // -/(S i) mulrAC. rewrite -invfM mulrC mulr_suml; apply: eq_big_seq => _ /irrS/irrP[t ->]. rewrite cfnorm_irr !divr1 mulr1 -expr2 -exprVn -exprMn. by rewrite (normr_idP _) // mulr_ge0 ?invr_ge0 ?ler0n // ltW ?irr1_gt0. rewrite subr_ge0 cfdotZr cfdot_suml (bigD1 i) //=. rewrite big1 ?addr0 => [|j /andP[_ ne_j]]; last by rewrite cfdotZl o_phi ?mulr0. rewrite cfdotZl invfM 2!mulrA -n_phi -[_ * _]mulrA mulrC. rewrite ler_wpM2r ?cfnorm_ge0 // (le_trans (y := 1)) //. by rewrite -{2}(mulVf (nzh i)) ler_wpM2l ?invr_ge0 ?ler0n ?min_i1. rewrite mulrC -normCK expr_ge1 ?normr_ge0 // norm_Cint_ge1 //. rewrite Cint_cfdot_vchar ?Znu ?seqInd_zcharW ?Sr //. suffices []: c i i1 != 0 \/ c i1 i != 0 by rewrite ?ci1_0. apply/Dade_sub_lin_nonorthogonal; rewrite ?mem_irr ?Sr ?r1 //; try exact: cohS. exact: disjoint_Atau. 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)