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