Timings for PFsection7.v

(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.                  *)
(* Distributed under the terms of CeCILL-B.                                  *)
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp
Require Import ssrbool ssrfun eqtype ssrnat seq path div choice.
From mathcomp
Require Import fintype tuple finfun bigop prime ssralg poly finset center.
From mathcomp
Require Import fingroup morphism perm automorphism quotient action zmodp.
From mathcomp
Require Import gfunctor gproduct cyclic pgroup commutator nilpotent frobenius.
From mathcomp
Require Import matrix mxalgebra mxrepresentation BGsection3 vector.
From mathcomp
Require Import ssrnum algC classfun character inertia vcharacter.
From mathcomp
Require Import PFsection1 PFsection2 PFsection4 PFsection5 PFsection6.

(******************************************************************************)
(* This file covers Peterfalvi, Section 7:                                    *)
(* Non-existence of a Certain Type of Group of Odd Order                      *)
(* Defined here:                                                              *)
(*    inDade ddA == the right inverse to the Dade isometry with respect to G, *)
(*                  L, A, given ddA : Dade_hypothesis G L A.                  *)
(*      phi^\rho == locally-bindable Notation for invDade ddA phi.            *)
(******************************************************************************)

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Import GroupScope GRing.Theory Num.Theory.
Local Open Scope ring_scope.

Reserved Notation "alpha ^\rho" (at level 2, format "alpha ^\rho").

Section Seven.

Variables (gT : finGroupType) (G : {group gT}).
Implicit Types (L H P : {group gT}) (DH : gT -> {group gT}).

