proposition: Lemma sum_norm2_char_generators gT (G : {group gT}) (chi : 'CF(G)) : let S := [pred s | generator G s] in chi \is a character -> {in S, forall s, chi s != 0} -> \sum_(s in S) `|chi s| ^+ 2 >= #|S|%:R.
proof: Proof. move=> S Nchi nz_chi_S; pose n := #|G|. have [g Sg | S_0] := pickP (generator G); last first. by rewrite eq_card0 // big_pred0 ?lerr. have defG: <[g]> = G by apply/esym/eqP. have [cycG Gg]: cyclic G /\ g \in G by rewrite -defG cycle_cyclic cycle_id. pose I := {k : 'I_n | coprime n k}; pose ItoS (k : I) := (g ^+ sval k)%g. have imItoS: codom ItoS =i S. move=> s; rewrite inE /= /ItoS /I /n /S -defG -orderE. apply/codomP/idP=> [[[i cogi] ->] | Ss]; first by rewrite generator_coprime. have [m ltmg Ds] := cyclePmin (cycle_generator Ss). by rewrite Ds generator_coprime in Ss; apply: ex_intro (Sub (Sub m _) _) _. have /injectiveP injItoS: injective ItoS. move=> k1 k2 /eqP; apply: contraTeq. by rewrite eq_expg_mod_order orderE defG -/n !modn_small. have [Qn galQn [QnC gQnC [eps [pr_eps defQn] QnG]]] := group_num_field_exists G. have{QnG} QnGg := QnG _ G _ _ g (order_dvdG Gg). pose calG := 'Gal({:Qn} / 1). have /fin_all_exists2[ItoQ inItoQ defItoQ] (k : I): exists2 nu, nu \in calG & nu eps = eps ^+ val k. - case: k => [[m _] /=]; rewrite coprime_sym => /Qn_aut_exists[nuC DnuC]. have [nuQ DnuQ] := restrict_aut_to_normal_num_field QnC nuC. have hom_nu: kHom 1 {:Qn} (linfun nuQ). rewrite k1HomE; apply/ahom_inP. by split=> [u v | ]; rewrite !lfunE ?rmorphM ?rmorph1. have [|nu cGnu Dnu] := kHom_to_gal _ (normalFieldf 1) hom_nu. by rewrite !subvf. exists nu => //; apply: (fmorph_inj QnC). rewrite -Dnu ?memvf // lfunE DnuQ rmorphXn DnuC //. by rewrite prim_expr_order // fmorph_primitive_root. have{defQn} imItoQ: calG = ItoQ @: {:I}. apply/setP=> nu; apply/idP/imsetP=> [cGnu | [k _ ->] //]. have pr_nu_e: n.-primitive_root (nu eps) by rewrite fmorph_primitive_root. have [i Dnue] := prim_rootP pr_eps (prim_expr_order pr_nu_e). rewrite Dnue prim_root_exp_coprime // coprime_sym in pr_nu_e. apply: ex_intro2 (Sub i _) _ _ => //; apply/eqP. rewrite /calG /= -defQn in ItoQ inItoQ defItoQ nu cGnu Dnue *. by rewrite gal_adjoin_eq // defItoQ -Dnue. have injItoQ: {in {:I} &, injective ItoQ}. move=> k1 k2 _ _ /(congr1 (fun nu : gal_of _ => nu eps))/eqP. by apply: contraTeq; rewrite !defItoQ (eq_prim_root_expr pr_eps) !modn_small. pose pi1 := \prod_(s in S) chi s; pose pi2 := \prod_(s in S) `|chi s| ^+ 2. have Qpi1: pi1 \in Crat. have [a Da] := QnGg _ Nchi; suffices ->: pi1 = QnC (galNorm 1 {:Qn} a). have /vlineP[q ->] := mem_galNorm galQn (memvf a). by rewrite rmorphZ_num rmorph1 mulr1 Crat_rat. rewrite /galNorm rmorph_prod -/calG imItoQ big_imset //=. rewrite /pi1 -(eq_bigl _ _ imItoS) -big_uniq // big_image /=. apply: eq_bigr => k _; have [nuC DnuC] := gQnC (ItoQ k); rewrite DnuC Da. have [r ->] := char_sum_irr Nchi; rewrite !sum_cfunE rmorph_sum. apply: eq_bigr => i _; have /QnGg[b Db] := irr_char i. have Lchi_i: 'chi_i \is a linear_char by rewrite irr_cyclic_lin. have /(prim_rootP pr_eps)[m Dem]: b ^+ n = 1. apply/eqP; rewrite -(fmorph_eq1 QnC) rmorphXn /= Db -lin_charX //. by rewrite -expg_mod_order orderE defG modnn lin_char1. rewrite -Db /= -DnuC Dem rmorphXn /= defItoQ exprAC -{m}Dem rmorphXn /= {b}Db. by rewrite lin_charX. clear I ItoS imItoS injItoS ItoQ inItoQ defItoQ imItoQ injItoQ. clear Qn galQn QnC gQnC eps pr_eps QnGg calG. have{Qpi1} Zpi1: pi1 \in Num.int. by rewrite Cint_rat_Aint // rpred_prod // => s _; apply: Aint_char. have{pi1 Zpi1} pi2_ge1: 1 <= pi2. have ->: pi2 = `|pi1| ^+ 2. by rewrite (big_morph Num.norm (@normrM _) (@normr1 _)) -prodrXl. by rewrite intr_normK // sqr_intr_ge1 //; apply/prodf_neq0. have Sgt0: (#|S| > 0)%N by rewrite (cardD1 g) [g \in S]Sg. rewrite -mulr_natr -ler_pdivlMr ?ltr0n //. have n2chi_ge0 s: s \in S -> 0 <= `|chi s| ^+ 2 by rewrite exprn_ge0. rewrite -(expr_ge1 Sgt0); last by rewrite divr_ge0 ?ler0n ?sumr_ge0. by rewrite (le_trans pi2_ge1) // leif_AGM. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime order) mathcomp(ssralg poly finset fingroup morphism perm) mathcomp(automorphism quotient action countalg finalg zmodp) mathcomp(commutator cyclic center pgroup sylow gseries) mathcomp(nilpotent abelian ssrnum ssrint archimedean polydiv) mathcomp(rat matrix mxalgebra intdiv mxpoly vector falgebra) mathcomp(fieldext separable galois algC cyclotomic algnum) mathcomp(mxrepresentation classfun character)