matita/matita/lib/arithmetics/chebyshev/psi_bounds.ma

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department of the University of Bologna, Italy.
   5     ||I||
   6     ||T||
   7     ||A||
   8     \   /  This file is distributed under the terms of the
   9      \ /   GNU General Public License Version 2
  10       V_____________________________________________________________*)
  11
  12 include "arithmetics/chebyshev/chebyshev_psi.ma".
  13 include "arithmetics/chebyshev/factorization.ma".
  14
  15 theorem le_B_Psi: ∀n. B n ≤ Psi n.
  16 #n >eq_Psi_Psi' @le_pi #p #ltp #primep
  17 @le_pi #i #lti #_ >(exp_n_1 p) in ⊢ (??%); @le_exp
  18   [@prime_to_lt_O @primeb_true_to_prime //
  19   |@le_S_S_to_le @lt_mod_m_m @lt_O_S
  20   ]
  21 qed.
  22
  23 theorem le_B_Psi4: ∀n. O < n → 2 * B (4*n) ≤ Psi (4*n).
  24 #n #posn >eq_Psi_Psi'
  25 cut (2 < (S (4*n)))
  26   [@le_S_S >(times_n_1 2) in ⊢ (?%?); @le_times //] #H2
  27 cut (O<log 2 (4*n))
  28   [@lt_O_log [@le_S_S_to_le @H2 |@le_S_S_to_le @H2]] #Hlog
  29 >Bdef >(bigop_diff ??? timesAC ? 2 ? H2) [2:%]
  30 >Psidef >(bigop_diff ??? timesAC ? 2 ? H2) in ⊢ (??%); [2:%]
  31 <associative_times @le_times
  32   [>(bigop_diff ??? timesAC ? 0 ? Hlog) [2://]
  33    >(bigop_diff ??? timesAC ? 0 ? Hlog) in ⊢ (??%); [2:%]
  34    <associative_times >timesACdef @le_times
  35     [<exp_n_1 cut (4=2*2) [//] #H4 >H4 >associative_times
  36      >commutative_times in ⊢ (?(??(??(?(?%?)?)))?);
  37      >div_times [2://] >divides_to_mod_O
  38       [@le_n |%{n} // |@lt_O_S]
  39     |@le_pi #i #lti #H >(exp_n_1 2) in ⊢ (??%);
  40      @le_exp [@lt_O_S |@le_S_S_to_le @lt_mod_m_m @lt_O_S]
  41     ]
  42   |@le_pi #p #ltp #Hp @le_pi #i #lti #H
  43    >(exp_n_1 p) in ⊢ (??%); @le_exp
  44     [@prime_to_lt_O @primeb_true_to_prime @(andb_true_r ?? Hp)
  45     |@le_S_S_to_le @lt_mod_m_m @lt_O_S
  46     ]
  47   ]
  48 qed.
  49
  50 let rec bool_to_nat b ≝
  51   match b with [true ⇒ 1 | false ⇒ 0].
  52
  53 theorem eq_Psi_2_n: ∀n.O < n →
  54 Psi(2*n) =
  55  ∏_{p <S (2*n) | primeb p}
  56   (∏_{i <log p (2*n)} (exp p (bool_to_nat (leb (S n) (exp p (S i)))))) *Psi n.
  57 #n #posn >eq_Psi_Psi' > eq_Psi_Psi'
  58 cut (
  59  ∏_{p < S n | primeb p} (∏_{i <log p n} p)
  60  = ∏_{p < S (2*n) | primeb p}
  61      (∏_{i <log p (2*n)} (p\sup(bool_to_nat (¬ (leb (S n) (exp p (S i))))))))
  62   [2: #Hcut >Psidef in ⊢ (???%); >Hcut
  63    <times_pi >Psidef @same_bigop
  64     [//
  65     |#p #lt1p #primep <times_pi @same_bigop
  66       [//
  67       |#i #lt1i #_ cases (true_or_false (leb (S n) (exp p (S i)))) #Hc >Hc
  68         [normalize <times_n_1 >plus_n_O //
  69         |normalize <plus_n_O <plus_n_O //
  70         ]
  71       ]
  72     ]
  73   |@(trans_eq ??
  74     (∏_{p < S n | primeb p}
  75       (∏_{i < log p n} (p \sup(bool_to_nat (¬leb (S n) (exp p (S i))))))))
  76     [@same_bigop
  77       [//
  78       |#p #lt1p #primep @same_bigop
  79         [//
  80         |#i #lti#_ >lt_to_leb_false
  81           [normalize @plus_n_O
  82           |@le_S_S @(transitive_le ? (exp p (log p n)))
  83             [@le_exp [@prime_to_lt_O @primeb_true_to_prime //|//]
  84             |@le_exp_log //
  85             ]
  86           ]
  87         ]
  88       ]
  89     |@(trans_eq ??
  90       (∏_{p < S (2*n) | primeb p}
  91        (∏_{i <log p n} (p \sup(bool_to_nat (¬leb (S n) (p \sup(S i))))))))
  92       [@(pad_bigop_nil … timesA)
  93         [@le_S_S //|#i #lti #upi %2 >lt_to_log_O //]
  94       |@same_bigop
  95         [//
  96         |#p #ltp #primep @(pad_bigop_nil … timesA)
  97           [@le_log
  98             [@prime_to_lt_SO @primeb_true_to_prime //|//]
  99           |#i #lei #iup %2 >le_to_leb_true
 100             [%
 101             |@(lt_to_le_to_lt ? (exp p (S (log p n))))
 102               [@lt_exp_log @prime_to_lt_SO @primeb_true_to_prime //
 103               |@le_exp
 104                 [@prime_to_lt_O @primeb_true_to_prime //
 105                 |@le_S_S //
 106                 ]
 107               ]
 108             ]
 109           ]
 110         ]
 111       ]
 112     ]
 113   ]
 114 qed.
 115
 116 theorem le_Psi_BPsi1: ∀n. O < n →
 117   Psi(2*n) ≤ B(2*n)*Psi n.
 118 #n #posn >(eq_Psi_2_n … posn) @le_times [2:@le_n]
 119 >Bdef @le_pi #p #ltp #primep @le_pi #i #lti #_ @le_exp
 120   [@prime_to_lt_O @primeb_true_to_prime //
 121   |cases (true_or_false (leb (S n) (exp p (S i)))) #Hc >Hc
 122     [whd in ⊢ (?%?);
 123      cut (2*n/p\sup(S i) = 1) [2: #Hcut >Hcut @le_n]
 124      @(div_mod_spec_to_eq (2*n) (exp p (S i))
 125        ? (mod (2*n) (exp p (S i))) ? (minus (2*n) (exp p (S i))) )
 126       [@div_mod_spec_div_mod @lt_O_exp @prime_to_lt_O @primeb_true_to_prime //
 127       |cut (p\sup(S i)≤2*n)
 128         [@(transitive_le ? (exp p (log p (2*n))))
 129           [@le_exp [@prime_to_lt_O @primeb_true_to_prime // | //]
 130           |@le_exp_log >(times_n_O O) in ⊢ (?%?); @lt_times //
 131           ]
 132         ] #Hcut
 133        @div_mod_spec_intro
 134         [@lt_plus_to_minus
 135           [// |normalize in ⊢ (? % ?); < plus_n_O @lt_plus @leb_true_to_le //]
 136         |>commutative_plus >commutative_times in ⊢ (???(??%));
 137          < times_n_1 @plus_minus_m_m //
 138         ]
 139       ]
 140     |@le_O_n
 141     ]
 142   ]
 143 qed.
 144
 145 theorem le_Psi_BPsi: ∀n. Psi(2*n) \le B(2*n)*Psi n.
 146 #n cases n [@le_n |#m @le_Psi_BPsi1 @lt_O_S]
 147 qed.
 148
 149 theorem le_Psi_exp: ∀n. Psi(2*n) ≤ (exp 2 (pred (2*n)))*Psi n.
 150 #n @(transitive_le ? (B(2*n)*Psi n))
 151   [@le_Psi_BPsi |@le_times [@le_B_exp |//]]
 152 qed.
 153
 154 theorem lt_4_to_le_Psi_exp: ∀n. 4 < n →
 155   Psi(2*n) ≤ exp 2 ((2*n)-2)*Psi n.
 156 #n #lt4n @(transitive_le ? (B(2*n)*Psi n))
 157   [@le_Psi_BPsi|@le_times [@(lt_4_to_le_B_exp … lt4n) |@le_n]]
 158 qed.
 159
 160 (* two technical lemmas *)
 161 lemma times_2_pred: ∀n. 2*(pred n) \le pred (2*n).
 162 #n cases n
 163   [@le_n|#m @monotonic_le_plus_r @le_n_Sn]
 164 qed.
 165
 166 lemma le_S_times_2: ∀n. O < n → S n ≤ 2*n.
 167 #n #posn elim posn
 168   [@le_n
 169   |#m #posm #Hind
 170    cut (2*(S m) = S(S(2*m))) [normalize <plus_n_Sm //] #Hcut >Hcut
 171    @le_S_S @(transitive_le … Hind) @le_n_Sn
 172   ]
 173 qed.
 174
 175 theorem le_Psi_exp1: ∀n.
 176   Psi(exp 2 n) ≤ exp 2 ((2*(exp 2 n)-(S(S n)))).
 177 #n elim n
 178   [@le_n
 179   |#n1 #Hind whd in ⊢ (?(?%)?); >commutative_times
 180    @(transitive_le ??? (le_Psi_exp ?))
 181    @(transitive_le ? (2\sup(pred (2*2^n1))*2^(2*2^n1-(S(S n1)))))
 182     [@monotonic_le_times_r //
 183     |<exp_plus_times @(le_exp … (lt_O_S ?))
 184      cut (S(S n1) ≤ 2*(exp 2 n1))
 185       [elim n1
 186         [@le_n
 187         |#n2 >commutative_times in ⊢ (%→?); #Hind1 @(transitive_le ? (2*(S(S n2))))
 188           [@le_S_times_2 @lt_O_S |@monotonic_le_times_r //]
 189         ]
 190       ] #Hcut
 191      @le_S_S_to_le cut(∀a,b. S a + b = S (a+b)) [//] #Hplus <Hplus >S_pred
 192       [>eq_minus_S_pred in ⊢ (??%); >S_pred
 193         [>plus_minus_associative
 194           [@monotonic_le_minus_l
 195            cut (∀a. 2*a = a + a) [//] #times2 <times2
 196            @monotonic_le_times_r >commutative_times @le_n
 197           |@Hcut
 198           ]
 199         |@lt_plus_to_minus_r whd in ⊢ (?%?);
 200          @(lt_to_le_to_lt ? (2*(S(S n1))))
 201           [>(times_n_1 (S(S n1))) in ⊢ (?%?); >commutative_times
 202            @monotonic_lt_times_l [@lt_O_S |@le_n]
 203           |@monotonic_le_times_r whd in ⊢ (??%); //
 204           ]
 205         ]
 206       |whd >(times_n_1 1) in ⊢ (?%?); @le_times
 207         [@le_n_Sn |@lt_O_exp @lt_O_S]
 208       ]
 209     ]
 210   ]
 211 qed.
 212
 213 theorem monotonic_Psi: monotonic nat le Psi.
 214 #n #m #lenm elim lenm
 215   [@le_n
 216   |#n1 #len #Hind @(transitive_le … Hind)
 217    cut (∏_{p < S n1 | primeb p}(p^(log p n1))
 218           ≤∏_{p < S n1 | primeb p}(p^(log p (S n1))))
 219     [@le_pi #p #ltp #primep @le_exp
 220       [@prime_to_lt_O @primeb_true_to_prime //
 221       |@le_log [@prime_to_lt_SO @primeb_true_to_prime // | //]
 222       ]
 223     ] #Hcut
 224    >psi_def in ⊢ (??%); cases (true_or_false (primeb (S n1))) #Hc
 225     [>bigop_Strue in ⊢ (??%); [2://]
 226      >(times_n_1 (Psi n1)) >commutative_times @le_times
 227       [@lt_O_exp @lt_O_S |@Hcut]
 228     |>bigop_Sfalse in ⊢ (??%); //
 229     ]
 230   ]
 231 qed.
 232
 233 (* example *)
 234 example Psi_1: Psi 1 = 1. // qed.
 235
 236 example Psi_2: Psi 2 = 2. // qed.
 237
 238 example Psi_3: Psi 3 = 6. // qed.
 239
 240 example Psi_4: Psi 4 = 12. // qed.
 241
 242 theorem le_Psi_exp4: ∀n. 1 < n →
 243   Psi(n) ≤ (pred n)*exp 2 ((2 * n) -3).
 244 #n @(nat_elim1 n)
 245 #m #Hind cases (even_or_odd m)
 246 #a * #Hm >Hm #Hlt
 247   [cut (0<a)
 248     [cases a in Hlt;
 249       [whd in ⊢ (??%→?); #lt10 @False_ind @(absurd ? lt10 (not_le_Sn_O 1))
 250     |#b #_ //]
 251     ] #Hcut
 252    cases (le_to_or_lt_eq … Hcut) #Ha
 253     [@(transitive_le ? (exp 2 (pred(2*a))*Psi a))
 254       [@le_Psi_exp
 255       |@(transitive_le ? (2\sup(pred(2*a))*((pred a)*2\sup((2*a)-3))))
 256         [@monotonic_le_times_r @(Hind ?? Ha)
 257          >Hm >(times_n_1 a) in ⊢ (?%?); >commutative_times
 258          @monotonic_lt_times_l [@lt_to_le // |@le_n]
 259         |<Hm <associative_times >commutative_times in ⊢ (?(?%?)?);
 260          >associative_times; @le_times
 261           [>Hm cases a[@le_n|#b normalize @le_plus_n_r]
 262           |<exp_plus_times @le_exp
 263             [@lt_O_S
 264             |@(transitive_le ? (m+(m-3)))
 265               [@monotonic_le_plus_l //
 266               |normalize <plus_n_O >plus_minus_associative
 267                 [@le_n
 268                 |>Hm @(transitive_le ? (2*2) ? (le_n_Sn 3))
 269                  @monotonic_le_times_r //
 270                 ]
 271               ]
 272             ]
 273           ]
 274         ]
 275       ]
 276     |<Ha normalize @le_n
 277     ]
 278   |cases (le_to_or_lt_eq O a (le_O_n ?)) #Ha
 279     [@(transitive_le ? (Psi (2*(S a))))
 280       [@monotonic_Psi >Hm normalize <plus_n_Sm @le_n_Sn
 281       |@(transitive_le … (le_Psi_exp ?) )
 282        @(transitive_le ? ((2\sup(pred (2*S a)))*(a*(exp 2 ((2*(S a))-3)))))
 283         [@monotonic_le_times_r @Hind
 284           [>Hm @le_S_S >(times_n_1 a) in ⊢ (?%?); >commutative_times
 285            @monotonic_lt_times_l //
 286           |@le_S_S //
 287           ]
 288         |cut (pred (S (2*a)) = 2*a) [//] #Spred >Spred
 289          cut (pred (2*(S a)) = S (2 * a)) [normalize //] #Spred1 >Spred1
 290          cut (2*(S a) = S(S(2*a))) [normalize <plus_n_Sm //] #times2
 291          cut (exp 2 (2*S a -3) = 2*(exp 2 (S(2*a) -3)))
 292           [>(commutative_times 2) in ⊢ (???%); >times2 >minus_Sn_m [%]
 293            @le_S_S >(times_n_1 2) in ⊢ (?%?); @monotonic_le_times_r @Ha
 294           ] #Hcut >Hcut
 295          <associative_times in ⊢ (? (? ? %) ?); <associative_times
 296          >commutative_times in ⊢ (? (? % ?) ?);
 297          >commutative_times in ⊢ (? (? (? % ?) ?) ?);
 298          >associative_times @monotonic_le_times_r
 299          <exp_plus_times @(le_exp … (lt_O_S ?))
 300          >plus_minus_associative
 301           [normalize >(plus_n_O (a+(a+0))) in ⊢ (?(?(??%)?)?); @le_n
 302           |@le_S_S >(times_n_1 2) in ⊢ (?%?); @monotonic_le_times_r @Ha
 303           ]
 304         ]
 305       ]
 306     |@False_ind <Ha in Hlt; normalize #Hfalse @(absurd ? Hfalse) //
 307     ]
 308   ]
 309 qed.
 310
 311 theorem le_n_8_to_le_Psi_exp: ∀n. n ≤ 8 →
 312   Psi(n) ≤ exp 2 ((2 * n) -3).
 313 #n cases n
 314   [#_ @le_n
 315   |#n1 cases n1
 316     [#_ @le_n
 317     |#n2 cases n2
 318       [#_ @le_n
 319       |#n3 cases n3
 320         [#_ @leb_true_to_le //
 321         |#n4 cases n4
 322           [#_ @leb_true_to_le //
 323           |#n5 cases n5
 324             [#_ @leb_true_to_le //
 325             |#n6 cases n6
 326               [#_ @leb_true_to_le //
 327               |#n7 cases n7
 328                 [#_ @leb_true_to_le //
 329                 |#n8 cases n8
 330                   [#_ @leb_true_to_le //
 331                   |#n9 #H @False_ind @(absurd ?? (lt_to_not_le ?? H))
 332                    @leb_true_to_le //
 333                   ]
 334                 ]
 335               ]
 336             ]
 337           ]
 338         ]
 339       ]
 340     ]
 341   ]
 342 qed.
 343
 344 theorem le_Psi_exp5: ∀n. Psi(n) ≤ exp 2 ((2 * n) -3).
 345 #n @(nat_elim1 n) #m #Hind
 346 cases (decidable_le 9 m)
 347   [#lem cases (even_or_odd m) #a * #Hm
 348     [>Hm in ⊢ (?%?); @(transitive_le … (le_Psi_exp ?))
 349      @(transitive_le ? (2\sup(pred(2*a))*(2\sup((2*a)-3))))
 350       [@monotonic_le_times_r @Hind >Hm >(times_n_1 a) in ⊢ (?%?);
 351        >commutative_times @(monotonic_lt_times_l  … (le_n ?))
 352        @(transitive_lt ? 3)
 353         [@lt_O_S |@(le_times_to_le 2) [@lt_O_S |<Hm @lt_to_le @lem]]
 354       |<Hm <exp_plus_times @(le_exp … (lt_O_S ?))
 355        whd in match (times 2 m); >commutative_times <times_n_1
 356        <plus_minus_associative
 357         [@monotonic_le_plus_l @le_pred_n
 358         |@(transitive_le … lem) @leb_true_to_le //
 359         ]
 360       ]
 361     |@(transitive_le ? (Psi (2*(S a))))
 362       [@monotonic_Psi >Hm normalize <plus_n_Sm @le_n_Sn
 363       |@(transitive_le ? ((exp 2 ((2*(S a))-2))*Psi (S a)))
 364         [@lt_4_to_le_Psi_exp @le_S_S
 365          @(le_times_to_le 2)[@le_n_Sn|@le_S_S_to_le <Hm @lem]
 366         |@(transitive_le ? ((2\sup((2*S a)-2))*(exp 2 ((2*(S a))-3))))
 367           [@monotonic_le_times_r @Hind >Hm @le_S_S
 368            >(times_n_1 a) in ⊢ (?%?);
 369            >commutative_times @(monotonic_lt_times_l  … (le_n ?))
 370            @(transitive_lt ? 3)
 371             [@lt_O_S |@(le_times_to_le 2) [@lt_O_S |@le_S_S_to_le <Hm @lem]]
 372           |cut (∀a. 2*(S a) = S(S(2*a))) [normalize #a <plus_n_Sm //] #times2
 373            >times2 <Hm <exp_plus_times @(le_exp … (lt_O_S ?))
 374            cases m
 375             [@le_n
 376             |#n1 cases n1
 377               [@le_n
 378               |#n2 normalize <minus_n_O <plus_n_O <plus_n_Sm
 379                normalize <minus_n_O <plus_n_Sm @le_n
 380               ]
 381             ]
 382           ]
 383         ]
 384       ]
 385     ]
 386   |#H @le_n_8_to_le_Psi_exp @le_S_S_to_le @not_le_to_lt //
 387   ]
 388 qed.
 389
 390 theorem le_exp_Psil:∀n. O < n → exp 2 n ≤ Psi (2 * n).
 391 #n #posn @(transitive_le ? ((exp 2 (2*n))/(2*n)))
 392   [@le_times_to_le_div
 393     [>(times_n_O O) in ⊢ (?%?); @lt_times [@lt_O_S|//]
 394     |normalize in ⊢ (??(??%)); < plus_n_O >exp_plus_times
 395      @le_times [2://] elim posn [//]
 396      #m #le1m #Hind whd in ⊢ (??%); >commutative_times in ⊢ (??%);
 397      @monotonic_le_times_r @(transitive_le … Hind)
 398      >(times_n_1 m) in ⊢ (?%?); >commutative_times
 399      @(monotonic_lt_times_l  … (le_n ?)) @le1m
 400     ]
 401   |@le_times_to_le_div2
 402     [>(times_n_O O) in ⊢ (?%?); @lt_times [@lt_O_S|//]
 403     |@(transitive_le ? ((B (2*n)*(2*n))))
 404       [<commutative_times in ⊢ (??%); @le_exp_B //
 405       |@le_times [@le_B_Psi|@le_n]
 406       ]
 407     ]
 408   ]
 409 qed.
 410
 411 theorem le_exp_Psi2:∀n. 1 < n → exp 2 (n / 2) \le Psi n.
 412 #n #lt1n @(transitive_le ? (Psi(n/2*2)))
 413   [>commutative_times @le_exp_Psil
 414    cases (le_to_or_lt_eq ? ? (le_O_n (n/2))) [//]
 415    #Heq @False_ind @(absurd ?? (lt_to_not_le ?? lt1n))
 416    >(div_mod n 2) <Heq whd in ⊢ (?%?);
 417    @le_S_S_to_le @(lt_mod_m_m n 2) @lt_O_S
 418   |@monotonic_Psi >(div_mod n 2) in ⊢ (??%); @le_plus_n_r
 419   ]
 420 qed.
 421
 422 theorem eq_sigma_pi_SO_n: ∀n.∑_{i < n} 1 = n.
 423 #n elim n //
 424 qed.
 425
 426 theorem lePsi_prim: ∀n.
 427   exp n (prim n) \le Psi n * ∏_{p < S n | primeb p} p.
 428 #n <(exp_sigma (S n) n primeb) <times_pi @le_pi
 429 #p #ltp #primep @lt_to_le @lt_exp_log
 430 @prime_to_lt_SO @primeb_true_to_prime //
 431 qed.
 432
 433 theorem le_prim_log : ∀n,b. 1 < b →
 434   log b (Psi n) ≤ prim n * (S (log b n)).
 435 #n #b #lt1b @(transitive_le … (log_exp1 …)) [@le_log // | //]
 436 qed.
 437
 438 (*********************** the inequalities ***********************)
 439 lemma exp_Sn: ∀b,n. exp b (S n) = b * (exp b n).
 440 normalize //
 441 qed.
 442
 443 theorem le_exp_priml: ∀n. O < n →
 444   exp 2 (2*n) ≤ exp (2*n) (S(prim (2*n))).
 445 #n #posn @(transitive_le ? (((2*n*(B (2*n))))))
 446   [@le_exp_B //
 447   |>exp_Sn @monotonic_le_times_r @(transitive_le ? (Psi (2*n)))
 448     [@le_B_Psi |@le_Psil]
 449   ]
 450 qed.
 451
 452 theorem le_exp_prim4l: ∀n. O < n →
 453   exp 2 (S(4*n)) ≤ exp (4*n) (S(prim (4*n))).
 454 #n #posn @(transitive_le ? (2*(4*n*(B (4*n)))))
 455   [>exp_Sn @monotonic_le_times_r
 456    cut (4*n = 2*(2*n)) [<associative_times //] #Hcut
 457    >Hcut @le_exp_B @lt_to_le whd >(times_n_1 2) in ⊢ (?%?);
 458    @monotonic_le_times_r //
 459   |>exp_Sn <associative_times >commutative_times in ⊢ (?(?%?)?);
 460    >associative_times @monotonic_le_times_r @(transitive_le ? (Psi (4*n)))
 461     [@le_B_Psi4 // |@le_Psil]
 462   ]
 463 qed.
 464
 465 theorem le_priml: ∀n. O < n →
 466   2*n ≤ (S (log 2 (2*n)))*S(prim (2*n)).
 467 #n #posn <(eq_log_exp 2 (2*n) ?) in ⊢ (?%?);
 468   [@(transitive_le ? ((log 2) (exp (2*n) (S(prim (2*n))))))
 469     [@le_log [@le_n |@le_exp_priml //]
 470     |>commutative_times in ⊢ (??%); @log_exp1 @le_n
 471     ]
 472   |@le_n
 473   ]
 474 qed.
 475
 476 theorem le_exp_primr: ∀n.
 477   exp n (prim n) ≤ exp 2 (2*(2*n-3)).
 478 #n @(transitive_le ? (exp (Psi n) 2))
 479   [>exp_Sn >exp_Sn whd in match (exp ? 0); <times_n_1 @lePsi_r2
 480   |>commutative_times <exp_exp_times @le_exp1 [@lt_O_S |@le_Psi_exp5]
 481   ]
 482 qed.
 483
 484 (* bounds *)
 485 theorem le_primr: ∀n. 1 < n → prim n \le 2*(2*n-3)/log 2 n.
 486 #n #lt1n @le_times_to_le_div
 487   [@lt_O_log //
 488   |@(transitive_le ? (log 2 (exp n (prim n))))
 489     [>commutative_times @log_exp2
 490       [@le_n |@lt_to_le //]
 491     |<(eq_log_exp 2 (2*(2*n-3))) in ⊢ (??%);
 492       [@le_log [@le_n |@le_exp_primr]
 493       |@le_n
 494       ]
 495     ]
 496   ]
 497 qed.
 498
 499 theorem le_priml1: ∀n. O < n →
 500   2*n/((log 2 n)+2) - 1 ≤ prim (2*n).
 501 #n #posn @le_plus_to_minus @le_times_to_le_div2
 502   [>commutative_plus @lt_O_S
 503   |>commutative_times in ⊢ (??%); <plus_n_Sm <plus_n_Sm in ⊢ (??(??%));
 504    <plus_n_O <commutative_plus <log_exp
 505     [@le_priml // | //| @le_n]
 506   ]
 507 qed.
 508
 509
 510
 511