proposition: Lemma coherent_FTtype1_core_ltr : a != 0 -> #|K|.-1%:R / v <= u - 1.
proof: Proof. have [nsHL nsKM]: H <| L /\ K <| M by rewrite !gFnormal. have [irr_phi irr_psi] := (irrL Lphi, irrM Mpsi). have frobL: [Frobenius L with kernel H] := FTtype1_Frobenius maxL Ltype1. have [[Itau1 Ztau1] Dtau1] := cohM. have o1M: orthonormal (map tau1M calM). apply: map_orthonormal Itau1 _. exact: sub_orthonormal (undup_uniq _) (irr_orthonormal M). have Lgt1: (1 < size calL)%N by apply: seqInd_nontrivial (mFT_odd _ ) _ Lphi. have [[_ _]] := Dade_Ind1_sub_lin cohL Lgt1 irr_phi Lphi phi1. rewrite -/tauL -/betaL -/calL => ZbetaL [Gamma [_ _ [b _ Dbeta]]]. rewrite odd_Frobenius_index_ler ?mFT_odd // -/u => -[]// _ ub_Ga _ nz_a. have Za: a \in Cint by rewrite Cint_cfdot_vchar // ?Ztau1 ?mem_zchar. have [X M_X [Del [defGa oXD oDM]]] := orthogonal_split (map tau1M calM) Gamma. apply: le_trans ub_Ga; rewrite defGa cfnormDd // ler_wpDr ?cfnorm_ge0 //. suffices ->: '[X] = (a / v) ^+ 2 * (\sum_(xi <- calM) xi 1%g ^+ 2 / '[xi]). rewrite sum_seqIndC1_square // -(natrB _ (cardG_gt0 K)) subn1. rewrite exprMn !mulrA divfK ?neq0CiG // mulrAC -mulrA. by rewrite ler_peMl ?sqr_Cint_ge1 // divr_ge0 ?ler0n. have [_ -> defX] := orthonormal_span o1M M_X. have Mgt1: (1 < size calM)%N by apply: seqInd_nontrivial (mFT_odd _ ) _ Mpsi. have [[oM1 _ _] _ _] := Dade_Ind1_sub_lin cohM Mgt1 irr_psi Mpsi psi1. rewrite exprMn -(Cint_normK Za) -[v]normr_nat -normfV -/v mulr_sumr. rewrite defX cfnorm_sum_orthonormal // big_map; apply: eq_big_seq => xi Mxi. have Zxi1 := Cint_seqInd1 Mxi; rewrite -(Cint_normK Zxi1) -(conj_Cint Zxi1). rewrite irrWnorm ?irrM // divr1 -!exprMn -!normrM; congr (`|_| ^+ 2). rewrite -mulrA mulrC -mulrA; apply: canRL (mulKf (neq0CiG _ _)) _. rewrite -(canLR (addrK _) defGa) cfdotBl (orthoPl oDM) ?map_f // subr0. rewrite -(canLR (addKr _) Dbeta) cfdotDl cfdotNl cfdotC cfdotDr cfdotBr. rewrite (orthoPr oM1) ?map_f // (orthogonalP oML) ?map_f // subrr add0r. rewrite cfdotZr cfdot_sumr big1_seq ?mulr0 ?oppr0 => [|nu Mnu]; last first. by rewrite cfdotZr (orthogonalP oML) ?map_f ?mulr0. apply/eqP; rewrite conjC0 oppr0 add0r -subr_eq0 -conjC_nat -!cfdotZr. rewrite -raddfZnat -raddfZ_Cint // -cfdotBr -raddfB -/v -psi1. rewrite Dtau1 ?zcharD1_seqInd ?sub_seqInd_zchar //. rewrite (cfdotElr (Dade_cfunS _ _) (Dade_cfunS _ _)) setIC. by have:= TItauML; rewrite -setI_eq0 => /eqP->; rewrite big_set0 mulr0. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop order prime binomial ssralg poly finset) mathcomp(fingroup morphism perm automorphism quotient action finalg zmodp) mathcomp(gfunctor gproduct center cyclic commutator gseries nilpotent) mathcomp(pgroup sylow hall abelian maximal frobenius) mathcomp(matrix mxalgebra mxrepresentation mxabelem vector) odd_order(BGsection1 BGsection3 BGsection7) odd_order(BGsection14 BGsection15 BGsection16 BGappendixC) mathcomp(ssrnum rat algC cyclotomic algnum) mathcomp(classfun character integral_char inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3 PFsection4) odd_order(PFsection5 PFsection6 PFsection7 PFsection8 PFsection9) odd_order(PFsection10 PFsection11 PFsection12 PFsection13)