proposition: Lemma sigma_goes_to_0 (eps : rat) : 0 < eps -> exists M : nat, forall n : nat, (M <= n)%N -> (sigma n < eps%:CR)%CR.
proof: Proof. move=> eps_pos. have [K2 [K3 [large [K2pos K3pos K2_maj hanson]]]] := hanson. pose C := 2%:Q * (K3 ^ 3) * Kdelta * Ka ^-1. have Cpos : 0 < C. by rewrite !(exprz_gt0, mulr_gt0) ?invr_gt0 ?lt_0_Ka ?lt_0_Kdelta. have heps : 0 < eps / C by apply: divr_gt0. have hr : 0 < K2 ^ 3 / 33%:Q < 1. by rewrite andbC -ltr_pdivlMr // invrK mul1r K2_maj divr_gt0 // exprn_gt0. have [N hN] := Gseqlt1 heps hr. pose_big_enough M. exists M => n hn. have aux : (sigma n < (2%:Q * (K3 * K2 ^ n) ^ 3 * Kdelta / Ka / 33%:Q ^ n)%:CR)%CR. rewrite /sigma -mulcrA -3!mulrA [in X in (_ < X)%CR]cst_crealM. apply: ltcr_mul2l; last exact/lt_creal_cst. have Dn_pos : 0 < (l n)%:Q. rewrite -[0]/(0%:Q) ltr_nat iter_lcmn_gt0; raise_big_enough. rewrite [in X in (_ < X)%CR]cst_crealM. apply: ltcr_pmul; first exact/lt_creal_cst/exprn_gt0. - apply/lt_creal_cst; apply: mulr_gt0; first exact: lt_0_Kdelta. apply: divr_gt0; last by apply: exprn_gt0; rewrite ltr0n. rewrite invr_gt0; exact: lt_0_Ka. - by apply/lt_creal_cst/ltrXn2r/hanson => //; raise_big_enough. - apply: lecr_lt_trans (NdeltaP _) _; first by raise_big_enough. apply/lt_creal_cst; rewrite ltr_pM2l; last exact: lt_0_Kdelta. apply: a_asympt; raise_big_enough. apply: lt_creal_trans aux _; apply/lt_creal_cst; set lhs := (X in (X < _)). have -> : lhs = C * (K2 ^ 3 / 33%:Q) ^ n. rewrite {}/lhs /C [in RHS]expfzMl exprzAC -[in RHS]expfV. set x := _ ^ n; set y := _ ^ n; field. by rewrite expfz_neq0 ?intr_eq0 // lt0r_neq0 ?lt_0_Ka. rewrite -ltr_pdivlMl -[X in _ < X]mulrC; last by rewrite mulrC; exact: Cpos. apply: hN; raise_big_enough. by close. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp(bigenough cauchyreals) extra_mathcomp extra_cauchyreals tactics shift bigopz arithmetics seq_defs c_props s_props z3seq_props a_props b_props b_over_a_props