matita/matita/lib/arithmetics/log.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/exp.ma".
  13 include "arithmetics/minimization.ma".
  14 include "arithmetics/div_and_mod.ma".
  15
  16 definition log ≝ λp,n.
  17   max n (λx.leb (exp p x) n).
  18
  19 lemma tech_log : ∀p,n. 1<p → 0 < n →
  20   log p n = max (S n) (λx.leb (exp p x) n).
  21 #p #n #lt1p #posn whd in ⊢ (???%);
  22 cut (leb (exp p n) n = false)
  23   [@not_le_to_leb_false @lt_to_not_le /2/
  24   |#Hleb >Hleb %
  25   ]
  26 qed.
  27
  28 theorem le_exp_log: ∀p,n. O < n →
  29   exp p (log p n) ≤ n.
  30 #a #n #posn @leb_true_to_le
  31 (* whd in match (log ??); *)
  32 @(f_max_true (λx.leb (exp a x) n)) %{0} % //
  33 @le_to_leb_true //
  34 qed.
  35
  36 theorem log_SO: ∀n. 1 < n → log n 1 = O.
  37 #n #lt1n @sym_eq @le_n_O_to_eq @(le_exp_to_le n) //
  38 qed.
  39
  40 theorem lt_to_log_O: ∀n,m. O < m → m < n → log n m = O.
  41 #n #m #posm #ltnm @sym_eq @le_n_O_to_eq @le_S_S_to_le @(lt_exp_to_lt n)
  42   [@(le_to_lt_to_lt ? m) //
  43   |normalize in ⊢ (??%); <plus_n_O @(le_to_lt_to_lt ? m) //
  44    @le_exp_log //
  45   ]
  46 qed.
  47
  48 theorem lt_log_n_n: ∀p, n. 1 < p → O < n → log p n < n.
  49 #p #n #lt1p #posn
  50 cut (log p n ≤ n)
  51   [whd in match (log ??); @le_max_n
  52   |#Hcut elim (le_to_or_lt_eq ? ? Hcut) //
  53    #Hn @False_ind @(absurd … (exp p n ≤ n))
  54     [<Hn in ⊢ (?(??%)?); @le_exp_log //
  55     |@lt_to_not_le @lt_m_exp_nm //
  56     ]
  57   ]
  58 qed.
  59
  60 theorem lt_O_log: ∀p, n. 1 < n → p ≤ n → O < log p n.
  61 #p #n #lt1p #lepn whd in match (log ??);
  62 @not_lt_to_le % #H lapply (lt_max_to_false ??? lt1p H)
  63 <exp_n_1 >(le_to_leb_true … lepn) #H destruct
  64 qed.
  65
  66 theorem le_log_n_n: ∀p,n. 1 < p → log p n ≤ n.
  67 #p #n #lt1p cases n [@le_n |#m @lt_to_le @lt_log_n_n //]
  68 qed.
  69
  70 theorem lt_exp_log: ∀p,n. 1 < p → n < exp p (S (log p n)).
  71 #p #n #lt1p cases n
  72   [normalize <plus_n_O @lt_to_le //
  73   |#m @not_le_to_lt @leb_false_to_not_le
  74    @(lt_max_to_false ? (S(S m)) (S (log p (S m))))
  75     [@le_S_S @lt_log_n_n //
  76     |<tech_log //
  77     ]
  78   ]
  79 qed.
  80
  81 theorem log_times1: ∀p,n,m. 1 < p → O < n → O < m →
  82   log p (n*m) ≤ S(log p n+log p m).
  83 #p #n #m #lt1p #posn #posm
  84 whd in ⊢ (?(%??)?); @f_false_to_le_max
  85   [%{O} %
  86     [>(times_n_O 0) in ⊢ (?%%); @lt_times //
  87     |@le_to_leb_true normalize >(times_n_O 0) in ⊢ (?%%); @lt_times //
  88     ]
  89   |#i #Hm @lt_to_leb_false
  90    @(lt_to_le_to_lt ? ((exp p (S(log p n)))*(exp p (S(log p m)))))
  91     [@lt_times @lt_exp_log //
  92     |<exp_plus_times @le_exp [@lt_to_le //]
  93      normalize <plus_n_Sm //
  94     ]
  95   ]
  96 qed.
  97
  98 theorem log_times: ∀p,n,m. 1 < p →
  99   log p (n*m) ≤ S(log p n+log p m).
 100 #p #n #m #lt1p cases n // -n #n cases m
 101   [<times_n_O @le_O_n |-m #m @log_times1 //]
 102 qed.
 103
 104 theorem log_times_l: ∀p,n,m.O < n → O < m → 1 < p →
 105   log p n+log p m ≤ log p (n*m).
 106 #p #n #m #posn #posm #lt1p whd in ⊢ (??(%??));
 107 @true_to_le_max
 108   [cases posn
 109     [>(log_SO … lt1p) >commutative_times <times_n_1 @lt_log_n_n //
 110     |-n #n #posn cases posm
 111       [>(log_SO … lt1p) < plus_n_O <times_n_1 @lt_log_n_n //
 112       |#m1 #lem1 @(transitive_le ? (S n + S m1))
 113         [@le_S_S @le_plus // @le_S_S_to_le @lt_log_n_n //
 114         |@le_S_S >commutative_plus normalize >plus_n_Sm
 115          @monotonic_le_plus_r >(times_n_1 n) in ⊢ (?%?);
 116          @monotonic_lt_times_r // @le_S_S //
 117         ]
 118       ]
 119     ]
 120   |@le_to_leb_true >exp_plus_times @le_times @le_exp_log //
 121   ]
 122 qed.
 123
 124 theorem log_exp: ∀p,n,m. 1 < p → O < m →
 125   log p ((exp p n)*m)=n+log p m.
 126 #p #n #m #lt1p #posm whd in ⊢ (??(%??)?);
 127 @max_spec_to_max %
 128   [elim n
 129     [<(exp_n_O p) >commutative_times <times_n_1
 130      @lt_log_n_n //
 131     |#a #Hind whd in ⊢ (?%?);
 132      @(lt_to_le_to_lt ? (S((p^a) *m))) [@le_S_S @Hind]
 133      whd in match (exp ? (S a)); >(commutative_times ? p)
 134      >associative_times >(times_n_1 (p^a * m)) in ⊢ (?%?);
 135      >commutative_times in ⊢ (?%?); @monotonic_lt_times_l //
 136      >(times_n_O 0) @lt_times // @lt_O_exp @lt_to_le //
 137     ]
 138   |@le_to_leb_true >exp_plus_times
 139    @monotonic_le_times_r @le_exp_log //
 140   |#i #Hi #Hm @lt_to_leb_false
 141    @(lt_to_le_to_lt ? ((exp p n)*(exp p (S(log p m)))))
 142     [@monotonic_lt_times_r [@lt_O_exp @lt_to_le // |@lt_exp_log //]
 143     |<exp_plus_times @le_exp [@lt_to_le // |<plus_n_Sm //]
 144     ]
 145   ]
 146 qed.
 147
 148 theorem eq_log_exp: ∀p,n. 1< p →
 149   log p (exp p n)=n.
 150 #p #n #lt1p  >(times_n_1 (p^n)) in ⊢ (??(??%)?); >log_exp // >log_SO //
 151 qed.
 152
 153 theorem log_exp1: ∀p,n,m. 1 < p →
 154   log p (exp n m) ≤ m*S(log p n).
 155 #p #n #m #lt1p elim m // -m #m #Hind
 156 @(transitive_le ? (S (log p n+log p (n\sup m))))
 157   [whd in match (exp ??); >commutative_times @log_times //
 158   |@le_S_S @monotonic_le_plus_r //
 159   ]
 160 qed.
 161
 162 theorem log_exp2: ∀p,n,m. 1 < p → 0 < n →
 163   m*(log p n) ≤ log p (exp n m).
 164 #p #n #m #ltp1 #posn @le_S_S_to_le @(lt_exp_to_lt p)
 165   [@lt_to_le //
 166   |>commutative_times <exp_exp_times @(le_to_lt_to_lt ? (exp n m))
 167     [elim m // -m #m #Hind whd in match (exp ??); @le_times // @le_exp_log //
 168     |@lt_exp_log //
 169     ]
 170   ]
 171 qed.
 172
 173 lemma le_log_S: ∀p,n.1 < p →
 174   log p n ≤ log p (S n).
 175 #p #n #lt1p normalize cases (leb (exp p n) (S n)) normalize //
 176 @le_max_f_max_g #i #ltin #H @le_to_leb_true @le_S @leb_true_to_le //
 177 qed.
 178
 179 theorem le_log: ∀p,n,m. 1 < p → n ≤ m →
 180   log p n ≤ log p m.
 181 #p #n #m #lt1p #lenm elim lenm // -m #m #lenm #Hind
 182 @(transitive_le … Hind) @le_log_S //
 183 qed.
 184
 185 theorem log_div: ∀p,n,m. 1 < p → O < m → m ≤ n →
 186   log p (n/m) ≤ log p n -log p m.
 187 #p #n #m #lt1p #posn #lemn
 188 @le_plus_to_minus_r @(transitive_le ? (log p ((n/m)*m)))
 189   [@log_times_l // @le_times_to_le_div //
 190   |@le_log //
 191   ]
 192 qed.
 193
 194 theorem log_n_n: ∀n. 1 < n → log n n = 1.
 195 #n #lt1n >(exp_n_1 n) in ⊢ (??(??%)?);
 196 >(times_n_1 (n^1)) in ⊢ (??(??%)?); >log_exp //
 197 qed.
 198
 199 theorem log_i_2n: ∀n,i. 1 < n → n < i → i ≤ 2*n →
 200   log i (2*n) = 1.
 201 #n #i #lt1n #ltni #lei
 202 cut (∀a,b. a≤b → b≤a → a=b)
 203   [#a #b #leab #leba cases (le_to_or_lt_eq … leab)
 204     [#ltab @False_ind @(absurd ? ltab) @le_to_not_lt // | //]] #Hcut
 205 @Hcut
 206   [@not_lt_to_le % #H
 207    @(absurd ?? (lt_to_not_le (2 * n) (exp i 2) ?))
 208     [@(transitive_le ? (exp i (log i (2*n))))
 209       [@le_exp // @(ltn_to_ltO ? ? ltni)
 210       |@le_exp_log >(times_n_O O) in ⊢ (?%?); @lt_times // @lt_to_le //
 211       ]
 212     |>exp_2 @lt_times @(le_to_lt_to_lt ? n) //
 213     ]
 214   |@(transitive_le ? (log i i))
 215     [<(log_n_n i) in ⊢ (?%?); // @(transitive_lt … lt1n) //
 216     |@le_log // @(transitive_lt … lt1n) //
 217     ]
 218   ]
 219 qed.
 220
 221 theorem exp_n_O: ∀n. O < n → exp O n = O.
 222 #n #posn @(lt_O_n_elim ? posn) normalize //
 223 qed.
 224