1301 using ln_inj_iff [of x 1] by simp |
1301 using ln_inj_iff [of x 1] by simp |
1302 |
1302 |
1303 lemma ln_less_zero: "0 < x \<Longrightarrow> x < 1 \<Longrightarrow> ln x < 0" |
1303 lemma ln_less_zero: "0 < x \<Longrightarrow> x < 1 \<Longrightarrow> ln x < 0" |
1304 by simp |
1304 by simp |
1305 |
1305 |
1306 lemma isCont_ln: "0 < x \<Longrightarrow> isCont ln x" |
1306 lemma ln_neg_is_const: "x \<le> 0 \<Longrightarrow> ln x = (THE x. False)" |
1307 apply (subgoal_tac "isCont ln (exp (ln x))", simp) |
1307 by (auto simp add: ln_def intro!: arg_cong[where f=The]) |
1308 apply (rule isCont_inverse_function [where f=exp], simp_all) |
1308 |
1309 done |
1309 lemma isCont_ln: assumes "x \<noteq> 0" shows "isCont ln x" |
|
1310 proof cases |
|
1311 assume "0 < x" |
|
1312 moreover then have "isCont ln (exp (ln x))" |
|
1313 by (intro isCont_inv_fun[where d="\<bar>x\<bar>" and f=exp]) auto |
|
1314 ultimately show ?thesis |
|
1315 by simp |
|
1316 next |
|
1317 assume "\<not> 0 < x" with `x \<noteq> 0` show "isCont ln x" |
|
1318 unfolding isCont_def |
|
1319 by (subst filterlim_cong[OF _ refl, of _ "nhds (ln 0)" _ "\<lambda>_. ln 0"]) |
|
1320 (auto simp: ln_neg_is_const not_less eventually_at dist_real_def |
|
1321 intro!: tendsto_const exI[of _ "\<bar>x\<bar>"]) |
|
1322 qed |
1310 |
1323 |
1311 lemma tendsto_ln [tendsto_intros]: |
1324 lemma tendsto_ln [tendsto_intros]: |
1312 "(f ---> a) F \<Longrightarrow> 0 < a \<Longrightarrow> ((\<lambda>x. ln (f x)) ---> ln a) F" |
1325 "(f ---> a) F \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> ((\<lambda>x. ln (f x)) ---> ln a) F" |
1313 by (rule isCont_tendsto_compose [OF isCont_ln]) |
1326 by (rule isCont_tendsto_compose [OF isCont_ln]) |
1314 |
1327 |
1315 lemma continuous_ln: |
1328 lemma continuous_ln: |
1316 "continuous F f \<Longrightarrow> 0 < f (Lim F (\<lambda>x. x)) \<Longrightarrow> continuous F (\<lambda>x. ln (f x))" |
1329 "continuous F f \<Longrightarrow> f (Lim F (\<lambda>x. x)) \<noteq> 0 \<Longrightarrow> continuous F (\<lambda>x. ln (f x))" |
1317 unfolding continuous_def by (rule tendsto_ln) |
1330 unfolding continuous_def by (rule tendsto_ln) |
1318 |
1331 |
1319 lemma isCont_ln' [continuous_intros]: |
1332 lemma isCont_ln' [continuous_intros]: |
1320 "continuous (at x) f \<Longrightarrow> 0 < f x \<Longrightarrow> continuous (at x) (\<lambda>x. ln (f x))" |
1333 "continuous (at x) f \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> continuous (at x) (\<lambda>x. ln (f x))" |
1321 unfolding continuous_at by (rule tendsto_ln) |
1334 unfolding continuous_at by (rule tendsto_ln) |
1322 |
1335 |
1323 lemma continuous_within_ln [continuous_intros]: |
1336 lemma continuous_within_ln [continuous_intros]: |
1324 "continuous (at x within s) f \<Longrightarrow> 0 < f x \<Longrightarrow> continuous (at x within s) (\<lambda>x. ln (f x))" |
1337 "continuous (at x within s) f \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> continuous (at x within s) (\<lambda>x. ln (f x))" |
1325 unfolding continuous_within by (rule tendsto_ln) |
1338 unfolding continuous_within by (rule tendsto_ln) |
1326 |
1339 |
1327 lemma continuous_on_ln [continuous_intros]: |
1340 lemma continuous_on_ln [continuous_intros]: |
1328 "continuous_on s f \<Longrightarrow> (\<forall>x\<in>s. 0 < f x) \<Longrightarrow> continuous_on s (\<lambda>x. ln (f x))" |
1341 "continuous_on s f \<Longrightarrow> (\<forall>x\<in>s. f x \<noteq> 0) \<Longrightarrow> continuous_on s (\<lambda>x. ln (f x))" |
1329 unfolding continuous_on_def by (auto intro: tendsto_ln) |
1342 unfolding continuous_on_def by (auto intro: tendsto_ln) |
1330 |
1343 |
1331 lemma DERIV_ln: "0 < x \<Longrightarrow> DERIV ln x :> inverse x" |
1344 lemma DERIV_ln: "0 < x \<Longrightarrow> DERIV ln x :> inverse x" |
1332 apply (rule DERIV_inverse_function [where f=exp and a=0 and b="x+1"]) |
1345 apply (rule DERIV_inverse_function [where f=exp and a=0 and b="x+1"]) |
1333 apply (auto intro: DERIV_cong [OF DERIV_exp exp_ln] isCont_ln) |
1346 apply (auto intro: DERIV_cong [OF DERIV_exp exp_ln] isCont_ln) |
1990 by (simp add: powr_def) |
2003 by (simp add: powr_def) |
1991 |
2004 |
1992 lemma ln_root: "\<lbrakk> n > 0; b > 0 \<rbrakk> \<Longrightarrow> ln (root n b) = ln b / n" |
2005 lemma ln_root: "\<lbrakk> n > 0; b > 0 \<rbrakk> \<Longrightarrow> ln (root n b) = ln b / n" |
1993 by(simp add: root_powr_inverse ln_powr) |
2006 by(simp add: root_powr_inverse ln_powr) |
1994 |
2007 |
|
2008 lemma ln_sqrt: "0 < x \<Longrightarrow> ln (sqrt x) = ln x / 2" |
|
2009 by (simp add: ln_powr powr_numeral ln_powr[symmetric] mult_commute) |
|
2010 |
1995 lemma log_root: "\<lbrakk> n > 0; a > 0 \<rbrakk> \<Longrightarrow> log b (root n a) = log b a / n" |
2011 lemma log_root: "\<lbrakk> n > 0; a > 0 \<rbrakk> \<Longrightarrow> log b (root n a) = log b a / n" |
1996 by(simp add: log_def ln_root) |
2012 by(simp add: log_def ln_root) |
1997 |
2013 |
1998 lemma log_powr: "log b (x powr y) = y * log b x" |
2014 lemma log_powr: "log b (x powr y) = y * log b x" |
1999 by (simp add: log_def ln_powr) |
2015 by (simp add: log_def ln_powr) |
2083 by auto |
2099 by auto |
2084 finally show ?thesis . |
2100 finally show ?thesis . |
2085 qed |
2101 qed |
2086 |
2102 |
2087 lemma tendsto_powr [tendsto_intros]: |
2103 lemma tendsto_powr [tendsto_intros]: |
2088 "\<lbrakk>(f ---> a) F; (g ---> b) F; 0 < a\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x powr g x) ---> a powr b) F" |
2104 "\<lbrakk>(f ---> a) F; (g ---> b) F; a \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x powr g x) ---> a powr b) F" |
2089 unfolding powr_def by (intro tendsto_intros) |
2105 unfolding powr_def by (intro tendsto_intros) |
2090 |
2106 |
2091 lemma continuous_powr: |
2107 lemma continuous_powr: |
2092 assumes "continuous F f" |
2108 assumes "continuous F f" |
2093 and "continuous F g" |
2109 and "continuous F g" |
2094 and "0 < f (Lim F (\<lambda>x. x))" |
2110 and "f (Lim F (\<lambda>x. x)) \<noteq> 0" |
2095 shows "continuous F (\<lambda>x. (f x) powr (g x))" |
2111 shows "continuous F (\<lambda>x. (f x) powr (g x))" |
2096 using assms unfolding continuous_def by (rule tendsto_powr) |
2112 using assms unfolding continuous_def by (rule tendsto_powr) |
2097 |
2113 |
2098 lemma continuous_at_within_powr[continuous_intros]: |
2114 lemma continuous_at_within_powr[continuous_intros]: |
2099 assumes "continuous (at a within s) f" |
2115 assumes "continuous (at a within s) f" |
2100 and "continuous (at a within s) g" |
2116 and "continuous (at a within s) g" |
2101 and "0 < f a" |
2117 and "f a \<noteq> 0" |
2102 shows "continuous (at a within s) (\<lambda>x. (f x) powr (g x))" |
2118 shows "continuous (at a within s) (\<lambda>x. (f x) powr (g x))" |
2103 using assms unfolding continuous_within by (rule tendsto_powr) |
2119 using assms unfolding continuous_within by (rule tendsto_powr) |
2104 |
2120 |
2105 lemma isCont_powr[continuous_intros, simp]: |
2121 lemma isCont_powr[continuous_intros, simp]: |
2106 assumes "isCont f a" "isCont g a" "0 < f a" |
2122 assumes "isCont f a" "isCont g a" "f a \<noteq> 0" |
2107 shows "isCont (\<lambda>x. (f x) powr g x) a" |
2123 shows "isCont (\<lambda>x. (f x) powr g x) a" |
2108 using assms unfolding continuous_at by (rule tendsto_powr) |
2124 using assms unfolding continuous_at by (rule tendsto_powr) |
2109 |
2125 |
2110 lemma continuous_on_powr[continuous_intros]: |
2126 lemma continuous_on_powr[continuous_intros]: |
2111 assumes "continuous_on s f" "continuous_on s g" and "\<forall>x\<in>s. 0 < f x" |
2127 assumes "continuous_on s f" "continuous_on s g" and "\<forall>x\<in>s. f x \<noteq> 0" |
2112 shows "continuous_on s (\<lambda>x. (f x) powr (g x))" |
2128 shows "continuous_on s (\<lambda>x. (f x) powr (g x))" |
2113 using assms unfolding continuous_on_def by (fast intro: tendsto_powr) |
2129 using assms unfolding continuous_on_def by (fast intro: tendsto_powr) |
2114 |
2130 |
2115 (* FIXME: generalize by replacing d by with g x and g ---> d? *) |
2131 (* FIXME: generalize by replacing d by with g x and g ---> d? *) |
2116 lemma tendsto_zero_powrI: |
2132 lemma tendsto_zero_powrI: |
2148 by (simp add: powr_powr Z_def dist_real_def) |
2164 by (simp add: powr_powr Z_def dist_real_def) |
2149 ultimately |
2165 ultimately |
2150 show "eventually (\<lambda>x. dist (f x powr s) 0 < e) F" by (rule eventually_elim1) |
2166 show "eventually (\<lambda>x. dist (f x powr s) 0 < e) F" by (rule eventually_elim1) |
2151 qed |
2167 qed |
2152 |
2168 |
|
2169 (* it is funny that this isn't in the library! It could go in Transcendental *) |
|
2170 lemma tendsto_exp_limit_at_right: |
|
2171 fixes x :: real |
|
2172 shows "((\<lambda>y. (1 + x * y) powr (1 / y)) ---> exp x) (at_right 0)" |
|
2173 proof cases |
|
2174 assume "x \<noteq> 0" |
|
2175 |
|
2176 have "((\<lambda>y. ln (1 + x * y)::real) has_real_derivative 1 * x) (at 0)" |
|
2177 by (auto intro!: derivative_eq_intros) |
|
2178 then have "((\<lambda>y. ln (1 + x * y) / y) ---> x) (at 0)" |
|
2179 by (auto simp add: has_field_derivative_def field_has_derivative_at) |
|
2180 then have *: "((\<lambda>y. exp (ln (1 + x * y) / y)) ---> exp x) (at 0)" |
|
2181 by (rule tendsto_intros) |
|
2182 then show ?thesis |
|
2183 proof (rule filterlim_mono_eventually) |
|
2184 show "eventually (\<lambda>xa. exp (ln (1 + x * xa) / xa) = (1 + x * xa) powr (1 / xa)) (at_right 0)" |
|
2185 unfolding eventually_at_right[OF zero_less_one] |
|
2186 using `x \<noteq> 0` by (intro exI[of _ "1 / \<bar>x\<bar>"]) (auto simp: field_simps powr_def) |
|
2187 qed (simp_all add: at_eq_sup_left_right) |
|
2188 qed (simp add: tendsto_const) |
|
2189 |
|
2190 lemma tendsto_exp_limit_at_top: |
|
2191 fixes x :: real |
|
2192 shows "((\<lambda>y. (1 + x / y) powr y) ---> exp x) at_top" |
|
2193 apply (subst filterlim_at_top_to_right) |
|
2194 apply (simp add: inverse_eq_divide) |
|
2195 apply (rule tendsto_exp_limit_at_right) |
|
2196 done |
|
2197 |
|
2198 lemma tendsto_exp_limit_sequentially: |
|
2199 fixes x :: real |
|
2200 shows "(\<lambda>n. (1 + x / n) ^ n) ----> exp x" |
|
2201 proof (rule filterlim_mono_eventually) |
|
2202 from reals_Archimedean2 [of "abs x"] obtain n :: nat where *: "real n > abs x" .. |
|
2203 hence "eventually (\<lambda>n :: nat. 0 < 1 + x / real n) at_top" |
|
2204 apply (intro eventually_sequentiallyI [of n]) |
|
2205 apply (case_tac "x \<ge> 0") |
|
2206 apply (rule add_pos_nonneg, auto intro: divide_nonneg_nonneg) |
|
2207 apply (subgoal_tac "x / real xa > -1") |
|
2208 apply (auto simp add: field_simps) |
|
2209 done |
|
2210 then show "eventually (\<lambda>n. (1 + x / n) powr n = (1 + x / n) ^ n) at_top" |
|
2211 by (rule eventually_elim1) (erule powr_realpow) |
|
2212 show "(\<lambda>n. (1 + x / real n) powr real n) ----> exp x" |
|
2213 by (rule filterlim_compose [OF tendsto_exp_limit_at_top filterlim_real_sequentially]) |
|
2214 qed auto |
|
2215 |
2153 subsection {* Sine and Cosine *} |
2216 subsection {* Sine and Cosine *} |
2154 |
2217 |
2155 definition sin_coeff :: "nat \<Rightarrow> real" where |
2218 definition sin_coeff :: "nat \<Rightarrow> real" where |
2156 "sin_coeff = (\<lambda>n. if even n then 0 else -1 ^ ((n - Suc 0) div 2) / real (fact n))" |
2219 "sin_coeff = (\<lambda>n. if even n then 0 else -1 ^ ((n - Suc 0) div 2) / real (fact n))" |
2157 |
2220 |
2372 |
2435 |
2373 lemma cos_double: "cos(2* x) = ((cos x)\<^sup>2) - ((sin x)\<^sup>2)" |
2436 lemma cos_double: "cos(2* x) = ((cos x)\<^sup>2) - ((sin x)\<^sup>2)" |
2374 using cos_add [where x=x and y=x] |
2437 using cos_add [where x=x and y=x] |
2375 by (simp add: power2_eq_square) |
2438 by (simp add: power2_eq_square) |
2376 |
2439 |
|
2440 lemma sin_x_le_x: assumes x: "x \<ge> 0" shows "sin x \<le> x" |
|
2441 proof - |
|
2442 let ?f = "\<lambda>x. x - sin x" |
|
2443 from x have "?f x \<ge> ?f 0" |
|
2444 apply (rule DERIV_nonneg_imp_nondecreasing) |
|
2445 apply (intro allI impI exI[of _ "1 - cos x" for x]) |
|
2446 apply (auto intro!: derivative_eq_intros simp: field_simps) |
|
2447 done |
|
2448 thus "sin x \<le> x" by simp |
|
2449 qed |
|
2450 |
|
2451 lemma sin_x_ge_neg_x: assumes x: "x \<ge> 0" shows "sin x \<ge> - x" |
|
2452 proof - |
|
2453 let ?f = "\<lambda>x. x + sin x" |
|
2454 from x have "?f x \<ge> ?f 0" |
|
2455 apply (rule DERIV_nonneg_imp_nondecreasing) |
|
2456 apply (intro allI impI exI[of _ "1 + cos x" for x]) |
|
2457 apply (auto intro!: derivative_eq_intros simp: field_simps real_0_le_add_iff) |
|
2458 done |
|
2459 thus "sin x \<ge> -x" by simp |
|
2460 qed |
|
2461 |
|
2462 lemma abs_sin_x_le_abs_x: "\<bar>sin x\<bar> \<le> \<bar>x\<bar>" |
|
2463 using sin_x_ge_neg_x [of x] sin_x_le_x [of x] sin_x_ge_neg_x [of "-x"] sin_x_le_x [of "-x"] |
|
2464 by (auto simp: abs_real_def) |
2377 |
2465 |
2378 subsection {* The Constant Pi *} |
2466 subsection {* The Constant Pi *} |
2379 |
2467 |
2380 definition pi :: real |
2468 definition pi :: real |
2381 where "pi = 2 * (THE x. 0 \<le> (x::real) & x \<le> 2 & cos x = 0)" |
2469 where "pi = 2 * (THE x. 0 \<le> (x::real) & x \<le> 2 & cos x = 0)" |