src/HOL/Transcendental.thy
 author paulson Thu Apr 30 15:28:01 2015 +0100 (2015-04-30) changeset 60162 645058aa9d6f parent 60155 91477b3a2d6b child 60182 e1ea5a6379c9 permissions -rw-r--r--
tidying some messy proofs
 wenzelm@32960 ` 1` ```(* Title: HOL/Transcendental.thy ``` wenzelm@32960 ` 2` ``` Author: Jacques D. Fleuriot, University of Cambridge, University of Edinburgh ``` wenzelm@32960 ` 3` ``` Author: Lawrence C Paulson ``` hoelzl@51527 ` 4` ``` Author: Jeremy Avigad ``` paulson@12196 ` 5` ```*) ``` paulson@12196 ` 6` wenzelm@58889 ` 7` ```section{*Power Series, Transcendental Functions etc.*} ``` paulson@15077 ` 8` nipkow@15131 ` 9` ```theory Transcendental ``` lp15@59669 ` 10` ```imports Binomial Series Deriv NthRoot ``` nipkow@15131 ` 11` ```begin ``` paulson@15077 ` 12` lp15@60155 ` 13` ```lemma reals_Archimedean4: ``` lp15@60155 ` 14` ``` assumes "0 < y" "0 \ x" ``` lp15@60155 ` 15` ``` obtains n where "real n * y \ x" "x < real (Suc n) * y" ``` lp15@60155 ` 16` ``` using floor_correct [of "x/y"] assms ``` lp15@60155 ` 17` ``` by (auto simp: Real.real_of_nat_Suc field_simps intro: that [of "nat (floor (x/y))"]) ``` lp15@60155 ` 18` lp15@59730 ` 19` ```lemma of_real_fact [simp]: "of_real (fact n) = fact n" ``` lp15@59730 ` 20` ``` by (metis of_nat_fact of_real_of_nat_eq) ``` lp15@59730 ` 21` lp15@59730 ` 22` ```lemma real_fact_nat [simp]: "real (fact n :: nat) = fact n" ``` lp15@59730 ` 23` ``` by (simp add: real_of_nat_def) ``` lp15@59730 ` 24` lp15@59731 ` 25` ```lemma real_fact_int [simp]: "real (fact n :: int) = fact n" ``` lp15@59731 ` 26` ``` by (metis of_int_of_nat_eq of_nat_fact real_of_int_def) ``` lp15@59731 ` 27` hoelzl@57025 ` 28` ```lemma root_test_convergence: ``` hoelzl@57025 ` 29` ``` fixes f :: "nat \ 'a::banach" ``` hoelzl@57025 ` 30` ``` assumes f: "(\n. root n (norm (f n))) ----> x" -- "could be weakened to lim sup" ``` hoelzl@57025 ` 31` ``` assumes "x < 1" ``` hoelzl@57025 ` 32` ``` shows "summable f" ``` hoelzl@57025 ` 33` ```proof - ``` hoelzl@57025 ` 34` ``` have "0 \ x" ``` hoelzl@57025 ` 35` ``` by (rule LIMSEQ_le[OF tendsto_const f]) (auto intro!: exI[of _ 1]) ``` hoelzl@57025 ` 36` ``` from `x < 1` obtain z where z: "x < z" "z < 1" ``` hoelzl@57025 ` 37` ``` by (metis dense) ``` hoelzl@57025 ` 38` ``` from f `x < z` ``` hoelzl@57025 ` 39` ``` have "eventually (\n. root n (norm (f n)) < z) sequentially" ``` hoelzl@57025 ` 40` ``` by (rule order_tendstoD) ``` hoelzl@57025 ` 41` ``` then have "eventually (\n. norm (f n) \ z^n) sequentially" ``` hoelzl@57025 ` 42` ``` using eventually_ge_at_top ``` hoelzl@57025 ` 43` ``` proof eventually_elim ``` hoelzl@57025 ` 44` ``` fix n assume less: "root n (norm (f n)) < z" and n: "1 \ n" ``` hoelzl@57025 ` 45` ``` from power_strict_mono[OF less, of n] n ``` hoelzl@57025 ` 46` ``` show "norm (f n) \ z ^ n" ``` hoelzl@57025 ` 47` ``` by simp ``` hoelzl@57025 ` 48` ``` qed ``` hoelzl@57025 ` 49` ``` then show "summable f" ``` hoelzl@57025 ` 50` ``` unfolding eventually_sequentially ``` hoelzl@57025 ` 51` ``` using z `0 \ x` by (auto intro!: summable_comparison_test[OF _ summable_geometric]) ``` hoelzl@57025 ` 52` ```qed ``` hoelzl@57025 ` 53` huffman@29164 ` 54` ```subsection {* Properties of Power Series *} ``` paulson@15077 ` 55` lp15@60141 ` 56` ```lemma powser_zero: ``` lp15@60141 ` 57` ``` fixes f :: "nat \ 'a::real_normed_algebra_1" ``` lp15@60141 ` 58` ``` shows "(\n. f n * 0 ^ n) = f 0" ``` lp15@60141 ` 59` ```proof - ``` lp15@60141 ` 60` ``` have "(\n<1. f n * 0 ^ n) = (\n. f n * 0 ^ n)" ``` lp15@60141 ` 61` ``` by (subst suminf_finite[where N="{0}"]) (auto simp: power_0_left) ``` lp15@60141 ` 62` ``` thus ?thesis unfolding One_nat_def by simp ``` lp15@60141 ` 63` ```qed ``` lp15@60141 ` 64` lp15@60141 ` 65` ```lemma powser_sums_zero: ``` lp15@60141 ` 66` ``` fixes a :: "nat \ 'a::real_normed_div_algebra" ``` lp15@60141 ` 67` ``` shows "(\n. a n * 0^n) sums a 0" ``` lp15@60141 ` 68` ``` using sums_finite [of "{0}" "\n. a n * 0 ^ n"] ``` lp15@60141 ` 69` ``` by simp ``` lp15@60141 ` 70` lp15@60141 ` 71` ```text{*Power series has a circle or radius of convergence: if it sums for @{term ``` wenzelm@53079 ` 72` ``` x}, then it sums absolutely for @{term z} with @{term "\z\ < \x\"}.*} ``` paulson@15077 ` 73` paulson@15077 ` 74` ```lemma powser_insidea: ``` huffman@53599 ` 75` ``` fixes x z :: "'a::real_normed_div_algebra" ``` lp15@59730 ` 76` ``` assumes 1: "summable (\n. f n * x^n)" ``` wenzelm@53079 ` 77` ``` and 2: "norm z < norm x" ``` huffman@23082 ` 78` ``` shows "summable (\n. norm (f n * z ^ n))" ``` huffman@20849 ` 79` ```proof - ``` huffman@20849 ` 80` ``` from 2 have x_neq_0: "x \ 0" by clarsimp ``` lp15@59730 ` 81` ``` from 1 have "(\n. f n * x^n) ----> 0" ``` huffman@20849 ` 82` ``` by (rule summable_LIMSEQ_zero) ``` lp15@59730 ` 83` ``` hence "convergent (\n. f n * x^n)" ``` huffman@20849 ` 84` ``` by (rule convergentI) ``` lp15@59730 ` 85` ``` hence "Cauchy (\n. f n * x^n)" ``` huffman@44726 ` 86` ``` by (rule convergent_Cauchy) ``` lp15@59730 ` 87` ``` hence "Bseq (\n. f n * x^n)" ``` huffman@20849 ` 88` ``` by (rule Cauchy_Bseq) ``` lp15@59730 ` 89` ``` then obtain K where 3: "0 < K" and 4: "\n. norm (f n * x^n) \ K" ``` huffman@20849 ` 90` ``` by (simp add: Bseq_def, safe) ``` huffman@23082 ` 91` ``` have "\N. \n\N. norm (norm (f n * z ^ n)) \ ``` lp15@59730 ` 92` ``` K * norm (z ^ n) * inverse (norm (x^n))" ``` huffman@20849 ` 93` ``` proof (intro exI allI impI) ``` wenzelm@53079 ` 94` ``` fix n::nat ``` wenzelm@53079 ` 95` ``` assume "0 \ n" ``` lp15@59730 ` 96` ``` have "norm (norm (f n * z ^ n)) * norm (x^n) = ``` lp15@59730 ` 97` ``` norm (f n * x^n) * norm (z ^ n)" ``` huffman@23082 ` 98` ``` by (simp add: norm_mult abs_mult) ``` huffman@23082 ` 99` ``` also have "\ \ K * norm (z ^ n)" ``` huffman@23082 ` 100` ``` by (simp only: mult_right_mono 4 norm_ge_zero) ``` lp15@59730 ` 101` ``` also have "\ = K * norm (z ^ n) * (inverse (norm (x^n)) * norm (x^n))" ``` huffman@20849 ` 102` ``` by (simp add: x_neq_0) ``` lp15@59730 ` 103` ``` also have "\ = K * norm (z ^ n) * inverse (norm (x^n)) * norm (x^n)" ``` haftmann@57512 ` 104` ``` by (simp only: mult.assoc) ``` huffman@23082 ` 105` ``` finally show "norm (norm (f n * z ^ n)) \ ``` lp15@59730 ` 106` ``` K * norm (z ^ n) * inverse (norm (x^n))" ``` huffman@20849 ` 107` ``` by (simp add: mult_le_cancel_right x_neq_0) ``` huffman@20849 ` 108` ``` qed ``` lp15@59730 ` 109` ``` moreover have "summable (\n. K * norm (z ^ n) * inverse (norm (x^n)))" ``` huffman@20849 ` 110` ``` proof - ``` huffman@23082 ` 111` ``` from 2 have "norm (norm (z * inverse x)) < 1" ``` huffman@23082 ` 112` ``` using x_neq_0 ``` huffman@53599 ` 113` ``` by (simp add: norm_mult nonzero_norm_inverse divide_inverse [where 'a=real, symmetric]) ``` huffman@23082 ` 114` ``` hence "summable (\n. norm (z * inverse x) ^ n)" ``` huffman@20849 ` 115` ``` by (rule summable_geometric) ``` huffman@23082 ` 116` ``` hence "summable (\n. K * norm (z * inverse x) ^ n)" ``` huffman@20849 ` 117` ``` by (rule summable_mult) ``` lp15@59730 ` 118` ``` thus "summable (\n. K * norm (z ^ n) * inverse (norm (x^n)))" ``` huffman@23082 ` 119` ``` using x_neq_0 ``` huffman@23082 ` 120` ``` by (simp add: norm_mult nonzero_norm_inverse power_mult_distrib ``` haftmann@57512 ` 121` ``` power_inverse norm_power mult.assoc) ``` huffman@20849 ` 122` ``` qed ``` huffman@23082 ` 123` ``` ultimately show "summable (\n. norm (f n * z ^ n))" ``` huffman@20849 ` 124` ``` by (rule summable_comparison_test) ``` huffman@20849 ` 125` ```qed ``` paulson@15077 ` 126` paulson@15229 ` 127` ```lemma powser_inside: ``` huffman@53599 ` 128` ``` fixes f :: "nat \ 'a::{real_normed_div_algebra,banach}" ``` wenzelm@53079 ` 129` ``` shows ``` lp15@59730 ` 130` ``` "summable (\n. f n * (x^n)) \ norm z < norm x \ ``` wenzelm@53079 ` 131` ``` summable (\n. f n * (z ^ n))" ``` wenzelm@53079 ` 132` ``` by (rule powser_insidea [THEN summable_norm_cancel]) ``` wenzelm@53079 ` 133` lp15@60141 ` 134` ```lemma powser_times_n_limit_0: ``` lp15@60141 ` 135` ``` fixes x :: "'a::{real_normed_div_algebra,banach}" ``` lp15@60141 ` 136` ``` assumes "norm x < 1" ``` lp15@60141 ` 137` ``` shows "(\n. of_nat n * x ^ n) ----> 0" ``` lp15@60141 ` 138` ```proof - ``` lp15@60141 ` 139` ``` have "norm x / (1 - norm x) \ 0" ``` lp15@60141 ` 140` ``` using assms ``` lp15@60141 ` 141` ``` by (auto simp: divide_simps) ``` lp15@60141 ` 142` ``` moreover obtain N where N: "norm x / (1 - norm x) < of_int N" ``` lp15@60141 ` 143` ``` using ex_le_of_int ``` lp15@60141 ` 144` ``` by (meson ex_less_of_int) ``` lp15@60141 ` 145` ``` ultimately have N0: "N>0" ``` lp15@60141 ` 146` ``` by auto ``` lp15@60141 ` 147` ``` then have *: "real (N + 1) * norm x / real N < 1" ``` lp15@60141 ` 148` ``` using N assms ``` lp15@60141 ` 149` ``` by (auto simp: field_simps) ``` lp15@60141 ` 150` ``` { fix n::nat ``` lp15@60141 ` 151` ``` assume "N \ int n" ``` lp15@60141 ` 152` ``` then have "real N * real_of_nat (Suc n) \ real_of_nat n * real (1 + N)" ``` lp15@60141 ` 153` ``` by (simp add: algebra_simps) ``` lp15@60141 ` 154` ``` then have "(real N * real_of_nat (Suc n)) * (norm x * norm (x ^ n)) ``` lp15@60141 ` 155` ``` \ (real_of_nat n * real (1 + N)) * (norm x * norm (x ^ n))" ``` lp15@60141 ` 156` ``` using N0 mult_mono by fastforce ``` lp15@60141 ` 157` ``` then have "real N * (norm x * (real_of_nat (Suc n) * norm (x ^ n))) ``` lp15@60141 ` 158` ``` \ real_of_nat n * (norm x * (real (1 + N) * norm (x ^ n)))" ``` lp15@60141 ` 159` ``` by (simp add: algebra_simps) ``` lp15@60141 ` 160` ``` } note ** = this ``` lp15@60141 ` 161` ``` show ?thesis using * ``` lp15@60141 ` 162` ``` apply (rule summable_LIMSEQ_zero [OF summable_ratio_test, where N1="nat N"]) ``` lp15@60141 ` 163` ``` apply (simp add: N0 norm_mult nat_le_iff field_simps power_Suc ** ``` lp15@60141 ` 164` ``` del: of_nat_Suc real_of_int_add) ``` lp15@60141 ` 165` ``` done ``` lp15@60141 ` 166` ```qed ``` lp15@60141 ` 167` lp15@60141 ` 168` ```corollary lim_n_over_pown: ``` lp15@60141 ` 169` ``` fixes x :: "'a::{real_normed_field,banach}" ``` lp15@60141 ` 170` ``` shows "1 < norm x \ ((\n. of_nat n / x^n) ---> 0) sequentially" ``` lp15@60141 ` 171` ```using powser_times_n_limit_0 [of "inverse x"] ``` lp15@60141 ` 172` ```by (simp add: norm_divide divide_simps) ``` lp15@60141 ` 173` lp15@60155 ` 174` ```lemma lim_1_over_n: "((\n. 1 / of_nat n) ---> (0::'a\real_normed_field)) sequentially" ``` lp15@60155 ` 175` ``` apply (clarsimp simp: lim_sequentially norm_divide dist_norm divide_simps) ``` lp15@60155 ` 176` ``` apply (auto simp: mult_ac dest!: ex_less_of_nat_mult [of _ 1]) ``` lp15@60155 ` 177` ``` by (metis le_eq_less_or_eq less_trans linordered_comm_semiring_strict_class.comm_mult_strict_left_mono ``` lp15@60155 ` 178` ``` of_nat_less_0_iff of_nat_less_iff zero_less_mult_iff zero_less_one) ``` lp15@60155 ` 179` lp15@60155 ` 180` ```lemma lim_inverse_n: "((\n. inverse(of_nat n)) ---> (0::'a\real_normed_field)) sequentially" ``` lp15@60155 ` 181` ``` using lim_1_over_n ``` lp15@60155 ` 182` ``` by (simp add: inverse_eq_divide) ``` lp15@60155 ` 183` wenzelm@53079 ` 184` ```lemma sum_split_even_odd: ``` wenzelm@53079 ` 185` ``` fixes f :: "nat \ real" ``` wenzelm@53079 ` 186` ``` shows ``` hoelzl@56193 ` 187` ``` "(\i<2 * n. if even i then f i else g i) = ``` hoelzl@56193 ` 188` ``` (\iii<2 * Suc n. if even i then f i else g i) = ``` hoelzl@56193 ` 195` ``` (\ii = (\ii real" ``` wenzelm@53079 ` 204` ``` assumes "g sums x" ``` hoelzl@29803 ` 205` ``` shows "(\ n. if even n then 0 else g ((n - 1) div 2)) sums x" ``` hoelzl@29803 ` 206` ``` unfolding sums_def ``` hoelzl@29803 ` 207` ```proof (rule LIMSEQ_I) ``` wenzelm@53079 ` 208` ``` fix r :: real ``` wenzelm@53079 ` 209` ``` assume "0 < r" ``` hoelzl@29803 ` 210` ``` from `g sums x`[unfolded sums_def, THEN LIMSEQ_D, OF this] ``` hoelzl@56193 ` 211` ``` obtain no where no_eq: "\ n. n \ no \ (norm (setsum g {.. 2 * no" ``` wenzelm@53079 ` 217` ``` hence "m div 2 \ no" by auto ``` hoelzl@56193 ` 218` ``` have sum_eq: "?SUM (2 * (m div 2)) = setsum g {..< m div 2}" ``` hoelzl@29803 ` 219` ``` using sum_split_even_odd by auto ``` wenzelm@53079 ` 220` ``` hence "(norm (?SUM (2 * (m div 2)) - x) < r)" ``` wenzelm@53079 ` 221` ``` using no_eq unfolding sum_eq using `m div 2 \ no` by auto ``` hoelzl@29803 ` 222` ``` moreover ``` hoelzl@29803 ` 223` ``` have "?SUM (2 * (m div 2)) = ?SUM m" ``` hoelzl@29803 ` 224` ``` proof (cases "even m") ``` wenzelm@53079 ` 225` ``` case True ``` haftmann@58710 ` 226` ``` then show ?thesis by (auto simp add: even_two_times_div_two) ``` hoelzl@29803 ` 227` ``` next ``` wenzelm@53079 ` 228` ``` case False ``` haftmann@58834 ` 229` ``` then have eq: "Suc (2 * (m div 2)) = m" by simp ``` hoelzl@29803 ` 230` ``` hence "even (2 * (m div 2))" using `odd m` by auto ``` hoelzl@29803 ` 231` ``` have "?SUM m = ?SUM (Suc (2 * (m div 2)))" unfolding eq .. ``` hoelzl@29803 ` 232` ``` also have "\ = ?SUM (2 * (m div 2))" using `even (2 * (m div 2))` by auto ``` hoelzl@29803 ` 233` ``` finally show ?thesis by auto ``` hoelzl@29803 ` 234` ``` qed ``` hoelzl@29803 ` 235` ``` ultimately have "(norm (?SUM m - x) < r)" by auto ``` hoelzl@29803 ` 236` ``` } ``` hoelzl@29803 ` 237` ``` thus "\ no. \ m \ no. norm (?SUM m - x) < r" by blast ``` hoelzl@29803 ` 238` ```qed ``` hoelzl@29803 ` 239` wenzelm@53079 ` 240` ```lemma sums_if: ``` wenzelm@53079 ` 241` ``` fixes g :: "nat \ real" ``` wenzelm@53079 ` 242` ``` assumes "g sums x" and "f sums y" ``` hoelzl@29803 ` 243` ``` shows "(\ n. if even n then f (n div 2) else g ((n - 1) div 2)) sums (x + y)" ``` hoelzl@29803 ` 244` ```proof - ``` hoelzl@29803 ` 245` ``` let ?s = "\ n. if even n then 0 else f ((n - 1) div 2)" ``` wenzelm@53079 ` 246` ``` { ``` wenzelm@53079 ` 247` ``` fix B T E ``` wenzelm@53079 ` 248` ``` have "(if B then (0 :: real) else E) + (if B then T else 0) = (if B then T else E)" ``` wenzelm@53079 ` 249` ``` by (cases B) auto ``` wenzelm@53079 ` 250` ``` } note if_sum = this ``` wenzelm@53079 ` 251` ``` have g_sums: "(\ n. if even n then 0 else g ((n - 1) div 2)) sums x" ``` wenzelm@53079 ` 252` ``` using sums_if'[OF `g sums x`] . ``` hoelzl@41970 ` 253` ``` { ``` wenzelm@41550 ` 254` ``` have if_eq: "\B T E. (if \ B then T else E) = (if B then E else T)" by auto ``` hoelzl@29803 ` 255` hoelzl@29803 ` 256` ``` have "?s sums y" using sums_if'[OF `f sums y`] . ``` hoelzl@41970 ` 257` ``` from this[unfolded sums_def, THEN LIMSEQ_Suc] ``` hoelzl@29803 ` 258` ``` have "(\ n. if even n then f (n div 2) else 0) sums y" ``` haftmann@57418 ` 259` ``` by (simp add: lessThan_Suc_eq_insert_0 image_iff setsum.reindex if_eq sums_def cong del: if_cong) ``` wenzelm@53079 ` 260` ``` } ``` wenzelm@53079 ` 261` ``` from sums_add[OF g_sums this] show ?thesis unfolding if_sum . ``` hoelzl@29803 ` 262` ```qed ``` hoelzl@29803 ` 263` hoelzl@29803 ` 264` ```subsection {* Alternating series test / Leibniz formula *} ``` hoelzl@29803 ` 265` hoelzl@29803 ` 266` ```lemma sums_alternating_upper_lower: ``` hoelzl@29803 ` 267` ``` fixes a :: "nat \ real" ``` hoelzl@29803 ` 268` ``` assumes mono: "\n. a (Suc n) \ a n" and a_pos: "\n. 0 \ a n" and "a ----> 0" ``` haftmann@58410 ` 269` ``` shows "\l. ((\n. (\i<2*n. (- 1)^i*a i) \ l) \ (\ n. \i<2*n. (- 1)^i*a i) ----> l) \ ``` haftmann@58410 ` 270` ``` ((\n. l \ (\i<2*n + 1. (- 1)^i*a i)) \ (\ n. \i<2*n + 1. (- 1)^i*a i) ----> l)" ``` hoelzl@29803 ` 271` ``` (is "\l. ((\n. ?f n \ l) \ _) \ ((\n. l \ ?g n) \ _)") ``` wenzelm@53079 ` 272` ```proof (rule nested_sequence_unique) ``` huffman@30082 ` 273` ``` have fg_diff: "\n. ?f n - ?g n = - a (2 * n)" unfolding One_nat_def by auto ``` hoelzl@29803 ` 274` wenzelm@53079 ` 275` ``` show "\n. ?f n \ ?f (Suc n)" ``` wenzelm@53079 ` 276` ``` proof ``` wenzelm@53079 ` 277` ``` fix n ``` wenzelm@53079 ` 278` ``` show "?f n \ ?f (Suc n)" using mono[of "2*n"] by auto ``` wenzelm@53079 ` 279` ``` qed ``` wenzelm@53079 ` 280` ``` show "\n. ?g (Suc n) \ ?g n" ``` wenzelm@53079 ` 281` ``` proof ``` wenzelm@53079 ` 282` ``` fix n ``` wenzelm@53079 ` 283` ``` show "?g (Suc n) \ ?g n" using mono[of "Suc (2*n)"] ``` wenzelm@53079 ` 284` ``` unfolding One_nat_def by auto ``` wenzelm@53079 ` 285` ``` qed ``` wenzelm@53079 ` 286` ``` show "\n. ?f n \ ?g n" ``` wenzelm@53079 ` 287` ``` proof ``` wenzelm@53079 ` 288` ``` fix n ``` wenzelm@53079 ` 289` ``` show "?f n \ ?g n" using fg_diff a_pos ``` wenzelm@53079 ` 290` ``` unfolding One_nat_def by auto ``` hoelzl@29803 ` 291` ``` qed ``` wenzelm@53079 ` 292` ``` show "(\n. ?f n - ?g n) ----> 0" unfolding fg_diff ``` wenzelm@53079 ` 293` ``` proof (rule LIMSEQ_I) ``` wenzelm@53079 ` 294` ``` fix r :: real ``` wenzelm@53079 ` 295` ``` assume "0 < r" ``` wenzelm@53079 ` 296` ``` with `a ----> 0`[THEN LIMSEQ_D] obtain N where "\ n. n \ N \ norm (a n - 0) < r" ``` wenzelm@53079 ` 297` ``` by auto ``` wenzelm@53079 ` 298` ``` hence "\n \ N. norm (- a (2 * n) - 0) < r" by auto ``` wenzelm@53079 ` 299` ``` thus "\N. \n \ N. norm (- a (2 * n) - 0) < r" by auto ``` wenzelm@53079 ` 300` ``` qed ``` hoelzl@41970 ` 301` ```qed ``` hoelzl@29803 ` 302` wenzelm@53079 ` 303` ```lemma summable_Leibniz': ``` wenzelm@53079 ` 304` ``` fixes a :: "nat \ real" ``` wenzelm@53079 ` 305` ``` assumes a_zero: "a ----> 0" ``` wenzelm@53079 ` 306` ``` and a_pos: "\ n. 0 \ a n" ``` wenzelm@53079 ` 307` ``` and a_monotone: "\ n. a (Suc n) \ a n" ``` hoelzl@29803 ` 308` ``` shows summable: "summable (\ n. (-1)^n * a n)" ``` hoelzl@56193 ` 309` ``` and "\n. (\i<2*n. (-1)^i*a i) \ (\i. (-1)^i*a i)" ``` hoelzl@56193 ` 310` ``` and "(\n. \i<2*n. (-1)^i*a i) ----> (\i. (-1)^i*a i)" ``` hoelzl@56193 ` 311` ``` and "\n. (\i. (-1)^i*a i) \ (\i<2*n+1. (-1)^i*a i)" ``` hoelzl@56193 ` 312` ``` and "(\n. \i<2*n+1. (-1)^i*a i) ----> (\i. (-1)^i*a i)" ``` hoelzl@29803 ` 313` ```proof - ``` wenzelm@53079 ` 314` ``` let ?S = "\n. (-1)^n * a n" ``` hoelzl@56193 ` 315` ``` let ?P = "\n. \i n. ?f n \ l" ``` wenzelm@53079 ` 320` ``` and "?f ----> l" ``` wenzelm@53079 ` 321` ``` and above_l: "\ n. l \ ?g n" ``` wenzelm@53079 ` 322` ``` and "?g ----> l" ``` hoelzl@29803 ` 323` ``` using sums_alternating_upper_lower[OF a_monotone a_pos a_zero] by blast ``` hoelzl@41970 ` 324` hoelzl@56193 ` 325` ``` let ?Sa = "\m. \n l" ``` hoelzl@29803 ` 327` ``` proof (rule LIMSEQ_I) ``` wenzelm@53079 ` 328` ``` fix r :: real ``` wenzelm@53079 ` 329` ``` assume "0 < r" ``` hoelzl@41970 ` 330` ``` with `?f ----> l`[THEN LIMSEQ_D] ``` hoelzl@29803 ` 331` ``` obtain f_no where f: "\ n. n \ f_no \ norm (?f n - l) < r" by auto ``` hoelzl@29803 ` 332` hoelzl@41970 ` 333` ``` from `0 < r` `?g ----> l`[THEN LIMSEQ_D] ``` hoelzl@29803 ` 334` ``` obtain g_no where g: "\ n. n \ g_no \ norm (?g n - l) < r" by auto ``` hoelzl@29803 ` 335` wenzelm@53079 ` 336` ``` { ``` wenzelm@53079 ` 337` ``` fix n :: nat ``` wenzelm@53079 ` 338` ``` assume "n \ (max (2 * f_no) (2 * g_no))" ``` wenzelm@53079 ` 339` ``` hence "n \ 2 * f_no" and "n \ 2 * g_no" by auto ``` hoelzl@29803 ` 340` ``` have "norm (?Sa n - l) < r" ``` hoelzl@29803 ` 341` ``` proof (cases "even n") ``` wenzelm@53079 ` 342` ``` case True ``` haftmann@58710 ` 343` ``` then have n_eq: "2 * (n div 2) = n" by (simp add: even_two_times_div_two) ``` wenzelm@53079 ` 344` ``` with `n \ 2 * f_no` have "n div 2 \ f_no" ``` wenzelm@53079 ` 345` ``` by auto ``` wenzelm@53079 ` 346` ``` from f[OF this] show ?thesis ``` wenzelm@53079 ` 347` ``` unfolding n_eq atLeastLessThanSuc_atLeastAtMost . ``` hoelzl@29803 ` 348` ``` next ``` wenzelm@53079 ` 349` ``` case False ``` wenzelm@53079 ` 350` ``` hence "even (n - 1)" by simp ``` haftmann@58710 ` 351` ``` then have n_eq: "2 * ((n - 1) div 2) = n - 1" ``` haftmann@58710 ` 352` ``` by (simp add: even_two_times_div_two) ``` wenzelm@53079 ` 353` ``` hence range_eq: "n - 1 + 1 = n" ``` wenzelm@53079 ` 354` ``` using odd_pos[OF False] by auto ``` wenzelm@53079 ` 355` wenzelm@53079 ` 356` ``` from n_eq `n \ 2 * g_no` have "(n - 1) div 2 \ g_no" ``` wenzelm@53079 ` 357` ``` by auto ``` wenzelm@53079 ` 358` ``` from g[OF this] show ?thesis ``` hoelzl@56193 ` 359` ``` unfolding n_eq range_eq . ``` hoelzl@29803 ` 360` ``` qed ``` hoelzl@29803 ` 361` ``` } ``` wenzelm@53079 ` 362` ``` thus "\no. \n \ no. norm (?Sa n - l) < r" by blast ``` hoelzl@29803 ` 363` ``` qed ``` wenzelm@53079 ` 364` ``` hence sums_l: "(\i. (-1)^i * a i) sums l" ``` hoelzl@56193 ` 365` ``` unfolding sums_def . ``` hoelzl@29803 ` 366` ``` thus "summable ?S" using summable_def by auto ``` hoelzl@29803 ` 367` hoelzl@29803 ` 368` ``` have "l = suminf ?S" using sums_unique[OF sums_l] . ``` hoelzl@29803 ` 369` wenzelm@53079 ` 370` ``` fix n ``` wenzelm@53079 ` 371` ``` show "suminf ?S \ ?g n" ``` wenzelm@53079 ` 372` ``` unfolding sums_unique[OF sums_l, symmetric] using above_l by auto ``` wenzelm@53079 ` 373` ``` show "?f n \ suminf ?S" ``` wenzelm@53079 ` 374` ``` unfolding sums_unique[OF sums_l, symmetric] using below_l by auto ``` wenzelm@53079 ` 375` ``` show "?g ----> suminf ?S" ``` wenzelm@53079 ` 376` ``` using `?g ----> l` `l = suminf ?S` by auto ``` wenzelm@53079 ` 377` ``` show "?f ----> suminf ?S" ``` wenzelm@53079 ` 378` ``` using `?f ----> l` `l = suminf ?S` by auto ``` hoelzl@29803 ` 379` ```qed ``` hoelzl@29803 ` 380` wenzelm@53079 ` 381` ```theorem summable_Leibniz: ``` wenzelm@53079 ` 382` ``` fixes a :: "nat \ real" ``` hoelzl@29803 ` 383` ``` assumes a_zero: "a ----> 0" and "monoseq a" ``` hoelzl@29803 ` 384` ``` shows "summable (\ n. (-1)^n * a n)" (is "?summable") ``` wenzelm@53079 ` 385` ``` and "0 < a 0 \ ``` haftmann@58410 ` 386` ``` (\n. (\i. (- 1)^i*a i) \ { \i<2*n. (- 1)^i * a i .. \i<2*n+1. (- 1)^i * a i})" (is "?pos") ``` wenzelm@53079 ` 387` ``` and "a 0 < 0 \ ``` haftmann@58410 ` 388` ``` (\n. (\i. (- 1)^i*a i) \ { \i<2*n+1. (- 1)^i * a i .. \i<2*n. (- 1)^i * a i})" (is "?neg") ``` haftmann@58410 ` 389` ``` and "(\n. \i<2*n. (- 1)^i*a i) ----> (\i. (- 1)^i*a i)" (is "?f") ``` haftmann@58410 ` 390` ``` and "(\n. \i<2*n+1. (- 1)^i*a i) ----> (\i. (- 1)^i*a i)" (is "?g") ``` hoelzl@29803 ` 391` ```proof - ``` hoelzl@29803 ` 392` ``` have "?summable \ ?pos \ ?neg \ ?f \ ?g" ``` hoelzl@29803 ` 393` ``` proof (cases "(\ n. 0 \ a n) \ (\m. \n\m. a n \ a m)") ``` hoelzl@29803 ` 394` ``` case True ``` wenzelm@53079 ` 395` ``` hence ord: "\n m. m \ n \ a n \ a m" and ge0: "\ n. 0 \ a n" ``` wenzelm@53079 ` 396` ``` by auto ``` wenzelm@53079 ` 397` ``` { ``` wenzelm@53079 ` 398` ``` fix n ``` wenzelm@53079 ` 399` ``` have "a (Suc n) \ a n" ``` wenzelm@53079 ` 400` ``` using ord[where n="Suc n" and m=n] by auto ``` wenzelm@53079 ` 401` ``` } note mono = this ``` wenzelm@53079 ` 402` ``` note leibniz = summable_Leibniz'[OF `a ----> 0` ge0] ``` hoelzl@29803 ` 403` ``` from leibniz[OF mono] ``` hoelzl@29803 ` 404` ``` show ?thesis using `0 \ a 0` by auto ``` hoelzl@29803 ` 405` ``` next ``` hoelzl@29803 ` 406` ``` let ?a = "\ n. - a n" ``` hoelzl@29803 ` 407` ``` case False ``` hoelzl@29803 ` 408` ``` with monoseq_le[OF `monoseq a` `a ----> 0`] ``` hoelzl@29803 ` 409` ``` have "(\ n. a n \ 0) \ (\m. \n\m. a m \ a n)" by auto ``` wenzelm@53079 ` 410` ``` hence ord: "\n m. m \ n \ ?a n \ ?a m" and ge0: "\ n. 0 \ ?a n" ``` wenzelm@53079 ` 411` ``` by auto ``` wenzelm@53079 ` 412` ``` { ``` wenzelm@53079 ` 413` ``` fix n ``` wenzelm@53079 ` 414` ``` have "?a (Suc n) \ ?a n" using ord[where n="Suc n" and m=n] ``` wenzelm@53079 ` 415` ``` by auto ``` wenzelm@53079 ` 416` ``` } note monotone = this ``` wenzelm@53079 ` 417` ``` note leibniz = ``` wenzelm@53079 ` 418` ``` summable_Leibniz'[OF _ ge0, of "\x. x", ``` wenzelm@53079 ` 419` ``` OF tendsto_minus[OF `a ----> 0`, unfolded minus_zero] monotone] ``` wenzelm@53079 ` 420` ``` have "summable (\ n. (-1)^n * ?a n)" ``` wenzelm@53079 ` 421` ``` using leibniz(1) by auto ``` wenzelm@53079 ` 422` ``` then obtain l where "(\ n. (-1)^n * ?a n) sums l" ``` wenzelm@53079 ` 423` ``` unfolding summable_def by auto ``` wenzelm@53079 ` 424` ``` from this[THEN sums_minus] have "(\ n. (-1)^n * a n) sums -l" ``` wenzelm@53079 ` 425` ``` by auto ``` hoelzl@29803 ` 426` ``` hence ?summable unfolding summable_def by auto ``` hoelzl@29803 ` 427` ``` moreover ``` wenzelm@53079 ` 428` ``` have "\a b :: real. \- a - - b\ = \a - b\" ``` wenzelm@53079 ` 429` ``` unfolding minus_diff_minus by auto ``` hoelzl@41970 ` 430` hoelzl@29803 ` 431` ``` from suminf_minus[OF leibniz(1), unfolded mult_minus_right minus_minus] ``` haftmann@58410 ` 432` ``` have move_minus: "(\n. - ((- 1) ^ n * a n)) = - (\n. (- 1) ^ n * a n)" ``` wenzelm@53079 ` 433` ``` by auto ``` hoelzl@29803 ` 434` hoelzl@29803 ` 435` ``` have ?pos using `0 \ ?a 0` by auto ``` wenzelm@53079 ` 436` ``` moreover have ?neg ``` wenzelm@53079 ` 437` ``` using leibniz(2,4) ``` wenzelm@53079 ` 438` ``` unfolding mult_minus_right setsum_negf move_minus neg_le_iff_le ``` wenzelm@53079 ` 439` ``` by auto ``` wenzelm@53079 ` 440` ``` moreover have ?f and ?g ``` wenzelm@53079 ` 441` ``` using leibniz(3,5)[unfolded mult_minus_right setsum_negf move_minus, THEN tendsto_minus_cancel] ``` wenzelm@53079 ` 442` ``` by auto ``` hoelzl@29803 ` 443` ``` ultimately show ?thesis by auto ``` hoelzl@29803 ` 444` ``` qed ``` lp15@59669 ` 445` ``` then show ?summable and ?pos and ?neg and ?f and ?g ``` paulson@54573 ` 446` ``` by safe ``` hoelzl@29803 ` 447` ```qed ``` paulson@15077 ` 448` huffman@29164 ` 449` ```subsection {* Term-by-Term Differentiability of Power Series *} ``` huffman@23043 ` 450` hoelzl@56193 ` 451` ```definition diffs :: "(nat \ 'a::ring_1) \ nat \ 'a" ``` hoelzl@56193 ` 452` ``` where "diffs c = (\n. of_nat (Suc n) * c (Suc n))" ``` paulson@15077 ` 453` paulson@15077 ` 454` ```text{*Lemma about distributing negation over it*} ``` wenzelm@53079 ` 455` ```lemma diffs_minus: "diffs (\n. - c n) = (\n. - diffs c n)" ``` wenzelm@53079 ` 456` ``` by (simp add: diffs_def) ``` paulson@15077 ` 457` huffman@29163 ` 458` ```lemma sums_Suc_imp: ``` hoelzl@56193 ` 459` ``` "(f::nat \ 'a::real_normed_vector) 0 = 0 \ (\n. f (Suc n)) sums s \ (\n. f n) sums s" ``` hoelzl@56193 ` 460` ``` using sums_Suc_iff[of f] by simp ``` paulson@15077 ` 461` paulson@15229 ` 462` ```lemma diffs_equiv: ``` hoelzl@41970 ` 463` ``` fixes x :: "'a::{real_normed_vector, ring_1}" ``` hoelzl@56193 ` 464` ``` shows "summable (\n. diffs c n * x^n) \ ``` hoelzl@56193 ` 465` ``` (\n. of_nat n * c n * x^(n - Suc 0)) sums (\n. diffs c n * x^n)" ``` wenzelm@53079 ` 466` ``` unfolding diffs_def ``` paulson@54573 ` 467` ``` by (simp add: summable_sums sums_Suc_imp) ``` paulson@15077 ` 468` paulson@15077 ` 469` ```lemma lemma_termdiff1: ``` haftmann@31017 ` 470` ``` fixes z :: "'a :: {monoid_mult,comm_ring}" shows ``` hoelzl@56193 ` 471` ``` "(\ppipp 0" ``` wenzelm@53079 ` 487` ``` shows ``` wenzelm@53079 ` 488` ``` "((z + h) ^ n - z ^ n) / h - of_nat n * z ^ (n - Suc 0) = ``` hoelzl@56193 ` 489` ``` h * (\p< n - Suc 0. \q< n - Suc 0 - p. ``` wenzelm@53079 ` 490` ``` (z + h) ^ q * z ^ (n - 2 - q))" (is "?lhs = ?rhs") ``` wenzelm@53079 ` 491` ``` apply (subgoal_tac "h * ?lhs = h * ?rhs", simp add: h) ``` wenzelm@53079 ` 492` ``` apply (simp add: right_diff_distrib diff_divide_distrib h) ``` haftmann@57512 ` 493` ``` apply (simp add: mult.assoc [symmetric]) ``` wenzelm@53079 ` 494` ``` apply (cases "n", simp) ``` lp15@60162 ` 495` ``` apply (simp add: diff_power_eq_setsum h ``` haftmann@57512 ` 496` ``` right_diff_distrib [symmetric] mult.assoc ``` hoelzl@56193 ` 497` ``` del: power_Suc setsum_lessThan_Suc of_nat_Suc) ``` wenzelm@53079 ` 498` ``` apply (subst lemma_realpow_rev_sumr) ``` wenzelm@53079 ` 499` ``` apply (subst sumr_diff_mult_const2) ``` wenzelm@53079 ` 500` ``` apply simp ``` wenzelm@53079 ` 501` ``` apply (simp only: lemma_termdiff1 setsum_right_distrib) ``` haftmann@57418 ` 502` ``` apply (rule setsum.cong [OF refl]) ``` haftmann@54230 ` 503` ``` apply (simp add: less_iff_Suc_add) ``` wenzelm@53079 ` 504` ``` apply (clarify) ``` lp15@60162 ` 505` ``` apply (simp add: setsum_right_distrib diff_power_eq_setsum ac_simps ``` hoelzl@56193 ` 506` ``` del: setsum_lessThan_Suc power_Suc) ``` haftmann@57512 ` 507` ``` apply (subst mult.assoc [symmetric], subst power_add [symmetric]) ``` haftmann@57514 ` 508` ``` apply (simp add: ac_simps) ``` wenzelm@53079 ` 509` ``` done ``` huffman@20860 ` 510` huffman@20860 ` 511` ```lemma real_setsum_nat_ivl_bounded2: ``` haftmann@35028 ` 512` ``` fixes K :: "'a::linordered_semidom" ``` huffman@23082 ` 513` ``` assumes f: "\p::nat. p < n \ f p \ K" ``` wenzelm@53079 ` 514` ``` and K: "0 \ K" ``` hoelzl@56193 ` 515` ``` shows "setsum f {.. of_nat n * K" ``` wenzelm@53079 ` 516` ``` apply (rule order_trans [OF setsum_mono]) ``` wenzelm@53079 ` 517` ``` apply (rule f, simp) ``` wenzelm@53079 ` 518` ``` apply (simp add: mult_right_mono K) ``` wenzelm@53079 ` 519` ``` done ``` paulson@15077 ` 520` paulson@15229 ` 521` ```lemma lemma_termdiff3: ``` haftmann@31017 ` 522` ``` fixes h z :: "'a::{real_normed_field}" ``` huffman@20860 ` 523` ``` assumes 1: "h \ 0" ``` wenzelm@53079 ` 524` ``` and 2: "norm z \ K" ``` wenzelm@53079 ` 525` ``` and 3: "norm (z + h) \ K" ``` huffman@23082 ` 526` ``` shows "norm (((z + h) ^ n - z ^ n) / h - of_nat n * z ^ (n - Suc 0)) ``` huffman@23082 ` 527` ``` \ of_nat n * of_nat (n - Suc 0) * K ^ (n - 2) * norm h" ``` huffman@20860 ` 528` ```proof - ``` huffman@23082 ` 529` ``` have "norm (((z + h) ^ n - z ^ n) / h - of_nat n * z ^ (n - Suc 0)) = ``` hoelzl@56193 ` 530` ``` norm (\pq \ of_nat n * (of_nat (n - Suc 0) * K ^ (n - 2)) * norm h" ``` huffman@23082 ` 534` ``` proof (rule mult_right_mono [OF _ norm_ge_zero]) ``` wenzelm@53079 ` 535` ``` from norm_ge_zero 2 have K: "0 \ K" ``` wenzelm@53079 ` 536` ``` by (rule order_trans) ``` huffman@23082 ` 537` ``` have le_Kn: "\i j n. i + j = n \ norm ((z + h) ^ i * z ^ j) \ K ^ n" ``` huffman@20860 ` 538` ``` apply (erule subst) ``` huffman@23082 ` 539` ``` apply (simp only: norm_mult norm_power power_add) ``` huffman@23082 ` 540` ``` apply (intro mult_mono power_mono 2 3 norm_ge_zero zero_le_power K) ``` huffman@20860 ` 541` ``` done ``` hoelzl@56193 ` 542` ``` show "norm (\pq of_nat n * (of_nat (n - Suc 0) * K ^ (n - 2))" ``` huffman@20860 ` 544` ``` apply (intro ``` huffman@23082 ` 545` ``` order_trans [OF norm_setsum] ``` huffman@20860 ` 546` ``` real_setsum_nat_ivl_bounded2 ``` huffman@20860 ` 547` ``` mult_nonneg_nonneg ``` huffman@47489 ` 548` ``` of_nat_0_le_iff ``` huffman@20860 ` 549` ``` zero_le_power K) ``` huffman@20860 ` 550` ``` apply (rule le_Kn, simp) ``` huffman@20860 ` 551` ``` done ``` huffman@20860 ` 552` ``` qed ``` huffman@23082 ` 553` ``` also have "\ = of_nat n * of_nat (n - Suc 0) * K ^ (n - 2) * norm h" ``` haftmann@57512 ` 554` ``` by (simp only: mult.assoc) ``` huffman@20860 ` 555` ``` finally show ?thesis . ``` huffman@20860 ` 556` ```qed ``` paulson@15077 ` 557` huffman@20860 ` 558` ```lemma lemma_termdiff4: ``` huffman@56167 ` 559` ``` fixes f :: "'a::real_normed_vector \ 'b::real_normed_vector" ``` huffman@20860 ` 560` ``` assumes k: "0 < (k::real)" ``` wenzelm@53079 ` 561` ``` and le: "\h. \h \ 0; norm h < k\ \ norm (f h) \ K * norm h" ``` huffman@20860 ` 562` ``` shows "f -- 0 --> 0" ``` huffman@56167 ` 563` ```proof (rule tendsto_norm_zero_cancel) ``` huffman@56167 ` 564` ``` show "(\h. norm (f h)) -- 0 --> 0" ``` huffman@56167 ` 565` ``` proof (rule real_tendsto_sandwich) ``` huffman@56167 ` 566` ``` show "eventually (\h. 0 \ norm (f h)) (at 0)" ``` huffman@20860 ` 567` ``` by simp ``` huffman@56167 ` 568` ``` show "eventually (\h. norm (f h) \ K * norm h) (at 0)" ``` huffman@56167 ` 569` ``` using k by (auto simp add: eventually_at dist_norm le) ``` huffman@56167 ` 570` ``` show "(\h. 0) -- (0::'a) --> (0::real)" ``` huffman@56167 ` 571` ``` by (rule tendsto_const) ``` huffman@56167 ` 572` ``` have "(\h. K * norm h) -- (0::'a) --> K * norm (0::'a)" ``` huffman@56167 ` 573` ``` by (intro tendsto_intros) ``` huffman@56167 ` 574` ``` then show "(\h. K * norm h) -- (0::'a) --> 0" ``` huffman@56167 ` 575` ``` by simp ``` huffman@20860 ` 576` ``` qed ``` huffman@20860 ` 577` ```qed ``` paulson@15077 ` 578` paulson@15229 ` 579` ```lemma lemma_termdiff5: ``` huffman@56167 ` 580` ``` fixes g :: "'a::real_normed_vector \ nat \ 'b::banach" ``` huffman@20860 ` 581` ``` assumes k: "0 < (k::real)" ``` huffman@20860 ` 582` ``` assumes f: "summable f" ``` huffman@23082 ` 583` ``` assumes le: "\h n. \h \ 0; norm h < k\ \ norm (g h n) \ f n * norm h" ``` huffman@20860 ` 584` ``` shows "(\h. suminf (g h)) -- 0 --> 0" ``` huffman@20860 ` 585` ```proof (rule lemma_termdiff4 [OF k]) ``` wenzelm@53079 ` 586` ``` fix h::'a ``` wenzelm@53079 ` 587` ``` assume "h \ 0" and "norm h < k" ``` huffman@23082 ` 588` ``` hence A: "\n. norm (g h n) \ f n * norm h" ``` huffman@20860 ` 589` ``` by (simp add: le) ``` huffman@23082 ` 590` ``` hence "\N. \n\N. norm (norm (g h n)) \ f n * norm h" ``` huffman@20860 ` 591` ``` by simp ``` huffman@23082 ` 592` ``` moreover from f have B: "summable (\n. f n * norm h)" ``` huffman@20860 ` 593` ``` by (rule summable_mult2) ``` huffman@23082 ` 594` ``` ultimately have C: "summable (\n. norm (g h n))" ``` huffman@20860 ` 595` ``` by (rule summable_comparison_test) ``` huffman@23082 ` 596` ``` hence "norm (suminf (g h)) \ (\n. norm (g h n))" ``` huffman@23082 ` 597` ``` by (rule summable_norm) ``` huffman@23082 ` 598` ``` also from A C B have "(\n. norm (g h n)) \ (\n. f n * norm h)" ``` hoelzl@56213 ` 599` ``` by (rule suminf_le) ``` huffman@23082 ` 600` ``` also from f have "(\n. f n * norm h) = suminf f * norm h" ``` huffman@20860 ` 601` ``` by (rule suminf_mult2 [symmetric]) ``` huffman@23082 ` 602` ``` finally show "norm (suminf (g h)) \ suminf f * norm h" . ``` huffman@20860 ` 603` ```qed ``` paulson@15077 ` 604` paulson@15077 ` 605` paulson@15077 ` 606` ```text{* FIXME: Long proofs*} ``` paulson@15077 ` 607` paulson@15077 ` 608` ```lemma termdiffs_aux: ``` haftmann@31017 ` 609` ``` fixes x :: "'a::{real_normed_field,banach}" ``` huffman@20849 ` 610` ``` assumes 1: "summable (\n. diffs (diffs c) n * K ^ n)" ``` wenzelm@53079 ` 611` ``` and 2: "norm x < norm K" ``` lp15@59730 ` 612` ``` shows "(\h. \n. c n * (((x + h) ^ n - x^n) / h ``` huffman@23082 ` 613` ``` - of_nat n * x ^ (n - Suc 0))) -- 0 --> 0" ``` huffman@20849 ` 614` ```proof - ``` huffman@20860 ` 615` ``` from dense [OF 2] ``` huffman@23082 ` 616` ``` obtain r where r1: "norm x < r" and r2: "r < norm K" by fast ``` huffman@23082 ` 617` ``` from norm_ge_zero r1 have r: "0 < r" ``` huffman@20860 ` 618` ``` by (rule order_le_less_trans) ``` huffman@20860 ` 619` ``` hence r_neq_0: "r \ 0" by simp ``` huffman@20860 ` 620` ``` show ?thesis ``` huffman@20849 ` 621` ``` proof (rule lemma_termdiff5) ``` huffman@23082 ` 622` ``` show "0 < r - norm x" using r1 by simp ``` huffman@23082 ` 623` ``` from r r2 have "norm (of_real r::'a) < norm K" ``` huffman@23082 ` 624` ``` by simp ``` huffman@23082 ` 625` ``` with 1 have "summable (\n. norm (diffs (diffs c) n * (of_real r ^ n)))" ``` huffman@20860 ` 626` ``` by (rule powser_insidea) ``` huffman@23082 ` 627` ``` hence "summable (\n. diffs (diffs (\n. norm (c n))) n * r ^ n)" ``` huffman@23082 ` 628` ``` using r ``` huffman@23082 ` 629` ``` by (simp add: diffs_def norm_mult norm_power del: of_nat_Suc) ``` huffman@23082 ` 630` ``` hence "summable (\n. of_nat n * diffs (\n. norm (c n)) n * r ^ (n - Suc 0))" ``` huffman@20860 ` 631` ``` by (rule diffs_equiv [THEN sums_summable]) ``` wenzelm@53079 ` 632` ``` also have "(\n. of_nat n * diffs (\n. norm (c n)) n * r ^ (n - Suc 0)) = ``` wenzelm@53079 ` 633` ``` (\n. diffs (\m. of_nat (m - Suc 0) * norm (c m) * inverse r) n * (r ^ n))" ``` huffman@20849 ` 634` ``` apply (rule ext) ``` huffman@20849 ` 635` ``` apply (simp add: diffs_def) ``` huffman@20849 ` 636` ``` apply (case_tac n, simp_all add: r_neq_0) ``` huffman@20849 ` 637` ``` done ``` hoelzl@41970 ` 638` ``` finally have "summable ``` huffman@23082 ` 639` ``` (\n. of_nat n * (of_nat (n - Suc 0) * norm (c n) * inverse r) * r ^ (n - Suc 0))" ``` huffman@20860 ` 640` ``` by (rule diffs_equiv [THEN sums_summable]) ``` huffman@20860 ` 641` ``` also have ``` huffman@23082 ` 642` ``` "(\n. of_nat n * (of_nat (n - Suc 0) * norm (c n) * inverse r) * ``` huffman@20860 ` 643` ``` r ^ (n - Suc 0)) = ``` huffman@23082 ` 644` ``` (\n. norm (c n) * of_nat n * of_nat (n - Suc 0) * r ^ (n - 2))" ``` huffman@20849 ` 645` ``` apply (rule ext) ``` huffman@20849 ` 646` ``` apply (case_tac "n", simp) ``` blanchet@55417 ` 647` ``` apply (rename_tac nat) ``` huffman@20849 ` 648` ``` apply (case_tac "nat", simp) ``` huffman@20849 ` 649` ``` apply (simp add: r_neq_0) ``` huffman@20849 ` 650` ``` done ``` wenzelm@53079 ` 651` ``` finally ``` wenzelm@53079 ` 652` ``` show "summable (\n. norm (c n) * of_nat n * of_nat (n - Suc 0) * r ^ (n - 2))" . ``` huffman@20849 ` 653` ``` next ``` huffman@23082 ` 654` ``` fix h::'a and n::nat ``` huffman@20860 ` 655` ``` assume h: "h \ 0" ``` huffman@23082 ` 656` ``` assume "norm h < r - norm x" ``` huffman@23082 ` 657` ``` hence "norm x + norm h < r" by simp ``` huffman@23082 ` 658` ``` with norm_triangle_ineq have xh: "norm (x + h) < r" ``` huffman@20860 ` 659` ``` by (rule order_le_less_trans) ``` lp15@59730 ` 660` ``` show "norm (c n * (((x + h) ^ n - x^n) / h - of_nat n * x ^ (n - Suc 0))) ``` huffman@23082 ` 661` ``` \ norm (c n) * of_nat n * of_nat (n - Suc 0) * r ^ (n - 2) * norm h" ``` haftmann@57512 ` 662` ``` apply (simp only: norm_mult mult.assoc) ``` huffman@23082 ` 663` ``` apply (rule mult_left_mono [OF _ norm_ge_zero]) ``` haftmann@57512 ` 664` ``` apply (simp add: mult.assoc [symmetric]) ``` paulson@54575 ` 665` ``` apply (metis h lemma_termdiff3 less_eq_real_def r1 xh) ``` huffman@20860 ` 666` ``` done ``` huffman@20849 ` 667` ``` qed ``` huffman@20849 ` 668` ```qed ``` webertj@20217 ` 669` huffman@20860 ` 670` ```lemma termdiffs: ``` haftmann@31017 ` 671` ``` fixes K x :: "'a::{real_normed_field,banach}" ``` huffman@20860 ` 672` ``` assumes 1: "summable (\n. c n * K ^ n)" ``` paulson@54575 ` 673` ``` and 2: "summable (\n. (diffs c) n * K ^ n)" ``` paulson@54575 ` 674` ``` and 3: "summable (\n. (diffs (diffs c)) n * K ^ n)" ``` paulson@54575 ` 675` ``` and 4: "norm x < norm K" ``` lp15@59730 ` 676` ``` shows "DERIV (\x. \n. c n * x^n) x :> (\n. (diffs c) n * x^n)" ``` hoelzl@56381 ` 677` ``` unfolding DERIV_def ``` huffman@29163 ` 678` ```proof (rule LIM_zero_cancel) ``` lp15@59730 ` 679` ``` show "(\h. (suminf (\n. c n * (x + h) ^ n) - suminf (\n. c n * x^n)) / h ``` lp15@59730 ` 680` ``` - suminf (\n. diffs c n * x^n)) -- 0 --> 0" ``` huffman@20860 ` 681` ``` proof (rule LIM_equal2) ``` huffman@29163 ` 682` ``` show "0 < norm K - norm x" using 4 by (simp add: less_diff_eq) ``` huffman@20860 ` 683` ``` next ``` huffman@23082 ` 684` ``` fix h :: 'a ``` huffman@23082 ` 685` ``` assume "norm (h - 0) < norm K - norm x" ``` huffman@23082 ` 686` ``` hence "norm x + norm h < norm K" by simp ``` huffman@23082 ` 687` ``` hence 5: "norm (x + h) < norm K" ``` huffman@23082 ` 688` ``` by (rule norm_triangle_ineq [THEN order_le_less_trans]) ``` lp15@59730 ` 689` ``` have "summable (\n. c n * x^n)" ``` huffman@56167 ` 690` ``` and "summable (\n. c n * (x + h) ^ n)" ``` lp15@59730 ` 691` ``` and "summable (\n. diffs c n * x^n)" ``` huffman@56167 ` 692` ``` using 1 2 4 5 by (auto elim: powser_inside) ``` lp15@59730 ` 693` ``` then have "((\n. c n * (x + h) ^ n) - (\n. c n * x^n)) / h - (\n. diffs c n * x^n) = ``` lp15@59730 ` 694` ``` (\n. (c n * (x + h) ^ n - c n * x^n) / h - of_nat n * c n * x ^ (n - Suc 0))" ``` huffman@56167 ` 695` ``` by (intro sums_unique sums_diff sums_divide diffs_equiv summable_sums) ``` lp15@59730 ` 696` ``` then show "((\n. c n * (x + h) ^ n) - (\n. c n * x^n)) / h - (\n. diffs c n * x^n) = ``` lp15@59730 ` 697` ``` (\n. c n * (((x + h) ^ n - x^n) / h - of_nat n * x ^ (n - Suc 0)))" ``` paulson@54575 ` 698` ``` by (simp add: algebra_simps) ``` huffman@20860 ` 699` ``` next ``` lp15@59730 ` 700` ``` show "(\h. \n. c n * (((x + h) ^ n - x^n) / h - of_nat n * x ^ (n - Suc 0))) -- 0 --> 0" ``` wenzelm@53079 ` 701` ``` by (rule termdiffs_aux [OF 3 4]) ``` huffman@20860 ` 702` ``` qed ``` huffman@20860 ` 703` ```qed ``` huffman@20860 ` 704` lp15@60141 ` 705` ```subsection {* The Derivative of a Power Series Has the Same Radius of Convergence *} ``` lp15@60141 ` 706` lp15@60141 ` 707` ```lemma termdiff_converges: ``` lp15@60141 ` 708` ``` fixes x :: "'a::{real_normed_field,banach}" ``` lp15@60141 ` 709` ``` assumes K: "norm x < K" ``` lp15@60141 ` 710` ``` and sm: "\x. norm x < K \ summable(\n. c n * x ^ n)" ``` lp15@60141 ` 711` ``` shows "summable (\n. diffs c n * x ^ n)" ``` lp15@60141 ` 712` ```proof (cases "x = 0") ``` lp15@60141 ` 713` ``` case True then show ?thesis ``` lp15@60141 ` 714` ``` using powser_sums_zero sums_summable by auto ``` lp15@60141 ` 715` ```next ``` lp15@60141 ` 716` ``` case False ``` lp15@60141 ` 717` ``` then have "K>0" ``` lp15@60141 ` 718` ``` using K less_trans zero_less_norm_iff by blast ``` lp15@60141 ` 719` ``` then obtain r::real where r: "norm x < norm r" "norm r < K" "r>0" ``` lp15@60141 ` 720` ``` using K False ``` lp15@60141 ` 721` ``` by (auto simp: abs_less_iff add_pos_pos intro: that [of "(norm x + K) / 2"]) ``` lp15@60141 ` 722` ``` have "(\n. of_nat n * (x / of_real r) ^ n) ----> 0" ``` lp15@60141 ` 723` ``` using r by (simp add: norm_divide powser_times_n_limit_0 [of "x / of_real r"]) ``` lp15@60141 ` 724` ``` then obtain N where N: "\n. n\N \ real_of_nat n * norm x ^ n < r ^ n" ``` lp15@60141 ` 725` ``` using r unfolding LIMSEQ_iff ``` lp15@60141 ` 726` ``` apply (drule_tac x=1 in spec) ``` lp15@60141 ` 727` ``` apply (auto simp: norm_divide norm_mult norm_power field_simps) ``` lp15@60141 ` 728` ``` done ``` lp15@60141 ` 729` ``` have "summable (\n. (of_nat n * c n) * x ^ n)" ``` lp15@60141 ` 730` ``` apply (rule summable_comparison_test' [of "\n. norm(c n * (of_real r) ^ n)" N]) ``` lp15@60141 ` 731` ``` apply (rule powser_insidea [OF sm [of "of_real ((r+K)/2)"]]) ``` lp15@60141 ` 732` ``` using N r norm_of_real [of "r+K", where 'a = 'a] ``` lp15@60141 ` 733` ``` apply (auto simp add: norm_divide norm_mult norm_power ) ``` lp15@60141 ` 734` ``` using less_eq_real_def by fastforce ``` lp15@60141 ` 735` ``` then have "summable (\n. (of_nat (Suc n) * c(Suc n)) * x ^ Suc n)" ``` lp15@60141 ` 736` ``` using summable_iff_shift [of "\n. of_nat n * c n * x ^ n" 1] ``` lp15@60141 ` 737` ``` by simp ``` lp15@60141 ` 738` ``` then have "summable (\n. (of_nat (Suc n) * c(Suc n)) * x ^ n)" ``` lp15@60141 ` 739` ``` using False summable_mult2 [of "\n. (of_nat (Suc n) * c(Suc n) * x ^ n) * x" "inverse x"] ``` lp15@60141 ` 740` ``` by (simp add: mult.assoc) (auto simp: power_Suc mult_ac) ``` lp15@60141 ` 741` ``` then show ?thesis ``` lp15@60141 ` 742` ``` by (simp add: diffs_def) ``` lp15@60141 ` 743` ```qed ``` lp15@60141 ` 744` lp15@60141 ` 745` ```lemma termdiff_converges_all: ``` lp15@60141 ` 746` ``` fixes x :: "'a::{real_normed_field,banach}" ``` lp15@60141 ` 747` ``` assumes "\x. summable (\n. c n * x^n)" ``` lp15@60141 ` 748` ``` shows "summable (\n. diffs c n * x^n)" ``` lp15@60141 ` 749` ``` apply (rule termdiff_converges [where K = "1 + norm x"]) ``` lp15@60141 ` 750` ``` using assms ``` lp15@60141 ` 751` ``` apply (auto simp: ) ``` lp15@60141 ` 752` ``` done ``` lp15@60141 ` 753` lp15@60141 ` 754` ```lemma termdiffs_strong: ``` lp15@60141 ` 755` ``` fixes K x :: "'a::{real_normed_field,banach}" ``` lp15@60141 ` 756` ``` assumes sm: "summable (\n. c n * K ^ n)" ``` lp15@60141 ` 757` ``` and K: "norm x < norm K" ``` lp15@60141 ` 758` ``` shows "DERIV (\x. \n. c n * x^n) x :> (\n. diffs c n * x^n)" ``` lp15@60141 ` 759` ```proof - ``` lp15@60141 ` 760` ``` have [simp]: "norm ((of_real (norm K) + of_real (norm x)) / 2 :: 'a) < norm K" ``` lp15@60141 ` 761` ``` using K ``` lp15@60141 ` 762` ``` apply (auto simp: norm_divide) ``` lp15@60141 ` 763` ``` apply (rule le_less_trans [of _ "of_real (norm K) + of_real (norm x)"]) ``` lp15@60141 ` 764` ``` apply (auto simp: mult_2_right norm_triangle_mono) ``` lp15@60141 ` 765` ``` done ``` lp15@60141 ` 766` ``` have "summable (\n. c n * (of_real (norm x + norm K) / 2) ^ n)" ``` lp15@60141 ` 767` ``` apply (rule summable_norm_cancel [OF powser_insidea [OF sm]]) ``` lp15@60141 ` 768` ``` using K ``` lp15@60141 ` 769` ``` apply (auto simp: algebra_simps) ``` lp15@60141 ` 770` ``` done ``` lp15@60141 ` 771` ``` moreover have "\x. norm x < norm K \ summable (\n. diffs c n * x ^ n)" ``` lp15@60141 ` 772` ``` by (blast intro: sm termdiff_converges powser_inside) ``` lp15@60141 ` 773` ``` moreover have "\x. norm x < norm K \ summable (\n. diffs(diffs c) n * x ^ n)" ``` lp15@60141 ` 774` ``` by (blast intro: sm termdiff_converges powser_inside) ``` lp15@60141 ` 775` ``` ultimately show ?thesis ``` lp15@60141 ` 776` ``` apply (rule termdiffs [where K = "of_real (norm x + norm K) / 2"]) ``` lp15@60141 ` 777` ``` apply (auto simp: algebra_simps) ``` lp15@60141 ` 778` ``` using K ``` lp15@60141 ` 779` ``` apply (simp add: norm_divide) ``` lp15@60141 ` 780` ``` apply (rule less_le_trans [of _ "of_real (norm K) + of_real (norm x)"]) ``` lp15@60141 ` 781` ``` apply (simp_all add: of_real_add [symmetric] del: of_real_add) ``` lp15@60141 ` 782` ``` done ``` lp15@60141 ` 783` ```qed ``` lp15@60141 ` 784` lp15@60141 ` 785` ```lemma powser_limit_0: ``` lp15@60141 ` 786` ``` fixes a :: "nat \ 'a::{real_normed_field,banach}" ``` lp15@60141 ` 787` ``` assumes s: "0 < s" ``` lp15@60141 ` 788` ``` and sm: "\x. norm x < s \ (\n. a n * x ^ n) sums (f x)" ``` lp15@60141 ` 789` ``` shows "(f ---> a 0) (at 0)" ``` lp15@60141 ` 790` ```proof - ``` lp15@60141 ` 791` ``` have "summable (\n. a n * (of_real s / 2) ^ n)" ``` lp15@60141 ` 792` ``` apply (rule sums_summable [where l = "f (of_real s / 2)", OF sm]) ``` lp15@60141 ` 793` ``` using s ``` lp15@60141 ` 794` ``` apply (auto simp: norm_divide) ``` lp15@60141 ` 795` ``` done ``` lp15@60141 ` 796` ``` then have "((\x. \n. a n * x ^ n) has_field_derivative (\n. diffs a n * 0 ^ n)) (at 0)" ``` lp15@60141 ` 797` ``` apply (rule termdiffs_strong) ``` lp15@60141 ` 798` ``` using s ``` lp15@60141 ` 799` ``` apply (auto simp: norm_divide) ``` lp15@60141 ` 800` ``` done ``` lp15@60141 ` 801` ``` then have "isCont (\x. \n. a n * x ^ n) 0" ``` lp15@60141 ` 802` ``` by (blast intro: DERIV_continuous) ``` lp15@60141 ` 803` ``` then have "((\x. \n. a n * x ^ n) ---> a 0) (at 0)" ``` lp15@60141 ` 804` ``` by (simp add: continuous_within powser_zero) ``` lp15@60141 ` 805` ``` then show ?thesis ``` lp15@60141 ` 806` ``` apply (rule Lim_transform) ``` lp15@60141 ` 807` ``` apply (auto simp add: LIM_eq) ``` lp15@60141 ` 808` ``` apply (rule_tac x="s" in exI) ``` lp15@60141 ` 809` ``` using s ``` lp15@60141 ` 810` ``` apply (auto simp: sm [THEN sums_unique]) ``` lp15@60141 ` 811` ``` done ``` lp15@60141 ` 812` ```qed ``` lp15@60141 ` 813` lp15@60141 ` 814` ```lemma powser_limit_0_strong: ``` lp15@60141 ` 815` ``` fixes a :: "nat \ 'a::{real_normed_field,banach}" ``` lp15@60141 ` 816` ``` assumes s: "0 < s" ``` lp15@60141 ` 817` ``` and sm: "\x. x \ 0 \ norm x < s \ (\n. a n * x ^ n) sums (f x)" ``` lp15@60141 ` 818` ``` shows "(f ---> a 0) (at 0)" ``` lp15@60141 ` 819` ```proof - ``` lp15@60141 ` 820` ``` have *: "((\x. if x = 0 then a 0 else f x) ---> a 0) (at 0)" ``` lp15@60141 ` 821` ``` apply (rule powser_limit_0 [OF s]) ``` lp15@60141 ` 822` ``` apply (case_tac "x=0") ``` lp15@60141 ` 823` ``` apply (auto simp add: powser_sums_zero sm) ``` lp15@60141 ` 824` ``` done ``` lp15@60141 ` 825` ``` show ?thesis ``` lp15@60141 ` 826` ``` apply (subst LIM_equal [where g = "(\x. if x = 0 then a 0 else f x)"]) ``` lp15@60141 ` 827` ``` apply (simp_all add: *) ``` lp15@60141 ` 828` ``` done ``` lp15@60141 ` 829` ```qed ``` lp15@60141 ` 830` paulson@15077 ` 831` hoelzl@29803 ` 832` ```subsection {* Derivability of power series *} ``` hoelzl@29803 ` 833` wenzelm@53079 ` 834` ```lemma DERIV_series': ``` wenzelm@53079 ` 835` ``` fixes f :: "real \ nat \ real" ``` hoelzl@29803 ` 836` ``` assumes DERIV_f: "\ n. DERIV (\ x. f x n) x0 :> (f' x0 n)" ``` wenzelm@53079 ` 837` ``` and allf_summable: "\ x. x \ {a <..< b} \ summable (f x)" and x0_in_I: "x0 \ {a <..< b}" ``` wenzelm@53079 ` 838` ``` and "summable (f' x0)" ``` wenzelm@53079 ` 839` ``` and "summable L" ``` wenzelm@53079 ` 840` ``` and L_def: "\n x y. \ x \ { a <..< b} ; y \ { a <..< b} \ \ \f x n - f y n\ \ L n * \x - y\" ``` hoelzl@29803 ` 841` ``` shows "DERIV (\ x. suminf (f x)) x0 :> (suminf (f' x0))" ``` hoelzl@56381 ` 842` ``` unfolding DERIV_def ``` hoelzl@29803 ` 843` ```proof (rule LIM_I) ``` wenzelm@53079 ` 844` ``` fix r :: real ``` wenzelm@53079 ` 845` ``` assume "0 < r" hence "0 < r/3" by auto ``` hoelzl@29803 ` 846` hoelzl@41970 ` 847` ``` obtain N_L where N_L: "\ n. N_L \ n \ \ \ i. L (i + n) \ < r/3" ``` hoelzl@29803 ` 848` ``` using suminf_exist_split[OF `0 < r/3` `summable L`] by auto ``` hoelzl@29803 ` 849` hoelzl@41970 ` 850` ``` obtain N_f' where N_f': "\ n. N_f' \ n \ \ \ i. f' x0 (i + n) \ < r/3" ``` hoelzl@29803 ` 851` ``` using suminf_exist_split[OF `0 < r/3` `summable (f' x0)`] by auto ``` hoelzl@29803 ` 852` hoelzl@29803 ` 853` ``` let ?N = "Suc (max N_L N_f')" ``` hoelzl@29803 ` 854` ``` have "\ \ i. f' x0 (i + ?N) \ < r/3" (is "?f'_part < r/3") and ``` hoelzl@29803 ` 855` ``` L_estimate: "\ \ i. L (i + ?N) \ < r/3" using N_L[of "?N"] and N_f' [of "?N"] by auto ``` hoelzl@29803 ` 856` wenzelm@53079 ` 857` ``` let ?diff = "\i x. (f (x0 + x) i - f x0 i) / x" ``` hoelzl@29803 ` 858` hoelzl@29803 ` 859` ``` let ?r = "r / (3 * real ?N)" ``` nipkow@56541 ` 860` ``` from `0 < r` have "0 < ?r" by simp ``` hoelzl@29803 ` 861` hoelzl@56193 ` 862` ``` let ?s = "\n. SOME s. 0 < s \ (\ x. x \ 0 \ \ x \ < s \ \ ?diff n x - f' x0 n \ < ?r)" ``` hoelzl@56193 ` 863` ``` def S' \ "Min (?s ` {..< ?N })" ``` hoelzl@29803 ` 864` hoelzl@29803 ` 865` ``` have "0 < S'" unfolding S'_def ``` hoelzl@29803 ` 866` ``` proof (rule iffD2[OF Min_gr_iff]) ``` hoelzl@56193 ` 867` ``` show "\x \ (?s ` {..< ?N }). 0 < x" ``` wenzelm@53079 ` 868` ``` proof ``` wenzelm@53079 ` 869` ``` fix x ``` hoelzl@56193 ` 870` ``` assume "x \ ?s ` {.. {.. (\x. x \ 0 \ \x\ < s \ \?diff n x - f' x0 n\ < ?r)" ``` wenzelm@53079 ` 875` ``` by auto ``` wenzelm@53079 ` 876` ``` have "0 < ?s n" by (rule someI2[where a=s]) (auto simp add: s_bound) ``` hoelzl@29803 ` 877` ``` thus "0 < x" unfolding `x = ?s n` . ``` hoelzl@29803 ` 878` ``` qed ``` hoelzl@29803 ` 879` ``` qed auto ``` hoelzl@29803 ` 880` hoelzl@29803 ` 881` ``` def S \ "min (min (x0 - a) (b - x0)) S'" ``` wenzelm@53079 ` 882` ``` hence "0 < S" and S_a: "S \ x0 - a" and S_b: "S \ b - x0" ``` wenzelm@53079 ` 883` ``` and "S \ S'" using x0_in_I and `0 < S'` ``` hoelzl@29803 ` 884` ``` by auto ``` hoelzl@29803 ` 885` wenzelm@53079 ` 886` ``` { ``` wenzelm@53079 ` 887` ``` fix x ``` wenzelm@53079 ` 888` ``` assume "x \ 0" and "\ x \ < S" ``` wenzelm@53079 ` 889` ``` hence x_in_I: "x0 + x \ { a <..< b }" ``` wenzelm@53079 ` 890` ``` using S_a S_b by auto ``` hoelzl@41970 ` 891` hoelzl@29803 ` 892` ``` note diff_smbl = summable_diff[OF allf_summable[OF x_in_I] allf_summable[OF x0_in_I]] ``` hoelzl@29803 ` 893` ``` note div_smbl = summable_divide[OF diff_smbl] ``` hoelzl@29803 ` 894` ``` note all_smbl = summable_diff[OF div_smbl `summable (f' x0)`] ``` hoelzl@29803 ` 895` ``` note ign = summable_ignore_initial_segment[where k="?N"] ``` hoelzl@29803 ` 896` ``` note diff_shft_smbl = summable_diff[OF ign[OF allf_summable[OF x_in_I]] ign[OF allf_summable[OF x0_in_I]]] ``` hoelzl@29803 ` 897` ``` note div_shft_smbl = summable_divide[OF diff_shft_smbl] ``` hoelzl@29803 ` 898` ``` note all_shft_smbl = summable_diff[OF div_smbl ign[OF `summable (f' x0)`]] ``` hoelzl@29803 ` 899` hoelzl@56193 ` 900` ``` { fix n ``` hoelzl@41970 ` 901` ``` have "\ ?diff (n + ?N) x \ \ L (n + ?N) * \ (x0 + x) - x0 \ / \ x \" ``` wenzelm@53079 ` 902` ``` using divide_right_mono[OF L_def[OF x_in_I x0_in_I] abs_ge_zero] ``` wenzelm@53079 ` 903` ``` unfolding abs_divide . ``` wenzelm@53079 ` 904` ``` hence "\ (\?diff (n + ?N) x \) \ \ L (n + ?N)" ``` hoelzl@56193 ` 905` ``` using `x \ 0` by auto } ``` hoelzl@56193 ` 906` ``` note 1 = this and 2 = summable_rabs_comparison_test[OF _ ign[OF `summable L`]] ``` hoelzl@56193 ` 907` ``` then have "\ \ i. ?diff (i + ?N) x \ \ (\ i. L (i + ?N))" ``` hoelzl@56213 ` 908` ``` by (metis (lifting) abs_idempotent order_trans[OF summable_rabs[OF 2] suminf_le[OF _ 2 ign[OF `summable L`]]]) ``` hoelzl@56193 ` 909` ``` then have "\ \ i. ?diff (i + ?N) x \ \ r / 3" (is "?L_part \ r/3") ``` wenzelm@53079 ` 910` ``` using L_estimate by auto ``` wenzelm@53079 ` 911` hoelzl@56193 ` 912` ``` have "\\n \ (\n?diff n x - f' x0 n \)" .. ``` hoelzl@56193 ` 913` ``` also have "\ < (\n {..< ?N}" ``` wenzelm@53079 ` 917` ``` have "\x\ < S" using `\x\ < S` . ``` hoelzl@29803 ` 918` ``` also have "S \ S'" using `S \ S'` . ``` hoelzl@41970 ` 919` ``` also have "S' \ ?s n" unfolding S'_def ``` hoelzl@29803 ` 920` ``` proof (rule Min_le_iff[THEN iffD2]) ``` hoelzl@56193 ` 921` ``` have "?s n \ (?s ` {.. ?s n \ ?s n" ``` hoelzl@56193 ` 922` ``` using `n \ {..< ?N}` by auto ``` hoelzl@56193 ` 923` ``` thus "\ a \ (?s ` {.. ?s n" by blast ``` hoelzl@29803 ` 924` ``` qed auto ``` wenzelm@53079 ` 925` ``` finally have "\x\ < ?s n" . ``` hoelzl@29803 ` 926` hoelzl@29803 ` 927` ``` from DERIV_D[OF DERIV_f[where n=n], THEN LIM_D, OF `0 < ?r`, unfolded real_norm_def diff_0_right, unfolded some_eq_ex[symmetric], THEN conjunct2] ``` hoelzl@29803 ` 928` ``` have "\x. x \ 0 \ \x\ < ?s n \ \?diff n x - f' x0 n\ < ?r" . ``` wenzelm@53079 ` 929` ``` with `x \ 0` and `\x\ < ?s n` show "\?diff n x - f' x0 n\ < ?r" ``` wenzelm@53079 ` 930` ``` by blast ``` hoelzl@29803 ` 931` ``` qed auto ``` hoelzl@56193 ` 932` ``` also have "\ = of_nat (card {.. = real ?N * ?r" ``` wenzelm@53079 ` 935` ``` unfolding real_eq_of_nat by auto ``` hoelzl@29803 ` 936` ``` also have "\ = r/3" by auto ``` hoelzl@56193 ` 937` ``` finally have "\\n < r / 3" (is "?diff_part < r / 3") . ``` hoelzl@29803 ` 938` hoelzl@29803 ` 939` ``` from suminf_diff[OF allf_summable[OF x_in_I] allf_summable[OF x0_in_I]] ``` wenzelm@53079 ` 940` ``` have "\(suminf (f (x0 + x)) - (suminf (f x0))) / x - suminf (f' x0)\ = ``` wenzelm@53079 ` 941` ``` \\n. ?diff n x - f' x0 n\" ``` wenzelm@53079 ` 942` ``` unfolding suminf_diff[OF div_smbl `summable (f' x0)`, symmetric] ``` wenzelm@53079 ` 943` ``` using suminf_divide[OF diff_smbl, symmetric] by auto ``` wenzelm@53079 ` 944` ``` also have "\ \ ?diff_part + \ (\n. ?diff (n + ?N) x) - (\ n. f' x0 (n + ?N)) \" ``` wenzelm@53079 ` 945` ``` unfolding suminf_split_initial_segment[OF all_smbl, where k="?N"] ``` wenzelm@53079 ` 946` ``` unfolding suminf_diff[OF div_shft_smbl ign[OF `summable (f' x0)`]] ``` haftmann@57512 ` 947` ``` apply (subst (5) add.commute) ``` wenzelm@53079 ` 948` ``` by (rule abs_triangle_ineq) ``` wenzelm@53079 ` 949` ``` also have "\ \ ?diff_part + ?L_part + ?f'_part" ``` wenzelm@53079 ` 950` ``` using abs_triangle_ineq4 by auto ``` hoelzl@41970 ` 951` ``` also have "\ < r /3 + r/3 + r/3" ``` huffman@36842 ` 952` ``` using `?diff_part < r/3` `?L_part \ r/3` and `?f'_part < r/3` ``` huffman@36842 ` 953` ``` by (rule add_strict_mono [OF add_less_le_mono]) ``` wenzelm@53079 ` 954` ``` finally have "\(suminf (f (x0 + x)) - suminf (f x0)) / x - suminf (f' x0)\ < r" ``` hoelzl@29803 ` 955` ``` by auto ``` wenzelm@53079 ` 956` ``` } ``` wenzelm@53079 ` 957` ``` thus "\ s > 0. \ x. x \ 0 \ norm (x - 0) < s \ ``` wenzelm@53079 ` 958` ``` norm (((\n. f (x0 + x) n) - (\n. f x0 n)) / x - (\n. f' x0 n)) < r" ``` wenzelm@53079 ` 959` ``` using `0 < S` unfolding real_norm_def diff_0_right by blast ``` hoelzl@29803 ` 960` ```qed ``` hoelzl@29803 ` 961` wenzelm@53079 ` 962` ```lemma DERIV_power_series': ``` wenzelm@53079 ` 963` ``` fixes f :: "nat \ real" ``` hoelzl@29803 ` 964` ``` assumes converges: "\ x. x \ {-R <..< R} \ summable (\ n. f n * real (Suc n) * x^n)" ``` wenzelm@53079 ` 965` ``` and x0_in_I: "x0 \ {-R <..< R}" and "0 < R" ``` hoelzl@29803 ` 966` ``` shows "DERIV (\ x. (\ n. f n * x^(Suc n))) x0 :> (\ n. f n * real (Suc n) * x0^n)" ``` hoelzl@29803 ` 967` ``` (is "DERIV (\ x. (suminf (?f x))) x0 :> (suminf (?f' x0))") ``` hoelzl@29803 ` 968` ```proof - ``` wenzelm@53079 ` 969` ``` { ``` wenzelm@53079 ` 970` ``` fix R' ``` wenzelm@53079 ` 971` ``` assume "0 < R'" and "R' < R" and "-R' < x0" and "x0 < R'" ``` wenzelm@53079 ` 972` ``` hence "x0 \ {-R' <..< R'}" and "R' \ {-R <..< R}" and "x0 \ {-R <..< R}" ``` wenzelm@53079 ` 973` ``` by auto ``` hoelzl@29803 ` 974` ``` have "DERIV (\ x. (suminf (?f x))) x0 :> (suminf (?f' x0))" ``` hoelzl@29803 ` 975` ``` proof (rule DERIV_series') ``` hoelzl@29803 ` 976` ``` show "summable (\ n. \f n * real (Suc n) * R'^n\)" ``` hoelzl@29803 ` 977` ``` proof - ``` wenzelm@53079 ` 978` ``` have "(R' + R) / 2 < R" and "0 < (R' + R) / 2" ``` wenzelm@53079 ` 979` ``` using `0 < R'` `0 < R` `R' < R` by auto ``` wenzelm@53079 ` 980` ``` hence in_Rball: "(R' + R) / 2 \ {-R <..< R}" ``` wenzelm@53079 ` 981` ``` using `R' < R` by auto ``` wenzelm@53079 ` 982` ``` have "norm R' < norm ((R' + R) / 2)" ``` wenzelm@53079 ` 983` ``` using `0 < R'` `0 < R` `R' < R` by auto ``` wenzelm@53079 ` 984` ``` from powser_insidea[OF converges[OF in_Rball] this] show ?thesis ``` wenzelm@53079 ` 985` ``` by auto ``` hoelzl@29803 ` 986` ``` qed ``` wenzelm@53079 ` 987` ``` { ``` wenzelm@53079 ` 988` ``` fix n x y ``` wenzelm@53079 ` 989` ``` assume "x \ {-R' <..< R'}" and "y \ {-R' <..< R'}" ``` wenzelm@32960 ` 990` ``` show "\?f x n - ?f y n\ \ \f n * real (Suc n) * R'^n\ * \x-y\" ``` wenzelm@32960 ` 991` ``` proof - ``` wenzelm@53079 ` 992` ``` have "\f n * x ^ (Suc n) - f n * y ^ (Suc n)\ = ``` hoelzl@56193 ` 993` ``` (\f n\ * \x-y\) * \\p" ``` lp15@60162 ` 994` ``` unfolding right_diff_distrib[symmetric] diff_power_eq_setsum abs_mult ``` wenzelm@53079 ` 995` ``` by auto ``` hoelzl@41970 ` 996` ``` also have "\ \ (\f n\ * \x-y\) * (\real (Suc n)\ * \R' ^ n\)" ``` wenzelm@32960 ` 997` ``` proof (rule mult_left_mono) ``` hoelzl@56193 ` 998` ``` have "\\p \ (\px ^ p * y ^ (n - p)\)" ``` wenzelm@53079 ` 999` ``` by (rule setsum_abs) ``` hoelzl@56193 ` 1000` ``` also have "\ \ (\p {.. n" by auto ``` wenzelm@53079 ` 1005` ``` { ``` wenzelm@53079 ` 1006` ``` fix n ``` wenzelm@53079 ` 1007` ``` fix x :: real ``` wenzelm@53079 ` 1008` ``` assume "x \ {-R'<..x\ \ R'" by auto ``` wenzelm@53079 ` 1010` ``` hence "\x^n\ \ R'^n" ``` wenzelm@53079 ` 1011` ``` unfolding power_abs by (rule power_mono, auto) ``` wenzelm@53079 ` 1012` ``` } ``` wenzelm@53079 ` 1013` ``` from mult_mono[OF this[OF `x \ {-R'<.. {-R'<..x^p * y^(n-p)\ \ R'^p * R'^(n-p)" ``` wenzelm@53079 ` 1015` ``` unfolding abs_mult by auto ``` wenzelm@53079 ` 1016` ``` thus "\x^p * y^(n-p)\ \ R'^n" ``` wenzelm@53079 ` 1017` ``` unfolding power_add[symmetric] using `p \ n` by auto ``` wenzelm@32960 ` 1018` ``` qed ``` wenzelm@53079 ` 1019` ``` also have "\ = real (Suc n) * R' ^ n" ``` wenzelm@53079 ` 1020` ``` unfolding setsum_constant card_atLeastLessThan real_of_nat_def by auto ``` hoelzl@56193 ` 1021` ``` finally show "\\p \ \real (Suc n)\ * \R' ^ n\" ``` wenzelm@53079 ` 1022` ``` unfolding abs_real_of_nat_cancel abs_of_nonneg[OF zero_le_power[OF less_imp_le[OF `0 < R'`]]] . ``` wenzelm@53079 ` 1023` ``` show "0 \ \f n\ * \x - y\" ``` wenzelm@53079 ` 1024` ``` unfolding abs_mult[symmetric] by auto ``` wenzelm@32960 ` 1025` ``` qed ``` wenzelm@53079 ` 1026` ``` also have "\ = \f n * real (Suc n) * R' ^ n\ * \x - y\" ``` haftmann@57512 ` 1027` ``` unfolding abs_mult mult.assoc[symmetric] by algebra ``` wenzelm@32960 ` 1028` ``` finally show ?thesis . ``` wenzelm@53079 ` 1029` ``` qed ``` wenzelm@53079 ` 1030` ``` } ``` wenzelm@53079 ` 1031` ``` { ``` wenzelm@53079 ` 1032` ``` fix n ``` wenzelm@53079 ` 1033` ``` show "DERIV (\ x. ?f x n) x0 :> (?f' x0 n)" ``` hoelzl@56381 ` 1034` ``` by (auto intro!: derivative_eq_intros simp del: power_Suc simp: real_of_nat_def) ``` wenzelm@53079 ` 1035` ``` } ``` wenzelm@53079 ` 1036` ``` { ``` wenzelm@53079 ` 1037` ``` fix x ``` wenzelm@53079 ` 1038` ``` assume "x \ {-R' <..< R'}" ``` wenzelm@53079 ` 1039` ``` hence "R' \ {-R <..< R}" and "norm x < norm R'" ``` wenzelm@53079 ` 1040` ``` using assms `R' < R` by auto ``` wenzelm@32960 ` 1041` ``` have "summable (\ n. f n * x^n)" ``` hoelzl@56193 ` 1042` ``` proof (rule summable_comparison_test, intro exI allI impI) ``` wenzelm@32960 ` 1043` ``` fix n ``` wenzelm@53079 ` 1044` ``` have le: "\f n\ * 1 \ \f n\ * real (Suc n)" ``` wenzelm@53079 ` 1045` ``` by (rule mult_left_mono) auto ``` lp15@59730 ` 1046` ``` show "norm (f n * x^n) \ norm (f n * real (Suc n) * x^n)" ``` wenzelm@53079 ` 1047` ``` unfolding real_norm_def abs_mult ``` wenzelm@53079 ` 1048` ``` by (rule mult_right_mono) (auto simp add: le[unfolded mult_1_right]) ``` hoelzl@56193 ` 1049` ``` qed (rule powser_insidea[OF converges[OF `R' \ {-R <..< R}`] `norm x < norm R'`]) ``` haftmann@57512 ` 1050` ``` from this[THEN summable_mult2[where c=x], unfolded mult.assoc, unfolded mult.commute] ``` wenzelm@53079 ` 1051` ``` show "summable (?f x)" by auto ``` wenzelm@53079 ` 1052` ``` } ``` wenzelm@53079 ` 1053` ``` show "summable (?f' x0)" ``` wenzelm@53079 ` 1054` ``` using converges[OF `x0 \ {-R <..< R}`] . ``` wenzelm@53079 ` 1055` ``` show "x0 \ {-R' <..< R'}" ``` wenzelm@53079 ` 1056` ``` using `x0 \ {-R' <..< R'}` . ``` hoelzl@29803 ` 1057` ``` qed ``` hoelzl@29803 ` 1058` ``` } note for_subinterval = this ``` hoelzl@29803 ` 1059` ``` let ?R = "(R + \x0\) / 2" ``` hoelzl@29803 ` 1060` ``` have "\x0\ < ?R" using assms by auto ``` hoelzl@29803 ` 1061` ``` hence "- ?R < x0" ``` hoelzl@29803 ` 1062` ``` proof (cases "x0 < 0") ``` hoelzl@29803 ` 1063` ``` case True ``` hoelzl@29803 ` 1064` ``` hence "- x0 < ?R" using `\x0\ < ?R` by auto ``` hoelzl@29803 ` 1065` ``` thus ?thesis unfolding neg_less_iff_less[symmetric, of "- x0"] by auto ``` hoelzl@29803 ` 1066` ``` next ``` hoelzl@29803 ` 1067` ``` case False ``` hoelzl@29803 ` 1068` ``` have "- ?R < 0" using assms by auto ``` hoelzl@41970 ` 1069` ``` also have "\ \ x0" using False by auto ``` hoelzl@29803 ` 1070` ``` finally show ?thesis . ``` hoelzl@29803 ` 1071` ``` qed ``` wenzelm@53079 ` 1072` ``` hence "0 < ?R" "?R < R" "- ?R < x0" and "x0 < ?R" ``` wenzelm@53079 ` 1073` ``` using assms by auto ``` hoelzl@29803 ` 1074` ``` from for_subinterval[OF this] ``` hoelzl@29803 ` 1075` ``` show ?thesis . ``` hoelzl@29803 ` 1076` ```qed ``` chaieb@29695 ` 1077` wenzelm@53079 ` 1078` huffman@29164 ` 1079` ```subsection {* Exponential Function *} ``` huffman@23043 ` 1080` immler@58656 ` 1081` ```definition exp :: "'a \ 'a::{real_normed_algebra_1,banach}" ``` lp15@59730 ` 1082` ``` where "exp = (\x. \n. x^n /\<^sub>R fact n)" ``` huffman@23043 ` 1083` huffman@23115 ` 1084` ```lemma summable_exp_generic: ``` haftmann@31017 ` 1085` ``` fixes x :: "'a::{real_normed_algebra_1,banach}" ``` lp15@59730 ` 1086` ``` defines S_def: "S \ \n. x^n /\<^sub>R fact n" ``` huffman@23115 ` 1087` ``` shows "summable S" ``` huffman@23115 ` 1088` ```proof - ``` lp15@59730 ` 1089` ``` have S_Suc: "\n. S (Suc n) = (x * S n) /\<^sub>R (Suc n)" ``` huffman@30273 ` 1090` ``` unfolding S_def by (simp del: mult_Suc) ``` huffman@23115 ` 1091` ``` obtain r :: real where r0: "0 < r" and r1: "r < 1" ``` huffman@23115 ` 1092` ``` using dense [OF zero_less_one] by fast ``` huffman@23115 ` 1093` ``` obtain N :: nat where N: "norm x < real N * r" ``` lp15@60155 ` 1094` ``` using ex_less_of_nat_mult r0 real_of_nat_def by auto ``` huffman@23115 ` 1095` ``` from r1 show ?thesis ``` hoelzl@56193 ` 1096` ``` proof (rule summable_ratio_test [rule_format]) ``` huffman@23115 ` 1097` ``` fix n :: nat ``` huffman@23115 ` 1098` ``` assume n: "N \ n" ``` huffman@23115 ` 1099` ``` have "norm x \ real N * r" ``` huffman@23115 ` 1100` ``` using N by (rule order_less_imp_le) ``` huffman@23115 ` 1101` ``` also have "real N * r \ real (Suc n) * r" ``` huffman@23115 ` 1102` ``` using r0 n by (simp add: mult_right_mono) ``` huffman@23115 ` 1103` ``` finally have "norm x * norm (S n) \ real (Suc n) * r * norm (S n)" ``` huffman@23115 ` 1104` ``` using norm_ge_zero by (rule mult_right_mono) ``` huffman@23115 ` 1105` ``` hence "norm (x * S n) \ real (Suc n) * r * norm (S n)" ``` huffman@23115 ` 1106` ``` by (rule order_trans [OF norm_mult_ineq]) ``` huffman@23115 ` 1107` ``` hence "norm (x * S n) / real (Suc n) \ r * norm (S n)" ``` haftmann@57514 ` 1108` ``` by (simp add: pos_divide_le_eq ac_simps) ``` huffman@23115 ` 1109` ``` thus "norm (S (Suc n)) \ r * norm (S n)" ``` huffman@35216 ` 1110` ``` by (simp add: S_Suc inverse_eq_divide) ``` huffman@23115 ` 1111` ``` qed ``` huffman@23115 ` 1112` ```qed ``` huffman@23115 ` 1113` huffman@23115 ` 1114` ```lemma summable_norm_exp: ``` haftmann@31017 ` 1115` ``` fixes x :: "'a::{real_normed_algebra_1,banach}" ``` lp15@59730 ` 1116` ``` shows "summable (\n. norm (x^n /\<^sub>R fact n))" ``` huffman@23115 ` 1117` ```proof (rule summable_norm_comparison_test [OF exI, rule_format]) ``` lp15@59730 ` 1118` ``` show "summable (\n. norm x^n /\<^sub>R fact n)" ``` huffman@23115 ` 1119` ``` by (rule summable_exp_generic) ``` wenzelm@53079 ` 1120` ``` fix n ``` lp15@59730 ` 1121` ``` show "norm (x^n /\<^sub>R fact n) \ norm x^n /\<^sub>R fact n" ``` huffman@35216 ` 1122` ``` by (simp add: norm_power_ineq) ``` huffman@23115 ` 1123` ```qed ``` huffman@23115 ` 1124` lp15@59730 ` 1125` ```lemma summable_exp: ``` lp15@59730 ` 1126` ``` fixes x :: "'a::{real_normed_field,banach}" ``` lp15@59730 ` 1127` ``` shows "summable (\n. inverse (fact n) * x^n)" ``` lp15@59730 ` 1128` ``` using summable_exp_generic [where x=x] ``` lp15@59730 ` 1129` ``` by (simp add: scaleR_conv_of_real nonzero_of_real_inverse) ``` lp15@59730 ` 1130` lp15@59730 ` 1131` ```lemma exp_converges: "(\n. x^n /\<^sub>R fact n) sums exp x" ``` wenzelm@53079 ` 1132` ``` unfolding exp_def by (rule summable_exp_generic [THEN summable_sums]) ``` huffman@23043 ` 1133` hoelzl@41970 ` 1134` ```lemma exp_fdiffs: ``` lp15@59730 ` 1135` ``` fixes XXX :: "'a::{real_normed_field,banach}" ``` lp15@59730 ` 1136` ``` shows "diffs (\n. inverse (fact n)) = (\n. inverse (fact n :: 'a))" ``` lp15@59730 ` 1137` ``` by (simp add: diffs_def mult_ac nonzero_inverse_mult_distrib nonzero_of_real_inverse ``` lp15@59730 ` 1138` ``` del: mult_Suc of_nat_Suc) ``` paulson@15077 ` 1139` huffman@23115 ` 1140` ```lemma diffs_of_real: "diffs (\n. of_real (f n)) = (\n. of_real (diffs f n))" ``` wenzelm@53079 ` 1141` ``` by (simp add: diffs_def) ``` huffman@23115 ` 1142` paulson@15077 ` 1143` ```lemma DERIV_exp [simp]: "DERIV exp x :> exp(x)" ``` wenzelm@53079 ` 1144` ``` unfolding exp_def scaleR_conv_of_real ``` wenzelm@53079 ` 1145` ``` apply (rule DERIV_cong) ``` wenzelm@53079 ` 1146` ``` apply (rule termdiffs [where K="of_real (1 + norm x)"]) ``` wenzelm@53079 ` 1147` ``` apply (simp_all only: diffs_of_real scaleR_conv_of_real exp_fdiffs) ``` wenzelm@53079 ` 1148` ``` apply (rule exp_converges [THEN sums_summable, unfolded scaleR_conv_of_real])+ ``` wenzelm@53079 ` 1149` ``` apply (simp del: of_real_add) ``` wenzelm@53079 ` 1150` ``` done ``` paulson@15077 ` 1151` hoelzl@56381 ` 1152` ```declare DERIV_exp[THEN DERIV_chain2, derivative_intros] ``` hoelzl@51527 ` 1153` immler@58656 ` 1154` ```lemma norm_exp: "norm (exp x) \ exp (norm x)" ``` immler@58656 ` 1155` ```proof - ``` immler@58656 ` 1156` ``` from summable_norm[OF summable_norm_exp, of x] ``` lp15@59730 ` 1157` ``` have "norm (exp x) \ (\n. inverse (fact n) * norm (x^n))" ``` immler@58656 ` 1158` ``` by (simp add: exp_def) ``` immler@58656 ` 1159` ``` also have "\ \ exp (norm x)" ``` immler@58656 ` 1160` ``` using summable_exp_generic[of "norm x"] summable_norm_exp[of x] ``` immler@58656 ` 1161` ``` by (auto simp: exp_def intro!: suminf_le norm_power_ineq) ``` immler@58656 ` 1162` ``` finally show ?thesis . ``` immler@58656 ` 1163` ```qed ``` immler@58656 ` 1164` immler@58656 ` 1165` ```lemma isCont_exp: ``` immler@58656 ` 1166` ``` fixes x::"'a::{real_normed_field,banach}" ``` immler@58656 ` 1167` ``` shows "isCont exp x" ``` huffman@44311 ` 1168` ``` by (rule DERIV_exp [THEN DERIV_isCont]) ``` huffman@44311 ` 1169` immler@58656 ` 1170` ```lemma isCont_exp' [simp]: ``` lp15@59613 ` 1171` ``` fixes f:: "_ \'a::{real_normed_field,banach}" ``` immler@58656 ` 1172` ``` shows "isCont f a \ isCont (\x. exp (f x)) a" ``` huffman@44311 ` 1173` ``` by (rule isCont_o2 [OF _ isCont_exp]) ``` huffman@44311 ` 1174` huffman@44311 ` 1175` ```lemma tendsto_exp [tendsto_intros]: ``` lp15@59613 ` 1176` ``` fixes f:: "_ \'a::{real_normed_field,banach}" ``` immler@58656 ` 1177` ``` shows "(f ---> a) F \ ((\x. exp (f x)) ---> exp a) F" ``` huffman@44311 ` 1178` ``` by (rule isCont_tendsto_compose [OF isCont_exp]) ``` huffman@23045 ` 1179` wenzelm@53079 ` 1180` ```lemma continuous_exp [continuous_intros]: ``` lp15@59613 ` 1181` ``` fixes f:: "_ \'a::{real_normed_field,banach}" ``` immler@58656 ` 1182` ``` shows "continuous F f \ continuous F (\x. exp (f x))" ``` hoelzl@51478 ` 1183` ``` unfolding continuous_def by (rule tendsto_exp) ``` hoelzl@51478 ` 1184` hoelzl@56371 ` 1185` ```lemma continuous_on_exp [continuous_intros]: ``` lp15@59613 ` 1186` ``` fixes f:: "_ \'a::{real_normed_field,banach}" ``` immler@58656 ` 1187` ``` shows "continuous_on s f \ continuous_on s (\x. exp (f x))" ``` hoelzl@51478 ` 1188` ``` unfolding continuous_on_def by (auto intro: tendsto_exp) ``` hoelzl@51478 ` 1189` wenzelm@53079 ` 1190` huffman@29167 ` 1191` ```subsubsection {* Properties of the Exponential Function *} ``` paulson@15077 ` 1192` huffman@23278 ` 1193` ```lemma exp_zero [simp]: "exp 0 = 1" ``` wenzelm@53079 ` 1194` ``` unfolding exp_def by (simp add: scaleR_conv_of_real powser_zero) ``` huffman@23278 ` 1195` immler@58656 ` 1196` ```lemma exp_series_add_commuting: ``` immler@58656 ` 1197` ``` fixes x y :: "'a::{real_normed_algebra_1, banach}" ``` lp15@59730 ` 1198` ``` defines S_def: "S \ \x n. x^n /\<^sub>R fact n" ``` immler@58656 ` 1199` ``` assumes comm: "x * y = y * x" ``` hoelzl@56213 ` 1200` ``` shows "S (x + y) n = (\i\n. S x i * S y (n - i))" ``` huffman@23115 ` 1201` ```proof (induct n) ``` huffman@23115 ` 1202` ``` case 0 ``` huffman@23115 ` 1203` ``` show ?case ``` huffman@23115 ` 1204` ``` unfolding S_def by simp ``` huffman@23115 ` 1205` ```next ``` huffman@23115 ` 1206` ``` case (Suc n) ``` haftmann@25062 ` 1207` ``` have S_Suc: "\x n. S x (Suc n) = (x * S x n) /\<^sub>R real (Suc n)" ``` huffman@30273 ` 1208` ``` unfolding S_def by (simp del: mult_Suc) ``` haftmann@25062 ` 1209` ``` hence times_S: "\x n. x * S x n = real (Suc n) *\<^sub>R S x (Suc n)" ``` huffman@23115 ` 1210` ``` by simp ``` immler@58656 ` 1211` ``` have S_comm: "\n. S x n * y = y * S x n" ``` immler@58656 ` 1212` ``` by (simp add: power_commuting_commutes comm S_def) ``` huffman@23115 ` 1213` haftmann@25062 ` 1214` ``` have "real (Suc n) *\<^sub>R S (x + y) (Suc n) = (x + y) * S (x + y) n" ``` huffman@23115 ` 1215` ``` by (simp only: times_S) ``` hoelzl@56213 ` 1216` ``` also have "\ = (x + y) * (\i\n. S x i * S y (n-i))" ``` huffman@23115 ` 1217` ``` by (simp only: Suc) ``` hoelzl@56213 ` 1218` ``` also have "\ = x * (\i\n. S x i * S y (n-i)) ``` hoelzl@56213 ` 1219` ``` + y * (\i\n. S x i * S y (n-i))" ``` webertj@49962 ` 1220` ``` by (rule distrib_right) ``` immler@58656 ` 1221` ``` also have "\ = (\i\n. x * S x i * S y (n-i)) ``` immler@58656 ` 1222` ``` + (\i\n. S x i * y * S y (n-i))" ``` immler@58656 ` 1223` ``` by (simp add: setsum_right_distrib ac_simps S_comm) ``` immler@58656 ` 1224` ``` also have "\ = (\i\n. x * S x i * S y (n-i)) ``` hoelzl@56213 ` 1225` ``` + (\i\n. S x i * (y * S y (n-i)))" ``` immler@58656 ` 1226` ``` by (simp add: ac_simps) ``` hoelzl@56213 ` 1227` ``` also have "\ = (\i\n. real (Suc i) *\<^sub>R (S x (Suc i) * S y (n-i))) ``` hoelzl@56213 ` 1228` ``` + (\i\n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i)))" ``` huffman@23115 ` 1229` ``` by (simp add: times_S Suc_diff_le) ``` hoelzl@56213 ` 1230` ``` also have "(\i\n. real (Suc i) *\<^sub>R (S x (Suc i) * S y (n-i))) = ``` hoelzl@56213 ` 1231` ``` (\i\Suc n. real i *\<^sub>R (S x i * S y (Suc n-i)))" ``` hoelzl@56213 ` 1232` ``` by (subst setsum_atMost_Suc_shift) simp ``` hoelzl@56213 ` 1233` ``` also have "(\i\n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i))) = ``` hoelzl@56213 ` 1234` ``` (\i\Suc n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i)))" ``` hoelzl@56213 ` 1235` ``` by simp ``` hoelzl@56213 ` 1236` ``` also have "(\i\Suc n. real i *\<^sub>R (S x i * S y (Suc n-i))) + ``` hoelzl@56213 ` 1237` ``` (\i\Suc n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i))) = ``` hoelzl@56213 ` 1238` ``` (\i\Suc n. real (Suc n) *\<^sub>R (S x i * S y (Suc n-i)))" ``` haftmann@57418 ` 1239` ``` by (simp only: setsum.distrib [symmetric] scaleR_left_distrib [symmetric] ``` hoelzl@56213 ` 1240` ``` real_of_nat_add [symmetric]) simp ``` hoelzl@56213 ` 1241` ``` also have "\ = real (Suc n) *\<^sub>R (\i\Suc n. S x i * S y (Suc n-i))" ``` huffman@23127 ` 1242` ``` by (simp only: scaleR_right.setsum) ``` huffman@23115 ` 1243` ``` finally show ``` hoelzl@56213 ` 1244` ``` "S (x + y) (Suc n) = (\i\Suc n. S x i * S y (Suc n - i))" ``` huffman@35216 ` 1245` ``` by (simp del: setsum_cl_ivl_Suc) ``` huffman@23115 ` 1246` ```qed ``` huffman@23115 ` 1247` immler@58656 ` 1248` ```lemma exp_add_commuting: "x * y = y * x \ exp (x + y) = exp x * exp y" ``` wenzelm@53079 ` 1249` ``` unfolding exp_def ``` immler@58656 ` 1250` ``` by (simp only: Cauchy_product summable_norm_exp exp_series_add_commuting) ``` immler@58656 ` 1251` immler@58656 ` 1252` ```lemma exp_add: ``` immler@58656 ` 1253` ``` fixes x y::"'a::{real_normed_field,banach}" ``` immler@58656 ` 1254` ``` shows "exp (x + y) = exp x * exp y" ``` immler@58656 ` 1255` ``` by (rule exp_add_commuting) (simp add: ac_simps) ``` immler@58656 ` 1256` lp15@59613 ` 1257` ```lemma exp_double: "exp(2 * z) = exp z ^ 2" ``` lp15@59613 ` 1258` ``` by (simp add: exp_add_commuting mult_2 power2_eq_square) ``` lp15@59613 ` 1259` immler@58656 ` 1260` ```lemmas mult_exp_exp = exp_add [symmetric] ``` huffman@29170 ` 1261` huffman@23241 ` 1262` ```lemma exp_of_real: "exp (of_real x) = of_real (exp x)" ``` wenzelm@53079 ` 1263` ``` unfolding exp_def ``` wenzelm@53079 ` 1264` ``` apply (subst suminf_of_real) ``` wenzelm@53079 ` 1265` ``` apply (rule summable_exp_generic) ``` wenzelm@53079 ` 1266` ``` apply (simp add: scaleR_conv_of_real) ``` wenzelm@53079 ` 1267` ``` done ``` huffman@23241 ` 1268` lp15@59862 ` 1269` ```corollary exp_in_Reals [simp]: "z \ \ \ exp z \ \" ``` lp15@59862 ` 1270` ``` by (metis Reals_cases Reals_of_real exp_of_real) ``` lp15@59862 ` 1271` huffman@29170 ` 1272` ```lemma exp_not_eq_zero [simp]: "exp x \ 0" ``` huffman@29170 ` 1273` ```proof ``` immler@58656 ` 1274` ``` have "exp x * exp (- x) = 1" by (simp add: exp_add_commuting[symmetric]) ``` huffman@29170 ` 1275` ``` also assume "exp x = 0" ``` huffman@29170 ` 1276` ``` finally show "False" by simp ``` paulson@15077 ` 1277` ```qed ``` paulson@15077 ` 1278` immler@58656 ` 1279` ```lemma exp_minus_inverse: ``` immler@58656 ` 1280` ``` shows "exp x * exp (- x) = 1" ``` immler@58656 ` 1281` ``` by (simp add: exp_add_commuting[symmetric]) ``` immler@58656 ` 1282` immler@58656 ` 1283` ```lemma exp_minus: ``` immler@58656 ` 1284` ``` fixes x :: "'a::{real_normed_field, banach}" ``` immler@58656 ` 1285` ``` shows "exp (- x) = inverse (exp x)" ``` immler@58656 ` 1286` ``` by (intro inverse_unique [symmetric] exp_minus_inverse) ``` immler@58656 ` 1287` immler@58656 ` 1288` ```lemma exp_diff: ``` immler@58656 ` 1289` ``` fixes x :: "'a::{real_normed_field, banach}" ``` immler@58656 ` 1290` ``` shows "exp (x - y) = exp x / exp y" ``` haftmann@54230 ` 1291` ``` using exp_add [of x "- y"] by (simp add: exp_minus divide_inverse) ``` paulson@15077 ` 1292` lp15@59613 ` 1293` ```lemma exp_of_nat_mult: ``` lp15@59613 ` 1294` ``` fixes x :: "'a::{real_normed_field,banach}" ``` lp15@59613 ` 1295` ``` shows "exp(of_nat n * x) = exp(x) ^ n" ``` lp15@60162 ` 1296` ``` by (induct n) (auto simp add: power_Suc distrib_left exp_add mult.commute) ``` lp15@60162 ` 1297` lp15@60162 ` 1298` ```corollary exp_real_of_nat_mult: "exp(real n * x) = exp(x) ^ n" ``` lp15@60162 ` 1299` ``` by (simp add: exp_of_nat_mult real_of_nat_def) ``` lp15@59613 ` 1300` lp15@59613 ` 1301` ```lemma exp_setsum: "finite I \ exp(setsum f I) = setprod (\x. exp(f x)) I" ``` lp15@59613 ` 1302` ``` by (induction I rule: finite_induct) (auto simp: exp_add_commuting mult.commute) ``` lp15@59613 ` 1303` huffman@29167 ` 1304` huffman@29167 ` 1305` ```subsubsection {* Properties of the Exponential Function on Reals *} ``` huffman@29167 ` 1306` huffman@29170 ` 1307` ```text {* Comparisons of @{term "exp x"} with zero. *} ``` huffman@29167 ` 1308` huffman@29167 ` 1309` ```text{*Proof: because every exponential can be seen as a square.*} ``` huffman@29167 ` 1310` ```lemma exp_ge_zero [simp]: "0 \ exp (x::real)" ``` huffman@29167 ` 1311` ```proof - ``` huffman@29167 ` 1312` ``` have "0 \ exp (x/2) * exp (x/2)" by simp ``` huffman@29167 ` 1313` ``` thus ?thesis by (simp add: exp_add [symmetric]) ``` huffman@29167 ` 1314` ```qed ``` huffman@29167 ` 1315` huffman@23115 ` 1316` ```lemma exp_gt_zero [simp]: "0 < exp (x::real)" ``` wenzelm@53079 ` 1317` ``` by (simp add: order_less_le) ``` paulson@15077 ` 1318` huffman@29170 ` 1319` ```lemma not_exp_less_zero [simp]: "\ exp (x::real) < 0" ``` wenzelm@53079 ` 1320` ``` by (simp add: not_less) ``` huffman@29170 ` 1321` huffman@29170 ` 1322` ```lemma not_exp_le_zero [simp]: "\ exp (x::real) \ 0" ``` wenzelm@53079 ` 1323` ``` by (simp add: not_le) ``` paulson@15077 ` 1324` huffman@23115 ` 1325` ```lemma abs_exp_cancel [simp]: "\exp x::real\ = exp x" ``` wenzelm@53079 ` 1326` ``` by simp ``` paulson@15077 ` 1327` huffman@29170 ` 1328` ```text {* Strict monotonicity of exponential. *} ``` huffman@29170 ` 1329` lp15@59669 ` 1330` ```lemma exp_ge_add_one_self_aux: ``` paulson@54575 ` 1331` ``` assumes "0 \ (x::real)" shows "1+x \ exp(x)" ``` paulson@54575 ` 1332` ```using order_le_imp_less_or_eq [OF assms] ``` lp15@59669 ` 1333` ```proof ``` paulson@54575 ` 1334` ``` assume "0 < x" ``` lp15@59730 ` 1335` ``` have "1+x \ (\n<2. inverse (fact n) * x^n)" ``` paulson@54575 ` 1336` ``` by (auto simp add: numeral_2_eq_2) ``` lp15@59730 ` 1337` ``` also have "... \ (\n. inverse (fact n) * x^n)" ``` hoelzl@56213 ` 1338` ``` apply (rule setsum_le_suminf [OF summable_exp]) ``` paulson@54575 ` 1339` ``` using `0 < x` ``` paulson@54575 ` 1340` ``` apply (auto simp add: zero_le_mult_iff) ``` paulson@54575 ` 1341` ``` done ``` lp15@59669 ` 1342` ``` finally show "1+x \ exp x" ``` paulson@54575 ` 1343` ``` by (simp add: exp_def) ``` paulson@54575 ` 1344` ```next ``` paulson@54575 ` 1345` ``` assume "0 = x" ``` paulson@54575 ` 1346` ``` then show "1 + x \ exp x" ``` paulson@54575 ` 1347` ``` by auto ``` paulson@54575 ` 1348` ```qed ``` huffman@29170 ` 1349` huffman@29170 ` 1350` ```lemma exp_gt_one: "0 < (x::real) \ 1 < exp x" ``` huffman@29170 ` 1351` ```proof - ``` huffman@29170 ` 1352` ``` assume x: "0 < x" ``` huffman@29170 ` 1353` ``` hence "1 < 1 + x" by simp ``` huffman@29170 ` 1354` ``` also from x have "1 + x \ exp x" ``` huffman@29170 ` 1355` ``` by (simp add: exp_ge_add_one_self_aux) ``` huffman@29170 ` 1356` ``` finally show ?thesis . ``` huffman@29170 ` 1357` ```qed ``` huffman@29170 ` 1358` paulson@15077 ` 1359` ```lemma exp_less_mono: ``` huffman@23115 ` 1360` ``` fixes x y :: real ``` wenzelm@53079 ` 1361` ``` assumes "x < y" ``` wenzelm@53079 ` 1362` ``` shows "exp x < exp y" ``` paulson@15077 ` 1363` ```proof - ``` huffman@29165 ` 1364` ``` from `x < y` have "0 < y - x" by simp ``` huffman@29165 ` 1365` ``` hence "1 < exp (y - x)" by (rule exp_gt_one) ``` huffman@29165 ` 1366` ``` hence "1 < exp y / exp x" by (simp only: exp_diff) ``` huffman@29165 ` 1367` ``` thus "exp x < exp y" by simp ``` paulson@15077 ` 1368` ```qed ``` paulson@15077 ` 1369` wenzelm@53079 ` 1370` ```lemma exp_less_cancel: "exp (x::real) < exp y \ x < y" ``` paulson@54575 ` 1371` ``` unfolding linorder_not_le [symmetric] ``` paulson@54575 ` 1372` ``` by (auto simp add: order_le_less exp_less_mono) ``` paulson@15077 ` 1373` huffman@29170 ` 1374` ```lemma exp_less_cancel_iff [iff]: "exp (x::real) < exp y \ x < y" ``` wenzelm@53079 ` 1375` ``` by (auto intro: exp_less_mono exp_less_cancel) ``` paulson@15077 ` 1376` huffman@29170 ` 1377` ```lemma exp_le_cancel_iff [iff]: "exp (x::real) \ exp y \ x \ y" ``` wenzelm@53079 ` 1378` ``` by (auto simp add: linorder_not_less [symmetric]) ``` paulson@15077 ` 1379` huffman@29170 ` 1380` ```lemma exp_inj_iff [iff]: "exp (x::real) = exp y \ x = y" ``` wenzelm@53079 ` 1381` ``` by (simp add: order_eq_iff) ``` paulson@15077 ` 1382` huffman@29170 ` 1383` ```text {* Comparisons of @{term "exp x"} with one. *} ``` huffman@29170 ` 1384` huffman@29170 ` 1385` ```lemma one_less_exp_iff [simp]: "1 < exp (x::real) \ 0 < x" ``` huffman@29170 ` 1386` ``` using exp_less_cancel_iff [where x=0 and y=x] by simp ``` huffman@29170 ` 1387` huffman@29170 ` 1388` ```lemma exp_less_one_iff [simp]: "exp (x::real) < 1 \ x < 0" ``` huffman@29170 ` 1389` ``` using exp_less_cancel_iff [where x=x and y=0] by simp ``` huffman@29170 ` 1390` huffman@29170 ` 1391` ```lemma one_le_exp_iff [simp]: "1 \ exp (x::real) \ 0 \ x" ``` huffman@29170 ` 1392` ``` using exp_le_cancel_iff [where x=0 and y=x] by simp ``` huffman@29170 ` 1393` huffman@29170 ` 1394` ```lemma exp_le_one_iff [simp]: "exp (x::real) \ 1 \ x \ 0" ``` huffman@29170 ` 1395` ``` using exp_le_cancel_iff [where x=x and y=0] by simp ``` huffman@29170 ` 1396` huffman@29170 ` 1397` ```lemma exp_eq_one_iff [simp]: "exp (x::real) = 1 \ x = 0" ``` huffman@29170 ` 1398` ``` using exp_inj_iff [where x=x and y=0] by simp ``` huffman@29170 ` 1399` wenzelm@53079 ` 1400` ```lemma lemma_exp_total: "1 \ y \ \x. 0 \ x & x \ y - 1 & exp(x::real) = y" ``` huffman@44755 ` 1401` ```proof (rule IVT) ``` huffman@44755 ` 1402` ``` assume "1 \ y" ``` huffman@44755 ` 1403` ``` hence "0 \ y - 1" by simp ``` huffman@44755 ` 1404` ``` hence "1 + (y - 1) \ exp (y - 1)" by (rule exp_ge_add_one_self_aux) ``` huffman@44755 ` 1405` ``` thus "y \ exp (y - 1)" by simp ``` huffman@44755 ` 1406` ```qed (simp_all add: le_diff_eq) ``` paulson@15077 ` 1407` wenzelm@53079 ` 1408` ```lemma exp_total: "0 < (y::real) \ \x. exp x = y" ``` huffman@44755 ` 1409` ```proof (rule linorder_le_cases [of 1 y]) ``` wenzelm@53079 ` 1410` ``` assume "1 \ y" ``` wenzelm@53079 ` 1411` ``` thus "\x. exp x = y" by (fast dest: lemma_exp_total) ``` huffman@44755 ` 1412` ```next ``` huffman@44755 ` 1413` ``` assume "0 < y" and "y \ 1" ``` huffman@44755 ` 1414` ``` hence "1 \ inverse y" by (simp add: one_le_inverse_iff) ``` huffman@44755 ` 1415` ``` then obtain x where "exp x = inverse y" by (fast dest: lemma_exp_total) ``` huffman@44755 ` 1416` ``` hence "exp (- x) = y" by (simp add: exp_minus) ``` huffman@44755 ` 1417` ``` thus "\x. exp x = y" .. ``` huffman@44755 ` 1418` ```qed ``` paulson@15077 ` 1419` paulson@15077 ` 1420` huffman@29164 ` 1421` ```subsection {* Natural Logarithm *} ``` paulson@15077 ` 1422` lp15@60017 ` 1423` ```class ln = real_normed_algebra_1 + banach + ``` lp15@60017 ` 1424` ``` fixes ln :: "'a \ 'a" ``` lp15@60017 ` 1425` ``` assumes ln_one [simp]: "ln 1 = 0" ``` lp15@60017 ` 1426` lp15@60017 ` 1427` ```definition powr :: "['a,'a] => 'a::ln" (infixr "powr" 80) ``` lp15@60017 ` 1428` ``` -- {*exponentation via ln and exp*} ``` lp15@60020 ` 1429` ``` where [code del]: "x powr a \ if x = 0 then 0 else exp(a * ln x)" ``` lp15@60017 ` 1430` lp15@60141 ` 1431` ```lemma powr_0 [simp]: "0 powr z = 0" ``` lp15@60141 ` 1432` ``` by (simp add: powr_def) ``` lp15@60141 ` 1433` lp15@60017 ` 1434` lp15@60017 ` 1435` ```instantiation real :: ln ``` lp15@60017 ` 1436` ```begin ``` lp15@60017 ` 1437` lp15@60017 ` 1438` ```definition ln_real :: "real \ real" ``` lp15@60017 ` 1439` ``` where "ln_real x = (THE u. exp u = x)" ``` lp15@60017 ` 1440` lp15@60017 ` 1441` ```instance ``` lp15@60017 ` 1442` ```by intro_classes (simp add: ln_real_def) ``` lp15@60017 ` 1443` lp15@60017 ` 1444` ```end ``` lp15@60017 ` 1445` lp15@60017 ` 1446` ```lemma powr_eq_0_iff [simp]: "w powr z = 0 \ w = 0" ``` lp15@60017 ` 1447` ``` by (simp add: powr_def) ``` lp15@60017 ` 1448` lp15@60017 ` 1449` ```lemma ln_exp [simp]: ``` lp15@60017 ` 1450` ``` fixes x::real shows "ln (exp x) = x" ``` lp15@60017 ` 1451` ``` by (simp add: ln_real_def) ``` lp15@60017 ` 1452` lp15@60017 ` 1453` ```lemma exp_ln [simp]: ``` lp15@60017 ` 1454` ``` fixes x::real shows "0 < x \ exp (ln x) = x" ``` huffman@44308 ` 1455` ``` by (auto dest: exp_total) ``` huffman@22654 ` 1456` lp15@60017 ` 1457` ```lemma exp_ln_iff [simp]: ``` lp15@60017 ` 1458` ``` fixes x::real shows "exp (ln x) = x \ 0 < x" ``` huffman@44308 ` 1459` ``` by (metis exp_gt_zero exp_ln) ``` paulson@15077 ` 1460` lp15@60017 ` 1461` ```lemma ln_unique: ``` lp15@60017 ` 1462` ``` fixes x::real shows "exp y = x \ ln x = y" ``` huffman@44308 ` 1463` ``` by (erule subst, rule ln_exp) ``` huffman@29171 ` 1464` lp15@60017 ` 1465` ```lemma ln_mult: ``` lp15@60017 ` 1466` ``` fixes x::real shows "0 < x \ 0 < y \ ln (x * y) = ln x + ln y" ``` wenzelm@53079 ` 1467` ``` by (rule ln_unique) (simp add: exp_add) ``` huffman@29171 ` 1468` lp15@60017 ` 1469` ```lemma ln_setprod: ``` lp15@60017 ` 1470` ``` fixes f:: "'a => real" ``` lp15@60017 ` 1471` ``` shows ``` lp15@59746 ` 1472` ``` "\finite I; \i. i \ I \ f i > 0\ \ ln(setprod f I) = setsum (\x. ln(f x)) I" ``` lp15@59746 ` 1473` ``` by (induction I rule: finite_induct) (auto simp: ln_mult setprod_pos) ``` lp15@59746 ` 1474` lp15@60017 ` 1475` ```lemma ln_inverse: ``` lp15@60017 ` 1476` ``` fixes x::real shows "0 < x \ ln (inverse x) = - ln x" ``` wenzelm@53079 ` 1477` ``` by (rule ln_unique) (simp add: exp_minus) ``` wenzelm@53079 ` 1478` lp15@60017 ` 1479` ```lemma ln_div: ``` lp15@60017 ` 1480` ``` fixes x::real shows "0 < x \ 0 < y \ ln (x / y) = ln x - ln y" ``` wenzelm@53079 ` 1481` ``` by (rule ln_unique) (simp add: exp_diff) ``` paulson@15077 ` 1482` lp15@59730 ` 1483` ```lemma ln_realpow: "0 < x \ ln (x^n) = real n * ln x" ``` wenzelm@53079 ` 1484` ``` by (rule ln_unique) (simp add: exp_real_of_nat_mult) ``` wenzelm@53079 ` 1485` lp15@60017 ` 1486` ```lemma ln_less_cancel_iff [simp]: ``` lp15@60017 ` 1487` ``` fixes x::real shows "0 < x \ 0 < y \ ln x < ln y \ x < y" ``` wenzelm@53079 ` 1488` ``` by (subst exp_less_cancel_iff [symmetric]) simp ``` wenzelm@53079 ` 1489` lp15@60017 ` 1490` ```lemma ln_le_cancel_iff [simp]: ``` lp15@60017 ` 1491` ``` fixes x::real shows "0 < x \ 0 < y \ ln x \ ln y \ x \ y" ``` huffman@44308 ` 1492` ``` by (simp add: linorder_not_less [symmetric]) ``` huffman@29171 ` 1493` lp15@60017 ` 1494` ```lemma ln_inj_iff [simp]: ``` lp15@60017 ` 1495` ``` fixes x::real shows "0 < x \ 0 < y \ ln x = ln y \ x = y" ``` huffman@44308 ` 1496` ``` by (simp add: order_eq_iff) ``` huffman@29171 ` 1497` lp15@60017 ` 1498` ```lemma ln_add_one_self_le_self [simp]: ``` lp15@60017 ` 1499` ``` fixes x::real shows "0 \ x \ ln (1 + x) \ x" ``` huffman@44308 ` 1500` ``` apply (rule exp_le_cancel_iff [THEN iffD1]) ``` huffman@44308 ` 1501` ``` apply (simp add: exp_ge_add_one_self_aux) ``` huffman@44308 ` 1502` ``` done ``` paulson@15077 ` 1503` lp15@60017 ` 1504` ```lemma ln_less_self [simp]: ``` lp15@60017 ` 1505` ``` fixes x::real shows "0 < x \ ln x < x" ``` huffman@44308 ` 1506` ``` by (rule order_less_le_trans [where y="ln (1 + x)"]) simp_all ``` huffman@44308 ` 1507` lp15@60017 ` 1508` ```lemma ln_ge_zero [simp]: ``` lp15@60017 ` 1509` ``` fixes x::real shows "1 \ x \ 0 \ ln x" ``` huffman@44308 ` 1510` ``` using ln_le_cancel_iff [of 1 x] by simp ``` huffman@44308 ` 1511` lp15@60017 ` 1512` ```lemma ln_ge_zero_imp_ge_one: ``` lp15@60017 ` 1513` ``` fixes x::real shows "0 \ ln x \ 0 < x \ 1 \ x" ``` huffman@44308 ` 1514` ``` using ln_le_cancel_iff [of 1 x] by simp ``` huffman@44308 ` 1515` lp15@60017 ` 1516` ```lemma ln_ge_zero_iff [simp]: ``` lp15@60017 ` 1517` ``` fixes x::real shows "0 < x \ 0 \ ln x \ 1 \ x" ``` huffman@44308 ` 1518` ``` using ln_le_cancel_iff [of 1 x] by simp ``` huffman@44308 ` 1519` lp15@60017 ` 1520` ```lemma ln_less_zero_iff [simp]: ``` lp15@60017 ` 1521` ``` fixes x::real shows "0 < x \ ln x < 0 \ x < 1" ``` huffman@44308 ` 1522` ``` using ln_less_cancel_iff [of x 1] by simp ``` huffman@44308 ` 1523` lp15@60017 ` 1524` ```lemma ln_gt_zero: ``` lp15@60017 ` 1525` ``` fixes x::real shows "1 < x \ 0 < ln x" ``` huffman@44308 ` 1526` ``` using ln_less_cancel_iff [of 1 x] by simp ``` huffman@44308 ` 1527` lp15@60017 ` 1528` ```lemma ln_gt_zero_imp_gt_one: ``` lp15@60017 ` 1529` ``` fixes x::real shows "0 < ln x \ 0 < x \ 1 < x" ``` huffman@44308 ` 1530` ``` using ln_less_cancel_iff [of 1 x] by simp ``` huffman@44308 ` 1531` lp15@60017 ` 1532` ```lemma ln_gt_zero_iff [simp]: ``` lp15@60017 ` 1533` ``` fixes x::real shows "0 < x \ 0 < ln x \ 1 < x" ``` huffman@44308 ` 1534` ``` using ln_less_cancel_iff [of 1 x] by simp ``` huffman@44308 ` 1535` lp15@60017 ` 1536` ```lemma ln_eq_zero_iff [simp]: ``` lp15@60017 ` 1537` ``` fixes x::real shows "0 < x \ ln x = 0 \ x = 1" ``` huffman@44308 ` 1538` ``` using ln_inj_iff [of x 1] by simp ``` huffman@44308 ` 1539` lp15@60017 ` 1540` ```lemma ln_less_zero: ``` lp15@60017 ` 1541` ``` fixes x::real shows "0 < x \ x < 1 \ ln x < 0" ``` huffman@44308 ` 1542` ``` by simp ``` paulson@15077 ` 1543` lp15@60017 ` 1544` ```lemma ln_neg_is_const: ``` lp15@60017 ` 1545` ``` fixes x::real shows "x \ 0 \ ln x = (THE x. False)" ``` lp15@60017 ` 1546` ``` by (auto simp add: ln_real_def intro!: arg_cong[where f=The]) ``` lp15@60017 ` 1547` lp15@60017 ` 1548` ```lemma isCont_ln: ``` lp15@60017 ` 1549` ``` fixes x::real assumes "x \ 0" shows "isCont ln x" ``` hoelzl@57275 ` 1550` ```proof cases ``` hoelzl@57275 ` 1551` ``` assume "0 < x" ``` hoelzl@57275 ` 1552` ``` moreover then have "isCont ln (exp (ln x))" ``` hoelzl@57275 ` 1553` ``` by (intro isCont_inv_fun[where d="\x\" and f=exp]) auto ``` hoelzl@57275 ` 1554` ``` ultimately show ?thesis ``` hoelzl@57275 ` 1555` ``` by simp ``` hoelzl@57275 ` 1556` ```next ``` hoelzl@57275 ` 1557` ``` assume "\ 0 < x" with `x \ 0` show "isCont ln x" ``` hoelzl@57275 ` 1558` ``` unfolding isCont_def ``` hoelzl@57275 ` 1559` ``` by (subst filterlim_cong[OF _ refl, of _ "nhds (ln 0)" _ "\_. ln 0"]) ``` hoelzl@57275 ` 1560` ``` (auto simp: ln_neg_is_const not_less eventually_at dist_real_def ``` hoelzl@58729 ` 1561` ``` intro!: exI[of _ "\x\"]) ``` hoelzl@57275 ` 1562` ```qed ``` huffman@23045 ` 1563` lp15@60017 ` 1564` ```lemma tendsto_ln [tendsto_intros]: ``` lp15@60017 ` 1565` ``` fixes a::real shows ``` hoelzl@57275 ` 1566` ``` "(f ---> a) F \ a \ 0 \ ((\x. ln (f x)) ---> ln a) F" ``` huffman@45915 ` 1567` ``` by (rule isCont_tendsto_compose [OF isCont_ln]) ``` huffman@45915 ` 1568` hoelzl@51478 ` 1569` ```lemma continuous_ln: ``` lp15@60017 ` 1570` ``` "continuous F f \ f (Lim F (\x. x)) \ 0 \ continuous F (\x. ln (f x :: real))" ``` hoelzl@51478 ` 1571` ``` unfolding continuous_def by (rule tendsto_ln) ``` hoelzl@51478 ` 1572` hoelzl@51478 ` 1573` ```lemma isCont_ln' [continuous_intros]: ``` lp15@60017 ` 1574` ``` "continuous (at x) f \ f x \ 0 \ continuous (at x) (\x. ln (f x :: real))" ``` hoelzl@51478 ` 1575` ``` unfolding continuous_at by (rule tendsto_ln) ``` hoelzl@51478 ` 1576` hoelzl@51478 ` 1577` ```lemma continuous_within_ln [continuous_intros]: ``` lp15@60017 ` 1578` ``` "continuous (at x within s) f \ f x \ 0 \ continuous (at x within s) (\x. ln (f x :: real))" ``` hoelzl@51478 ` 1579` ``` unfolding continuous_within by (rule tendsto_ln) ``` hoelzl@51478 ` 1580` hoelzl@56371 ` 1581` ```lemma continuous_on_ln [continuous_intros]: ``` lp15@60017 ` 1582` ``` "continuous_on s f \ (\x\s. f x \ 0) \ continuous_on s (\x. ln (f x :: real))" ``` hoelzl@51478 ` 1583` ``` unfolding continuous_on_def by (auto intro: tendsto_ln) ``` hoelzl@51478 ` 1584` lp15@60017 ` 1585` ```lemma DERIV_ln: ``` lp15@60017 ` 1586` ``` fixes x::real shows "0 < x \ DERIV ln x :> inverse x" ``` huffman@44308 ` 1587` ``` apply (rule DERIV_inverse_function [where f=exp and a=0 and b="x+1"]) ``` paulson@54576 ` 1588` ``` apply (auto intro: DERIV_cong [OF DERIV_exp exp_ln] isCont_ln) ``` huffman@44308 ` 1589` ``` done ``` huffman@23045 ` 1590` lp15@60017 ` 1591` ```lemma DERIV_ln_divide: ``` lp15@60017 ` 1592` ``` fixes x::real shows "0 < x \ DERIV ln x :> 1 / x" ``` paulson@33667 ` 1593` ``` by (rule DERIV_ln[THEN DERIV_cong], simp, simp add: divide_inverse) ``` paulson@33667 ` 1594` hoelzl@56381 ` 1595` ```declare DERIV_ln_divide[THEN DERIV_chain2, derivative_intros] ``` hoelzl@51527 ` 1596` wenzelm@53079 ` 1597` ```lemma ln_series: ``` wenzelm@53079 ` 1598` ``` assumes "0 < x" and "x < 2" ``` wenzelm@53079 ` 1599` ``` shows "ln x = (\ n. (-1)^n * (1 / real (n + 1)) * (x - 1)^(Suc n))" ``` wenzelm@53079 ` 1600` ``` (is "ln x = suminf (?f (x - 1))") ``` hoelzl@29803 ` 1601` ```proof - ``` wenzelm@53079 ` 1602` ``` let ?f' = "\x n. (-1)^n * (x - 1)^n" ``` hoelzl@29803 ` 1603` hoelzl@29803 ` 1604` ``` have "ln x - suminf (?f (x - 1)) = ln 1 - suminf (?f (1 - 1))" ``` hoelzl@29803 ` 1605` ``` proof (rule DERIV_isconst3[where x=x]) ``` wenzelm@53079 ` 1606` ``` fix x :: real ``` wenzelm@53079 ` 1607` ``` assume "x \ {0 <..< 2}" ``` wenzelm@53079 ` 1608` ``` hence "0 < x" and "x < 2" by auto ``` wenzelm@53079 ` 1609` ``` have "norm (1 - x) < 1" ``` wenzelm@53079 ` 1610` ``` using `0 < x` and `x < 2` by auto ``` hoelzl@29803 ` 1611` ``` have "1 / x = 1 / (1 - (1 - x))" by auto ``` wenzelm@53079 ` 1612` ``` also have "\ = (\ n. (1 - x)^n)" ``` wenzelm@53079 ` 1613` ``` using geometric_sums[OF `norm (1 - x) < 1`] by (rule sums_unique) ``` wenzelm@53079 ` 1614` ``` also have "\ = suminf (?f' x)" ``` wenzelm@53079 ` 1615` ``` unfolding power_mult_distrib[symmetric] ``` wenzelm@53079 ` 1616` ``` by (rule arg_cong[where f=suminf], rule arg_cong[where f="op ^"], auto) ``` wenzelm@53079 ` 1617` ``` finally have "DERIV ln x :> suminf (?f' x)" ``` wenzelm@53079 ` 1618` ``` using DERIV_ln[OF `0 < x`] unfolding divide_inverse by auto ``` hoelzl@29803 ` 1619` ``` moreover ``` hoelzl@29803 ` 1620` ``` have repos: "\ h x :: real. h - 1 + x = h + x - 1" by auto ``` wenzelm@53079 ` 1621` ``` have "DERIV (\x. suminf (?f x)) (x - 1) :> ``` wenzelm@53079 ` 1622` ``` (\n. (-1)^n * (1 / real (n + 1)) * real (Suc n) * (x - 1) ^ n)" ``` hoelzl@29803 ` 1623` ``` proof (rule DERIV_power_series') ``` wenzelm@53079 ` 1624` ``` show "x - 1 \ {- 1<..<1}" and "(0 :: real) < 1" ``` wenzelm@53079 ` 1625` ``` using `0 < x` `x < 2` by auto ``` wenzelm@53079 ` 1626` ``` fix x :: real ``` wenzelm@53079 ` 1627` ``` assume "x \ {- 1<..<1}" ``` wenzelm@53079 ` 1628` ``` hence "norm (-x) < 1" by auto ``` lp15@59730 ` 1629` ``` show "summable (\n. (- 1) ^ n * (1 / real (n + 1)) * real (Suc n) * x^n)" ``` wenzelm@53079 ` 1630` ``` unfolding One_nat_def ``` wenzelm@53079 ` 1631` ``` by (auto simp add: power_mult_distrib[symmetric] summable_geometric[OF `norm (-x) < 1`]) ``` hoelzl@29803 ` 1632` ``` qed ``` wenzelm@53079 ` 1633` ``` hence "DERIV (\x. suminf (?f x)) (x - 1) :> suminf (?f' x)" ``` wenzelm@53079 ` 1634` ``` unfolding One_nat_def by auto ``` wenzelm@53079 ` 1635` ``` hence "DERIV (\x. suminf (?f (x - 1))) x :> suminf (?f' x)" ``` hoelzl@56381 ` 1636` ``` unfolding DERIV_def repos . ``` hoelzl@29803 ` 1637` ``` ultimately have "DERIV (\x. ln x - suminf (?f (x - 1))) x :> (suminf (?f' x) - suminf (?f' x))" ``` hoelzl@29803 ` 1638` ``` by (rule DERIV_diff) ``` hoelzl@29803 ` 1639` ``` thus "DERIV (\x. ln x - suminf (?f (x - 1))) x :> 0" by auto ``` hoelzl@29803 ` 1640` ``` qed (auto simp add: assms) ``` huffman@44289 ` 1641` ``` thus ?thesis by auto ``` hoelzl@29803 ` 1642` ```qed ``` paulson@15077 ` 1643` lp15@59730 ` 1644` ```lemma exp_first_two_terms: ``` lp15@59730 ` 1645` ``` fixes x :: "'a::{real_normed_field,banach}" ``` lp15@59730 ` 1646` ``` shows "exp x = 1 + x + (\ n. inverse(fact (n+2)) * (x ^ (n+2)))" ``` hoelzl@50326 ` 1647` ```proof - ``` lp15@59730 ` 1648` ``` have "exp x = suminf (\n. inverse(fact n) * (x^n))" ``` lp15@59730 ` 1649` ``` by (simp add: exp_def scaleR_conv_of_real nonzero_of_real_inverse) ``` lp15@59669 ` 1650` ``` also from summable_exp have "... = (\ n. inverse(fact(n+2)) * (x ^ (n+2))) + ``` lp15@59730 ` 1651` ``` (\ n::nat<2. inverse(fact n) * (x^n))" (is "_ = _ + ?a") ``` hoelzl@50326 ` 1652` ``` by (rule suminf_split_initial_segment) ``` hoelzl@50326 ` 1653` ``` also have "?a = 1 + x" ``` hoelzl@50326 ` 1654` ``` by (simp add: numeral_2_eq_2) ``` hoelzl@56193 ` 1655` ``` finally show ?thesis ``` hoelzl@56193 ` 1656` ``` by simp ``` hoelzl@50326 ` 1657` ```qed ``` hoelzl@50326 ` 1658` wenzelm@53079 ` 1659` ```lemma exp_bound: "0 <= (x::real) \ x <= 1 \ exp x <= 1 + x + x\<^sup>2" ``` hoelzl@50326 ` 1660` ```proof - ``` hoelzl@50326 ` 1661` ``` assume a: "0 <= x" ``` hoelzl@50326 ` 1662` ``` assume b: "x <= 1" ``` wenzelm@53079 ` 1663` ``` { ``` wenzelm@53079 ` 1664` ``` fix n :: nat ``` lp15@59730 ` 1665` ``` have "(2::nat) * 2 ^ n \ fact (n + 2)" ``` wenzelm@53079 ` 1666` ``` by (induct n) simp_all ``` lp15@59730 ` 1667` ``` hence "real ((2::nat) * 2 ^ n) \ real_of_nat (fact (n + 2))" ``` hoelzl@50326 ` 1668` ``` by (simp only: real_of_nat_le_iff) ``` lp15@59730 ` 1669` ``` hence "((2::real) * 2 ^ n) \ fact (n + 2)" ``` lp15@59730 ` 1670` ``` unfolding of_nat_fact real_of_nat_def ``` lp15@59730 ` 1671` ``` by (simp add: of_nat_mult of_nat_power) ``` lp15@59730 ` 1672` ``` hence "inverse (fact (n + 2)) \ inverse ((2::real) * 2 ^ n)" ``` hoelzl@50326 ` 1673` ``` by (rule le_imp_inverse_le) simp ``` lp15@59730 ` 1674` ``` hence "inverse (fact (n + 2)) \ 1/(2::real) * (1/2)^n" ``` wenzelm@53079 ` 1675` ``` by (simp add: power_inverse) ``` wenzelm@53015 ` 1676` ``` hence "inverse (fact (n + 2)) * (x^n * x\<^sup>2) \ 1/2 * (1/2)^n * (1 * x\<^sup>2)" ``` hoelzl@50326 ` 1677` ``` by (rule mult_mono) ``` nipkow@56536 ` 1678` ``` (rule mult_mono, simp_all add: power_le_one a b) ``` wenzelm@53015 ` 1679` ``` hence "inverse (fact (n + 2)) * x ^ (n + 2) \ (x\<^sup>2/2) * ((1/2)^n)" ``` lp15@59730 ` 1680` ``` unfolding power_add by (simp add: ac_simps del: fact.simps) } ``` hoelzl@50326 ` 1681` ``` note aux1 = this ``` wenzelm@53015 ` 1682` ``` have "(\n. x\<^sup>2 / 2 * (1 / 2) ^ n) sums (x\<^sup>2 / 2 * (1 / (1 - 1 / 2)))" ``` hoelzl@50326 ` 1683` ``` by (intro sums_mult geometric_sums, simp) ``` wenzelm@53076 ` 1684` ``` hence aux2: "(\n. x\<^sup>2 / 2 * (1 / 2) ^ n) sums x\<^sup>2" ``` hoelzl@50326 ` 1685` ``` by simp ``` wenzelm@53079 ` 1686` ``` have "suminf (\n. inverse(fact (n+2)) * (x ^ (n+2))) <= x\<^sup>2" ``` hoelzl@50326 ` 1687` ``` proof - ``` wenzelm@53079 ` 1688` ``` have "suminf (\n. inverse(fact (n+2)) * (x ^ (n+2))) <= ``` wenzelm@53079 ` 1689` ``` suminf (\n. (x\<^sup>2/2) * ((1/2)^n))" ``` hoelzl@56213 ` 1690` ``` apply (rule suminf_le) ``` hoelzl@50326 ` 1691` ``` apply (rule allI, rule aux1) ``` hoelzl@50326 ` 1692` ``` apply (rule summable_exp [THEN summable_ignore_initial_segment]) ``` hoelzl@50326 ` 1693` ``` by (rule sums_summable, rule aux2) ``` wenzelm@53076 ` 1694` ``` also have "... = x\<^sup>2" ``` hoelzl@50326 ` 1695` ``` by (rule sums_unique [THEN sym], rule aux2) ``` hoelzl@50326 ` 1696` ``` finally show ?thesis . ``` hoelzl@50326 ` 1697` ``` qed ``` hoelzl@50326 ` 1698` ``` thus ?thesis unfolding exp_first_two_terms by auto ``` hoelzl@50326 ` 1699` ```qed ``` hoelzl@50326 ` 1700` lp15@59613 ` 1701` ```corollary exp_half_le2: "exp(1/2) \ (2::real)" ``` lp15@59613 ` 1702` ``` using exp_bound [of "1/2"] ``` lp15@59613 ` 1703` ``` by (simp add: field_simps) ``` lp15@59613 ` 1704` lp15@59741 ` 1705` ```corollary exp_le: "exp 1 \ (3::real)" ``` lp15@59741 ` 1706` ``` using exp_bound [of 1] ``` lp15@59741 ` 1707` ``` by (simp add: field_simps) ``` lp15@59741 ` 1708` lp15@59613 ` 1709` ```lemma exp_bound_half: "norm(z) \ 1/2 \ norm(exp z) \ 2" ``` lp15@59613 ` 1710` ``` by (blast intro: order_trans intro!: exp_half_le2 norm_exp) ``` lp15@59613 ` 1711` lp15@59613 ` 1712` ```lemma exp_bound_lemma: ``` lp15@59613 ` 1713` ``` assumes "norm(z) \ 1/2" shows "norm(exp z) \ 1 + 2 * norm(z)" ``` lp15@59613 ` 1714` ```proof - ``` lp15@59613 ` 1715` ``` have n: "(norm z)\<^sup>2 \ norm z * 1" ``` lp15@59613 ` 1716` ``` unfolding power2_eq_square ``` lp15@59613 ` 1717` ``` apply (rule mult_left_mono) ``` lp15@59613 ` 1718` ``` using assms ``` lp15@60017 ` 1719` ``` apply auto ``` lp15@59613 ` 1720` ``` done ``` lp15@59613 ` 1721` ``` show ?thesis ``` lp15@59613 ` 1722` ``` apply (rule order_trans [OF norm_exp]) ``` lp15@59613 ` 1723` ``` apply (rule order_trans [OF exp_bound]) ``` lp15@59613 ` 1724` ``` using assms n ``` lp15@60017 ` 1725` ``` apply auto ``` lp15@59613 ` 1726` ``` done ``` lp15@59613 ` 1727` ```qed ``` lp15@59613 ` 1728` lp15@59613 ` 1729` ```lemma real_exp_bound_lemma: ``` lp15@59613 ` 1730` ``` fixes x :: real ``` lp15@59613 ` 1731` ``` shows "0 \ x \ x \ 1/2 \ exp(x) \ 1 + 2 * x" ``` lp15@59613 ` 1732` ```using exp_bound_lemma [of x] ``` lp15@59613 ` 1733` ```by simp ``` lp15@59613 ` 1734` lp15@60017 ` 1735` ```lemma ln_one_minus_pos_upper_bound: ``` lp15@60017 ` 1736` ``` fixes x::real shows "0 <= x \ x < 1 \ ln (1 - x) <= - x" ``` hoelzl@50326 ` 1737` ```proof - ``` hoelzl@50326 ` 1738` ``` assume a: "0 <= (x::real)" and b: "x < 1" ``` wenzelm@53076 ` 1739` ``` have "(1 - x) * (1 + x + x\<^sup>2) = (1 - x^3)" ``` hoelzl@50326 ` 1740` ``` by (simp add: algebra_simps power2_eq_square power3_eq_cube) ``` hoelzl@50326 ` 1741` ``` also have "... <= 1" ``` hoelzl@50326 ` 1742` ``` by (auto simp add: a) ``` wenzelm@53076 ` 1743` ``` finally have "(1 - x) * (1 + x + x\<^sup>2) <= 1" . ``` wenzelm@53015 ` 1744` ``` moreover have c: "0 < 1 + x + x\<^sup>2" ``` hoelzl@50326 ` 1745` ``` by (simp add: add_pos_nonneg a) ``` wenzelm@53076 ` 1746` ``` ultimately have "1 - x <= 1 / (1 + x + x\<^sup>2)" ``` hoelzl@50326 ` 1747` ``` by (elim mult_imp_le_div_pos) ``` hoelzl@50326 ` 1748` ``` also have "... <= 1 / exp x" ``` lp15@59669 ` 1749` ``` by (metis a abs_one b exp_bound exp_gt_zero frac_le less_eq_real_def real_sqrt_abs ``` paulson@54576 ` 1750` ``` real_sqrt_pow2_iff real_sqrt_power) ``` hoelzl@50326 ` 1751` ``` also have "... = exp (-x)" ``` hoelzl@50326 ` 1752` ``` by (auto simp add: exp_minus divide_inverse) ``` hoelzl@50326 ` 1753` ``` finally have "1 - x <= exp (- x)" . ``` hoelzl@50326 ` 1754` ``` also have "1 - x = exp (ln (1 - x))" ``` paulson@54576 ` 1755` ``` by (metis b diff_0 exp_ln_iff less_iff_diff_less_0 minus_diff_eq) ``` hoelzl@50326 ` 1756` ``` finally have "exp (ln (1 - x)) <= exp (- x)" . ``` hoelzl@50326 ` 1757` ``` thus ?thesis by (auto simp only: exp_le_cancel_iff) ``` hoelzl@50326 ` 1758` ```qed ``` hoelzl@50326 ` 1759` hoelzl@50326 ` 1760` ```lemma exp_ge_add_one_self [simp]: "1 + (x::real) <= exp x" ``` hoelzl@50326 ` 1761` ``` apply (case_tac "0 <= x") ``` hoelzl@50326 ` 1762` ``` apply (erule exp_ge_add_one_self_aux) ``` hoelzl@50326 ` 1763` ``` apply (case_tac "x <= -1") ``` hoelzl@50326 ` 1764` ``` apply (subgoal_tac "1 + x <= 0") ``` hoelzl@50326 ` 1765` ``` apply (erule order_trans) ``` hoelzl@50326 ` 1766` ``` apply simp ``` hoelzl@50326 ` 1767` ``` apply simp ``` hoelzl@50326 ` 1768` ``` apply (subgoal_tac "1 + x = exp(ln (1 + x))") ``` hoelzl@50326 ` 1769` ``` apply (erule ssubst) ``` hoelzl@50326 ` 1770` ``` apply (subst exp_le_cancel_iff) ``` hoelzl@50326 ` 1771` ``` apply (subgoal_tac "ln (1 - (- x)) <= - (- x)") ``` hoelzl@50326 ` 1772` ``` apply simp ``` hoelzl@50326 ` 1773` ``` apply (rule ln_one_minus_pos_upper_bound) ``` hoelzl@50326 ` 1774` ``` apply auto ``` hoelzl@50326 ` 1775` ```done ``` hoelzl@50326 ` 1776` lp15@60017 ` 1777` ```lemma ln_one_plus_pos_lower_bound: ``` lp15@60017 ` 1778` ``` fixes x::real shows "0 <= x \ x <= 1 \ x - x\<^sup>2 <= ln (1 + x)" ``` hoelzl@51527 ` 1779` ```proof - ``` hoelzl@51527 ` 1780` ``` assume a: "0 <= x" and b: "x <= 1" ``` wenzelm@53076 ` 1781` ``` have "exp (x - x\<^sup>2) = exp x / exp (x\<^sup>2)" ``` hoelzl@51527 ` 1782` ``` by (rule exp_diff) ``` wenzelm@53076 ` 1783` ``` also have "... <= (1 + x + x\<^sup>2) / exp (x \<^sup>2)" ``` paulson@54576 ` 1784` ``` by (metis a b divide_right_mono exp_bound exp_ge_zero) ``` wenzelm@53076 ` 1785` ``` also have "... <= (1 + x + x\<^sup>2) / (1 + x\<^sup>2)" ``` nipkow@56544 ` 1786` ``` by (simp add: a divide_left_mono add_pos_nonneg) ``` hoelzl@51527 ` 1787` ``` also from a have "... <= 1 + x" ``` hoelzl@51527 ` 1788` ``` by (simp add: field_simps add_strict_increasing zero_le_mult_iff) ``` wenzelm@53076 ` 1789` ``` finally have "exp (x - x\<^sup>2) <= 1 + x" . ``` hoelzl@51527 ` 1790` ``` also have "... = exp (ln (1 + x))" ``` hoelzl@51527 ` 1791` ``` proof - ``` hoelzl@51527 ` 1792` ``` from a have "0 < 1 + x" by auto ``` hoelzl@51527 ` 1793` ``` thus ?thesis ``` hoelzl@51527 ` 1794` ``` by (auto simp only: exp_ln_iff [THEN sym]) ``` hoelzl@51527 ` 1795` ``` qed ``` wenzelm@53076 ` 1796` ``` finally have "exp (x - x\<^sup>2) <= exp (ln (1 + x))" . ``` paulson@54576 ` 1797` ``` thus ?thesis ``` lp15@59669 ` 1798` ``` by (metis exp_le_cancel_iff) ``` hoelzl@51527 ` 1799` ```qed ``` hoelzl@51527 ` 1800` wenzelm@53079 ` 1801` ```lemma ln_one_minus_pos_lower_bound: ``` lp15@60017 ` 1802` ``` fixes x::real ``` lp15@60017 ` 1803` ``` shows "0 <= x \ x <= (1 / 2) \ - x - 2 * x\<^sup>2 <= ln (1 - x)" ``` hoelzl@51527 ` 1804` ```proof - ``` hoelzl@51527 ` 1805` ``` assume a: "0 <= x" and b: "x <= (1 / 2)" ``` wenzelm@53079 ` 1806` ``` from b have c: "x < 1" by auto ``` hoelzl@51527 ` 1807` ``` then have "ln (1 - x) = - ln (1 + x / (1 - x))" ``` paulson@54576 ` 1808` ``` apply (subst ln_inverse [symmetric]) ``` paulson@54576 ` 1809` ``` apply (simp add: field_simps) ``` paulson@54576 ` 1810` ``` apply (rule arg_cong [where f=ln]) ``` paulson@54576 ` 1811` ``` apply (simp add: field_simps) ``` paulson@54576 ` 1812` ``` done ``` hoelzl@51527 ` 1813` ``` also have "- (x / (1 - x)) <= ..." ``` wenzelm@53079 ` 1814` ``` proof - ``` hoelzl@51527 ` 1815` ``` have "ln (1 + x / (1 - x)) <= x / (1 - x)" ``` hoelzl@56571 ` 1816` ``` using a c by (intro ln_add_one_self_le_self) auto ``` hoelzl@51527 ` 1817` ``` thus ?thesis ``` hoelzl@51527 ` 1818` ``` by auto ``` hoelzl@51527 ` 1819` ``` qed ``` hoelzl@51527 ` 1820` ``` also have "- (x / (1 - x)) = -x / (1 - x)" ``` hoelzl@51527 ` 1821` ``` by auto ``` hoelzl@51527 ` 1822` ``` finally have d: "- x / (1 - x) <= ln (1 - x)" . ``` hoelzl@51527 ` 1823` ``` have "0 < 1 - x" using a b by simp ``` wenzelm@53076 ` 1824` ``` hence e: "-x - 2 * x\<^sup>2 <= - x / (1 - x)" ``` hoelzl@51527 ` 1825` ``` using mult_right_le_one_le[of "x*x" "2*x"] a b ``` wenzelm@53079 ` 1826` ``` by (simp add: field_simps power2_eq_square) ``` wenzelm@53076 ` 1827` ``` from e d show "- x - 2 * x\<^sup>2 <= ln (1 - x)" ``` hoelzl@51527 ` 1828` ``` by (rule order_trans) ``` hoelzl@51527 ` 1829` ```qed ``` hoelzl@51527 ` 1830` lp15@60017 ` 1831` ```lemma ln_add_one_self_le_self2: ``` lp15@60017 ` 1832` ``` fixes x::real shows "-1 < x \ ln(1 + x) <= x" ``` hoelzl@51527 ` 1833` ``` apply (subgoal_tac "ln (1 + x) \ ln (exp x)", simp) ``` hoelzl@51527 ` 1834` ``` apply (subst ln_le_cancel_iff) ``` hoelzl@51527 ` 1835` ``` apply auto ``` wenzelm@53079 ` 1836` ``` done ``` hoelzl@51527 ` 1837` hoelzl@51527 ` 1838` ```lemma abs_ln_one_plus_x_minus_x_bound_nonneg: ``` lp15@60017 ` 1839` ``` fixes x::real shows "0 <= x \ x <= 1 \ abs(ln (1 + x) - x) <= x\<^sup>2" ``` hoelzl@51527 ` 1840` ```proof - ``` hoelzl@51527 ` 1841` ``` assume x: "0 <= x" ``` hoelzl@51527 ` 1842` ``` assume x1: "x <= 1" ``` hoelzl@51527 ` 1843` ``` from x have "ln (1 + x) <= x" ``` hoelzl@51527 ` 1844` ``` by (rule ln_add_one_self_le_self) ``` wenzelm@53079 ` 1845` ``` then have "ln (1 + x) - x <= 0" ``` hoelzl@51527 ` 1846` ``` by simp ``` hoelzl@51527 ` 1847` ``` then have "abs(ln(1 + x) - x) = - (ln(1 + x) - x)" ``` hoelzl@51527 ` 1848` ``` by (rule abs_of_nonpos) ``` wenzelm@53079 ` 1849` ``` also have "... = x - ln (1 + x)" ``` hoelzl@51527 ` 1850` ``` by simp ``` wenzelm@53076 ` 1851` ``` also have "... <= x\<^sup>2" ``` hoelzl@51527 ` 1852` ``` proof - ``` wenzelm@53076 ` 1853` ``` from x x1 have "x - x\<^sup>2 <= ln (1 + x)" ``` hoelzl@51527 ` 1854` ``` by (intro ln_one_plus_pos_lower_bound) ``` hoelzl@51527 ` 1855` ``` thus ?thesis ``` hoelzl@51527 ` 1856` ``` by simp ``` hoelzl@51527 ` 1857` ``` qed ``` hoelzl@51527 ` 1858` ``` finally show ?thesis . ``` hoelzl@51527 ` 1859` ```qed ``` hoelzl@51527 ` 1860` hoelzl@51527 ` 1861` ```lemma abs_ln_one_plus_x_minus_x_bound_nonpos: ``` lp15@60017 ` 1862` ``` fixes x::real shows "-(1 / 2) <= x \ x <= 0 \ abs(ln (1 + x) - x) <= 2 * x\<^sup>2" ``` hoelzl@51527 ` 1863` ```proof - ``` hoelzl@51527 ` 1864` ``` assume a: "-(1 / 2) <= x" ``` hoelzl@51527 ` 1865` ``` assume b: "x <= 0" ``` wenzelm@53079 ` 1866` ``` have "abs(ln (1 + x) - x) = x - ln(1 - (-x))" ``` hoelzl@51527 ` 1867` ``` apply (subst abs_of_nonpos) ``` hoelzl@51527 ` 1868` ``` apply simp ``` hoelzl@51527 ` 1869` ``` apply (rule ln_add_one_self_le_self2) ``` hoelzl@51527 ` 1870` ``` using a apply auto ``` hoelzl@51527 ` 1871` ``` done ``` wenzelm@53076 ` 1872` ``` also have "... <= 2 * x\<^sup>2" ``` wenzelm@53076 ` 1873` ``` apply (subgoal_tac "- (-x) - 2 * (-x)\<^sup>2 <= ln (1 - (-x))") ``` hoelzl@51527 ` 1874` ``` apply (simp add: algebra_simps) ``` hoelzl@51527 ` 1875` ``` apply (rule ln_one_minus_pos_lower_bound) ``` hoelzl@51527 ` 1876` ``` using a b apply auto ``` hoelzl@51527 ` 1877` ``` done ``` hoelzl@51527 ` 1878` ``` finally show ?thesis . ``` hoelzl@51527 ` 1879` ```qed ``` hoelzl@51527 ` 1880` hoelzl@51527 ` 1881` ```lemma abs_ln_one_plus_x_minus_x_bound: ``` lp15@60017 ` 1882` ``` fixes x::real shows "abs x <= 1 / 2 \ abs(ln (1 + x) - x) <= 2 * x\<^sup>2" ``` hoelzl@51527 ` 1883` ``` apply (case_tac "0 <= x") ``` hoelzl@51527 ` 1884` ``` apply (rule order_trans) ``` hoelzl@51527 ` 1885` ``` apply (rule abs_ln_one_plus_x_minus_x_bound_nonneg) ``` hoelzl@51527 ` 1886` ``` apply auto ``` hoelzl@51527 ` 1887` ``` apply (rule abs_ln_one_plus_x_minus_x_bound_nonpos) ``` hoelzl@51527 ` 1888` ``` apply auto ``` wenzelm@53079 ` 1889` ``` done ``` wenzelm@53079 ` 1890` lp15@60017 ` 1891` ```lemma ln_x_over_x_mono: ``` lp15@60017 ` 1892` ``` fixes x::real shows "exp 1 <= x \ x <= y \ (ln y / y) <= (ln x / x)" ``` hoelzl@51527 ` 1893` ```proof - ``` hoelzl@51527 ` 1894` ``` assume x: "exp 1 <= x" "x <= y" ``` hoelzl@51527 ` 1895` ``` moreover have "0 < exp (1::real)" by simp ``` hoelzl@51527 ` 1896` ``` ultimately have a: "0 < x" and b: "0 < y" ``` hoelzl@51527 ` 1897` ``` by (fast intro: less_le_trans order_trans)+ ``` hoelzl@51527 ` 1898` ``` have "x * ln y - x * ln x = x * (ln y - ln x)" ``` hoelzl@51527 ` 1899` ``` by (simp add: algebra_simps) ``` hoelzl@51527 ` 1900` ``` also have "... = x * ln(y / x)" ``` hoelzl@51527 ` 1901` ``` by (simp only: ln_div a b) ``` hoelzl@51527 ` 1902` ``` also have "y / x = (x + (y - x)) / x" ``` hoelzl@51527 ` 1903` ``` by simp ``` hoelzl@51527 ` 1904` ``` also have "... = 1 + (y - x) / x" ``` hoelzl@51527 ` 1905` ``` using x a by (simp add: field_simps) ``` hoelzl@51527 ` 1906` ``` also have "x * ln(1 + (y - x) / x) <= x * ((y - x) / x)" ``` lp15@59669 ` 1907` ``` using x a ``` hoelzl@56571 ` 1908` ``` by (intro mult_left_mono ln_add_one_self_le_self) simp_all ``` hoelzl@51527 ` 1909` ``` also have "... = y - x" using a by simp ``` hoelzl@51527 ` 1910` ``` also have "... = (y - x) * ln (exp 1)" by simp ``` hoelzl@51527 ` 1911` ``` also have "... <= (y - x) * ln x" ``` hoelzl@51527 ` 1912` ``` apply (rule mult_left_mono) ``` hoelzl@51527 ` 1913` ``` apply (subst ln_le_cancel_iff) ``` hoelzl@51527 ` 1914` ``` apply fact ``` hoelzl@51527 ` 1915` ``` apply (rule a) ``` hoelzl@51527 ` 1916` ``` apply (rule x) ``` hoelzl@51527 ` 1917` ``` using x apply simp ``` hoelzl@51527 ` 1918` ``` done ``` hoelzl@51527 ` 1919` ``` also have "... = y * ln x - x * ln x" ``` hoelzl@51527 ` 1920` ``` by (rule left_diff_distrib) ``` hoelzl@51527 ` 1921` ``` finally have "x * ln y <= y * ln x" ``` hoelzl@51527 ` 1922` ``` by arith ``` hoelzl@51527 ` 1923` ``` then have "ln y <= (y * ln x) / x" using a by (simp add: field_simps) ``` hoelzl@51527 ` 1924` ``` also have "... = y * (ln x / x)" by simp ``` hoelzl@51527 ` 1925` ``` finally show ?thesis using b by (simp add: field_simps) ``` hoelzl@51527 ` 1926` ```qed ``` hoelzl@51527 ` 1927` lp15@60017 ` 1928` ```lemma ln_le_minus_one: ``` lp15@60017 ` 1929` ``` fixes x::real shows "0 < x \ ln x \ x - 1" ``` hoelzl@51527 ` 1930` ``` using exp_ge_add_one_self[of "ln x"] by simp ``` hoelzl@51527 ` 1931` lp15@60141 ` 1932` ```corollary ln_diff_le: ``` lp15@60141 ` 1933` ``` fixes x::real ``` lp15@60141 ` 1934` ``` shows "0 < x \ 0 < y \ ln x - ln y \ (x - y) / y" ``` lp15@60141 ` 1935` ``` by (simp add: ln_div [symmetric] diff_divide_distrib ln_le_minus_one) ``` lp15@60141 ` 1936` hoelzl@51527 ` 1937` ```lemma ln_eq_minus_one: ``` lp15@60017 ` 1938` ``` fixes x::real ``` wenzelm@53079 ` 1939` ``` assumes "0 < x" "ln x = x - 1" ``` wenzelm@53079 ` 1940` ``` shows "x = 1" ``` hoelzl@51527 ` 1941` ```proof - ``` wenzelm@53079 ` 1942` ``` let ?l = "\y. ln y - y + 1" ``` lp15@60017 ` 1943` ``` have D: "\x::real. 0 < x \ DERIV ?l x :> (1 / x - 1)" ``` hoelzl@56381 ` 1944` ``` by (auto intro!: derivative_eq_intros) ``` hoelzl@51527 ` 1945` hoelzl@51527 ` 1946` ``` show ?thesis ``` hoelzl@51527 ` 1947` ``` proof (cases rule: linorder_cases) ``` hoelzl@51527 ` 1948` ``` assume "x < 1" ``` hoelzl@51527 ` 1949` ``` from dense[OF `x < 1`] obtain a where "x < a" "a < 1" by blast ``` hoelzl@51527 ` 1950` ``` from `x < a` have "?l x < ?l a" ``` hoelzl@51527 ` 1951` ``` proof (rule DERIV_pos_imp_increasing, safe) ``` wenzelm@53079 ` 1952` ``` fix y ``` wenzelm@53079 ` 1953` ``` assume "x \ y" "y \ a" ``` hoelzl@51527 ` 1954` ``` with `0 < x` `a < 1` have "0 < 1 / y - 1" "0 < y" ``` hoelzl@51527 ` 1955` ``` by (auto simp: field_simps) ``` hoelzl@51527 ` 1956` ``` with D show "\z. DERIV ?l y :> z \ 0 < z" ``` hoelzl@51527 ` 1957` ``` by auto ``` hoelzl@51527 ` 1958` ``` qed ``` hoelzl@51527 ` 1959` ``` also have "\ \ 0" ``` hoelzl@51527 ` 1960` ``` using ln_le_minus_one `0 < x` `x < a` by (auto simp: field_simps) ``` hoelzl@51527 ` 1961` ``` finally show "x = 1" using assms by auto ``` hoelzl@51527 ` 1962` ``` next ``` hoelzl@51527 ` 1963` ``` assume "1 < x" ``` wenzelm@53079 ` 1964` ``` from dense[OF this] obtain a where "1 < a" "a < x" by blast ``` hoelzl@51527 ` 1965` ``` from `a < x` have "?l x < ?l a" ``` hoelzl@51527 ` 1966` ``` proof (rule DERIV_neg_imp_decreasing, safe) ``` wenzelm@53079 ` 1967` ``` fix y ``` wenzelm@53079 ` 1968` ``` assume "a \ y" "y \ x" ``` hoelzl@51527 ` 1969` ``` with `1 < a` have "1 / y - 1 < 0" "0 < y" ``` hoelzl@51527 ` 1970` ``` by (auto simp: field_simps) ``` hoelzl@51527 ` 1971` ``` with D show "\z. DERIV ?l y :> z \ z < 0" ``` hoelzl@51527 ` 1972` ``` by blast ``` hoelzl@51527 ` 1973` ``` qed ``` hoelzl@51527 ` 1974` ``` also have "\ \ 0" ``` hoelzl@51527 ` 1975` ``` using ln_le_minus_one `1 < a` by (auto simp: field_simps) ``` hoelzl@51527 ` 1976` ``` finally show "x = 1" using assms by auto ``` wenzelm@53079 ` 1977` ``` next ``` wenzelm@53079 ` 1978` ``` assume "x = 1" ``` wenzelm@53079 ` 1979` ``` then show ?thesis by simp ``` wenzelm@53079 ` 1980` ``` qed ``` hoelzl@51527 ` 1981` ```qed ``` hoelzl@51527 ` 1982` hoelzl@50326 ` 1983` ```lemma exp_at_bot: "(exp ---> (0::real)) at_bot" ``` hoelzl@50326 ` 1984` ``` unfolding tendsto_Zfun_iff ``` hoelzl@50326 ` 1985` ```proof (rule ZfunI, simp add: eventually_at_bot_dense) ``` hoelzl@50326 ` 1986` ``` fix r :: real assume "0 < r" ``` wenzelm@53079 ` 1987` ``` { ``` wenzelm@53079 ` 1988` ``` fix x ``` wenzelm@53079 ` 1989` ``` assume "x < ln r" ``` hoelzl@50326 ` 1990` ``` then have "exp x < exp (ln r)" ``` hoelzl@50326 ` 1991` ``` by simp ``` hoelzl@50326 ` 1992` ``` with `0 < r` have "exp x < r" ``` wenzelm@53079 ` 1993` ``` by simp ``` wenzelm@53079 ` 1994` ``` } ``` hoelzl@50326 ` 1995` ``` then show "\k. \n at_top" ``` hoelzl@50346 ` 1999` ``` by (rule filterlim_at_top_at_top[where Q="\x. True" and P="\x. 0 < x" and g="ln"]) ``` hoelzl@50346 ` 2000` ``` (auto intro: eventually_gt_at_top) ``` hoelzl@50326 ` 2001` lp15@59613 ` 2002` ```lemma lim_exp_minus_1: ``` lp15@59613 ` 2003` ``` fixes x :: "'a::{real_normed_field,banach}" ``` lp15@59613 ` 2004` ``` shows "((\z::'a. (exp(z) - 1) / z) ---> 1) (at 0)" ``` lp15@59613 ` 2005` ```proof - ``` lp15@59613 ` 2006` ``` have "((\z::'a. exp(z) - 1) has_field_derivative 1) (at 0)" ``` lp15@59613 ` 2007` ``` by (intro derivative_eq_intros | simp)+ ``` lp15@59613 ` 2008` ``` then show ?thesis ``` lp15@59613 ` 2009` ``` by (simp add: Deriv.DERIV_iff2) ``` lp15@59613 ` 2010` ```qed ``` lp15@59613 ` 2011` lp15@60017 ` 2012` ```lemma ln_at_0: "LIM x at_right 0. ln (x::real) :> at_bot" ``` hoelzl@50346 ` 2013` ``` by (rule filterlim_at_bot_at_right[where Q="\x. 0 < x" and P="\x. True" and g="exp"]) ``` hoelzl@51641 ` 2014` ``` (auto simp: eventually_at_filter) ``` hoelzl@50326 ` 2015` lp15@60017 ` 2016` ```lemma ln_at_top: "LIM x at_top. ln (x::real) :> at_top" ``` hoelzl@50346 ` 2017` ``` by (rule filterlim_at_top_at_top[where Q="\x. 0 < x" and P="\x. True" and g="exp"]) ``` hoelzl@50346 ` 2018` ``` (auto intro: eventually_gt_at_top) ``` hoelzl@50326 ` 2019` hoelzl@50347 ` 2020` ```lemma tendsto_power_div_exp_0: "((\x. x ^ k / exp x) ---> (0::real)) at_top" ``` hoelzl@50347 ` 2021` ```proof (induct k) ``` wenzelm@53079 ` 2022` ``` case 0 ``` hoelzl@50347 ` 2023` ``` show "((\x. x ^ 0 / exp x) ---> (0::real)) at_top" ``` hoelzl@50347 ` 2024` ``` by (simp add: inverse_eq_divide[symmetric]) ``` hoelzl@50347 ` 2025` ``` (metis filterlim_compose[OF tendsto_inverse_0] exp_at_top filterlim_mono ``` hoelzl@50347 ` 2026` ``` at_top_le_at_infinity order_refl) ``` hoelzl@50347 ` 2027` ```next ``` hoelzl@50347 ` 2028` ``` case (Suc k) ``` hoelzl@50347 ` 2029` ``` show ?case ``` hoelzl@50347 ` 2030` ``` proof (rule lhospital_at_top_at_top) ``` hoelzl@50347 ` 2031` ``` show "eventually (\x. DERIV (\x. x ^ Suc k) x :> (real (Suc k) * x^k)) at_top" ``` hoelzl@56381 ` 2032` ``` by eventually_elim (intro derivative_eq_intros, auto) ``` hoelzl@50347 ` 2033` ``` show "eventually (\x. DERIV exp x :> exp x) at_top" ``` hoelzl@56381 ` 2034` ``` by eventually_elim auto ``` hoelzl@50347 ` 2035` ``` show "eventually (\x. exp x \ 0) at_top" ``` hoelzl@50347 ` 2036` ``` by auto ``` hoelzl@50347 ` 2037` ``` from tendsto_mult[OF tendsto_const Suc, of "real (Suc k)"] ``` hoelzl@50347 ` 2038` ``` show "((\x. real (Suc k) * x ^ k / exp x) ---> 0) at_top" ``` hoelzl@50347 ` 2039` ``` by simp ``` hoelzl@50347 ` 2040` ``` qed (rule exp_at_top) ``` hoelzl@50347 ` 2041` ```qed ``` hoelzl@50347 ` 2042` hoelzl@51527 ` 2043` wenzelm@53079 ` 2044` ```definition log :: "[real,real] => real" ``` wenzelm@53079 ` 2045` ``` -- {*logarithm of @{term x} to base @{term a}*} ``` wenzelm@53079 ` 2046` ``` where "log a x = ln x / ln a" ``` hoelzl@51527 ` 2047` hoelzl@51527 ` 2048` hoelzl@51527 ` 2049` ```lemma tendsto_log [tendsto_intros]: ``` hoelzl@51527 ` 2050` ``` "\(f ---> a) F; (g ---> b) F; 0 < a; a \ 1; 0 < b\ \ ((\x. log (f x) (g x)) ---> log a b) F" ``` hoelzl@51527 ` 2051` ``` unfolding log_def by (intro tendsto_intros) auto ``` hoelzl@51527 ` 2052` hoelzl@51527 ` 2053` ```lemma continuous_log: ``` wenzelm@53079 ` 2054` ``` assumes "continuous F f" ``` wenzelm@53079 ` 2055` ``` and "continuous F g" ``` wenzelm@53079 ` 2056` ``` and "0 < f (Lim F (\x. x))" ``` wenzelm@53079 ` 2057` ``` and "f (Lim F (\x. x)) \ 1" ``` wenzelm@53079 ` 2058` ``` and "0 < g (Lim F (\x. x))" ``` hoelzl@51527 ` 2059` ``` shows "continuous F (\x. log (f x) (g x))" ``` hoelzl@51527 ` 2060` ``` using assms unfolding continuous_def by (rule tendsto_log) ``` hoelzl@51527 ` 2061` hoelzl@51527 ` 2062` ```lemma continuous_at_within_log[continuous_intros]: ``` wenzelm@53079 ` 2063` ``` assumes "continuous (at a within s) f" ``` wenzelm@53079 ` 2064` ``` and "continuous (at a within s) g" ``` wenzelm@53079 ` 2065` ``` and "0 < f a" ``` wenzelm@53079 ` 2066` ``` and "f a \ 1" ``` wenzelm@53079 ` 2067` ``` and "0 < g a" ``` hoelzl@51527 ` 2068` ``` shows "continuous (at a within s) (\x. log (f x) (g x))" ``` hoelzl@51527 ` 2069` ``` using assms unfolding continuous_within by (rule tendsto_log) ``` hoelzl@51527 ` 2070` hoelzl@51527 ` 2071` ```lemma isCont_log[continuous_intros, simp]: ``` hoelzl@51527 ` 2072` ``` assumes "isCont f a" "isCont g a" "0 < f a" "f a \ 1" "0 < g a" ``` hoelzl@51527 ` 2073` ``` shows "isCont (\x. log (f x) (g x)) a" ``` hoelzl@51527 ` 2074` ``` using assms unfolding continuous_at by (rule tendsto_log) ``` hoelzl@51527 ` 2075` hoelzl@56371 ` 2076` ```lemma continuous_on_log[continuous_intros]: ``` wenzelm@53079 ` 2077` ``` assumes "continuous_on s f" "continuous_on s g" ``` wenzelm@53079 ` 2078` ``` and "\x\s. 0 < f x" "\x\s. f x \ 1" "\x\s. 0 < g x" ``` hoelzl@51527 ` 2079` ``` shows "continuous_on s (\x. log (f x) (g x))" ``` hoelzl@51527 ` 2080` ``` using assms unfolding continuous_on_def by (fast intro: tendsto_log) ``` hoelzl@51527 ` 2081` hoelzl@51527 ` 2082` ```lemma powr_one_eq_one [simp]: "1 powr a = 1" ``` wenzelm@53079 ` 2083` ``` by (simp add: powr_def) ``` hoelzl@51527 ` 2084` lp15@60017 ` 2085` ```lemma powr_zero_eq_one [simp]: "x powr 0 = (if x=0 then 0 else 1)" ``` wenzelm@53079 ` 2086` ``` by (simp add: powr_def) ``` hoelzl@51527 ` 2087` lp15@60017 ` 2088` ```lemma powr_one_gt_zero_iff [simp]: ``` lp15@60017 ` 2089` ``` fixes x::real shows "(x powr 1 = x) = (0 \ x)" ``` lp15@60017 ` 2090` ``` by (auto simp: powr_def) ``` hoelzl@51527 ` 2091` ```declare powr_one_gt_zero_iff [THEN iffD2, simp] ``` hoelzl@51527 ` 2092` lp15@60017 ` 2093` ```lemma powr_mult: ``` lp15@60017 ` 2094` ``` fixes x::real shows "0 \ x \ 0 \ y \ (x * y) powr a = (x powr a) * (y powr a)" ``` wenzelm@53079 ` 2095` ``` by (simp add: powr_def exp_add [symmetric] ln_mult distrib_left) ``` hoelzl@51527 ` 2096` lp15@60017 ` 2097` ```lemma powr_ge_pzero [simp]: ``` lp15@60017 ` 2098` ``` fixes x::real shows "0 <= x powr y" ``` wenzelm@53079 ` 2099` ``` by (simp add: powr_def) ``` hoelzl@51527 ` 2100` lp15@60017 ` 2101` ```lemma powr_divide: ``` lp15@60017 ` 2102` ``` fixes x::real shows "0 < x \ 0 < y \ (x / y) powr a = (x powr a) / (y powr a)" ``` wenzelm@53079 ` 2103` ``` apply (simp add: divide_inverse positive_imp_inverse_positive powr_mult) ``` wenzelm@53079 ` 2104` ``` apply (simp add: powr_def exp_minus [symmetric] exp_add [symmetric] ln_inverse) ``` wenzelm@53079 ` 2105` ``` done ``` hoelzl@51527 ` 2106` lp15@60017 ` 2107` ```lemma powr_divide2: ``` lp15@60017 ` 2108` ``` fixes x::real shows "x powr a / x powr b = x powr (a - b)" ``` hoelzl@51527 ` 2109` ``` apply (simp add: powr_def) ``` hoelzl@51527 ` 2110` ``` apply (subst exp_diff [THEN sym]) ``` hoelzl@51527 ` 2111` ``` apply (simp add: left_diff_distrib) ``` wenzelm@53079 ` 2112` ``` done ``` hoelzl@51527 ` 2113` lp15@60017 ` 2114` ```lemma powr_add: ``` lp15@60017 ` 2115` ``` fixes x::real shows "x powr (a + b) = (x powr a) * (x powr b)" ``` wenzelm@53079 ` 2116` ``` by (simp add: powr_def exp_add [symmetric] distrib_right) ``` wenzelm@53079 ` 2117` lp15@60017 ` 2118` ```lemma powr_mult_base: ``` lp15@60017 ` 2119` ``` fixes x::real shows "0 < x \x * x powr y = x powr (1 + y)" ``` wenzelm@53079 ` 2120` ``` using assms by (auto simp: powr_add) ``` hoelzl@51527 ` 2121` lp15@60017 ` 2122` ```lemma powr_powr: ``` lp15@60017 ` 2123` ``` fixes x::real shows "(x powr a) powr b = x powr (a * b)" ``` wenzelm@53079 ` 2124` ``` by (simp add: powr_def) ``` hoelzl@51527 ` 2125` lp15@60017 ` 2126` ```lemma powr_powr_swap: ``` lp15@60017 ` 2127` ``` fixes x::real shows "(x powr a) powr b = (x powr b) powr a" ``` haftmann@57512 ` 2128` ``` by (simp add: powr_powr mult.commute) ``` hoelzl@51527 ` 2129` lp15@60017 ` 2130` ```lemma powr_minus: ``` lp15@60017 ` 2131` ``` fixes x::real shows "x powr (-a) = inverse (x powr a)" ``` wenzelm@53079 ` 2132` ``` by (simp add: powr_def exp_minus [symmetric]) ``` hoelzl@51527 ` 2133` lp15@60017 ` 2134` ```lemma powr_minus_divide: ``` lp15@60017 ` 2135` ``` fixes x::real shows "x powr (-a) = 1/(x powr a)" ``` wenzelm@53079 ` 2136` ``` by (simp add: divide_inverse powr_minus) ``` wenzelm@53079 ` 2137` lp15@60017 ` 2138` ```lemma divide_powr_uminus: ``` lp15@60017 ` 2139` ``` fixes a::real shows "a / b powr c = a * b powr (- c)" ``` immler@58984 ` 2140` ``` by (simp add: powr_minus_divide) ``` immler@58984 ` 2141` lp15@60017 ` 2142` ```lemma powr_less_mono: ``` lp15@60017 ` 2143` ``` fixes x::real shows "a < b \ 1 < x \ x powr a < x powr b" ``` wenzelm@53079 ` 2144` ``` by (simp add: powr_def) ``` wenzelm@53079 ` 2145` lp15@60017 ` 2146` ```lemma powr_less_cancel: ``` lp15@60017 ` 2147` ``` fixes x::real shows "x powr a < x powr b \ 1 < x \ a < b" ``` wenzelm@53079 ` 2148` ``` by (simp add: powr_def) ``` wenzelm@53079 ` 2149` lp15@60017 ` 2150` ```lemma powr_less_cancel_iff [simp]: ``` lp15@60017 ` 2151` ``` fixes x::real shows "1 < x \ (x powr a < x powr b) = (a < b)" ``` wenzelm@53079 ` 2152` ``` by (blast intro: powr_less_cancel powr_less_mono) ``` wenzelm@53079 ` 2153` lp15@60017 ` 2154` ```lemma powr_le_cancel_iff [simp]: ``` lp15@60017 ` 2155` ``` fixes x::real shows "1 < x \ (x powr a \ x powr b) = (a \ b)" ``` wenzelm@53079 ` 2156` ``` by (simp add: linorder_not_less [symmetric]) ``` hoelzl@51527 ` 2157` hoelzl@51527 ` 2158` ```lemma log_ln: "ln x = log (exp(1)) x" ``` wenzelm@53079 ` 2159` ``` by (simp add: log_def) ``` wenzelm@53079 ` 2160` wenzelm@53079 ` 2161` ```lemma DERIV_log: ``` wenzelm@53079 ` 2162` ``` assumes "x > 0" ``` wenzelm@53079 ` 2163` ``` shows "DERIV (\y. log b y) x :> 1 / (ln b * x)" ``` hoelzl@51527 ` 2164` ```proof - ``` hoelzl@51527 ` 2165` ``` def lb \ "1 / ln b" ``` hoelzl@51527 ` 2166` ``` moreover have "DERIV (\y. lb * ln y) x :> lb / x" ``` hoelzl@56381 ` 2167` ``` using `x > 0` by (auto intro!: derivative_eq_intros) ``` hoelzl@51527 ` 2168` ``` ultimately show ?thesis ``` hoelzl@51527 ` 2169` ``` by (simp add: log_def) ``` hoelzl@51527 ` 2170` ```qed ``` hoelzl@51527 ` 2171` hoelzl@56381 ` 2172` ```lemmas DERIV_log[THEN DERIV_chain2, derivative_intros] ``` hoelzl@51527 ` 2173` wenzelm@53079 ` 2174` ```lemma powr_log_cancel [simp]: "0 < a \ a \ 1 \ 0 < x \ a powr (log a x) = x" ``` wenzelm@53079 ` 2175` ``` by (simp add: powr_def log_def) ``` wenzelm@53079 ` 2176` wenzelm@53079 ` 2177` ```lemma log_powr_cancel [simp]: "0 < a \ a \ 1 \ log a (a powr y) = y" ``` wenzelm@53079 ` 2178` ``` by (simp add: log_def powr_def) ``` wenzelm@53079 ` 2179` wenzelm@53079 ` 2180` ```lemma log_mult: ``` wenzelm@53079 ` 2181` ``` "0 < a \ a \ 1 \ 0 < x \ 0 < y \ ``` wenzelm@53079 ` 2182` ``` log a (x * y) = log a x + log a y" ``` wenzelm@53079 ` 2183` ``` by (simp add: log_def ln_mult divide_inverse distrib_right) ``` wenzelm@53079 ` 2184` wenzelm@53079 ` 2185` ```lemma log_eq_div_ln_mult_log: ``` wenzelm@53079 ` 2186` ``` "0 < a \ a \ 1 \ 0 < b \ b \ 1 \ 0 < x \ ``` wenzelm@53079 ` 2187` ``` log a x = (ln b/ln a) * log b x" ``` wenzelm@53079 ` 2188` ``` by (simp add: log_def divide_inverse) ``` hoelzl@51527 ` 2189` hoelzl@51527 ` 2190` ```text{*Base 10 logarithms*} ``` wenzelm@53079 ` 2191` ```lemma log_base_10_eq1: "0 < x \ log 10 x = (ln (exp 1) / ln 10) * ln x" ``` wenzelm@53079 ` 2192` ``` by (simp add: log_def) ``` wenzelm@53079 ` 2193` wenzelm@53079 ` 2194` ```lemma log_base_10_eq2: "0 < x \ log 10 x = (log 10 (exp 1)) * ln x" ``` wenzelm@53079 ` 2195` ``` by (simp add: log_def) ``` hoelzl@51527 ` 2196` hoelzl@51527 ` 2197` ```lemma log_one [simp]: "log a 1 = 0" ``` wenzelm@53079 ` 2198` ``` by (simp add: log_def) ``` hoelzl@51527 ` 2199` hoelzl@51527 ` 2200` ```lemma log_eq_one [simp]: "[| 0 < a; a \ 1 |] ==> log a a = 1" ``` wenzelm@53079 ` 2201` ``` by (simp add: log_def) ``` wenzelm@53079 ` 2202` wenzelm@53079 ` 2203` ```lemma log_inverse: "0 < a \ a \ 1 \ 0 < x \ log a (inverse x) = - log a x" ``` wenzelm@53079 ` 2204` ``` apply (rule_tac a1 = "log a x" in add_left_cancel [THEN iffD1]) ``` wenzelm@53079 ` 2205` ``` apply (simp add: log_mult [symmetric]) ``` wenzelm@53079 ` 2206` ``` done ``` wenzelm@53079 ` 2207` wenzelm@53079 ` 2208` ```lemma log_divide: "0 < a \ a \ 1 \ 0 < x \ 0 < y \ log a (x/y) = log a x - log a y" ``` wenzelm@53079 ` 2209` ``` by (simp add: log_mult divide_inverse log_inverse) ``` hoelzl@51527 ` 2210` lp15@60017 ` 2211` ```lemma powr_gt_zero [simp]: "0 < x powr a \ (x::real) \ 0" ``` lp15@60017 ` 2212` ``` by (simp add: powr_def) ``` lp15@60017 ` 2213` immler@58984 ` 2214` ```lemma log_add_eq_powr: "0 < b \ b \ 1 \ 0 < x \ log b x + y = log b (x * b powr y)" ``` immler@58984 ` 2215` ``` and add_log_eq_powr: "0 < b \ b \ 1 \ 0 < x \ y + log b x = log b (b powr y * x)" ``` immler@58984 ` 2216` ``` and log_minus_eq_powr: "0 < b \ b \ 1 \ 0 < x \ log b x - y = log b (x * b powr -y)" ``` immler@58984 ` 2217` ``` and minus_log_eq_powr: "0 < b \ b \ 1 \ 0 < x \ y - log b x = log b (b powr y / x)" ``` immler@58984 ` 2218` ``` by (simp_all add: log_mult log_divide) ``` immler@58984 ` 2219` hoelzl@51527 ` 2220` ```lemma log_less_cancel_iff [simp]: ``` wenzelm@53079 ` 2221` ``` "1 < a \ 0 < x \ 0 < y \ log a x < log a y \ x < y" ``` wenzelm@53079 ` 2222` ``` apply safe ``` wenzelm@53079 ` 2223` ``` apply (rule_tac [2] powr_less_cancel) ``` wenzelm@53079 ` 2224` ``` apply (drule_tac a = "log a x" in powr_less_mono, auto) ``` wenzelm@53079 ` 2225` ``` done ``` wenzelm@53079 ` 2226` wenzelm@53079 ` 2227` ```lemma log_inj: ``` wenzelm@53079 ` 2228` ``` assumes "1 < b" ``` wenzelm@53079 ` 2229` ``` shows "inj_on (log b) {0 <..}" ``` hoelzl@51527 ` 2230` ```proof (rule inj_onI, simp) ``` wenzelm@53079 ` 2231` ``` fix x y ``` wenzelm@53079 ` 2232` ``` assume pos: "0 < x" "0 < y" and *: "log b x = log b y" ``` hoelzl@51527 ` 2233` ``` show "x = y" ``` hoelzl@51527 ` 2234` ``` proof (cases rule: linorder_cases) ``` wenzelm@53079 ` 2235` ``` assume "x = y" ``` wenzelm@53079 ` 2236` ``` then show ?thesis by simp ``` wenzelm@53079 ` 2237` ``` next ``` hoelzl@51527 ` 2238` ``` assume "x < y" hence "log b x < log b y" ``` hoelzl@51527 ` 2239` ``` using log_less_cancel_iff[OF `1 < b`] pos by simp ``` wenzelm@53079 ` 2240` ``` then show ?thesis using * by simp ``` hoelzl@51527 ` 2241` ``` next ``` hoelzl@51527 ` 2242` ``` assume "y < x" hence "log b y < log b x" ``` hoelzl@51527 ` 2243` ``` using log_less_cancel_iff[OF `1 < b`] pos by simp ``` wenzelm@53079 ` 2244` ``` then show ?thesis using * by simp ``` wenzelm@53079 ` 2245` ``` qed ``` hoelzl@51527 ` 2246` ```qed ``` hoelzl@51527 ` 2247` hoelzl@51527 ` 2248` ```lemma log_le_cancel_iff [simp]: ``` wenzelm@53079 ` 2249` ``` "1 < a \ 0 < x \ 0 < y \ (log a x \ log a y) = (x \ y)" ``` wenzelm@53079 ` 2250` ``` by (simp add: linorder_not_less [symmetric]) ``` hoelzl@51527 ` 2251` hoelzl@51527 ` 2252` ```lemma zero_less_log_cancel_iff[simp]: "1 < a \ 0 < x \ 0 < log a x \ 1 < x" ``` hoelzl@51527 ` 2253` ``` using log_less_cancel_iff[of a 1 x] by simp ``` hoelzl@51527 ` 2254` hoelzl@51527 ` 2255` ```lemma zero_le_log_cancel_iff[simp]: "1 < a \ 0 < x \ 0 \ log a x \ 1 \ x" ``` hoelzl@51527 ` 2256` ``` using log_le_cancel_iff[of a 1 x] by simp ``` hoelzl@51527 ` 2257` hoelzl@51527 ` 2258` ```lemma log_less_zero_cancel_iff[simp]: "1 < a \ 0 < x \ log a x < 0 \ x < 1" ``` hoelzl@51527 ` 2259` ``` using log_less_cancel_iff[of a x 1] by simp ``` hoelzl@51527 ` 2260` hoelzl@51527 ` 2261` ```lemma log_le_zero_cancel_iff[simp]: "1 < a \ 0 < x \ log a x \ 0 \ x \ 1" ``` hoelzl@51527 ` 2262` ``` using log_le_cancel_iff[of a x 1] by simp ``` hoelzl@51527 ` 2263` hoelzl@51527 ` 2264` ```lemma one_less_log_cancel_iff[simp]: "1 < a \ 0 < x \ 1 < log a x \ a < x" ``` hoelzl@51527 ` 2265` ``` using log_less_cancel_iff[of a a x] by simp ``` hoelzl@51527 ` 2266` hoelzl@51527 ` 2267` ```lemma one_le_log_cancel_iff[simp]: "1 < a \ 0 < x \ 1 \ log a x \ a \ x" ``` hoelzl@51527 ` 2268` ``` using log_le_cancel_iff[of a a x] by simp ``` hoelzl@51527 ` 2269` hoelzl@51527 ` 2270` ```lemma log_less_one_cancel_iff[simp]: "1 < a \ 0 < x \ log a x < 1 \ x < a" ``` hoelzl@51527 ` 2271` ``` using log_less_cancel_iff[of a x a] by simp ``` hoelzl@51527 ` 2272` hoelzl@51527 ` 2273` ```lemma log_le_one_cancel_iff[simp]: "1 < a \ 0 < x \ log a x \ 1 \ x \ a" ``` hoelzl@51527 ` 2274` ``` using log_le_cancel_iff[of a x a] by simp ``` hoelzl@51527 ` 2275` immler@58984 ` 2276` ```lemma le_log_iff: ``` immler@58984 ` 2277` ``` assumes "1 < b" "x > 0" ``` lp15@60017 ` 2278` ``` shows "y \ log b x \ b powr y \ (x::real)" ``` lp15@60017 ` 2279` ``` using assms ``` lp15@60017 ` 2280` ``` apply auto ``` lp15@60017 ` 2281` ``` apply (metis (no_types, hide_lams) less_irrefl less_le_trans linear powr_le_cancel_iff ``` lp15@60017 ` 2282` ``` powr_log_cancel zero_less_one) ``` lp15@60017 ` 2283` ``` apply (metis not_less order.trans order_refl powr_le_cancel_iff powr_log_cancel zero_le_one) ``` lp15@60017 ` 2284` ``` done ``` immler@58984 ` 2285` immler@58984 ` 2286` ```lemma less_log_iff: ``` immler@58984 ` 2287` ``` assumes "1 < b" "x > 0" ``` immler@58984 ` 2288` ``` shows "y < log b x \ b powr y < x" ``` lp15@60017 ` 2289` ``` by (metis assms dual_order.strict_trans less_irrefl powr_less_cancel_iff ``` immler@58984 ` 2290` ``` powr_log_cancel zero_less_one) ``` immler@58984 ` 2291` immler@58984 ` 2292` ```lemma ``` immler@58984 ` 2293` ``` assumes "1 < b" "x > 0" ``` immler@58984 ` 2294` ``` shows log_less_iff: "log b x < y \ x < b powr y" ``` immler@58984 ` 2295` ``` and log_le_iff: "log b x \ y \ x \ b powr y" ``` immler@58984 ` 2296` ``` using le_log_iff[OF assms, of y] less_log_iff[OF assms, of y] ``` immler@58984 ` 2297` ``` by auto ``` immler@58984 ` 2298` immler@58984 ` 2299` ```lemmas powr_le_iff = le_log_iff[symmetric] ``` immler@58984 ` 2300` ``` and powr_less_iff = le_log_iff[symmetric] ``` immler@58984 ` 2301` ``` and less_powr_iff = log_less_iff[symmetric] ``` immler@58984 ` 2302` ``` and le_powr_iff = log_le_iff[symmetric] ``` immler@58984 ` 2303` immler@58984 ` 2304` ```lemma ``` immler@58984 ` 2305` ``` floor_log_eq_powr_iff: "x > 0 \ b > 1 \ \log b x\ = k \ b powr k \ x \ x < b powr (k + 1)" ``` immler@58984 ` 2306` ``` by (auto simp add: floor_eq_iff powr_le_iff less_powr_iff) ``` immler@58984 ` 2307` hoelzl@51527 ` 2308` ```lemma powr_realpow: "0 < x ==> x powr (real n) = x^n" ``` wenzelm@53079 ` 2309` ``` apply (induct n) ``` wenzelm@53079 ` 2310` ``` apply simp ``` lp15@60162 ` 2311` ``` by (simp add: add.commute power.simps(2) powr_add real_of_nat_Suc) ``` hoelzl@51527 ` 2312` haftmann@54489 ` 2313` ```lemma powr_realpow_numeral: "0 < x \ x powr (numeral n :: real) = x ^ (numeral n)" ``` haftmann@54489 ` 2314` ``` unfolding real_of_nat_numeral [symmetric] by (rule powr_realpow) ``` noschinl@52139 ` 2315` nipkow@57180 ` 2316` ```lemma powr2_sqrt[simp]: "0 < x \ sqrt x powr 2 = x" ``` nipkow@57180 ` 2317` ```by(simp add: powr_realpow_numeral) ``` nipkow@57180 ` 2318` hoelzl@51527 ` 2319` ```lemma powr_realpow2: "0 <= x ==> 0 < n ==> x^n = (if (x = 0) then 0 else x powr (real n))" ``` hoelzl@51527 ` 2320` ``` apply (case_tac "x = 0", simp, simp) ``` hoelzl@51527 ` 2321` ``` apply (rule powr_realpow [THEN sym], simp) ``` wenzelm@53079 ` 2322` ``` done ``` hoelzl@51527 ` 2323` hoelzl@51527 ` 2324` ```lemma powr_int: ``` hoelzl@51527 ` 2325` ``` assumes "x > 0" ``` hoelzl@51527 ` 2326` ``` shows "x powr i = (if i \ 0 then x ^ nat i else 1 / x ^ nat (-i))" ``` wenzelm@53079 ` 2327` ```proof (cases "i < 0") ``` wenzelm@53079 ` 2328` ``` case True ``` hoelzl@51527 ` 2329` ``` have r: "x powr i = 1 / x powr (-i)" by (simp add: powr_minus field_simps) ``` hoelzl@51527 ` 2330` ``` show ?thesis using `i < 0` `x > 0` by (simp add: r field_simps powr_realpow[symmetric]) ``` wenzelm@53079 ` 2331` ```next ``` wenzelm@53079 ` 2332` ``` case False ``` wenzelm@53079 ` 2333` ``` then show ?thesis by (simp add: assms powr_realpow[symmetric]) ``` wenzelm@53079 ` 2334` ```qed ``` hoelzl@51527 ` 2335` immler@58981 ` 2336` ```lemma compute_powr[code]: ``` immler@58981 ` 2337` ``` fixes i::real ``` immler@58981 ` 2338` ``` shows "b powr i = ``` immler@58981 ` 2339` ``` (if b \ 0 then Code.abort (STR ''op powr with nonpositive base'') (\_. b powr i) ``` nipkow@59587 ` 2340` ``` else if floor i = i then (if 0 \ i then b ^ nat(floor i) else 1 / b ^ nat(floor (- i))) ``` immler@58981 ` 2341` ``` else Code.abort (STR ''op powr with non-integer exponent'') (\_. b powr i))" ``` nipkow@59587 ` 2342` ``` by (auto simp: powr_int) ``` immler@58981 ` 2343` lp15@60017 ` 2344` ```lemma powr_one: ``` lp15@60017 ` 2345` ``` fixes x::real shows "0 \ x \ x powr 1 = x" ``` lp15@60017 ` 2346` ``` using powr_realpow [of x 1] ``` lp15@60017 ` 2347` ``` by simp ``` lp15@60017 ` 2348` lp15@60017 ` 2349` ```lemma powr_numeral: ``` lp15@60017 ` 2350` ``` fixes x::real shows "0 < x \ x powr numeral n = x ^ numeral n" ``` haftmann@54489 ` 2351` ``` by (fact powr_realpow_numeral) ``` haftmann@54489 ` 2352` lp15@60017 ` 2353` ```lemma powr_neg_one: ``` lp15@60017 ` 2354` ``` fixes x::real shows "0 < x \ x powr - 1 = 1 / x" ``` haftmann@54489 ` 2355` ``` using powr_int [of x "- 1"] by simp ``` haftmann@54489 ` 2356` lp15@60017 ` 2357` ```lemma powr_neg_numeral: ``` lp15@60017 ` 2358` ``` fixes x::real shows "0 < x \ x powr - numeral n = 1 / x ^ numeral n" ``` haftmann@54489 ` 2359` ``` using powr_int [of x "- numeral n"] by simp ``` hoelzl@51527 ` 2360` wenzelm@53079 ` 2361` ```lemma root_powr_inverse: "0 < n \ 0 < x \ root n x = x powr (1/n)" ``` hoelzl@51527 ` 2362` ``` by (rule real_root_pos_unique) (auto simp: powr_realpow[symmetric] powr_powr) ``` hoelzl@51527 ` 2363` lp15@60017 ` 2364` ```lemma ln_powr: ``` lp15@60017 ` 2365` ``` fixes x::real shows "x \ 0 \ ln (x powr y) = y * ln x" ``` hoelzl@56483 ` 2366` ``` by (simp add: powr_def) ``` hoelzl@56483 ` 2367` nipkow@56952 ` 2368` ```lemma ln_root: "\ n > 0; b > 0 \ \ ln (root n b) = ln b / n" ``` nipkow@56952 ` 2369` ```by(simp add: root_powr_inverse ln_powr) ``` nipkow@56952 ` 2370` hoelzl@57275 ` 2371` ```lemma ln_sqrt: "0 < x \ ln (sqrt x) = ln x / 2" ``` haftmann@57512 ` 2372` ``` by (simp add: ln_powr powr_numeral ln_powr[symmetric] mult.commute) ``` hoelzl@57275 ` 2373` nipkow@56952 ` 2374` ```lemma log_root: "\ n > 0; a > 0 \ \ log b (root n a) = log b a / n" ``` nipkow@56952 ` 2375` ```by(simp add: log_def ln_root) ``` nipkow@56952 ` 2376` lp15@60017 ` 2377` ```lemma log_powr: "x \ 0 \ log b (x powr y) = y * log b x" ``` hoelzl@56483 ` 2378` ``` by (simp add: log_def ln_powr) ``` hoelzl@56483 ` 2379` lp15@59730 ` 2380` ```lemma log_nat_power: "0 < x \ log b (x^n) = real n * log b x" ``` hoelzl@56483 ` 2381` ``` by (simp add: log_powr powr_realpow [symmetric]) ``` hoelzl@56483 ` 2382` hoelzl@56483 ` 2383` ```lemma log_base_change: "0 < a \ a \ 1 \ log b x = log a x / log a b" ``` hoelzl@56483 ` 2384` ``` by (simp add: log_def) ``` hoelzl@56483 ` 2385` hoelzl@56483 ` 2386` ```lemma log_base_pow: "0 < a \ log (a ^ n) x = log a x / n" ``` hoelzl@56483 ` 2387` ``` by (simp add: log_def ln_realpow) ``` hoelzl@56483 ` 2388` lp15@60017 ` 2389` ```lemma log_base_powr: "a \ 0 \ log (a powr b) x = log a x / b" ``` hoelzl@56483 ` 2390` ``` by (simp add: log_def ln_powr) ``` hoelzl@51527 ` 2391` nipkow@56952 ` 2392` ```lemma log_base_root: "\ n > 0; b > 0 \ \ log (root n b) x = n * (log b x)" ``` nipkow@56952 ` 2393` ```by(simp add: log_def ln_root) ``` nipkow@56952 ` 2394` lp15@60017 ` 2395` ```lemma ln_bound: ``` lp15@60017 ` 2396` ``` fixes x::real shows "1 <= x ==> ln x <= x" ``` hoelzl@51527 ` 2397` ``` apply (subgoal_tac "ln(1 + (x - 1)) <= x - 1") ``` hoelzl@51527 ` 2398` ``` apply simp ``` hoelzl@51527 ` 2399` ``` apply (rule ln_add_one_self_le_self, simp) ``` wenzelm@53079 ` 2400` ``` done ``` hoelzl@51527 ` 2401` lp15@60017 ` 2402` ```lemma powr_mono: ``` lp15@60017 ` 2403` ``` fixes x::real shows "a <= b ==> 1 <= x ==> x powr a <= x powr b" ``` wenzelm@53079 ` 2404` ``` apply (cases "x = 1", simp) ``` wenzelm@53079 ` 2405` ``` apply (cases "a = b", simp) ``` hoelzl@51527 ` 2406` ``` apply (rule order_less_imp_le) ``` hoelzl@51527 ` 2407` ``` apply (rule powr_less_mono, auto) ``` wenzelm@53079 ` 2408` ``` done ``` hoelzl@51527 ` 2409` lp15@60017 ` 2410` ```lemma ge_one_powr_ge_zero: ``` lp15@60017 ` 2411` ``` fixes x::real shows "1 <= x ==> 0 <= a ==> 1 <= x powr a" ``` lp15@60017 ` 2412` ```using powr_mono by fastforce ``` lp15@60017 ` 2413` lp15@60017 ` 2414` ```lemma powr_less_mono2: ``` lp15@60141 ` 2415` ``` fixes x::real shows "0 < a ==> 0 \ x ==> x < y ==> x powr a < y powr a" ``` lp15@60017 ` 2416` ``` by (simp add: powr_def) ``` lp15@60017 ` 2417` lp15@60017 ` 2418` ```lemma powr_less_mono2_neg: ``` lp15@60017 ` 2419` ``` fixes x::real shows "a < 0 ==> 0 < x ==> x < y ==> y powr a < x powr a" ``` lp15@60017 ` 2420` ``` by (simp add: powr_def) ``` lp15@60017 ` 2421` lp15@60017 ` 2422` ```lemma powr_mono2: ``` lp15@60141 ` 2423` ``` fixes x::real shows "0 <= a ==> 0 \ x ==> x <= y ==> x powr a <= y powr a" ``` hoelzl@51527 ` 2424` ``` apply (case_tac "a = 0", simp) ``` hoelzl@51527 ` 2425` ``` apply (case_tac "x = y", simp) ``` lp15@60141 ` 2426` ``` apply (metis dual_order.strict_iff_order powr_less_mono2) ``` wenzelm@53079 ` 2427` ``` done ``` wenzelm@53079 ` 2428` lp15@60017 ` 2429` ```lemma powr_inj: ``` lp15@60017 ` 2430` ``` fixes x::real shows "0 < a \ a \ 1 \ a powr x = a powr y \ x = y" ``` hoelzl@51527 ` 2431` ``` unfolding powr_def exp_inj_iff by simp ``` hoelzl@51527 ` 2432` lp15@60141 ` 2433` ```lemma powr_half_sqrt: "0 \ x \ x powr (1/2) = sqrt x" ``` lp15@60141 ` 2434` ``` by (simp add: powr_def root_powr_inverse sqrt_def) ``` lp15@60141 ` 2435` lp15@60017 ` 2436` ```lemma ln_powr_bound: ``` lp15@60017 ` 2437` ``` fixes x::real shows "1 <= x ==> 0 < a ==> ln x <= (x powr a) / a" ``` lp15@60017 ` 2438` ```by (metis exp_gt_zero linear ln_eq_zero_iff ln_exp ln_less_self ln_powr mult.commute mult_imp_le_div_pos not_less powr_gt_zero) ``` lp15@60017 ` 2439` hoelzl@51527 ` 2440` hoelzl@51527 ` 2441` ```lemma ln_powr_bound2: ``` lp15@60017 ` 2442` ``` fixes x::real ``` hoelzl@51527 ` 2443` ``` assumes "1 < x" and "0 < a" ``` hoelzl@51527 ` 2444` ``` shows "(ln x) powr a <= (a powr a) * x" ``` hoelzl@51527 ` 2445` ```proof - ```