1028 assumes "continuous (at a within s) f" |
1028 assumes "continuous (at a within s) f" |
1029 and "f a \<noteq> 0" |
1029 and "f a \<noteq> 0" |
1030 shows "continuous (at a within s) (\<lambda>x. inverse (f x))" |
1030 shows "continuous (at a within s) (\<lambda>x. inverse (f x))" |
1031 using assms unfolding continuous_within by (rule tendsto_inverse) |
1031 using assms unfolding continuous_within by (rule tendsto_inverse) |
1032 |
1032 |
1033 lemma continuous_at_inverse[continuous_intros, simp]: |
|
1034 fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_div_algebra" |
|
1035 assumes "isCont f a" |
|
1036 and "f a \<noteq> 0" |
|
1037 shows "isCont (\<lambda>x. inverse (f x)) a" |
|
1038 using assms unfolding continuous_at by (rule tendsto_inverse) |
|
1039 |
|
1040 lemma continuous_on_inverse[continuous_intros]: |
1033 lemma continuous_on_inverse[continuous_intros]: |
1041 fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_div_algebra" |
1034 fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_div_algebra" |
1042 assumes "continuous_on s f" |
1035 assumes "continuous_on s f" |
1043 and "\<forall>x\<in>s. f x \<noteq> 0" |
1036 and "\<forall>x\<in>s. f x \<noteq> 0" |
1044 shows "continuous_on s (\<lambda>x. inverse (f x))" |
1037 shows "continuous_on s (\<lambda>x. inverse (f x))" |
1133 fixes F |
1126 fixes F |
1134 assumes "filterlim f at_infinity F" |
1127 assumes "filterlim f at_infinity F" |
1135 shows "filterlim (\<lambda>x. norm (f x)) at_top F" |
1128 shows "filterlim (\<lambda>x. norm (f x)) at_top F" |
1136 proof - |
1129 proof - |
1137 { |
1130 { |
1138 fix r :: real |
1131 fix r :: real |
1139 have "\<forall>\<^sub>F x in F. r \<le> norm (f x)" using filterlim_at_infinity[of 0 f F] assms |
1132 have "\<forall>\<^sub>F x in F. r \<le> norm (f x)" using filterlim_at_infinity[of 0 f F] assms |
1140 by (cases "r > 0") |
1133 by (cases "r > 0") |
1141 (auto simp: not_less intro: always_eventually order.trans[OF _ norm_ge_zero]) |
1134 (auto simp: not_less intro: always_eventually order.trans[OF _ norm_ge_zero]) |
1142 } |
1135 } |
1143 thus ?thesis by (auto simp: filterlim_at_top) |
1136 thus ?thesis by (auto simp: filterlim_at_top) |
1144 qed |
1137 qed |
1145 |
1138 |
1146 lemma filterlim_norm_at_top_imp_at_infinity: |
1139 lemma filterlim_norm_at_top_imp_at_infinity: |
1147 fixes F |
1140 fixes F |
1148 assumes "filterlim (\<lambda>x. norm (f x)) at_top F" |
1141 assumes "filterlim (\<lambda>x. norm (f x)) at_top F" |
1149 shows "filterlim f at_infinity F" |
1142 shows "filterlim f at_infinity F" |
1150 using filterlim_at_infinity[of 0 f F] assms by (auto simp: filterlim_at_top) |
1143 using filterlim_at_infinity[of 0 f F] assms by (auto simp: filterlim_at_top) |
1201 qed (simp_all add: filterlim_ident) |
1194 qed (simp_all add: filterlim_ident) |
1202 |
1195 |
1203 lemma filterlim_of_real_at_infinity [tendsto_intros]: |
1196 lemma filterlim_of_real_at_infinity [tendsto_intros]: |
1204 "filterlim (of_real :: real \<Rightarrow> 'a :: real_normed_algebra_1) at_infinity at_top" |
1197 "filterlim (of_real :: real \<Rightarrow> 'a :: real_normed_algebra_1) at_infinity at_top" |
1205 by (intro filterlim_norm_at_top_imp_at_infinity) (auto simp: filterlim_abs_real) |
1198 by (intro filterlim_norm_at_top_imp_at_infinity) (auto simp: filterlim_abs_real) |
1206 |
1199 |
1207 lemma not_tendsto_and_filterlim_at_infinity: |
1200 lemma not_tendsto_and_filterlim_at_infinity: |
1208 fixes c :: "'a::real_normed_vector" |
1201 fixes c :: "'a::real_normed_vector" |
1209 assumes "F \<noteq> bot" |
1202 assumes "F \<noteq> bot" |
1210 and "(f \<longlongrightarrow> c) F" |
1203 and "(f \<longlongrightarrow> c) F" |
1211 and "filterlim f at_infinity F" |
1204 and "filterlim f at_infinity F" |
1345 |
1338 |
1346 lemma filterlim_uminus_at_bot_at_top: "LIM x at_top. - x :: real :> at_bot" |
1339 lemma filterlim_uminus_at_bot_at_top: "LIM x at_top. - x :: real :> at_bot" |
1347 unfolding filterlim_at_bot eventually_at_top_dense |
1340 unfolding filterlim_at_bot eventually_at_top_dense |
1348 by (metis leI less_minus_iff order_less_asym) |
1341 by (metis leI less_minus_iff order_less_asym) |
1349 |
1342 |
1350 lemma at_bot_mirror : |
1343 lemma at_bot_mirror : |
1351 shows "(at_bot::('a::{ordered_ab_group_add,linorder} filter)) = filtermap uminus at_top" |
1344 shows "(at_bot::('a::{ordered_ab_group_add,linorder} filter)) = filtermap uminus at_top" |
1352 apply (rule filtermap_fun_inverse[of uminus, symmetric]) |
1345 apply (rule filtermap_fun_inverse[of uminus, symmetric]) |
1353 subgoal unfolding filterlim_at_top eventually_at_bot_linorder using le_minus_iff by auto |
1346 subgoal unfolding filterlim_at_top eventually_at_bot_linorder using le_minus_iff by auto |
1354 subgoal unfolding filterlim_at_bot eventually_at_top_linorder using minus_le_iff by auto |
1347 subgoal unfolding filterlim_at_bot eventually_at_top_linorder using minus_le_iff by auto |
1355 by auto |
1348 by auto |
1356 |
1349 |
1357 lemma at_top_mirror : |
1350 lemma at_top_mirror : |
1358 shows "(at_top::('a::{ordered_ab_group_add,linorder} filter)) = filtermap uminus at_bot" |
1351 shows "(at_top::('a::{ordered_ab_group_add,linorder} filter)) = filtermap uminus at_bot" |
1359 apply (subst at_bot_mirror) |
1352 apply (subst at_bot_mirror) |
1360 by (auto simp add: filtermap_filtermap) |
1353 by (auto simp add: filtermap_filtermap) |
1361 |
1354 |
1362 lemma filterlim_at_top_mirror: "(LIM x at_top. f x :> F) \<longleftrightarrow> (LIM x at_bot. f (-x::real) :> F)" |
1355 lemma filterlim_at_top_mirror: "(LIM x at_top. f x :> F) \<longleftrightarrow> (LIM x at_bot. f (-x::real) :> F)" |
1363 unfolding filterlim_def at_top_mirror filtermap_filtermap .. |
1356 unfolding filterlim_def at_top_mirror filtermap_filtermap .. |
1551 unfolding filterlim_at |
1544 unfolding filterlim_at |
1552 using assms |
1545 using assms |
1553 by (auto intro: filterlim_at_infinity_imp_eventually_ne tendsto_imp_eventually_ne eventually_conj) |
1546 by (auto intro: filterlim_at_infinity_imp_eventually_ne tendsto_imp_eventually_ne eventually_conj) |
1554 then show ?thesis |
1547 then show ?thesis |
1555 by (subst filterlim_inverse_at_iff[symmetric]) simp_all |
1548 by (subst filterlim_inverse_at_iff[symmetric]) simp_all |
1556 qed |
1549 qed |
1557 |
1550 |
1558 lemma tendsto_inverse_0_at_top: "LIM x F. f x :> at_top \<Longrightarrow> ((\<lambda>x. inverse (f x) :: real) \<longlongrightarrow> 0) F" |
1551 lemma tendsto_inverse_0_at_top: "LIM x F. f x :> at_top \<Longrightarrow> ((\<lambda>x. inverse (f x) :: real) \<longlongrightarrow> 0) F" |
1559 by (metis filterlim_at filterlim_mono[OF _ at_top_le_at_infinity order_refl] filterlim_inverse_at_iff) |
1552 by (metis filterlim_at filterlim_mono[OF _ at_top_le_at_infinity order_refl] filterlim_inverse_at_iff) |
1560 |
1553 |
1561 lemma real_tendsto_divide_at_top: |
1554 lemma real_tendsto_divide_at_top: |
1732 lemma filterlim_power_at_infinity [tendsto_intros]: |
1725 lemma filterlim_power_at_infinity [tendsto_intros]: |
1733 fixes F and f :: "'a \<Rightarrow> 'b :: real_normed_div_algebra" |
1726 fixes F and f :: "'a \<Rightarrow> 'b :: real_normed_div_algebra" |
1734 assumes "filterlim f at_infinity F" "n > 0" |
1727 assumes "filterlim f at_infinity F" "n > 0" |
1735 shows "filterlim (\<lambda>x. f x ^ n) at_infinity F" |
1728 shows "filterlim (\<lambda>x. f x ^ n) at_infinity F" |
1736 by (rule filterlim_norm_at_top_imp_at_infinity) |
1729 by (rule filterlim_norm_at_top_imp_at_infinity) |
1737 (auto simp: norm_power intro!: filterlim_pow_at_top assms |
1730 (auto simp: norm_power intro!: filterlim_pow_at_top assms |
1738 intro: filterlim_at_infinity_imp_norm_at_top) |
1731 intro: filterlim_at_infinity_imp_norm_at_top) |
1739 |
1732 |
1740 lemma filterlim_tendsto_add_at_top: |
1733 lemma filterlim_tendsto_add_at_top: |
1741 assumes f: "(f \<longlongrightarrow> c) F" |
1734 assumes f: "(f \<longlongrightarrow> c) F" |
1742 and g: "LIM x F. g x :> at_top" |
1735 and g: "LIM x F. g x :> at_top" |
2558 using assms |
2551 using assms |
2559 unfolding uniformly_continuous_on_def by (meson Cauchy_def) |
2552 unfolding uniformly_continuous_on_def by (meson Cauchy_def) |
2560 |
2553 |
2561 lemma isUCont_Cauchy: "isUCont f \<Longrightarrow> Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. f (X n))" |
2554 lemma isUCont_Cauchy: "isUCont f \<Longrightarrow> Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. f (X n))" |
2562 by (rule uniformly_continuous_on_Cauchy[where S=UNIV and f=f]) simp_all |
2555 by (rule uniformly_continuous_on_Cauchy[where S=UNIV and f=f]) simp_all |
2563 |
2556 |
2564 lemma uniformly_continuous_imp_Cauchy_continuous: |
2557 lemma uniformly_continuous_imp_Cauchy_continuous: |
2565 fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" |
2558 fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" |
2566 shows "\<lbrakk>uniformly_continuous_on S f; Cauchy \<sigma>; \<And>n. (\<sigma> n) \<in> S\<rbrakk> \<Longrightarrow> Cauchy(f \<circ> \<sigma>)" |
2559 shows "\<lbrakk>uniformly_continuous_on S f; Cauchy \<sigma>; \<And>n. (\<sigma> n) \<in> S\<rbrakk> \<Longrightarrow> Cauchy(f \<circ> \<sigma>)" |
2567 by (simp add: uniformly_continuous_on_def Cauchy_def) meson |
2560 by (simp add: uniformly_continuous_on_def Cauchy_def) meson |
2568 |
2561 |
2822 text \<open>Continuity of inverse function.\<close> |
2815 text \<open>Continuity of inverse function.\<close> |
2823 |
2816 |
2824 lemma isCont_inverse_function: |
2817 lemma isCont_inverse_function: |
2825 fixes f g :: "real \<Rightarrow> real" |
2818 fixes f g :: "real \<Rightarrow> real" |
2826 assumes d: "0 < d" |
2819 assumes d: "0 < d" |
2827 and inj: "\<forall>z. \<bar>z-x\<bar> \<le> d \<longrightarrow> g (f z) = z" |
2820 and inj: "\<And>z. \<bar>z-x\<bar> \<le> d \<Longrightarrow> g (f z) = z" |
2828 and cont: "\<forall>z. \<bar>z-x\<bar> \<le> d \<longrightarrow> isCont f z" |
2821 and cont: "\<And>z. \<bar>z-x\<bar> \<le> d \<Longrightarrow> isCont f z" |
2829 shows "isCont g (f x)" |
2822 shows "isCont g (f x)" |
2830 proof - |
2823 proof - |
2831 let ?A = "f (x - d)" |
2824 let ?A = "f (x - d)" |
2832 let ?B = "f (x + d)" |
2825 let ?B = "f (x + d)" |
2833 let ?D = "{x - d..x + d}" |
2826 let ?D = "{x - d..x + d}" |
2852 qed |
2845 qed |
2853 |
2846 |
2854 lemma isCont_inverse_function2: |
2847 lemma isCont_inverse_function2: |
2855 fixes f g :: "real \<Rightarrow> real" |
2848 fixes f g :: "real \<Rightarrow> real" |
2856 shows |
2849 shows |
2857 "a < x \<Longrightarrow> x < b \<Longrightarrow> |
2850 "\<lbrakk>a < x; x < b; |
2858 \<forall>z. a \<le> z \<and> z \<le> b \<longrightarrow> g (f z) = z \<Longrightarrow> |
2851 \<And>z. \<lbrakk>a \<le> z; z \<le> b\<rbrakk> \<Longrightarrow> g (f z) = z; |
2859 \<forall>z. a \<le> z \<and> z \<le> b \<longrightarrow> isCont f z \<Longrightarrow> isCont g (f x)" |
2852 \<And>z. \<lbrakk>a \<le> z; z \<le> b\<rbrakk> \<Longrightarrow> isCont f z\<rbrakk> \<Longrightarrow> isCont g (f x)" |
2860 apply (rule isCont_inverse_function [where f=f and d="min (x - a) (b - x)"]) |
2853 apply (rule isCont_inverse_function [where f=f and d="min (x - a) (b - x)"]) |
2861 apply (simp_all add: abs_le_iff) |
2854 apply (simp_all add: abs_le_iff) |
2862 done |
2855 done |
2863 |
|
2864 (* need to rename second continuous_at_inverse *) |
|
2865 lemma isCont_inv_fun: |
|
2866 fixes f g :: "real \<Rightarrow> real" |
|
2867 shows "0 < d \<Longrightarrow> (\<forall>z. \<bar>z - x\<bar> \<le> d \<longrightarrow> g (f z) = z) \<Longrightarrow> |
|
2868 \<forall>z. \<bar>z - x\<bar> \<le> d \<longrightarrow> isCont f z \<Longrightarrow> isCont g (f x)" |
|
2869 by (rule isCont_inverse_function) |
|
2870 |
2856 |
2871 text \<open>Bartle/Sherbert: Introduction to Real Analysis, Theorem 4.2.9, p. 110.\<close> |
2857 text \<open>Bartle/Sherbert: Introduction to Real Analysis, Theorem 4.2.9, p. 110.\<close> |
2872 lemma LIM_fun_gt_zero: "f \<midarrow>c\<rightarrow> l \<Longrightarrow> 0 < l \<Longrightarrow> \<exists>r. 0 < r \<and> (\<forall>x. x \<noteq> c \<and> \<bar>c - x\<bar> < r \<longrightarrow> 0 < f x)" |
2858 lemma LIM_fun_gt_zero: "f \<midarrow>c\<rightarrow> l \<Longrightarrow> 0 < l \<Longrightarrow> \<exists>r. 0 < r \<and> (\<forall>x. x \<noteq> c \<and> \<bar>c - x\<bar> < r \<longrightarrow> 0 < f x)" |
2873 for f :: "real \<Rightarrow> real" |
2859 for f :: "real \<Rightarrow> real" |
2874 apply (drule (1) LIM_D) |
2860 apply (drule (1) LIM_D) |