matita/matita/lib/arithmetics/chebyshev/chebyshev.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/log.ma".
  13 include "arithmetics/big_pi.ma".
  14 include "arithmetics/ord.ma".
  15
  16 (* include "nat/factorization.ma".
  17 include "nat/factorial2.ma".
  18 include "nat/o.ma". *)
  19
  20 (* (prim n) counts the number of prime numbers up to n included *)
  21 definition prim ≝ λn. ∑_{i < S n | primeb i} 1.
  22
  23 lemma le_prim_n: ∀n. prim n ≤ n.
  24 #n elim n // -n #n #H
  25 whd in ⊢ (?%?); cases (primeb (S n)) whd in ⊢ (?%?);
  26   [@le_S_S @H |@le_S @H]
  27 qed.
  28
  29 lemma not_prime_times_2: ∀n. 1 < n → ¬prime (2*n).
  30 #n #ltn % * #H #H1 @(absurd (2 = 2*n))
  31   [@H1 // %{n} //
  32   |@lt_to_not_eq >(times_n_1 2) in ⊢ (?%?); @monotonic_lt_times_r //
  33   ]
  34 qed.
  35
  36 theorem eq_prim_prim_pred: ∀n. 1 < n →
  37   prim (2*n) = prim (pred (2*n)).
  38 #n #ltn
  39 lapply (S_pred (2*n) ?) [>(times_n_1 0) in ⊢ (?%?); @lt_times //] #H2n
  40 lapply (not_prime_times_2 n ltn) #notp2n
  41 whd in ⊢ (??%?); >(not_prime_to_primeb_false … notp2n) whd in ⊢ (??%?);
  42 <H2n in ⊢ (??%?); %
  43 qed.
  44
  45 theorem le_prim_n1: ∀n. 4 ≤ n →
  46   prim (S(2*n)) ≤ n.
  47 #n #le4 elim le4 -le4
  48   [@le_n
  49   |#m #le4 cut (S (2*m) = pred (2*(S m))) [normalize //] #Heq >Heq
  50    <eq_prim_prim_pred [2: @le_S_S @(transitive_le … le4) //]
  51    #H whd in ⊢ (?%?); cases (primeb (S (2*S m)))
  52     [@le_S_S @H |@le_S @H]
  53   ]
  54 qed.
  55
  56 (* usefull to kill a successor in bertrand *)
  57 theorem le_prim_n2: ∀n. 7 ≤ n → prim (S(2*n)) ≤ pred n.
  58 #n #le7 elim le7 -le7
  59   [@le_n
  60   |#m #le7 cut (S (2*m) = pred (2*(S m))) [normalize //] #Heq >Heq
  61    <eq_prim_prim_pred [2: @le_S_S @(transitive_le … le7) //]
  62    #H whd in ⊢ (?%?);
  63    whd in ⊢ (??%); <(S_pred m) in ⊢ (??%); [2: @(transitive_le … le7) //]
  64    cases (primeb (S (2*S m))) [@le_S_S @H |@le_S @H]
  65   ]
  66 qed.
  67
  68 lemma even_or_odd: ∀n.∃a.n=2*a ∨ n = S(2*a).
  69 #n elim n -n
  70   [%{0} %1 %
  71   |#n * #a * #Hn [%{a} %2 @eq_f @Hn | %{(S a)} %1 >Hn normalize //
  72   ]
  73 qed.
  74
  75 (* axiom daemon : ∀P:Prop.P. *)
  76
  77 (* la prova potrebbe essere migliorata *)
  78 theorem le_prim_n3: ∀n. 15 ≤ n →
  79   prim n ≤ pred (n/2).
  80 #n #len cases (even_or_odd (pred n)) #a * #Hpredn
  81   [cut (n = S (2*a)) [<Hpredn @sym_eq @S_pred @(transitive_le … len) //] #Hn
  82    >Hn @(transitive_le ? (pred a))
  83     [@le_prim_n2 @(le_times_to_le 2) [//|@le_S_S_to_le <Hn @len]
  84     |@monotonic_pred @le_times_to_le_div //
  85     ]
  86   |cut (n = (2*S a))
  87     [normalize normalize in Hpredn:(???%); <plus_n_Sm <Hpredn @sym_eq @S_pred
  88      @(transitive_le … len) //] #Hn
  89    >Hn @(transitive_le ? (pred a))
  90     [>eq_prim_prim_pred
  91       [2:@(lt_times_n_to_lt_r 2) <Hn @(transitive_le … len) //]
  92      <Hn >Hpredn @le_prim_n2 @le_S_S_to_le @(lt_times_n_to_lt_r 2) <Hn @len
  93     |@monotonic_pred @le_times_to_le_div //
  94     ]
  95   ]
  96 qed.
  97
  98 (* This is chebishev psi function *)
  99 definition A: nat → nat ≝
 100   λn.∏_{p < S n | primeb p} (exp p (log p n)).
 101
 102 definition psi_def : ∀n.
 103   A n = ∏_{p < S n | primeb p} (exp p (log p n)).
 104 // qed.
 105
 106 theorem le_Al1: ∀n.
 107   A n ≤ ∏_{p < S n | primeb p} n.
 108 #n cases n [@le_n |#m @le_pi #i #_ #_ @le_exp_log //]
 109 qed.
 110
 111 theorem le_Al: ∀n. A n ≤ exp n (prim n).
 112 #n <exp_sigma @le_Al1
 113 qed.
 114
 115 theorem leA_r2: ∀n.
 116   exp n (prim n) ≤ A n * A n.
 117 #n elim (le_to_or_lt_eq ?? (le_O_n n)) #Hn
 118   [<(exp_sigma (S n) n primeb) <times_pi
 119    @le_pi #i #lti #primei
 120    cut (1<n)
 121      [@(lt_to_le_to_lt … (le_S_S_to_le … lti)) @prime_to_lt_SO
 122       @primeb_true_to_prime //] #lt1n
 123    <exp_plus_times
 124    @(transitive_le ? (exp i (S(log i n))))
 125     [@lt_to_le @lt_exp_log @prime_to_lt_SO @primeb_true_to_prime //
 126     |@le_exp
 127       [@prime_to_lt_O @primeb_true_to_prime //
 128       |>(plus_n_O (log i n)) in ⊢ (?%?); >plus_n_Sm
 129        @monotonic_le_plus_r @lt_O_log //
 130        @le_S_S_to_le //
 131       ]
 132     ]
 133   |<Hn @le_n
 134   ]
 135 qed.
 136
 137 (* an equivalent formulation for psi *)
 138 definition A': nat → nat ≝
 139 λn. ∏_{p < S n | primeb p} (∏_{i < log p n} p).
 140
 141 lemma Adef: ∀n. A' n = ∏_{p < S n | primeb p} (∏_{i < log p n} p).
 142 // qed-.
 143
 144 theorem eq_A_A': ∀n.A n = A' n.
 145 #n @same_bigop // #i #lti #primebi
 146 @(trans_eq ? ? (exp i (∑_{x < log i n} 1)))
 147   [@eq_f @sym_eq @sigma_const
 148   |@sym_eq @exp_sigma
 149   ]
 150 qed.
 151
 152 theorem eq_pi_p_primeb_divides_b: ∀n,m.
 153 ∏_{p<n | primeb p ∧ dividesb p m} (exp p (ord m p))
 154   = ∏_{p<n | primeb p} (exp p (ord m p)).
 155 #n #m elim n // #n1 #Hind cases (true_or_false (primeb n1)) #Hprime
 156   [>bigop_Strue in ⊢ (???%); //
 157    cases (true_or_false (dividesb n1 m)) #Hdivides
 158     [>bigop_Strue [@eq_f @Hind| @true_to_andb_true //]
 159   |>bigop_Sfalse
 160     [>not_divides_to_ord_O
 161       [whd in ⊢ (???(?%?)); //
 162       |@dividesb_false_to_not_divides //
 163       |@primeb_true_to_prime //
 164       ]
 165     |>Hprime >Hdivides %
 166     ]
 167   ]
 168 |>bigop_Sfalse [>bigop_Sfalse // |>Hprime %]
 169 ]
 170 qed.
 171
 172 (* integrations to minimization *)
 173 theorem false_to_lt_max: ∀f,n,m.O < n →
 174   f n = false → max m f ≤ n → max m f < n.
 175 #f #n #m #posn #Hfn #Hmax cases (le_to_or_lt_eq ?? Hmax) -Hmax #Hmax
 176   [//
 177   |cases (exists_max_forall_false f m)
 178     [* #_ #Hfmax @False_ind @(absurd ?? not_eq_true_false) //
 179     |* //
 180     ]
 181   ]
 182 qed.
 183
 184 (* boh ...
 185 theorem lt_max_to_false : ∀f,n,m.
 186   max n f < m → m ≤ n → f m = false.
 187 #f #n elim n
 188   [#m #H1 #H2 @False_ind @(absurd ? H2) @lt_to_not_le //
 189   |#n1 #Hind #m whd in ⊢ (?%?→?); #Hmax #ltm
 190 elim (max_S_max f n1); in H1 ⊢ %.
 191 elim H1.
 192 absurd (m \le S n1).assumption.
 193 apply lt_to_not_le.rewrite < H5.assumption.
 194 elim H1.
 195 apply (le_n_Sm_elim m n1 H2).
 196 intro.
 197 apply H.rewrite < H5.assumption.
 198 apply le_S_S_to_le.assumption.
 199 intro.rewrite > H6.assumption.
 200 qed. *)
 201
 202 (* integrations to minimization *)
 203 lemma lt_1_max_prime: ∀n. 1 <  n →
 204   1 < max (S n) (λi:nat.primeb i∧dividesb i n).
 205 #n #lt1n
 206 @(lt_to_le_to_lt ? (smallest_factor n))
 207   [@lt_SO_smallest_factor //
 208   |@true_to_le_max
 209     [@le_S_S @le_smallest_factor_n
 210     |@true_to_andb_true
 211       [@prime_to_primeb_true @prime_smallest_factor_n //
 212       |@divides_to_dividesb_true
 213         [@lt_O_smallest_factor @lt_to_le //
 214         |@divides_smallest_factor_n @lt_to_le //
 215         ]
 216       ]
 217     ]
 218   ]
 219 qed.
 220
 221 theorem lt_max_to_pi_p_primeb: ∀q,m. O<m → max (S m) (λi.primeb i ∧ dividesb i m)<q →
 222   m = ∏_{p < q | primeb p ∧ dividesb p m} (exp p (ord m p)).
 223 #q elim q
 224   [#m #posm #Hmax normalize @False_ind @(absurd … Hmax (not_le_Sn_O ?))
 225   |#n #Hind #m #posm #Hmax
 226    cases (true_or_false (primeb n∧dividesb n m)) #Hcase
 227     [>bigop_Strue
 228       [>(exp_ord n m … posm) in ⊢ (??%?);
 229         [@eq_f >(Hind (ord_rem m n))
 230           [@same_bigop
 231             [#x #ltxn cases (true_or_false (primeb x)) #Hx >Hx
 232               [cases (true_or_false (dividesb x (ord_rem m n))) #Hx1 >Hx1
 233                 [@sym_eq @divides_to_dividesb_true
 234                   [@prime_to_lt_O @primeb_true_to_prime //
 235                   |@(transitive_divides ? (ord_rem m n))
 236                     [@dividesb_true_to_divides //
 237                     |@(divides_ord_rem … posm) @(transitive_lt … ltxn)
 238                      @prime_to_lt_SO @primeb_true_to_prime //
 239                     ]
 240                   ]
 241                 |@sym_eq @not_divides_to_dividesb_false
 242                   [@prime_to_lt_O @primeb_true_to_prime //
 243                   |@(ord_O_to_not_divides … posm)
 244                     [@primeb_true_to_prime //
 245                     |<(ord_ord_rem n … posm … ltxn)
 246                       [@not_divides_to_ord_O
 247                         [@primeb_true_to_prime //
 248                         |@dividesb_false_to_not_divides //
 249                         ]
 250                       |@primeb_true_to_prime //
 251                       |@primeb_true_to_prime @(andb_true_l ?? Hcase)
 252                       ]
 253                     ]
 254                   ]
 255                 ]
 256               |//
 257               ]
 258             |#x #ltxn #Hx @eq_f @ord_ord_rem //
 259               [@primeb_true_to_prime @(andb_true_l ? ? Hcase)
 260               |@primeb_true_to_prime @(andb_true_l ? ? Hx)
 261               ]
 262             ]
 263           |@not_eq_to_le_to_lt
 264             [elim (exists_max_forall_false (λi:nat.primeb i∧dividesb i (ord_rem m n)) (S(ord_rem m n)))
 265               [* #Hex #Hord_rem cases Hex #x * #H6 #H7 % #H
 266                >H in Hord_rem; #Hn @(absurd ?? (not_divides_ord_rem m n posm ?))
 267                 [@dividesb_true_to_divides @(andb_true_r ?? Hn)
 268                 |@prime_to_lt_SO @primeb_true_to_prime @(andb_true_l ?? Hn)
 269                 ]
 270               |* #Hall #Hmax >Hmax @lt_to_not_eq @prime_to_lt_O
 271                @primeb_true_to_prime @(andb_true_l ?? Hcase)
 272               ]
 273             |@(transitive_le ? (max (S m) (λi:nat.primeb i∧dividesb i (ord_rem m n))))
 274               [@le_to_le_max @le_S_S @(divides_to_le … posm) @(divides_ord_rem … posm)
 275                @prime_to_lt_SO @primeb_true_to_prime @(andb_true_l ?? Hcase)
 276               |@(transitive_le ? (max (S m) (λi:nat.primeb i∧dividesb i m)))
 277                 [@le_max_f_max_g #i #ltim #Hi
 278                  cases (true_or_false (primeb i)) #Hprimei >Hprimei
 279                   [@divides_to_dividesb_true
 280                     [@prime_to_lt_O @primeb_true_to_prime //
 281                     |@(transitive_divides ? (ord_rem m n))
 282                       [@dividesb_true_to_divides @(andb_true_r ?? Hi)
 283                       |@(divides_ord_rem … posm)
 284                        @prime_to_lt_SO @primeb_true_to_prime
 285                        @(andb_true_l ?? Hcase)
 286                       ]
 287                     ]
 288                   |>Hprimei in Hi; #Hi @Hi
 289                   ]
 290                 |@le_S_S_to_le //
 291                 ]
 292               ]
 293             ]
 294           |@(lt_O_ord_rem … posm) @prime_to_lt_SO
 295            @primeb_true_to_prime @(andb_true_l ?? Hcase)
 296           ]
 297         |@prime_to_lt_SO @primeb_true_to_prime @(andb_true_l ?? Hcase)
 298         ]
 299       |//
 300       ]
 301     |cases (le_to_or_lt_eq ?? posm) #Hm
 302       [>bigop_Sfalse
 303         [@(Hind … posm) @false_to_lt_max
 304           [@(lt_to_le_to_lt ? (max (S m) (λi:nat.primeb i∧dividesb i m)))
 305             [@lt_to_le @lt_1_max_prime //
 306             |@le_S_S_to_le //
 307             ]
 308           |//
 309           |@le_S_S_to_le //
 310           ]
 311         |@Hcase
 312         ]
 313       |<Hm
 314        <(bigop_false (S n) ? 1 times (λp:nat.p\sup(ord 1 p))) in ⊢ (??%?);
 315        @same_bigop
 316         [#i #lein cases (true_or_false (primeb i)) #primei >primei //
 317          @sym_eq @not_divides_to_dividesb_false
 318           [@prime_to_lt_O @primeb_true_to_prime //
 319           |% #divi @(absurd ?? (le_to_not_lt i 1 ?))
 320             [@prime_to_lt_SO @(primeb_true_to_prime ? primei)
 321             |@divides_to_le //
 322             ]
 323           ]
 324         |//
 325         ]
 326       ]
 327     ]
 328   ]
 329 qed.
 330
 331 (* factorization of n into primes *)
 332 theorem pi_p_primeb_dividesb: ∀n. O < n →
 333   n = ∏_{ p < S n | primeb p ∧ dividesb p n} (exp p (ord n p)).
 334 #n #posn @lt_max_to_pi_p_primeb // @lt_max_n @le_S @posn
 335 qed.
 336
 337 theorem pi_p_primeb: ∀n. O < n →
 338   n = ∏_{ p < (S n) | primeb p}(exp p (ord n p)).
 339 #n #posn <eq_pi_p_primeb_divides_b @pi_p_primeb_dividesb //
 340 qed.
 341
 342 theorem le_ord_log: ∀n,p. O < n → 1 < p →
 343   ord n p ≤ log p n.
 344 #n #p #posn #lt1p >(exp_ord p ? lt1p posn) in ⊢ (??(??%));
 345 >log_exp // @lt_O_ord_rem //
 346 qed.
 347
 348 theorem sigma_p_dividesb:
 349 ∀m,n,p. O < n → prime p → p ∤ n →
 350 m = ∑_{ i < m | dividesb (p\sup (S i)) ((exp p m)*n)} 1.
 351 #m elim m // -m #m #Hind #n #p #posn #primep #ndivp
 352 >bigop_Strue
 353   [>commutative_plus <plus_n_Sm @eq_f <plus_n_O
 354    >(Hind n p posn primep ndivp) in ⊢ (? ? % ?);
 355    @same_bigop
 356     [#i #ltim cases (true_or_false (dividesb (p\sup(S i)) (p\sup m*n))) #Hc >Hc
 357       [@sym_eq @divides_to_dividesb_true
 358         [@lt_O_exp @prime_to_lt_O //
 359         |%{((exp p (m - i))*n)} <associative_times
 360          <exp_plus_times @eq_f2 // @eq_f normalize @eq_f >commutative_plus
 361          @plus_minus_m_m @lt_to_le //
 362         ]
 363       |(* @sym_eq *)
 364        @False_ind @(absurd ?? (dividesb_false_to_not_divides ? ? Hc))
 365        %{((exp p (m - S i))*n)} <associative_times <exp_plus_times @eq_f2
 366         [@eq_f >commutative_plus @plus_minus_m_m //
 367            assumption
 368         |%
 369         ]
 370       ]
 371     |//
 372     ]
 373   |@divides_to_dividesb_true
 374     [@lt_O_exp @prime_to_lt_O // | %{n} //]
 375   ]
 376 qed.
 377
 378 theorem sigma_p_dividesb1:
 379 ∀m,n,p,k. O < n → prime p → p ∤ n → m ≤ k →
 380   m = ∑_{i < k | dividesb (p\sup (S i)) ((exp p m)*n)} 1.
 381 #m #n #p #k #posn #primep #ndivp #lemk
 382 lapply (prime_to_lt_SO ? primep) #lt1p
 383 lapply (prime_to_lt_O ? primep) #posp
 384 >(sigma_p_dividesb m n p posn primep ndivp) in ⊢ (??%?);
 385 >(pad_bigop k m) // @same_bigop
 386   [#i #ltik cases (true_or_false (leb m i)) #Him > Him
 387     [whd in ⊢(??%?); @sym_eq
 388      @not_divides_to_dividesb_false
 389       [@lt_O_exp //
 390       |lapply (leb_true_to_le … Him) -Him #Him
 391        % #Hdiv @(absurd ?? (le_to_not_lt ?? Him))
 392        (* <(ord_exp p m lt1p) *) >(plus_n_O m)
 393        <(not_divides_to_ord_O ?? primep ndivp)
 394        <(ord_exp p m lt1p)
 395        <ord_times //
 396         [whd <(ord_exp p (S i) lt1p)
 397          @divides_to_le_ord //
 398           [@lt_O_exp //
 399           |>(times_n_O O) @lt_times // @lt_O_exp //
 400           ]
 401         |@lt_O_exp //
 402         ]
 403       ]
 404     |%
 405     ]
 406   |//
 407   ]
 408 qed.
 409
 410 theorem eq_ord_sigma_p:
 411 ∀n,m,x. O < n → prime x →
 412 exp x m ≤ n → n < exp x (S m) →
 413 ord n x= ∑_{i < m | dividesb (x\sup (S i)) n} 1.
 414 #n #m #x #posn #primex #Hexp #ltn
 415 lapply (prime_to_lt_SO ? primex) #lt1x
 416 >(exp_ord x n) in ⊢ (???%); // @sigma_p_dividesb1
 417   [@lt_O_ord_rem //
 418   |//
 419   |@not_divides_ord_rem //
 420   |@le_S_S_to_le @(le_to_lt_to_lt ? (log x n))
 421     [@le_ord_log //
 422     |@(lt_exp_to_lt x)
 423       [@lt_to_le //
 424       |@(le_to_lt_to_lt ? n ? ? ltn) @le_exp_log //
 425       ]
 426     ]
 427   ]
 428 qed.
 429
 430 theorem pi_p_primeb1: ∀n. O < n →
 431 n = ∏_{p < S n| primeb p}
 432   (∏_{i < log p n| dividesb (exp p (S i)) n} p).
 433 #n #posn >(pi_p_primeb n posn) in ⊢ (??%?);
 434 @same_bigop
 435   [//
 436   |#p #ltp #primep >exp_sigma @eq_f @eq_ord_sigma_p
 437     [//
 438     |@primeb_true_to_prime //
 439     |@le_exp_log //
 440     |@lt_exp_log @prime_to_lt_SO @primeb_true_to_prime //
 441     ]
 442   ]
 443 qed.
 444
 445 (* the factorial function *)
 446 theorem eq_fact_pi_p:∀n.
 447   fact n = ∏_{i < S n | leb 1 i} i.
 448 #n elim n // #n1 #Hind whd in ⊢ (??%?); >commutative_times >bigop_Strue
 449   [@eq_f // | % ]
 450 qed.
 451
 452 theorem eq_sigma_p_div: ∀n,q.O < q →
 453   ∑_{ m < S n | leb (S O) m ∧ dividesb q m} 1 =n/q.
 454 #n #q #posq
 455 @(div_mod_spec_to_eq n q ? (n \mod q) ? (n \mod q))
 456   [@div_mod_spec_intro
 457     [@lt_mod_m_m //
 458     |elim n
 459       [normalize cases q //
 460       |#n1 #Hind cases (or_div_mod1 n1 q posq)
 461         [* #divq #eqn1  >divides_to_mod_O //
 462          <plus_n_O >bigop_Strue
 463           [>eqn1 in ⊢ (??%?); @eq_f2
 464             [<commutative_plus <plus_n_Sm <plus_n_O @eq_f
 465              @(div_mod_spec_to_eq n1 q (div n1 q) (mod n1 q) ? (mod n1 q))
 466               [@div_mod_spec_div_mod //
 467               |@div_mod_spec_intro [@lt_mod_m_m // | //]
 468               ]
 469             |%
 470             ]
 471           |@true_to_andb_true [//|@divides_to_dividesb_true //]
 472           ]
 473         |* #ndiv #eqn1 >bigop_Sfalse
 474           [>(mod_S … posq)
 475             [< plus_n_Sm @eq_f //
 476             |cases (le_to_or_lt_eq (S (mod n1 q)) q ?)
 477               [//
 478               |#eqq @False_ind cases ndiv #Hdiv @Hdiv
 479                %{(S(div n1 q))} <times_n_Sm <commutative_plus //
 480               |@lt_mod_m_m //
 481               ]
 482             ]
 483           |>not_divides_to_dividesb_false //
 484           ]
 485         ]
 486       ]
 487     ]
 488   |@div_mod_spec_div_mod //
 489   ]
 490 qed.
 491
 492 definition Atimes ≝ mk_Aop nat 1 times ???.
 493   [#a normalize <plus_n_O %
 494   |#a @sym_eq @times_n_1
 495   |#a #b #c @sym_eq @associative_times
 496   ]
 497 qed.
 498
 499 definition ACtimes ≝ mk_ACop nat 1 Atimes commutative_times.
 500
 501 lemma ACtimesdef: ∀n,m. ACtimes n m = n * m.
 502 // qed-.
 503
 504 (* still another characterization of the factorial *)
 505 theorem fact_pi_p: ∀n.
 506 fact n = ∏_{ p < S n | primeb p}
 507            (∏_{i < log p n} (exp p (n /(exp p (S i))))).
 508 #n >eq_fact_pi_p
 509 @(trans_eq ??
 510   (∏_{m < S n | leb 1 m}
 511    (∏_{p < S m | primeb p}
 512     (∏_{i < log p m | dividesb (exp p (S i)) m} p))))
 513   [@same_bigop [// |#x #Hx1 #Hx2  @pi_p_primeb1 @leb_true_to_le //]
 514   |@(trans_eq ??
 515     (∏_{m < S n | leb 1 m}
 516       (∏_{p < S m | primeb p ∧ leb p m}
 517        (∏_{ i < log p m | dividesb ((p)\sup(S i)) m} p))))
 518     [@same_bigop
 519       [//
 520       |#x #Hx1 #Hx2 @same_bigop
 521         [#p #ltp >(le_to_leb_true … (le_S_S_to_le …ltp))
 522          cases (primeb p) //
 523         |//
 524         ]
 525       ]
 526     |@(trans_eq ??
 527       (∏_{m < S n | leb 1 m}
 528        (∏_{p < S n | primeb p ∧ leb p m}
 529          (∏_{i < log p m |dividesb ((p)\sup(S i)) m} p))))
 530       [@same_bigop
 531         [//
 532         |#p #Hp1 #Hp2 @pad_bigop1
 533           [@Hp1
 534           |#i #lti #upi >lt_to_leb_false
 535             [cases (primeb i) //|@lti]
 536           ]
 537         ]
 538       |(* make a general theorem *)
 539        @(trans_eq ??
 540         (∏_{p < S n | primeb p}
 541           (∏_{m < S n | leb p m}
 542            (∏_{i < log p m | dividesb (p^(S i)) m} p))))
 543         [@(bigop_commute … ACtimes … (lt_O_S n) (lt_O_S n))
 544          #i #j #lti #ltj
 545          cases (true_or_false (primeb j ∧ leb j i)) #Hc >Hc
 546           [>(le_to_leb_true 1 i)
 547             [//
 548             |@(transitive_le ? j)
 549               [@prime_to_lt_O @primeb_true_to_prime @(andb_true_l ? ? Hc)
 550               |@leb_true_to_le @(andb_true_r ?? Hc)
 551               ]
 552             ]
 553           |cases(leb 1 i) //
 554           ]
 555         |@same_bigop
 556           [//
 557           |#p #Hp1 #Hp2
 558            @(trans_eq ??
 559             (∏_{m < S n | leb p m}
 560              (∏_{i < log p n | dividesb (p\sup(S i)) m} p)))
 561             [@same_bigop
 562               [//
 563               |#x #Hx1 #Hx2 @sym_eq
 564                @sym_eq @pad_bigop1
 565                 [@le_log
 566                   [@prime_to_lt_SO @primeb_true_to_prime //
 567                   |@le_S_S_to_le //
 568                   ]
 569                 |#i #Hi1 #Hi2 @not_divides_to_dividesb_false
 570                   [@lt_O_exp @prime_to_lt_O @primeb_true_to_prime //
 571                   |@(not_to_not … (lt_to_not_le x (exp p (S i)) ?))
 572                     [#H @divides_to_le // @(lt_to_le_to_lt ? p)
 573                       [@prime_to_lt_O @primeb_true_to_prime //
 574                       |@leb_true_to_le //
 575                       ]
 576                     |@(lt_to_le_to_lt ? (exp p (S(log p x))))
 577                       [@lt_exp_log @prime_to_lt_SO @primeb_true_to_prime //
 578                       |@le_exp
 579                         [@ prime_to_lt_O @primeb_true_to_prime //
 580                         |@le_S_S //
 581                         ]
 582                       ]
 583                     ]
 584                   ]
 585                 ]
 586               ]
 587             |@
 588              (trans_eq ? ?
 589               (∏_{i < log p n}
 590                 (∏_{m < S n | leb p m ∧ dividesb (p\sup(S i)) m} p)))
 591               [@(bigop_commute ?????? nat 1 ACtimes (λm,i.p) ???) //
 592                cut (p ≤ n) [@le_S_S_to_le //] #lepn
 593                @(lt_O_log … lepn) @(lt_to_le_to_lt … lepn) @prime_to_lt_SO
 594                @primeb_true_to_prime //
 595               |@same_bigop
 596                 [//
 597                 |#m #ltm #_ >exp_sigma @eq_f
 598                  @(trans_eq ??
 599                   (∑_{i < S n |leb 1 i∧dividesb (p\sup(S m)) i} 1))
 600                   [@same_bigop
 601                     [#i #lti
 602                      cases (true_or_false (dividesb (p\sup(S m)) i)) #Hc >Hc
 603                       [cases (true_or_false (leb p i)) #Hp3 >Hp3
 604                         [>le_to_leb_true
 605                           [//
 606                           |@(transitive_le ? p)
 607                             [@prime_to_lt_O @primeb_true_to_prime //
 608                             |@leb_true_to_le //
 609                             ]
 610                           ]
 611                         |>lt_to_leb_false
 612                           [//
 613                           |@not_le_to_lt
 614                            @(not_to_not ??? (leb_false_to_not_le ?? Hp3)) #posi
 615                            @(transitive_le ? (exp p (S m)))
 616                             [>(exp_n_1 p) in ⊢ (?%?);
 617                              @le_exp
 618                               [@prime_to_lt_O @primeb_true_to_prime //
 619                               |@le_S_S @le_O_n
 620                               ]
 621                             |@(divides_to_le … posi)
 622                              @dividesb_true_to_divides //
 623                             ]
 624                           ]
 625                         ]
 626                       |cases (leb p i) cases (leb 1 i) //
 627                       ]
 628                     |//
 629                     ]
 630                   |@eq_sigma_p_div @lt_O_exp
 631                    @prime_to_lt_O @primeb_true_to_prime //
 632                   ]
 633                 ]
 634               ]
 635             ]
 636           ]
 637         ]
 638       ]
 639     ]
 640   ]
 641 qed.
 642
 643 theorem fact_pi_p2: ∀n. fact (2*n) =
 644 ∏_{p < S (2*n) | primeb p}
 645   (∏_{i < log p (2*n)}
 646     (exp p (2*(n /(exp p (S i))))*(exp p (mod (2*n /(exp p (S i))) 2)))).
 647 #n >fact_pi_p @same_bigop
 648   [//
 649   |#p #ltp #primep @same_bigop
 650     [//
 651     |#i #lti #_ <exp_plus_times @eq_f
 652      >commutative_times in ⊢ (???(?%?));
 653      cut (0 < p ^ (S i))
 654        [@lt_O_exp @prime_to_lt_O @primeb_true_to_prime //]
 655      generalize in match (p ^(S i)); #a #posa
 656      >(div_times_times n a 2) // >(commutative_times n 2)
 657      <eq_div_div_div_times //
 658     ]
 659   ]
 660 qed.
 661
 662 theorem fact_pi_p3: ∀n. fact (2*n) =
 663 ∏_{p < S (2*n) | primeb p}
 664   (∏_{i < log p (2*n)}(exp p (2*(n /(exp p (S i)))))) *
 665 ∏_{p < S (2*n) | primeb p}
 666   (∏_{i < log p (2*n)}(exp p (mod (2*n /(exp p (S i))) 2))).
 667 #n <times_pi >fact_pi_p2 @same_bigop
 668   [//
 669   |#p #ltp #primep @times_pi
 670   ]
 671 qed.
 672
 673 theorem pi_p_primeb4: ∀n. 1 < n →
 674 ∏_{p < S (2*n) | primeb p}
 675   (∏_{i < log p (2*n)}(exp p (2*(n /(exp p (S i))))))
 676 =
 677 ∏_{p < S n | primeb p}
 678   (∏_{i < log p (2*n)}(exp p (2*(n /(exp p (S i)))))).
 679 #n #lt1n
 680 @sym_eq @(pad_bigop_nil … ACtimes)
 681   [@le_S_S /2 by /
 682   |#i #ltn #lti %2
 683    >log_i_2n //
 684     [>bigop_Strue // whd in ⊢ (??(??%)?); <times_n_1
 685      <exp_n_1 >eq_div_O //
 686     |@le_S_S_to_le //
 687     ]
 688   ]
 689 qed.
 690
 691 theorem pi_p_primeb5: ∀n. 1 < n →
 692 ∏_{p < S (2*n) | primeb p}
 693   (∏_{i < log p (2*n)} (exp p (2*(n /(exp p (S i))))))
 694 =
 695 ∏_{p < S n | primeb p}
 696   (∏_{i < log p n} (exp p (2*(n /(exp p (S i)))))).
 697 #n #lt1n >(pi_p_primeb4 ? lt1n) @same_bigop
 698   [//
 699   |#p #lepn #primebp @sym_eq @(pad_bigop_nil … ACtimes)
 700     [@le_log
 701       [@prime_to_lt_SO @primeb_true_to_prime //
 702       |//
 703       ]
 704     |#i #lelog #lti %2 >eq_div_O //
 705      @(lt_to_le_to_lt ? (exp p (S(log p n))))
 706       [@lt_exp_log @prime_to_lt_SO @primeb_true_to_prime //
 707       |@le_exp
 708         [@prime_to_lt_O @primeb_true_to_prime // |@le_S_S //]
 709       ]
 710     ]
 711   ]
 712 qed.
 713
 714 theorem exp_fact_2: ∀n.
 715 exp (fact n) 2 =
 716   ∏_{p < S n| primeb p}
 717     (∏_{i < log p n} (exp p (2*(n /(exp p (S i)))))).
 718 #n >fact_pi_p <exp_pi @same_bigop
 719   [//
 720   |#p #ltp #primebp @sym_eq
 721    @(trans_eq ?? (∏_{x < log p n} (exp (exp p (n/(exp p (S x)))) 2)))
 722   [@same_bigop
 723     [//
 724     |#x #ltx #_ @sym_eq >commutative_times @exp_exp_times
 725     ]
 726   |@exp_pi
 727   ]
 728 qed.
 729
 730 definition B ≝ λn.
 731 ∏_{p < S n | primeb p}
 732   (∏_{i < log p n} (exp p (mod (n /(exp p (S i))) 2))).
 733
 734 lemma Bdef : ∀n.B n =
 735   ∏_{p < S n | primeb p}
 736   (∏_{i < log p n} (exp p (mod (n /(exp p (S i))) 2))).
 737 // qed-.
 738
 739 example B_SSSO: B 3 = 6. //
 740 qed.
 741
 742 example B_SSSSO: B 4 = 6. //
 743 qed.
 744
 745 example B_SSSSSO: B 5 = 30. //
 746 qed.
 747
 748 example B_SSSSSSO: B 6 = 20. //
 749 qed.
 750
 751 example B_SSSSSSSO: B 7 = 140. //
 752 qed.
 753
 754 example B_SSSSSSSSO: B 8 = 70. //
 755 qed.
 756
 757 theorem eq_fact_B:∀n. 1 < n →
 758   (2*n)! = exp (n!) 2 * B(2*n).
 759 #n #lt1n >fact_pi_p3 @eq_f2
 760   [@sym_eq >pi_p_primeb5 [@exp_fact_2|//] |// ]
 761 qed.
 762
 763 theorem le_B_A: ∀n. B n ≤ A n.
 764 #n >eq_A_A' @le_pi #p #ltp #primep
 765 @le_pi #i #lti #_ >(exp_n_1 p) in ⊢ (??%); @le_exp
 766   [@prime_to_lt_O @primeb_true_to_prime //
 767   |@le_S_S_to_le @lt_mod_m_m @lt_O_S
 768   ]
 769 qed.
 770
 771 theorem le_B_A4: ∀n. O < n → 2 * B (4*n) ≤ A (4*n).
 772 #n #posn >eq_A_A'
 773 cut (2 < (S (4*n)))
 774   [@le_S_S >(times_n_1 2) in ⊢ (?%?); @le_times //] #H2
 775 cut (O<log 2 (4*n))
 776   [@lt_O_log [@le_S_S_to_le @H2 |@le_S_S_to_le @H2]] #Hlog
 777 >Bdef >(bigop_diff ??? ACtimes ? 2 ? H2) [2:%]
 778 >Adef >(bigop_diff ??? ACtimes ? 2 ? H2) in ⊢ (??%); [2:%]
 779 <associative_times @le_times
 780   [>(bigop_diff ??? ACtimes ? 0 ? Hlog) [2://]
 781    >(bigop_diff ??? ACtimes ? 0 ? Hlog) in ⊢ (??%); [2:%]
 782    <associative_times >ACtimesdef @le_times
 783     [<exp_n_1 cut (4=2*2) [//] #H4 >H4 >associative_times
 784      >commutative_times in ⊢ (?(??(??(?(?%?)?)))?);
 785      >div_times [2://] >divides_to_mod_O
 786       [@le_n |%{n} // |@lt_O_S]
 787     |@le_pi #i #lti #H >(exp_n_1 2) in ⊢ (??%);
 788      @le_exp [@lt_O_S |@le_S_S_to_le @lt_mod_m_m @lt_O_S]
 789     ]
 790   |@le_pi #p #ltp #Hp @le_pi #i #lti #H
 791    >(exp_n_1 p) in ⊢ (??%); @le_exp
 792     [@prime_to_lt_O @primeb_true_to_prime @(andb_true_r ?? Hp)
 793     |@le_S_S_to_le @lt_mod_m_m @lt_O_S
 794     ]
 795   ]
 796 qed.
 797
 798 (* not usefull
 799 theorem le_fact_A:\forall n.S O < n \to
 800 fact (2*n) \le exp (fact n) 2 * A (2*n).
 801 intros.
 802 rewrite > eq_fact_B
 803   [apply le_times_r.
 804    apply le_B_A
 805   |assumption
 806   ]
 807 qed. *)
 808
 809 theorem lt_SO_to_le_B_exp: ∀n. 1 < n →
 810   B (2*n) ≤ exp 2 (pred (2*n)).
 811 #n #lt1n @(le_times_to_le (exp (fact n) 2))
 812   [@lt_O_exp //
 813   |<(eq_fact_B … lt1n) <commutative_times in ⊢ (??%);
 814    >exp_2 <associative_times @fact_to_exp
 815   ]
 816 qed.
 817
 818 theorem le_B_exp: ∀n.
 819   B (2*n) ≤ exp 2 (pred (2*n)).
 820 #n cases n
 821   [@le_n|#n1 cases n1 [@le_n |#n2 @lt_SO_to_le_B_exp @le_S_S @lt_O_S]]
 822 qed.
 823
 824 theorem lt_4_to_le_B_exp: ∀n.4 < n →
 825   B (2*n) \le exp 2 ((2*n)-2).
 826 #n #lt4n @(le_times_to_le (exp (fact n) 2))
 827   [@lt_O_exp //
 828   |<eq_fact_B
 829     [<commutative_times in ⊢ (??%); >exp_2 <associative_times
 830      @lt_4_to_fact //
 831     |@lt_to_le @lt_to_le @lt_to_le //
 832     ]
 833   ]
 834 qed.
 835
 836 theorem lt_1_to_le_exp_B: ∀n. 1 < n →
 837   exp 2 (2*n) ≤ 2 * n * B (2*n).
 838 #n #lt1n
 839 @(le_times_to_le (exp (fact n) 2))
 840   [@lt_O_exp @le_1_fact
 841   |<associative_times in ⊢ (??%); >commutative_times in ⊢ (??(?%?));
 842    >associative_times in ⊢ (??%); <(eq_fact_B … lt1n)
 843    <commutative_times; @exp_to_fact2 @lt_to_le //
 844   ]
 845 qed.
 846
 847 theorem le_exp_B: ∀n. O < n →
 848   exp 2 (2*n) ≤ 2 * n * B (2*n).
 849 #n #posn cases posn
 850   [@le_n |#m #lt1m @lt_1_to_le_exp_B @le_S_S // ]
 851 qed.
 852
 853 let rec bool_to_nat b ≝
 854   match b with [true ⇒ 1 | false ⇒ 0].
 855
 856 theorem eq_A_2_n: ∀n.O < n →
 857 A(2*n) =
 858  ∏_{p <S (2*n) | primeb p}
 859   (∏_{i <log p (2*n)} (exp p (bool_to_nat (leb (S n) (exp p (S i)))))) *A n.
 860 #n #posn >eq_A_A' > eq_A_A'
 861 cut (
 862  ∏_{p < S n | primeb p} (∏_{i <log p n} p)
 863  = ∏_{p < S (2*n) | primeb p}
 864      (∏_{i <log p (2*n)} (p\sup(bool_to_nat (¬ (leb (S n) (exp p (S i))))))))
 865   [2: #Hcut >Adef in ⊢ (???%); >Hcut
 866    <times_pi >Adef @same_bigop
 867     [//
 868     |#p #lt1p #primep <times_pi @same_bigop
 869       [//
 870       |#i #lt1i #_ cases (true_or_false (leb (S n) (exp p (S i)))) #Hc >Hc
 871         [normalize <times_n_1 >plus_n_O //
 872         |normalize <plus_n_O <plus_n_O //
 873         ]
 874       ]
 875     ]
 876   |@(trans_eq ??
 877     (∏_{p < S n | primeb p}
 878       (∏_{i < log p n} (p \sup(bool_to_nat (¬leb (S n) (exp p (S i))))))))
 879     [@same_bigop
 880       [//
 881       |#p #lt1p #primep @same_bigop
 882         [//
 883         |#i #lti#_ >lt_to_leb_false
 884           [normalize @plus_n_O
 885           |@le_S_S @(transitive_le ? (exp p (log p n)))
 886             [@le_exp [@prime_to_lt_O @primeb_true_to_prime //|//]
 887             |@le_exp_log //
 888             ]
 889           ]
 890         ]
 891       ]
 892     |@(trans_eq ??
 893       (∏_{p < S (2*n) | primeb p}
 894        (∏_{i <log p n} (p \sup(bool_to_nat (¬leb (S n) (p \sup(S i))))))))
 895       [@(pad_bigop_nil … Atimes)
 896         [@le_S_S //|#i #lti #upi %2 >lt_to_log_O //]
 897       |@same_bigop
 898         [//
 899         |#p #ltp #primep @(pad_bigop_nil … Atimes)
 900           [@le_log
 901             [@prime_to_lt_SO @primeb_true_to_prime //|//]
 902           |#i #lei #iup %2 >le_to_leb_true
 903             [%
 904             |@(lt_to_le_to_lt ? (exp p (S (log p n))))
 905               [@lt_exp_log @prime_to_lt_SO @primeb_true_to_prime //
 906               |@le_exp
 907                 [@prime_to_lt_O @primeb_true_to_prime //
 908                 |@le_S_S //
 909                 ]
 910               ]
 911             ]
 912           ]
 913         ]
 914       ]
 915     ]
 916   ]
 917 qed.
 918
 919 theorem le_A_BA1: ∀n. O < n →
 920   A(2*n) ≤ B(2*n)*A n.
 921 #n #posn >(eq_A_2_n … posn) @le_times [2:@le_n]
 922 >Bdef @le_pi #p #ltp #primep @le_pi #i #lti #_ @le_exp
 923   [@prime_to_lt_O @primeb_true_to_prime //
 924   |cases (true_or_false (leb (S n) (exp p (S i)))) #Hc >Hc
 925     [whd in ⊢ (?%?);
 926      cut (2*n/p\sup(S i) = 1) [2: #Hcut >Hcut @le_n]
 927      @(div_mod_spec_to_eq (2*n) (exp p (S i))
 928        ? (mod (2*n) (exp p (S i))) ? (minus (2*n) (exp p (S i))) )
 929       [@div_mod_spec_div_mod @lt_O_exp @prime_to_lt_O @primeb_true_to_prime //
 930       |cut (p\sup(S i)≤2*n)
 931         [@(transitive_le ? (exp p (log p (2*n))))
 932           [@le_exp [@prime_to_lt_O @primeb_true_to_prime // | //]
 933           |@le_exp_log >(times_n_O O) in ⊢ (?%?); @lt_times //
 934           ]
 935         ] #Hcut
 936        @div_mod_spec_intro
 937         [@lt_plus_to_minus
 938           [// |normalize in ⊢ (? % ?); < plus_n_O @lt_plus @leb_true_to_le //]
 939         |>commutative_plus >commutative_times in ⊢ (???(??%));
 940          < times_n_1 @plus_minus_m_m //
 941         ]
 942       ]
 943     |@le_O_n
 944     ]
 945   ]
 946 qed.
 947
 948 theorem le_A_BA: ∀n. A(2*n) \le B(2*n)*A n.
 949 #n cases n [@le_n |#m @le_A_BA1 @lt_O_S]
 950 qed.
 951
 952 theorem le_A_exp: ∀n. A(2*n) ≤ (exp 2 (pred (2*n)))*A n.
 953 #n @(transitive_le ? (B(2*n)*A n))
 954   [@le_A_BA |@le_times [@le_B_exp |//]]
 955 qed.
 956
 957 theorem lt_4_to_le_A_exp: ∀n. 4 < n →
 958   A(2*n) ≤ exp 2 ((2*n)-2)*A n.
 959 #n #lt4n @(transitive_le ? (B(2*n)*A n))
 960   [@le_A_BA|@le_times [@(lt_4_to_le_B_exp … lt4n) |@le_n]]
 961 qed.
 962
 963 (* two technical lemmas *)
 964 lemma times_2_pred: ∀n. 2*(pred n) \le pred (2*n).
 965 #n cases n
 966   [@le_n|#m @monotonic_le_plus_r @le_n_Sn]
 967 qed.
 968
 969 lemma le_S_times_2: ∀n. O < n → S n ≤ 2*n.
 970 #n #posn elim posn
 971   [@le_n
 972   |#m #posm #Hind
 973    cut (2*(S m) = S(S(2*m))) [normalize <plus_n_Sm //] #Hcut >Hcut
 974    @le_S_S @(transitive_le … Hind) @le_n_Sn
 975   ]
 976 qed.
 977
 978 theorem le_A_exp1: ∀n.
 979   A(exp 2 n) ≤ exp 2 ((2*(exp 2 n)-(S(S n)))).
 980 #n elim n
 981   [@le_n
 982   |#n1 #Hind whd in ⊢ (?(?%)?); >commutative_times
 983    @(transitive_le ??? (le_A_exp ?))
 984    @(transitive_le ? (2\sup(pred (2*2^n1))*2^(2*2^n1-(S(S n1)))))
 985     [@monotonic_le_times_r //
 986     |<exp_plus_times @(le_exp … (lt_O_S ?))
 987      cut (S(S n1) ≤ 2*(exp 2 n1))
 988       [elim n1
 989         [@le_n
 990         |#n2 >commutative_times in ⊢ (%→?); #Hind1 @(transitive_le ? (2*(S(S n2))))
 991           [@le_S_times_2 @lt_O_S |@monotonic_le_times_r //]
 992         ]
 993       ] #Hcut
 994      @le_S_S_to_le cut(∀a,b. S a + b = S (a+b)) [//] #Hplus <Hplus >S_pred
 995       [>eq_minus_S_pred in ⊢ (??%); >S_pred
 996         [>plus_minus_commutative
 997           [@monotonic_le_minus_l
 998            cut (∀a. 2*a = a + a) [//] #times2 <times2
 999            @monotonic_le_times_r >commutative_times @le_n
1000           |@Hcut
1001           ]
1002         |@lt_plus_to_minus_r whd in ⊢ (?%?);
1003          @(lt_to_le_to_lt ? (2*(S(S n1))))
1004           [>(times_n_1 (S(S n1))) in ⊢ (?%?); >commutative_times
1005            @monotonic_lt_times_l [@lt_O_S |@le_n]
1006           |@monotonic_le_times_r whd in ⊢ (??%); //
1007           ]
1008         ]
1009       |whd >(times_n_1 1) in ⊢ (?%?); @le_times
1010         [@le_n_Sn |@lt_O_exp @lt_O_S]
1011       ]
1012     ]
1013   ]
1014 qed.
1015
1016 theorem monotonic_A: monotonic nat le A.
1017 #n #m #lenm elim lenm
1018   [@le_n
1019   |#n1 #len #Hind @(transitive_le … Hind)
1020    cut (∏_{p < S n1 | primeb p}(p^(log p n1))
1021           ≤∏_{p < S n1 | primeb p}(p^(log p (S n1))))
1022     [@le_pi #p #ltp #primep @le_exp
1023       [@prime_to_lt_O @primeb_true_to_prime //
1024       |@le_log [@prime_to_lt_SO @primeb_true_to_prime // | //]
1025       ]
1026     ] #Hcut
1027    >psi_def in ⊢ (??%); cases (true_or_false (primeb (S n1))) #Hc
1028     [>bigop_Strue in ⊢ (??%); [2://]
1029      >(times_n_1 (A n1)) >commutative_times @le_times
1030       [@lt_O_exp @lt_O_S |@Hcut]
1031     |>bigop_Sfalse in ⊢ (??%); //
1032     ]
1033   ]
1034 qed.
1035
1036 (*
1037 theorem le_A_exp2: \forall n. O < n \to
1038 A(n) \le (exp (S(S O)) ((S(S O)) * (S(S O)) * n)).
1039 intros.
1040 apply (trans_le ? (A (exp (S(S O)) (S(log (S(S O)) n)))))
1041   [apply monotonic_A.
1042    apply lt_to_le.
1043    apply lt_exp_log.
1044    apply le_n
1045   |apply (trans_le ? ((exp (S(S O)) ((S(S O))*(exp (S(S O)) (S(log (S(S O)) n)))))))
1046     [apply le_A_exp1
1047     |apply le_exp
1048       [apply lt_O_S
1049       |rewrite > assoc_times.apply le_times_r.
1050        change with ((S(S O))*((S(S O))\sup(log (S(S O)) n))≤(S(S O))*n).
1051        apply le_times_r.
1052        apply le_exp_log.
1053        assumption
1054       ]
1055     ]
1056   ]
1057 qed.
1058 *)
1059
1060 (* example *)
1061 example A_1: A 1 = 1. // qed.
1062
1063 example A_2: A 2 = 2. // qed.
1064
1065 example A_3: A 3 = 6. // qed.
1066
1067 example A_4: A 4 = 12. // qed.
1068
1069 (*
1070 (* a better result *)
1071 theorem le_A_exp3: \forall n. S O < n \to
1072 A(n) \le exp (pred n) (2*(exp 2 (2 * n)).
1073 intro.
1074 apply (nat_elim1 n).
1075 intros.
1076 elim (or_eq_eq_S m).
1077 elim H2
1078   [elim (le_to_or_lt_eq (S O) a)
1079     [rewrite > H3 in ⊢ (? % ?).
1080      apply (trans_le ? ((exp (S(S O)) ((S(S O)*a)))*A a))
1081       [apply le_A_exp
1082       |apply (trans_le ? (((S(S O)))\sup((S(S O))*a)*
1083          ((pred a)\sup((S(S O)))*((S(S O)))\sup((S(S O))*a))))
1084         [apply le_times_r.
1085          apply H
1086           [rewrite > H3.
1087            rewrite > times_n_SO in ⊢ (? % ?).
1088            rewrite > sym_times.
1089            apply lt_times_l1
1090             [apply lt_to_le.assumption
1091             |apply le_n
1092             ]
1093           |assumption
1094           ]
1095         |rewrite > sym_times.
1096          rewrite > assoc_times.
1097          rewrite < exp_plus_times.
1098          apply (trans_le ?
1099           (pred a\sup((S(S O)))*(S(S O))\sup(S(S O))*(S(S O))\sup((S(S O))*m)))
1100           [rewrite > assoc_times.
1101            apply le_times_r.
1102            rewrite < exp_plus_times.
1103            apply le_exp
1104             [apply lt_O_S
1105             |rewrite < H3.
1106              simplify.
1107              rewrite < plus_n_O.
1108              apply le_S.apply le_S.
1109              apply le_n
1110             ]
1111           |apply le_times_l.
1112            rewrite > times_exp.
1113            apply monotonic_exp1.
1114            rewrite > H3.
1115            rewrite > sym_times.
1116            cases a
1117             [apply le_n
1118             |simplify.
1119              rewrite < plus_n_Sm.
1120              apply le_S.
1121              apply le_n
1122             ]
1123           ]
1124         ]
1125       ]
1126     |rewrite < H4 in H3.
1127      simplify in H3.
1128      rewrite > H3.
1129      simplify.
1130      apply le_S_S.apply le_S_S.apply le_O_n
1131     |apply not_lt_to_le.intro.
1132      apply (lt_to_not_le ? ? H1).
1133      rewrite > H3.
1134      apply (le_n_O_elim a)
1135       [apply le_S_S_to_le.assumption
1136       |apply le_O_n
1137       ]
1138     ]
1139   |elim (le_to_or_lt_eq O a (le_O_n ?))
1140     [apply (trans_le ? (A ((S(S O))*(S a))))
1141       [apply monotonic_A.
1142        rewrite > H3.
1143        rewrite > times_SSO.
1144        apply le_n_Sn
1145       |apply (trans_le ? ((exp (S(S O)) ((S(S O)*(S a))))*A (S a)))
1146         [apply le_A_exp
1147         |apply (trans_le ? (((S(S O)))\sup((S(S O))*S a)*
1148            (a\sup((S(S O)))*((S(S O)))\sup((S(S O))*(S a)))))
1149           [apply le_times_r.
1150            apply H
1151             [rewrite > H3.
1152              apply le_S_S.
1153              simplify.
1154              rewrite > plus_n_SO.
1155              apply le_plus_r.
1156              rewrite < plus_n_O.
1157              assumption
1158             |apply le_S_S.assumption
1159             ]
1160           |rewrite > sym_times.
1161            rewrite > assoc_times.
1162            rewrite < exp_plus_times.
1163            apply (trans_le ?
1164             (a\sup((S(S O)))*(S(S O))\sup(S(S O))*(S(S O))\sup((S(S O))*m)))
1165             [rewrite > assoc_times.
1166              apply le_times_r.
1167              rewrite < exp_plus_times.
1168              apply le_exp
1169               [apply lt_O_S
1170               |rewrite > times_SSO.
1171                rewrite < H3.
1172                simplify.
1173                rewrite < plus_n_Sm.
1174                rewrite < plus_n_O.
1175                apply le_n
1176               ]
1177             |apply le_times_l.
1178              rewrite > times_exp.
1179              apply monotonic_exp1.
1180              rewrite > H3.
1181              rewrite > sym_times.
1182              apply le_n
1183             ]
1184           ]
1185         ]
1186       ]
1187     |rewrite < H4 in H3.simplify in H3.
1188      apply False_ind.
1189      apply (lt_to_not_le ? ? H1).
1190      rewrite > H3.
1191      apply le_
1192     ]
1193   ]
1194 qed.
1195 *)
1196
1197 theorem le_A_exp4: ∀n. 1 < n →
1198   A(n) ≤ (pred n)*exp 2 ((2 * n) -3).
1199 #n @(nat_elim1 n)
1200 #m #Hind cases (even_or_odd m)
1201 #a * #Hm >Hm #Hlt
1202   [cut (0<a)
1203     [cases a in Hlt;
1204       [whd in ⊢ (??%→?); #lt10 @False_ind @(absurd ? lt10 (not_le_Sn_O 1))
1205     |#b #_ //]
1206     ] #Hcut
1207    cases (le_to_or_lt_eq … Hcut) #Ha
1208     [@(transitive_le ? (exp 2 (pred(2*a))*A a))
1209       [@le_A_exp
1210       |@(transitive_le ? (2\sup(pred(2*a))*((pred a)*2\sup((2*a)-3))))
1211         [@monotonic_le_times_r @(Hind ?? Ha)
1212          >Hm >(times_n_1 a) in ⊢ (?%?); >commutative_times
1213          @monotonic_lt_times_l [@lt_to_le // |@le_n]
1214         |<Hm <associative_times >commutative_times in ⊢ (?(?%?)?);
1215          >associative_times; @le_times
1216           [>Hm cases a[@le_n|#b normalize @le_plus_n_r]
1217           |<exp_plus_times @le_exp
1218             [@lt_O_S
1219             |@(transitive_le ? (m+(m-3)))
1220               [@monotonic_le_plus_l //
1221               |normalize <plus_n_O >plus_minus_commutative
1222                 [@le_n
1223                 |>Hm @(transitive_le ? (2*2) ? (le_n_Sn 3))
1224                  @monotonic_le_times_r //
1225                 ]
1226               ]
1227             ]
1228           ]
1229         ]
1230       ]
1231     |<Ha normalize @le_n
1232     ]
1233   |cases (le_to_or_lt_eq O a (le_O_n ?)) #Ha
1234     [@(transitive_le ? (A (2*(S a))))
1235       [@monotonic_A >Hm normalize <plus_n_Sm @le_n_Sn
1236       |@(transitive_le … (le_A_exp ?) )
1237        @(transitive_le ? ((2\sup(pred (2*S a)))*(a*(exp 2 ((2*(S a))-3)))))
1238         [@monotonic_le_times_r @Hind
1239           [>Hm @le_S_S >(times_n_1 a) in ⊢ (?%?); >commutative_times
1240            @monotonic_lt_times_l //
1241           |@le_S_S //
1242           ]
1243         |cut (pred (S (2*a)) = 2*a) [//] #Spred >Spred
1244          cut (pred (2*(S a)) = S (2 * a)) [normalize //] #Spred1 >Spred1
1245          cut (2*(S a) = S(S(2*a))) [normalize <plus_n_Sm //] #times2
1246          cut (exp 2 (2*S a -3) = 2*(exp 2 (S(2*a) -3)))
1247           [>(commutative_times 2) in ⊢ (???%); >times2 >minus_Sn_m [%]
1248            @le_S_S >(times_n_1 2) in ⊢ (?%?); @monotonic_le_times_r @Ha
1249           ] #Hcut >Hcut
1250          <associative_times in ⊢ (? (? ? %) ?); <associative_times
1251          >commutative_times in ⊢ (? (? % ?) ?);
1252          >commutative_times in ⊢ (? (? (? % ?) ?) ?);
1253          >associative_times @monotonic_le_times_r
1254          <exp_plus_times @(le_exp … (lt_O_S ?))
1255          >plus_minus_commutative
1256           [normalize >(plus_n_O (a+(a+0))) in ⊢ (?(?(??%)?)?); @le_n
1257           |@le_S_S >(times_n_1 2) in ⊢ (?%?); @monotonic_le_times_r @Ha
1258           ]
1259         ]
1260       ]
1261     |@False_ind <Ha in Hlt; normalize #Hfalse @(absurd ? Hfalse) //
1262     ]
1263   ]
1264 qed.
1265
1266 theorem le_n_8_to_le_A_exp: ∀n. n ≤ 8 →
1267   A(n) ≤ exp 2 ((2 * n) -3).
1268 #n cases n
1269   [#_ @le_n
1270   |#n1 cases n1
1271     [#_ @le_n
1272     |#n2 cases n2
1273       [#_ @le_n
1274       |#n3 cases n3
1275         [#_ @leb_true_to_le //
1276         |#n4 cases n4
1277           [#_ @leb_true_to_le //
1278           |#n5 cases n5
1279             [#_ @leb_true_to_le //
1280             |#n6 cases n6
1281               [#_ @leb_true_to_le //
1282               |#n7 cases n7
1283                 [#_ @leb_true_to_le //
1284                 |#n8 cases n8
1285                   [#_ @leb_true_to_le //
1286                   |#n9 #H @False_ind @(absurd ?? (lt_to_not_le ?? H))
1287                    @leb_true_to_le //
1288                   ]
1289                 ]
1290               ]
1291             ]
1292           ]
1293         ]
1294       ]
1295     ]
1296   ]
1297 qed.
1298
1299 theorem le_A_exp5: ∀n. A(n) ≤ exp 2 ((2 * n) -3).
1300 #n @(nat_elim1 n) #m #Hind
1301 cases (decidable_le 9 m)
1302   [#lem cases (even_or_odd m) #a * #Hm
1303     [>Hm in ⊢ (?%?); @(transitive_le … (le_A_exp ?))
1304      @(transitive_le ? (2\sup(pred(2*a))*(2\sup((2*a)-3))))
1305       [@monotonic_le_times_r @Hind >Hm >(times_n_1 a) in ⊢ (?%?);
1306        >commutative_times @(monotonic_lt_times_l  … (le_n ?))
1307        @(transitive_lt ? 3)
1308         [@lt_O_S |@(le_times_to_le 2) [@lt_O_S |<Hm @lt_to_le @lem]]
1309       |<Hm <exp_plus_times @(le_exp … (lt_O_S ?))
1310        whd in match (times 2 m); >commutative_times <times_n_1
1311        <plus_minus_commutative
1312         [@monotonic_le_plus_l @le_pred_n
1313         |@(transitive_le … lem) @leb_true_to_le //
1314         ]
1315       ]
1316     |@(transitive_le ? (A (2*(S a))))
1317       [@monotonic_A >Hm normalize <plus_n_Sm @le_n_Sn
1318       |@(transitive_le ? ((exp 2 ((2*(S a))-2))*A (S a)))
1319         [@lt_4_to_le_A_exp @le_S_S
1320          @(le_times_to_le 2)[@le_n_Sn|@le_S_S_to_le <Hm @lem]
1321         |@(transitive_le ? ((2\sup((2*S a)-2))*(exp 2 ((2*(S a))-3))))
1322           [@monotonic_le_times_r @Hind >Hm @le_S_S
1323            >(times_n_1 a) in ⊢ (?%?);
1324            >commutative_times @(monotonic_lt_times_l  … (le_n ?))
1325            @(transitive_lt ? 3)
1326             [@lt_O_S |@(le_times_to_le 2) [@lt_O_S |@le_S_S_to_le <Hm @lem]]
1327           |cut (∀a. 2*(S a) = S(S(2*a))) [normalize #a <plus_n_Sm //] #times2
1328            >times2 <Hm <exp_plus_times @(le_exp … (lt_O_S ?))
1329            cases m
1330             [@le_n
1331             |#n1 cases n1
1332               [@le_n
1333               |#n2 normalize <minus_n_O <plus_n_O <plus_n_Sm
1334                normalize <minus_n_O <plus_n_Sm @le_n
1335               ]
1336             ]
1337           ]
1338         ]
1339       ]
1340     ]
1341   |#H @le_n_8_to_le_A_exp @le_S_S_to_le @not_le_to_lt //
1342   ]
1343 qed.
1344
1345 theorem le_exp_Al:∀n. O < n → exp 2 n ≤ A (2 * n).
1346 #n #posn @(transitive_le ? ((exp 2 (2*n))/(2*n)))
1347   [@le_times_to_le_div
1348     [>(times_n_O O) in ⊢ (?%?); @lt_times [@lt_O_S|//]
1349     |normalize in ⊢ (??(??%)); < plus_n_O >exp_plus_times
1350      @le_times [2://] elim posn [//]
1351      #m #le1m #Hind whd in ⊢ (??%); >commutative_times in ⊢ (??%);
1352      @monotonic_le_times_r @(transitive_le … Hind)
1353      >(times_n_1 m) in ⊢ (?%?); >commutative_times
1354      @(monotonic_lt_times_l  … (le_n ?)) @le1m
1355     ]
1356   |@le_times_to_le_div2
1357     [>(times_n_O O) in ⊢ (?%?); @lt_times [@lt_O_S|//]
1358     |@(transitive_le ? ((B (2*n)*(2*n))))
1359       [<commutative_times in ⊢ (??%); @le_exp_B //
1360       |@le_times [@le_B_A|@le_n]
1361       ]
1362     ]
1363   ]
1364 qed.
1365
1366 theorem le_exp_A2:∀n. 1 < n → exp 2 (n / 2) \le A n.
1367 #n #lt1n @(transitive_le ? (A(n/2*2)))
1368   [>commutative_times @le_exp_Al
1369    cases (le_to_or_lt_eq ? ? (le_O_n (n/2))) [//]
1370    #Heq @False_ind @(absurd ?? (lt_to_not_le ?? lt1n))
1371    >(div_mod n 2) <Heq whd in ⊢ (?%?);
1372    @le_S_S_to_le @(lt_mod_m_m n 2) @lt_O_S
1373   |@monotonic_A >(div_mod n 2) in ⊢ (??%); @le_plus_n_r
1374   ]
1375 qed.
1376
1377 theorem eq_sigma_pi_SO_n: ∀n.∑_{i < n} 1 = n.
1378 #n elim n //
1379 qed.
1380
1381 theorem leA_prim: ∀n.
1382   exp n (prim n) \le A n * ∏_{p < S n | primeb p} p.
1383 #n <(exp_sigma (S n) n primeb) <times_pi @le_pi
1384 #p #ltp #primep @lt_to_le @lt_exp_log
1385 @prime_to_lt_SO @primeb_true_to_prime //
1386 qed.
1387
1388 theorem le_prim_log : ∀n,b. 1 < b →
1389   log b (A n) ≤ prim n * (S (log b n)).
1390 #n #b #lt1b @(transitive_le … (log_exp1 …)) [@le_log // | //]
1391 qed.
1392
1393 (*********************** the inequalities ***********************)
1394 lemma exp_Sn: ∀b,n. exp b (S n) = b * (exp b n).
1395 normalize //
1396 qed.
1397
1398 theorem le_exp_priml: ∀n. O < n →
1399   exp 2 (2*n) ≤ exp (2*n) (S(prim (2*n))).
1400 #n #posn @(transitive_le ? (((2*n*(B (2*n))))))
1401   [@le_exp_B //
1402   |>exp_Sn @monotonic_le_times_r @(transitive_le ? (A (2*n)))
1403     [@le_B_A |@le_Al]
1404   ]
1405 qed.
1406
1407 theorem le_exp_prim4l: ∀n. O < n →
1408   exp 2 (S(4*n)) ≤ exp (4*n) (S(prim (4*n))).
1409 #n #posn @(transitive_le ? (2*(4*n*(B (4*n)))))
1410   [>exp_Sn @monotonic_le_times_r
1411    cut (4*n = 2*(2*n)) [<associative_times //] #Hcut
1412    >Hcut @le_exp_B @lt_to_le whd >(times_n_1 2) in ⊢ (?%?);
1413    @monotonic_le_times_r //
1414   |>exp_Sn <associative_times >commutative_times in ⊢ (?(?%?)?);
1415    >associative_times @monotonic_le_times_r @(transitive_le ? (A (4*n)))
1416     [@le_B_A4 // |@le_Al]
1417   ]
1418 qed.
1419
1420 theorem le_priml: ∀n. O < n →
1421   2*n ≤ (S (log 2 (2*n)))*S(prim (2*n)).
1422 #n #posn <(eq_log_exp 2 (2*n) ?) in ⊢ (?%?);
1423   [@(transitive_le ? ((log 2) (exp (2*n) (S(prim (2*n))))))
1424     [@le_log [@le_n |@le_exp_priml //]
1425     |>commutative_times in ⊢ (??%); @log_exp1 @le_n
1426     ]
1427   |@le_n
1428   ]
1429 qed.
1430
1431 theorem le_exp_primr: ∀n.
1432   exp n (prim n) ≤ exp 2 (2*(2*n-3)).
1433 #n @(transitive_le ? (exp (A n) 2))
1434   [>exp_Sn >exp_Sn whd in match (exp ? 0); <times_n_1 @leA_r2
1435   |>commutative_times <exp_exp_times @le_exp1 [@lt_O_S |@le_A_exp5]
1436   ]
1437 qed.
1438
1439 (* bounds *)
1440 theorem le_primr: ∀n. 1 < n → prim n \le 2*(2*n-3)/log 2 n.
1441 #n #lt1n @le_times_to_le_div
1442   [@lt_O_log //
1443   |@(transitive_le ? (log 2 (exp n (prim n))))
1444     [>commutative_times @log_exp2
1445       [@le_n |@lt_to_le //]
1446     |<(eq_log_exp 2 (2*(2*n-3))) in ⊢ (??%);
1447       [@le_log [@le_n |@le_exp_primr]
1448       |@le_n
1449       ]
1450     ]
1451   ]
1452 qed.
1453
1454 theorem le_priml1: ∀n. O < n →
1455   2*n/((log 2 n)+2) - 1 ≤ prim (2*n).
1456 #n #posn @le_plus_to_minus @le_times_to_le_div2
1457   [>commutative_plus @lt_O_S
1458   |>commutative_times in ⊢ (??%); <plus_n_Sm <plus_n_Sm in ⊢ (??(??%));
1459    <plus_n_O <commutative_plus <log_exp
1460     [@le_priml // | //| @le_n]
1461   ]
1462 qed.
1463
1464
1465
1466