proposition: 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: 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 := 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.
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)