matita/library/nat/chebyshev_thm.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15
  16
  17 include "nat/neper.ma".
  18
  19 definition C \def \lambda n.pi_p (S n) primeb
  20   (\lambda p.match (leb (p*p) n) with
  21     [ true => p
  22     | false => S (n/p) ]).
  23
  24 theorem asdasd : \forall n. exp n (prim n) \leq (A n)*(C n).
  25 intro;unfold prim;rewrite < exp_sigma_p;unfold A;unfold C;rewrite < times_pi_p;
  26 apply le_pi_p;intros;
  27 apply (bool_elim ? (leb (i*i) n));intro
  28     [change in \vdash (? ? (? ? %)) with i;
  29      rewrite > sym_times;change in \vdash (? ? %) with (exp i (S (log i n)));
  30      apply lt_to_le;apply lt_exp_log;apply prime_to_lt_SO;
  31      apply primeb_true_to_prime;assumption
  32     |change in \vdash (? ? (? ? %)) with (S (n/i));
  33      cut (log i n = S O)
  34        [rewrite > Hcut;rewrite < exp_n_SO;
  35         apply lt_to_le;rewrite > sym_times;apply lt_div_S;apply prime_to_lt_O;
  36         apply primeb_true_to_prime;assumption
  37        |apply antisymmetric_le
  38          [apply le_S_S_to_le;apply not_le_to_lt;intro;
  39           apply (leb_false_to_not_le ? ? H2);apply (trans_le ? (exp i (log i n)))
  40            [rewrite < exp_SSO;apply le_exp;
  41               [apply prime_to_lt_O;
  42                apply primeb_true_to_prime;assumption
  43               |assumption]
  44            |apply le_exp_log;apply (trans_le ? i)
  45               [apply prime_to_lt_O;apply primeb_true_to_prime;assumption
  46               |apply le_S_S_to_le;assumption]]
  47          |apply (trans_le ? (log i i))
  48            [rewrite > log_n_n;
  49               [apply le_n
  50               |apply prime_to_lt_SO;apply primeb_true_to_prime;assumption]
  51            |apply le_log
  52               [apply prime_to_lt_SO;apply primeb_true_to_prime;assumption
  53               |apply le_S_S_to_le;assumption]]]]]
  54 qed.
  55
  56 definition theta_pi \def
  57   \lambda n.pi_p (S n) primeb (\lambda p.p).
  58
  59 definition C1 \def
  60   \lambda n. pi_p (S n) (\lambda x. (primeb x) \land (leb (x*x) n)) (\lambda p.p).
  61
  62 definition C2 \def
  63   \lambda n. pi_p (S n) (\lambda x. (primeb x) \land (leb (S n) (x*x))) (\lambda p.S (n/p)).
  64
  65
  66 theorem jj : \forall n.C n = C1 n * C2 n.
  67 intro;unfold C;unfold C1;unfold C2;
  68 cut (\forall m.pi_p (S n) primeb
  69 (λp:nat
  70  .match leb (p*p) m in bool return λb:bool.nat with
  71   [true⇒p|false⇒S (m/p)])
  72 =pi_p (S n) (λx:nat.primeb x∧leb (x*x) m) (λp:nat.p)
  73  *pi_p (S n) (λx:nat.primeb x∧leb (S m) (x*x)) (λp:nat.S (m/p)))
  74   [apply Hcut;
  75   |intro;elim n 0
  76      [simplify;reflexivity
  77      |intro;apply (bool_elim ? (primeb (S n1)))
  78         [intros;rewrite > true_to_pi_p_Sn
  79            [apply (bool_elim ? (leb ((S n1)*(S n1)) m))
  80               [intro;rewrite > true_to_pi_p_Sn in \vdash (? ? ? (? % ?))
  81                  [rewrite > false_to_pi_p_Sn in \vdash (? ? ? (? ? %))
  82                     [rewrite > H1;rewrite > H2;rewrite < assoc_times;reflexivity
  83                     |rewrite > H;lapply (leb_true_to_le ? ? H2);
  84                      lapply (le_to_not_lt ? ? Hletin);
  85                      apply (bool_elim ? (leb (S m) (S n1 * S n1)))
  86                        [intro;apply False_ind;apply Hletin1;
  87                         apply leb_true_to_le;assumption
  88                        |intro;reflexivity]]
  89                  |rewrite > H2;rewrite > H;reflexivity]
  90               |intro;rewrite > false_to_pi_p_Sn in \vdash (? ? ? (? % ?))
  91                  [rewrite > true_to_pi_p_Sn in \vdash (? ? ? (? ? %))
  92                     [rewrite > H1;rewrite < assoc_times;
  93                      rewrite > sym_times in \vdash (? ? (? % ?) ?);
  94                      rewrite > assoc_times;reflexivity
  95                     |rewrite > H;
  96                      change in \vdash (? ? % ?) with (leb (S m) (S n1* S n1));
  97                      apply le_to_leb_true;apply not_le_to_lt;
  98                      apply leb_false_to_not_le;assumption]
  99                  |rewrite > H;rewrite > H2;reflexivity]]
 100            |assumption]
 101         |intros;rewrite > false_to_pi_p_Sn
 102            [rewrite > false_to_pi_p_Sn in \vdash (? ? ? (? % ?))
 103               [rewrite > false_to_pi_p_Sn in \vdash (? ? ? (? ? %))
 104                  [rewrite > H1;reflexivity
 105                  |rewrite > H;elim (leb (S m) (S n1*S n1));simplify;reflexivity]
 106               |rewrite > H;elim (leb (S n1*S n1) m);simplify;reflexivity]
 107            |assumption]]]]
 108 qed.
 109
 110 theorem log_pi_p : \forall n,b,f,g.S O < b \to
 111   log b (pi_p n f g) \leq
 112     (sigma_p n f (\lambda x.S O)) + (sigma_p n f (\lambda x.log b (g x))).
 113 intros;elim n
 114   [simplify;rewrite < times_n_SO;apply (leb_elim b (S O))
 115     [intro;elim (lt_to_not_le ? ? H);assumption
 116     |intro;simplify;apply le_n]
 117   |apply (bool_elim ? (f n1))
 118     [intro;rewrite > true_to_pi_p_Sn
 119        [rewrite > true_to_sigma_p_Sn
 120           [rewrite > true_to_sigma_p_Sn
 121              [apply (trans_le ? (S ((log b (g n1)) + (log b (pi_p n1 f g)))))
 122                 [apply log_times;assumption
 123                 |rewrite > assoc_plus;
 124                  change in \vdash (? ? %) with (S (sigma_p n1 f (\lambda x.S O)+(log b (g n1)+sigma_p n1 f (\lambda x.log b (g x)))));
 125                  apply le_S_S;rewrite < assoc_plus;
 126                  rewrite > sym_plus in \vdash (? ? (? % ?));
 127                  rewrite > assoc_plus;apply le_plus;
 128                    [apply le_n]]]]]
 129      assumption
 130     |intro;rewrite > false_to_pi_p_Sn
 131        [rewrite > false_to_sigma_p_Sn
 132           [rewrite > false_to_sigma_p_Sn]]
 133      assumption]]
 134 qed.
 135
 136 axiom daemon : False.
 137 (*
 138 lemma lt_log_to_lt : \forall b,m,n.S O < b \to log b m < log b n \to m < n.
 139 intros;apply not_le_to_lt;intro;elim (le_to_not_lt ? ? (le_log ? ? ? H H2));
 140 assumption.
 141 qed.
 142
 143 theorem ababbs: \forall n,a,b.S O < b \to O < n \to n < exp b a \to log b n < a.
 144 intros;unfold log;apply not_le_to_lt;intro;apply (lt_to_not_le ? ? H2);
 145 elim (le_to_or_lt_eq ? ? H3)
 146   [apply lt_to_le;apply (lt_log_to_lt b ? ? H);rewrite > eq_log_exp;assumption
 147   |apply (trans_le ? (exp b (log b n)))
 148      [rewrite < H4;apply le_n
 149      |apply le_exp_log;assumption]]
 150 qed.
 151
 152 theorem exp_exp_to_log : \forall b,n,k.S O < b \to
 153 exp b k \leq n \to n < exp b (S k) \to log b n = k.
 154 intros;unfold log;lapply (ababbs ? ? ? H ? H2)
 155   [apply (trans_le ? ? ? ? H1);apply lt_O_exp
 156   |unfold log in Hletin;lapply (le_to_leb_true ? ? H1);
 157    lapply (f_m_to_le_max (λx:nat.leb ((b)\sup(x)) n) n ? ? Hletin1)
 158      [
 159   elim (le_to_or_lt_eq ? ? (le_S_S_to_le ? ? Hletin))
 160      [unfold log in H3;
 161 ]]elim daemon.
 162 qed.
 163
 164 theorem xxx_log : \forall a,b.S O < b \to O < a \to log b (b*a) = S (log b a).
 165 intros 3;elim a
 166   [elim (not_le_Sn_O ? H1);
 167   |apply (inj_exp_r b)
 168      [assumption
 169      |*)
 170
 171 theorem le_log_C2_sigma_p : \forall n,b. S O < b \to
 172 log b (C2 n) \leq
 173 (sigma_p (S n) (\lambda x.(primeb x) \land (leb (S n) (x*x))) (\lambda x.S O)) +
 174 (prim n + (((sigma_p n (\lambda x.leb (S n) (x*x)) (\lambda i.prim i * S (n!/i)))
 175   *(S (log b 3)))/n!)).
 176 intros;unfold C2;
 177 apply (trans_le ? (sigma_p (S n) (λx:nat.primeb x∧leb (S n) (x*x)) (λx:nat.1)
 178 +sigma_p (S n) (λx:nat.primeb x∧leb (S n) (x*x))
 179  (λi.log b (S (n/i)))))
 180   [apply log_pi_p;assumption
 181   |apply le_plus
 182      [apply le_n
 183      |apply (trans_le ? (sigma_p (S n) (λx:nat.primeb x∧leb (S n) (x*x)) (λi:nat.S (log b (n/i)))))
 184         [apply le_sigma_p;intros;cut (log b (b*(n/i)) = S (log b (n/i)))
 185            [rewrite < Hcut;apply le_log
 186               [assumption
 187               |elim H
 188                  [rewrite < times_SSO_n;change in \vdash (? % ?) with (S O + (n/i));
 189                   apply le_plus;
 190                     [apply le_times_to_le_div
 191                        [apply (prime_to_lt_O i (primeb_true_to_prime ? (andb_true_true ? ? H2)));
 192                        |rewrite < times_n_SO;apply le_S_S_to_le;assumption]
 193                     |apply le_n]
 194                  |apply (trans_le ? ? ? H4);apply le_times_l;apply le_S;apply le_n]]
 195            |rewrite > exp_n_SO in ⊢ (? ? (? ? (? % ?)) ?);
 196             rewrite > log_exp;
 197               [reflexivity
 198               |assumption
 199               |apply le_times_to_le_div;
 200                  [apply (prime_to_lt_O i (primeb_true_to_prime ? (andb_true_true ? ? H2)));
 201                  |rewrite < times_n_SO;apply le_S_S_to_le;assumption]]]
 202         |change in ⊢ (? (? ? ? (λi:?.%)) ?) with ((S O) + (log b (n/i)));
 203          rewrite > (sigma_p_plus_1 ? (\lambda x.S O));
 204          apply le_plus
 205            [unfold prim;apply le_sigma_p1;intros;elim (leb (S n) (i*i));
 206               [rewrite > andb_sym;apply le_n
 207               |rewrite > andb_sym;apply le_O_n]
 208            |apply sigma_p_log_div;assumption]]]]
 209 qed.
 210
 211 lemma le_prim_n_stima : \forall n,b. S O < b \to b \leq n \to
 212 prim n \leq (S (((S (S (S (S O))))*(S (log b (pred n)))) +
 213               ((S (S (S (S O))))*n)))/(log b n).
 214 (* la stima del secondo addendo è ottenuta considerando che
 215    logreale 2 è sempre <= 1 (si dimostra per casi: b = 2, b > 2) *)
 216 intros;apply le_times_to_le_div;
 217   [apply lt_O_log;
 218      [apply (trans_le ? b)
 219         [apply lt_to_le;assumption
 220         |assumption]
 221      |assumption]
 222   |apply (trans_le ? (log b (exp n (prim n))))
 223      [rewrite > sym_times;apply log_exp2
 224         [assumption
 225         |apply (trans_le ? b ? ? H1);apply lt_to_le;assumption]
 226      |apply (trans_le ? (log b ((exp (pred n) (S (S (S (S O)))))
 227                                *(exp (S (S O)) ((S (S (S (S O))))*n)))))
 228         [apply le_log
 229            [assumption
 230            |apply le_exp_primr;apply (trans_le ? ? ? H H1)]
 231         |apply (trans_le ? (S ((log b (exp (pred n) (S (S (S (S O)))))) +
 232                               (log b (exp (S (S O)) ((S (S (S (S O))))*n))))))
 233            [apply log_times;assumption
 234            |apply le_S_S;apply le_plus
 235               [apply log_exp1;assumption
 236               |cases H
 237                  [rewrite > times_n_SO in \vdash (? (? ? %) ?);
 238                   rewrite > log_exp
 239                     [rewrite < plus_n_O;apply le_n
 240                     |apply le_n
 241                     |apply le_n]
 242                  |apply (trans_le ? (((S (S (S (S O))))*n)*(S (log (S m) (S (S O))))))
 243                     [apply log_exp1;apply le_S;assumption
 244                     |rewrite > times_n_SO in \vdash (? ? %);
 245                      apply le_times_r;apply le_S_S;
 246                      rewrite > lt_to_log_O
 247                        [apply le_n
 248                        |apply lt_O_S
 249                        |apply le_S_S;assumption]]]]]]]]
 250 qed.
 251
 252 (*
 253
 254 theorem le_log_C2_stima : \forall n,b. S O < b \to
 255 log b (C2 n) \leq
 256 (sigma_p (S n) (\lambda x.(primeb x) \land (leb (S n) (x*x))) (\lambda x.S O)) +
 257 (((S (((S (S (S (S O))))*(S (log b (pred n)))) +
 258               ((S (S (S (S O))))*n)))/(log b n)) +
 259  (((sigma_p n (\lambda x.leb (S n) (x*x))
 260               (\lambda i.((S (((S (S (S (S O))))*(S (log b (pred n)))) +
 261               ((S (S (S (S O))))*n)))/(log b n))* S (n!/i)))
 262   *(S (log b 3)))/n!)).
 263 elim daemon.
 264
 265 theorem le_log_C2_sigma_p : \forall n,b. S O < b \to
 266 log b (C2 n) \leq
 267 (sigma_p (S n) (\lambda x.(primeb x) \land (leb (S n) (x*x))) (\lambda x.S O)) +
 268 (sigma_p (S n) (\lambda x.(primeb x) \land (leb (S n) (x*x)))
 269    (\lambda p.(sigma_p (n+p) (\lambda i.leb p i)
 270        (\lambda i.S ((n+p)!/i*(S (log b 3)))))/(n+p)!)).
 271 intros;unfold C2;
 272 apply (trans_le ? (sigma_p (S n) (λx:nat.primeb x∧leb (S n) (x*x)) (λx:nat.1)
 273 +sigma_p (S n) (λx:nat.primeb x∧leb (S n) (x*x))
 274  (λi.log b (S (n/i)))))
 275   [apply log_pi_p;assumption
 276   |apply le_plus
 277      [apply le_n
 278      |apply le_sigma_p;intros;cut (S (n/i) = (n+i)/i)
 279         [rewrite > Hcut;apply le_log_div_sigma_p
 280            [assumption
 281            |apply prime_to_lt_O;apply primeb_true_to_prime;
 282             elim (and_true ? ? H2);assumption
 283            |apply le_plus_n
 284            |apply le_n]
 285         |lapply (prime_to_lt_O i (primeb_true_to_prime ? (andb_true_true ? ? H2))) as H3;
 286          apply (div_mod_spec_to_eq (n+i) i (S (n/i)) (n \mod i) ? ((n+i) \mod i))
 287            [constructor 1
 288               [apply lt_mod_m_m;assumption
 289               |simplify;rewrite > assoc_plus;rewrite < div_mod;
 290                  [apply sym_plus
 291                  |assumption]]
 292            |apply div_mod_spec_div_mod;assumption]]]]
 293 qed.
 294 *)
 295
 296 definition sqrt \def
 297   \lambda n.max n (\lambda x.leb (x*x) n).
 298
 299 theorem le_sqrt_to_le_times_l : \forall m,n.n \leq sqrt m \to n*n \leq m.
 300 intros;apply (trans_le ? (sqrt m * sqrt m))
 301   [apply le_times;assumption
 302   |apply leb_true_to_le;apply (f_max_true (λx:nat.leb (x*x) m) m);
 303    apply (ex_intro ? ? O);split
 304      [apply le_O_n
 305      |simplify;reflexivity]]
 306 qed.
 307
 308 theorem le_sqrt_to_le_times_r : \forall m,n.sqrt m < n \to m < n*n.
 309 intros;apply not_le_to_lt;intro;
 310 apply ((leb_false_to_not_le ? ?
 311            (lt_max_to_false (\lambda x.leb (x*x) m) m n H ?))
 312          H1);
 313 apply (trans_le ? ? ? ? H1);cases n
 314   [apply le_n
 315   |rewrite > times_n_SO in \vdash (? % ?);rewrite > sym_times;apply le_times
 316      [apply le_S_S;apply le_O_n
 317      |apply le_n]]
 318 qed.
 319
 320 theorem eq_theta_pi_sqrt_C1 : \forall n. theta_pi (sqrt n) = C1 n.
 321 intro;unfold theta_pi;unfold C1;rewrite > (false_to_eq_pi_p (S (sqrt n)) (S n))
 322   [generalize in match (le_sqrt_to_le_times_l n);elim (sqrt n)
 323      [simplify;reflexivity
 324      |apply (bool_elim ? (primeb (S n1)))
 325         [intro;rewrite > true_to_pi_p_Sn
 326            [rewrite > true_to_pi_p_Sn in \vdash (? ? ? %)
 327               [apply eq_f2
 328                  [reflexivity
 329                  |apply H;intros;apply H1;apply le_S;assumption]
 330               |apply (andb_elim (primeb (S n1)) (leb (S n1 * S n1) n));
 331                rewrite > H2;whd;apply le_to_leb_true;apply H1;apply le_n]
 332            |assumption]
 333         |intro;rewrite > false_to_pi_p_Sn
 334            [rewrite > false_to_pi_p_Sn in \vdash (? ? ? %)
 335               [apply H;intros;apply H1;apply le_S;assumption
 336               |apply (andb_elim (primeb (S n1)) (leb (S n1 * S n1) n));
 337                rewrite > H2;whd;reflexivity]
 338            |assumption]]]
 339   |apply le_S_S;unfold sqrt;apply le_max_n
 340   |intros;apply (andb_elim (primeb i) (leb (i*i) n));elim (primeb i);simplify
 341      [rewrite > lt_to_leb_false
 342         [reflexivity
 343         |apply le_sqrt_to_le_times_r;assumption]
 344      |reflexivity]]
 345 qed.