(* Properties of the inverse to the Dade isometry (Peterfalvi (7.1) to (7.3). *)
Section InverseDade.

Variables (A : {set gT}) (L : {group gT}).
Hypothesis ddA : Dade_hypothesis G L A.

Local Notation "alpha ^\tau" := (Dade ddA alpha).
Local Notation Atau := (Dade_support ddA).
Local Notation H := (Dade_signalizer ddA).

Let nsAL : A <| L. Proof. by have [] := ddA. Qed.
Let sAL : A \subset L. Proof. exact: normal_sub nsAL. Qed.
Let nAL : L \subset 'N(A). Proof. exact: normal_norm nsAL. Qed.
Let sLG : L \subset G. Proof. by have [] := ddA. Qed.

(* This is the Definition embedded in Peterfalvi, Hypothesis (7.1). *)
Fact invDade_subproof (chi : 'CF(G)) :
  is_class_fun <<L>>
    [ffun a => #|H a|%:R^-1 * (\sum_(x in H a) chi (x * a)%g) *+ (a \in A)].
Proof.
rewrite genGid; apply: intro_class_fun => [x y Lx Ly | x notLx]; last first.
  by rewrite (contraNF (subsetP sAL x)).
rewrite memJ_norm ?(subsetP nAL) // !mulrb; case: ifP => // Ax.
rewrite (DadeJ ddA) // cardJg; congr (_ * _).
rewrite big_imset /= => [|z y0 _ _ /=]; last exact: conjg_inj.
by apply: eq_bigr => u Hu; rewrite -conjMg cfunJ // (subsetP sLG).
Qed.
Definition invDade alpha := Cfun 1 (invDade_subproof alpha).  

Local Notation "alpha ^\rho" := (invDade alpha).

Fact invDade_is_linear : linear invDade.
Proof.
move=> mu alpha beta; apply/cfunP=> a; rewrite !cfunElock.
rewrite mulrnAr -mulrnDl mulrCA -mulrDr; congr (_ * _ *+ _).
by rewrite big_distrr -big_split; apply: eq_bigr => x _; rewrite !cfunE.
Qed.
Canonical invDade_linear := Linear invDade_is_linear.
Canonical invDade_additive := Additive invDade_is_linear.

Lemma invDade_on chi : chi^\rho \in 'CF(L, A).
Proof. by apply/cfun_onP=> x notAx; rewrite cfunElock (negPf notAx). Qed.

Lemma invDade_cfun1 : 1^\rho = '1_A.
Proof.
apply/cfunP=> x; rewrite cfuniE // cfunElock mulrb; case: ifP => //= Ax.
apply: canLR (mulKf (neq0CG _)) _; rewrite mulr1 -sumr_const.
apply: eq_bigr => u Hu; rewrite cfun1E (subsetP (subsetIl G 'C[x])) //.
have /sdprodP[_ <- _ _] := Dade_sdprod ddA Ax.
by rewrite mem_mulg // inE cent1id (subsetP sAL).
Qed.

(* This is Peterfalvi (2.7), restated using invDade. *)
Lemma invDade_reciprocity chi alpha :
  alpha \in 'CF(L, A) -> '[alpha^\tau, chi] = '[alpha, chi^\rho].
Proof.
move=> Aalpha; apply: general_Dade_reciprocity => //= a Aa.
by rewrite cfunElock Aa.
Qed.

(* This is Peterfalvi (7.2)(a). *)
Lemma DadeK alpha : alpha \in 'CF(L, A) -> (alpha^\tau)^\rho = alpha.
Proof.
move=> Aalpha; apply/cfunP=> a; rewrite cfunElock mulrb.
case: ifPn => [Aa | /cfun_on0-> //]; apply: canLR (mulKf (neq0CG _)) _.
rewrite mulr_natl -sumr_const; apply: eq_bigr => x Hx.
by rewrite (DadeE _ Aa) ?mem_class_support // mem_mulg ?set11.
Qed.

(* This is Peterfalvi (7.2)(b); note that by (7.2)(a) chi is in the image of  *)
(* tau iff chi = (chi^\rho)^\tau, and this condition is easier to write.      *)
Lemma leC_norm_invDade chi :
  '[chi^\rho] <= '[chi] ?= iff (chi == (chi^\rho)^\tau).
Proof.
have Achi_rho := invDade_on chi; rewrite -(Dade_isometry ddA) //.
set chi1 := _^\tau; rewrite -subr_eq0 -cfnorm_eq0; set mu := chi - chi1.
have owv: '[chi1, mu] = 0.
  by rewrite invDade_reciprocity ?raddfB //= DadeK ?subrr.
rewrite -(subrK chi1 chi) -/mu addrC cfnormD owv conjC0 !addr0.
split; first by rewrite -subr_ge0 addrC addKr cfnorm_ge0.
by rewrite eq_sym addrC -subr_eq0 addrK.
Qed.

(* This is Peterfalvi (7.3). *)
Lemma leC_cfnorm_invDade_support chi :
  '[chi^\rho] <= #|G|%:R^-1 * (\sum_(g in Atau) `|chi g| ^+ 2)
     ?= iff [forall a in A, forall u in H a, chi (u * a)%g == chi a].
Proof.
have nsAtauG: Atau <| G := Dade_support_normal ddA.
pose chi1 := chi * '1_Atau; set RHS := _ * _.
have inA1 a x: a \in A -> x \in H a -> (x * a)%g \in Dade_support1 ddA a.
  by move=> Aa Hx; rewrite mem_class_support ?mem_mulg ?set11.
have chi1E a x: a \in A -> x \in H a -> chi1 (x * a)%g = chi (x * a)%g.
  move=> Aa Hx; rewrite cfunE cfuniE // mulr_natr mulrb.
  by case: bigcupP => // [[]]; exists a; rewrite ?inA1.
have ->: chi^\rho = chi1^\rho.
  apply/cfunP => a; rewrite !cfunElock !mulrb; case: ifP => // Aa.
  by congr (_ * _); apply: eq_bigr => x /chi1E->.
have Achi1: chi1 \in 'CF(G, Atau).
  by apply/cfun_onP=> x ?; rewrite cfunE (cfun_onP (cfuni_on _ _)) ?mulr0.
have{Achi1 RHS} <-: '[chi1] = RHS.
  rewrite (cfnormE Achi1); congr (_ * _).
  by apply: eq_bigr => x Atau_x; rewrite cfunE cfuniE // Atau_x mulr1.
congr (_ <= _ ?= iff _): (leC_norm_invDade chi1).
apply/eqP/forall_inP=> [chi1_id a Aa | chi_id].
  apply/forall_inP => x Ha_x; rewrite -{2}[a]mul1g -!chi1E // chi1_id mul1g.
  by rewrite (DadeE _ Aa) ?inA1 ?Dade_id.
apply/cfunP => g; rewrite cfunE cfuniE // mulr_natr mulrb.
case: ifPn => [/bigcupP[a Aa] | /(cfun_onP (Dade_cfunS _ _))-> //].
case/imset2P=> _ z /rcosetP[x Hx ->] Gz ->{g}; rewrite !cfunJ {z Gz}//.
have{chi_id} chi_id := eqP (forall_inP (chi_id a Aa) _ _).
rewrite chi_id // (DadeE _ Aa) ?inA1 {x Hx}// cfunElock mulrb Aa.
apply: canRL (mulKf (neq0CG _)) _; rewrite mulr_natl -sumr_const.
by apply: eq_bigr => x Hx; rewrite chi1E ?chi_id.
Qed.

(* This is the norm expansion embedded in Peterfalvi (7.3). *)
Lemma cfnormE_invDade chi :
  '[chi^\rho] = #|L|%:R^-1 * (\sum_(a in A) `|chi^\rho a| ^+ 2).
Proof. by apply: cfnormE; apply: invDade_on. Qed.

End InverseDade.

(* Hypothesis (7.4) and Lemma (7.5). *)
Section DadeCoverInequality.

(* These declarations correspond to Peterfalvi, Hypothesis (7.4); as it is    *)
(* only instantiated twice after this section we leave it unbundled.          *)
Variables (I : finType) (L : I -> {group gT}) (A : I -> {set gT}).
Hypothesis ddA : forall i : I, Dade_hypothesis G (L i) (A i).

Local Notation Atau i := (Dade_support (ddA i)).
Local Notation "alpha ^\rho" := (invDade (ddA _) alpha).
Hypothesis disjointA : forall i j, i != j -> [disjoint Atau i & Atau j].

(* This is Peterfalvi (7.5), generalised to all class functions of norm 1. *)
Lemma Dade_cover_inequality (chi : 'CF(G)) (G0 := G :\: \bigcup_i Atau i) :
    '[chi] = 1 ->
  #|G|%:R^-1 * (\sum_(g in G0) `|chi g| ^+ 2 - #|G0|%:R)
    + \sum_i ('[chi^\rho]_(L i) - #|A i|%:R / #|L i|%:R) <= 0.
Proof.
move=> Nchi1; set vG := _^-1; rewrite sumrB /= addrCA mulrBr -addrA.
pose F (xi : 'CF(G)) (B : {set gT}) := vG * \sum_(g in B) `|xi g| ^+ 2.
have sumF xi: F xi G0 + \sum_i F xi (Atau i) = '[xi].
  rewrite (cfnormE (cfun_onG _)) -mulr_sumr -mulrDr; congr (_ * _).
  rewrite -partition_disjoint_bigcup //=; set U_A := \bigcup_i _.
  have sUG: U_A \subset G by apply/bigcupsP=> i _; apply: Dade_support_sub.
  by rewrite -(setIidPr sUG) addrC -big_setID.
have ->: \sum_i #|A i|%:R / #|L i|%:R = \sum_i F 1 (Atau i).
  apply: eq_bigr => i _; apply/eqP; rewrite /F.
  have [[/andP[sAL nAL] _ _ _ _] sHG] := (ddA i, Dade_signalizer_sub (ddA i)).
  rewrite -{1}[A i]setIid -cfdot_cfuni /normal ?sAL // -(invDade_cfun1 (ddA i)).
  rewrite leC_cfnorm_invDade_support; apply/forall_inP=> a Aa.
  by apply/forall_inP=> x Hx; rewrite !cfun1E groupMl // (subsetP (sHG a)).
have ->: vG * #|G0|%:R = F 1 G0.
  congr (_ * _); rewrite -sumr_const; apply: eq_bigr => x /setDP[Gx _].
  by rewrite cfun1E Gx normr1 expr1n.
rewrite -opprD sumF cfnorm1 -Nchi1 -sumF opprD addNKr -oppr_ge0 opprB -sumrB.
by rewrite sumr_ge0 // => i _; rewrite subr_ge0 leC_cfnorm_invDade_support.
Qed.

(*
set vG := _^-1; rewrite sumrB /= addrCA mulrBr -addrA.
pose F t (B : {set gT}) := vG * \sum_(g in B) `|'chi[G]_t g| ^+ 2.
have sumF t: F t G0 + \sum_i F t (Atau i) = 1.
  rewrite -(cfnorm_irr t) (cfnormE (cfun_onG _)) -mulr_sumr -mulrDr.
  congr (_ * _); rewrite -partition_disjoint_bigcup //=; set U_A := \bigcup_i _.
  have sUG: U_A \subset G by apply/bigcupsP=> i _; apply: Dade_support_sub.
  by rewrite -(setIidPr sUG) addrC -big_setID.
have ->: \sum_i #|A i|%:R / #|L i|%:R = \sum_i F 0 (Atau i).
  apply: eq_bigr => i _; apply/eqP; rewrite /F irr0.
  have [[/andP[sAL nAL] _ _ _ _] sHG] := (ddA i, Dade_signalizer_sub (ddA i)).
  rewrite -{1}[A i]setIid -cfdot_cfuni /normal ?sAL // -(invDade_cfun1 (ddA i)).
  rewrite leC_cfnorm_invDade_support; apply/forall_inP=> a Aa.
  by apply/forall_inP=> x Hx; rewrite !cfun1E groupMl // (subsetP (sHG a)).
have ->: vG * #|G0|%:R = F 0 G0.
  congr (_ * _); rewrite -sumr_const; apply: eq_bigr => x /setDP[Gx _].
  by rewrite irr0 cfun1E Gx normr1 expr1n.
rewrite -opprD sumF -(sumF r) opprD addNKr -oppr_ge0 opprB -sumrB.
by rewrite sumr_ge0 // => i _; rewrite subr_ge0 leC_cfnorm_invDade_support.
Qed.
*)

End DadeCoverInequality.

(* Hypothesis (7.6), and Lemmas (7.7) and (7.8) *)
Section Dade_seqIndC1.

(* In this section, A = H^# with H <| L. *)
Variables L H : {group gT}.
Let A := H^#.
Hypothesis ddA : Dade_hypothesis G L A.

Local Notation Atau := (Dade_support ddA).
Local Notation "alpha ^\tau" := (Dade ddA alpha).
Local Notation "alpha ^\rho" := (invDade ddA alpha).

Let calT := seqIndT H L.
Local Notation calS := (seqIndD H L H 1).
Local Notation Ind1H := ('Ind[gval L, gval H] 1).
Let uniqS : uniq calS := seqInd_uniq _ _.

Let h := #|H|%:R : algC.
Let e := #|L : H|%:R : algC.

Let nsAL : A <| L. Proof. by have [] := ddA. Qed.
Let sLG : L \subset G. Proof. by have [] := ddA. Qed.
Let nsHL : H <| L. Proof. by rewrite -normalD1. Qed.
Let sHL := normal_sub nsHL.
Let nHL := normal_norm nsHL.

Let nzh : h != 0 := neq0CG H.
Let nze : e != 0 := neq0CiG L H.
Let nzL : #|L|%:R != 0 := neq0CG L.

Let eh : e * h = #|L|%:R. Proof. by rewrite -natrM mulnC Lagrange. Qed.

Section InvDadeSeqInd.

Variables (xi0 : 'CF(L)) (S : seq 'CF(L)) (chi : 'CF(G)).
Implicit Types xi mu : 'CF(L).

Let d xi := xi 1%g / xi0 1%g.
Let psi xi := xi - d xi *: xi0.
Let c xi := '[(psi xi)^\tau, chi].

Let uc c xi mu := (c xi)^* * c mu / ('[xi] * '[mu]).
Let u c xi mu := uc c xi mu * ('[xi, mu] - xi 1%g * mu 1%g / (e * h)).

(* This is Peterfalvi (7.7); it is stated using a bespoke concrete Prop so as *)
(* to encapsulate the coefficient definitions given above.                    *)
CoInductive is_invDade_seqInd_sum : Prop :=
  InvDadeSeqIndSum (c := c) (u := u c) of
   (*a*) {in A, forall x, (chi^\rho) x = \sum_(xi <- S) (c xi)^* / '[xi] * xi x}
 & (*b*) '[chi^\rho] = \sum_(xi <- S) \sum_(mu <- S) u xi mu.

Lemma invDade_seqInd_sum : perm_eq calT (xi0 :: S) -> is_invDade_seqInd_sum.
Proof.
move=> defT; pose chi0 := \sum_(xi <- S) (c xi)^* / '[xi] *: xi.
have Txi0: xi0 \in calT by rewrite (perm_eq_mem defT) mem_head.
have sST : {subset S <= calT}.
  by move=> xi Sxi; rewrite (perm_eq_mem defT) mem_behead.
have nz_xi01 : xi0 1%g != 0 by apply: seqInd1_neq0 Txi0.
have part_a: {in A, chi^\rho =1 chi0}.
  pose phi := (chi^\rho - chi0) * '1_A.
  have Aphi : phi \in 'CF(L, A) := mul_cfuni_on A _.
  suffices: '[phi, chi^\rho - chi0] == 0; last clearbody phi.
    rewrite -(eq_cfdotr Aphi (eq_mul_cfuni _ nsAL)) cfnorm_eq0 => /eqP phi0.
    by move=> x Ax; rewrite -[chi0]add0r -phi0 cfunE eq_mul_cfuni ?cfunE ?subrK.
  have{Aphi} [Hphi phi1]: phi \in 'CF(L, H) /\ phi 1%g = 0.
    by move: Aphi; rewrite cfun_onD1 => /andP[-> /eqP].
  have{Hphi} def_phi: phi = e^-1 *: 'Ind ('Res[H] phi).
    apply/cfunP=> y; have [Hy | notHy] := boolP (y \in H); last first.
      by rewrite cfunE !(cfun_on0 _ notHy) ?mulr0 ?cfInd_normal.
    rewrite cfunE cfIndE // mulrA -invfM eh.
    apply: (canRL (mulKf nzL)); rewrite mulr_natl -sumr_const.
    by apply: eq_bigr => z Lz; rewrite cfResE ?memJ_norm ?cfunJ ?(subsetP nHL).
  have{def_phi} Tphi: phi \in <<calT>>%VS.
    rewrite def_phi memvZ // ['Res _]cfun_sum_cfdot linear_sum.
    apply: memv_suml => i _; rewrite linearZ memvZ ?memv_span //=.
    by apply/seqIndP; exists i; rewrite ?inE.
  have{Tphi} [z def_phi _] := free_span (seqInd_free nsHL _) Tphi.
  have {phi def_phi phi1} ->: phi = \sum_(xi <- S) z xi *: psi xi.
    rewrite def_phi (eq_big_perm _ defT) !big_cons /= 2!cfunE in phi1 *.
    rewrite (canRL (mulfK nz_xi01) (canRL (addrK _) phi1)) add0r addrC mulNr.
    rewrite sum_cfunE mulr_suml scaleNr scaler_suml -sumrB.
    by apply: eq_bigr => xi _; rewrite cfunE -mulrA -scalerA -scalerBr.
  rewrite cfdot_suml big1_seq //= => xi Sxi; have Txi := sST xi Sxi.
  rewrite cfdotZl cfdotBr -invDade_reciprocity -/(c xi); last first.
    rewrite cfun_onD1 !cfunE divfK // subrr eqxx andbT.
    by rewrite memvB ?memvZ //= ((seqInd_on _) setT).
  have [oSS /orthoPl o_xi0S]: pairwise_orthogonal S /\ orthogonal xi0 S.
    have:= seqInd_orthogonal nsHL setT; rewrite (eq_pairwise_orthogonal defT).
    by rewrite /= -cat1s pairwise_orthogonal_cat => /and3P[].
  rewrite cfdotBl cfdotC cfproj_sum_orthogonal {oSS}// cfdotZl cfdot_sumr.
  rewrite big1_seq ?mulr0 => [|mu Smu]; last by rewrite cfdotZr o_xi0S ?mulr0.
  by rewrite subr0 divfK ?(cfnorm_seqInd_neq0 _ Txi) // conjCK subrr mulr0.
split=> [x /part_a-> | ].
  by rewrite sum_cfunE; apply: eq_bigr => ?; rewrite cfunE.
rewrite (cfdotEl _ (invDade_on ddA _)) mulrC mulr_suml.
pose F xi mu x := uc c xi mu * (xi x * (mu x)^*) / #|L|%:R.
transitivity (\sum_(x in A) \sum_(xi <- S) \sum_(mu <- S) F xi mu x).
  apply: eq_bigr => x Ax; rewrite part_a // sum_cfunE -mulrA mulr_suml.
  apply: eq_bigr => xi _; rewrite mulrA -mulr_suml rmorph_sum; congr (_ * _).
  rewrite mulr_sumr; apply: eq_bigr => mu _; rewrite !cfunE (cfdotC mu).
  rewrite -{1}[mu x]conjCK -fmorph_div -rmorphM conjCK -4!mulrA 2!(mulrCA _^-1).
  by rewrite (mulrA _^-1) -invfM 2!(mulrCA (xi x)) mulrA 2!(mulrA _^*).
rewrite exchange_big; apply: eq_bigr => xi _; rewrite exchange_big /=.
apply: eq_big_seq => mu Smu; have Tmu := sST mu Smu.
rewrite /u eh (cfdotEr _ (seqInd_on nsHL Tmu)) (mulrC _^-1) -mulrBl mulrA.
rewrite -mulr_suml -mulr_sumr (big_setD1 1%g (group1 H)) /=; congr (_ * _ * _).
by rewrite addrC conj_Cnat ?addKr // (Cnat_seqInd1 Tmu).
Qed.

End InvDadeSeqInd.

Notation "1" := (1 : 'CF(_)) : classfun_scope.

(* This is Peterfalvi (7.8). *)
(* Our version is slightly stronger because we state the nontriviality of S   *)
(* directly than through the coherence premise (see the discussion of (5.2)). *)
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 
  [/\ (*a1*) [/\ orthogonal calSnu 1%CF, '[beta, 1] = 1 & beta \in 'Z[irr G]],
      exists2 Gamma : 'CF(G),
      (*a2*) [/\ orthogonal calSnu Gamma, '[Gamma, 1] = 0
             & exists2 a, a \in Cint & beta = 1 - nu zeta + a *: sumSnu + Gamma]
    & (*b*) e <= (h - 1) / 2%:R ->
            '[(nu zeta)^\rho] >= 1 - e / h /\ '[Gamma] <= e - 1
    & (*c*) {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.
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/perm_eqlP; have Tind1: Ind1H \in calT := seqIndT_Ind1 H L.
  by rewrite (perm_eqlP (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} 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} defX: X = - nu zeta + a *: sumSnu.
  rewrite linear_sum defX big_map !(eq_big_perm _ 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 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_ltrNge ?Creal_Cint // ltr_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 (ler_trans _ (ler_wpmul2l u_ge0 a_ge1)) // mulrA.
  by rewrite ler_wpmul2r ?ler0n // -(ler_pmul2l 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.

End Dade_seqIndC1.

(* The other results of the section are specific to groups of odd order. *)
Hypothesis oddG : odd #|G|.

(* We explicitly factor out several intermediate results from the proof of    *)
(* (7.9) that are reused throughout the proof (including in (7.10) below).    *)

Import ssrint.
Lemma cfdot_real_vchar_even phi psi :
    phi \in 'Z[irr G] /\ cfReal phi  -> psi \in 'Z[irr G] /\ cfReal psi ->
  (2 %| '[phi, psi])%C = (2 %| '[phi, 1])%C || (2 %| '[psi, 1])%C.
Proof.
move=> [Zphi Rphi] [Zpsi Rpsi]; rewrite cfdot_vchar_r // (bigD1 (0 : 'I__)) //=.
rewrite addrC -irr0 (bigID [pred i | conjC_Iirr i < i]%N) /=.
set a1 := \sum_(i | _) _; set a2 := \sum_(i | _) _; suffices ->: a1 = a2.
  rewrite -mulr2n -mulr_natr (rpredDl _ (dvdC_mull _ _)) //; last first.
    by rewrite rpred_sum // => i; rewrite rpredM ?Cint_cfdot_vchar_irr.
  have /CintP[m1 ->] := Cint_cfdot_vchar_irr 0 Zphi.
  have /CintP[m2 ->] := Cint_cfdot_vchar_irr 0 Zpsi.
  rewrite [m1]intEsign [m2]intEsign !rmorphMsign mulrACA -!mulrA !rpredMsign.
  by rewrite -natrM !(dvdC_nat 2) Euclid_dvdM.
rewrite /a2 (reindex_inj (inv_inj (@conjC_IirrK _ _))) /=.
apply: eq_big => [t | t _]; last first.
  by rewrite !conjC_IirrE !cfdot_real_conjC ?aut_Cint ?Cint_cfdot_vchar_irr.
rewrite (inv_eq (@conjC_IirrK _ _)) conjC_IirrK -leqNgt ltn_neqAle val_eqE.
rewrite -!(inj_eq irr_inj) !conjC_IirrE irr0 cfConjC_cfun1 odd_eq_conj_irr1 //.
by rewrite andbA andbb.
Qed.

Section DisjointDadeOrtho.

Variables (L1 L2 H1 H2 : {group gT}).
Let A1 := H1^#.
Let A2 := H2^#.

Hypothesis ddA1 : Dade_hypothesis G L1 A1.
Hypothesis ddA2 : Dade_hypothesis G L2 A2.
Let Atau1 := Dade_support ddA1.
Let tau1 := Dade ddA1.
Let Atau2 := Dade_support ddA2.
Let tau2 := Dade ddA2.

Hypothesis disjointA : [disjoint Atau1 & Atau2].

Lemma disjoint_Dade_ortho phi psi : '[tau1 phi, tau2 psi] = 0.
Proof.
rewrite (cfdot_complement (Dade_cfunS _ _)) ?(cfun_onS _ (Dade_cfunS _ _)) //.
by rewrite subsetD disjoint_sym Dade_support_sub.
Qed.

Let odd_Dade_context L H : Dade_hypothesis G L H^# -> H <| L /\ odd #|L|.
Proof. by case=> nsAL sLG _ _ _; rewrite -normalD1 (oddSg sLG). Qed.

(* This lemma encapsulates uses of lemma (4.1) in sections 7 and 14. *)
Lemma disjoint_coherent_ortho nu1 nu2 chi1 chi2 :
    let S1 := seqIndD H1 L1 H1 1 in coherent_with S1 L1^# tau1 nu1 ->
    let S2 := seqIndD H2 L2 H2 1 in coherent_with S2 L2^# tau2 nu2 ->
    chi1 \in irr L1 -> chi1 \in S1 -> chi2 \in irr L2 -> chi2 \in S2 -> 
  '[nu1 chi1, nu2 chi2] = 0.
Proof.
move=> S1 cohS1 S2 cohS2 /irrP[i1 ->] Schi1 /irrP[i2 ->] Schi2.
have [[nsHL1 oddL1] [[Inu1 Znu1] nu1tau]] := (odd_Dade_context ddA1, cohS1).
have [[nsHL2 oddL2] [[Inu2 Znu2] nu2tau]] := (odd_Dade_context ddA2, cohS2).
pose nu_chiC L (nu : 'CF(L) -> 'CF(G)) i := map nu ('chi_i :: ('chi_i)^*)%CF.
have: orthonormal (nu_chiC L1 nu1 i1) && orthonormal (nu_chiC L2 nu2 i2).
  rewrite /orthonormal /= !andbT !Inu1 ?Inu2 ?seqInd_zcharW ?cfAut_seqInd //=.
  rewrite !cfnorm_conjC !cfnorm_irr (seqInd_conjC_ortho _ _ _ Schi1) ?eqxx //=.
  by rewrite (seqInd_conjC_ortho _ _ _ Schi2).
move/orthonormal_vchar_diff_ortho=> -> //.
  by split; apply/allP; rewrite /= !(Znu1, Znu2) ?seqInd_zcharW ?cfAut_seqInd.
rewrite -!raddfB !(nu1tau, nu2tau) ?zcharD1_seqInd ?seqInd_sub_aut_zchar //.
by rewrite !Dade1 disjoint_Dade_ortho !eqxx.
Qed.

(* This is Peterfalvi (7.9). *)
(* We have inlined Hypothesis (7.4) because although it is readily available  *)
(* for the proof of (7.10), it would be inconvenient to establish in (14.4).  *)
(* Note that our Delta corresponds to Delta - 1 in the Peterfalvi proof.      *)
Let beta L H ddA zeta := @Dade _ G L H^# ddA ('Ind[L, H] 1 - zeta).
Lemma Dade_sub_lin_nonorthogonal nu1 nu2 zeta1 zeta2 :
    let S1 := seqIndD H1 L1 H1 1 in coherent_with S1 L1^# tau1 nu1 -> 
    let S2 := seqIndD H2 L2 H2 1 in coherent_with S2 L2^# tau2 nu2 ->
    zeta1 \in irr L1 -> zeta1 \in S1 -> zeta1 1%g = #|L1 : H1|%:R ->
    zeta2 \in irr L2 -> zeta2 \in S2 -> zeta2 1%g = #|L2 : H2|%:R ->
  '[beta ddA1 zeta1, nu2 zeta2] != 0 \/ '[beta ddA2 zeta2, nu1 zeta1] != 0.
Proof.
move=> S1 cohS1 S2 cohS2 irr_zeta1 Szeta1 zeta1_1 irr_zeta2 Szeta2 zeta2_1.
apply/nandP; pose Delta ddA nu zeta := beta ddA zeta + nu zeta.
have Delta_context L H (A := H^#) ddA (tau := Dade ddA) nu zeta :
    let S := seqIndD H L H 1 in coherent_with S L^# tau nu ->
    zeta \in irr L -> zeta \in S -> zeta 1%g = #|L : H|%:R ->
  let D := Delta L H ddA nu zeta in '[D, 1] = 1 /\ D \in 'Z[irr G] /\ cfReal D.
- move=> S cohS irr_zeta Szeta zeta_1 D.
  have [[nsHL oddL] [[_ Znu] nu_tau]] := (odd_Dade_context ddA, cohS).
  have ntS: (size S > 1)%N by apply: seqInd_nontrivial Szeta.
  have [[nuS1_0 beta1_1 Zbeta] _ _] :=
    Dade_Ind1_sub_lin cohS ntS irr_zeta Szeta zeta_1.
  rewrite cfdotDl {}beta1_1 {nuS1_0}(orthoPr nuS1_0) ?map_f // addr0.
  rewrite rpredD ?{}Znu ?seqInd_zcharW {Zbeta}// /cfReal; do !split=> //.
  rewrite rmorphD /= -subr_eq0 opprD addrAC addrA -addrA addr_eq0 opprD.
  rewrite (cfConjC_Dade_coherent cohS) // opprK -Dade_conjC -!raddfB /=.
  rewrite nu_tau ?zcharD1_seqInd ?seqInd_sub_aut_zchar //=.
  by rewrite rmorphB /= conj_cfInd cfConjC_cfun1 opprB addrC addrA subrK.
have: ~~ (2 %| '[Delta L1 H1 ddA1 nu1 zeta1, Delta L2 H2 ddA2 nu2 zeta2])%C.
  have /Delta_context/(_ irr_zeta1 Szeta1 zeta1_1)[Delta1_1 ZR_Delta1] := cohS1.
  have /Delta_context/(_ irr_zeta2 Szeta2 zeta2_1)[Delta2_1 ZR_Delta2] := cohS2.
  by rewrite cfdot_real_vchar_even // Delta1_1 Delta2_1 (dvdC_nat 2 1).
rewrite cfdotDl !cfdotDr disjoint_Dade_ortho // add0r addrC cfdotC.
apply: contra => /andP[/eqP-> /eqP->]; rewrite conjC0 add0r addr0.
by rewrite (disjoint_coherent_ortho cohS1 cohS2) ?dvdC0.
Qed.

End DisjointDadeOrtho.

(* A numerical fact used in Sections 7 and 14. *)
Lemma odd_Frobenius_index_ler (R : numFieldType) (K L : {group gT}) :
    odd #|L| -> [Frobenius L with kernel K] ->
  #|L : K|%:R <= (#|K|%:R - 1) / 2%:R :> R.
Proof.
move=> oddL /existsP[H frobL]; rewrite ler_pdivl_mulr ?ltr0n // ler_subr_addl.
have ->: #|L : K| = #|H| by have [/index_sdprod] := Frobenius_context frobL.
by rewrite -natrM -mulrS ler_nat muln2 (ltn_odd_Frobenius_ker frobL).
Qed.

(* This final section factors the assumptions common to (7.10) and (7.11).    *)
(* We add solvability of the Frobenius groups, so as not to rely on the       *)
(* theorem of Thompson asserting the nilpotence of Frobenius kernels.         *)

Section CoherentFrobeniusPartition.

Variables (k : nat) (L H E : 'I_k -> {group gT}).

Local Notation A i := (gval (H i))^#.
Let h_ i : algC := #|H i|%:R.
Let e_ i : algC := #|L i : H i|%:R.
Let G0 := G :\: \bigcup_(i < k) class_support (H i)^# G.

Hypothesis k_ge2: (k >= 2)%N.

(*a*) Hypothesis frobeniusL_G :
  forall i, [/\ L i \subset G, solvable (L i) & [Frobenius L i = H i ><| E i]].

(*b*) Hypothesis normedTI_A : forall i, normedTI (A i) G (L i).

(*c*) Hypothesis card_coprime : forall i j, i != j -> coprime #|H i| #|H j|.

(* A numerical fact that is used in both (7.10) and (7.11) *)
Let e_bounds i : 1 < e_ i /\ e_ i <= (h_ i - 1) / 2%:R.
Proof.
have [/oddSg/(_ oddG)oddL _ frobL] := frobeniusL_G i.
rewrite ltr1n odd_Frobenius_index_ler ?(FrobeniusWker frobL) //.
by have [/index_sdprod <-] := Frobenius_context frobL; rewrite cardG_gt1.
Qed.

(* This is Peterfalvi (7.10). *)
Lemma coherent_Frobenius_bound : exists i, let e := e_ i in let h := h_ i in
  (e - 1) * ((h - 2%:R * e - 1) / (e * h) + 2%:R / (h * (h + 2%:R)))
     <= (#|G0|%:R - 1) / #|G|%:R.
Proof.
have [sLG solL frobL] := all_and3 frobeniusL_G.
have oddL i := oddSg (sLG i) oddG.
have /all_and2[nsHL ntH] i: H i <| L i /\ H i :!=: 1%g.
  by case/Frobenius_context: (frobL i) => /sdprod_context[].
have sHL i: H i \subset L i by case/andP: (nsHL i).
pose DH i := @Dade_signalizer gT G (L i) (A i).
have /fin_all_exists[ddA DH1] i: exists dd, {in A i, forall a, DH i dd a = 1%G}.
  have /Dade_normedTI_P[|ddAi _] := normedTI_A i; last by exists ddAi.
  by apply: normedTI_Dade => //; rewrite setSD // (subset_trans (sHL i)).
pose tau i := Dade (ddA i); pose rho i := invDade (ddA i).
pose Atau i := Dade_support (ddA i).
have defAtau i: Atau i = class_support (A i) G.
  rewrite class_supportEl; apply: eq_bigr => x Ax.
  by rewrite /Dade_support1 -/(DH i) DH1 // mul1g class_support_set1l.
have disjoint_Atau i j : i != j -> [disjoint Atau i & Atau j].
  move=> neq_ij; rewrite !defAtau !class_supportEr -setI_eq0 big_distrlr /=.
  rewrite pair_big big1 // => [[x y] _] /=; apply/eqP.
  by rewrite !conjD1g -setDIl setD_eq0 coprime_TIg // !cardJg card_coprime.
have{defAtau} defG0: G0 = G :\: \bigcup_i Atau i.
  by congr (_ :\: _); apply: eq_bigr => i; rewrite defAtau.
pose S i := seqIndD (H i) (L i) (H i) 1.
have irrS i: {subset S i <= irr (L i)}.
  move=> _ /seqIndC1P[t nz_t ->]; rewrite irr_induced_Frobenius_ker //.
  exact: FrobeniusWker (frobL i).
have /fin_all_exists[r lin_r] i: exists r, 'chi_r \in S i /\ 'chi_r 1%g = e_ i.
  have lt1Hi: [1] \proper H i by rewrite proper1G.
  have solHi := solvableS (sHL i) (solL i).
  have [xi Sxi lin_xi] := exists_linInd (nsHL i) solHi lt1Hi (normal1 _).
  by have /irrP[r def_xi] := irrS i xi Sxi; exists r; rewrite -def_xi.
have{lin_r} [Sr r1] := all_and2 lin_r.
have ntS i: (size (S i) > 1)%N by apply: seqInd_nontrivial (Sr i).
have /fin_all_exists[nu cohS] i: coherent (S i) (L i)^# 'Ind[G, L i].
  have [[[frobLi tiAiL] sLiG] oddLi] := (frobL i, normedTI_A i, sLG i, oddL i).
  have [defLi ntHi ntEi _ _] := Frobenius_context frobLi.
  have{ntEi} nilHi: nilpotent (H i) by apply: (Frobenius_sol_kernel_nil frobLi).
  exact: Sibley_coherence (or_introl _ frobLi).
have{cohS} [/all_and2[Inu Znu] nu_Ind] := all_and2 cohS.
have{DH DH1 nu_Ind} cohS i: coherent_with (S i) (L i)^# (tau i) (nu i).
  split=> // phi Sphi; rewrite /tau nu_Ind ?Dade_Ind //.
  by rewrite (@zchar_on _ _ (S i)) -?zcharD1_seqInd.
have n1S i xi: xi \in S i -> '[xi] = 1.
  by case/irrS/irrP=> t ->; rewrite cfnorm_irr.
have n1Snu i xi: xi \in S i -> '[nu i xi] = 1.
  by move=> Sxi; rewrite Inu ?n1S ?seqInd_zcharW.
have o_nu i j: i != j -> {in S i & S j, forall xi xj, '[nu i xi, nu j xj] = 0}.
  move/disjoint_Atau/disjoint_coherent_ortho=> o_ij xi xj Sxi Sxj.
  by rewrite o_ij ?irrS //; apply: cohS.
have /all_and2[nze nzh] i: e_ i != 0 /\ h_ i != 0 by rewrite neq0CiG neq0CG.
have h_gt1 i: 1 < h_ i by rewrite ltr1n cardG_gt1.
have eh i: e_ i * h_ i = #|L i|%:R by rewrite -natrM mulnC Lagrange.
have def_h1 i: h_ i - 1 = #|A i|%:R.
  by rewrite /h_ (cardsD1 1%g) group1 addnC natrD addrK.
have [i1 min_i1]: {i1 | forall i, i != i1 -> h_ i1 + 2%:R <= h_ i}.
  exists [arg min_(i < Ordinal k_ge2) #|H i|]; case: arg_minP => // i1 _ min_i1.
  have oddH i: #|H i| = #|H i|./2.*2.+1.
    by rewrite -{1}[#|H i|]odd_double_half (oddSg (sHL i)).
  move=> i neq_i; rewrite -natrD ler_nat (oddH i) oddH addn2 -doubleS ltnS.
  rewrite leq_double ltn_neqAle andbC half_leq ?min_i1 //=.
  apply: contraTneq (card_coprime neq_i) => eqHii1.
  by rewrite oddH -eqHii1 -oddH /coprime gcdnn -trivg_card1.
exists i1 => e h; set lhs := (e - 1) * _.
have nzh2: h + 2%:R != 0 by rewrite -natrD addnC pnatr_eq0.
have{lhs} ->: lhs = 1 - e / h - (h - 1) / (e * h) - (e - 1) / (h + 2%:R).
  rewrite {}/lhs -{2}(addrK h 2%:R) !invfM (mulrBl _ _ h) mulVKf ?nzh //.
  rewrite addrCA (addrC _ h) mulrCA mulrA addrA mulrBr; congr (_ - _).
  rewrite mulfK // mulrDr addrAC addrC mulrC mulrBl -mulrA mulVKf ?nze //.
  rewrite mulrC mulrBr mulrBl mul1r addrAC addrC addrA; congr (_ - _).
  rewrite mulrCA mulVKf ?nze // addrCA mulrCA mulr_natl opprD addNKr.
  by rewrite !mulrBl opprB addrA subrK divff ?nzh.
pose beta i := tau i ('Ind[L i, H i] 1 - 'chi_(r i)).
have betaP i := Dade_Ind1_sub_lin (cohS i) (ntS i) (mem_irr _) (Sr i) (r1 i).
pose chi i := nu i 'chi_(r i); pose c i j := '[beta i, chi j].
have:= betaP i1; rewrite -/(S _) -/(tau _) -/(beta _) -/(chi _) -/(e_ _) -/e.
move=> [[oSnu1 o_beta1 Zbeta1] [Gamma [oSnuGamma oGamma1] [a Za def_beta1]]].
have [_ lt_e_h2] := e_bounds i1; rewrite -/(rho _) -/(h_ _) -/h.
case/(_ lt_e_h2)=> min_rho1 maxGamma _ {lt_e_h2}.
pose calB := [set i | (i != i1) && (c i i1 == 0)].
pose sumB := \sum_(i in calB) (h_ i - 1) / (e_ i * h_ i).
suffices{min_rho1} sumB_max: sumB <= (e - 1) / (h + 2%:R).
  rewrite -subr_ge0 opprB addrCA -opprB subr_ge0; apply: ler_trans sumB_max.
  rewrite -subr_ge0 opprB addrCA -(opprB _ sumB) subr_ge0.
  have Zchi1: chi i1 \in 'Z[irr G] by rewrite Znu ?seqInd_zcharW ?Sr.
  have [eps [t def_chi1]] := vchar_norm1P Zchi1 (n1Snu i1 'chi_(r i1) (Sr i1)).
  pose sumG0 := \sum_(g in G0) `|'chi_t g| ^+ 2.
  apply: (@ler_trans _ ((#|G0|%:R - sumG0) / #|G|%:R)); last first.
    rewrite ler_pmul2r ?invr_gt0 ?gt0CG // ler_add2l ler_opp2.
    rewrite [sumG0](bigD1 1%g) /=; last first.
      rewrite !inE group1 andbT; apply/bigcupP=> [[i _]].
      by rewrite class_supportEr => /bigcupP[x _]; rewrite conjD1g !inE eqxx.
    rewrite -[1]addr0 ler_add ?sumr_ge0 // => [|x _]; last first.
      by rewrite -normrX normr_ge0.
    have Zchit1: 'chi_t 1%g \in Cint by rewrite CintE Cnat_irr1.
    by rewrite expr_ge1 ?normr_ge0 // norm_Cint_ge1 ?irr1_neq0.
  pose ea i : algC := #|(H i)^#|%:R / #|L i|%:R.
  apply: (@ler_trans _ (\sum_i ('[rho i 'chi_t] - ea i))); last first.
    rewrite -subr_ge0 -opprB oppr_ge0 -mulNr opprB addrC mulrC.
    by rewrite /sumG0 defG0 Dade_cover_inequality ?cfnorm_irr.
  rewrite (bigID (mem calB)) /= addrC ler_add //.
    rewrite -subr_ge0 opprK -big_split sumr_ge0 //= => i _.
    by rewrite def_h1 eh subrK cfnorm_ge0.
  rewrite (bigD1 i1) ?inE ?eqxx ?andbF //= -ler_subl_addl (@ler_trans _ 0) //.
    rewrite opprB /ea -def_h1 -eh -/h -/e addrA subrK subr_le0.
    by rewrite -(cfnorm_sign eps) -linearZ -def_chi1.
  rewrite sumr_ge0 // => i; rewrite inE /c andbC => /andP[neq_i].
  rewrite neq_i subr_ge0 def_chi1 cfdotZr mulf_eq0 => /norP[_ not_o_beta_chi].
  have [[_ _ Zbeta_i] _ /(_ _ (mem_irr t))[|_ ->]] := betaP i.
    apply/orthoPr=> _ /mapP[xi Sxi ->]; rewrite -['chi_t](signrZK eps).
    by rewrite -def_chi1 cfdotZr o_nu ?mulr0 ?Sr.
  rewrite -[ea i]mulr1 /ea ler_wpmul2l ?mulr_ge0 ?invr_ge0 ?ler0n //.
  by rewrite -/(tau i) -/(beta i) sqr_Cint_ge1 ?Cint_cfdot_vchar_irr.
rewrite -(mulfK nzh2 sumB) -{2 3}natrD ler_wpmul2r ?invr_ge0 ?ler0n //.
apply: ler_trans maxGamma; rewrite mulr_suml.
pose phi i : 'CF(G) := \sum_(xi <- S i) xi 1%g / e_ i / '[xi] *: nu i xi.
have o_phi_nu i j xi: i != j -> xi \in S j -> '[phi i, nu j xi] = 0.
  move/o_nu=> o_ij Sxi; rewrite cfdot_suml big1_seq //= => pi Spi.
  by rewrite cfdotZl o_ij ?mulr0.
have o_phi i j: i != j -> '[phi i, phi j] = 0.
  move/o_phi_nu=> o_ij; rewrite cfdot_sumr big1_seq // => xi Sxi.
  by rewrite cfdotZr o_ij ?mulr0.
pose X : 'CF(G) := \sum_(i in calB) c i1 i *: phi i; pose Gamma1 := Gamma - X.
have ->: Gamma = Gamma1 + X by rewrite subrK.
have{betaP def_beta1} /cfnormDd->: '[Gamma1, X] = 0.
  rewrite cfdot_sumr big1 // => i Bi; have [neq_i _] := setIdP Bi.
  rewrite cfdotZr cfdot_sumr big1_seq ?mulr0 //= => xi Sxi.
  apply/eqP; rewrite cfdotZr cfdotBl mulf_eq0; apply/pred2P; right.
  rewrite cfdot_suml (bigD1 i) ?big1 //= => [|j /andP[_ neq_j]]; last first.
    by rewrite cfdotZl o_phi_nu ?mulr0.
  rewrite cfdotZl cfproj_sum_orthogonal ?seqInd_orthogonal //; last exact: Inu.
  rewrite n1S // divr1 mulr1 addr0 mulrC -(canLR (addKr _) def_beta1).
  rewrite !(cfdotDl, cfdotNl) cfdotZl o_nu ?o_phi_nu ?Sr 1?eq_sym // mulr0.
  have[[/orthoPr oSnui_1 _ _] _ _] := betaP i; rewrite -/(S i) in oSnui_1.
  rewrite cfdotC oSnui_1 ?map_f // conjC0 !(add0r, oppr0).
  have Nxie: xi 1%g / e_ i \in Cnat by apply: dvd_index_seqInd1 _ Sxi.
  rewrite -(conj_Cnat Nxie) // -cfdotZr -raddfZ_Cnat // -!raddfB /=.
  have [_ Dnu] := cohS i.
  rewrite Dnu ?zcharD1_seqInd ?seqInd_sub_lin_vchar ?Sr ?r1 //.
  by rewrite disjoint_Dade_ortho ?disjoint_Atau 1?eq_sym.
rewrite -subr_ge0 cfdot_sumr -addrA -sumrB addr_ge0 ?cfnorm_ge0 //.
rewrite sumr_ge0 // => i Bi; have [neq_i ci1_0] := setIdP Bi.
have n_phi: '[phi i] = (h_ i - 1) / e_ i.
  rewrite cfnorm_sum_orthogonal ?seqInd_orthogonal //; last exact: Inu.
  rewrite -[_ - 1](mulKf (nze i)) -sum_seqIndC1_square // -/(S i) mulrAC.
  rewrite -invfM mulrC mulr_suml; apply: eq_big_seq => _ /irrS/irrP[t ->].
  rewrite cfnorm_irr !divr1 mulr1 -expr2 -exprVn -exprMn.
  by rewrite (normr_idP _) // mulr_ge0 ?invr_ge0 ?ler0n // ltrW ?irr1_gt0.
rewrite subr_ge0 cfdotZr cfdot_suml (bigD1 i) //=.
rewrite big1 ?addr0 => [|j /andP[_ ne_j]]; last by rewrite cfdotZl o_phi ?mulr0.
rewrite cfdotZl invfM 2!mulrA -n_phi -[_ * _]mulrA mulrC.
rewrite ler_wpmul2r ?cfnorm_ge0 // (@ler_trans _ 1) //.
  by rewrite -{2}(mulVf (nzh i)) ler_wpmul2l ?invr_ge0 ?ler0n ?min_i1.
rewrite mulrC -normCK expr_ge1 ?normr_ge0 // norm_Cint_ge1 //.
  rewrite Cint_cfdot_vchar ?Znu ?seqInd_zcharW ?Sr //.
suffices []: c i i1 != 0 \/ c i1 i != 0 by rewrite ?ci1_0.
apply/Dade_sub_lin_nonorthogonal; rewrite ?mem_irr ?Sr ?r1 //; try exact: cohS.
exact: disjoint_Atau.
Qed.

(* This is Peterfalvi (7.11). *)
Theorem no_coherent_Frobenius_partition : G0 != 1%G.
Proof.
have [i] := coherent_Frobenius_bound; apply: contraTneq => ->.
have [] := e_bounds i; set e := e_ i; set h := h_ i => e_gt1 le_e_h2.
rewrite cards1 subrr mul0r ltr_geF // pmulr_rgt0 ?subr_gt0 // ltr_paddl //.
  rewrite ?(mulr_ge0, invr_ge0) ?ler0n // addrAC subr_ge0.
  by rewrite -[_ - 1](@divfK _ 2%:R) ?pnatr_eq0 // mulrC ler_wpmul2r ?ler0n.
by rewrite -natrD addnC ?(pmulr_rgt0, invr_gt0) ?ltr0n.
Qed.

End CoherentFrobeniusPartition.

End Seven.