proposition: Lemma extend_coherent S1 xi1 chi : cfConjC_subset S1 S -> xi1 \in S1 -> chi \in S -> chi \notin S1 -> [/\ coherent S1 L^# tau, (xi1 1%g %| chi 1%g)%C & 2%:R * chi 1%g * xi1 1%g < \sum_(xi <- S1) xi 1%g ^+ 2 / '[xi]] -> coherent (chi :: chi^*%CF :: S1) L^# tau.
proof: Proof. move=> ccsS1S S1xi1 Schi notS1chi [[tau1 cohS1] xi1_dv_chi1 ub_chi1]. have [[uS1 sS1S ccS1] [[Itau1 Ztau1] Dtau1]] := (ccsS1S, cohS1). have{xi1_dv_chi1} [a Za chi1] := dvdCP _ _ xi1_dv_chi1. have [[N_S nrS ccS] ZItau oS R_P oR] := cohS; have [Itau Ztau] := ZItau. have [Sxi1 [ZRchi o1Rchi sumRchi]] := (sS1S _ S1xi1, R_P _ Schi). have ocS1 xi: xi \in S1 -> '[chi, xi] = 0. by apply: orthoPl; rewrite orthogonal_sym subset_ortho_subcoherent. have /andP[/memPn/=nzS _] := oS; have [Nchi nz_chi] := (N_S _ Schi, nzS _ Schi). have oS1: pairwise_orthogonal S1 by apply: sub_pairwise_orthogonal oS. have [freeS freeS1] := (orthogonal_free oS, orthogonal_free oS1). have nz_nS1 xi: xi \in S1 -> '[xi] != 0 by rewrite cfnorm_eq0 => /sS1S/nzS. have nz_xi11: xi1 1%g != 0 by rewrite char1_eq0 ?N_S ?nzS. have inj_tau1: {in 'Z[S1] &, injective tau1} := Zisometry_inj Itau1. have Z_S1: {subset S1 <= 'Z[S1]} by move=> xi /mem_zchar->. have inj_tau1_S1: {in S1 &, injective tau1} := sub_in2 Z_S1 inj_tau1. pose a_ t1xi := S1`_(index t1xi (map tau1 S1)) 1%g / xi1 1%g / '[t1xi]. have a_E xi: xi \in S1 -> a_ (tau1 xi) = xi 1%g / xi1 1%g / '[xi]. by move=> S1xi; rewrite /a_ nth_index_map // Itau1 ?Z_S1. have a_xi1 : a_ (tau1 xi1) = '[xi1]^-1 by rewrite a_E // -mulrA mulVKf //. have Zachi: chi - a *: xi1 \in 'Z[S, L^#]. by rewrite zcharD1E !cfunE -chi1 subrr rpredB ?scale_zchar ?mem_zchar /=. have Ztau_achi := zcharW (Ztau _ Zachi). have [X R_X [Y defXY]] := subcoherent_split Schi Ztau_achi. have [eqXY oXY oYRchi] := defXY; pose X1 := map tau1 (in_tuple S1). suffices defY: Y = a *: tau1 xi1. by move: eqXY; rewrite defY; apply: extend_coherent_with; rewrite -?defY. have oX1: pairwise_orthogonal X1 by apply: map_pairwise_orthogonal. have N_S1_1 xi: xi \in S1 -> xi 1%g \in Cnat by move/sS1S/N_S/Cnat_char1. have oRchiX1 psi: psi \in 'Z[R chi] -> orthogonal psi X1. move/zchar_span=> Rpsi; apply/orthoPl=> chi2 /memv_span. by apply: span_orthogonal Rpsi; rewrite orthogonal_sym coherent_ortho_supp. have [lam Zlam [Z oZS1 defY]]: exists2 lam, lam \in Cint & exists2 Z : 'CF(G), orthogonal Z (map tau1 S1) & Y = a *: tau1 xi1 - lam *: (\sum_(xi <- X1) a_ xi *: xi) + Z. - pose lam := a * '[xi1] - '[Y, tau1 xi1]; exists lam. rewrite rpredD ?mulr_natl ?rpredN //. by rewrite rpredM // CintE Cnat_cfdot_char ?N_S. rewrite Cint_cfdot_vchar ?Ztau1 ?Z_S1 // -(subrK X Y) -opprB -eqXY addrC. by rewrite rpredB // (zchar_trans ZRchi). set Z' := _ - _; exists (Y - Z'); last by rewrite addrC subrK. have oXtau1 xi: xi \in S1 -> '[Y, tau1 xi] = - '[X - Y, tau1 xi]. move=> S1xi; rewrite cfdotBl opprB. by rewrite (orthogonalP (oRchiX1 X R_X) X) ?subr0 ?mem_head ?map_f. apply/orthogonalP=> _ _ /predU1P[-> | //] /mapP[xi S1xi ->]. rewrite !cfdotBl !cfdotZl Itau1 ?mem_zchar //. rewrite cfproj_sum_orthogonal ?map_f // a_E // Itau1 ?Z_S1 //. apply: (mulIf nz_xi11); rewrite divfK ?nz_nS1 // 2!mulrBl. rewrite [in lam * _]mulrA divfK // mul0r mulrBl opprB. rewrite -addrA [_ * xi1 _ + _]addrCA [a * _ * _ + _]addrC. rewrite !addrA !oXtau1 // !mulNr. rewrite -(conj_Cnat (N_S1_1 _ S1xi)) -(conj_Cnat (N_S1_1 _ S1xi1)). rewrite opprK [- _ + _]addrC -!(mulrC _^*) -!cfdotZr -cfdotBr. rewrite -!raddfZ_Cnat ?N_S1_1 // -raddfB; set beta : 'CF(L) := _ - _. have Zbeta: beta \in 'Z[S1, L^#]. rewrite zcharD1E !cfunE mulrC subrr eqxx. by rewrite rpredB ?rpredZ_Cint ?Z_S1 // CintE N_S1_1. rewrite -eqXY Dtau1 // Itau // ?(zchar_subset sS1S) //. rewrite cfdotBl !cfdotBr !cfdotZr !ocS1 // !mulr0 subrr add0r !cfdotZl. by rewrite opprB addrAC subrK subrr. have [||leXchi _] := subcoherent_norm _ _ (erefl _) defXY. - rewrite Schi scale_zchar ?char_vchar ?N_S /orthogonal //= !cfdotZr ocS1 //. by rewrite -[xi1]cfConjCK cfdot_conjC ocS1 ?ccS1 // conjC0 mulr0 eqxx. - apply: sub_iso_to ZItau; [apply: zchar_trans_on; apply/allP | exact: zcharW]. rewrite /= Zachi sub_aut_zchar ?zchar_onG ?mem_zchar ?ccS //. by move=> xi /N_S/char_vchar. have normXY: '[X] + '[Y] = '[chi] + '[a *: xi1]. by rewrite -!cfnormBd // ?cfdotZr ?ocS1 ?mulr0 // -eqXY Itau. have{leXchi normXY}: '[Y] <= a ^+ 2 * '[xi1]. by rewrite -(lerD2l '[X]) normXY cfnormZ Cint_normK // lerD2r. rewrite {}defY cfnormDd; last first. rewrite cfdotC (span_orthogonal oZS1) ?rmorph0 ?memv_span1 //. rewrite big_seq memvB ?memvZ ?memv_suml ?memv_span ?map_f //. by move=> theta S1theta; rewrite memvZ ?memv_span. rewrite -cfnormN opprB cfnormB !cfnormZ !Cint_normK // addrAC lerBlDl. rewrite cfdotZl cfdotZr cfnorm_sum_orthogonal ?cfproj_sum_orthogonal ?map_f //. rewrite a_xi1 Itau1 ?Z_S1 // addrAC lerD2r !(divfK, mulrA) ?nz_nS1 //. rewrite !conj_Cint ?rpredM // => /le_gtF-lb_2_lam_a. suffices lam0: lam = 0; last apply: contraFeq lb_2_lam_a => nz_lam. suffices ->: Z = 0 by rewrite lam0 scale0r subrK. by apply: contraFeq lb_2_lam_a; rewrite -cfnorm_gt0 lam0 expr0n !mul0r !add0r. rewrite ltr_wpDr ?cfnorm_ge0 // -mulr2n -mulr_natl mulrCA. have xi11_gt0: xi1 1%g > 0 by rewrite char1_gt0 ?N_S ?sS1S -?cfnorm_eq0 ?nz_nS1. have a_gt0: a > 0 by rewrite -(ltr_pM2r xi11_gt0) mul0r -chi1 char1_gt0. apply: le_lt_trans (_ : lam ^+ 2 * (2%:R * a) < _). by rewrite ler_pM2r ?mulr_gt0 ?ltr0n ?Cint_ler_sqr. rewrite ltr_pM2l ?(lt_le_trans ltr01) ?sqr_Cint_ge1 {lam Zlam nz_lam}//. rewrite -(ltr_pM2r xi11_gt0) -mulrA -chi1 -(ltr_pM2r xi11_gt0). congr (_ < _): ub_chi1; rewrite -mulrA -expr2 mulr_suml big_map. apply/eq_big_seq=> xi S1xi; rewrite a_E // Itau1 ?mem_zchar //. rewrite ger0_norm ?divr_ge0 ?cfnorm_ge0 ?char1_ge0 ?N_S ?sS1S //. rewrite [_ / _ / _]mulrAC [RHS]mulrAC -exprMn divfK //. by rewrite [RHS]mulrAC divfK ?nz_nS1 // mulrA. 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 zmodp) mathcomp(gfunctor gproduct cyclic pgroup frobenius) mathcomp(matrix mxalgebra mxrepresentation vector ssrint) mathcomp(ssrnum algC classfun character inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3 PFsection4)