proposition: Theorem t3_nat : exists K : nat, (0 < K)%N /\ forall n : nat, (iter_lcmn n <= K * 3 ^ n)%N.
proof: Proof. pose cond n k := (a k <= n < a k.+1)%N. suff [K [Kpos KP]] : exists K : nat, (0 < K)%N /\ (forall n k, cond n k -> C n k.+1 <= K * 3 ^ n)%N. exists K; split => // -[| n]; first by rewrite expn0 muln1 iter_lcmn0. case: n => [| n]; first by rewrite iter_lcmn1 muln_gt0 Kpos. by apply/leq_trans/KP/n_between_a => //; apply/lcm_leq_Cnk. suff [K [Kpos KP]] : exists K : rat, (0 < K) /\ forall n k, cond n k -> (C n k.+1)%:R <= K * 3%:R ^ n. move: (floorQ K) (floorQ_ge0 (ltW Kpos)) (floorQ_spec K). case=> // k _ /andP [_ leKSn]; exists k.+1; split=> // n m {}/KP KP. suff: (C n m.+1)%:R <= (k%:Q + 1) * 3%:R ^ n. by rewrite -[_ + 1%:R]natrD -[_ ^ n]natrX -natrM ler_nat addn1. exact/le_trans/ler_wpM2r/ltW/leKSn/exprz_ge0. move mE: 10%N%:Q => m. have lt0m : 0 < m by rewrite -mE. have le0m : 0 <= m by exact: ltW. have lt1m : 1 < m by rewrite -mE. have le1m : 1 <= m by exact: ltW. move epsE: (w / 3%:R) => eps. have lt0eps1 : 0 < eps < 1. by rewrite -epsE ltr_pdivlMr // mul0r ltr_pdivrMr // mul1r w_lt3 w_gt0. pose u n k eps : rat := (m * n%:R) ^ k.+1 * eps ^ n.+1. suff hloglog : exists (K : rat), (0 < K) /\ (forall n k, cond n k -> u n k eps < K). have [K [lt0K KP]] := hloglog. exists (K * 3%:Q); split; first exact: mulr_gt0. move=> n k hcond. apply: le_trans (ltW (t2_rat hcond)) _; rewrite -mulrA -exprSz. rewrite -ler_pdivrMr; last exact: exprz_gt0. by rewrite -mulrA -expr_div_n mE epsE; apply/ltW/KP. have [lt0eps lteps1] := andP lt0eps1. pose loglog n := trunc_log 2 (trunc_log 2 n). pose v n : rat := (m * n%:R) ^ (loglog n).+3 * eps ^ n.+1. have le0v n : 0 <= v n. by rewrite /v pmulr_lge0 ?exprz_gt0 // exprz_ge0 // mulr_ge0 // ler0n. suff {u} [K [Kpos KP]] : exists K : rat, 0 < K /\ forall n, v n < K. exists K; split => // n k /better_k_bound hkn; apply: le_lt_trans (KP n). rewrite /u /v ler_pM2r; last exact: exprz_gt0. case: n hkn => [| n] hkn; first by rewrite mulr0 !exp0rz. apply: exp_incr_expp; first by apply: mulr_ege1=> //; rewrite ler1n. by rewrite ltnS -addn2. have h1 n : ((trunc_log 2 n).+1 <= 2 ^ (loglog n).+1)%N by exact: trunc_log_ltn. have {}h1 n : (n < 2 ^ 2 ^ (loglog n).+1)%N. have h : (n < 2 ^ (trunc_log 2 n).+1)%N by exact: trunc_log_ltn. have {}h : (2 ^ (trunc_log 2 n).+1 <= 2 ^ 2 ^ (loglog n).+1)%N by rewrite leq_exp2l. exact/leq_trans/h/trunc_log_ltn. have h2 n : (1 < n)%N -> (2 ^ 2 ^ loglog n <= n)%N. move=> lt1n. have h: (2 ^ trunc_log 2 n <= n)%N by apply/trunc_logP/ltnW. apply: leq_trans h; rewrite leq_exp2l; last by []. exact/trunc_logP/trunc_log_max. pose y n := (2 ^ 2 ^ (loglog n).+1)%N; pose x n := (2 ^ 2 ^ loglog n)%N. pose t n := (m * (y n)%:R) ^ (loglog n).+3 * eps ^ (x n).+1. have le0y n : 0 <= (y n)%:R :> rat by rewrite ler0n. suff {v le0v} [K [Kpos KP]] : exists K : rat, 0 < K /\ forall n, t n < K. pose KK := K + v 0%N + v 1%N. have ltKKK : K <= KK by rewrite /KK -addrA lerDl addr_ge0. have ltvKK n : (n <= 1)%N -> v n < KK. rewrite leq_eqVlt ltnS leqn0 /KK => /orP [] /eqP ->. - by rewrite cprD ltr_pwDl. - by rewrite addrAC cprD ltr_pwDl. exists KK; split => [|n]; first exact: lt_le_trans ltKKK. have [le1n | lt1n] := leqP n 1; first exact: ltvKK. apply/lt_le_trans/ltKKK/le_lt_trans/(KP n); rewrite /v /t. apply/ler_pM/exp_incr_expn => //. - exact/exprz_ge0/mulr_ge0/ler0n. - exact/exprz_ge0/ltW. - apply: lerXn2r; last first. + by apply: ler_wpM2l; rewrite // ler_nat ltnW // h1. + by rewrite rpredM // rpred_nat. + by rewrite rpredM // rpred_nat. - by rewrite ltnS h2. pose u n := (m * (x n)%:R) ^+ (2 * (loglog n).+3) * eps ^ x n. suff {t y le0y} [K [Kpos KP]] : exists K : rat, 0 < K /\ forall n, u n < K. exists K; split => // n. apply: le_lt_trans (KP n); rewrite {KP} /u /t. apply: ler_pM. - by apply: exprz_ge0; rewrite pmulr_rge0 // ler0n. - by apply: exprz_ge0; apply: ltW. - rewrite exprnP PoszM -exprz_exp; apply: lerXn2r. + by apply: rpredM => //; apply: rpred_nat. + by apply: rpredX; apply: rpredM => //; apply: rpred_nat. - rewrite expfzMl; apply: ler_pM=> //; first by apply: ler_eXnr. by rewrite -exprnP -natrX ler_nat /x /y expnS mulnC expnM. - rewrite -exprnP exprSr; apply: ler_piMr; last by apply: ltW. apply: exprn_ge0; exact: ltW. have {}h2 n : (1 < n)%N -> (x n <= n)%N by apply: h2. pose alpha n := (2 ^ 2 ^ n)%N. have le0alpha n : 0 <= (alpha n)%:R :> rat by rewrite ler0n. have lt_0_alpha n : (0 < alpha n)%N by rewrite /alpha expn_gt0. pose t n := (m * (alpha n)%:R) ^ (2 * n.+3)%:Z * eps ^ alpha n. have lt_0_t n : 0 < t n. by apply/mulr_gt0/exprz_gt0/lt0eps/exprz_gt0/mulr_gt0; rewrite ?ltr0n. have le_0_t n : 0 <= t n by exact: ltW. suff {x h1 h2 u} [K [Kpos KP]] : exists K : rat, 0 < K /\ forall n, t n < K. by exists K; split => // n; apply: le_lt_trans (KP (loglog n)). pose l n := (alpha n)%:R ^ 4 * eps ^ ((alpha n)%:Z ^ 2 - 2%:Z * (alpha n)%:Z). have alphaS n : (alpha n.+1 = alpha n ^ 2)%N. by rewrite /alpha expnS mulnC expnM. have le_0_alpham2 k : 0 <= (alpha k)%:Z - 2%:Z. rewrite /alpha; apply: (@le_trans _ _ ((2 ^ 2 ^ 0)%:Z - 2%:Z)) => //. by apply: lerB=> //; rewrite lez_nat leq_exp2l // leq_exp2l. have maj_t n : t n.+1 <= t n ^ 2 * l n. rewrite /t 2!expfzMl !exprz_exp expfzMl -2!mulrA -[_ * _ * l n]mulrA. apply: ler_pM; first exact: exprz_ge0. - apply: mulr_ge0; apply: exprz_ge0 => //; exact: ltW. - rewrite ler_weXn2l //; lia. rewrite /l mulrCA 2!mulrA -exprzD_nat -mulrA -expfzDr; last exact: lt0r_neq0. apply: ler_pM; first exact: exprz_ge0. - apply: exprz_ge0; exact: ltW. - rewrite alphaS natrX exprnP exprz_exp ler_weXn2l //; last lia. by rewrite ler1n expn_gt0. - by rewrite addrCA mulrC addrN addr0 alphaS. have le_0_l n : 0 <= l n. rewrite /l; apply: mulr_ge0; first by apply/exprz_ge0/ler0n. by apply/exprz_ge0/ltW. pose eps1 := rat_of_Z 5949909309448377. pose eps2 := rat_of_Z (6 * 10 ^ 15). have lt0eps2 : 0 < eps2 by exact: rat_of_Z_Zpos. have eps2_val : eps2 = 3%:R * rat_of_Z (2 * 10 ^ 15). by rewrite /eps2; ring. have epsF : eps = eps1 / eps2. by rewrite -epsE eps2_val invfM [RHS]mulrA [RHS]mulrAC w_val. have a3 : alpha 3%N = expn 2 8 by []. have lt_l3_1 : l 3%N <= 1. have -> : l 3%N = (2%:R * eps ^ (2%:R ^ 3 * ((alpha 3%N)%:R - 2%:R))) ^ (2 ^ 5)%N%:R. rewrite /l a3 [RHS]expfzMl -!natz !natrX !natz !exprnP !exprz_exp. by congr (_ ^ _ * eps ^ _). rewrite expr_le1 //; last exact/mulr_ge0/exprz_ge0/ltW. suff: 2%:R * eps ^ 90 <= 1. by apply: le_trans; rewrite ler_pM2l ?ler_piXz2l. rewrite epsF expfzMl -expfV mulrA ler_pdivrMr; last exact: exprz_gt0. rewrite mul1r -subr_ge0 -!rat_of_Z_pow mulr_natl -rmorphMn -rmorphB. vm_compute; exact: rat_of_Z_ZposW. rewrite [l]lock in lt_l3_1. have lt_t4_1 : t 4%N < 1. rewrite {l le_0_l lt_l3_1 maj_t loglog a3}. pose a4 := locked alpha 4%N. have lt0a4 : (0 < a4)%N by rewrite /a4 -lock. have -> : t 4%N = (m * a4%:R) ^ 14 * eps ^ alpha 4%N by rewrite /t /a4 -lock. suff [M hM hm]: exists2 M, (M * 14 <= alpha 4)%N & (m * a4%:R) * eps ^ M < 1. have {hm} : (m * a4%:R) ^14 * eps ^ (M * 14)%N < 1. rewrite PoszM -exprz_exp -expfzMl; apply: exprn_ilt1=> //. rewrite -mulrA pmulr_rge0 // pmulr_rge0 ?ltr0n //; apply: exprz_ge0; exact: ltW. apply: le_lt_trans. rewrite ler_pM2l; first by rewrite ler_piXz2l. by apply: exprz_gt0; rewrite pmulr_rgt0 // ltr0n. pose e := rat_of_Z 992 / rat_of_Z (10 ^ 3). have ltepse : eps < e. rewrite epsF ltr_pdivrMr // /e mulrAC ltr_pdivlMr; last exact: rat_of_Z_Zpos. have -> : eps2 = rat_of_Z (6 * 10 ^ 12) * rat_of_Z (10 ^ 3). by rewrite /eps2; ring. rewrite mulrA ltr_pM2r ?rat_of_Z_Zpos // -subr_gt0 /eps1 -rmorphM -rmorphB. exact: rat_of_Z_Zpos. suff [M le14M]: exists2 M, (M * 14 <= alpha 4)%N & (m * a4%:R) * (e ^ M) < 1. move=> hm; exists M => //; apply: le_lt_trans hm. rewrite ler_pM2l; last first. by rewrite pmulr_rgt0 // ltr0n. by apply: lerXn2r; apply: ltW; rewrite // divr_gt0 // rat_of_Z_Zpos. suff [M le14M hm]: exists2 M, (M * 14 <= alpha 4)%N & 0 < rat_of_Z (10 ^ 3) ^ M - (m * a4%:R) * rat_of_Z 992 ^ M. exists M => //. rewrite /e expfzMl -expfV mulrA ltr_pdivrMr; last by rewrite exprz_gt0 // rat_of_Z_Zpos. by rewrite mul1r -subr_gt0. exists 2000%N; first by rewrite /alpha -subn_eq0. rewrite -mE -!rat_of_Z_pow. rewrite pmulrn -intrM mulrzl -rmorphMz -rmorphB -mulrzl intrM. rewrite /a4 -lock /alpha. vm_compute; exact: rat_of_Z_Zpos. rewrite [t]lock in lt_t4_1. have lt_ln_1 (n : nat) : (3 <= n)%N -> l n <= 1. elim: n => [// | n ihn]. rewrite leq_eqVlt => /predU1P [<- | {}/ihn ihn]; first by rewrite [l]lock. suff h : l n.+1 <= (l n) ^ 2 by apply: le_trans h _; apply: mulr_ile1. rewrite /l expfzMl exprz_exp; apply: ler_pM. - exact/exprz_ge0/ler0n. - exact/exprz_ge0/ltW. - by rewrite alphaS natrX exprnP exprz_exp. rewrite exprz_exp ler_piXz2l //. - rewrite alphaS -subr_ge0; set a := alpha _; set x := (X in 0 <= X). have {x} -> : x = a%:Z ^+ 2 ^+ 2 - (2%:Z * a%:Z) ^+ 2 + 4%:Z * a%:Z. by rewrite /x; ring. rewrite subr_sqr; apply: addr_ge0; apply: mulr_ge0 => //. by rewrite expr2 -mulrBl; apply/mulr_ge0/isT/le_0_alpham2. - by rewrite -topredE /= -mulrBl; apply: mulr_ge0; first exact: le_0_alpham2. - by rewrite -topredE /= -mulrBl; apply: mulr_ge0; first exact: mulr_ge0. suff [K [lt0K [N Pn]]] : exists K : rat, 0 < K /\ exists N : nat, (forall n, (N < n)%N -> t n < K). pose KK := (K + \sum_(0 <= j < N.+1) t j). have le0sum : 0 <= \sum_(0 <= j < N.+1) t j by apply: sumr_ge0=> n _; exact: ltW. have lt0KK : 0 < KK by rewrite /KK; apply: ltr_pwDl. have ltKK : K <= KK by rewrite /KK lerDl. have KKmaj j : (j <= N)%N -> t j < KK. move=> lej4; rewrite /KK (bigD1_seq j) //=; last by rewrite mem_iota iota_uniq. - rewrite addrA addrAC cprD; apply: ltr_pwDl=> //; apply: sumr_ge0=> n _; exact: ltW. by rewrite mem_index_iota. exists KK; split => //; elim=> [| n ihn]; first exact: KKmaj. case: (ltnP n.+1 N.+1) => [lenN | ltNn]; first exact: KKmaj. by apply: lt_le_trans ltKK; apply: Pn. exists 1; split => //; exists 3%N; elim=> [| n ihn] //. rewrite leq_eqVlt => /predU1P [<- | lt3n]; first by rewrite [t]lock. have {}ihn := ihn lt3n. apply: le_lt_trans (maj_t _) _; apply: (@le_lt_trans _ _ (t n ^ 2)); last first. by apply: mulr_ilt1. rewrite ger_pMr; first by apply: lt_ln_1; rewrite ltnS in lt3n; apply: ltn_trans lt3n. exact: exprz_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