matita/matita/lib/arithmetics/sqrt.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/log.ma".
  13
  14 definition sqrt ≝
  15   λn.max (S n) (λx.leb (x*x) n).
  16
  17 lemma sqrt_def : ∀n.sqrt n = max (S n) (λx.leb (x*x) n).
  18 // qed.
  19
  20 theorem eq_sqrt: ∀n. sqrt (n*n) = n.
  21 #n >sqrt_def @max_spec_to_max %
  22   [@le_S_S //
  23   |@le_to_leb_true @le_n
  24   |#i #ltin #li @lt_to_leb_false @lt_times //
  25   ]
  26 qed.
  27
  28 theorem le_sqrt_to_le_times_l : ∀m,n.n ≤ sqrt m → n*n ≤ m.
  29 #m #n #len @(transitive_le ? (sqrt m * sqrt m))
  30   [@le_times //
  31   |@leb_true_to_le @(f_max_true (λx:nat.leb (x*x) m) (S m))
  32    %{0} % //
  33   ]
  34 qed.
  35
  36 theorem lt_sqrt_to_lt_times_l : ∀m,n.
  37   n < sqrt m → n*n < m.
  38 #m #n #ltn @(transitive_le ? (sqrt m * sqrt m))
  39   [@(transitive_le ? (S n * S n))
  40     [@le_S_S // |@le_times //]
  41   |@le_sqrt_to_le_times_l @le_n]
  42 qed.
  43
  44 theorem lt_sqrt_to_lt_times_r : ∀m,n.sqrt m < n → m < n*n.
  45 #m #n #ltmn @not_le_to_lt % #H1
  46 lapply (lt_max_to_false (\lambda x.leb (x*x) m) (S m) n ? ltmn)
  47   [@le_S_S @(transitive_le … H1) //
  48   |>(le_to_leb_true … H1) #H destruct (H)
  49   ]
  50 qed.
  51
  52 lemma leq_sqrt_n : ∀n. sqrt n * sqrt n ≤ n.
  53 #n @le_sqrt_to_le_times_l //
  54 qed.
  55
  56 lemma le_sqrt_n : ∀n.sqrt n ≤ n.
  57 #n @(transitive_le … (leq_sqrt_n n)) //
  58 qed.
  59
  60 lemma lt_sqrt_n : ∀n.1 < n → sqrt n < n.
  61 #n #lt1n cases (le_to_or_lt_eq ? ? (le_sqrt_n n)) #Hcase
  62   [//
  63   |@False_ind @(absurd ?? (le_to_not_lt ? ? (leq_sqrt_n n)))
  64    >Hcase >Hcase >(times_n_1 n) in ⊢ (?%?); @monotonic_lt_times_r
  65     [@lt_to_le //|//]
  66 qed.
  67
  68 lemma lt_sqrt: ∀n.n < (S (sqrt n))^2.
  69 #n cases n
  70   [@le_n
  71   |#n1 cases n1
  72     [@leb_true_to_le //
  73     |#n2 @not_le_to_lt @leb_false_to_not_le >exp_2
  74      @(lt_max_to_false (λx.(leb (x*x) (S(S n2)))) (S(S(S n2))))
  75       [@le_S_S @lt_sqrt_n @le_S_S @lt_O_S
  76       |@le_S_S @le_n
  77       ]
  78     ]
  79   ]
  80 qed.
  81
  82 (* approximations *)
  83 lemma le_sqrt_n1: ∀n. n - 2*sqrt n ≤ exp (sqrt n) 2.
  84 #n  @le_plus_to_minus @le_S_S_to_le
  85 cut (S ((sqrt n)\sup 2+2*sqrt n) = (exp (S(sqrt n)) 2))
  86   [2:#Hcut >Hcut @lt_sqrt]
  87 >exp_2 >exp_2 generalize in match (sqrt n); #a
  88 normalize //
  89 qed.
  90
  91 (* falso per n=2, m=7 e n=3, m =15
  92   a technical lemma used in Bertrand *)
  93 lemma le_sqrt_nl: ∀n,m. 3 < n →
  94   m*(pred m)*n ≤ exp (sqrt ((exp m 2)*n)) 2.
  95 #n #m #lt3n >(minus_n_O m) in ⊢ (? (? (? ? (? %)) ?) ?);
  96 <eq_minus_S_pred >distributive_times_minus <times_n_1
  97 >commutative_times >distributive_times_minus
  98 >commutative_times
  99 @(transitive_le ? (m*m*n -2*sqrt(m*m*n)))
 100   [@monotonic_le_minus_r
 101    @(le_exp_to_le1 ?? 2 (lt_O_S ?))
 102    <times_exp @(transitive_le ? ((exp 2 2)*(m*m*n)))
 103     [@monotonic_le_times_r >exp_2 @leq_sqrt_n
 104     |<exp_2 <times_exp <associative_times
 105      <commutative_times in ⊢ (?(?%?)?);
 106      >associative_times >commutative_times
 107      @le_times [2://] >exp_2 in ⊢ (??%); @le_times //
 108     ]
 109   |<exp_2 @le_sqrt_n1
 110   ]
 111 qed.
 112
 113 lemma le_sqrt_log: ∀n,b. 2 < b  → log b n ≤ sqrt n.
 114 #n #b #lt2b >sqrt_def
 115 @true_to_le_max
 116   [@le_S_S @le_log_n_n @lt_to_le //
 117   |@le_to_leb_true cases (le_to_or_lt_eq ? ? (le_O_n n)) #Hn
 118     [@(transitive_le … (le_exp_log b n Hn))
 119      elim (log b n)
 120       [@le_O_n
 121       |#n1 #Hind normalize in ⊢ (??%);
 122        cases(le_to_or_lt_eq ?? (le_O_n n1)) #H0
 123         [cases(le_to_or_lt_eq ? ? H0) #H1
 124           [@(transitive_le ? (3*(n1*n1)))
 125             [normalize in ⊢ (?%?); >commutative_times in ⊢ (?%?);
 126              whd in ⊢ (??%);
 127              cut (S (n1+(S n1*n1)) = n1*n1 + ((S n1) + n1))
 128               [normalize >commutative_plus in ⊢ (???%); normalize //] #Hcut
 129              >Hcut @monotonic_le_plus_r normalize in ⊢ (??%); <plus_n_O @le_plus
 130               [>(times_n_1 n1) in ⊢ (?%?); @monotonic_lt_times_r // |//]
 131             |>commutative_times @le_times //
 132             ]
 133           |<H1 normalize <plus_n_O
 134            cut (4 = 2*2) [//] #H4 >H4 @lt_to_le @lt_times //
 135           ]
 136         |<H0 normalize <plus_n_O @(transitive_le … lt2b) @leb_true_to_le //
 137         ]
 138       ]
 139     |<Hn @le_n
 140     ]
 141   ]
 142 qed.
 143
 144 lemma le_sqrt_log_n : ∀n,b. 2 < b → sqrt n * log b n ≤ n.
 145 #n #b #lt2b @(transitive_le … (leq_sqrt_n ?))
 146 @monotonic_le_times_r @le_sqrt_log //
 147 qed.
 148
 149 theorem le_square_exp:∀n. 3 < n → exp n 2 ≤ exp 2 n.
 150 #n #lt3n elim lt3n
 151   [@le_n
 152   |#m #le4m #Hind normalize <plus_n_O >commutative_times
 153    normalize <(commutative_times 2) normalize <associative_plus
 154    <plus_n_O >commutative_plus >plus_n_Sm @le_plus
 155      [<exp_2 @Hind
 156      |elim le4m [@leb_true_to_le //]
 157       #m1 #lem1 #Hind1 normalize >commutative_times normalize
 158       <plus_n_O <plus_n_Sm >(plus_n_O (S(m1+m1))) >plus_n_Sm >plus_n_Sm
 159       @le_plus [@Hind1 |>(exp_n_1 2) in ⊢ (?%?); @le_exp
 160        [@lt_O_S |@(transitive_le … lem1) @leb_true_to_le //]
 161      ]
 162    ]
 163  ]
 164 qed.
 165
 166 lemma le_log2_sqrt: ∀n. 2^4 ≤ n→ log 2 n ≤ sqrt n.
 167 #n #le_n >sqrt_def
 168 @true_to_le_max
 169   [@le_S_S @le_log_n_n //
 170   |@le_to_leb_true
 171    cut (0<n) [@(transitive_lt … le_n) @lt_O_S] #posn
 172    @(transitive_le … (le_exp_log 2 n posn))
 173    <exp_2 @le_square_exp @true_to_le_max
 174     [@(lt_to_le_to_lt … le_n) @leb_true_to_le // |@le_to_leb_true //]
 175   ]
 176 qed.
 177
 178 lemma square_S: ∀a. (S a)^2 = a^2 + 2*a +1.
 179 #a normalize >commutative_times normalize //
 180 qed.
 181
 182 theorem le_squareS_exp:∀n. 5 < n → exp (S n) 2 ≤ exp 2 n.
 183 #n #lt4n elim lt4n
 184   [@leb_true_to_le //
 185   |#m #le4m #Hind >square_S whd in ⊢(??%); >commutative_times in ⊢(??%);
 186    normalize in ⊢(??%); <plus_n_O >associative_plus @le_plus [@Hind]
 187    elim le4m [@leb_true_to_le //] #a #lea #Hinda
 188    @(transitive_le ? (2*(2*(S a)+1)))
 189     [@lt_to_le whd >plus_n_Sm >(times_n_1 2) in ⊢ (?(??%)?);
 190      <distributive_times_plus @monotonic_le_times_r @le_plus [2://]
 191      normalize //
 192     |whd in ⊢ (??%); >commutative_times in ⊢(??%); @monotonic_le_times_r @Hinda
 193     ]
 194  ]
 195 qed.
 196
 197
 198 lemma lt_log2_sqrt: ∀n. 2^6 ≤ n→ log 2 n < sqrt n.
 199 #n #le_n >sqrt_def
 200 cut (0<n) [@(transitive_lt … le_n) @lt_O_S] #posn
 201 @true_to_le_max
 202   [@le_S_S @lt_log_n_n //
 203   |@le_to_leb_true
 204    cut (0<n) [@(transitive_lt … le_n) @lt_O_S] #posn
 205    @(transitive_le … (le_exp_log 2 n posn))
 206    <exp_2 @le_squareS_exp @true_to_le_max
 207     [@(lt_to_le_to_lt … le_n) @leb_true_to_le //
 208     |@le_to_leb_true //
 209     ]
 210   ]
 211 qed.
 212
 213 (* monotonicity *)
 214 theorem monotonic_sqrt: monotonic nat le sqrt.
 215 #n #m #lenm >sqrt_def @true_to_le_max
 216   [@le_S_S @(transitive_le … lenm) @le_sqrt_n
 217   |@le_to_leb_true @(transitive_le … lenm) @leq_sqrt_n
 218   ]
 219 qed.
 220
 221