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 axiom daemon : ∀P:Prop.P.
  71
  72 theorem lt_exp_log: ∀p,n. 1 < p → n < exp p (S (log p n)).
  73 #p #n #lt1p cases n
  74   [normalize <plus_n_O @lt_to_le //
  75   |#m @not_le_to_lt @leb_false_to_not_le
  76    @(lt_max_to_false ? (S(S m)) (S (log p (S m))))
  77     [@le_S_S @lt_log_n_n //
  78     |<tech_log //
  79     ]
  80   ]
  81 qed.
  82
  83 theorem log_times1: ∀p,n,m. 1 < p → O < n → O < m →
  84   log p (n*m) ≤ S(log p n+log p m).
  85 #p #n #m #lt1p #posn #posm
  86 whd in ⊢ (?(%??)?); @f_false_to_le_max
  87   [%{O} %
  88     [>(times_n_O 0) in ⊢ (?%%); @lt_times //
  89     |@le_to_leb_true normalize >(times_n_O 0) in ⊢ (?%%); @lt_times //
  90     ]
  91   |#i #Hm @lt_to_leb_false
  92    @(lt_to_le_to_lt ? ((exp p (S(log p n)))*(exp p (S(log p m)))))
  93     [@lt_times @lt_exp_log //
  94     |<exp_plus_times @le_exp [@lt_to_le //]
  95      normalize <plus_n_Sm //
  96     ]
  97   ]
  98 qed.
  99
 100 theorem log_times: ∀p,n,m. 1 < p →
 101   log p (n*m) ≤ S(log p n+log p m).
 102 #p #n #m #lt1p cases n // -n #n cases m
 103   [<times_n_O @le_O_n |-m #m @log_times1 //]
 104 qed.
 105
 106 theorem log_times_l: ∀p,n,m.O < n → O < m → 1 < p →
 107   log p n+log p m ≤ log p (n*m).
 108 #p #n #m #posn #posm #lt1p whd in ⊢ (??(%??));
 109 @true_to_le_max
 110   [cases posn
 111     [>(log_SO … lt1p) >commutative_times <times_n_1 @lt_log_n_n //
 112     |-n #n #posn cases posm
 113       [>(log_SO … lt1p) < plus_n_O <times_n_1 @lt_log_n_n //
 114       |#m1 #lem1 @(transitive_le ? (S n + S m1))
 115         [@le_S_S @le_plus // @le_S_S_to_le @lt_log_n_n //
 116         |@le_S_S >commutative_plus normalize >plus_n_Sm
 117          @monotonic_le_plus_r >(times_n_1 n) in ⊢ (?%?);
 118          @monotonic_lt_times_r // @le_S_S //
 119         ]
 120       ]
 121     ]
 122   |@le_to_leb_true >exp_plus_times @le_times @le_exp_log //
 123   ]
 124 qed.
 125
 126 theorem log_exp: ∀p,n,m. 1 < p → O < m →
 127   log p ((exp p n)*m)=n+log p m.
 128 #p #n #m #lt1p #posm whd in ⊢ (??(%??)?);
 129 @max_spec_to_max %
 130   [elim n
 131     [<(exp_n_O p) >commutative_times <times_n_1
 132      @lt_log_n_n //
 133     |#a #Hind whd in ⊢ (?%?);
 134      @(lt_to_le_to_lt ? (S((p^a) *m))) [@le_S_S @Hind]
 135      whd in match (exp ? (S a)); >(commutative_times ? p)
 136      >associative_times >(times_n_1 (p^a * m)) in ⊢ (?%?);
 137      >commutative_times in ⊢ (?%?); @monotonic_lt_times_l //
 138      >(times_n_O 0) @lt_times // @lt_O_exp @lt_to_le //
 139     ]
 140   |@le_to_leb_true >exp_plus_times
 141    @monotonic_le_times_r @le_exp_log //
 142   |#i #Hi #Hm @lt_to_leb_false
 143    @(lt_to_le_to_lt ? ((exp p n)*(exp p (S(log p m)))))
 144     [@monotonic_lt_times_r [@lt_O_exp @lt_to_le // |@lt_exp_log //]
 145     |<exp_plus_times @le_exp [@lt_to_le // |<plus_n_Sm //]
 146     ]
 147   ]
 148 qed.
 149
 150 theorem eq_log_exp: ∀p,n. 1< p →
 151   log p (exp p n)=n.
 152 #p #n #lt1p  >(times_n_1 (p^n)) in ⊢ (??(??%)?); >log_exp // >log_SO //
 153 qed.
 154
 155 theorem log_exp1: ∀p,n,m. 1 < p →
 156   log p (exp n m) ≤ m*S(log p n).
 157 #p #n #m #lt1p elim m // -m #m #Hind
 158 @(transitive_le ? (S (log p n+log p (n\sup m))))
 159   [whd in match (exp ??); >commutative_times @log_times //
 160   |@le_S_S @monotonic_le_plus_r //
 161   ]
 162 qed.
 163
 164 theorem log_exp2: ∀p,n,m. 1 < p → 0 < n →
 165   m*(log p n) ≤ log p (exp n m).
 166 #p #n #m #ltp1 #posn @le_S_S_to_le @(lt_exp_to_lt p)
 167   [@lt_to_le //
 168   |>commutative_times <exp_exp_times @(le_to_lt_to_lt ? (exp n m))
 169     [elim m // -m #m #Hind whd in match (exp ??); @le_times // @le_exp_log //
 170     |@lt_exp_log //
 171     ]
 172   ]
 173 qed.
 174
 175 lemma le_log_S: ∀p,n.1 < p →
 176   log p n ≤ log p (S n).
 177 #p #n #lt1p normalize cases (leb (exp p n) (S n)) normalize //
 178 @le_max_f_max_g #i #ltin #H @le_to_leb_true @le_S @leb_true_to_le //
 179 qed.
 180
 181 theorem le_log: ∀p,n,m. 1 < p → n ≤ m →
 182   log p n ≤ log p m.
 183 #p #n #m #lt1p #lenm elim lenm // -m #m #lenm #Hind
 184 @(transitive_le … Hind) @le_log_S //
 185 qed.
 186
 187 theorem log_div: ∀p,n,m. 1 < p → O < m → m ≤ n →
 188   log p (n/m) ≤ log p n -log p m.
 189 #p #n #m #lt1p #posn #lemn
 190 @le_plus_to_minus_r @(transitive_le ? (log p ((n/m)*m)))
 191   [@log_times_l // @le_times_to_le_div //
 192   |@le_log //
 193   ]
 194 qed.
 195
 196 theorem log_n_n: ∀n. 1 < n → log n n = 1.
 197 #n #lt1n >(exp_n_1 n) in ⊢ (??(??%)?);
 198 >(times_n_1 (n^1)) in ⊢ (??(??%)?); >log_exp //
 199 qed.
 200
 201 theorem log_i_2n: ∀n,i. 1 < n → n < i → i ≤ 2*n →
 202   log i (2*n) = 1.
 203 #n #i #lt1n #ltni #lei
 204 cut (∀a,b. a≤b → b≤a → a=b)
 205   [#a #b #leab #leba cases (le_to_or_lt_eq … leab)
 206     [#ltab @False_ind @(absurd ? ltab) @le_to_not_lt // | //]] #Hcut
 207 @Hcut
 208   [@not_lt_to_le % #H
 209    @(absurd ?? (lt_to_not_le (2 * n) (exp i 2) ?))
 210     [@(transitive_le ? (exp i (log i (2*n))))
 211       [@le_exp // @(ltn_to_ltO ? ? ltni)
 212       |@le_exp_log >(times_n_O O) in ⊢ (?%?); @lt_times // @lt_to_le //
 213       ]
 214     |>exp_2 @lt_times @(le_to_lt_to_lt ? n) //
 215     ]
 216   |@(transitive_le ? (log i i))
 217     [<(log_n_n i) in ⊢ (?%?); // @(transitive_lt … lt1n) //
 218     |@le_log // @(transitive_lt … lt1n) //
 219     ]
 220   ]
 221 qed.
 222
 223 theorem exp_n_O: ∀n. O < n → exp O n = O.
 224 #n #posn @(lt_O_n_elim ? posn) normalize //
 225 qed.
 226