proposition: Theorem t2 n k (Hank : (a k <= n < (a k.+1))%N) : (C n k.+1)%:Q%:C < exp_quo (10%:Q * n%:Q) (2*k.+1 - 1) 2 * (w%:C ^+ n.+1).
proof: Proof. have n_gt0 : (0 < n)%N. by case/andP: Hank => + _; apply/leq_trans/a_pos. have lt0nC : 0 < n%:Q%:C. by rewrite ltr0q ltr0n. have le0nR : 0 <= n%:Q. by rewrite ler0n. have H10_ge1 : 1 <= (10 * n)%N%:Q. by rewrite ler1n muln_gt0. set cn := (C _ _)%:Q%:C. set t10n_to := exp_quo (10 * n)%N%:Q. have wq_ge0 m : 0 <= w%:C ^+ m by rewrite exprn_ge0 // ler0q. suff step1 : cn < t10n_to (2 * k.+1 - 1)%N 2%N * w%:C ^+ n * w_seq k.+1. apply: lt_le_trans step1 _; rewrite -intrM exprSr mulrA. by apply/ler_wpM2l/w_upper_bounded/mulr_ge0/wq_ge0/exp_quo_ge0/ler0n. rewrite -mulrA; set tw := (X in _ < _ * X). have tw_pos : 0 <= tw by apply: mulr_ge0. have tenn_to_pos : 0 <= ((10 * n)%N%:Q ^+ k)%:C. by rewrite ler0q exprn_ge0 ?ler0n. suff step2 : cn < ((10 * n)%N%:Q ^+ k)%:C * t10n_to 1%N (a k.+1).-1 * tw. apply: lt_le_trans step2 _; rewrite exp_quo_r_nat. have ->: t10n_to (2 * k.+1 - 1)%N 2%N = t10n_to k 1%N * t10n_to 1%N 2%N. rewrite -exp_quo_plus ?ler0n //; apply: exp_quo_equiv; ring_lia. apply/ler_wpM2r/ler_wpM2l/exp_quo_lessn => //; last by rewrite !mul1n. by rewrite exp_quo_ge0 // ler0n. have ->: tw = w%:C ^+ n * n%:Q%:C * (w_seq k.+1 / n%:Q%:C). by rewrite mulrACA divff ?lt0r_neq0 // mulr1. have Helper0 : 0 < \prod_(i < k.+1) (a i)%:~R :> algC by rewrite prodr_gt0. have Helper1 : 0 < \prod_(i < k.+1) a' i by rewrite prodr_gt0. have step3 : w_seq k.+1 / n%:Q%:C >= (\prod_(i < k.+1) exp_quo (a i)%:Q (a i).-1 (a i))^-1. rewrite remark_t2_2 /w_seq invfM // invrK mulrC. rewrite ler_pdivrMr // -mulrA ler_pMr // mulrC ler_pdivlMr // mul1r. case/andP: Hank => _; rewrite a_rec addn1 ltnS big_mkord => H. by rewrite -prodMz 2!CratrE ler_nat. have ler0_10npow : 0 <= ((10 * n)%N%:Q ^+ k)%:C * t10n_to 1%N (a k.+1).-1. by rewrite mulr_ge0 ?exp_quo_ge0 ?ler0n. have t_ge0_0 : 0 <= \prod_(i < k.+1) exp_quo (a i)%:Q (a i).-1 (a i). by rewrite prodr_ge0 // => i _; rewrite exp_quo_ge0 // ler0n. have t_ge0_1 : 0 < exp_quo n%:Q (n * (a k.+1).-2) (a k.+1).-1. by rewrite exp_quo_gt0 // ltr0n. have t_ge0_2 : 0 <= (n ^ n)%N%:Q%:C. by rewrite ler0q ler0n. have t_ge0_3 : 0 <= w_seq k.+1 ^+ n. by rewrite exprn_ge0. have t_ge0_4 : 0 <= w_seq k.+1 ^+ n * ((n ^ n)%N%:Q%:C / exp_quo n%:Q (n * (a k.+1).-2) (a k.+1).-1). by apply/mulr_ge0/divr_ge0/exp_quo_ge0. suff step4 : cn < ((10 * n)%N%:Q ^+ k)%:C * t10n_to 1%N (a k.+1).-1 * ((w_seq k.+1) ^+ n * ((n ^ n)%N%:Q%:C / exp_quo n%:Q (n * (a k.+1).-2)%N ((a k.+1).-1)) / (\prod_(i < k.+1) exp_quo (a i)%:Q (a i).-1 (a i))). apply: lt_le_trans step4 _; apply/ler_wpM2l/ler_pM/step3/ler_pM => //. - by rewrite invr_ge0. - by rewrite divr_ge0 // ltW. - by apply/lerXn2r/w_upper_bounded; rewrite nnegrE // ler0q. - by rewrite ler_pdivrMr //; exact: remark_t2_1. congr (_ < _): (l10 (proj1 (andP Hank))). have -> : forall k1, exp_quo n%:Q (n * (a k1.+1).-2) (a k1.+1).-1 = \prod_(i < k1.+1) exp_quo n%:Q n (a i). elim=> [|k1 HIk1]; first by rewrite big_ord_recr big_ord0 /= mul1r muln1. rewrite big_ord_recr /= -HIk1 -exp_quo_plus //; apply: exp_quo_equiv => //=. - by rewrite muln_gt0 /= muln_gt0; apply/andP. - by rewrite muln_gt0 andbT muln_gt0; apply/andP. lia. rewrite /w_seq /t10n_to [in RHS]rmorphXn -subn1 -prod_is_exp_sum. rewrite -3!mulrA ![_ * (_%:C * _)]mulrCA; congr (_ * _). rewrite -prodrXl -!prodfV -!big_split /=; apply: eq_bigr => i _. rewrite -exprM mul1n [_^-1 / _ in RHS]mulrC [RHS]mulrA [RHS]mulrACA. rewrite -!exp_quoV ?divr_ge0 // -intrM -!exp_quoMl ?ler0n //. by rewrite invfM invrK [_ * (a i)%:~R]mulrC. Qed.
imports: ZArith mathcomp(all_ssreflect all_algebra all_field) extra_mathcomp tactics binomialz floor arithmetics posnum rat_of_Z hanson_elem_arith hanson_elem_analysis