matita/matita/lib/arithmetics/chebyshev/chebyshev_B.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.ma".
  13
  14 definition B ≝ λn.
  15 ∏_{p < S n | primeb p}
  16   (∏_{i < log p n} (exp p (mod (n /(exp p (S i))) 2))).
  17
  18 lemma Bdef : ∀n.B n =
  19   ∏_{p < S n | primeb p}
  20   (∏_{i < log p n} (exp p (mod (n /(exp p (S i))) 2))).
  21 // qed-.
  22
  23 example B_SSSO: B 3 = 6. //
  24 qed.
  25
  26 example B_SSSSO: B 4 = 6. //
  27 qed.
  28
  29 example B_SSSSSO: B 5 = 30. //
  30 qed.
  31
  32 example B_SSSSSSO: B 6 = 20. //
  33 qed.
  34
  35 example B_SSSSSSSO: B 7 = 140. //
  36 qed.
  37
  38 example B_SSSSSSSSO: B 8 = 70. //
  39 qed.
  40
  41 theorem eq_fact_B:∀n. 1 < n →
  42   (2*n)! = exp (n!) 2 * B(2*n).
  43 #n #lt1n >fact_pi_p3 @eq_f2
  44   [@sym_eq >pi_p_primeb5 [@exp_fact_2|//] |// ]
  45 qed.
  46
  47 theorem le_B_A: ∀n. B n ≤ A n.
  48 #n >eq_A_A' @le_pi #p #ltp #primep
  49 @le_pi #i #lti #_ >(exp_n_1 p) in ⊢ (??%); @le_exp
  50   [@prime_to_lt_O @primeb_true_to_prime //
  51   |@le_S_S_to_le @lt_mod_m_m @lt_O_S
  52   ]
  53 qed.
  54
  55 theorem le_B_A4: ∀n. O < n → 2 * B (4*n) ≤ A (4*n).
  56 #n #posn >eq_A_A'
  57 cut (2 < (S (4*n)))
  58   [@le_S_S >(times_n_1 2) in ⊢ (?%?); @le_times //] #H2
  59 cut (O<log 2 (4*n))
  60   [@lt_O_log [@le_S_S_to_le @H2 |@le_S_S_to_le @H2]] #Hlog
  61 >Bdef >(bigop_diff ??? timesAC ? 2 ? H2) [2:%]
  62 >Adef >(bigop_diff ??? timesAC ? 2 ? H2) in ⊢ (??%); [2:%]
  63 <associative_times @le_times
  64   [>(bigop_diff ??? timesAC ? 0 ? Hlog) [2://]
  65    >(bigop_diff ??? timesAC ? 0 ? Hlog) in ⊢ (??%); [2:%]
  66    <associative_times >timesACdef @le_times
  67     [<exp_n_1 cut (4=2*2) [//] #H4 >H4 >associative_times
  68      >commutative_times in ⊢ (?(??(??(?(?%?)?)))?);
  69      >div_times [2://] >divides_to_mod_O
  70       [@le_n |%{n} // |@lt_O_S]
  71     |@le_pi #i #lti #H >(exp_n_1 2) in ⊢ (??%);
  72      @le_exp [@lt_O_S |@le_S_S_to_le @lt_mod_m_m @lt_O_S]
  73     ]
  74   |@le_pi #p #ltp #Hp @le_pi #i #lti #H
  75    >(exp_n_1 p) in ⊢ (??%); @le_exp
  76     [@prime_to_lt_O @primeb_true_to_prime @(andb_true_r ?? Hp)
  77     |@le_S_S_to_le @lt_mod_m_m @lt_O_S
  78     ]
  79   ]
  80 qed.
  81
  82 (* not usefull
  83 theorem le_fact_A:\forall n.S O < n \to
  84 fact (2*n) \le exp (fact n) 2 * A (2*n).
  85 intros.
  86 rewrite > eq_fact_B
  87   [apply le_times_r.
  88    apply le_B_A
  89   |assumption
  90   ]
  91 qed. *)
  92
  93 theorem lt_SO_to_le_B_exp: ∀n. 1 < n →
  94   B (2*n) ≤ exp 2 (pred (2*n)).
  95 #n #lt1n @(le_times_to_le (exp (fact n) 2))
  96   [@lt_O_exp //
  97   |<(eq_fact_B … lt1n) <commutative_times in ⊢ (??%);
  98    >exp_2 <associative_times @fact_to_exp
  99   ]
 100 qed.
 101
 102 theorem le_B_exp: ∀n.
 103   B (2*n) ≤ exp 2 (pred (2*n)).
 104 #n cases n
 105   [@le_n|#n1 cases n1 [@le_n |#n2 @lt_SO_to_le_B_exp @le_S_S @lt_O_S]]
 106 qed.
 107
 108 theorem lt_4_to_le_B_exp: ∀n.4 < n →
 109   B (2*n) \le exp 2 ((2*n)-2).
 110 #n #lt4n @(le_times_to_le (exp (fact n) 2))
 111   [@lt_O_exp //
 112   |<eq_fact_B
 113     [<commutative_times in ⊢ (??%); >exp_2 <associative_times
 114      @lt_4_to_fact //
 115     |@lt_to_le @lt_to_le @lt_to_le //
 116     ]
 117   ]
 118 qed.
 119
 120 theorem lt_1_to_le_exp_B: ∀n. 1 < n →
 121   exp 2 (2*n) ≤ 2 * n * B (2*n).
 122 #n #lt1n
 123 @(le_times_to_le (exp (fact n) 2))
 124   [@lt_O_exp @le_1_fact
 125   |<associative_times in ⊢ (??%); >commutative_times in ⊢ (??(?%?));
 126    >associative_times in ⊢ (??%); <(eq_fact_B … lt1n)
 127    <commutative_times; @exp_to_fact2 @lt_to_le //
 128   ]
 129 qed.
 130
 131 theorem le_exp_B: ∀n. O < n →
 132   exp 2 (2*n) ≤ 2 * n * B (2*n).
 133 #n #posn cases posn
 134   [@le_n |#m #lt1m @lt_1_to_le_exp_B @le_S_S // ]
 135 qed.
 136
 137 let rec bool_to_nat b ≝
 138   match b with [true ⇒ 1 | false ⇒ 0].
 139
 140 theorem eq_A_2_n: ∀n.O < n →
 141 A(2*n) =
 142  ∏_{p <S (2*n) | primeb p}
 143   (∏_{i <log p (2*n)} (exp p (bool_to_nat (leb (S n) (exp p (S i)))))) *A n.
 144 #n #posn >eq_A_A' > eq_A_A'
 145 cut (
 146  ∏_{p < S n | primeb p} (∏_{i <log p n} p)
 147  = ∏_{p < S (2*n) | primeb p}
 148      (∏_{i <log p (2*n)} (p\sup(bool_to_nat (¬ (leb (S n) (exp p (S i))))))))
 149   [2: #Hcut >Adef in ⊢ (???%); >Hcut
 150    <times_pi >Adef @same_bigop
 151     [//
 152     |#p #lt1p #primep <times_pi @same_bigop
 153       [//
 154       |#i #lt1i #_ cases (true_or_false (leb (S n) (exp p (S i)))) #Hc >Hc
 155         [normalize <times_n_1 >plus_n_O //
 156         |normalize <plus_n_O <plus_n_O //
 157         ]
 158       ]
 159     ]
 160   |@(trans_eq ??
 161     (∏_{p < S n | primeb p}
 162       (∏_{i < log p n} (p \sup(bool_to_nat (¬leb (S n) (exp p (S i))))))))
 163     [@same_bigop
 164       [//
 165       |#p #lt1p #primep @same_bigop
 166         [//
 167         |#i #lti#_ >lt_to_leb_false
 168           [normalize @plus_n_O
 169           |@le_S_S @(transitive_le ? (exp p (log p n)))
 170             [@le_exp [@prime_to_lt_O @primeb_true_to_prime //|//]
 171             |@le_exp_log //
 172             ]
 173           ]
 174         ]
 175       ]
 176     |@(trans_eq ??
 177       (∏_{p < S (2*n) | primeb p}
 178        (∏_{i <log p n} (p \sup(bool_to_nat (¬leb (S n) (p \sup(S i))))))))
 179       [@(pad_bigop_nil … timesA)
 180         [@le_S_S //|#i #lti #upi %2 >lt_to_log_O //]
 181       |@same_bigop
 182         [//
 183         |#p #ltp #primep @(pad_bigop_nil … timesA)
 184           [@le_log
 185             [@prime_to_lt_SO @primeb_true_to_prime //|//]
 186           |#i #lei #iup %2 >le_to_leb_true
 187             [%
 188             |@(lt_to_le_to_lt ? (exp p (S (log p n))))
 189               [@lt_exp_log @prime_to_lt_SO @primeb_true_to_prime //
 190               |@le_exp
 191                 [@prime_to_lt_O @primeb_true_to_prime //
 192                 |@le_S_S //
 193                 ]
 194               ]
 195             ]
 196           ]
 197         ]
 198       ]
 199     ]
 200   ]
 201 qed.
 202
 203 theorem le_A_BA1: ∀n. O < n →
 204   A(2*n) ≤ B(2*n)*A n.
 205 #n #posn >(eq_A_2_n … posn) @le_times [2:@le_n]
 206 >Bdef @le_pi #p #ltp #primep @le_pi #i #lti #_ @le_exp
 207   [@prime_to_lt_O @primeb_true_to_prime //
 208   |cases (true_or_false (leb (S n) (exp p (S i)))) #Hc >Hc
 209     [whd in ⊢ (?%?);
 210      cut (2*n/p\sup(S i) = 1) [2: #Hcut >Hcut @le_n]
 211      @(div_mod_spec_to_eq (2*n) (exp p (S i))
 212        ? (mod (2*n) (exp p (S i))) ? (minus (2*n) (exp p (S i))) )
 213       [@div_mod_spec_div_mod @lt_O_exp @prime_to_lt_O @primeb_true_to_prime //
 214       |cut (p\sup(S i)≤2*n)
 215         [@(transitive_le ? (exp p (log p (2*n))))
 216           [@le_exp [@prime_to_lt_O @primeb_true_to_prime // | //]
 217           |@le_exp_log >(times_n_O O) in ⊢ (?%?); @lt_times //
 218           ]
 219         ] #Hcut
 220        @div_mod_spec_intro
 221         [@lt_plus_to_minus
 222           [// |normalize in ⊢ (? % ?); < plus_n_O @lt_plus @leb_true_to_le //]
 223         |>commutative_plus >commutative_times in ⊢ (???(??%));
 224          < times_n_1 @plus_minus_m_m //
 225         ]
 226       ]
 227     |@le_O_n
 228     ]
 229   ]
 230 qed.
 231
 232 theorem le_A_BA: ∀n. A(2*n) \le B(2*n)*A n.
 233 #n cases n [@le_n |#m @le_A_BA1 @lt_O_S]
 234 qed.
 235
 236 theorem le_A_exp: ∀n. A(2*n) ≤ (exp 2 (pred (2*n)))*A n.
 237 #n @(transitive_le ? (B(2*n)*A n))
 238   [@le_A_BA |@le_times [@le_B_exp |//]]
 239 qed.
 240
 241 theorem lt_4_to_le_A_exp: ∀n. 4 < n →
 242   A(2*n) ≤ exp 2 ((2*n)-2)*A n.
 243 #n #lt4n @(transitive_le ? (B(2*n)*A n))
 244   [@le_A_BA|@le_times [@(lt_4_to_le_B_exp … lt4n) |@le_n]]
 245 qed.
 246
 247 (* two technical lemmas *)
 248 lemma times_2_pred: ∀n. 2*(pred n) \le pred (2*n).
 249 #n cases n
 250   [@le_n|#m @monotonic_le_plus_r @le_n_Sn]
 251 qed.
 252
 253 lemma le_S_times_2: ∀n. O < n → S n ≤ 2*n.
 254 #n #posn elim posn
 255   [@le_n
 256   |#m #posm #Hind
 257    cut (2*(S m) = S(S(2*m))) [normalize <plus_n_Sm //] #Hcut >Hcut
 258    @le_S_S @(transitive_le … Hind) @le_n_Sn
 259   ]
 260 qed.
 261
 262 theorem le_A_exp1: ∀n.
 263   A(exp 2 n) ≤ exp 2 ((2*(exp 2 n)-(S(S n)))).
 264 #n elim n
 265   [@le_n
 266   |#n1 #Hind whd in ⊢ (?(?%)?); >commutative_times
 267    @(transitive_le ??? (le_A_exp ?))
 268    @(transitive_le ? (2\sup(pred (2*2^n1))*2^(2*2^n1-(S(S n1)))))
 269     [@monotonic_le_times_r //
 270     |<exp_plus_times @(le_exp … (lt_O_S ?))
 271      cut (S(S n1) ≤ 2*(exp 2 n1))
 272       [elim n1
 273         [@le_n
 274         |#n2 >commutative_times in ⊢ (%→?); #Hind1 @(transitive_le ? (2*(S(S n2))))
 275           [@le_S_times_2 @lt_O_S |@monotonic_le_times_r //]
 276         ]
 277       ] #Hcut
 278      @le_S_S_to_le cut(∀a,b. S a + b = S (a+b)) [//] #Hplus <Hplus >S_pred
 279       [>eq_minus_S_pred in ⊢ (??%); >S_pred
 280         [>plus_minus_commutative
 281           [@monotonic_le_minus_l
 282            cut (∀a. 2*a = a + a) [//] #times2 <times2
 283            @monotonic_le_times_r >commutative_times @le_n
 284           |@Hcut
 285           ]
 286         |@lt_plus_to_minus_r whd in ⊢ (?%?);
 287          @(lt_to_le_to_lt ? (2*(S(S n1))))
 288           [>(times_n_1 (S(S n1))) in ⊢ (?%?); >commutative_times
 289            @monotonic_lt_times_l [@lt_O_S |@le_n]
 290           |@monotonic_le_times_r whd in ⊢ (??%); //
 291           ]
 292         ]
 293       |whd >(times_n_1 1) in ⊢ (?%?); @le_times
 294         [@le_n_Sn |@lt_O_exp @lt_O_S]
 295       ]
 296     ]
 297   ]
 298 qed.
 299
 300 theorem monotonic_A: monotonic nat le A.
 301 #n #m #lenm elim lenm
 302   [@le_n
 303   |#n1 #len #Hind @(transitive_le … Hind)
 304    cut (∏_{p < S n1 | primeb p}(p^(log p n1))
 305           ≤∏_{p < S n1 | primeb p}(p^(log p (S n1))))
 306     [@le_pi #p #ltp #primep @le_exp
 307       [@prime_to_lt_O @primeb_true_to_prime //
 308       |@le_log [@prime_to_lt_SO @primeb_true_to_prime // | //]
 309       ]
 310     ] #Hcut
 311    >psi_def in ⊢ (??%); cases (true_or_false (primeb (S n1))) #Hc
 312     [>bigop_Strue in ⊢ (??%); [2://]
 313      >(times_n_1 (A n1)) >commutative_times @le_times
 314       [@lt_O_exp @lt_O_S |@Hcut]
 315     |>bigop_Sfalse in ⊢ (??%); //
 316     ]
 317   ]
 318 qed.
 319
 320 (*
 321 theorem le_A_exp2: \forall n. O < n \to
 322 A(n) \le (exp (S(S O)) ((S(S O)) * (S(S O)) * n)).
 323 intros.
 324 apply (trans_le ? (A (exp (S(S O)) (S(log (S(S O)) n)))))
 325   [apply monotonic_A.
 326    apply lt_to_le.
 327    apply lt_exp_log.
 328    apply le_n
 329   |apply (trans_le ? ((exp (S(S O)) ((S(S O))*(exp (S(S O)) (S(log (S(S O)) n)))))))
 330     [apply le_A_exp1
 331     |apply le_exp
 332       [apply lt_O_S
 333       |rewrite > assoc_times.apply le_times_r.
 334        change with ((S(S O))*((S(S O))\sup(log (S(S O)) n))≤(S(S O))*n).
 335        apply le_times_r.
 336        apply le_exp_log.
 337        assumption
 338       ]
 339     ]
 340   ]
 341 qed.
 342 *)
 343
 344 (* example *)
 345 example A_1: A 1 = 1. // qed.
 346
 347 example A_2: A 2 = 2. // qed.
 348
 349 example A_3: A 3 = 6. // qed.
 350
 351 example A_4: A 4 = 12. // qed.
 352
 353 (*
 354 (* a better result *)
 355 theorem le_A_exp3: \forall n. S O < n \to
 356 A(n) \le exp (pred n) (2*(exp 2 (2 * n)).
 357 intro.
 358 apply (nat_elim1 n).
 359 intros.
 360 elim (or_eq_eq_S m).
 361 elim H2
 362   [elim (le_to_or_lt_eq (S O) a)
 363     [rewrite > H3 in ⊢ (? % ?).
 364      apply (trans_le ? ((exp (S(S O)) ((S(S O)*a)))*A a))
 365       [apply le_A_exp
 366       |apply (trans_le ? (((S(S O)))\sup((S(S O))*a)*
 367          ((pred a)\sup((S(S O)))*((S(S O)))\sup((S(S O))*a))))
 368         [apply le_times_r.
 369          apply H
 370           [rewrite > H3.
 371            rewrite > times_n_SO in ⊢ (? % ?).
 372            rewrite > sym_times.
 373            apply lt_times_l1
 374             [apply lt_to_le.assumption
 375             |apply le_n
 376             ]
 377           |assumption
 378           ]
 379         |rewrite > sym_times.
 380          rewrite > assoc_times.
 381          rewrite < exp_plus_times.
 382          apply (trans_le ?
 383           (pred a\sup((S(S O)))*(S(S O))\sup(S(S O))*(S(S O))\sup((S(S O))*m)))
 384           [rewrite > assoc_times.
 385            apply le_times_r.
 386            rewrite < exp_plus_times.
 387            apply le_exp
 388             [apply lt_O_S
 389             |rewrite < H3.
 390              simplify.
 391              rewrite < plus_n_O.
 392              apply le_S.apply le_S.
 393              apply le_n
 394             ]
 395           |apply le_times_l.
 396            rewrite > times_exp.
 397            apply monotonic_exp1.
 398            rewrite > H3.
 399            rewrite > sym_times.
 400            cases a
 401             [apply le_n
 402             |simplify.
 403              rewrite < plus_n_Sm.
 404              apply le_S.
 405              apply le_n
 406             ]
 407           ]
 408         ]
 409       ]
 410     |rewrite < H4 in H3.
 411      simplify in H3.
 412      rewrite > H3.
 413      simplify.
 414      apply le_S_S.apply le_S_S.apply le_O_n
 415     |apply not_lt_to_le.intro.
 416      apply (lt_to_not_le ? ? H1).
 417      rewrite > H3.
 418      apply (le_n_O_elim a)
 419       [apply le_S_S_to_le.assumption
 420       |apply le_O_n
 421       ]
 422     ]
 423   |elim (le_to_or_lt_eq O a (le_O_n ?))
 424     [apply (trans_le ? (A ((S(S O))*(S a))))
 425       [apply monotonic_A.
 426        rewrite > H3.
 427        rewrite > times_SSO.
 428        apply le_n_Sn
 429       |apply (trans_le ? ((exp (S(S O)) ((S(S O)*(S a))))*A (S a)))
 430         [apply le_A_exp
 431         |apply (trans_le ? (((S(S O)))\sup((S(S O))*S a)*
 432            (a\sup((S(S O)))*((S(S O)))\sup((S(S O))*(S a)))))
 433           [apply le_times_r.
 434            apply H
 435             [rewrite > H3.
 436              apply le_S_S.
 437              simplify.
 438              rewrite > plus_n_SO.
 439              apply le_plus_r.
 440              rewrite < plus_n_O.
 441              assumption
 442             |apply le_S_S.assumption
 443             ]
 444           |rewrite > sym_times.
 445            rewrite > assoc_times.
 446            rewrite < exp_plus_times.
 447            apply (trans_le ?
 448             (a\sup((S(S O)))*(S(S O))\sup(S(S O))*(S(S O))\sup((S(S O))*m)))
 449             [rewrite > assoc_times.
 450              apply le_times_r.
 451              rewrite < exp_plus_times.
 452              apply le_exp
 453               [apply lt_O_S
 454               |rewrite > times_SSO.
 455                rewrite < H3.
 456                simplify.
 457                rewrite < plus_n_Sm.
 458                rewrite < plus_n_O.
 459                apply le_n
 460               ]
 461             |apply le_times_l.
 462              rewrite > times_exp.
 463              apply monotonic_exp1.
 464              rewrite > H3.
 465              rewrite > sym_times.
 466              apply le_n
 467             ]
 468           ]
 469         ]
 470       ]
 471     |rewrite < H4 in H3.simplify in H3.
 472      apply False_ind.
 473      apply (lt_to_not_le ? ? H1).
 474      rewrite > H3.
 475      apply le_
 476     ]
 477   ]
 478 qed.
 479 *)
 480
 481 theorem le_A_exp4: ∀n. 1 < n →
 482   A(n) ≤ (pred n)*exp 2 ((2 * n) -3).
 483 #n @(nat_elim1 n)
 484 #m #Hind cases (even_or_odd m)
 485 #a * #Hm >Hm #Hlt
 486   [cut (0<a)
 487     [cases a in Hlt;
 488       [whd in ⊢ (??%→?); #lt10 @False_ind @(absurd ? lt10 (not_le_Sn_O 1))
 489     |#b #_ //]
 490     ] #Hcut
 491    cases (le_to_or_lt_eq … Hcut) #Ha
 492     [@(transitive_le ? (exp 2 (pred(2*a))*A a))
 493       [@le_A_exp
 494       |@(transitive_le ? (2\sup(pred(2*a))*((pred a)*2\sup((2*a)-3))))
 495         [@monotonic_le_times_r @(Hind ?? Ha)
 496          >Hm >(times_n_1 a) in ⊢ (?%?); >commutative_times
 497          @monotonic_lt_times_l [@lt_to_le // |@le_n]
 498         |<Hm <associative_times >commutative_times in ⊢ (?(?%?)?);
 499          >associative_times; @le_times
 500           [>Hm cases a[@le_n|#b normalize @le_plus_n_r]
 501           |<exp_plus_times @le_exp
 502             [@lt_O_S
 503             |@(transitive_le ? (m+(m-3)))
 504               [@monotonic_le_plus_l //
 505               |normalize <plus_n_O >plus_minus_commutative
 506                 [@le_n
 507                 |>Hm @(transitive_le ? (2*2) ? (le_n_Sn 3))
 508                  @monotonic_le_times_r //
 509                 ]
 510               ]
 511             ]
 512           ]
 513         ]
 514       ]
 515     |<Ha normalize @le_n
 516     ]
 517   |cases (le_to_or_lt_eq O a (le_O_n ?)) #Ha
 518     [@(transitive_le ? (A (2*(S a))))
 519       [@monotonic_A >Hm normalize <plus_n_Sm @le_n_Sn
 520       |@(transitive_le … (le_A_exp ?) )
 521        @(transitive_le ? ((2\sup(pred (2*S a)))*(a*(exp 2 ((2*(S a))-3)))))
 522         [@monotonic_le_times_r @Hind
 523           [>Hm @le_S_S >(times_n_1 a) in ⊢ (?%?); >commutative_times
 524            @monotonic_lt_times_l //
 525           |@le_S_S //
 526           ]
 527         |cut (pred (S (2*a)) = 2*a) [//] #Spred >Spred
 528          cut (pred (2*(S a)) = S (2 * a)) [normalize //] #Spred1 >Spred1
 529          cut (2*(S a) = S(S(2*a))) [normalize <plus_n_Sm //] #times2
 530          cut (exp 2 (2*S a -3) = 2*(exp 2 (S(2*a) -3)))
 531           [>(commutative_times 2) in ⊢ (???%); >times2 >minus_Sn_m [%]
 532            @le_S_S >(times_n_1 2) in ⊢ (?%?); @monotonic_le_times_r @Ha
 533           ] #Hcut >Hcut
 534          <associative_times in ⊢ (? (? ? %) ?); <associative_times
 535          >commutative_times in ⊢ (? (? % ?) ?);
 536          >commutative_times in ⊢ (? (? (? % ?) ?) ?);
 537          >associative_times @monotonic_le_times_r
 538          <exp_plus_times @(le_exp … (lt_O_S ?))
 539          >plus_minus_commutative
 540           [normalize >(plus_n_O (a+(a+0))) in ⊢ (?(?(??%)?)?); @le_n
 541           |@le_S_S >(times_n_1 2) in ⊢ (?%?); @monotonic_le_times_r @Ha
 542           ]
 543         ]
 544       ]
 545     |@False_ind <Ha in Hlt; normalize #Hfalse @(absurd ? Hfalse) //
 546     ]
 547   ]
 548 qed.
 549
 550 theorem le_n_8_to_le_A_exp: ∀n. n ≤ 8 →
 551   A(n) ≤ exp 2 ((2 * n) -3).
 552 #n cases n
 553   [#_ @le_n
 554   |#n1 cases n1
 555     [#_ @le_n
 556     |#n2 cases n2
 557       [#_ @le_n
 558       |#n3 cases n3
 559         [#_ @leb_true_to_le //
 560         |#n4 cases n4
 561           [#_ @leb_true_to_le //
 562           |#n5 cases n5
 563             [#_ @leb_true_to_le //
 564             |#n6 cases n6
 565               [#_ @leb_true_to_le //
 566               |#n7 cases n7
 567                 [#_ @leb_true_to_le //
 568                 |#n8 cases n8
 569                   [#_ @leb_true_to_le //
 570                   |#n9 #H @False_ind @(absurd ?? (lt_to_not_le ?? H))
 571                    @leb_true_to_le //
 572                   ]
 573                 ]
 574               ]
 575             ]
 576           ]
 577         ]
 578       ]
 579     ]
 580   ]
 581 qed.
 582
 583 theorem le_A_exp5: ∀n. A(n) ≤ exp 2 ((2 * n) -3).
 584 #n @(nat_elim1 n) #m #Hind
 585 cases (decidable_le 9 m)
 586   [#lem cases (even_or_odd m) #a * #Hm
 587     [>Hm in ⊢ (?%?); @(transitive_le … (le_A_exp ?))
 588      @(transitive_le ? (2\sup(pred(2*a))*(2\sup((2*a)-3))))
 589       [@monotonic_le_times_r @Hind >Hm >(times_n_1 a) in ⊢ (?%?);
 590        >commutative_times @(monotonic_lt_times_l  … (le_n ?))
 591        @(transitive_lt ? 3)
 592         [@lt_O_S |@(le_times_to_le 2) [@lt_O_S |<Hm @lt_to_le @lem]]
 593       |<Hm <exp_plus_times @(le_exp … (lt_O_S ?))
 594        whd in match (times 2 m); >commutative_times <times_n_1
 595        <plus_minus_commutative
 596         [@monotonic_le_plus_l @le_pred_n
 597         |@(transitive_le … lem) @leb_true_to_le //
 598         ]
 599       ]
 600     |@(transitive_le ? (A (2*(S a))))
 601       [@monotonic_A >Hm normalize <plus_n_Sm @le_n_Sn
 602       |@(transitive_le ? ((exp 2 ((2*(S a))-2))*A (S a)))
 603         [@lt_4_to_le_A_exp @le_S_S
 604          @(le_times_to_le 2)[@le_n_Sn|@le_S_S_to_le <Hm @lem]
 605         |@(transitive_le ? ((2\sup((2*S a)-2))*(exp 2 ((2*(S a))-3))))
 606           [@monotonic_le_times_r @Hind >Hm @le_S_S
 607            >(times_n_1 a) in ⊢ (?%?);
 608            >commutative_times @(monotonic_lt_times_l  … (le_n ?))
 609            @(transitive_lt ? 3)
 610             [@lt_O_S |@(le_times_to_le 2) [@lt_O_S |@le_S_S_to_le <Hm @lem]]
 611           |cut (∀a. 2*(S a) = S(S(2*a))) [normalize #a <plus_n_Sm //] #times2
 612            >times2 <Hm <exp_plus_times @(le_exp … (lt_O_S ?))
 613            cases m
 614             [@le_n
 615             |#n1 cases n1
 616               [@le_n
 617               |#n2 normalize <minus_n_O <plus_n_O <plus_n_Sm
 618                normalize <minus_n_O <plus_n_Sm @le_n
 619               ]
 620             ]
 621           ]
 622         ]
 623       ]
 624     ]
 625   |#H @le_n_8_to_le_A_exp @le_S_S_to_le @not_le_to_lt //
 626   ]
 627 qed.
 628
 629 theorem le_exp_Al:∀n. O < n → exp 2 n ≤ A (2 * n).
 630 #n #posn @(transitive_le ? ((exp 2 (2*n))/(2*n)))
 631   [@le_times_to_le_div
 632     [>(times_n_O O) in ⊢ (?%?); @lt_times [@lt_O_S|//]
 633     |normalize in ⊢ (??(??%)); < plus_n_O >exp_plus_times
 634      @le_times [2://] elim posn [//]
 635      #m #le1m #Hind whd in ⊢ (??%); >commutative_times in ⊢ (??%);
 636      @monotonic_le_times_r @(transitive_le … Hind)
 637      >(times_n_1 m) in ⊢ (?%?); >commutative_times
 638      @(monotonic_lt_times_l  … (le_n ?)) @le1m
 639     ]
 640   |@le_times_to_le_div2
 641     [>(times_n_O O) in ⊢ (?%?); @lt_times [@lt_O_S|//]
 642     |@(transitive_le ? ((B (2*n)*(2*n))))
 643       [<commutative_times in ⊢ (??%); @le_exp_B //
 644       |@le_times [@le_B_A|@le_n]
 645       ]
 646     ]
 647   ]
 648 qed.
 649
 650 theorem le_exp_A2:∀n. 1 < n → exp 2 (n / 2) \le A n.
 651 #n #lt1n @(transitive_le ? (A(n/2*2)))
 652   [>commutative_times @le_exp_Al
 653    cases (le_to_or_lt_eq ? ? (le_O_n (n/2))) [//]
 654    #Heq @False_ind @(absurd ?? (lt_to_not_le ?? lt1n))
 655    >(div_mod n 2) <Heq whd in ⊢ (?%?);
 656    @le_S_S_to_le @(lt_mod_m_m n 2) @lt_O_S
 657   |@monotonic_A >(div_mod n 2) in ⊢ (??%); @le_plus_n_r
 658   ]
 659 qed.
 660
 661 theorem eq_sigma_pi_SO_n: ∀n.∑_{i < n} 1 = n.
 662 #n elim n //
 663 qed.
 664
 665 theorem leA_prim: ∀n.
 666   exp n (prim n) \le A n * ∏_{p < S n | primeb p} p.
 667 #n <(exp_sigma (S n) n primeb) <times_pi @le_pi
 668 #p #ltp #primep @lt_to_le @lt_exp_log
 669 @prime_to_lt_SO @primeb_true_to_prime //
 670 qed.
 671
 672 theorem le_prim_log : ∀n,b. 1 < b →
 673   log b (A n) ≤ prim n * (S (log b n)).
 674 #n #b #lt1b @(transitive_le … (log_exp1 …)) [@le_log // | //]
 675 qed.
 676
 677 (*********************** the inequalities ***********************)
 678 lemma exp_Sn: ∀b,n. exp b (S n) = b * (exp b n).
 679 normalize //
 680 qed.
 681
 682 theorem le_exp_priml: ∀n. O < n →
 683   exp 2 (2*n) ≤ exp (2*n) (S(prim (2*n))).
 684 #n #posn @(transitive_le ? (((2*n*(B (2*n))))))
 685   [@le_exp_B //
 686   |>exp_Sn @monotonic_le_times_r @(transitive_le ? (A (2*n)))
 687     [@le_B_A |@le_Al]
 688   ]
 689 qed.
 690
 691 theorem le_exp_prim4l: ∀n. O < n →
 692   exp 2 (S(4*n)) ≤ exp (4*n) (S(prim (4*n))).
 693 #n #posn @(transitive_le ? (2*(4*n*(B (4*n)))))
 694   [>exp_Sn @monotonic_le_times_r
 695    cut (4*n = 2*(2*n)) [<associative_times //] #Hcut
 696    >Hcut @le_exp_B @lt_to_le whd >(times_n_1 2) in ⊢ (?%?);
 697    @monotonic_le_times_r //
 698   |>exp_Sn <associative_times >commutative_times in ⊢ (?(?%?)?);
 699    >associative_times @monotonic_le_times_r @(transitive_le ? (A (4*n)))
 700     [@le_B_A4 // |@le_Al]
 701   ]
 702 qed.
 703
 704 theorem le_priml: ∀n. O < n →
 705   2*n ≤ (S (log 2 (2*n)))*S(prim (2*n)).
 706 #n #posn <(eq_log_exp 2 (2*n) ?) in ⊢ (?%?);
 707   [@(transitive_le ? ((log 2) (exp (2*n) (S(prim (2*n))))))
 708     [@le_log [@le_n |@le_exp_priml //]
 709     |>commutative_times in ⊢ (??%); @log_exp1 @le_n
 710     ]
 711   |@le_n
 712   ]
 713 qed.
 714
 715 theorem le_exp_primr: ∀n.
 716   exp n (prim n) ≤ exp 2 (2*(2*n-3)).
 717 #n @(transitive_le ? (exp (A n) 2))
 718   [>exp_Sn >exp_Sn whd in match (exp ? 0); <times_n_1 @leA_r2
 719   |>commutative_times <exp_exp_times @le_exp1 [@lt_O_S |@le_A_exp5]
 720   ]
 721 qed.
 722
 723 (* bounds *)
 724 theorem le_primr: ∀n. 1 < n → prim n \le 2*(2*n-3)/log 2 n.
 725 #n #lt1n @le_times_to_le_div
 726   [@lt_O_log //
 727   |@(transitive_le ? (log 2 (exp n (prim n))))
 728     [>commutative_times @log_exp2
 729       [@le_n |@lt_to_le //]
 730     |<(eq_log_exp 2 (2*(2*n-3))) in ⊢ (??%);
 731       [@le_log [@le_n |@le_exp_primr]
 732       |@le_n
 733       ]
 734     ]
 735   ]
 736 qed.
 737
 738 theorem le_priml1: ∀n. O < n →
 739   2*n/((log 2 n)+2) - 1 ≤ prim (2*n).
 740 #n #posn @le_plus_to_minus @le_times_to_le_div2
 741   [>commutative_plus @lt_O_S
 742   |>commutative_times in ⊢ (??%); <plus_n_Sm <plus_n_Sm in ⊢ (??(??%));
 743    <plus_n_O <commutative_plus <log_exp
 744     [@le_priml // | //| @le_n]
 745   ]
 746 qed.
 747
 748
 749
 750