Cauchy's integral formula for circles. Starting to fix eventually_mono.
--- a/src/HOL/Filter.thy Mon Dec 07 10:38:04 2015 +0100
+++ b/src/HOL/Filter.thy Mon Dec 07 16:44:26 2015 +0000
@@ -71,6 +71,11 @@
unfolding eventually_def
by (rule is_filter.mono [OF is_filter_Rep_filter])
+lemma eventually_mono':
+ "\<lbrakk>eventually P F; \<And>x. P x \<Longrightarrow> Q x\<rbrakk> \<Longrightarrow> eventually Q F"
+ unfolding eventually_def
+ by (blast intro: is_filter.mono [OF is_filter_Rep_filter])
+
lemma eventually_conj:
assumes P: "eventually (\<lambda>x. P x) F"
assumes Q: "eventually (\<lambda>x. Q x) F"
@@ -82,10 +87,11 @@
assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
assumes "eventually (\<lambda>x. P x) F"
shows "eventually (\<lambda>x. Q x) F"
-proof (rule eventually_mono)
- show "\<forall>x. (P x \<longrightarrow> Q x) \<and> P x \<longrightarrow> Q x" by simp
- show "eventually (\<lambda>x. (P x \<longrightarrow> Q x) \<and> P x) F"
+proof -
+ have "eventually (\<lambda>x. (P x \<longrightarrow> Q x) \<and> P x) F"
using assms by (rule eventually_conj)
+ then show ?thesis
+ by (blast intro: eventually_mono')
qed
lemma eventually_rev_mp:
@@ -172,7 +178,7 @@
lemma frequently_mp:
assumes ev: "\<forall>\<^sub>Fx in F. P x \<longrightarrow> Q x" and P: "\<exists>\<^sub>Fx in F. P x" shows "\<exists>\<^sub>Fx in F. Q x"
-proof -
+proof -
from ev have "eventually (\<lambda>x. \<not> Q x \<longrightarrow> \<not> P x) F"
by (rule eventually_rev_mp) (auto intro!: always_eventually)
from eventually_mp[OF this] P show ?thesis
@@ -225,7 +231,7 @@
"(\<forall>\<^sub>Fx in F. C \<longrightarrow> P x) \<longleftrightarrow> (C \<longrightarrow> (\<forall>\<^sub>Fx in F. P x))"
by (cases C; simp add: not_frequently)+
-lemmas eventually_frequently_simps =
+lemmas eventually_frequently_simps =
eventually_frequently_const_simps
not_eventually
eventually_conj_iff
@@ -340,7 +346,7 @@
unfolding le_filter_def eventually_inf by (auto intro: eventually_True) }
{ assume "F \<le> F'" and "F \<le> F''" thus "F \<le> inf F' F''"
unfolding le_filter_def eventually_inf
- by (auto elim!: eventually_mono intro: eventually_conj) }
+ by (auto intro: eventually_mono' [OF eventually_conj]) }
{ show "F \<le> sup F F'" and "F' \<le> sup F F'"
unfolding le_filter_def eventually_sup by simp_all }
{ assume "F \<le> F''" and "F' \<le> F''" thus "sup F F' \<le> F''"
@@ -404,10 +410,13 @@
lemma trivial_limit_def: "trivial_limit F \<longleftrightarrow> eventually (\<lambda>x. False) F"
by (rule eventually_False [symmetric])
+lemma False_imp_not_eventually: "(\<forall>x. \<not> P x ) \<Longrightarrow> \<not> trivial_limit net \<Longrightarrow> \<not> eventually (\<lambda>x. P x) net"
+ by (simp add: eventually_False)
+
lemma eventually_Inf: "eventually P (Inf B) \<longleftrightarrow> (\<exists>X\<subseteq>B. finite X \<and> eventually P (Inf X))"
proof -
let ?F = "\<lambda>P. \<exists>X\<subseteq>B. finite X \<and> eventually P (Inf X)"
-
+
{ fix P have "eventually P (Abs_filter ?F) \<longleftrightarrow> ?F P"
proof (rule eventually_Abs_filter is_filter.intro)+
show "?F (\<lambda>x. True)"
@@ -605,7 +614,7 @@
have "eventually P (INF k. principal {k <..}) \<longleftrightarrow> (\<exists>N::'a. \<forall>n>N. P n)"
by (subst eventually_INF_base) (auto simp: eventually_principal intro: max.cobounded1 max.cobounded2)
also have "(INF k. principal {k::'a <..}) = at_top"
- unfolding at_top_def
+ unfolding at_top_def
by (intro INF_eq) (auto intro: less_imp_le simp: Ici_subset_Ioi_iff gt_ex)
finally show ?thesis .
qed
@@ -645,7 +654,7 @@
have "eventually P (INF k. principal {..< k}) \<longleftrightarrow> (\<exists>N::'a. \<forall>n<N. P n)"
by (subst eventually_INF_base) (auto simp: eventually_principal intro: min.cobounded1 min.cobounded2)
also have "(INF k. principal {..< k::'a}) = at_bot"
- unfolding at_bot_def
+ unfolding at_bot_def
by (intro INF_eq) (auto intro: less_imp_le simp: Iic_subset_Iio_iff lt_ex)
finally show ?thesis .
qed
@@ -828,11 +837,11 @@
unfolding filterlim_def by (rule order_trans[OF filtermap_INF INF_mono])
lemma filterlim_base:
- "(\<And>m x. m \<in> J \<Longrightarrow> i m \<in> I) \<Longrightarrow> (\<And>m x. m \<in> J \<Longrightarrow> x \<in> F (i m) \<Longrightarrow> f x \<in> G m) \<Longrightarrow>
+ "(\<And>m x. m \<in> J \<Longrightarrow> i m \<in> I) \<Longrightarrow> (\<And>m x. m \<in> J \<Longrightarrow> x \<in> F (i m) \<Longrightarrow> f x \<in> G m) \<Longrightarrow>
LIM x (INF i:I. principal (F i)). f x :> (INF j:J. principal (G j))"
by (force intro!: filterlim_INF_INF simp: image_subset_iff)
-lemma filterlim_base_iff:
+lemma filterlim_base_iff:
assumes "I \<noteq> {}" and chain: "\<And>i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> F i \<subseteq> F j \<or> F j \<subseteq> F i"
shows "(LIM x (INF i:I. principal (F i)). f x :> INF j:J. principal (G j)) \<longleftrightarrow>
(\<forall>j\<in>J. \<exists>i\<in>I. \<forall>x\<in>F i. f x \<in> G j)"
@@ -912,7 +921,7 @@
shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z>c. eventually (\<lambda>x. Z \<le> f x) F)"
by (metis filterlim_at_top order_less_le_trans gt_ex filterlim_at_top_ge)
-lemma filterlim_at_bot:
+lemma filterlim_at_bot:
fixes f :: "'a \<Rightarrow> ('b::linorder)"
shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. f x \<le> Z) F)"
by (auto simp: filterlim_iff eventually_at_bot_linorder elim!: eventually_elim1)
@@ -926,12 +935,12 @@
assume "\<forall>Z. eventually (\<lambda>x. f x \<le> Z) F"
hence "eventually (\<lambda>x. f x \<le> Z') F" by auto
thus "eventually (\<lambda>x. f x < Z) F"
- apply (rule eventually_mono[rotated])
+ apply (rule eventually_mono')
using 1 by auto
- next
- fix Z :: 'b
+ next
+ fix Z :: 'b
show "\<forall>Z. eventually (\<lambda>x. f x < Z) F \<Longrightarrow> eventually (\<lambda>x. f x \<le> Z) F"
- by (drule spec [of _ Z], erule eventually_mono[rotated], auto simp add: less_imp_le)
+ by (drule spec [of _ Z], erule eventually_mono', auto simp add: less_imp_le)
qed
lemma filterlim_at_bot_le:
@@ -958,7 +967,7 @@
where "rel_filter R F G = ((R ===> op =) ===> op =) (Rep_filter F) (Rep_filter G)"
lemma rel_filter_eventually:
- "rel_filter R F G \<longleftrightarrow>
+ "rel_filter R F G \<longleftrightarrow>
((R ===> op =) ===> op =) (\<lambda>P. eventually P F) (\<lambda>P. eventually P G)"
by(simp add: rel_filter_def eventually_def)
@@ -984,7 +993,7 @@
from Q have *: "\<And>x. T (Rep x) x" unfolding Quotient_alt_def by blast
fix F
- show "rel_filter T (filtermap Rep F) F"
+ show "rel_filter T (filtermap Rep F) F"
by(auto elim: rel_funD intro: * intro!: ext arg_cong[where f="\<lambda>P. eventually P F"] rel_funI
del: iffI simp add: eventually_filtermap rel_filter_eventually)
qed(auto simp add: map_fun_def o_def eventually_filtermap filter_eq_iff fun_eq_iff rel_filter_eventually
@@ -1063,7 +1072,7 @@
proof(rule left_totalI)
fix F :: "'a filter"
from bi_total_fun[OF bi_unique_fun[OF \<open>bi_total A\<close> bi_unique_eq] bi_total_eq]
- obtain G where [transfer_rule]: "((A ===> op =) ===> op =) (\<lambda>P. eventually P F) G"
+ obtain G where [transfer_rule]: "((A ===> op =) ===> op =) (\<lambda>P. eventually P F) G"
unfolding bi_total_def by blast
moreover have "is_filter (\<lambda>P. eventually P F) \<longleftrightarrow> is_filter G" by transfer_prover
hence "is_filter G" by(simp add: eventually_def is_filter_Rep_filter)
@@ -1094,7 +1103,7 @@
fix P :: "'a \<Rightarrow> bool"
obtain P' where [transfer_rule]: "(A ===> op =) P P'"
using left_total_fun[OF assms left_total_eq] unfolding left_total_def by blast
- have "eventually P F = eventually P' G"
+ have "eventually P F = eventually P' G"
and "eventually P F' = eventually P' G" by transfer_prover+
thus "eventually P F = eventually P F'" by simp
qed
@@ -1139,7 +1148,7 @@
context
fixes A :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
- assumes [transfer_rule]: "bi_unique A"
+ assumes [transfer_rule]: "bi_unique A"
begin
lemma le_filter_parametric [transfer_rule]:
@@ -1173,4 +1182,4 @@
end
-end
\ No newline at end of file
+end
--- a/src/HOL/Library/Extended_Real.thy Mon Dec 07 10:38:04 2015 +0100
+++ b/src/HOL/Library/Extended_Real.thy Mon Dec 07 16:44:26 2015 +0000
@@ -2443,11 +2443,8 @@
assume "open S" and "x \<in> S"
then have S: "open S" "ereal x \<in> ereal ` S"
by (simp_all add: inj_image_mem_iff)
- have "\<forall>x. f x \<in> ereal ` S \<longrightarrow> real_of_ereal (f x) \<in> S"
- by auto
- from this lim[THEN topological_tendstoD, OF open_ereal, OF S]
show "eventually (\<lambda>x. real_of_ereal (f x) \<in> S) net"
- by (rule eventually_mono)
+ by (auto intro: eventually_mono' [OF lim[THEN topological_tendstoD, OF open_ereal, OF S]])
qed
lemma lim_ereal[simp]: "((\<lambda>n. ereal (f n)) ---> ereal x) net \<longleftrightarrow> (f ---> x) net"
--- a/src/HOL/Library/Liminf_Limsup.thy Mon Dec 07 10:38:04 2015 +0100
+++ b/src/HOL/Library/Liminf_Limsup.thy Mon Dec 07 16:44:26 2015 +0000
@@ -100,7 +100,7 @@
lemma Liminf_eq:
assumes "eventually (\<lambda>x. f x = g x) F"
shows "Liminf F f = Liminf F g"
- by (intro antisym Liminf_mono eventually_mono[OF _ assms]) auto
+ by (intro antisym Liminf_mono eventually_mono'[OF assms]) auto
lemma Limsup_mono:
assumes ev: "eventually (\<lambda>x. f x \<le> g x) F"
@@ -116,7 +116,7 @@
lemma Limsup_eq:
assumes "eventually (\<lambda>x. f x = g x) net"
shows "Limsup net f = Limsup net g"
- by (intro antisym Limsup_mono eventually_mono[OF _ assms]) auto
+ by (intro antisym Limsup_mono eventually_mono'[OF assms]) auto
lemma Liminf_le_Limsup:
assumes ntriv: "\<not> trivial_limit F"
--- a/src/HOL/Limits.thy Mon Dec 07 10:38:04 2015 +0100
+++ b/src/HOL/Limits.thy Mon Dec 07 16:44:26 2015 +0000
@@ -661,6 +661,10 @@
subsubsection \<open>Linear operators and multiplication\<close>
+lemma linear_times:
+ fixes c::"'a::real_algebra" shows "linear (\<lambda>x. c * x)"
+ by (auto simp: linearI distrib_left)
+
lemma (in bounded_linear) tendsto:
"(g ---> a) F \<Longrightarrow> ((\<lambda>x. f (g x)) ---> f a) F"
by (simp only: tendsto_Zfun_iff diff [symmetric] Zfun)
@@ -713,6 +717,16 @@
lemmas tendsto_mult [tendsto_intros] =
bounded_bilinear.tendsto [OF bounded_bilinear_mult]
+lemma tendsto_mult_left:
+ fixes c::"'a::real_normed_algebra"
+ shows "(f ---> l) F \<Longrightarrow> ((\<lambda>x. c * (f x)) ---> c * l) F"
+by (rule tendsto_mult [OF tendsto_const])
+
+lemma tendsto_mult_right:
+ fixes c::"'a::real_normed_algebra"
+ shows "(f ---> l) F \<Longrightarrow> ((\<lambda>x. (f x) * c) ---> l * c) F"
+by (rule tendsto_mult [OF _ tendsto_const])
+
lemmas continuous_of_real [continuous_intros] =
bounded_linear.continuous [OF bounded_linear_of_real]
--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Mon Dec 07 10:38:04 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Mon Dec 07 16:44:26 2015 +0000
@@ -1508,7 +1508,7 @@
apply (auto simp: has_contour_integral_integral)
done
-lemma contour_integral_0: "contour_integral g (\<lambda>x. 0) = 0"
+lemma contour_integral_0 [simp]: "contour_integral g (\<lambda>x. 0) = 0"
by (simp add: contour_integral_unique has_contour_integral_0)
lemma contour_integral_setsum:
@@ -4728,4 +4728,472 @@
\<Longrightarrow> winding_number h z = winding_number g z"
by (metis segment_bound(2) norm_minus_commute not_le winding_number_loops_linear_eq)
+
+proposition winding_number_subpath_combine:
+ "\<lbrakk>path g; z \<notin> path_image g;
+ u \<in> {0..1}; v \<in> {0..1}; w \<in> {0..1}\<rbrakk>
+ \<Longrightarrow> winding_number (subpath u v g) z + winding_number (subpath v w g) z =
+ winding_number (subpath u w g) z"
+apply (rule trans [OF winding_number_join [THEN sym]
+ winding_number_homotopic_paths [OF homotopic_join_subpaths]])
+apply (auto dest: path_image_subpath_subset)
+done
+
+
+subsection\<open>Partial circle path\<close>
+
+definition part_circlepath :: "[complex, real, real, real, real] \<Rightarrow> complex"
+ where "part_circlepath z r s t \<equiv> \<lambda>x. z + of_real r * exp (ii * of_real (linepath s t x))"
+
+lemma pathstart_part_circlepath [simp]:
+ "pathstart(part_circlepath z r s t) = z + r*exp(ii * s)"
+by (metis part_circlepath_def pathstart_def pathstart_linepath)
+
+lemma pathfinish_part_circlepath [simp]:
+ "pathfinish(part_circlepath z r s t) = z + r*exp(ii*t)"
+by (metis part_circlepath_def pathfinish_def pathfinish_linepath)
+
+proposition has_vector_derivative_part_circlepath [derivative_intros]:
+ "((part_circlepath z r s t) has_vector_derivative
+ (ii * r * (of_real t - of_real s) * exp(ii * linepath s t x)))
+ (at x within X)"
+ apply (simp add: part_circlepath_def linepath_def scaleR_conv_of_real)
+ apply (rule has_vector_derivative_real_complex)
+ apply (rule derivative_eq_intros | simp)+
+ done
+
+corollary vector_derivative_part_circlepath:
+ "vector_derivative (part_circlepath z r s t) (at x) =
+ ii * r * (of_real t - of_real s) * exp(ii * linepath s t x)"
+ using has_vector_derivative_part_circlepath vector_derivative_at by blast
+
+corollary vector_derivative_part_circlepath01:
+ "\<lbrakk>0 \<le> x; x \<le> 1\<rbrakk>
+ \<Longrightarrow> vector_derivative (part_circlepath z r s t) (at x within {0..1}) =
+ ii * r * (of_real t - of_real s) * exp(ii * linepath s t x)"
+ using has_vector_derivative_part_circlepath
+ by (auto simp: vector_derivative_at_within_ivl)
+
+lemma valid_path_part_circlepath [simp]: "valid_path (part_circlepath z r s t)"
+ apply (simp add: valid_path_def)
+ apply (rule C1_differentiable_imp_piecewise)
+ apply (auto simp: C1_differentiable_on_eq vector_derivative_works vector_derivative_part_circlepath has_vector_derivative_part_circlepath
+ intro!: continuous_intros)
+ done
+
+lemma path_part_circlepath [simp]: "path (part_circlepath z r s t)"
+ by (simp add: valid_path_imp_path)
+
+proposition path_image_part_circlepath:
+ assumes "s \<le> t"
+ shows "path_image (part_circlepath z r s t) = {z + r * exp(ii * of_real x) | x. s \<le> x \<and> x \<le> t}"
+proof -
+ { fix z::real
+ assume "0 \<le> z" "z \<le> 1"
+ with \<open>s \<le> t\<close> have "\<exists>x. (exp (\<i> * linepath s t z) = exp (\<i> * of_real x)) \<and> s \<le> x \<and> x \<le> t"
+ apply (rule_tac x="(1 - z) * s + z * t" in exI)
+ apply (simp add: linepath_def scaleR_conv_of_real algebra_simps)
+ apply (rule conjI)
+ using mult_right_mono apply blast
+ using affine_ineq by (metis "mult.commute")
+ }
+ moreover
+ { fix z
+ assume "s \<le> z" "z \<le> t"
+ then have "z + of_real r * exp (\<i> * of_real z) \<in> (\<lambda>x. z + of_real r * exp (\<i> * linepath s t x)) ` {0..1}"
+ apply (rule_tac x="(z - s)/(t - s)" in image_eqI)
+ apply (simp add: linepath_def scaleR_conv_of_real divide_simps exp_eq)
+ apply (auto simp: algebra_simps divide_simps)
+ done
+ }
+ ultimately show ?thesis
+ by (fastforce simp add: path_image_def part_circlepath_def)
+qed
+
+corollary path_image_part_circlepath_subset:
+ "\<lbrakk>s \<le> t; 0 \<le> r\<rbrakk> \<Longrightarrow> path_image(part_circlepath z r s t) \<subseteq> sphere z r"
+by (auto simp: path_image_part_circlepath sphere_def dist_norm algebra_simps norm_mult)
+
+proposition in_path_image_part_circlepath:
+ assumes "w \<in> path_image(part_circlepath z r s t)" "s \<le> t" "0 \<le> r"
+ shows "norm(w - z) = r"
+proof -
+ have "w \<in> {c. dist z c = r}"
+ by (metis (no_types) path_image_part_circlepath_subset sphere_def subset_eq assms)
+ thus ?thesis
+ by (simp add: dist_norm norm_minus_commute)
+qed
+
+proposition finite_bounded_log: "finite {z::complex. norm z \<le> b \<and> exp z = w}"
+proof (cases "w = 0")
+ case True then show ?thesis by auto
+next
+ case False
+ have *: "finite {x. cmod (complex_of_real (2 * real_of_int x * pi) * \<i>) \<le> b + cmod (Ln w)}"
+ apply (simp add: norm_mult finite_int_iff_bounded_le)
+ apply (rule_tac x="floor ((b + cmod (Ln w)) / (2*pi))" in exI)
+ apply (auto simp: divide_simps le_floor_iff)
+ done
+ have [simp]: "\<And>P f. {z. P z \<and> (\<exists>n. z = f n)} = f ` {n. P (f n)}"
+ by blast
+ show ?thesis
+ apply (subst exp_Ln [OF False, symmetric])
+ apply (simp add: exp_eq)
+ using norm_add_leD apply (fastforce intro: finite_subset [OF _ *])
+ done
+qed
+
+lemma finite_bounded_log2:
+ fixes a::complex
+ assumes "a \<noteq> 0"
+ shows "finite {z. norm z \<le> b \<and> exp(a*z) = w}"
+proof -
+ have *: "finite ((\<lambda>z. z / a) ` {z. cmod z \<le> b * cmod a \<and> exp z = w})"
+ by (rule finite_imageI [OF finite_bounded_log])
+ show ?thesis
+ by (rule finite_subset [OF _ *]) (force simp: assms norm_mult)
+qed
+
+proposition has_contour_integral_bound_part_circlepath_strong:
+ assumes fi: "(f has_contour_integral i) (part_circlepath z r s t)"
+ and "finite k" and le: "0 \<le> B" "0 < r" "s \<le> t"
+ and B: "\<And>x. x \<in> path_image(part_circlepath z r s t) - k \<Longrightarrow> norm(f x) \<le> B"
+ shows "cmod i \<le> B * r * (t - s)"
+proof -
+ consider "s = t" | "s < t" using \<open>s \<le> t\<close> by linarith
+ then show ?thesis
+ proof cases
+ case 1 with fi [unfolded has_contour_integral]
+ have "i = 0" by (simp add: vector_derivative_part_circlepath)
+ with assms show ?thesis by simp
+ next
+ case 2
+ have [simp]: "abs r = r" using \<open>r > 0\<close> by linarith
+ have [simp]: "cmod (complex_of_real t - complex_of_real s) = t-s"
+ by (metis "2" abs_of_pos diff_gt_0_iff_gt norm_of_real of_real_diff)
+ have "finite (part_circlepath z r s t -` {y} \<inter> {0..1})" if "y \<in> k" for y
+ proof -
+ def w \<equiv> "(y - z)/of_real r / exp(ii * of_real s)"
+ have fin: "finite (of_real -` {z. cmod z \<le> 1 \<and> exp (\<i> * complex_of_real (t - s) * z) = w})"
+ apply (rule finite_vimageI [OF finite_bounded_log2])
+ using \<open>s < t\<close> apply (auto simp: inj_of_real)
+ done
+ show ?thesis
+ apply (simp add: part_circlepath_def linepath_def vimage_def)
+ apply (rule finite_subset [OF _ fin])
+ using le
+ apply (auto simp: w_def algebra_simps scaleR_conv_of_real exp_add exp_diff)
+ done
+ qed
+ then have fin01: "finite ((part_circlepath z r s t) -` k \<inter> {0..1})"
+ by (rule finite_finite_vimage_IntI [OF \<open>finite k\<close>])
+ have **: "((\<lambda>x. if (part_circlepath z r s t x) \<in> k then 0
+ else f(part_circlepath z r s t x) *
+ vector_derivative (part_circlepath z r s t) (at x)) has_integral i) {0..1}"
+ apply (rule has_integral_spike
+ [where f = "\<lambda>x. f(part_circlepath z r s t x) * vector_derivative (part_circlepath z r s t) (at x)"])
+ apply (rule negligible_finite [OF fin01])
+ using fi has_contour_integral
+ apply auto
+ done
+ have *: "\<And>x. \<lbrakk>0 \<le> x; x \<le> 1; part_circlepath z r s t x \<notin> k\<rbrakk> \<Longrightarrow> cmod (f (part_circlepath z r s t x)) \<le> B"
+ by (auto intro!: B [unfolded path_image_def image_def, simplified])
+ show ?thesis
+ apply (rule has_integral_bound [where 'a=real, simplified, OF _ **, simplified])
+ using assms apply force
+ apply (simp add: norm_mult vector_derivative_part_circlepath)
+ using le * "2" \<open>r > 0\<close> by auto
+ qed
+qed
+
+corollary has_contour_integral_bound_part_circlepath:
+ "\<lbrakk>(f has_contour_integral i) (part_circlepath z r s t);
+ 0 \<le> B; 0 < r; s \<le> t;
+ \<And>x. x \<in> path_image(part_circlepath z r s t) \<Longrightarrow> norm(f x) \<le> B\<rbrakk>
+ \<Longrightarrow> norm i \<le> B*r*(t - s)"
+ by (auto intro: has_contour_integral_bound_part_circlepath_strong)
+
+proposition contour_integrable_continuous_part_circlepath:
+ "continuous_on (path_image (part_circlepath z r s t)) f
+ \<Longrightarrow> f contour_integrable_on (part_circlepath z r s t)"
+ apply (simp add: contour_integrable_on has_contour_integral_def vector_derivative_part_circlepath path_image_def)
+ apply (rule integrable_continuous_real)
+ apply (fast intro: path_part_circlepath [unfolded path_def] continuous_intros continuous_on_compose2 [where g=f, OF _ _ order_refl])
+ done
+
+proposition winding_number_part_circlepath_pos_less:
+ assumes "s < t" and no: "norm(w - z) < r"
+ shows "0 < Re (winding_number(part_circlepath z r s t) w)"
+proof -
+ have "0 < r" by (meson no norm_not_less_zero not_le order.strict_trans2)
+ note valid_path_part_circlepath
+ moreover have " w \<notin> path_image (part_circlepath z r s t)"
+ using assms by (auto simp: path_image_def image_def part_circlepath_def norm_mult linepath_def)
+ moreover have "0 < r * (t - s) * (r - cmod (w - z))"
+ using assms by (metis \<open>0 < r\<close> diff_gt_0_iff_gt mult_pos_pos)
+ ultimately show ?thesis
+ apply (rule winding_number_pos_lt [where e = "r*(t - s)*(r - norm(w - z))"])
+ apply (simp add: vector_derivative_part_circlepath right_diff_distrib [symmetric] mult_ac)
+ apply (rule mult_left_mono)+
+ using Re_Im_le_cmod [of "w-z" "linepath s t x" for x]
+ apply (simp add: exp_Euler cos_of_real sin_of_real part_circlepath_def algebra_simps cos_squared_eq [unfolded power2_eq_square])
+ using assms \<open>0 < r\<close> by auto
+qed
+
+proposition simple_path_part_circlepath:
+ "simple_path(part_circlepath z r s t) \<longleftrightarrow> (r \<noteq> 0 \<and> s \<noteq> t \<and> abs(s - t) \<le> 2*pi)"
+proof (cases "r = 0 \<or> s = t")
+ case True
+ then show ?thesis
+ apply (rule disjE)
+ apply (force simp: part_circlepath_def simple_path_def intro: bexI [where x = "1/4"] bexI [where x = "1/3"])+
+ done
+next
+ case False then have "r \<noteq> 0" "s \<noteq> t" by auto
+ have *: "\<And>x y z s t. ii*((1 - x) * s + x * t) = ii*(((1 - y) * s + y * t)) + z \<longleftrightarrow> ii*(x - y) * (t - s) = z"
+ by (simp add: algebra_simps)
+ have abs01: "\<And>x y::real. 0 \<le> x \<and> x \<le> 1 \<and> 0 \<le> y \<and> y \<le> 1
+ \<Longrightarrow> (x = y \<or> x = 0 \<and> y = 1 \<or> x = 1 \<and> y = 0 \<longleftrightarrow> abs(x - y) \<in> {0,1})"
+ by auto
+ have abs_away: "\<And>P. (\<forall>x\<in>{0..1}. \<forall>y\<in>{0..1}. P(abs(x - y))) \<longleftrightarrow> (\<forall>x::real. 0 \<le> x \<and> x \<le> 1 \<longrightarrow> P x)"
+ by force
+ have **: "\<And>x y. (\<exists>n. (complex_of_real x - of_real y) * (of_real t - of_real s) = 2 * (of_int n * of_real pi)) \<longleftrightarrow>
+ (\<exists>n. abs(x - y) * (t - s) = 2 * (of_int n * pi))"
+ by (force simp: algebra_simps abs_if dest: arg_cong [where f=Re] arg_cong [where f=complex_of_real]
+ intro: exI [where x = "-n" for n])
+ have 1: "\<forall>x. 0 \<le> x \<and> x \<le> 1 \<longrightarrow> (\<exists>n. x * (t - s) = 2 * (real_of_int n * pi)) \<longrightarrow> x = 0 \<or> x = 1 \<Longrightarrow> \<bar>s - t\<bar> \<le> 2 * pi"
+ apply (rule ccontr)
+ apply (drule_tac x="2*pi / abs(t-s)" in spec)
+ using False
+ apply (simp add: abs_minus_commute divide_simps)
+ apply (frule_tac x=1 in spec)
+ apply (drule_tac x="-1" in spec)
+ apply (simp add:)
+ done
+ have 2: "\<bar>s - t\<bar> = \<bar>2 * (real_of_int n * pi) / x\<bar>" if "x \<noteq> 0" "x * (t - s) = 2 * (real_of_int n * pi)" for x n
+ proof -
+ have "t-s = 2 * (real_of_int n * pi)/x"
+ using that by (simp add: field_simps)
+ then show ?thesis by (metis abs_minus_commute)
+ qed
+ show ?thesis using False
+ apply (simp add: simple_path_def path_part_circlepath)
+ apply (simp add: part_circlepath_def linepath_def exp_eq * ** abs01 del: Set.insert_iff)
+ apply (subst abs_away)
+ apply (auto simp: 1)
+ apply (rule ccontr)
+ apply (auto simp: 2 divide_simps abs_mult dest: of_int_leD)
+ done
+qed
+
+proposition arc_part_circlepath:
+ assumes "r \<noteq> 0" "s \<noteq> t" "abs(s - t) < 2*pi"
+ shows "arc (part_circlepath z r s t)"
+proof -
+ have *: "x = y" if eq: "\<i> * (linepath s t x) = \<i> * (linepath s t y) + 2 * of_int n * complex_of_real pi * \<i>"
+ and x: "x \<in> {0..1}" and y: "y \<in> {0..1}" for x y n
+ proof -
+ have "(linepath s t x) = (linepath s t y) + 2 * of_int n * complex_of_real pi"
+ by (metis add_divide_eq_iff complex_i_not_zero mult.commute nonzero_mult_divide_cancel_left eq)
+ then have "s*y + t*x = s*x + (t*y + of_int n * (pi * 2))"
+ by (force simp: algebra_simps linepath_def dest: arg_cong [where f=Re])
+ then have st: "x \<noteq> y \<Longrightarrow> (s-t) = (of_int n * (pi * 2) / (y-x))"
+ by (force simp: field_simps)
+ show ?thesis
+ apply (rule ccontr)
+ using assms x y
+ apply (simp add: st abs_mult field_simps)
+ using st
+ apply (auto simp: dest: of_int_lessD)
+ done
+ qed
+ show ?thesis
+ using assms
+ apply (simp add: arc_def)
+ apply (simp add: part_circlepath_def inj_on_def exp_eq)
+ apply (blast intro: *)
+ done
+qed
+
+
+subsection\<open>Special case of one complete circle\<close>
+
+definition circlepath :: "[complex, real, real] \<Rightarrow> complex"
+ where "circlepath z r \<equiv> part_circlepath z r 0 (2*pi)"
+
+lemma circlepath: "circlepath z r = (\<lambda>x. z + r * exp(2 * of_real pi * ii * of_real x))"
+ by (simp add: circlepath_def part_circlepath_def linepath_def algebra_simps)
+
+lemma pathstart_circlepath [simp]: "pathstart (circlepath z r) = z + r"
+ by (simp add: circlepath_def)
+
+lemma pathfinish_circlepath [simp]: "pathfinish (circlepath z r) = z + r"
+ by (simp add: circlepath_def) (metis exp_two_pi_i mult.commute)
+
+proposition has_vector_derivative_circlepath [derivative_intros]:
+ "((circlepath z r) has_vector_derivative (2 * pi * ii * r * exp (2 * of_real pi * ii * of_real x)))
+ (at x within X)"
+ apply (simp add: circlepath_def scaleR_conv_of_real)
+ apply (rule derivative_eq_intros)
+ apply (simp add: algebra_simps)
+ done
+
+corollary vector_derivative_circlepath:
+ "vector_derivative (circlepath z r) (at x) =
+ 2 * pi * ii * r * exp(2 * of_real pi * ii * x)"
+using has_vector_derivative_circlepath vector_derivative_at by blast
+
+corollary vector_derivative_circlepath01:
+ "\<lbrakk>0 \<le> x; x \<le> 1\<rbrakk>
+ \<Longrightarrow> vector_derivative (circlepath z r) (at x within {0..1}) =
+ 2 * pi * ii * r * exp(2 * of_real pi * ii * x)"
+ using has_vector_derivative_circlepath
+ by (auto simp: vector_derivative_at_within_ivl)
+
+lemma valid_path_circlepath [simp]: "valid_path (circlepath z r)"
+ by (simp add: circlepath_def)
+
+lemma path_circlepath [simp]: "path (circlepath z r)"
+ by (simp add: valid_path_imp_path)
+
+proposition path_image_circlepath [simp]:
+ assumes "0 \<le> r" shows "path_image (circlepath z r) = sphere z r"
+proof -
+ have *: "x \<in> (\<lambda>u. z + (cmod (x - z)) * exp (\<i> * (of_real u * (of_real pi * 2)))) ` {0..1}" for x
+ proof (cases "x = z")
+ case True then show ?thesis by force
+ next
+ case False
+ def w \<equiv> "x - z"
+ then have "w \<noteq> 0" by (simp add: False)
+ have **: "\<And>t. \<lbrakk>Re w = cos t * cmod w; Im w = sin t * cmod w\<rbrakk> \<Longrightarrow> w = of_real (cmod w) * exp (\<i> * t)"
+ using cis_conv_exp complex_eq_iff by auto
+ show ?thesis
+ apply (rule sincos_total_2pi [of "Re(w/of_real(norm w))" "Im(w/of_real(norm w))"])
+ apply (simp add: divide_simps \<open>w \<noteq> 0\<close> cmod_power2 [symmetric])
+ apply (rule_tac x="t / (2*pi)" in image_eqI)
+ apply (simp add: divide_simps \<open>w \<noteq> 0\<close>)
+ using False **
+ apply (auto simp: w_def)
+ done
+ qed
+ show ?thesis
+ unfolding circlepath path_image_def sphere_def dist_norm
+ by (force simp: assms algebra_simps norm_mult norm_minus_commute intro: *)
+qed
+
+lemma has_contour_integral_bound_circlepath_strong:
+ "\<lbrakk>(f has_contour_integral i) (circlepath z r);
+ finite k; 0 \<le> B; 0 < r;
+ \<And>x. \<lbrakk>norm(x - z) = r; x \<notin> k\<rbrakk> \<Longrightarrow> norm(f x) \<le> B\<rbrakk>
+ \<Longrightarrow> norm i \<le> B*(2*pi*r)"
+ unfolding circlepath_def
+ by (auto simp: algebra_simps in_path_image_part_circlepath dest!: has_contour_integral_bound_part_circlepath_strong)
+
+corollary has_contour_integral_bound_circlepath:
+ "\<lbrakk>(f has_contour_integral i) (circlepath z r);
+ 0 \<le> B; 0 < r; \<And>x. norm(x - z) = r \<Longrightarrow> norm(f x) \<le> B\<rbrakk>
+ \<Longrightarrow> norm i \<le> B*(2*pi*r)"
+ by (auto intro: has_contour_integral_bound_circlepath_strong)
+
+proposition contour_integrable_continuous_circlepath:
+ "continuous_on (path_image (circlepath z r)) f
+ \<Longrightarrow> f contour_integrable_on (circlepath z r)"
+ by (simp add: circlepath_def contour_integrable_continuous_part_circlepath)
+
+lemma simple_path_circlepath: "simple_path(circlepath z r) \<longleftrightarrow> (r \<noteq> 0)"
+ by (simp add: circlepath_def simple_path_part_circlepath)
+
+lemma notin_path_image_circlepath [simp]: "cmod (w - z) < r \<Longrightarrow> w \<notin> path_image (circlepath z r)"
+ apply (subst path_image_circlepath)
+ apply (meson le_cases less_le_trans norm_not_less_zero)
+ apply (simp add: sphere_def dist_norm norm_minus_commute)
+ done
+
+proposition contour_integral_circlepath:
+ "0 < r \<Longrightarrow> contour_integral (circlepath z r) (\<lambda>w. 1 / (w - z)) = 2 * complex_of_real pi * \<i>"
+ apply (rule contour_integral_unique)
+ apply (simp add: has_contour_integral_def)
+ apply (subst has_integral_cong)
+ apply (simp add: vector_derivative_circlepath01)
+ using has_integral_const_real [of _ 0 1]
+ apply (force simp: circlepath)
+ done
+
+lemma winding_number_circlepath_centre: "0 < r \<Longrightarrow> winding_number (circlepath z r) z = 1"
+ apply (rule winding_number_unique_loop)
+ apply (simp_all add: sphere_def valid_path_imp_path)
+ apply (rule_tac x="circlepath z r" in exI)
+ apply (simp add: sphere_def contour_integral_circlepath)
+ done
+
+proposition winding_number_circlepath:
+ assumes "norm(w - z) < r" shows "winding_number(circlepath z r) w = 1"
+proof (cases "w = z")
+ case True then show ?thesis
+ using assms winding_number_circlepath_centre by auto
+next
+ case False
+ have [simp]: "r > 0"
+ using assms le_less_trans norm_ge_zero by blast
+ def r' \<equiv> "norm(w - z)"
+ have "r' < r"
+ by (simp add: assms r'_def)
+ have disjo: "cball z r' \<inter> sphere z r = {}"
+ using \<open>r' < r\<close> by (force simp: cball_def sphere_def)
+ have "winding_number(circlepath z r) w = winding_number(circlepath z r) z"
+ apply (rule winding_number_around_inside [where s = "cball z r'"])
+ apply (simp_all add: disjo order.strict_implies_order winding_number_circlepath_centre)
+ apply (simp_all add: False r'_def dist_norm norm_minus_commute)
+ done
+ also have "... = 1"
+ by (simp add: winding_number_circlepath_centre)
+ finally show ?thesis .
+qed
+
+
+text\<open> Hence the Cauchy formula for points inside a circle.\<close>
+
+theorem Cauchy_integral_circlepath:
+ assumes "continuous_on (cball z r) f" "f holomorphic_on (ball z r)" "norm(w - z) < r"
+ shows "((\<lambda>u. f u/(u - w)) has_contour_integral (2 * of_real pi * ii * f w))
+ (circlepath z r)"
+proof -
+ have "r > 0"
+ using assms le_less_trans norm_ge_zero by blast
+ have "((\<lambda>u. f u / (u - w)) has_contour_integral (2 * pi) * \<i> * winding_number (circlepath z r) w * f w)
+ (circlepath z r)"
+ apply (rule Cauchy_integral_formula_weak [where s = "cball z r" and k = "{}"])
+ using assms \<open>r > 0\<close>
+ apply (simp_all add: dist_norm norm_minus_commute)
+ apply (metis at_within_interior dist_norm holomorphic_on_def interior_ball mem_ball norm_minus_commute)
+ apply (simp add: cball_def sphere_def dist_norm, clarify)
+ apply (simp add:)
+ by (metis dist_commute dist_norm less_irrefl)
+ then show ?thesis
+ by (simp add: winding_number_circlepath assms)
+qed
+
+corollary Cauchy_integral_circlepath_simple:
+ assumes "f holomorphic_on cball z r" "norm(w - z) < r"
+ shows "((\<lambda>u. f u/(u - w)) has_contour_integral (2 * of_real pi * ii * f w))
+ (circlepath z r)"
+using assms by (force simp: holomorphic_on_imp_continuous_on holomorphic_on_subset Cauchy_integral_circlepath)
+
+
+lemma no_bounded_connected_component_imp_winding_number_zero:
+ assumes g: "path g" "path_image g \<subseteq> s" "pathfinish g = pathstart g" "z \<notin> s"
+ and nb: "\<And>z. bounded (connected_component_set (- s) z) \<longrightarrow> z \<in> s"
+ shows "winding_number g z = 0"
+apply (rule winding_number_zero_in_outside)
+apply (simp_all add: assms)
+by (metis nb [of z] \<open>path_image g \<subseteq> s\<close> \<open>z \<notin> s\<close> contra_subsetD mem_Collect_eq outside outside_mono)
+
+lemma no_bounded_path_component_imp_winding_number_zero:
+ assumes g: "path g" "path_image g \<subseteq> s" "pathfinish g = pathstart g" "z \<notin> s"
+ and nb: "\<And>z. bounded (path_component_set (- s) z) \<longrightarrow> z \<in> s"
+ shows "winding_number g z = 0"
+apply (rule no_bounded_connected_component_imp_winding_number_zero [OF g])
+by (simp add: bounded_subset nb path_component_subset_connected_component)
+
end
--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Mon Dec 07 10:38:04 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Mon Dec 07 16:44:26 2015 +0000
@@ -24,8 +24,8 @@
using bounded_linear.has_derivative[OF bounded_linear_of_real] .
lemma has_vector_derivative_real_complex:
- "DERIV f (of_real a) :> f' \<Longrightarrow> ((\<lambda>x. f (of_real x)) has_vector_derivative f') (at a)"
- using has_derivative_compose[of of_real of_real a UNIV f "op * f'"]
+ "DERIV f (of_real a) :> f' \<Longrightarrow> ((\<lambda>x. f (of_real x)) has_vector_derivative f') (at a within s)"
+ using has_derivative_compose[of of_real of_real a _ f "op * f'"]
by (simp add: scaleR_conv_of_real ac_simps has_vector_derivative_def has_field_derivative_def)
lemma fact_cancel:
@@ -33,10 +33,6 @@
shows "of_nat (Suc n) * c / (fact (Suc n)) = c / (fact n)"
by (simp add: of_nat_mult del: of_nat_Suc times_nat.simps)
-lemma linear_times:
- fixes c::"'a::real_algebra" shows "linear (\<lambda>x. c * x)"
- by (auto simp: linearI distrib_left)
-
lemma bilinear_times:
fixes c::"'a::real_algebra" shows "bilinear (\<lambda>x y::'a. x*y)"
by (auto simp: bilinear_def distrib_left distrib_right intro!: linearI)
@@ -44,16 +40,6 @@
lemma linear_cnj: "linear cnj"
using bounded_linear.linear[OF bounded_linear_cnj] .
-lemma tendsto_mult_left:
- fixes c::"'a::real_normed_algebra"
- shows "(f ---> l) F \<Longrightarrow> ((\<lambda>x. c * (f x)) ---> c * l) F"
-by (rule tendsto_mult [OF tendsto_const])
-
-lemma tendsto_mult_right:
- fixes c::"'a::real_normed_algebra"
- shows "(f ---> l) F \<Longrightarrow> ((\<lambda>x. (f x) * c) ---> l * c) F"
-by (rule tendsto_mult [OF _ tendsto_const])
-
lemma tendsto_Re_upper:
assumes "~ (trivial_limit F)"
"(f ---> l) F"
--- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Mon Dec 07 10:38:04 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Mon Dec 07 16:44:26 2015 +0000
@@ -854,6 +854,13 @@
obtains r a::real where "z = complex_of_real r * (cos a + \<i> * sin a)" "0 \<le> r" "0 \<le> a" "a < 2*pi"
using Arg cis.ctr cis_conv_exp by fastforce
+lemma Re_Im_le_cmod: "Im w * sin \<phi> + Re w * cos \<phi> \<le> cmod w"
+proof (cases w rule: complex_split_polar)
+ case (1 r a) with sin_cos_le1 [of a \<phi>] show ?thesis
+ apply (simp add: norm_mult cmod_unit_one)
+ by (metis (no_types, hide_lams) abs_le_D1 distrib_left mult.commute mult.left_commute mult_left_le)
+qed
+
subsection\<open>Analytic properties of tangent function\<close>
lemma cnj_tan: "cnj(tan z) = tan(cnj z)"
--- a/src/HOL/Multivariate_Analysis/Integration.thy Mon Dec 07 10:38:04 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Mon Dec 07 16:44:26 2015 +0000
@@ -2622,7 +2622,7 @@
lemma integral_neg: "f integrable_on s \<Longrightarrow> integral s (\<lambda>x. - f x) = - integral s f"
by (rule integral_unique) (metis integrable_integral has_integral_neg)
-lemma integral_sub: "f integrable_on s \<Longrightarrow> g integrable_on s \<Longrightarrow>
+lemma integral_diff: "f integrable_on s \<Longrightarrow> g integrable_on s \<Longrightarrow>
integral s (\<lambda>x. f x - g x) = integral s f - integral s g"
by (rule integral_unique) (metis integrable_integral has_integral_sub)
@@ -2645,7 +2645,7 @@
lemma integrable_neg: "f integrable_on s \<Longrightarrow> (\<lambda>x. -f(x)) integrable_on s"
unfolding integrable_on_def by(auto intro: has_integral_neg)
-lemma integrable_sub:
+lemma integrable_diff:
"f integrable_on s \<Longrightarrow> g integrable_on s \<Longrightarrow> (\<lambda>x. f x - g x) integrable_on s"
unfolding integrable_on_def by(auto intro: has_integral_sub)
@@ -4623,6 +4623,8 @@
qed
qed
+lemmas integrable_uniform_limit_real = integrable_uniform_limit [where 'a=real, simplified]
+
subsection \<open>Negligible sets.\<close>
@@ -8933,19 +8935,19 @@
have *: "\<And>x f g. (if x \<in> s then f x else 0) - (if x \<in> s then g x else 0) =
(if x \<in> s then f x - g x else (0::real))"
by auto
- note ** = abs_of_nonneg[OF integral_nonneg[OF integrable_sub, OF h g]]
+ note ** = abs_of_nonneg[OF integral_nonneg[OF integrable_diff, OF h g]]
show "norm (integral (cbox a b) (\<lambda>x. if x \<in> s then h x else 0) -
integral (cbox a b) (\<lambda>x. if x \<in> s then g x else 0)) \<le>
norm (integral (cbox c d) (\<lambda>x. if x \<in> s then h x else 0) -
integral (cbox c d) (\<lambda>x. if x \<in> s then g x else 0))"
- unfolding integral_sub[OF h g,symmetric] real_norm_def
+ unfolding integral_diff[OF h g,symmetric] real_norm_def
apply (subst **)
defer
apply (subst **)
defer
apply (rule has_integral_subset_le)
defer
- apply (rule integrable_integral integrable_sub h g)+
+ apply (rule integrable_integral integrable_diff h g)+
proof safe
fix x
assume "x \<in> cbox a b"
@@ -10123,7 +10125,7 @@
qed
have sub: "\<And>k. integral s (\<lambda>x. f k x - f 0 x) = integral s (f k) - integral s (f 0)"
- apply (subst integral_sub)
+ apply (subst integral_diff)
apply (rule assms(1)[rule_format])+
apply rule
done
@@ -10144,7 +10146,7 @@
next
case (2 k)
then show ?case
- apply (rule integrable_sub)
+ apply (rule integrable_diff)
using assms(1)
apply auto
done
@@ -10182,7 +10184,7 @@
apply -
apply rule
defer
- apply (subst(asm) integral_sub)
+ apply (subst(asm) integral_diff)
using assms(1)
apply auto
apply (rule LIMSEQ_imp_Suc)
@@ -11653,11 +11655,11 @@
"J = integral (cbox a b) g"
using I[of n] J by (simp_all add: integral_unique)
then have "dist (I n) J = norm (integral (cbox a b) (\<lambda>x. f n x - g x))"
- by (simp add: integral_sub dist_norm)
+ by (simp add: integral_diff dist_norm)
also have "\<dots> \<le> integral (cbox a b) (\<lambda>x. (e' / content (cbox a b)))"
using elim
by (intro integral_norm_bound_integral)
- (auto intro!: integrable_sub absolutely_integrable_onI)
+ (auto intro!: integrable_diff absolutely_integrable_onI)
also have "\<dots> < e"
using \<open>0 < e\<close>
by (simp add: e'_def)
@@ -12029,12 +12031,12 @@
apply clarify
apply (rule le_less_trans [OF _ e2_less])
apply (rule integrable_bound)
- apply (auto intro: integrable_sub continuous_on_imp_integrable_on_Pair1)
+ apply (auto intro: integrable_diff continuous_on_imp_integrable_on_Pair1)
done
} note * = this
show ?thesis
apply (rule integrable_continuous)
- apply (simp add: * continuous_on_iff dist_norm integral_sub [symmetric] continuous_on_imp_integrable_on_Pair1 [OF assms])
+ apply (simp add: * continuous_on_iff dist_norm integral_diff [symmetric] continuous_on_imp_integrable_on_Pair1 [OF assms])
done
qed
@@ -12217,10 +12219,10 @@
by (blast intro: continuous_on_imp_integrable_on_Pair1)
have 1: "norm (integral (cbox (u,w) (v,z)) f - integral (cbox (u,w) (v,z)) (\<lambda>x. f (t1,t2)))
\<le> e * content (cbox (u,w) (v,z)) / content ?CBOX / 2"
- apply (simp only: integral_sub [symmetric] f_int_uwvz integrable_const)
+ apply (simp only: integral_diff [symmetric] f_int_uwvz integrable_const)
apply (rule order_trans [OF integrable_bound [of "e / content ?CBOX / 2"]])
using cbp e' nf'
- apply (auto simp: integrable_sub f_int_uwvz integrable_const)
+ apply (auto simp: integrable_diff f_int_uwvz integrable_const)
done
have int_integrable: "(\<lambda>x. integral (cbox w z) (\<lambda>y. f (x, y))) integrable_on cbox u v"
using assms integral_integrable_2dim continuous_on_subset uwvz_sub(2) by blast
@@ -12228,24 +12230,24 @@
"\<And>x. x \<in> cbox u v \<Longrightarrow>
norm (integral (cbox w z) (\<lambda>y. f (x, y)) - integral (cbox w z) (\<lambda>y. f (t1, t2)))
\<le> e * content (cbox w z) / content (cbox (a, c) (b, d)) / 2"
- apply (simp only: integral_sub [symmetric] f_int_uv integrable_const)
+ apply (simp only: integral_diff [symmetric] f_int_uv integrable_const)
apply (rule order_trans [OF integrable_bound [of "e / content ?CBOX / 2"]])
using cbp e' nf'
- apply (auto simp: integrable_sub f_int_uv integrable_const)
+ apply (auto simp: integrable_diff f_int_uv integrable_const)
done
have "norm (integral (cbox u v)
(\<lambda>x. integral (cbox w z) (\<lambda>y. f (x,y)) - integral (cbox w z) (\<lambda>y. f (t1,t2))))
\<le> e * content (cbox w z) / content ?CBOX / 2 * content (cbox u v)"
apply (rule integrable_bound [OF _ _ normint_wz])
using cbp e'
- apply (auto simp: divide_simps content_pos_le integrable_sub int_integrable integrable_const)
+ apply (auto simp: divide_simps content_pos_le integrable_diff int_integrable integrable_const)
done
also have "... \<le> e * content (cbox (u,w) (v,z)) / content ?CBOX / 2"
by (simp add: content_Pair divide_simps)
finally have 2: "norm (integral (cbox u v) (\<lambda>x. integral (cbox w z) (\<lambda>y. f (x,y))) -
integral (cbox u v) (\<lambda>x. integral (cbox w z) (\<lambda>y. f (t1,t2))))
\<le> e * content (cbox (u,w) (v,z)) / content ?CBOX / 2"
- by (simp only: integral_sub [symmetric] int_integrable integrable_const)
+ by (simp only: integral_diff [symmetric] int_integrable integrable_const)
have norm_xx: "\<lbrakk>x' = y'; norm(x - x') \<le> e/2; norm(y - y') \<le> e/2\<rbrakk> \<Longrightarrow> norm(x - y) \<le> e" for x::'c and y x' y' e
using norm_triangle_mono [of "x-y'" "e/2" "y'-y" "e/2"] real_sum_of_halves
by (simp add: norm_minus_commute)
--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy Mon Dec 07 10:38:04 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy Mon Dec 07 16:44:26 2015 +0000
@@ -1,5 +1,5 @@
(* Title: HOL/Multivariate_Analysis/Path_Connected.thy
- Author: Robert Himmelmann, TU Muenchen, and LC Paulson with material from HOL Light
+ Authors: LC Paulson and Robert Himmelmann (TU Muenchen), based on material from HOL Light
*)
section \<open>Continuous paths and path-connected sets\<close>
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Dec 07 10:38:04 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Dec 07 16:44:26 2015 +0000
@@ -2282,15 +2282,6 @@
lemma trivial_limit_eq: "trivial_limit net \<longleftrightarrow> (\<forall>P. eventually P net)"
by (simp add: filter_eq_iff)
-text\<open>Combining theorems for "eventually"\<close>
-
-lemma eventually_rev_mono:
- "eventually P net \<Longrightarrow> (\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> eventually Q net"
- using eventually_mono [of P Q] by fast
-
-lemma not_eventually: "(\<forall>x. \<not> P x ) \<Longrightarrow> \<not> trivial_limit net \<Longrightarrow> \<not> eventually (\<lambda>x. P x) net"
- by (simp add: eventually_False)
-
subsection \<open>Limits\<close>
@@ -2319,7 +2310,7 @@
by (auto simp add: tendsto_iff eventually_at_infinity)
lemma Lim_eventually: "eventually (\<lambda>x. f x = l) net \<Longrightarrow> (f ---> l) net"
- by (rule topological_tendstoI, auto elim: eventually_rev_mono)
+ by (rule topological_tendstoI, auto elim: eventually_mono')
text\<open>The expected monotonicity property.\<close>
@@ -2998,7 +2989,7 @@
by fast
qed
-lemma closure_ball:
+lemma closure_ball [simp]:
fixes x :: "'a::real_normed_vector"
shows "0 < e \<Longrightarrow> closure (ball x e) = cball x e"
apply (rule equalityI)
@@ -3016,7 +3007,7 @@
done
(* In a trivial vector space, this fails for e = 0. *)
-lemma interior_cball:
+lemma interior_cball [simp]:
fixes x :: "'a::{real_normed_vector, perfect_space}"
shows "interior (cball x e) = ball x e"
proof (cases "e \<ge> 0")
@@ -3108,12 +3099,12 @@
apply arith
done
-lemma cball_eq_empty: "cball x e = {} \<longleftrightarrow> e < 0"
+lemma cball_eq_empty [simp]: "cball x e = {} \<longleftrightarrow> e < 0"
apply (simp add: set_eq_iff not_le)
apply (metis zero_le_dist dist_self order_less_le_trans)
done
-lemma cball_empty: "e < 0 \<Longrightarrow> cball x e = {}"
+lemma cball_empty [simp]: "e < 0 \<Longrightarrow> cball x e = {}"
by (simp add: cball_eq_empty)
lemma cball_eq_sing:
@@ -3133,6 +3124,26 @@
shows "e = 0 \<Longrightarrow> cball x e = {x}"
by (auto simp add: set_eq_iff)
+lemma ball_divide_subset: "d \<ge> 1 \<Longrightarrow> ball x (e/d) \<subseteq> ball x e"
+ apply (cases "e \<le> 0")
+ apply (simp add: ball_empty divide_simps)
+ apply (rule subset_ball)
+ apply (simp add: divide_simps)
+ done
+
+lemma ball_divide_subset_numeral: "ball x (e / numeral w) \<subseteq> ball x e"
+ using ball_divide_subset one_le_numeral by blast
+
+lemma cball_divide_subset: "d \<ge> 1 \<Longrightarrow> cball x (e/d) \<subseteq> cball x e"
+ apply (cases "e < 0")
+ apply (simp add: divide_simps)
+ apply (rule subset_cball)
+ apply (metis divide_1 frac_le not_le order_refl zero_less_one)
+ done
+
+lemma cball_divide_subset_numeral: "cball x (e / numeral w) \<subseteq> cball x e"
+ using cball_divide_subset one_le_numeral by blast
+
subsection \<open>Boundedness\<close>
@@ -5723,7 +5734,7 @@
using \<open>open U\<close> and \<open>f x \<in> U\<close>
unfolding tendsto_def by fast
then have "eventually (\<lambda>y. f y \<noteq> a) (at x within s)"
- using \<open>a \<notin> U\<close> by (fast elim: eventually_mono [rotated])
+ using \<open>a \<notin> U\<close> by (fast elim: eventually_mono')
then show ?thesis
using \<open>f x \<noteq> a\<close> by (auto simp: dist_commute zero_less_dist_iff eventually_at)
qed
@@ -8206,9 +8217,8 @@
qed
next
assume ?rhs then show ?lhs
- apply (auto simp: ball_def dist_norm )
+ apply (auto simp: ball_def dist_norm)
apply (metis add.commute add_le_cancel_right dist_norm dist_triangle_alt order_trans)
- using le_less_trans apply fastforce
done
qed
@@ -8249,7 +8259,6 @@
assume ?rhs then show ?lhs
apply (auto simp: ball_def dist_norm )
apply (metis add.commute add_le_cancel_right dist_norm dist_triangle_alt le_less_trans)
- using le_less_trans apply fastforce
done
qed
@@ -8361,8 +8370,7 @@
using \<open>?lhs\<close> ball_eq_empty cball_eq_empty apply blast+
done
next
- assume ?rhs then show ?lhs
- by (auto simp add: set_eq_subset ball_subset_cball_iff cball_subset_ball_iff)
+ assume ?rhs then show ?lhs by auto
qed
lemma cball_eq_ball_iff:
@@ -8377,8 +8385,7 @@
using \<open>?lhs\<close> ball_eq_empty cball_eq_empty apply blast+
done
next
- assume ?rhs then show ?lhs
- by (auto simp add: set_eq_subset ball_subset_cball_iff cball_subset_ball_iff)
+ assume ?rhs then show ?lhs using ball_eq_cball_iff by blast
qed
no_notation
--- a/src/HOL/Multivariate_Analysis/Uniform_Limit.thy Mon Dec 07 10:38:04 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Uniform_Limit.thy Mon Dec 07 16:44:26 2015 +0000
@@ -477,9 +477,7 @@
lemma uniform_limit_on_subset:
"uniform_limit J f g F \<Longrightarrow> I \<subseteq> J \<Longrightarrow> uniform_limit I f g F"
- by (auto intro!: uniform_limitI dest!: uniform_limitD intro: eventually_rev_mono)
-
-
+ by (auto intro!: uniform_limitI dest!: uniform_limitD intro: eventually_mono')
lemma uniformly_convergent_add:
"uniformly_convergent_on A f \<Longrightarrow> uniformly_convergent_on A g\<Longrightarrow>
--- a/src/HOL/NSA/HyperDef.thy Mon Dec 07 10:38:04 2015 +0100
+++ b/src/HOL/NSA/HyperDef.thy Mon Dec 07 16:44:26 2015 +0000
@@ -231,7 +231,7 @@
text{*A few lemmas first*}
-lemma lemma_omega_empty_singleton_disj:
+lemma lemma_omega_empty_singleton_disj:
"{n::nat. x = real n} = {} \<or> (\<exists>y. {n::nat. x = real n} = {y})"
by force
@@ -243,8 +243,7 @@
apply (simp add: omega_def star_of_def star_n_eq_iff)
apply clarify
apply (rule_tac x2="x-1" in lemma_finite_omega_set [THEN FreeUltrafilterNat.finite, THEN notE])
-apply (rule eventually_mono)
-prefer 2 apply assumption
+apply (erule eventually_mono')
apply auto
done
--- a/src/HOL/NSA/NSA.thy Mon Dec 07 10:38:04 2015 +0100
+++ b/src/HOL/NSA/NSA.thy Mon Dec 07 16:44:26 2015 +0000
@@ -2106,7 +2106,7 @@
apply (simp add: omega_def)
apply (rule FreeUltrafilterNat_HInfinite)
apply clarify
-apply (rule_tac u1 = "u-1" in eventually_mono [OF _ FreeUltrafilterNat_nat_gt_real])
+apply (rule_tac u1 = "u-1" in eventually_mono' [OF FreeUltrafilterNat_nat_gt_real])
apply auto
done
--- a/src/HOL/Topological_Spaces.thy Mon Dec 07 10:38:04 2015 +0100
+++ b/src/HOL/Topological_Spaces.thy Mon Dec 07 16:44:26 2015 +0000
@@ -1758,7 +1758,7 @@
with \<open>finite D\<close> have "eventually (\<lambda>y. y \<notin> \<Union>D) (nhds y)"
by (simp add: eventually_ball_finite)
with \<open>s \<subseteq> \<Union>D\<close> have "eventually (\<lambda>y. y \<notin> s) (nhds y)"
- by (auto elim!: eventually_mono [rotated])
+ by (auto elim!: eventually_mono')
thus "\<exists>t. open t \<and> y \<in> t \<and> t \<subseteq> - s"
by (simp add: eventually_nhds subset_eq)
qed