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