proposition: Lemma irr1_bound_quo (B C D : {group gT}) i : B <| C -> B \subset cfker 'chi[G]_i -> B \subset D -> D \subset C -> C \subset G -> (D / B \subset 'Z(C / B))%g -> 'chi_i 1%g <= #|G : C|%:R * sqrtC #|C : D|%:R.
proof: Proof. move=> BnC BsK BsD DsC CsG QsZ. case: (boolP ('Res[C] 'chi_i == 0))=> [HH|]. have: ('Res[C] 'chi_i) 1%g = 0 by rewrite (eqP HH) cfunE. by rewrite cfResE // => HH1; case/eqP: (irr1_neq0 i). have IC := cfRes_char C (irr_char i). case/neq0_has_constt=> i1 Hi1. have CIr: i \in irr_constt ('Ind[G] 'chi_i1). by rewrite inE /= -Frobenius_reciprocity /= cfdotC conjC_eq0. have BsKi : B \subset cfker 'chi_i1. suff BsKri: B \subset cfker ('Res[C] 'chi_i). by apply: (subset_trans BsKri); apply: (cfker_constt _ Hi1). apply/subsetP=> g GiG. have F: g \in C by rewrite (subsetP (subset_trans BsD _)). rewrite cfkerEchar // inE F !cfResE //. by move: (subsetP BsK _ GiG); rewrite cfkerEirr inE. pose i2 := quo_Iirr B i1. have ZsC: 'Z(C / B)%g \subset 'Z('chi_i2)%CF. by rewrite -(cap_cfcenter_irr (C / B)); apply: bigcap_inf. have CBsH: C :&: B \subset D. apply/subsetP=> g; rewrite inE; case/andP=> _ HH. by apply: (subsetP (BsD)). have I1B: 'chi_i1 1%g ^+ 2 <= #|C : D|%:R. case: (irr1_bound i2)=> HH _; move: HH. have ->: 'chi_i2 1%g = 'chi_i1 1%g. by rewrite quo_IirrE // -(coset_id (group1 B)) cfQuoE. move/le_trans; apply. rewrite ler_nat // -(index_quotient_eq CBsH) ?normal_norm //. rewrite -(@leq_pmul2l #|'Z('chi_i2)%CF|) ?cardG_gt0 ?cfcenter_sub //. rewrite Lagrange ?quotientS ?cfcenter_sub //. rewrite -(@leq_pmul2l #|(D / B)%g|) ?cardG_gt0 //. rewrite mulnA mulnAC Lagrange ?quotientS //. rewrite mulnC leq_pmul2l ?cardG_gt0 // subset_leq_card //. exact: subset_trans QsZ ZsC. have IC': 'Ind[G] 'chi_i1 \is a character := cfInd_char G (irr_char i1). move: (char1_ge_constt IC' CIr); rewrite cfInd1 //= => /le_trans-> //. have chi1_1_ge0: 0 <= 'chi_i1 1%g by rewrite ltW ?irr1_gt0. rewrite ler_pM2l ?gt0CiG //. by rewrite -(@ler_pXn2r _ 2) -?topredE /= ?sqrtC_ge0 ?ler0n ?sqrtCK. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop prime order ssralg finset fingroup morphism) mathcomp(perm automorphism quotient action zmodp finalg center commutator) mathcomp(poly cyclic pgroup nilpotent matrix mxalgebra mxrepresentation) mathcomp(vector falgebra fieldext ssrnum algC rat algnum galois) mathcomp(classfun character inertia integral_char vcharacter)