matita/matita/lib/arithmetics/chebyshev/chebyshev.ma.old

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