179 done |
179 done |
180 qed |
180 qed |
181 |
181 |
182 corollary lim_n_over_pown: |
182 corollary lim_n_over_pown: |
183 fixes x :: "'a::{real_normed_field,banach}" |
183 fixes x :: "'a::{real_normed_field,banach}" |
184 shows "1 < norm x \<Longrightarrow> ((\<lambda>n. of_nat n / x^n) ---> 0) sequentially" |
184 shows "1 < norm x \<Longrightarrow> ((\<lambda>n. of_nat n / x^n) \<longlongrightarrow> 0) sequentially" |
185 using powser_times_n_limit_0 [of "inverse x"] |
185 using powser_times_n_limit_0 [of "inverse x"] |
186 by (simp add: norm_divide divide_simps) |
186 by (simp add: norm_divide divide_simps) |
187 |
187 |
188 lemma sum_split_even_odd: |
188 lemma sum_split_even_odd: |
189 fixes f :: "nat \<Rightarrow> real" |
189 fixes f :: "nat \<Rightarrow> real" |
809 |
809 |
810 lemma powser_limit_0: |
810 lemma powser_limit_0: |
811 fixes a :: "nat \<Rightarrow> 'a::{real_normed_field,banach}" |
811 fixes a :: "nat \<Rightarrow> 'a::{real_normed_field,banach}" |
812 assumes s: "0 < s" |
812 assumes s: "0 < s" |
813 and sm: "\<And>x. norm x < s \<Longrightarrow> (\<lambda>n. a n * x ^ n) sums (f x)" |
813 and sm: "\<And>x. norm x < s \<Longrightarrow> (\<lambda>n. a n * x ^ n) sums (f x)" |
814 shows "(f ---> a 0) (at 0)" |
814 shows "(f \<longlongrightarrow> a 0) (at 0)" |
815 proof - |
815 proof - |
816 have "summable (\<lambda>n. a n * (of_real s / 2) ^ n)" |
816 have "summable (\<lambda>n. a n * (of_real s / 2) ^ n)" |
817 apply (rule sums_summable [where l = "f (of_real s / 2)", OF sm]) |
817 apply (rule sums_summable [where l = "f (of_real s / 2)", OF sm]) |
818 using s |
818 using s |
819 apply (auto simp: norm_divide) |
819 apply (auto simp: norm_divide) |
823 using s |
823 using s |
824 apply (auto simp: norm_divide) |
824 apply (auto simp: norm_divide) |
825 done |
825 done |
826 then have "isCont (\<lambda>x. \<Sum>n. a n * x ^ n) 0" |
826 then have "isCont (\<lambda>x. \<Sum>n. a n * x ^ n) 0" |
827 by (blast intro: DERIV_continuous) |
827 by (blast intro: DERIV_continuous) |
828 then have "((\<lambda>x. \<Sum>n. a n * x ^ n) ---> a 0) (at 0)" |
828 then have "((\<lambda>x. \<Sum>n. a n * x ^ n) \<longlongrightarrow> a 0) (at 0)" |
829 by (simp add: continuous_within powser_zero) |
829 by (simp add: continuous_within powser_zero) |
830 then show ?thesis |
830 then show ?thesis |
831 apply (rule Lim_transform) |
831 apply (rule Lim_transform) |
832 apply (auto simp add: LIM_eq) |
832 apply (auto simp add: LIM_eq) |
833 apply (rule_tac x="s" in exI) |
833 apply (rule_tac x="s" in exI) |
838 |
838 |
839 lemma powser_limit_0_strong: |
839 lemma powser_limit_0_strong: |
840 fixes a :: "nat \<Rightarrow> 'a::{real_normed_field,banach}" |
840 fixes a :: "nat \<Rightarrow> 'a::{real_normed_field,banach}" |
841 assumes s: "0 < s" |
841 assumes s: "0 < s" |
842 and sm: "\<And>x. x \<noteq> 0 \<Longrightarrow> norm x < s \<Longrightarrow> (\<lambda>n. a n * x ^ n) sums (f x)" |
842 and sm: "\<And>x. x \<noteq> 0 \<Longrightarrow> norm x < s \<Longrightarrow> (\<lambda>n. a n * x ^ n) sums (f x)" |
843 shows "(f ---> a 0) (at 0)" |
843 shows "(f \<longlongrightarrow> a 0) (at 0)" |
844 proof - |
844 proof - |
845 have *: "((\<lambda>x. if x = 0 then a 0 else f x) ---> a 0) (at 0)" |
845 have *: "((\<lambda>x. if x = 0 then a 0 else f x) \<longlongrightarrow> a 0) (at 0)" |
846 apply (rule powser_limit_0 [OF s]) |
846 apply (rule powser_limit_0 [OF s]) |
847 apply (case_tac "x=0") |
847 apply (case_tac "x=0") |
848 apply (auto simp add: powser_sums_zero sm) |
848 apply (auto simp add: powser_sums_zero sm) |
849 done |
849 done |
850 show ?thesis |
850 show ?thesis |
1206 shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. exp (f x)) a" |
1206 shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. exp (f x)) a" |
1207 by (rule isCont_o2 [OF _ isCont_exp]) |
1207 by (rule isCont_o2 [OF _ isCont_exp]) |
1208 |
1208 |
1209 lemma tendsto_exp [tendsto_intros]: |
1209 lemma tendsto_exp [tendsto_intros]: |
1210 fixes f:: "_ \<Rightarrow>'a::{real_normed_field,banach}" |
1210 fixes f:: "_ \<Rightarrow>'a::{real_normed_field,banach}" |
1211 shows "(f ---> a) F \<Longrightarrow> ((\<lambda>x. exp (f x)) ---> exp a) F" |
1211 shows "(f \<longlongrightarrow> a) F \<Longrightarrow> ((\<lambda>x. exp (f x)) \<longlongrightarrow> exp a) F" |
1212 by (rule isCont_tendsto_compose [OF isCont_exp]) |
1212 by (rule isCont_tendsto_compose [OF isCont_exp]) |
1213 |
1213 |
1214 lemma continuous_exp [continuous_intros]: |
1214 lemma continuous_exp [continuous_intros]: |
1215 fixes f:: "_ \<Rightarrow>'a::{real_normed_field,banach}" |
1215 fixes f:: "_ \<Rightarrow>'a::{real_normed_field,banach}" |
1216 shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. exp (f x))" |
1216 shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. exp (f x))" |
1595 intro!: exI[of _ "\<bar>x\<bar>"]) |
1595 intro!: exI[of _ "\<bar>x\<bar>"]) |
1596 qed |
1596 qed |
1597 |
1597 |
1598 lemma tendsto_ln [tendsto_intros]: |
1598 lemma tendsto_ln [tendsto_intros]: |
1599 fixes a::real shows |
1599 fixes a::real shows |
1600 "(f ---> a) F \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> ((\<lambda>x. ln (f x)) ---> ln a) F" |
1600 "(f \<longlongrightarrow> a) F \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> ((\<lambda>x. ln (f x)) \<longlongrightarrow> ln a) F" |
1601 by (rule isCont_tendsto_compose [OF isCont_ln]) |
1601 by (rule isCont_tendsto_compose [OF isCont_ln]) |
1602 |
1602 |
1603 lemma continuous_ln: |
1603 lemma continuous_ln: |
1604 "continuous F f \<Longrightarrow> f (Lim F (\<lambda>x. x)) \<noteq> 0 \<Longrightarrow> continuous F (\<lambda>x. ln (f x :: real))" |
1604 "continuous F f \<Longrightarrow> f (Lim F (\<lambda>x. x)) \<noteq> 0 \<Longrightarrow> continuous F (\<lambda>x. ln (f x :: real))" |
1605 unfolding continuous_def by (rule tendsto_ln) |
1605 unfolding continuous_def by (rule tendsto_ln) |
2034 by (rule filterlim_at_top_at_top[where Q="\<lambda>x. True" and P="\<lambda>x. 0 < x" and g="ln"]) |
2034 by (rule filterlim_at_top_at_top[where Q="\<lambda>x. True" and P="\<lambda>x. 0 < x" and g="ln"]) |
2035 (auto intro: eventually_gt_at_top) |
2035 (auto intro: eventually_gt_at_top) |
2036 |
2036 |
2037 lemma lim_exp_minus_1: |
2037 lemma lim_exp_minus_1: |
2038 fixes x :: "'a::{real_normed_field,banach}" |
2038 fixes x :: "'a::{real_normed_field,banach}" |
2039 shows "((\<lambda>z::'a. (exp(z) - 1) / z) ---> 1) (at 0)" |
2039 shows "((\<lambda>z::'a. (exp(z) - 1) / z) \<longlongrightarrow> 1) (at 0)" |
2040 proof - |
2040 proof - |
2041 have "((\<lambda>z::'a. exp(z) - 1) has_field_derivative 1) (at 0)" |
2041 have "((\<lambda>z::'a. exp(z) - 1) has_field_derivative 1) (at 0)" |
2042 by (intro derivative_eq_intros | simp)+ |
2042 by (intro derivative_eq_intros | simp)+ |
2043 then show ?thesis |
2043 then show ?thesis |
2044 by (simp add: Deriv.DERIV_iff2) |
2044 by (simp add: Deriv.DERIV_iff2) |
2057 |
2057 |
2058 lemma filtermap_exp_at_top: "filtermap (exp::real \<Rightarrow> real) at_top = at_top" |
2058 lemma filtermap_exp_at_top: "filtermap (exp::real \<Rightarrow> real) at_top = at_top" |
2059 by (intro filtermap_fun_inverse[of ln] exp_at_top ln_at_top) |
2059 by (intro filtermap_fun_inverse[of ln] exp_at_top ln_at_top) |
2060 (auto simp: eventually_at_top_dense) |
2060 (auto simp: eventually_at_top_dense) |
2061 |
2061 |
2062 lemma tendsto_power_div_exp_0: "((\<lambda>x. x ^ k / exp x) ---> (0::real)) at_top" |
2062 lemma tendsto_power_div_exp_0: "((\<lambda>x. x ^ k / exp x) \<longlongrightarrow> (0::real)) at_top" |
2063 proof (induct k) |
2063 proof (induct k) |
2064 case 0 |
2064 case 0 |
2065 show "((\<lambda>x. x ^ 0 / exp x) ---> (0::real)) at_top" |
2065 show "((\<lambda>x. x ^ 0 / exp x) \<longlongrightarrow> (0::real)) at_top" |
2066 by (simp add: inverse_eq_divide[symmetric]) |
2066 by (simp add: inverse_eq_divide[symmetric]) |
2067 (metis filterlim_compose[OF tendsto_inverse_0] exp_at_top filterlim_mono |
2067 (metis filterlim_compose[OF tendsto_inverse_0] exp_at_top filterlim_mono |
2068 at_top_le_at_infinity order_refl) |
2068 at_top_le_at_infinity order_refl) |
2069 next |
2069 next |
2070 case (Suc k) |
2070 case (Suc k) |
2075 show "eventually (\<lambda>x. DERIV exp x :> exp x) at_top" |
2075 show "eventually (\<lambda>x. DERIV exp x :> exp x) at_top" |
2076 by eventually_elim auto |
2076 by eventually_elim auto |
2077 show "eventually (\<lambda>x. exp x \<noteq> 0) at_top" |
2077 show "eventually (\<lambda>x. exp x \<noteq> 0) at_top" |
2078 by auto |
2078 by auto |
2079 from tendsto_mult[OF tendsto_const Suc, of "real (Suc k)"] |
2079 from tendsto_mult[OF tendsto_const Suc, of "real (Suc k)"] |
2080 show "((\<lambda>x. real (Suc k) * x ^ k / exp x) ---> 0) at_top" |
2080 show "((\<lambda>x. real (Suc k) * x ^ k / exp x) \<longlongrightarrow> 0) at_top" |
2081 by simp |
2081 by simp |
2082 qed (rule exp_at_top) |
2082 qed (rule exp_at_top) |
2083 qed |
2083 qed |
2084 |
2084 |
2085 |
2085 |
2087 \<comment> \<open>logarithm of @{term x} to base @{term a}\<close> |
2087 \<comment> \<open>logarithm of @{term x} to base @{term a}\<close> |
2088 where "log a x = ln x / ln a" |
2088 where "log a x = ln x / ln a" |
2089 |
2089 |
2090 |
2090 |
2091 lemma tendsto_log [tendsto_intros]: |
2091 lemma tendsto_log [tendsto_intros]: |
2092 "\<lbrakk>(f ---> a) F; (g ---> b) F; 0 < a; a \<noteq> 1; 0 < b\<rbrakk> \<Longrightarrow> ((\<lambda>x. log (f x) (g x)) ---> log a b) F" |
2092 "\<lbrakk>(f \<longlongrightarrow> a) F; (g \<longlongrightarrow> b) F; 0 < a; a \<noteq> 1; 0 < b\<rbrakk> \<Longrightarrow> ((\<lambda>x. log (f x) (g x)) \<longlongrightarrow> log a b) F" |
2093 unfolding log_def by (intro tendsto_intros) auto |
2093 unfolding log_def by (intro tendsto_intros) auto |
2094 |
2094 |
2095 lemma continuous_log: |
2095 lemma continuous_log: |
2096 assumes "continuous F f" |
2096 assumes "continuous F f" |
2097 and "continuous F g" |
2097 and "continuous F g" |
2503 finally show ?thesis . |
2503 finally show ?thesis . |
2504 qed |
2504 qed |
2505 |
2505 |
2506 lemma tendsto_powr [tendsto_intros]: |
2506 lemma tendsto_powr [tendsto_intros]: |
2507 fixes a::real |
2507 fixes a::real |
2508 assumes f: "(f ---> a) F" and g: "(g ---> b) F" and a: "a \<noteq> 0" |
2508 assumes f: "(f \<longlongrightarrow> a) F" and g: "(g \<longlongrightarrow> b) F" and a: "a \<noteq> 0" |
2509 shows "((\<lambda>x. f x powr g x) ---> a powr b) F" |
2509 shows "((\<lambda>x. f x powr g x) \<longlongrightarrow> a powr b) F" |
2510 unfolding powr_def |
2510 unfolding powr_def |
2511 proof (rule filterlim_If) |
2511 proof (rule filterlim_If) |
2512 from f show "((\<lambda>x. 0) ---> (if a = 0 then 0 else exp (b * ln a))) (inf F (principal {x. f x = 0}))" |
2512 from f show "((\<lambda>x. 0) \<longlongrightarrow> (if a = 0 then 0 else exp (b * ln a))) (inf F (principal {x. f x = 0}))" |
2513 by simp (auto simp: filterlim_iff eventually_inf_principal elim: eventually_mono dest: t1_space_nhds) |
2513 by simp (auto simp: filterlim_iff eventually_inf_principal elim: eventually_mono dest: t1_space_nhds) |
2514 qed (insert f g a, auto intro!: tendsto_intros intro: tendsto_mono inf_le1) |
2514 qed (insert f g a, auto intro!: tendsto_intros intro: tendsto_mono inf_le1) |
2515 |
2515 |
2516 lemma continuous_powr: |
2516 lemma continuous_powr: |
2517 assumes "continuous F f" |
2517 assumes "continuous F f" |
2537 shows "continuous_on s (\<lambda>x. (f x) powr (g x))" |
2537 shows "continuous_on s (\<lambda>x. (f x) powr (g x))" |
2538 using assms unfolding continuous_on_def by (fast intro: tendsto_powr) |
2538 using assms unfolding continuous_on_def by (fast intro: tendsto_powr) |
2539 |
2539 |
2540 lemma tendsto_powr2: |
2540 lemma tendsto_powr2: |
2541 fixes a::real |
2541 fixes a::real |
2542 assumes f: "(f ---> a) F" and g: "(g ---> b) F" and f_nonneg: "\<forall>\<^sub>F x in F. 0 \<le> f x" and b: "0 < b" |
2542 assumes f: "(f \<longlongrightarrow> a) F" and g: "(g \<longlongrightarrow> b) F" and f_nonneg: "\<forall>\<^sub>F x in F. 0 \<le> f x" and b: "0 < b" |
2543 shows "((\<lambda>x. f x powr g x) ---> a powr b) F" |
2543 shows "((\<lambda>x. f x powr g x) \<longlongrightarrow> a powr b) F" |
2544 unfolding powr_def |
2544 unfolding powr_def |
2545 proof (rule filterlim_If) |
2545 proof (rule filterlim_If) |
2546 from f show "((\<lambda>x. 0) ---> (if a = 0 then 0 else exp (b * ln a))) (inf F (principal {x. f x = 0}))" |
2546 from f show "((\<lambda>x. 0) \<longlongrightarrow> (if a = 0 then 0 else exp (b * ln a))) (inf F (principal {x. f x = 0}))" |
2547 by simp (auto simp: filterlim_iff eventually_inf_principal elim: eventually_mono dest: t1_space_nhds) |
2547 by simp (auto simp: filterlim_iff eventually_inf_principal elim: eventually_mono dest: t1_space_nhds) |
2548 next |
2548 next |
2549 { assume "a = 0" |
2549 { assume "a = 0" |
2550 with f f_nonneg have "LIM x inf F (principal {x. f x \<noteq> 0}). f x :> at_right 0" |
2550 with f f_nonneg have "LIM x inf F (principal {x. f x \<noteq> 0}). f x :> at_right 0" |
2551 by (auto simp add: filterlim_at eventually_inf_principal le_less |
2551 by (auto simp add: filterlim_at eventually_inf_principal le_less |
2552 elim: eventually_mono intro: tendsto_mono inf_le1) |
2552 elim: eventually_mono intro: tendsto_mono inf_le1) |
2553 then have "((\<lambda>x. exp (g x * ln (f x))) ---> 0) (inf F (principal {x. f x \<noteq> 0}))" |
2553 then have "((\<lambda>x. exp (g x * ln (f x))) \<longlongrightarrow> 0) (inf F (principal {x. f x \<noteq> 0}))" |
2554 by (auto intro!: filterlim_compose[OF exp_at_bot] filterlim_compose[OF ln_at_0] |
2554 by (auto intro!: filterlim_compose[OF exp_at_bot] filterlim_compose[OF ln_at_0] |
2555 filterlim_tendsto_pos_mult_at_bot[OF _ \<open>0 < b\<close>] |
2555 filterlim_tendsto_pos_mult_at_bot[OF _ \<open>0 < b\<close>] |
2556 intro: tendsto_mono inf_le1 g) } |
2556 intro: tendsto_mono inf_le1 g) } |
2557 then show "((\<lambda>x. exp (g x * ln (f x))) ---> (if a = 0 then 0 else exp (b * ln a))) (inf F (principal {x. f x \<noteq> 0}))" |
2557 then show "((\<lambda>x. exp (g x * ln (f x))) \<longlongrightarrow> (if a = 0 then 0 else exp (b * ln a))) (inf F (principal {x. f x \<noteq> 0}))" |
2558 using f g by (auto intro!: tendsto_intros intro: tendsto_mono inf_le1) |
2558 using f g by (auto intro!: tendsto_intros intro: tendsto_mono inf_le1) |
2559 qed |
2559 qed |
2560 |
2560 |
2561 lemma DERIV_powr: |
2561 lemma DERIV_powr: |
2562 fixes r::real |
2562 fixes r::real |
2594 qed |
2594 qed |
2595 |
2595 |
2596 declare has_real_derivative_powr[THEN DERIV_chain2, derivative_intros] |
2596 declare has_real_derivative_powr[THEN DERIV_chain2, derivative_intros] |
2597 |
2597 |
2598 lemma tendsto_zero_powrI: |
2598 lemma tendsto_zero_powrI: |
2599 assumes "(f ---> (0::real)) F" "(g ---> b) F" "\<forall>\<^sub>F x in F. 0 \<le> f x" "0 < b" |
2599 assumes "(f \<longlongrightarrow> (0::real)) F" "(g \<longlongrightarrow> b) F" "\<forall>\<^sub>F x in F. 0 \<le> f x" "0 < b" |
2600 shows "((\<lambda>x. f x powr g x) ---> 0) F" |
2600 shows "((\<lambda>x. f x powr g x) \<longlongrightarrow> 0) F" |
2601 using tendsto_powr2[OF assms] by simp |
2601 using tendsto_powr2[OF assms] by simp |
2602 |
2602 |
2603 lemma tendsto_neg_powr: |
2603 lemma tendsto_neg_powr: |
2604 assumes "s < 0" |
2604 assumes "s < 0" |
2605 and f: "LIM x F. f x :> at_top" |
2605 and f: "LIM x F. f x :> at_top" |
2606 shows "((\<lambda>x. f x powr s) ---> (0::real)) F" |
2606 shows "((\<lambda>x. f x powr s) \<longlongrightarrow> (0::real)) F" |
2607 proof - |
2607 proof - |
2608 have "((\<lambda>x. exp (s * ln (f x))) ---> (0::real)) F" (is "?X") |
2608 have "((\<lambda>x. exp (s * ln (f x))) \<longlongrightarrow> (0::real)) F" (is "?X") |
2609 by (auto intro!: filterlim_compose[OF exp_at_bot] filterlim_compose[OF ln_at_top] |
2609 by (auto intro!: filterlim_compose[OF exp_at_bot] filterlim_compose[OF ln_at_top] |
2610 filterlim_tendsto_neg_mult_at_bot assms) |
2610 filterlim_tendsto_neg_mult_at_bot assms) |
2611 also have "?X \<longleftrightarrow> ((\<lambda>x. f x powr s) ---> (0::real)) F" |
2611 also have "?X \<longleftrightarrow> ((\<lambda>x. f x powr s) \<longlongrightarrow> (0::real)) F" |
2612 using f filterlim_at_top_dense[of f F] |
2612 using f filterlim_at_top_dense[of f F] |
2613 by (intro filterlim_cong[OF refl refl]) (auto simp: neq_iff powr_def elim: eventually_mono) |
2613 by (intro filterlim_cong[OF refl refl]) (auto simp: neq_iff powr_def elim: eventually_mono) |
2614 finally show ?thesis . |
2614 finally show ?thesis . |
2615 qed |
2615 qed |
2616 |
2616 |
2617 lemma tendsto_exp_limit_at_right: |
2617 lemma tendsto_exp_limit_at_right: |
2618 fixes x :: real |
2618 fixes x :: real |
2619 shows "((\<lambda>y. (1 + x * y) powr (1 / y)) ---> exp x) (at_right 0)" |
2619 shows "((\<lambda>y. (1 + x * y) powr (1 / y)) \<longlongrightarrow> exp x) (at_right 0)" |
2620 proof cases |
2620 proof cases |
2621 assume "x \<noteq> 0" |
2621 assume "x \<noteq> 0" |
2622 have "((\<lambda>y. ln (1 + x * y)::real) has_real_derivative 1 * x) (at 0)" |
2622 have "((\<lambda>y. ln (1 + x * y)::real) has_real_derivative 1 * x) (at 0)" |
2623 by (auto intro!: derivative_eq_intros) |
2623 by (auto intro!: derivative_eq_intros) |
2624 then have "((\<lambda>y. ln (1 + x * y) / y) ---> x) (at 0)" |
2624 then have "((\<lambda>y. ln (1 + x * y) / y) \<longlongrightarrow> x) (at 0)" |
2625 by (auto simp add: has_field_derivative_def field_has_derivative_at) |
2625 by (auto simp add: has_field_derivative_def field_has_derivative_at) |
2626 then have *: "((\<lambda>y. exp (ln (1 + x * y) / y)) ---> exp x) (at 0)" |
2626 then have *: "((\<lambda>y. exp (ln (1 + x * y) / y)) \<longlongrightarrow> exp x) (at 0)" |
2627 by (rule tendsto_intros) |
2627 by (rule tendsto_intros) |
2628 then show ?thesis |
2628 then show ?thesis |
2629 proof (rule filterlim_mono_eventually) |
2629 proof (rule filterlim_mono_eventually) |
2630 show "eventually (\<lambda>xa. exp (ln (1 + x * xa) / xa) = (1 + x * xa) powr (1 / xa)) (at_right 0)" |
2630 show "eventually (\<lambda>xa. exp (ln (1 + x * xa) / xa) = (1 + x * xa) powr (1 / xa)) (at_right 0)" |
2631 unfolding eventually_at_right[OF zero_less_one] |
2631 unfolding eventually_at_right[OF zero_less_one] |
2817 shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. cos (f x)) a" |
2817 shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. cos (f x)) a" |
2818 by (rule isCont_o2 [OF _ isCont_cos]) |
2818 by (rule isCont_o2 [OF _ isCont_cos]) |
2819 |
2819 |
2820 lemma tendsto_sin [tendsto_intros]: |
2820 lemma tendsto_sin [tendsto_intros]: |
2821 fixes f:: "_ \<Rightarrow> 'a::{real_normed_field,banach}" |
2821 fixes f:: "_ \<Rightarrow> 'a::{real_normed_field,banach}" |
2822 shows "(f ---> a) F \<Longrightarrow> ((\<lambda>x. sin (f x)) ---> sin a) F" |
2822 shows "(f \<longlongrightarrow> a) F \<Longrightarrow> ((\<lambda>x. sin (f x)) \<longlongrightarrow> sin a) F" |
2823 by (rule isCont_tendsto_compose [OF isCont_sin]) |
2823 by (rule isCont_tendsto_compose [OF isCont_sin]) |
2824 |
2824 |
2825 lemma tendsto_cos [tendsto_intros]: |
2825 lemma tendsto_cos [tendsto_intros]: |
2826 fixes f:: "_ \<Rightarrow> 'a::{real_normed_field,banach}" |
2826 fixes f:: "_ \<Rightarrow> 'a::{real_normed_field,banach}" |
2827 shows "(f ---> a) F \<Longrightarrow> ((\<lambda>x. cos (f x)) ---> cos a) F" |
2827 shows "(f \<longlongrightarrow> a) F \<Longrightarrow> ((\<lambda>x. cos (f x)) \<longlongrightarrow> cos a) F" |
2828 by (rule isCont_tendsto_compose [OF isCont_cos]) |
2828 by (rule isCont_tendsto_compose [OF isCont_cos]) |
2829 |
2829 |
2830 lemma continuous_sin [continuous_intros]: |
2830 lemma continuous_sin [continuous_intros]: |
2831 fixes f:: "_ \<Rightarrow> 'a::{real_normed_field,banach}" |
2831 fixes f:: "_ \<Rightarrow> 'a::{real_normed_field,banach}" |
2832 shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. sin (f x))" |
2832 shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. sin (f x))" |
4047 shows "\<lbrakk>isCont f a; cos (f a) \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. tan (f x)) a" |
4047 shows "\<lbrakk>isCont f a; cos (f a) \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. tan (f x)) a" |
4048 by (rule isCont_o2 [OF _ isCont_tan]) |
4048 by (rule isCont_o2 [OF _ isCont_tan]) |
4049 |
4049 |
4050 lemma tendsto_tan [tendsto_intros]: |
4050 lemma tendsto_tan [tendsto_intros]: |
4051 fixes f :: "'a \<Rightarrow> 'a::{real_normed_field,banach}" |
4051 fixes f :: "'a \<Rightarrow> 'a::{real_normed_field,banach}" |
4052 shows "\<lbrakk>(f ---> a) F; cos a \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. tan (f x)) ---> tan a) F" |
4052 shows "\<lbrakk>(f \<longlongrightarrow> a) F; cos a \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. tan (f x)) \<longlongrightarrow> tan a) F" |
4053 by (rule isCont_tendsto_compose [OF isCont_tan]) |
4053 by (rule isCont_tendsto_compose [OF isCont_tan]) |
4054 |
4054 |
4055 lemma continuous_tan: |
4055 lemma continuous_tan: |
4056 fixes f :: "'a \<Rightarrow> 'a::{real_normed_field,banach}" |
4056 fixes f :: "'a \<Rightarrow> 'a::{real_normed_field,banach}" |
4057 shows "continuous F f \<Longrightarrow> cos (f (Lim F (\<lambda>x. x))) \<noteq> 0 \<Longrightarrow> continuous F (\<lambda>x. tan (f x))" |
4057 shows "continuous F f \<Longrightarrow> cos (f (Lim F (\<lambda>x. x))) \<noteq> 0 \<Longrightarrow> continuous F (\<lambda>x. tan (f x))" |
4316 shows "\<lbrakk>isCont f a; sin (f a) \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. cot (f x)) a" |
4316 shows "\<lbrakk>isCont f a; sin (f a) \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. cot (f x)) a" |
4317 by (rule isCont_o2 [OF _ isCont_cot]) |
4317 by (rule isCont_o2 [OF _ isCont_cot]) |
4318 |
4318 |
4319 lemma tendsto_cot [tendsto_intros]: |
4319 lemma tendsto_cot [tendsto_intros]: |
4320 fixes f :: "'a \<Rightarrow> 'a::{real_normed_field,banach}" |
4320 fixes f :: "'a \<Rightarrow> 'a::{real_normed_field,banach}" |
4321 shows "\<lbrakk>(f ---> a) F; sin a \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. cot (f x)) ---> cot a) F" |
4321 shows "\<lbrakk>(f \<longlongrightarrow> a) F; sin a \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. cot (f x)) \<longlongrightarrow> cot a) F" |
4322 by (rule isCont_tendsto_compose [OF isCont_cot]) |
4322 by (rule isCont_tendsto_compose [OF isCont_cot]) |
4323 |
4323 |
4324 lemma continuous_cot: |
4324 lemma continuous_cot: |
4325 fixes f :: "'a \<Rightarrow> 'a::{real_normed_field,banach}" |
4325 fixes f :: "'a \<Rightarrow> 'a::{real_normed_field,banach}" |
4326 shows "continuous F f \<Longrightarrow> sin (f (Lim F (\<lambda>x. x))) \<noteq> 0 \<Longrightarrow> continuous F (\<lambda>x. cot (f x))" |
4326 shows "continuous F f \<Longrightarrow> sin (f (Lim F (\<lambda>x. x))) \<noteq> 0 \<Longrightarrow> continuous F (\<lambda>x. cot (f x))" |
4629 apply (erule (1) isCont_inverse_function2 [where f=tan]) |
4629 apply (erule (1) isCont_inverse_function2 [where f=tan]) |
4630 apply (metis arctan_tan order_le_less_trans order_less_le_trans) |
4630 apply (metis arctan_tan order_le_less_trans order_less_le_trans) |
4631 apply (metis cos_gt_zero_pi isCont_tan order_less_le_trans less_le) |
4631 apply (metis cos_gt_zero_pi isCont_tan order_less_le_trans less_le) |
4632 done |
4632 done |
4633 |
4633 |
4634 lemma tendsto_arctan [tendsto_intros]: "(f ---> x) F \<Longrightarrow> ((\<lambda>x. arctan (f x)) ---> arctan x) F" |
4634 lemma tendsto_arctan [tendsto_intros]: "(f \<longlongrightarrow> x) F \<Longrightarrow> ((\<lambda>x. arctan (f x)) \<longlongrightarrow> arctan x) F" |
4635 by (rule isCont_tendsto_compose [OF isCont_arctan]) |
4635 by (rule isCont_tendsto_compose [OF isCont_arctan]) |
4636 |
4636 |
4637 lemma continuous_arctan [continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. arctan (f x))" |
4637 lemma continuous_arctan [continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. arctan (f x))" |
4638 unfolding continuous_def by (rule tendsto_arctan) |
4638 unfolding continuous_def by (rule tendsto_arctan) |
4639 |
4639 |
4688 lemma filterlim_tan_at_left: "filterlim tan at_top (at_left (pi/2))" |
4688 lemma filterlim_tan_at_left: "filterlim tan at_top (at_left (pi/2))" |
4689 by (rule filterlim_at_top_at_left[where Q="\<lambda>x. - pi/2 < x \<and> x < pi/2" and P="\<lambda>x. True" and g=arctan]) |
4689 by (rule filterlim_at_top_at_left[where Q="\<lambda>x. - pi/2 < x \<and> x < pi/2" and P="\<lambda>x. True" and g=arctan]) |
4690 (auto simp: arctan le_less eventually_at dist_real_def simp del: less_divide_eq_numeral1 |
4690 (auto simp: arctan le_less eventually_at dist_real_def simp del: less_divide_eq_numeral1 |
4691 intro!: tan_monotone exI[of _ "pi/2"]) |
4691 intro!: tan_monotone exI[of _ "pi/2"]) |
4692 |
4692 |
4693 lemma tendsto_arctan_at_top: "(arctan ---> (pi/2)) at_top" |
4693 lemma tendsto_arctan_at_top: "(arctan \<longlongrightarrow> (pi/2)) at_top" |
4694 proof (rule tendstoI) |
4694 proof (rule tendstoI) |
4695 fix e :: real |
4695 fix e :: real |
4696 assume "0 < e" |
4696 assume "0 < e" |
4697 def y \<equiv> "pi/2 - min (pi/2) e" |
4697 def y \<equiv> "pi/2 - min (pi/2) e" |
4698 then have y: "0 \<le> y" "y < pi/2" "pi/2 \<le> e + y" |
4698 then have y: "0 \<le> y" "y < pi/2" "pi/2 \<le> e + y" |
4710 show "dist (arctan x) (pi / 2) < e" |
4710 show "dist (arctan x) (pi / 2) < e" |
4711 by (simp add: dist_real_def) |
4711 by (simp add: dist_real_def) |
4712 qed |
4712 qed |
4713 qed |
4713 qed |
4714 |
4714 |
4715 lemma tendsto_arctan_at_bot: "(arctan ---> - (pi/2)) at_bot" |
4715 lemma tendsto_arctan_at_bot: "(arctan \<longlongrightarrow> - (pi/2)) at_bot" |
4716 unfolding filterlim_at_bot_mirror arctan_minus |
4716 unfolding filterlim_at_bot_mirror arctan_minus |
4717 by (intro tendsto_minus tendsto_arctan_at_top) |
4717 by (intro tendsto_minus tendsto_arctan_at_top) |
4718 |
4718 |
4719 |
4719 |
4720 subsection\<open>Prove Totality of the Trigonometric Functions\<close> |
4720 subsection\<open>Prove Totality of the Trigonometric Functions\<close> |