1(* Title: HOL/NthRoot.thy 2 Author: Jacques D. Fleuriot, 1998 3 Author: Lawrence C Paulson, 2004 4*) 5 6section \<open>Nth Roots of Real Numbers\<close> 7 8theory NthRoot 9 imports Deriv 10begin 11 12 13subsection \<open>Existence of Nth Root\<close> 14 15text \<open>Existence follows from the Intermediate Value Theorem\<close> 16 17lemma realpow_pos_nth: 18 fixes a :: real 19 assumes n: "0 < n" 20 and a: "0 < a" 21 shows "\<exists>r>0. r ^ n = a" 22proof - 23 have "\<exists>r\<ge>0. r \<le> (max 1 a) \<and> r ^ n = a" 24 proof (rule IVT) 25 show "0 ^ n \<le> a" 26 using n a by (simp add: power_0_left) 27 show "0 \<le> max 1 a" 28 by simp 29 from n have n1: "1 \<le> n" 30 by simp 31 have "a \<le> max 1 a ^ 1" 32 by simp 33 also have "max 1 a ^ 1 \<le> max 1 a ^ n" 34 using n1 by (rule power_increasing) simp 35 finally show "a \<le> max 1 a ^ n" . 36 show "\<forall>r. 0 \<le> r \<and> r \<le> max 1 a \<longrightarrow> isCont (\<lambda>x. x ^ n) r" 37 by simp 38 qed 39 then obtain r where r: "0 \<le> r \<and> r ^ n = a" 40 by fast 41 with n a have "r \<noteq> 0" 42 by (auto simp add: power_0_left) 43 with r have "0 < r \<and> r ^ n = a" 44 by simp 45 then show ?thesis .. 46qed 47 48(* Used by Integration/RealRandVar.thy in AFP *) 49lemma realpow_pos_nth2: "(0::real) < a \<Longrightarrow> \<exists>r>0. r ^ Suc n = a" 50 by (blast intro: realpow_pos_nth) 51 52text \<open>Uniqueness of nth positive root.\<close> 53lemma realpow_pos_nth_unique: "0 < n \<Longrightarrow> 0 < a \<Longrightarrow> \<exists>!r. 0 < r \<and> r ^ n = a" for a :: real 54 by (auto intro!: realpow_pos_nth simp: power_eq_iff_eq_base) 55 56 57subsection \<open>Nth Root\<close> 58 59text \<open> 60 We define roots of negative reals such that \<open>root n (- x) = - root n x\<close>. 61 This allows us to omit side conditions from many theorems. 62\<close> 63 64lemma inj_sgn_power: 65 assumes "0 < n" 66 shows "inj (\<lambda>y. sgn y * \<bar>y\<bar>^n :: real)" 67 (is "inj ?f") 68proof (rule injI) 69 have x: "(0 < a \<and> b < 0) \<or> (a < 0 \<and> 0 < b) \<Longrightarrow> a \<noteq> b" for a b :: real 70 by auto 71 fix x y 72 assume "?f x = ?f y" 73 with power_eq_iff_eq_base[of n "\<bar>x\<bar>" "\<bar>y\<bar>"] \<open>0 < n\<close> show "x = y" 74 by (cases rule: linorder_cases[of 0 x, case_product linorder_cases[of 0 y]]) 75 (simp_all add: x) 76qed 77 78lemma sgn_power_injE: 79 "sgn a * \<bar>a\<bar> ^ n = x \<Longrightarrow> x = sgn b * \<bar>b\<bar> ^ n \<Longrightarrow> 0 < n \<Longrightarrow> a = b" 80 for a b :: real 81 using inj_sgn_power[THEN injD, of n a b] by simp 82 83definition root :: "nat \<Rightarrow> real \<Rightarrow> real" 84 where "root n x = (if n = 0 then 0 else the_inv (\<lambda>y. sgn y * \<bar>y\<bar>^n) x)" 85 86lemma root_0 [simp]: "root 0 x = 0" 87 by (simp add: root_def) 88 89lemma root_sgn_power: "0 < n \<Longrightarrow> root n (sgn y * \<bar>y\<bar>^n) = y" 90 using the_inv_f_f[OF inj_sgn_power] by (simp add: root_def) 91 92lemma sgn_power_root: 93 assumes "0 < n" 94 shows "sgn (root n x) * \<bar>(root n x)\<bar>^n = x" 95 (is "?f (root n x) = x") 96proof (cases "x = 0") 97 case True 98 with assms root_sgn_power[of n 0] show ?thesis 99 by simp 100next 101 case False 102 with realpow_pos_nth[OF \<open>0 < n\<close>, of "\<bar>x\<bar>"] 103 obtain r where "0 < r" "r ^ n = \<bar>x\<bar>" 104 by auto 105 with \<open>x \<noteq> 0\<close> have S: "x \<in> range ?f" 106 by (intro image_eqI[of _ _ "sgn x * r"]) 107 (auto simp: abs_mult sgn_mult power_mult_distrib abs_sgn_eq mult_sgn_abs) 108 from \<open>0 < n\<close> f_the_inv_into_f[OF inj_sgn_power[OF \<open>0 < n\<close>] this] show ?thesis 109 by (simp add: root_def) 110qed 111 112lemma split_root: "P (root n x) \<longleftrightarrow> (n = 0 \<longrightarrow> P 0) \<and> (0 < n \<longrightarrow> (\<forall>y. sgn y * \<bar>y\<bar>^n = x \<longrightarrow> P y))" 113proof (cases "n = 0") 114 case True 115 then show ?thesis by simp 116next 117 case False 118 then show ?thesis 119 by simp (metis root_sgn_power sgn_power_root) 120qed 121 122lemma real_root_zero [simp]: "root n 0 = 0" 123 by (simp split: split_root add: sgn_zero_iff) 124 125lemma real_root_minus: "root n (- x) = - root n x" 126 by (clarsimp split: split_root elim!: sgn_power_injE simp: sgn_minus) 127 128lemma real_root_less_mono: "0 < n \<Longrightarrow> x < y \<Longrightarrow> root n x < root n y" 129proof (clarsimp split: split_root) 130 have *: "0 < b \<Longrightarrow> a < 0 \<Longrightarrow> \<not> a > b" for a b :: real 131 by auto 132 fix a b :: real 133 assume "0 < n" "sgn a * \<bar>a\<bar> ^ n < sgn b * \<bar>b\<bar> ^ n" 134 then show "a < b" 135 using power_less_imp_less_base[of a n b] 136 power_less_imp_less_base[of "- b" n "- a"] 137 by (simp add: sgn_real_def * [of "a ^ n" "- ((- b) ^ n)"] 138 split: if_split_asm) 139qed 140 141lemma real_root_gt_zero: "0 < n \<Longrightarrow> 0 < x \<Longrightarrow> 0 < root n x" 142 using real_root_less_mono[of n 0 x] by simp 143 144lemma real_root_ge_zero: "0 \<le> x \<Longrightarrow> 0 \<le> root n x" 145 using real_root_gt_zero[of n x] 146 by (cases "n = 0") (auto simp add: le_less) 147 148lemma real_root_pow_pos: "0 < n \<Longrightarrow> 0 < x \<Longrightarrow> root n x ^ n = x" (* TODO: rename *) 149 using sgn_power_root[of n x] real_root_gt_zero[of n x] by simp 150 151lemma real_root_pow_pos2 [simp]: "0 < n \<Longrightarrow> 0 \<le> x \<Longrightarrow> root n x ^ n = x" (* TODO: rename *) 152 by (auto simp add: order_le_less real_root_pow_pos) 153 154lemma sgn_root: "0 < n \<Longrightarrow> sgn (root n x) = sgn x" 155 by (auto split: split_root simp: sgn_real_def) 156 157lemma odd_real_root_pow: "odd n \<Longrightarrow> root n x ^ n = x" 158 using sgn_power_root[of n x] 159 by (simp add: odd_pos sgn_real_def split: if_split_asm) 160 161lemma real_root_power_cancel: "0 < n \<Longrightarrow> 0 \<le> x \<Longrightarrow> root n (x ^ n) = x" 162 using root_sgn_power[of n x] by (auto simp add: le_less power_0_left) 163 164lemma odd_real_root_power_cancel: "odd n \<Longrightarrow> root n (x ^ n) = x" 165 using root_sgn_power[of n x] 166 by (simp add: odd_pos sgn_real_def power_0_left split: if_split_asm) 167 168lemma real_root_pos_unique: "0 < n \<Longrightarrow> 0 \<le> y \<Longrightarrow> y ^ n = x \<Longrightarrow> root n x = y" 169 using root_sgn_power[of n y] by (auto simp add: le_less power_0_left) 170 171lemma odd_real_root_unique: "odd n \<Longrightarrow> y ^ n = x \<Longrightarrow> root n x = y" 172 by (erule subst, rule odd_real_root_power_cancel) 173 174lemma real_root_one [simp]: "0 < n \<Longrightarrow> root n 1 = 1" 175 by (simp add: real_root_pos_unique) 176 177text \<open>Root function is strictly monotonic, hence injective.\<close> 178 179lemma real_root_le_mono: "0 < n \<Longrightarrow> x \<le> y \<Longrightarrow> root n x \<le> root n y" 180 by (auto simp add: order_le_less real_root_less_mono) 181 182lemma real_root_less_iff [simp]: "0 < n \<Longrightarrow> root n x < root n y \<longleftrightarrow> x < y" 183 by (cases "x < y") (simp_all add: real_root_less_mono linorder_not_less real_root_le_mono) 184 185lemma real_root_le_iff [simp]: "0 < n \<Longrightarrow> root n x \<le> root n y \<longleftrightarrow> x \<le> y" 186 by (cases "x \<le> y") (simp_all add: real_root_le_mono linorder_not_le real_root_less_mono) 187 188lemma real_root_eq_iff [simp]: "0 < n \<Longrightarrow> root n x = root n y \<longleftrightarrow> x = y" 189 by (simp add: order_eq_iff) 190 191lemmas real_root_gt_0_iff [simp] = real_root_less_iff [where x=0, simplified] 192lemmas real_root_lt_0_iff [simp] = real_root_less_iff [where y=0, simplified] 193lemmas real_root_ge_0_iff [simp] = real_root_le_iff [where x=0, simplified] 194lemmas real_root_le_0_iff [simp] = real_root_le_iff [where y=0, simplified] 195lemmas real_root_eq_0_iff [simp] = real_root_eq_iff [where y=0, simplified] 196 197lemma real_root_gt_1_iff [simp]: "0 < n \<Longrightarrow> 1 < root n y \<longleftrightarrow> 1 < y" 198 using real_root_less_iff [where x=1] by simp 199 200lemma real_root_lt_1_iff [simp]: "0 < n \<Longrightarrow> root n x < 1 \<longleftrightarrow> x < 1" 201 using real_root_less_iff [where y=1] by simp 202 203lemma real_root_ge_1_iff [simp]: "0 < n \<Longrightarrow> 1 \<le> root n y \<longleftrightarrow> 1 \<le> y" 204 using real_root_le_iff [where x=1] by simp 205 206lemma real_root_le_1_iff [simp]: "0 < n \<Longrightarrow> root n x \<le> 1 \<longleftrightarrow> x \<le> 1" 207 using real_root_le_iff [where y=1] by simp 208 209lemma real_root_eq_1_iff [simp]: "0 < n \<Longrightarrow> root n x = 1 \<longleftrightarrow> x = 1" 210 using real_root_eq_iff [where y=1] by simp 211 212 213text \<open>Roots of multiplication and division.\<close> 214 215lemma real_root_mult: "root n (x * y) = root n x * root n y" 216 by (auto split: split_root elim!: sgn_power_injE 217 simp: sgn_mult abs_mult power_mult_distrib) 218 219lemma real_root_inverse: "root n (inverse x) = inverse (root n x)" 220 by (auto split: split_root elim!: sgn_power_injE 221 simp: power_inverse) 222 223lemma real_root_divide: "root n (x / y) = root n x / root n y" 224 by (simp add: divide_inverse real_root_mult real_root_inverse) 225 226lemma real_root_abs: "0 < n \<Longrightarrow> root n \<bar>x\<bar> = \<bar>root n x\<bar>" 227 by (simp add: abs_if real_root_minus) 228 229lemma root_abs_power: "n > 0 \<Longrightarrow> abs (root n (y ^n)) = abs y" 230 using root_sgn_power [of n] 231 by (metis abs_ge_zero power_abs real_root_abs real_root_power_cancel) 232 233lemma real_root_power: "0 < n \<Longrightarrow> root n (x ^ k) = root n x ^ k" 234 by (induct k) (simp_all add: real_root_mult) 235 236 237text \<open>Roots of roots.\<close> 238 239lemma real_root_Suc_0 [simp]: "root (Suc 0) x = x" 240 by (simp add: odd_real_root_unique) 241 242lemma real_root_mult_exp: "root (m * n) x = root m (root n x)" 243 by (auto split: split_root elim!: sgn_power_injE 244 simp: sgn_zero_iff sgn_mult power_mult[symmetric] 245 abs_mult power_mult_distrib abs_sgn_eq) 246 247lemma real_root_commute: "root m (root n x) = root n (root m x)" 248 by (simp add: real_root_mult_exp [symmetric] mult.commute) 249 250 251text \<open>Monotonicity in first argument.\<close> 252 253lemma real_root_strict_decreasing: 254 assumes "0 < n" "n < N" "1 < x" 255 shows "root N x < root n x" 256proof - 257 from assms have "root n (root N x) ^ n < root N (root n x) ^ N" 258 by (simp add: real_root_commute power_strict_increasing del: real_root_pow_pos2) 259 with assms show ?thesis by simp 260qed 261 262lemma real_root_strict_increasing: 263 assumes "0 < n" "n < N" "0 < x" "x < 1" 264 shows "root n x < root N x" 265proof - 266 from assms have "root N (root n x) ^ N < root n (root N x) ^ n" 267 by (simp add: real_root_commute power_strict_decreasing del: real_root_pow_pos2) 268 with assms show ?thesis by simp 269qed 270 271lemma real_root_decreasing: "0 < n \<Longrightarrow> n \<le> N \<Longrightarrow> 1 \<le> x \<Longrightarrow> root N x \<le> root n x" 272 by (auto simp add: order_le_less real_root_strict_decreasing) 273 274lemma real_root_increasing: "0 < n \<Longrightarrow> n \<le> N \<Longrightarrow> 0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> root n x \<le> root N x" 275 by (auto simp add: order_le_less real_root_strict_increasing) 276 277 278text \<open>Continuity and derivatives.\<close> 279 280lemma isCont_real_root: "isCont (root n) x" 281proof (cases "n > 0") 282 case True 283 let ?f = "\<lambda>y::real. sgn y * \<bar>y\<bar>^n" 284 have "continuous_on ({0..} \<union> {.. 0}) (\<lambda>x. if 0 < x then x ^ n else - ((-x) ^ n) :: real)" 285 using True by (intro continuous_on_If continuous_intros) auto 286 then have "continuous_on UNIV ?f" 287 by (rule continuous_on_cong[THEN iffD1, rotated 2]) (auto simp: not_less le_less True) 288 then have [simp]: "isCont ?f x" for x 289 by (simp add: continuous_on_eq_continuous_at) 290 have "isCont (root n) (?f (root n x))" 291 by (rule isCont_inverse_function [where f="?f" and d=1]) (auto simp: root_sgn_power True) 292 then show ?thesis 293 by (simp add: sgn_power_root True) 294next 295 case False 296 then show ?thesis 297 by (simp add: root_def[abs_def]) 298qed 299 300lemma tendsto_real_root [tendsto_intros]: 301 "(f \<longlongrightarrow> x) F \<Longrightarrow> ((\<lambda>x. root n (f x)) \<longlongrightarrow> root n x) F" 302 using isCont_tendsto_compose[OF isCont_real_root, of f x F] . 303 304lemma continuous_real_root [continuous_intros]: 305 "continuous F f \<Longrightarrow> continuous F (\<lambda>x. root n (f x))" 306 unfolding continuous_def by (rule tendsto_real_root) 307 308lemma continuous_on_real_root [continuous_intros]: 309 "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. root n (f x))" 310 unfolding continuous_on_def by (auto intro: tendsto_real_root) 311 312lemma DERIV_real_root: 313 assumes n: "0 < n" 314 and x: "0 < x" 315 shows "DERIV (root n) x :> inverse (real n * root n x ^ (n - Suc 0))" 316proof (rule DERIV_inverse_function) 317 show "0 < x" 318 using x . 319 show "x < x + 1" 320 by simp 321 show "DERIV (\<lambda>x. x ^ n) (root n x) :> real n * root n x ^ (n - Suc 0)" 322 by (rule DERIV_pow) 323 show "real n * root n x ^ (n - Suc 0) \<noteq> 0" 324 using n x by simp 325 show "isCont (root n) x" 326 by (rule isCont_real_root) 327qed (use n in auto) 328 329lemma DERIV_odd_real_root: 330 assumes n: "odd n" 331 and x: "x \<noteq> 0" 332 shows "DERIV (root n) x :> inverse (real n * root n x ^ (n - Suc 0))" 333proof (rule DERIV_inverse_function) 334 show "x - 1 < x" "x < x + 1" 335 by auto 336 show "DERIV (\<lambda>x. x ^ n) (root n x) :> real n * root n x ^ (n - Suc 0)" 337 by (rule DERIV_pow) 338 show "real n * root n x ^ (n - Suc 0) \<noteq> 0" 339 using odd_pos [OF n] x by simp 340 show "isCont (root n) x" 341 by (rule isCont_real_root) 342qed (use n odd_real_root_pow in auto) 343 344lemma DERIV_even_real_root: 345 assumes n: "0 < n" 346 and "even n" 347 and x: "x < 0" 348 shows "DERIV (root n) x :> inverse (- real n * root n x ^ (n - Suc 0))" 349proof (rule DERIV_inverse_function) 350 show "x - 1 < x" 351 by simp 352 show "x < 0" 353 using x . 354 show "- (root n y ^ n) = y" if "x - 1 < y" and "y < 0" for y 355 proof - 356 have "root n (-y) ^ n = -y" 357 using that \<open>0 < n\<close> by simp 358 with real_root_minus and \<open>even n\<close> 359 show "- (root n y ^ n) = y" by simp 360 qed 361 show "DERIV (\<lambda>x. - (x ^ n)) (root n x) :> - real n * root n x ^ (n - Suc 0)" 362 by (auto intro!: derivative_eq_intros) 363 show "- real n * root n x ^ (n - Suc 0) \<noteq> 0" 364 using n x by simp 365 show "isCont (root n) x" 366 by (rule isCont_real_root) 367qed 368 369lemma DERIV_real_root_generic: 370 assumes "0 < n" 371 and "x \<noteq> 0" 372 and "even n \<Longrightarrow> 0 < x \<Longrightarrow> D = inverse (real n * root n x ^ (n - Suc 0))" 373 and "even n \<Longrightarrow> x < 0 \<Longrightarrow> D = - inverse (real n * root n x ^ (n - Suc 0))" 374 and "odd n \<Longrightarrow> D = inverse (real n * root n x ^ (n - Suc 0))" 375 shows "DERIV (root n) x :> D" 376 using assms 377 by (cases "even n", cases "0 < x") 378 (auto intro: DERIV_real_root[THEN DERIV_cong] 379 DERIV_odd_real_root[THEN DERIV_cong] 380 DERIV_even_real_root[THEN DERIV_cong]) 381 382lemma power_tendsto_0_iff [simp]: 383 fixes f :: "'a \<Rightarrow> real" 384 assumes "n > 0" 385 shows "((\<lambda>x. f x ^ n) \<longlongrightarrow> 0) F \<longleftrightarrow> (f \<longlongrightarrow> 0) F" 386proof - 387 have "((\<lambda>x. \<bar>root n (f x ^ n)\<bar>) \<longlongrightarrow> 0) F \<Longrightarrow> (f \<longlongrightarrow> 0) F" 388 by (auto simp: assms root_abs_power tendsto_rabs_zero_iff) 389 then have "((\<lambda>x. f x ^ n) \<longlongrightarrow> 0) F \<Longrightarrow> (f \<longlongrightarrow> 0) F" 390 by (metis tendsto_real_root abs_0 real_root_zero tendsto_rabs) 391 with assms show ?thesis 392 by (auto simp: tendsto_null_power) 393qed 394 395subsection \<open>Square Root\<close> 396 397definition sqrt :: "real \<Rightarrow> real" 398 where "sqrt = root 2" 399 400lemma pos2: "0 < (2::nat)" 401 by simp 402 403lemma real_sqrt_unique: "y\<^sup>2 = x \<Longrightarrow> 0 \<le> y \<Longrightarrow> sqrt x = y" 404 unfolding sqrt_def by (rule real_root_pos_unique [OF pos2]) 405 406lemma real_sqrt_abs [simp]: "sqrt (x\<^sup>2) = \<bar>x\<bar>" 407 by (metis power2_abs abs_ge_zero real_sqrt_unique) 408 409lemma real_sqrt_pow2 [simp]: "0 \<le> x \<Longrightarrow> (sqrt x)\<^sup>2 = x" 410 unfolding sqrt_def by (rule real_root_pow_pos2 [OF pos2]) 411 412lemma real_sqrt_pow2_iff [simp]: "(sqrt x)\<^sup>2 = x \<longleftrightarrow> 0 \<le> x" 413 by (metis real_sqrt_pow2 zero_le_power2) 414 415lemma real_sqrt_zero [simp]: "sqrt 0 = 0" 416 unfolding sqrt_def by (rule real_root_zero) 417 418lemma real_sqrt_one [simp]: "sqrt 1 = 1" 419 unfolding sqrt_def by (rule real_root_one [OF pos2]) 420 421lemma real_sqrt_four [simp]: "sqrt 4 = 2" 422 using real_sqrt_abs[of 2] by simp 423 424lemma real_sqrt_minus: "sqrt (- x) = - sqrt x" 425 unfolding sqrt_def by (rule real_root_minus) 426 427lemma real_sqrt_mult: "sqrt (x * y) = sqrt x * sqrt y" 428 unfolding sqrt_def by (rule real_root_mult) 429 430lemma real_sqrt_mult_self[simp]: "sqrt a * sqrt a = \<bar>a\<bar>" 431 using real_sqrt_abs[of a] unfolding power2_eq_square real_sqrt_mult . 432 433lemma real_sqrt_inverse: "sqrt (inverse x) = inverse (sqrt x)" 434 unfolding sqrt_def by (rule real_root_inverse) 435 436lemma real_sqrt_divide: "sqrt (x / y) = sqrt x / sqrt y" 437 unfolding sqrt_def by (rule real_root_divide) 438 439lemma real_sqrt_power: "sqrt (x ^ k) = sqrt x ^ k" 440 unfolding sqrt_def by (rule real_root_power [OF pos2]) 441 442lemma real_sqrt_gt_zero: "0 < x \<Longrightarrow> 0 < sqrt x" 443 unfolding sqrt_def by (rule real_root_gt_zero [OF pos2]) 444 445lemma real_sqrt_ge_zero: "0 \<le> x \<Longrightarrow> 0 \<le> sqrt x" 446 unfolding sqrt_def by (rule real_root_ge_zero) 447 448lemma real_sqrt_less_mono: "x < y \<Longrightarrow> sqrt x < sqrt y" 449 unfolding sqrt_def by (rule real_root_less_mono [OF pos2]) 450 451lemma real_sqrt_le_mono: "x \<le> y \<Longrightarrow> sqrt x \<le> sqrt y" 452 unfolding sqrt_def by (rule real_root_le_mono [OF pos2]) 453 454lemma real_sqrt_less_iff [simp]: "sqrt x < sqrt y \<longleftrightarrow> x < y" 455 unfolding sqrt_def by (rule real_root_less_iff [OF pos2]) 456 457lemma real_sqrt_le_iff [simp]: "sqrt x \<le> sqrt y \<longleftrightarrow> x \<le> y" 458 unfolding sqrt_def by (rule real_root_le_iff [OF pos2]) 459 460lemma real_sqrt_eq_iff [simp]: "sqrt x = sqrt y \<longleftrightarrow> x = y" 461 unfolding sqrt_def by (rule real_root_eq_iff [OF pos2]) 462 463lemma real_less_lsqrt: "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> x < y\<^sup>2 \<Longrightarrow> sqrt x < y" 464 using real_sqrt_less_iff[of x "y\<^sup>2"] by simp 465 466lemma real_le_lsqrt: "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> x \<le> y\<^sup>2 \<Longrightarrow> sqrt x \<le> y" 467 using real_sqrt_le_iff[of x "y\<^sup>2"] by simp 468 469lemma real_le_rsqrt: "x\<^sup>2 \<le> y \<Longrightarrow> x \<le> sqrt y" 470 using real_sqrt_le_mono[of "x\<^sup>2" y] by simp 471 472lemma real_less_rsqrt: "x\<^sup>2 < y \<Longrightarrow> x < sqrt y" 473 using real_sqrt_less_mono[of "x\<^sup>2" y] by simp 474 475lemma real_sqrt_power_even: 476 assumes "even n" "x \<ge> 0" 477 shows "sqrt x ^ n = x ^ (n div 2)" 478proof - 479 from assms obtain k where "n = 2*k" by (auto elim!: evenE) 480 with assms show ?thesis by (simp add: power_mult) 481qed 482 483lemma sqrt_le_D: "sqrt x \<le> y \<Longrightarrow> x \<le> y\<^sup>2" 484 by (meson not_le real_less_rsqrt) 485 486lemma sqrt_ge_absD: "\<bar>x\<bar> \<le> sqrt y \<Longrightarrow> x\<^sup>2 \<le> y" 487 using real_sqrt_le_iff[of "x\<^sup>2"] by simp 488 489lemma sqrt_even_pow2: 490 assumes n: "even n" 491 shows "sqrt (2 ^ n) = 2 ^ (n div 2)" 492proof - 493 from n obtain m where m: "n = 2 * m" .. 494 from m have "sqrt (2 ^ n) = sqrt ((2 ^ m)\<^sup>2)" 495 by (simp only: power_mult[symmetric] mult.commute) 496 then show ?thesis 497 using m by simp 498qed 499 500lemmas real_sqrt_gt_0_iff [simp] = real_sqrt_less_iff [where x=0, unfolded real_sqrt_zero] 501lemmas real_sqrt_lt_0_iff [simp] = real_sqrt_less_iff [where y=0, unfolded real_sqrt_zero] 502lemmas real_sqrt_ge_0_iff [simp] = real_sqrt_le_iff [where x=0, unfolded real_sqrt_zero] 503lemmas real_sqrt_le_0_iff [simp] = real_sqrt_le_iff [where y=0, unfolded real_sqrt_zero] 504lemmas real_sqrt_eq_0_iff [simp] = real_sqrt_eq_iff [where y=0, unfolded real_sqrt_zero] 505 506lemmas real_sqrt_gt_1_iff [simp] = real_sqrt_less_iff [where x=1, unfolded real_sqrt_one] 507lemmas real_sqrt_lt_1_iff [simp] = real_sqrt_less_iff [where y=1, unfolded real_sqrt_one] 508lemmas real_sqrt_ge_1_iff [simp] = real_sqrt_le_iff [where x=1, unfolded real_sqrt_one] 509lemmas real_sqrt_le_1_iff [simp] = real_sqrt_le_iff [where y=1, unfolded real_sqrt_one] 510lemmas real_sqrt_eq_1_iff [simp] = real_sqrt_eq_iff [where y=1, unfolded real_sqrt_one] 511 512lemma sqrt_add_le_add_sqrt: 513 assumes "0 \<le> x" "0 \<le> y" 514 shows "sqrt (x + y) \<le> sqrt x + sqrt y" 515 by (rule power2_le_imp_le) (simp_all add: power2_sum assms) 516 517lemma isCont_real_sqrt: "isCont sqrt x" 518 unfolding sqrt_def by (rule isCont_real_root) 519 520lemma tendsto_real_sqrt [tendsto_intros]: 521 "(f \<longlongrightarrow> x) F \<Longrightarrow> ((\<lambda>x. sqrt (f x)) \<longlongrightarrow> sqrt x) F" 522 unfolding sqrt_def by (rule tendsto_real_root) 523 524lemma continuous_real_sqrt [continuous_intros]: 525 "continuous F f \<Longrightarrow> continuous F (\<lambda>x. sqrt (f x))" 526 unfolding sqrt_def by (rule continuous_real_root) 527 528lemma continuous_on_real_sqrt [continuous_intros]: 529 "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. sqrt (f x))" 530 unfolding sqrt_def by (rule continuous_on_real_root) 531 532lemma DERIV_real_sqrt_generic: 533 assumes "x \<noteq> 0" 534 and "x > 0 \<Longrightarrow> D = inverse (sqrt x) / 2" 535 and "x < 0 \<Longrightarrow> D = - inverse (sqrt x) / 2" 536 shows "DERIV sqrt x :> D" 537 using assms unfolding sqrt_def 538 by (auto intro!: DERIV_real_root_generic) 539 540lemma DERIV_real_sqrt: "0 < x \<Longrightarrow> DERIV sqrt x :> inverse (sqrt x) / 2" 541 using DERIV_real_sqrt_generic by simp 542 543declare 544 DERIV_real_sqrt_generic[THEN DERIV_chain2, derivative_intros] 545 DERIV_real_root_generic[THEN DERIV_chain2, derivative_intros] 546 547lemmas has_derivative_real_sqrt[derivative_intros] = DERIV_real_sqrt[THEN DERIV_compose_FDERIV] 548 549lemma not_real_square_gt_zero [simp]: "\<not> 0 < x * x \<longleftrightarrow> x = 0" 550 for x :: real 551 apply auto 552 using linorder_less_linear [where x = x and y = 0] 553 apply (simp add: zero_less_mult_iff) 554 done 555 556lemma real_sqrt_abs2 [simp]: "sqrt (x * x) = \<bar>x\<bar>" 557 apply (subst power2_eq_square [symmetric]) 558 apply (rule real_sqrt_abs) 559 done 560 561lemma real_inv_sqrt_pow2: "0 < x \<Longrightarrow> (inverse (sqrt x))\<^sup>2 = inverse x" 562 by (simp add: power_inverse) 563 564lemma real_sqrt_eq_zero_cancel: "0 \<le> x \<Longrightarrow> sqrt x = 0 \<Longrightarrow> x = 0" 565 by simp 566 567lemma real_sqrt_ge_one: "1 \<le> x \<Longrightarrow> 1 \<le> sqrt x" 568 by simp 569 570lemma sqrt_divide_self_eq: 571 assumes nneg: "0 \<le> x" 572 shows "sqrt x / x = inverse (sqrt x)" 573proof (cases "x = 0") 574 case True 575 then show ?thesis by simp 576next 577 case False 578 then have pos: "0 < x" 579 using nneg by arith 580 show ?thesis 581 proof (rule right_inverse_eq [THEN iffD1, symmetric]) 582 show "sqrt x / x \<noteq> 0" 583 by (simp add: divide_inverse nneg False) 584 show "inverse (sqrt x) / (sqrt x / x) = 1" 585 by (simp add: divide_inverse mult.assoc [symmetric] 586 power2_eq_square [symmetric] real_inv_sqrt_pow2 pos False) 587 qed 588qed 589 590lemma real_div_sqrt: "0 \<le> x \<Longrightarrow> x / sqrt x = sqrt x" 591 by (cases "x = 0") (simp_all add: sqrt_divide_self_eq [of x] field_simps) 592 593lemma real_divide_square_eq [simp]: "(r * a) / (r * r) = a / r" 594 for a r :: real 595 by (cases "r = 0") (simp_all add: divide_inverse ac_simps) 596 597lemma lemma_real_divide_sqrt_less: "0 < u \<Longrightarrow> u / sqrt 2 < u" 598 by (simp add: divide_less_eq) 599 600lemma four_x_squared: "4 * x\<^sup>2 = (2 * x)\<^sup>2" 601 for x :: real 602 by (simp add: power2_eq_square) 603 604lemma sqrt_at_top: "LIM x at_top. sqrt x :: real :> at_top" 605 by (rule filterlim_at_top_at_top[where Q="\<lambda>x. True" and P="\<lambda>x. 0 < x" and g="power2"]) 606 (auto intro: eventually_gt_at_top) 607 608 609subsection \<open>Square Root of Sum of Squares\<close> 610 611lemma sum_squares_bound: "2 * x * y \<le> x\<^sup>2 + y\<^sup>2" 612 for x y :: "'a::linordered_field" 613proof - 614 have "(x - y)\<^sup>2 = x * x - 2 * x * y + y * y" 615 by algebra 616 then have "0 \<le> x\<^sup>2 - 2 * x * y + y\<^sup>2" 617 by (metis sum_power2_ge_zero zero_le_double_add_iff_zero_le_single_add power2_eq_square) 618 then show ?thesis 619 by arith 620qed 621 622lemma arith_geo_mean: 623 fixes u :: "'a::linordered_field" 624 assumes "u\<^sup>2 = x * y" "x \<ge> 0" "y \<ge> 0" 625 shows "u \<le> (x + y)/2" 626 apply (rule power2_le_imp_le) 627 using sum_squares_bound assms 628 apply (auto simp: zero_le_mult_iff) 629 apply (auto simp: algebra_simps power2_eq_square) 630 done 631 632lemma arith_geo_mean_sqrt: 633 fixes x :: real 634 assumes "x \<ge> 0" "y \<ge> 0" 635 shows "sqrt (x * y) \<le> (x + y)/2" 636 apply (rule arith_geo_mean) 637 using assms 638 apply (auto simp: zero_le_mult_iff) 639 done 640 641lemma real_sqrt_sum_squares_mult_ge_zero [simp]: "0 \<le> sqrt ((x\<^sup>2 + y\<^sup>2) * (xa\<^sup>2 + ya\<^sup>2))" 642 by (metis real_sqrt_ge_0_iff split_mult_pos_le sum_power2_ge_zero) 643 644lemma real_sqrt_sum_squares_mult_squared_eq [simp]: 645 "(sqrt ((x\<^sup>2 + y\<^sup>2) * (xa\<^sup>2 + ya\<^sup>2)))\<^sup>2 = (x\<^sup>2 + y\<^sup>2) * (xa\<^sup>2 + ya\<^sup>2)" 646 by (simp add: zero_le_mult_iff) 647 648lemma real_sqrt_sum_squares_eq_cancel: "sqrt (x\<^sup>2 + y\<^sup>2) = x \<Longrightarrow> y = 0" 649 by (drule arg_cong [where f = "\<lambda>x. x\<^sup>2"]) simp 650 651lemma real_sqrt_sum_squares_eq_cancel2: "sqrt (x\<^sup>2 + y\<^sup>2) = y \<Longrightarrow> x = 0" 652 by (drule arg_cong [where f = "\<lambda>x. x\<^sup>2"]) simp 653 654lemma real_sqrt_sum_squares_ge1 [simp]: "x \<le> sqrt (x\<^sup>2 + y\<^sup>2)" 655 by (rule power2_le_imp_le) simp_all 656 657lemma real_sqrt_sum_squares_ge2 [simp]: "y \<le> sqrt (x\<^sup>2 + y\<^sup>2)" 658 by (rule power2_le_imp_le) simp_all 659 660lemma real_sqrt_ge_abs1 [simp]: "\<bar>x\<bar> \<le> sqrt (x\<^sup>2 + y\<^sup>2)" 661 by (rule power2_le_imp_le) simp_all 662 663lemma real_sqrt_ge_abs2 [simp]: "\<bar>y\<bar> \<le> sqrt (x\<^sup>2 + y\<^sup>2)" 664 by (rule power2_le_imp_le) simp_all 665 666lemma le_real_sqrt_sumsq [simp]: "x \<le> sqrt (x * x + y * y)" 667 by (simp add: power2_eq_square [symmetric]) 668 669lemma sqrt_sum_squares_le_sum: 670 "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> sqrt (x\<^sup>2 + y\<^sup>2) \<le> x + y" 671 by (rule power2_le_imp_le) (simp_all add: power2_sum) 672 673lemma L2_set_mult_ineq_lemma: 674 fixes a b c d :: real 675 shows "2 * (a * c) * (b * d) \<le> a\<^sup>2 * d\<^sup>2 + b\<^sup>2 * c\<^sup>2" 676proof - 677 have "0 \<le> (a * d - b * c)\<^sup>2" by simp 678 also have "\<dots> = a\<^sup>2 * d\<^sup>2 + b\<^sup>2 * c\<^sup>2 - 2 * (a * d) * (b * c)" 679 by (simp only: power2_diff power_mult_distrib) 680 also have "\<dots> = a\<^sup>2 * d\<^sup>2 + b\<^sup>2 * c\<^sup>2 - 2 * (a * c) * (b * d)" 681 by simp 682 finally show "2 * (a * c) * (b * d) \<le> a\<^sup>2 * d\<^sup>2 + b\<^sup>2 * c\<^sup>2" 683 by simp 684qed 685 686lemma sqrt_sum_squares_le_sum_abs: "sqrt (x\<^sup>2 + y\<^sup>2) \<le> \<bar>x\<bar> + \<bar>y\<bar>" 687 by (rule power2_le_imp_le) (simp_all add: power2_sum) 688 689lemma real_sqrt_sum_squares_triangle_ineq: 690 "sqrt ((a + c)\<^sup>2 + (b + d)\<^sup>2) \<le> sqrt (a\<^sup>2 + b\<^sup>2) + sqrt (c\<^sup>2 + d\<^sup>2)" 691proof - 692 have "(a * c + b * d) \<le> (sqrt (a\<^sup>2 + b\<^sup>2) * sqrt (c\<^sup>2 + d\<^sup>2))" 693 by (rule power2_le_imp_le) (simp_all add: power2_sum power_mult_distrib ring_distribs L2_set_mult_ineq_lemma add.commute) 694 then have "(a + c)\<^sup>2 + (b + d)\<^sup>2 \<le> (sqrt (a\<^sup>2 + b\<^sup>2) + sqrt (c\<^sup>2 + d\<^sup>2))\<^sup>2" 695 by (simp add: power2_sum) 696 then show ?thesis 697 by (auto intro: power2_le_imp_le) 698qed 699 700lemma real_sqrt_sum_squares_less: "\<bar>x\<bar> < u / sqrt 2 \<Longrightarrow> \<bar>y\<bar> < u / sqrt 2 \<Longrightarrow> sqrt (x\<^sup>2 + y\<^sup>2) < u" 701 apply (rule power2_less_imp_less) 702 apply simp 703 apply (drule power_strict_mono [OF _ abs_ge_zero pos2]) 704 apply (drule power_strict_mono [OF _ abs_ge_zero pos2]) 705 apply (simp add: power_divide) 706 apply (drule order_le_less_trans [OF abs_ge_zero]) 707 apply (simp add: zero_less_divide_iff) 708 done 709 710lemma sqrt2_less_2: "sqrt 2 < (2::real)" 711 by (metis not_less not_less_iff_gr_or_eq numeral_less_iff real_sqrt_four 712 real_sqrt_le_iff semiring_norm(75) semiring_norm(78) semiring_norm(85)) 713 714lemma sqrt_sum_squares_half_less: 715 "x < u/2 \<Longrightarrow> y < u/2 \<Longrightarrow> 0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> sqrt (x\<^sup>2 + y\<^sup>2) < u" 716 apply (rule real_sqrt_sum_squares_less) 717 apply (auto simp add: abs_if field_simps) 718 apply (rule le_less_trans [where y = "x*2"]) 719 using less_eq_real_def sqrt2_less_2 apply force 720 apply assumption 721 apply (rule le_less_trans [where y = "y*2"]) 722 using less_eq_real_def sqrt2_less_2 mult_le_cancel_left 723 apply auto 724 done 725 726lemma LIMSEQ_root: "(\<lambda>n. root n n) \<longlonglongrightarrow> 1" 727proof - 728 define x where "x n = root n n - 1" for n 729 have "x \<longlonglongrightarrow> sqrt 0" 730 proof (rule tendsto_sandwich[OF _ _ tendsto_const]) 731 show "(\<lambda>x. sqrt (2 / x)) \<longlonglongrightarrow> sqrt 0" 732 by (intro tendsto_intros tendsto_divide_0[OF tendsto_const] filterlim_mono[OF filterlim_real_sequentially]) 733 (simp_all add: at_infinity_eq_at_top_bot) 734 have "x n \<le> sqrt (2 / real n)" if "2 < n" for n :: nat 735 proof - 736 have "1 + (real (n - 1) * n) / 2 * (x n)\<^sup>2 = 1 + of_nat (n choose 2) * (x n)\<^sup>2" 737 by (auto simp add: choose_two field_char_0_class.of_nat_div mod_eq_0_iff_dvd) 738 also have "\<dots> \<le> (\<Sum>k\<in>{0, 2}. of_nat (n choose k) * x n^k)" 739 by (simp add: x_def) 740 also have "\<dots> \<le> (\<Sum>k\<le>n. of_nat (n choose k) * x n^k)" 741 using \<open>2 < n\<close> 742 by (intro sum_mono2) (auto intro!: mult_nonneg_nonneg zero_le_power simp: x_def le_diff_eq) 743 also have "\<dots> = (x n + 1) ^ n" 744 by (simp add: binomial_ring) 745 also have "\<dots> = n" 746 using \<open>2 < n\<close> by (simp add: x_def) 747 finally have "real (n - 1) * (real n / 2 * (x n)\<^sup>2) \<le> real (n - 1) * 1" 748 by simp 749 then have "(x n)\<^sup>2 \<le> 2 / real n" 750 using \<open>2 < n\<close> unfolding mult_le_cancel_left by (simp add: field_simps) 751 from real_sqrt_le_mono[OF this] show ?thesis 752 by simp 753 qed 754 then show "eventually (\<lambda>n. x n \<le> sqrt (2 / real n)) sequentially" 755 by (auto intro!: exI[of _ 3] simp: eventually_sequentially) 756 show "eventually (\<lambda>n. sqrt 0 \<le> x n) sequentially" 757 by (auto intro!: exI[of _ 1] simp: eventually_sequentially le_diff_eq x_def) 758 qed 759 from tendsto_add[OF this tendsto_const[of 1]] show ?thesis 760 by (simp add: x_def) 761qed 762 763lemma LIMSEQ_root_const: 764 assumes "0 < c" 765 shows "(\<lambda>n. root n c) \<longlonglongrightarrow> 1" 766proof - 767 have ge_1: "(\<lambda>n. root n c) \<longlonglongrightarrow> 1" if "1 \<le> c" for c :: real 768 proof - 769 define x where "x n = root n c - 1" for n 770 have "x \<longlonglongrightarrow> 0" 771 proof (rule tendsto_sandwich[OF _ _ tendsto_const]) 772 show "(\<lambda>n. c / n) \<longlonglongrightarrow> 0" 773 by (intro tendsto_divide_0[OF tendsto_const] filterlim_mono[OF filterlim_real_sequentially]) 774 (simp_all add: at_infinity_eq_at_top_bot) 775 have "x n \<le> c / n" if "1 < n" for n :: nat 776 proof - 777 have "1 + x n * n = 1 + of_nat (n choose 1) * x n^1" 778 by (simp add: choose_one) 779 also have "\<dots> \<le> (\<Sum>k\<in>{0, 1}. of_nat (n choose k) * x n^k)" 780 by (simp add: x_def) 781 also have "\<dots> \<le> (\<Sum>k\<le>n. of_nat (n choose k) * x n^k)" 782 using \<open>1 < n\<close> \<open>1 \<le> c\<close> 783 by (intro sum_mono2) 784 (auto intro!: mult_nonneg_nonneg zero_le_power simp: x_def le_diff_eq) 785 also have "\<dots> = (x n + 1) ^ n" 786 by (simp add: binomial_ring) 787 also have "\<dots> = c" 788 using \<open>1 < n\<close> \<open>1 \<le> c\<close> by (simp add: x_def) 789 finally show ?thesis 790 using \<open>1 \<le> c\<close> \<open>1 < n\<close> by (simp add: field_simps) 791 qed 792 then show "eventually (\<lambda>n. x n \<le> c / n) sequentially" 793 by (auto intro!: exI[of _ 3] simp: eventually_sequentially) 794 show "eventually (\<lambda>n. 0 \<le> x n) sequentially" 795 using \<open>1 \<le> c\<close> 796 by (auto intro!: exI[of _ 1] simp: eventually_sequentially le_diff_eq x_def) 797 qed 798 from tendsto_add[OF this tendsto_const[of 1]] show ?thesis 799 by (simp add: x_def) 800 qed 801 show ?thesis 802 proof (cases "1 \<le> c") 803 case True 804 with ge_1 show ?thesis by blast 805 next 806 case False 807 with \<open>0 < c\<close> have "1 \<le> 1 / c" 808 by simp 809 then have "(\<lambda>n. 1 / root n (1 / c)) \<longlonglongrightarrow> 1 / 1" 810 by (intro tendsto_divide tendsto_const ge_1 \<open>1 \<le> 1 / c\<close> one_neq_zero) 811 then show ?thesis 812 by (rule filterlim_cong[THEN iffD1, rotated 3]) 813 (auto intro!: exI[of _ 1] simp: eventually_sequentially real_root_divide) 814 qed 815qed 816 817 818text "Legacy theorem names:" 819lemmas real_root_pos2 = real_root_power_cancel 820lemmas real_root_pos_pos = real_root_gt_zero [THEN order_less_imp_le] 821lemmas real_root_pos_pos_le = real_root_ge_zero 822lemmas real_sqrt_eq_zero_cancel_iff = real_sqrt_eq_0_iff 823 824end 825