proposition: Lemma zchar_small_norm phi n : phi \in 'Z[irr G] -> '[phi] = n%:R -> (n < 4)%N -> {S : n.-tuple 'CF(G) | [/\ orthonormal S, {subset S <= 'Z[irr G]} & phi = \sum_(xi <- S) xi]}.
proof: Proof. move=> Zphi def_n lt_n_4. pose S := [seq '[phi, 'chi_i] *: 'chi_i | i in irr_constt phi]. have def_phi: phi = \sum_(xi <- S) xi. rewrite big_image big_mkcond {1}[phi]cfun_sum_cfdot. by apply: eq_bigr => i _; rewrite if_neg; case: eqP => // ->; rewrite scale0r. have orthS: orthonormal S. apply/orthonormalP; split=> [|_ _ /mapP[i phi_i ->] /mapP[j _ ->]]. rewrite map_inj_in_uniq ?enum_uniq // => i j; rewrite mem_enum => phi_i _. by move/eqP; rewrite eq_scaled_irr (negbTE phi_i) => /andP[_ /= /eqP]. rewrite eq_scaled_irr cfdotZl cfdotZr cfdot_irr mulrA mulr_natr mulrb. rewrite mem_enum in phi_i; rewrite (negbTE phi_i) andbC; case: eqP => // <-. have /natrP[m def_m] := natr_norm_int (Cint_cfdot_vchar_irr i Zphi). apply/eqP; rewrite eqxx /= -normCK def_m -natrX eqr_nat eqn_leq lt0n. rewrite expn_eq0 andbT -eqC_nat -def_m normr_eq0 [~~ _]phi_i andbT. rewrite (leq_exp2r _ 1) // -ltnS -(@ltn_exp2r _ _ 2) //. apply: leq_ltn_trans lt_n_4; rewrite -leC_nat -def_n natrX. rewrite cfdot_sum_irr (bigD1 i) //= -normCK def_m addrC -subr_ge0 addrK. by rewrite sumr_ge0 // => ? _; apply: mul_conjC_ge0. have <-: size S = n. by apply/eqP; rewrite -eqC_nat -def_n def_phi cfnorm_orthonormal. exists (in_tuple S); split=> // _ /mapP[i _ ->]. by rewrite scale_zchar ?irr_vchar // Cint_cfdot_vchar_irr. 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 finalg action gproduct) mathcomp(zmodp commutator cyclic center pgroup sylow) mathcomp(frobenius vector ssrnum ssrint archimedean intdiv) mathcomp(algC algnum classfun character integral_char)