proposition: Lemma Dade_Ind1_sub_lin (nu : {additive 'CF(L) -> 'CF(G)}) zeta : coherent_with calS L^# (Dade ddA) nu -> (1 < size calS)%N -> zeta \in irr L -> zeta \in calS -> zeta 1%g = e -> let beta := (Ind1H - zeta)^\tau in let calSnu := map nu calS in let sumSnu := \sum_(xi <- calS) xi 1%g / e / '[xi] *: nu xi in [/\ [/\ orthogonal calSnu 1%CF, '[beta, 1] = 1 & beta \in 'Z[irr G]], exists2 Gamma : 'CF(G), [/\ orthogonal calSnu Gamma, '[Gamma, 1] = 0 & exists2 a, a \in Cint & beta = 1 - nu zeta + a *: sumSnu + Gamma] & e <= (h - 1) / 2%:R -> '[(nu zeta)^\rho] >= 1 - e / h /\ '[Gamma] <= e - 1 & {in irr G, forall chi : 'CF(G), orthogonal calSnu chi -> [/\ {in A, forall x, chi^\rho x = '[beta, chi]} & '[chi^\rho] = #|A|%:R / #|L|%:R * '[beta, chi] ^+ 2]}].
proof: Proof. move=> [[Inu Znu] nu_tau] nt_calS /irrWnorm Nzeta1 Szeta zeta1. set mu := _ - _ => beta calSnu sumSnu; pose S1 := rem zeta calS. have defS: perm_eq calS (zeta :: S1) := perm_to_rem Szeta. have defZS: 'Z[calS, L^#] =i 'Z[calS, A] by apply: zcharD1_seqInd. have S1P xi: xi \in S1 -> xi != zeta /\ xi \in calS. by rewrite mem_rem_uniq // => /andP[]. have defT: perm_eql calT [:: Ind1H, zeta & S1]. apply/permPl; have Tind1: Ind1H \in calT := seqIndT_Ind1 H L. by rewrite (permPl (perm_to_rem Tind1)) perm_cons -seqIndC1_rem. have mu_vchar: mu \in 'Z[irr L, A] := cfInd1_sub_lin_vchar nsHL Szeta zeta1. have beta_vchar: beta \in 'Z[irr G] by apply: Dade_vchar. have [mu_on beta_on] := (zchar_on mu_vchar, zchar_on beta_vchar). have{nt_calS} ntS1: (size S1 > 0)%N by rewrite size_rem // -subn1 subn_gt0. case defS1: S1 ntS1 => // [phi S2] _. have /S1P[neq_phi Sphi]: phi \in S1 by rewrite defS1 mem_head. have nz_phi1: phi 1%g != 0 by rewrite (seqInd1_neq0 nsHL Sphi). have NatS1e xi (Sxi : xi \in calS) := dvd_index_seqInd1 nsHL Sxi. have oS1: {in calS, forall psi, '[psi, 1] = 0} by apply: seqInd_ortho_1. have oS1H: {in calS, forall psi, '[psi, Ind1H] = 0} by apply: seqInd_ortho_Ind1. have InuS: {in calS &, isometry nu} by apply: sub_in2 Inu; apply: seqInd_zcharW. have ZnuS xi (Sxi : xi \in calS) := Znu xi (seqInd_zcharW Sxi). have S_Se xi (Sxi : xi \in calS) := seqInd_sub_lin_vchar nsHL Szeta zeta1 Sxi. have oSnu1: orthogonal calSnu 1%CF. have dotSnu1 psi : psi \in calS -> '[nu psi, 1] = psi 1%g / e * '[nu zeta, 1]. move=> Spsi; apply/eqP; rewrite -subr_eq0 -cfdotZl -cfdotBl. rewrite -raddfZ_Cnat ?NatS1e // -raddfB; have Spi := S_Se _ Spsi. rewrite nu_tau ?defZS // invDade_reciprocity ?(zchar_on Spi) //. rewrite invDade_cfun1 (eq_cfdotr (zchar_on Spi) (eq_cfuni nsAL)). by rewrite cfdotBl cfdotZl !oS1 // mulr0 subr0. suffices oz1: '[nu zeta, 1] = 0. by apply/orthoPr=> _ /mapP[psi Spsi ->]; rewrite dotSnu1 // oz1 mulr0. have norm_nu_zeta : '[nu zeta] = 1 by rewrite InuS // irrWnorm. have [et [t defz]] := vchar_norm1P (ZnuS _ Szeta) norm_nu_zeta. rewrite defz cfdotZl -{1}irr0 cfdot_irr mulr_natr mulrb; case: eqP => // t0. have /eqP/idPn[] := seqInd_ortho nsHL Sphi Szeta neq_phi. rewrite -InuS // defz t0 cfdotZr irr0 dotSnu1 // mulrCA -irr0 -t0. by rewrite -cfdotZr -defz norm_nu_zeta mulr1 mulf_neq0 ?invr_eq0. have dot_beta_1: '[beta, 1] = 1. rewrite invDade_reciprocity // invDade_cfun1 (eq_cfdotr _ (eq_cfuni nsAL)) //. by rewrite cfdotBl -Frobenius_reciprocity cfRes_cfun1 ?cfnorm1 ?oS1 ?subr0. have o_beta1: '[beta - 1, 1] = 0 by rewrite cfdotBl dot_beta_1 cfnorm1 subrr. have [X SnuX [Gamma [def_beta1 _ oSnuG]]]:= orthogonal_split calSnu (beta - 1). have oG1: '[Gamma, 1] = 0. rewrite -(addKr X Gamma) -def_beta1 addrC cfdotBl o_beta1. by rewrite (span_orthogonal oSnu1) ?subr0 // memv_span ?mem_head. have oSS: pairwise_orthogonal calS by apply: seqInd_orthogonal. have oSnuS: pairwise_orthogonal calSnu by apply: map_pairwise_orthogonal. have [a_ def_a defX] := orthogonal_span oSnuS SnuX. have{} def_a: {in calS, forall xi, a_ (nu xi) = '[beta, nu xi] / '[xi]}. move=> xi Sxi; rewrite (canRL (subrK 1) def_beta1) !cfdotDl def_a InuS //. by rewrite (cfdotC 1) (orthoPl oSnuG) ?(orthoPr oSnu1) ?map_f ?conjC0 ?addr0. pose a := '[beta, nu zeta] + 1; have Z1 := Cint1. have{Z1} Za: a \in Cint by rewrite rpredD ?Cint_cfdot_vchar // ZnuS. have {a_ def_a} defX: X = - nu zeta + a *: sumSnu. rewrite linear_sum defX big_map !(perm_big _ defS) !big_cons /= addrCA. rewrite def_a // Nzeta1 !divr1 zeta1 divff // scalerDl !scale1r addrA. rewrite addrK; congr (_ + _); apply: eq_big_seq => xi /S1P[neq_xi Sxi]. rewrite def_a // scalerA mulrA mulrDl mul1r; congr (_ / _ *: _). rewrite mulrC -(conj_Cnat (NatS1e _ Sxi)) -cfdotZr -raddfZ_Cnat ?NatS1e //. rewrite addrC; apply: canRL (subrK _) _; rewrite -!raddfB /= -/e. have Spi := S_Se xi Sxi; rewrite nu_tau ?defZS //. rewrite Dade_isometry ?(zchar_on Spi) // cfdotC cfdotBl cfdotZl !cfdotBr. by rewrite !oS1H ?(seqInd_ortho _ Sxi) // Nzeta1 subr0 !add0r mulrN1 opprK. have Ind1H1: Ind1H 1%g = e by rewrite cfInd1 // cfun11 mulr1. split=> // [ | chi /irrP[t def_chi] o_chiSnu]. rewrite (canRL (subrK 1) def_beta1) defX addrC 2!addrA. exists Gamma; first by rewrite orthogonal_sym; split; last exists a. move=> lt_e_h2; pose v := h^-1; pose u := e^-1 * (1 - v); set w := 1 - e / h. have hu: h * u = e^-1 * (h - 1) by rewrite mulrCA (mulrBr h) mulr1 divff. have ->: '[(nu zeta)^\rho] = u * a ^+ 2 - v * a *+ 2 + w. have defT1: perm_eq calT [:: phi, Ind1H, zeta & S2]. by rewrite defT defS1 (perm_catCA [:: _; _] phi). have [c ua _ ->] := invDade_seqInd_sum (nu zeta) defT1. have def_c xi: xi \in calS -> c xi = '[xi, zeta]. move=> S2xi; rewrite /c mulrC -{1}[xi]scale1r -(mulVf nz_phi1) -!scalerA. rewrite -scalerBr linearZ cfdotZl /=; set pi := _ - _. have Spi: pi \in 'Z[calS, A] by apply: sub_seqInd_zchar. rewrite -nu_tau ?defZS // Inu ?(zcharW Spi) ?seqInd_zcharW //. by rewrite cfdotBl !cfdotZl (seqInd_ortho _ Sphi) // mulr0 subr0 mulKf. have c2: c zeta = 1 by rewrite def_c. have c1: c Ind1H = a. by rewrite /a -c2 -cfdotDl -linearD !addrA subrK zeta1 -Ind1H1. have{def_c} c3 xi: xi \in S2 -> c xi = 0. move=> S2xi; have /S1P[neq_xi Sxi]: xi \in S1 by rewrite defS1 mem_behead. by rewrite def_c // (seqInd_ortho _ Sxi). rewrite !big_cons; have kill0 := (mul0r, mulr0, big1, conjC0). rewrite !big1_seq /ua; try by move=> psi /c3->; do 2?rewrite ?kill0 => *. rewrite !addr0 c1 c2 Nzeta1 cfnorm_Ind_cfun1 // -/e Ind1H1 zeta1 conjC1. rewrite cfdotC (seqInd_ortho_Ind1 _ _ Szeta) // !kill0 sub0r !mulrN !mulr1. rewrite divr1 !mul1r !invfM mulrBr !mulrA !mulfK ?divfK // -/w. rewrite aut_Cint // -[_ / h]mulrA -{1}[e^-1]mulr1 -2!mulrBr -/u -/v. by rewrite mulrC mulrA addrA (mulrC v) -[_ - _]addrA -opprD. have ->: '[Gamma] = e - 1 - h * (u * a ^+ 2 - v * a *+ 2). have /(canLR (addrK 1)) <-: '[beta] = e + 1. rewrite Dade_isometry // cfnormBd ?cfnorm_Ind_cfun1 ?Nzeta1 //. by rewrite cfdotC (seqInd_ortho_Ind1 _ _ Szeta) ?conjC0. rewrite -[beta](subrK 1) cfnormDd; last first. by rewrite cfdotBl dot_beta_1 cfnorm1 subrr. rewrite cfnorm1 addrK def_beta1 (addrC X) cfnormDd; last first. by rewrite (span_orthogonal oSnuG) // memv_span ?mem_head. do 2!apply: canRL (addrK _) _; rewrite -addrA; congr (_ + _). rewrite defX (addrC (- nu _)) cfnormB cfnormZ Cint_normK // InuS //. rewrite cfdotZl cfproj_sum_orthogonal // Nzeta1 zeta1 divff // divr1. rewrite !mulr1 aut_Cint // mulrBr mulrDr mulVKf // addrAC. rewrite mulrA mulrC hu -[e^-1](divfK nze) -expr2; congr (_ * _ - _ + 1). rewrite -mulrA -sum_seqIndC1_square // mulr_sumr cfnorm_sum_orthogonal //. apply: eq_big_seq => xi Sxi. have [nz_xi Nxi1] := (cfnorm_seqInd_neq0 nsHL Sxi, Cnat_seqInd1 Sxi). rewrite (normr_idP _) ?mulr_ge0 ?invr_ge0 ?ler0n ?cfnorm_ge0 ?Cnat_ge0 //. by rewrite mulrCA !exprMn ['[xi]]lock !mulrA divfK // -lock. apply/andP; rewrite -(subr_ge0 w) addrK andbC -subr_ge0 addrC opprB subrK. rewrite pmulr_rge0 ?gt0CG // andbb -mulr_natr (mulrAC v). have v_ge0: 0 <= v by [rewrite invr_ge0 ler0n]; have L_gt0 := gt0CG L. have Lu: #|L|%:R * u = h - 1 by rewrite -eh -mulrA hu mulVKf. have h1ge0: 0 <= h - 1 by rewrite subr_ge0 ler1n cardG_gt0. have{h1ge0} u_ge0: 0 <= u by rewrite -Lu pmulr_rge0 in h1ge0. have [a_le0 | ] := boolP (a <= 0). by rewrite -mulrN -sqrrN addr_ge0 ?(u_ge0, mulr_ge0) ?oppr_ge0 ?ler0n. rewrite -real_ltNge ?Creal_Cint // lt_def => /andP[]. move/(norm_Cint_ge1 Za)=> a_ge1 a_ge0; rewrite mulrA -mulrBl. rewrite (normr_idP _) // -(@mulVf _ 2%:R) ?pnatr_eq0 // in a_ge1. rewrite mulr_ge0 // subr_ge0 (le_trans _ (ler_wpM2l u_ge0 a_ge1)) // mulrA. by rewrite ler_wpM2r ?ler0n // -(ler_pM2l L_gt0) mulrA Lu -eh mulfK. have Zchi: chi \in 'Z[irr G] by rewrite def_chi irr_vchar. have def_chi0: {in A, chi^\rho =1 (fun _ => '[beta, chi])}. have defT1: perm_eq calT [:: zeta, Ind1H & S1]. by rewrite defT (perm_catCA Ind1H zeta). move=> x Ax; have [_ Hx] := setD1P Ax. have [c _ -> // _] := invDade_seqInd_sum chi defT1. rewrite big_cons big1_seq ?addr0 /c => [|xi /S1P[neq_xi /= Sxi]]; last first. rewrite zeta1 -nu_tau ?defZS ?S_Se // raddfB cfdotBl raddfZ_Cnat ?NatS1e //. by rewrite cfdotZl !(orthoPr o_chiSnu) ?map_f // mulr0 subr0 conjC0 !mul0r. rewrite Ind1H1 zeta1 divff // scale1r -/beta aut_Cint ?Cint_cfdot_vchar //. by rewrite cfnorm_Ind_cfun1 ?cfInd_cfun1 // cfunE cfuniE // Hx mulr1 divfK. split=> //; rewrite -mulrA mulrCA cfnormE_invDade; congr (_ * _). rewrite mulr_natl -sumr_const; apply: eq_bigr => _ /def_chi0->. by rewrite Cint_normK ?Cint_cfdot_vchar. 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)