proposition: Lemma lower_bound_card_Qh (F : finFieldType) (h : {poly F}) k s p (M : {set 'Z_k}) (Q : {set {poly %/ h}}) : Mk_spec F s M -> Qh_spec k s Q -> p \in [char F] -> 1 < order_modn k p -> coprime k p -> monic_irreducible_poly h -> 1 < k -> rdvdp h ('X^k - 1) -> poly_order h 'X k = k -> 0 < s < p -> 2 ^ minn s #|M| <= #|Q|.
proof: Proof. move=> HMk HQh pC pO_gt1 kCp hMI k_gt1 hDxk XoE sB. have hQE : mk_monic h = h by rewrite /mk_monic !hMI. rewrite -/{poly %/ h with hMI} in Q HQh *. set t := minn _ _. have Mk_gt1 : 1 < #|M|. apply: leq_trans pO_gt1 _. apply: is_iexpm_order (HMk) _ => //. by apply: is_iexp_fin_char; rewrite // coprime_sym. have t_gt0 : 0 < t. by rewrite leq_min; case/andP: sB => -> _; rewrite ltnW. have F1 (b : bool) c : c <= s -> is_ipoly k s (('X + (c%:R)%:P :{poly F}) ^+ b). case: b => cD; first by rewrite expr1; apply: is_ipoly_Xaddc. by rewrite expr0; apply: is_ipoly1. have F2 (b : bool) c : c <= s -> size (('X + (c%:R)%:P : {poly F})%R ^+ b) <= 2. case: b => cD; last by rewrite expr0 size_polyC oner_eq0. rewrite (_ : 2%N = maxn(size ('X : {poly F})) (size ((c%:R)%:P : {poly F}))). by rewrite expr1 size_add. by rewrite size_polyX size_polyC; case: eqP. pose m := ([ffun i : 'I_t.+1 => i == ord0] |: [set i | (i : {ffun 'I_t.+1 -> bool}) ord0 == false]) :\ [ffun i : 'I_t.+1 => i != ord0]. have mTrue1 x : x \in m -> exists (i : 'I_t.+1), x i == false. rewrite !inE => /andP[H /orP[/eqP->|xE]]. case: (t) t_gt0 x H => // t1 _ x H. by exists (inZp 1); rewrite !ffunE /=; case: eqP. by exists ord0. have mTrue2 x : 1 < t -> x \in m -> exists (i : 'I_t.+1), exists j, [/\ j != i, x i = false & x j = false]. rewrite /m; case: (t) t_gt0 x => // [] [|t1] // _ x _. rewrite !inE => /andP[H /orP[/eqP->|/eqP xE]]. by exists (inZp 1); exists (inZp 2); rewrite !ffunE. have [/existsP[i /andP[iE /eqP xiE]]|] := boolP [exists i, (i != ord0) && (x i == false)]. by exists ord0; exists i. rewrite negb_exists => /forallP Hf. case/eqP: H; apply/ffunP=> i; rewrite !ffunE. case: eqP => [->|/eqP H] //. case E : (x i) => //. by case/negP: (Hf i); rewrite H // E. have <- : #|m| = 2 ^ t. rewrite cardsDS; last first. by apply/subsetP=> j; rewrite !inE => /eqP->; rewrite ffunE eqxx orbT. rewrite cardsU !cards1. set u := #|_ :&: _|. have /eqP->: u == 0%N. rewrite cards_eq0; apply/eqP/setP=> i; rewrite !inE. by apply/idP => /andP[/eqP->]; rewrite ffunE eqxx. rewrite subn0 addnC addnK. have <- : [set [ffun i => if unlift ord0 i is Some v then f v else false] | f : {ffun 'I_t -> bool}] = [set i | (i : {ffun 'I_t.+1 -> bool}) ord0 == false]. apply/setP=> f; rewrite !inE; apply/imsetP/idP=>[[g _ ->]|/eqP fE]. by rewrite ffunE unlift_none. exists [ffun i => f (fintype.lift ord0 i)]; first by rewrite inE. apply/ffunP=> j; rewrite ffunE; case: unliftP => [v ->|->] //. by rewrite ffunE. rewrite card_imset; first by rewrite card_ffun card_bool card_ord. move=> f g H; apply/ffunP=> i. have := (congr1 (fun f : {ffun _ -> _} => f (fintype.lift ord0 i)) H). by rewrite !ffunE liftK. pose f := fun (b : {ffun 'I_t.+1 -> bool}) (i : 'I_t.+1) => ('X + (i%:R)%:P : {poly F}) ^+ b i. pose g b : {poly %/ h}:= in_qpoly h (\prod_(i < t.+1) f b i). have F3 b : b \in m -> size (\prod_(i < t.+1) f b i)%R <= #|M|. have vE i : #|((fun i0 : 'I_t.+1 => i0 != i) : pred _)| = t. set v := #|_|; rewrite -[t]/(t.+1.-1) -[t.+1]card_ord. rewrite -cardsT [in RHS](cardsD1 i) inE /=. by apply: eq_card => j; rewrite !inE andbT. move: t_gt0; rewrite leq_eqVlt => /orP[/eqP tE1 /mTrue1 [i /eqP iE]| t_gt]. rewrite (bigD1 i) //= {1}/f; rewrite iE expr0 mul1r. apply: leq_trans (size_prod_leq _ _) _ => /=. rewrite vE leq_subLR. rewrite (leq_ltn_trans _ (_ : (\sum_(j < t.+1 | j != i) 2) < _)) //. apply: leq_sum => j _; apply: F2. rewrite -ltnS; apply: leq_trans (ltn_ord j) _. by rewrite ltnS geq_minl. by rewrite sum_nat_const [#|_|]vE muln2 -addnn ltn_add2l -tE1. move=> bM; have [i [j [jDi biE bjE]]] := mTrue2 _ t_gt bM. rewrite (bigD1 i) //= {1}/f; rewrite biE expr0 mul1r. rewrite (bigD1 j) //= {1}/f; rewrite bjE expr0 mul1r. apply: leq_trans (size_prod_leq _ _) _ => /=. set v := #|_|. have vE1 : v = t.-1. rewrite -[t]/(t.+1.-1) -[t.+1]card_ord. rewrite -cardsT [in RHS](cardsD1 i) inE /=. rewrite [in RHS](cardsD1 j) !inE /= jDi /=. by apply: eq_card => l; rewrite !inE /= andbT andbC. rewrite vE1 leq_subLR. rewrite (leq_ltn_trans _ (_ : (\sum_(l < t.+1 | (l != i) && (l != j)) 2) < _)) //. apply: leq_sum => l _; apply: F2. rewrite -ltnS; apply: leq_trans (ltn_ord l) _. by rewrite ltnS geq_minl. rewrite sum_nat_const [#|_|]vE1 muln2 -addnn ltn_add2l. by rewrite prednK ?geq_minr // ltnW. have F4 b : b \in m -> is_ipoly k s (\prod_(i < t.+1) f b i). move=> bIm m1 Hm1. elim/big_rec: _ => [|i x _ xI]; first by apply: introspective1r. apply: introspecMr => //. rewrite /f; case: (b i); last by rewrite expr0; apply: introspective1r. rewrite expr1; case: (i : nat) (ltn_ord i) => [_|i1]. by rewrite addr0; apply: introspectiveX. rewrite ltnS => i1Lt. case: Hm1=> _; apply=> /=; apply: leq_trans i1Lt _. by rewrite geq_minl. suff /card_in_imset<- : {in m &, injective g}. rewrite subset_leqif_cards //; apply/subsetP => i /imsetP[/= b bIm ->]. by case: HQh => // /(_ (\prod_(i < t.+1) f b i) (F4 _ bIm)) /eqP[]. move=> m1 m2 m1I m2I /val_eqP/eqP/= H. have F5 b (x : 'I_ _) : b \in m -> (\prod_(i < t.+1) f b i).[-(x%:R)] == 0 = (b x). move=> bIm; rewrite horner_prod. apply/GRing.prodf_eq0/idP=> /= [[j _]|bxE]; last first. by exists x=> //; rewrite /f bxE expr1 !hornerE addrC subrr. rewrite /f horner_exp !hornerE; case: (boolP (b j)) => bjE; last first. by rewrite expr0 oner_eq0. rewrite expr1 addrC. rewrite {2}/is_true -{}bjE. wlog: x j / x <= j => [Hw|]. case: (leqP x j)=> [xLj|jLx]; first by apply: Hw. rewrite -oppr_eq0 opprB => xjE0. by apply/esym/Hw => //; apply: ltnW. rewrite leq_eqVlt => /orP[/val_eqP->//|xLhj]. rewrite -natrB 1?ltnW // -(dvdn_charf pC). rewrite gtnNdvd //; first by rewrite subn_gt0. apply: leq_ltn_trans (leq_subr _ _) _. apply: leq_trans (ltn_ord _) _. apply: leq_ltn_trans (geq_minl _ _) _. by case/andP: sB. suff : \prod_(i < t.+1) f m1 i = \prod_(i < t.+1) f m2 i. by move=> Hprod; apply/ffunP=> i; rewrite -F5 // Hprod F5. apply: Mk_rmodp_inj (F3 _ m1I) (F3 _ m2I) (F4 _ m1I) (F4 _ m2I) H => //. - by rewrite hQE. - by rewrite ltnW. - by rewrite hQE. by rewrite hQE. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound