matita/matita/lib/arithmetics/chebyshev/chebyshev_teta.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||  This file is distributed under the terms of the
   8     \   /  GNU General Public License Version 2
   9      \ /
  10       V_______________________________________________________________ *)
  11
  12 include "arithmetics/binomial.ma".
  13 include "arithmetics/gcd.ma".
  14 include "arithmetics/chebyshev/chebyshev.ma".
  15
  16 (* This is chebishev teta function *)
  17
  18 definition teta: nat → nat ≝ λn.
  19   ∏_{p < S n| primeb p} p.
  20
  21 lemma teta_def: ∀n.teta n = ∏_{p < S n| primeb p} p.
  22 // qed.
  23
  24 theorem lt_O_teta: ∀n. O < teta n.
  25 #n elim n
  26   [@le_n
  27   |#n1 #Hind cases (true_or_false (primeb (S n1))) #Hc
  28     [>teta_def >bigop_Strue
  29       [>(times_n_O O) @lt_times // | //]
  30     |>teta_def >bigop_Sfalse //
  31     ]
  32   ]
  33 qed.
  34
  35 theorem divides_fact_to_divides: ∀p,n. prime p → divides p n! →
  36   ∃m.O < m ∧ m \le n ∧ divides p m.
  37 #p #n #primep elim n
  38   [normalize in ⊢ (%→?); #H @False_ind @(absurd (p ≤1))
  39     [@divides_to_le //|@lt_to_not_le @prime_to_lt_SO @primep]
  40   |#n1 #Hind >factS #Hdiv
  41    cases (divides_times_to_divides ??? primep Hdiv) #Hcase
  42     [%{(S n1)} %[ % [@lt_O_S |@le_n] |@Hcase]
  43     |cases(Hind Hcase) #a * * #posa #lea #diva
  44      %{a} % [% [// |@le_S //] |//]
  45     ]
  46   ]
  47 qed.
  48
  49 theorem divides_fact_to_le: ∀p,n. prime p → divides p n! → p ≤ n.
  50 #p #n #primep #divp cases (divides_fact_to_divides p n primep divp)
  51 #a * * #posa #lea #diva @(transitive_le ? a) [@divides_to_le // | //]
  52 qed.
  53
  54 theorem prime_to_divides_M: ∀m,p.
  55   prime p → S m < p → p ≤ S(2*m) → divides p (M m).
  56 #m #p #primep #lemp #lep >Mdef >bceq
  57 cases (bc2 (S(2*m)) m ?)
  58   [#q #Hq >Hq >commutative_times >div_times
  59     [cases (divides_times_to_divides p (m!*(S (2*m)-m)!) q primep ?)
  60       [#Hdiv @False_ind
  61        cases (divides_times_to_divides p (m!) (S (2*m)-m)! primep ?)
  62         [-Hdiv #Hdiv @(absurd (p ≤ m))
  63           [@divides_fact_to_le //
  64           |@(lt_to_not_le ?? (lt_to_le ?? lemp))
  65           ]
  66         |-Hdiv #Hdiv @(absurd (p ≤S m))
  67           [@(divides_fact_to_le … primep)
  68            cut (S m = S(2*m)-m)
  69             [normalize in ⊢ (???(?%?)); <plus_n_O
  70              >plus_n_Sm >commutative_plus @minus_plus_m_m
  71             ] #HSm
  72            >HSm //
  73           |@lt_to_not_le //
  74           ]
  75         |//
  76         ]
  77       |//
  78       |<Hq @divides_fact [@prime_to_lt_O // |//]
  79       ]
  80     |>(times_n_O O) in ⊢ (?%?); @lt_times //
  81     ]
  82   |normalize in ⊢ (??(?%)); <plus_n_O //
  83   ]
  84 qed.
  85
  86 theorem divides_pi_p_M1: ∀m.∀i. i ≤ S(S(2*m)) →
  87   ∏_{p < i | leb (S(S m)) p ∧ primeb p} p ∣ M m .
  88 #m #i elim i
  89   [#_ @(quotient ?? (M m)) >commutative_times @times_n_1
  90   |#n #Hind #len
  91    cases (true_or_false (leb (S (S m)) n ∧ primeb n)) #Hc
  92     [>bigop_Strue
  93       [@divides_to_divides_times
  94         [@primeb_true_to_prime @(andb_true_r ?? Hc)
  95         |cut (∀p.prime p → n ≤ p → ¬p∣∏_{p < n | leb (S (S m)) p∧primeb p} p)
  96           [2: #Hcut @(Hcut … (le_n ?)) @primeb_true_to_prime @(andb_true_r ?? Hc)]
  97          #p #primep elim n
  98           [#_ normalize @(not_to_not ? (p ≤ 1))
  99             [@divides_to_le @lt_O_S|@lt_to_not_le @prime_to_lt_SO //]
 100           |#n1 #Hind1 #Hn1 cases (true_or_false (leb (S (S m)) n1∧primeb n1)) #Hc1
 101             [>bigop_Strue
 102               [% #Habs cases(divides_times_to_divides ??? primep Habs)
 103                 [-Habs #Habs @(absurd … Hn1) @le_to_not_lt
 104                  @(divides_to_le … Habs) @prime_to_lt_O
 105                  @primeb_true_to_prime @(andb_true_r ?? Hc1)
 106                 |-Habs #Habs @(absurd … Habs) @Hind1 @lt_to_le //
 107                 ]
 108               |@Hc1
 109               ]
 110             |>bigop_Sfalse // @Hind1 @lt_to_le //
 111             ]
 112           ]
 113         |@prime_to_divides_M
 114           [@primeb_true_to_prime @(andb_true_r ?? Hc)
 115           |@leb_true_to_le @(andb_true_l ?? Hc)
 116           |@le_S_S_to_le //
 117           ]
 118         |@Hind @lt_to_le //
 119         ]
 120       |@Hc
 121       ]
 122     |>bigop_Sfalse // @Hind @lt_to_le @len
 123     ]
 124   ]
 125 qed.
 126
 127 theorem divides_pi_p_M:∀m.
 128   ∏_{p < S(S(2*m)) | leb (S(S m)) p ∧ primeb p} p ∣ (M m).
 129 #m  @divides_pi_p_M1 @le_n
 130 qed.
 131
 132 theorem teta_pi_p_teta: ∀m. teta (S (2*m))
 133 = (∏_{p < S (S (2*m)) | leb (S (S m)) p∧primeb p} p)*teta (S m).
 134 #m >teta_def >teta_def
 135 <(bigop_I ???? timesA)
 136 >(bigop_sumI 0 (S(S m)) (S(S(2*m))) (λp.primeb p) … timesA (λp.p))
 137   [2:@le_S_S @le_S_S // |3:@le_O_n]
 138 @eq_f2
 139   [>bigop_I_gen // |@(bigop_I … timesA)]
 140 qed.
 141
 142 theorem div_teta_teta: ∀m.
 143   teta (S(2*m))/teta (S m) =
 144     ∏_{p < S(S(2*m)) | leb (S(S m)) p ∧ primeb p} p.
 145 #m @(div_mod_spec_to_eq ????? 0 (div_mod_spec_div_mod …))
 146   [@lt_O_teta
 147   |@div_mod_spec_intro [@lt_O_teta |<plus_n_O @teta_pi_p_teta]
 148   ]
 149 qed.
 150
 151 theorem le_teta_M_teta: ∀m.
 152   teta (S(2*m)) ≤ (M m)*teta (S m).
 153 #m >teta_pi_p_teta @le_times [2://] @divides_to_le
 154   [@lt_O_bc @lt_to_le @le_S_S // | @divides_pi_p_M
 155   ]
 156 qed.
 157
 158 theorem lt_O_to_le_teta_exp_teta: ∀m. O < m→
 159   teta (S(2*m)) < exp 2 (2*m)*teta (S m).
 160 #m #posm @(le_to_lt_to_lt ? (M m*teta (S m)))
 161   [@le_teta_M_teta
 162   |@monotonic_lt_times_l [@lt_O_teta|@lt_M //]
 163   ]
 164 qed.
 165
 166 theorem teta_pred: ∀n. 1 < n → teta (2*n) = teta (pred (2*n)).
 167 #n #lt1n >teta_def >teta_def >bigop_Sfalse
 168   [>S_pred
 169     [//
 170     |>(times_n_O 2) in ⊢ (?%?); @monotonic_lt_times_r @lt_to_le //
 171     ]
 172   |@not_prime_to_primeb_false % * #lt2n #Hprime
 173    @(absurd (2=2*n))
 174     [@(Hprime … (le_n ?)) %{n} //
 175     |@lt_to_not_eq >(times_n_1 2) in ⊢ (?%?); @monotonic_lt_times_r //
 176     ]
 177   ]
 178 qed.
 179
 180 theorem le_teta: ∀m.teta m ≤ exp 2 (2*m).
 181 #m @(nat_elim1 m) #m1 #Hind
 182 cut (∀a. 2 *a = a+a) [//] #times2
 183 cases (even_or_odd m1) #a * #Ha >Ha
 184   [lapply Ha cases a
 185     [#_ @le_n
 186     |#n cases n
 187       [#_ @leb_true_to_le //
 188       |#n1 #Hn1 >teta_pred
 189         [cut (pred (2*S(S n1)) = (S (2*S n1)))
 190           [normalize >plus_n_Sm in ⊢ (???%); //] #Hcut >Hcut
 191          @(transitive_le ? (exp 2 (2*(S n1))*teta (S (S n1))))
 192           [@lt_to_le @lt_O_to_le_teta_exp_teta @lt_O_S
 193           |>times2 in ⊢ (??%);>exp_plus_times in ⊢ (??%); @le_times
 194             [@le_exp [@lt_O_S |@monotonic_le_times_r @le_n_Sn]
 195             |@Hind >Hn1 >times2 //
 196             ]
 197           ]
 198         |@le_S_S @lt_O_S
 199         ]
 200       ]
 201     ]
 202   |lapply Ha cases a
 203     [#_ @leb_true_to_le //
 204     |#n #Hn @(transitive_le ? (exp 2 (2*(S n))*teta (S (S n))))
 205       [@lt_to_le @lt_O_to_le_teta_exp_teta @lt_O_S
 206       |>times2 in ⊢ (??%); <plus_n_Sm <commutative_plus >plus_n_Sm
 207        >exp_plus_times in ⊢ (??%); @monotonic_le_times_r
 208        cut (∀a. 2*(S a) = S(S(2*a))) [#a normalize <plus_n_Sm //] #timesSS
 209        <timesSS @Hind >Hn @le_S_S >times2 //
 210       ]
 211     ]
 212   ]
 213 qed.
 214