proposition: Lemma FTtype345_Dade_bridge0 : (w1 < w2)%N -> {chi | [/\ (mu_ 0 - zeta)^\tau = \sum_i eta_ i 0 - chi, chi \in 'Z[irr G], '[chi] = 1 & forall i j, '[chi, eta_ i j] = 0]}.
proof: Proof. move=> w1_lt_w2; set psi := mu_ 0 - zeta; pose Wsig := map sigma (irr W). have [X wsigX [chi [DpsiG _ o_chiW]]] := orthogonal_split Wsig psi^\tau. exists (- chi); rewrite opprK rpredN cfnormN. have o_chi_w i j: '[chi, eta_ i j] = 0. by rewrite (orthoPl o_chiW) ?map_f ?mem_irr. have [Isigma Zsigma] := cycTI_Zisometry ctiWG. have o1Wsig: orthonormal Wsig by rewrite map_orthonormal ?irr_orthonormal. have [a_ Da defX] := orthonormal_span o1Wsig wsigX. have{} Da i j: a_ (eta_ i j) = '[psi^\tau, eta_ i j]. by rewrite DpsiG cfdotDl o_chi_w addr0 Da. have sumX: X = \sum_i \sum_j a_ (eta_ i j) *: eta_ i j. rewrite pair_bigA defX big_map (big_nth 0) size_tuple big_mkord /=. rewrite (reindex (dprod_Iirr defW)) /=. by apply: eq_bigr => [[i j] /= _]; rewrite -tnth_nth. by exists (inv_dprod_Iirr defW) => ij; rewrite (inv_dprod_IirrK, dprod_IirrK). have Zpsi: psi \in 'Z[irr M]. by rewrite rpredB ?irr_vchar ?(mem_zchar irr_zeta) ?char_vchar ?prTIred_char. have{Zpsi} M'psi: psi \in 'Z[irr M, M'^#]. by rewrite -defA zchar_split Zpsi mu0Bzeta_on. have A0psi: psi \in 'CF(M, 'A0(M)). by apply: cfun_onS (zchar_on M'psi); rewrite defA0 subsetUl. have a_00: a_ (eta_ 0 0) = 1. rewrite Da [w_ 0 0](cycTIirr00 defW) [sigma 1]cycTIiso1. rewrite Dade_reciprocity // => [|x _ y _]; last by rewrite !cfun1E !inE. rewrite rmorph1 /= -(prTIirr00 ptiWM) -/(mu2_ 0 0) cfdotC. by rewrite cfdotBr o_mu2_zeta subr0 cfdot_prTIirr_red rmorph1. have n2psiG: '[psi^\tau] = w1.+1%:R. rewrite Dade_isometry // cfnormBd ?o_mu_zeta //. by rewrite cfnorm_prTIred irrWnorm // -/w1 mulrSr. have psiG_V0 x: x \in V -> psi^\tau x = 0. move=> Vx; rewrite Dade_id ?defA0; last first. by rewrite inE orbC mem_class_support. rewrite (cfun_on0 (zchar_on M'psi)) // -defA. suffices /setDP[]: x \in 'A0(M) :\: 'A(M) by []. by rewrite (FTsupp0_typeP maxM MtypeP) // mem_class_support. have ZpsiG: psi^\tau \in 'Z[irr G]. by rewrite Dade_vchar // zchar_split (zcharW M'psi). have n2psiGsum: '[psi^\tau] = \sum_i \sum_j `|a_ (eta_ i j)| ^+ 2 + '[chi]. rewrite DpsiG addrC cfnormDd; last first. by rewrite (span_orthogonal o_chiW) ?memv_span1. rewrite addrC defX cfnorm_sum_orthonormal // big_map pair_bigA; congr (_ + _). rewrite big_tuple /= (reindex (dprod_Iirr defW)) //. by exists (inv_dprod_Iirr defW) => ij; rewrite (inv_dprod_IirrK, dprod_IirrK). have NCpsiG: (cyclicTI_NC ctiWG psi^\tau < 2 * minn w1 w2)%N. apply: (@leq_ltn_trans w1.+1); last first. by rewrite /minn w1_lt_w2 mul2n -addnn (leq_add2r w1 2) cardG_gt1. pose z_a := [pred ij | a_ (eta_ ij.1 ij.2) == 0]. have ->: cyclicTI_NC ctiWG psi^\tau = #|[predC z_a]|. by apply: eq_card => ij; rewrite !inE -Da. rewrite -leC_nat -n2psiG n2psiGsum ler_wpDr ?cfnorm_ge0 // pair_bigA. rewrite (bigID z_a) big1 /= => [|ij /eqP->]; last by rewrite normCK mul0r. rewrite add0r -sumr_const ler_sum // => [[i j] nz_ij]. by rewrite expr_ge1 ?norm_Cint_ge1 // Da Cint_cfdot_vchar ?Zsigma ?irr_vchar. have nz_psiG00: '[psi^\tau, eta_ 0 0] != 0 by rewrite -Da a_00 oner_eq0. have [a_i|a_j] := small_cycTI_NC psiG_V0 NCpsiG nz_psiG00. have psiGi: psi^\tau = \sum_i eta_ i 0 + chi. rewrite DpsiG sumX; congr (_ + _); apply: eq_bigr => i _. rewrite big_ord_recl /= Da a_i -Da a_00 mul1r scale1r. by rewrite big1 ?addr0 // => j1 _; rewrite Da a_i mul0r scale0r. split=> // [||i j]; last by rewrite cfdotNl o_chi_w oppr0. rewrite -(canLR (addKr _) psiGi) rpredD // rpredN rpred_sum // => j _. by rewrite Zsigma ?irr_vchar. apply: (addrI w1%:R); rewrite -mulrSr -n2psiG n2psiGsum; congr (_ + _). rewrite -nirrW1 // -sumr_const; apply: eq_bigr => i _. rewrite big_ord_recl /= Da a_i -Da a_00 mul1r normr1. by rewrite expr1n big1 ?addr0 // => j1 _; rewrite Da a_i normCK !mul0r. suffices /idPn[]: '[psi^\tau] >= w2%:R. rewrite odd_geq /= ?uphalf_half mFT_odd //= in w1_lt_w2. by rewrite n2psiG leC_nat -ltnNge odd_geq ?mFT_odd. rewrite n2psiGsum exchange_big /= ler_wpDr ?cfnorm_ge0 //. rewrite -nirrW2 -sumr_const; apply: ler_sum => i _. rewrite big_ord_recl /= Da a_j -Da a_00 mul1r normr1. by rewrite expr1n big1 ?addr0 // => j1 _; rewrite Da a_j normCK !mul0r. Qed.
imports: 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 finalg zmodp) mathcomp(gfunctor gproduct cyclic commutator gseries nilpotent pgroup) mathcomp(sylow hall abelian maximal frobenius) mathcomp(matrix mxalgebra mxrepresentation mxabelem vector) odd_order(BGsection1 BGsection3 BGsection7 BGsection15 BGsection16) mathcomp(ssrnum algC classfun character integral_char inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3 PFsection4) odd_order(PFsection5 PFsection6 PFsection7 PFsection8 PFsection9)