proposition: Lemma BCH_argument_lemma (w : 'rV[F0]_n) (m : nat) (mn : m < n) : w != 0 -> (forall i : 'I_n, n - m <= i < n -> (dft (rVexp a n) n (\row_i (gmorph w``_ i))) ``_ i = 0) -> m.+1 <= wH w.
proof: Proof. move=> w0 dftw0. have size_rVpoly : size (rVpoly (dft (rVexp a n) n (\row_i (gmorph w``_i)))) <= n - m. apply/leq_sizeP => j nmj. case/boolP : (j < n) => jn. by rewrite coef_poly jn insubT // dftw0 // nmj. by rewrite coef_poly (negbTE jn). have neq_0 : rVpoly (dft (rVexp a n) n (\row_i (gmorph w``_i))) != 0. apply: contra w0. move/eqP/(congr1 (@poly_rV _ n)). rewrite rVpolyK linear0. move/eqP. rewrite dft0 // => dft_0. apply/eqP/rowP => i. rewrite mxE. move/eqP/(congr1 (fun x : 'rV[F]_n => x ``_ i)) : dft_0. rewrite !mxE -(rmorph0 gmorph). by move/fmorph_inj. have root_rVpoly: forall rs, all (root (rVpoly (dft (rVexp a n) n (\row_i (gmorph w``_i))))) rs -> uniq rs -> size rs <= n - m -1. move=> rs all_rs uniq_rs. rewrite -ltnS. apply: (leq_trans (max_poly_roots neq_0 all_rs uniq_rs) _). by rewrite subnS subn0 prednK // subn_gt0. rewrite wH_rVpoly. suff : n - m > count (fun i : 'I_n => (rVpoly w)`_i == 0) (enum 'I_n). set f := fun i => _. move: (count_predC f (enum 'I_n)). rewrite size_enum_ord => Hn. rewrite -[in X in _ <= X - _ -> _]Hn -(ltn_add2r m) subnK; last first. by rewrite count_predC size_enum_ord ltnW. rewrite ltn_add2l. move/leq_trans; apply. by apply/eq_leq/eq_count. rewrite (_ : count _ _ = count (fun i : 'I_n => (rVpoly (dft (rVexp a n) n (\row_i gmorph w ``_ i))).[a ^- i] == 0) (enum 'I_n)); last first. apply eq_count => i. rewrite coef_poly (ltn_ord i) insubT // => ni. apply eq_trans with ((\row_i0 gmorph w ``_ i0) ``_ i == 0). rewrite mxE. apply/idP/idP => [/eqP H|]. rewrite (_ : Sub _ _ = i) in H; last by apply val_inj. by rewrite H rmorph0. rewrite [X in _ == X -> _](_ : 0 = gmorph 0); last by rewrite rmorph0. move/eqP/fmorph_inj. rewrite (_ : Sub _ _ = i) //; last by apply val_inj. by move/eqP. rewrite (tdcoor_of_fdcoor Hchar an i (\row_i gmorph w ``_ i)). rewrite mulf_eq0 invr_eq0 /=. rewrite -[RHS]orFb. congr (_ || _). apply/negbTE. by rewrite natf_neq0. rewrite ltnNge. apply/negP => abs. set rs := filter (fun i => root (rVpoly (dft (rVexp a n) n (\row_i0 gmorph w ``_ i0))) i) (map (fun i : 'I_n => a ^- i) (enum 'I_n)). have rs_uniq : uniq rs. rewrite filter_uniq //. rewrite map_inj_in_uniq ?enum_uniq // => i j _ _ bij. move/prim_root_not_uroot_on : an => an'. apply/eqP; rewrite -(exp_inj (primitive_uroot_neq0 an) an'); apply/eqP. move/(congr1 (fun x => x ^-1)) : bij. by rewrite -!exprVn invrK. have rs_root : all (root (rVpoly (dft (rVexp a n) n (\row_i gmorph w ``_ i)))) rs. apply/allP => x. by rewrite mem_filter => /andP[]. move: (root_rVpoly _ rs_root rs_uniq). apply/negP. rewrite -ltnNge subn1 prednK // ?subn_gt0 // /rs size_filter. apply: (leq_trans abs). apply eq_leq. rewrite [in RHS]count_map. by apply eq_count => i /=. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv zmodp) mathcomp(matrix mxalgebra mxpoly vector cyclic perm) ssr_ext ssralg_ext hamming