proposition: Lemma w_seq_bound k (Hk : (2 <= k)%N) l : w_seq (k + l) <= w_seq k * exp_quo (a k)%:Q (2 ^ l.+1 - 2) (2 ^ l * a k).
proof: Proof. elim: l => [|l HIl]. by rewrite addn0 /= expn1 subnn /= /exp_quo expr0 mulr1. rewrite addnS /w_seq big_ord_recr /=. suff -> : exp_quo (a k)%:Q (2 ^ l.+2 - 2) (2 ^ l.+1 * a k) = exp_quo (a k)%:Q (2 ^ l.+1 - 2) (2 ^ l * a k) * (2 ^ l).-root (a' k). rewrite mulrA. apply: ler_pM; rewrite ?a'_bound // ?rootC_ge0 ?CratrE ?a_pos ?ler0n //. by rewrite prodr_ge0 // => i _ ; exact: a'_ge0. rewrite -prod_root ?CratrE ?expn_gt0 ?a_pos ?ler0n //. have -> : (2 ^ l * a k).-root (a k)%:R = exp_quo (a k)%:R 1 (2 ^ l * a k). by rewrite /exp_quo expr1 2!CratrE. rewrite -exp_quo_plus ?ler0n // ?muln_gt0 ?a_pos ?expn_gt0 //. rewrite [(2 ^ l.+1)%N]expnS -mulnA -mulnDl -subnA ?leq_pmulr ?expn_gt0 //=. set m := (2 ^ l * a k)%N. apply: exp_quo_equiv; last first. - by rewrite mulnACA [in RHS]mulnBl -expnS -expnSr. - by rewrite ler0n. - by rewrite !muln_gt0 ?a_pos ?expn_gt0. - by rewrite !muln_gt0 ?a_pos ?expn_gt0. 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