matita/matita/lib/arithmetics/chebyshev/chebyshev_psi.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/sigma_pi.ma".
  14
  15 (* (prim n) counts the number of prime numbers up to n included *)
  16 definition prim ≝ λn. ∑_{i < S n | primeb i} 1.
  17
  18 lemma le_prim_n: ∀n. prim n ≤ n.
  19 #n elim n // -n #n #H
  20 whd in ⊢ (?%?); cases (primeb (S n)) whd in ⊢ (?%?);
  21   [@le_S_S @H |@le_S @H]
  22 qed.
  23
  24 lemma not_prime_times_2: ∀n. 1 < n → ¬prime (2*n).
  25 #n #ltn % * #H #H1 @(absurd (2 = 2*n))
  26   [@H1 // %{n} //
  27   |@lt_to_not_eq >(times_n_1 2) in ⊢ (?%?); @monotonic_lt_times_r //
  28   ]
  29 qed.
  30
  31 theorem eq_prim_prim_pred: ∀n. 1 < n →
  32   prim (2*n) = prim (pred (2*n)).
  33 #n #ltn
  34 lapply (S_pred (2*n) ?) [>(times_n_1 0) in ⊢ (?%?); @lt_times //] #H2n
  35 lapply (not_prime_times_2 n ltn) #notp2n
  36 whd in ⊢ (??%?); >(not_prime_to_primeb_false … notp2n) whd in ⊢ (??%?);
  37 <H2n in ⊢ (??%?); %
  38 qed.
  39
  40 theorem le_prim_n1: ∀n. 4 ≤ n →
  41   prim (S(2*n)) ≤ n.
  42 #n #le4 elim le4 -le4
  43   [@le_n
  44   |#m #le4 cut (S (2*m) = pred (2*(S m))) [normalize //] #Heq >Heq
  45    <eq_prim_prim_pred [2: @le_S_S @(transitive_le … le4) //]
  46    #H whd in ⊢ (?%?); cases (primeb (S (2*S m)))
  47     [@le_S_S @H |@le_S @H]
  48   ]
  49 qed.
  50
  51 (* usefull to kill a successor in bertrand *)
  52 theorem le_prim_n2: ∀n. 7 ≤ n → prim (S(2*n)) ≤ pred n.
  53 #n #le7 elim le7 -le7
  54   [@le_n
  55   |#m #le7 cut (S (2*m) = pred (2*(S m))) [normalize //] #Heq >Heq
  56    <eq_prim_prim_pred [2: @le_S_S @(transitive_le … le7) //]
  57    #H whd in ⊢ (?%?);
  58    whd in ⊢ (??%); <(S_pred m) in ⊢ (??%); [2: @(transitive_le … le7) //]
  59    cases (primeb (S (2*S m))) [@le_S_S @H |@le_S @H]
  60   ]
  61 qed.
  62
  63 lemma even_or_odd: ∀n.∃a.n=2*a ∨ n = S(2*a).
  64 #n elim n -n
  65   [%{0} %1 %
  66   |#n * #a * #Hn [%{a} %2 @eq_f @Hn | %{(S a)} %1 >Hn normalize //
  67   ]
  68 qed.
  69
  70 (* la prova potrebbe essere migliorata *)
  71 theorem le_prim_n3: ∀n. 15 ≤ n →
  72   prim n ≤ pred (n/2).
  73 #n #len cases (even_or_odd (pred n)) #a * #Hpredn
  74   [cut (n = S (2*a)) [<Hpredn @sym_eq @S_pred @(transitive_le … len) //] #Hn
  75    >Hn @(transitive_le ? (pred a))
  76     [@le_prim_n2 @(le_times_to_le 2) [//|@le_S_S_to_le <Hn @len]
  77     |@monotonic_pred @le_times_to_le_div //
  78     ]
  79   |cut (n = (2*S a))
  80     [normalize normalize in Hpredn:(???%); <plus_n_Sm <Hpredn @sym_eq @S_pred
  81      @(transitive_le … len) //] #Hn
  82    >Hn @(transitive_le ? (pred a))
  83     [>eq_prim_prim_pred
  84       [2:@(lt_times_n_to_lt_r 2) <Hn @(transitive_le … len) //]
  85      <Hn >Hpredn @le_prim_n2 @le_S_S_to_le @(lt_times_n_to_lt_r 2) <Hn @len
  86     |@monotonic_pred @le_times_to_le_div //
  87     ]
  88   ]
  89 qed.
  90
  91 (* This is chebishev psi function *)
  92 definition Psi: nat → nat ≝
  93   λn.∏_{p < S n | primeb p} (exp p (log p n)).
  94
  95 definition psi_def : ∀n.
  96   Psi n = ∏_{p < S n | primeb p} (exp p (log p n)).
  97 // qed.
  98
  99 theorem le_Psil1: ∀n.
 100   Psi n ≤ ∏_{p < S n | primeb p} n.
 101 #n cases n [@le_n |#m @le_pi #i #_ #_ @le_exp_log //]
 102 qed.
 103
 104 theorem le_Psil: ∀n. Psi n ≤ exp n (prim n).
 105 #n <exp_sigma @le_Psil1
 106 qed.
 107
 108 theorem lePsi_r2: ∀n.
 109   exp n (prim n) ≤ Psi n * Psi n.
 110 #n elim (le_to_or_lt_eq ?? (le_O_n n)) #Hn
 111   [<(exp_sigma (S n) n primeb) <times_pi
 112    @le_pi #i #lti #primei
 113    cut (1<n)
 114      [@(lt_to_le_to_lt … (le_S_S_to_le … lti)) @prime_to_lt_SO
 115       @primeb_true_to_prime //] #lt1n
 116    <exp_plus_times
 117    @(transitive_le ? (exp i (S(log i n))))
 118     [@lt_to_le @lt_exp_log @prime_to_lt_SO @primeb_true_to_prime //
 119     |@le_exp
 120       [@prime_to_lt_O @primeb_true_to_prime //
 121       |>(plus_n_O (log i n)) in ⊢ (?%?); >plus_n_Sm
 122        @monotonic_le_plus_r @lt_O_log //
 123        @le_S_S_to_le //
 124       ]
 125     ]
 126   |<Hn @le_n
 127   ]
 128 qed.
 129
 130 (* an equivalent formulation for psi *)
 131 definition Psi': nat → nat ≝
 132 λn. ∏_{p < S n | primeb p} (∏_{i < log p n} p).
 133
 134 lemma Psidef: ∀n. Psi' n = ∏_{p < S n | primeb p} (∏_{i < log p n} p).
 135 // qed-.
 136
 137 theorem eq_Psi_Psi': ∀n.Psi n = Psi' n.
 138 #n @same_bigop // #i #lti #primebi
 139 @(trans_eq ? ? (exp i (∑_{x < log i n} 1)))
 140   [@eq_f @sym_eq @sigma_const
 141   |@sym_eq @exp_sigma
 142   ]
 143 qed.