--- a/src/HOL/Analysis/Convex.thy Fri Mar 03 11:25:29 2023 +0100
+++ b/src/HOL/Analysis/Convex.thy Fri Mar 03 12:22:07 2023 +0000
@@ -2369,9 +2369,6 @@
using hull_inc u by fastforce
qed
-lemma inner_sum_Basis[simp]: "i \<in> Basis \<Longrightarrow> (\<Sum>Basis) \<bullet> i = 1"
- by (simp add: inner_sum_left sum.If_cases inner_Basis)
-
lemma convex_set_plus:
assumes "convex S" and "convex T" shows "convex (S + T)"
proof -
--- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy Fri Mar 03 11:25:29 2023 +0100
+++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy Fri Mar 03 12:22:07 2023 +0000
@@ -895,6 +895,17 @@
by (rule bounded_subset)
qed
+lemma continuous_on_compact_bound:
+ assumes "compact A" "continuous_on A f"
+ obtains B where "B \<ge> 0" "\<And>x. x \<in> A \<Longrightarrow> norm (f x) \<le> B"
+proof -
+ have "compact (f ` A)" by (metis assms compact_continuous_image)
+ then obtain B where "\<forall>x\<in>A. norm (f x) \<le> B"
+ by (auto dest!: compact_imp_bounded simp: bounded_iff)
+ hence "max B 0 \<ge> 0" and "\<forall>x\<in>A. norm (f x) \<le> max B 0" by auto
+ thus ?thesis using that by blast
+qed
+
lemma closure_Int_ball_not_empty:
assumes "S \<subseteq> closure T" "x \<in> S" "r > 0"
shows "T \<inter> ball x r \<noteq> {}"
--- a/src/HOL/Analysis/Euclidean_Space.thy Fri Mar 03 11:25:29 2023 +0100
+++ b/src/HOL/Analysis/Euclidean_Space.thy Fri Mar 03 12:22:07 2023 +0000
@@ -53,6 +53,9 @@
lemma (in euclidean_space) sgn_Basis: "u \<in> Basis \<Longrightarrow> sgn u = u"
unfolding sgn_div_norm by (simp add: scaleR_one)
+lemma inner_sum_Basis[simp]: "i \<in> Basis \<Longrightarrow> inner (\<Sum>Basis) i = 1"
+ by (simp add: inner_sum_left sum.If_cases inner_Basis)
+
lemma (in euclidean_space) Basis_zero [simp]: "0 \<notin> Basis"
proof
assume "0 \<in> Basis" thus "False"
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Fri Mar 03 11:25:29 2023 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Fri Mar 03 12:22:07 2023 +0000
@@ -12,8 +12,7 @@
lemma norm_diff2: "\<lbrakk>y = y1 + y2; x = x1 + x2; e = e1 + e2; norm(y1 - x1) \<le> e1; norm(y2 - x2) \<le> e2\<rbrakk>
\<Longrightarrow> norm(y-x) \<le> e"
- using norm_triangle_mono [of "y1 - x1" "e1" "y2 - x2" "e2"]
- by (simp add: add_diff_add)
+ by (smt (verit, ccfv_SIG) norm_diff_triangle_ineq)
lemma setcomp_dot1: "{z. P (z \<bullet> (i,0))} = {(x,y). P(x \<bullet> i)}"
by auto
@@ -2326,11 +2325,9 @@
qed
lemma has_integral_spike_eq:
- assumes "negligible S"
- and gf: "\<And>x. x \<in> T - S \<Longrightarrow> g x = f x"
+ assumes "negligible S" and "\<And>x. x \<in> T - S \<Longrightarrow> g x = f x"
shows "(f has_integral y) T \<longleftrightarrow> (g has_integral y) T"
- using has_integral_spike [OF \<open>negligible S\<close>] gf
- by metis
+ by (metis assms has_integral_spike)
lemma integrable_spike:
assumes "f integrable_on T" "negligible S" "\<And>x. x \<in> T - S \<Longrightarrow> g x = f x"
@@ -4878,13 +4875,22 @@
lemma integrable_on_superset:
fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
- assumes "f integrable_on S"
- and "\<And>x. x \<notin> S \<Longrightarrow> f x = 0"
- and "S \<subseteq> t"
+ assumes "f integrable_on S" and "\<And>x. x \<notin> S \<Longrightarrow> f x = 0" and "S \<subseteq> t"
shows "f integrable_on t"
- using assms
- unfolding integrable_on_def
- by (auto intro:has_integral_on_superset)
+ by (meson assms has_integral_on_superset integrable_integral integrable_on_def)
+
+lemma integral_subset_negligible:
+ fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: banach"
+ assumes "S \<subseteq> T" "negligible (T - S)"
+ shows "integral S f = integral T f"
+proof -
+ have "integral T f = integral T (\<lambda>x. if x \<in> S then f x else 0)"
+ by (rule integral_spike[of "T - S"]) (use assms in auto)
+ also have "\<dots> = integral (S \<inter> T) f"
+ by (subst integral_restrict_Int) auto
+ also have "S \<inter> T = S" using assms by auto
+ finally show ?thesis ..
+qed
lemma integral_restrict_UNIV:
fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Fri Mar 03 11:25:29 2023 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Fri Mar 03 12:22:07 2023 +0000
@@ -840,6 +840,76 @@
by (metis assms continuous_on_compose continuous_on_swap swap_cbox_Pair)
qed
+lemma open_contains_cbox:
+ fixes x :: "'a :: euclidean_space"
+ assumes "open A" "x \<in> A"
+ obtains a b where "cbox a b \<subseteq> A" "x \<in> box a b" "\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i"
+proof -
+ from assms obtain R where R: "R > 0" "ball x R \<subseteq> A"
+ by (auto simp: open_contains_ball)
+ define r :: real where "r = R / (2 * sqrt DIM('a))"
+ from \<open>R > 0\<close> have [simp]: "r > 0" by (auto simp: r_def)
+ define d :: 'a where "d = r *\<^sub>R Topology_Euclidean_Space.One"
+ have "cbox (x - d) (x + d) \<subseteq> A"
+ proof safe
+ fix y assume y: "y \<in> cbox (x - d) (x + d)"
+ have "dist x y = sqrt (\<Sum>i\<in>Basis. (dist (x \<bullet> i) (y \<bullet> i))\<^sup>2)"
+ by (subst euclidean_dist_l2) (auto simp: L2_set_def)
+ also from y have "sqrt (\<Sum>i\<in>Basis. (dist (x \<bullet> i) (y \<bullet> i))\<^sup>2) \<le> sqrt (\<Sum>i\<in>(Basis::'a set). r\<^sup>2)"
+ by (intro real_sqrt_le_mono sum_mono power_mono)
+ (auto simp: dist_norm d_def cbox_def algebra_simps)
+ also have "\<dots> = sqrt (DIM('a) * r\<^sup>2)" by simp
+ also have "DIM('a) * r\<^sup>2 = (R / 2) ^ 2"
+ by (simp add: r_def power_divide)
+ also have "sqrt \<dots> = R / 2"
+ using \<open>R > 0\<close> by simp
+ also from \<open>R > 0\<close> have "\<dots> < R" by simp
+ finally have "y \<in> ball x R" by simp
+ with R show "y \<in> A" by blast
+ qed
+ thus ?thesis
+ using that[of "x - d" "x + d"] by (auto simp: algebra_simps d_def box_def)
+qed
+
+lemma open_contains_box:
+ fixes x :: "'a :: euclidean_space"
+ assumes "open A" "x \<in> A"
+ obtains a b where "box a b \<subseteq> A" "x \<in> box a b" "\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i"
+ by (meson assms box_subset_cbox dual_order.trans open_contains_cbox)
+
+lemma inner_image_box:
+ assumes "(i :: 'a :: euclidean_space) \<in> Basis"
+ assumes "\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i"
+ shows "(\<lambda>x. x \<bullet> i) ` box a b = {a \<bullet> i<..<b \<bullet> i}"
+proof safe
+ fix x assume x: "x \<in> {a \<bullet> i<..<b \<bullet> i}"
+ let ?y = "(\<Sum>j\<in>Basis. (if i = j then x else (a + b) \<bullet> j / 2) *\<^sub>R j)"
+ from x assms have "?y \<bullet> i \<in> (\<lambda>x. x \<bullet> i) ` box a b"
+ by (intro imageI) (auto simp: box_def algebra_simps)
+ also have "?y \<bullet> i = (\<Sum>j\<in>Basis. (if i = j then x else (a + b) \<bullet> j / 2) * (j \<bullet> i))"
+ by (simp add: inner_sum_left)
+ also have "\<dots> = (\<Sum>j\<in>Basis. if i = j then x else 0)"
+ by (intro sum.cong) (auto simp: inner_not_same_Basis assms)
+ also have "\<dots> = x" using assms by simp
+ finally show "x \<in> (\<lambda>x. x \<bullet> i) ` box a b" .
+qed (insert assms, auto simp: box_def)
+
+lemma inner_image_cbox:
+ assumes "(i :: 'a :: euclidean_space) \<in> Basis"
+ assumes "\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i"
+ shows "(\<lambda>x. x \<bullet> i) ` cbox a b = {a \<bullet> i..b \<bullet> i}"
+proof safe
+ fix x assume x: "x \<in> {a \<bullet> i..b \<bullet> i}"
+ let ?y = "(\<Sum>j\<in>Basis. (if i = j then x else a \<bullet> j) *\<^sub>R j)"
+ from x assms have "?y \<bullet> i \<in> (\<lambda>x. x \<bullet> i) ` cbox a b"
+ by (intro imageI) (auto simp: cbox_def)
+ also have "?y \<bullet> i = (\<Sum>j\<in>Basis. (if i = j then x else a \<bullet> j) * (j \<bullet> i))"
+ by (simp add: inner_sum_left)
+ also have "\<dots> = (\<Sum>j\<in>Basis. if i = j then x else 0)"
+ by (intro sum.cong) (auto simp: inner_not_same_Basis assms)
+ also have "\<dots> = x" using assms by simp
+ finally show "x \<in> (\<lambda>x. x \<bullet> i) ` cbox a b" .
+qed (insert assms, auto simp: cbox_def)
subsection \<open>General Intervals\<close>
--- a/src/HOL/Archimedean_Field.thy Fri Mar 03 11:25:29 2023 +0100
+++ b/src/HOL/Archimedean_Field.thy Fri Mar 03 12:22:07 2023 +0000
@@ -417,33 +417,7 @@
lemma floor_divide_of_nat_eq: "\<lfloor>of_nat m / of_nat n\<rfloor> = of_nat (m div n)"
for m n :: nat
-proof (cases "n = 0")
- case True
- then show ?thesis by simp
-next
- case False
- then have *: "\<lfloor>of_nat (m mod n) / of_nat n :: 'a\<rfloor> = 0"
- by (auto intro: floor_unique)
- have "(of_nat m :: 'a) = of_nat (m div n * n + m mod n)"
- by simp
- also have "\<dots> = (of_nat (m div n) + of_nat (m mod n) / of_nat n) * of_nat n"
- using False by (simp only: of_nat_add) (simp add: field_simps)
- finally have "(of_nat m / of_nat n :: 'a) = \<dots> / of_nat n"
- by simp
- then have "(of_nat m / of_nat n :: 'a) = of_nat (m div n) + of_nat (m mod n) / of_nat n"
- using False by (simp only:) simp
- then have "\<lfloor>of_nat m / of_nat n :: 'a\<rfloor> = \<lfloor>of_nat (m div n) + of_nat (m mod n) / of_nat n :: 'a\<rfloor>"
- by simp
- then have "\<lfloor>of_nat m / of_nat n :: 'a\<rfloor> = \<lfloor>of_nat (m mod n) / of_nat n + of_nat (m div n) :: 'a\<rfloor>"
- by (simp add: ac_simps)
- moreover have "(of_nat (m div n) :: 'a) = of_int (of_nat (m div n))"
- by simp
- ultimately have "\<lfloor>of_nat m / of_nat n :: 'a\<rfloor> =
- \<lfloor>of_nat (m mod n) / of_nat n :: 'a\<rfloor> + of_nat (m div n)"
- by (simp only: floor_add_int)
- with * show ?thesis
- by simp
-qed
+ by (metis floor_divide_of_int_eq of_int_of_nat_eq unique_euclidean_semiring_with_nat_class.of_nat_div)
lemma floor_divide_lower:
fixes q :: "'a::floor_ceiling"
--- a/src/HOL/Complex_Analysis/Contour_Integration.thy Fri Mar 03 11:25:29 2023 +0100
+++ b/src/HOL/Complex_Analysis/Contour_Integration.thy Fri Mar 03 12:22:07 2023 +0000
@@ -23,7 +23,7 @@
subsection\<open>Definition\<close>
text\<open>
- This definition is for complex numbers only, and does not generalise to
+ This definition is for complex numbers only, and does not generalise to
line integrals in a vector field
\<close>
@@ -92,6 +92,47 @@
(\<lambda>t. f(g t) * vector_derivative g (at t)) integrable_on {0..1}"
by (simp add: has_contour_integral integrable_on_def contour_integrable_on_def)
+lemma has_contour_integral_mirror_iff:
+ assumes "valid_path g"
+ shows "(f has_contour_integral I) (-g) \<longleftrightarrow> ((\<lambda>x. -f (- x)) has_contour_integral I) g"
+proof -
+ from assms have "g piecewise_differentiable_on {0..1}"
+ by (auto simp: valid_path_def piecewise_C1_imp_differentiable)
+ then obtain S where "finite S" and S: "\<And>x. x \<in> {0..1} - S \<Longrightarrow> g differentiable at x within {0..1}"
+ unfolding piecewise_differentiable_on_def by blast
+ have S': "g differentiable at x" if "x \<in> {0..1} - ({0, 1} \<union> S)" for x
+ proof -
+ from that have "x \<in> interior {0..1}" by auto
+ with S[of x] that show ?thesis by (auto simp: at_within_interior[of _ "{0..1}"])
+ qed
+
+ have "(f has_contour_integral I) (-g) \<longleftrightarrow>
+ ((\<lambda>x. f (- g x) * vector_derivative (-g) (at x)) has_integral I) {0..1}"
+ by (simp add: has_contour_integral)
+ also have "\<dots> \<longleftrightarrow> ((\<lambda>x. -f (- g x) * vector_derivative g (at x)) has_integral I) {0..1}"
+ by (intro has_integral_spike_finite_eq[of "S \<union> {0, 1}"])
+ (insert \<open>finite S\<close> S', auto simp: o_def fun_Compl_def)
+ also have "\<dots> \<longleftrightarrow> ((\<lambda>x. -f (-x)) has_contour_integral I) g"
+ by (simp add: has_contour_integral)
+ finally show ?thesis .
+qed
+
+lemma contour_integral_on_mirror_iff:
+ assumes "valid_path g"
+ shows "f contour_integrable_on (-g) \<longleftrightarrow> (\<lambda>x. -f (- x)) contour_integrable_on g"
+ by (auto simp: contour_integrable_on_def has_contour_integral_mirror_iff assms)
+
+lemma contour_integral_mirror:
+ assumes "valid_path g"
+ shows "contour_integral (-g) f = contour_integral g (\<lambda>x. -f (- x))"
+proof (cases "f contour_integrable_on (-g)")
+ case True with contour_integral_unique assms show ?thesis
+ by (auto simp: contour_integrable_on_def has_contour_integral_mirror_iff)
+next
+ case False then show ?thesis
+ by (simp add: assms contour_integral_on_mirror_iff not_integrable_contour_integral)
+qed
+
subsection\<^marker>\<open>tag unimportant\<close> \<open>Reversing a path\<close>
lemma has_contour_integral_reversepath:
@@ -170,12 +211,12 @@
has_integral_affinity01 [OF 2, where m= 2 and c="-1", THEN has_integral_cmul [where c=2]]
by (simp_all only: image_affinity_atLeastAtMost_div_diff, simp_all add: scaleR_conv_of_real mult_ac)
have g1: "vector_derivative (\<lambda>x. if x*2 \<le> 1 then g1 (2*x) else g2 (2*x - 1)) (at z) =
- 2 *\<^sub>R vector_derivative g1 (at (z*2))"
+ 2 *\<^sub>R vector_derivative g1 (at (z*2))"
if "0 \<le> z" "z*2 < 1" "z*2 \<notin> s1" for z
proof (rule vector_derivative_at [OF has_vector_derivative_transform_within])
show "0 < \<bar>z - 1/2\<bar>"
using that by auto
- have "((*) 2 has_vector_derivative 2) (at z)"
+ have "((*) 2 has_vector_derivative 2) (at z)"
by (simp add: has_vector_derivative_def has_derivative_def bounded_linear_mult_left)
moreover have "(g1 has_vector_derivative vector_derivative g1 (at (z * 2))) (at (2 * z))"
using s1 that by (auto simp: algebra_simps vector_derivative_works)
@@ -185,7 +226,7 @@
qed (use that in \<open>simp_all add: dist_real_def abs_if split: if_split_asm\<close>)
have g2: "vector_derivative (\<lambda>x. if x*2 \<le> 1 then g1 (2*x) else g2 (2*x - 1)) (at z) =
- 2 *\<^sub>R vector_derivative g2 (at (z*2 - 1))"
+ 2 *\<^sub>R vector_derivative g2 (at (z*2 - 1))"
if "1 < z*2" "z \<le> 1" "z*2 - 1 \<notin> s2" for z
proof (rule vector_derivative_at [OF has_vector_derivative_transform_within])
show "0 < \<bar>z - 1/2\<bar>"
@@ -234,7 +275,7 @@
then have *: "(\<lambda>x. (f ((g1 +++ g2) (x/2))/2) * vector_derivative (g1 +++ g2) (at (x/2))) integrable_on {0..1}"
by (auto dest: integrable_cmul [where c="1/2"] simp: scaleR_conv_of_real)
have g1: "vector_derivative (\<lambda>x. if x*2 \<le> 1 then g1 (2*x) else g2 (2*x - 1)) (at (z/2)) =
- 2 *\<^sub>R vector_derivative g1 (at z)"
+ 2 *\<^sub>R vector_derivative g1 (at z)"
if "0 < z" "z < 1" "z \<notin> s1" for z
proof (rule vector_derivative_at [OF has_vector_derivative_transform_within])
show "0 < \<bar>(z - 1)/2\<bar>"
@@ -261,14 +302,14 @@
where s2: "finite s2" "\<forall>x\<in>{0..1} - s2. g2 differentiable at x"
using assms by (auto simp: valid_path_def piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
have "(\<lambda>x. f ((g1 +++ g2) (x/2 + 1/2)) * vector_derivative (g1 +++ g2) (at (x/2 + 1/2))) integrable_on {0..1}"
- using assms integrable_affinity [of _ "1/2::real" 1 "1/2" "1/2"]
+ using assms integrable_affinity [of _ "1/2::real" 1 "1/2" "1/2"]
integrable_on_subcbox [where a="1/2" and b=1]
by (fastforce simp: contour_integrable_on image_affinity_atLeastAtMost_diff)
then have *: "(\<lambda>x. (f ((g1 +++ g2) (x/2 + 1/2))/2) * vector_derivative (g1 +++ g2) (at (x/2 + 1/2)))
integrable_on {0..1}"
by (auto dest: integrable_cmul [where c="1/2"] simp: scaleR_conv_of_real)
have g2: "vector_derivative (\<lambda>x. if x*2 \<le> 1 then g1 (2*x) else g2 (2*x - 1)) (at (z/2+1/2)) =
- 2 *\<^sub>R vector_derivative g2 (at z)"
+ 2 *\<^sub>R vector_derivative g2 (at z)"
if "0 < z" "z < 1" "z \<notin> s2" for z
proof (rule vector_derivative_at [OF has_vector_derivative_transform_within])
show "0 < \<bar>z/2\<bar>"
@@ -600,6 +641,22 @@
unfolding contour_integral_integral using assms
by (intro integral_cong) (auto simp: path_image_def)
+lemma contour_integral_spike_finite_simple_path:
+ assumes "finite A" "simple_path g" "g = g'" "\<And>x. x \<in> path_image g - A \<Longrightarrow> f x = f' x"
+ shows "contour_integral g f = contour_integral g' f'"
+ unfolding contour_integral_integral
+proof (rule integral_spike)
+ have "finite (g -` A \<inter> {0<..<1})" using \<open>simple_path g\<close> \<open>finite A\<close>
+ by (intro finite_vimage_IntI simple_path_inj_on) auto
+ hence "finite ({0, 1} \<union> g -` A \<inter> {0<..<1})" by auto
+ thus "negligible ({0, 1} \<union> g -` A \<inter> {0<..<1})" by (rule negligible_finite)
+next
+ fix x assume "x \<in> {0..1} - ({0, 1} \<union> g -` A \<inter> {0<..<1})"
+ hence "g x \<in> path_image g - A" by (auto simp: path_image_def)
+ from assms(4)[OF this] and assms(3)
+ show "f' (g' x) * vector_derivative g' (at x) = f (g x) * vector_derivative g (at x)" by simp
+ qed
+
text \<open>Contour integral along a segment on the real axis\<close>
@@ -619,7 +676,7 @@
also have "(\<lambda>x. f (a + b * of_real x - a * of_real x)) =
(\<lambda>x. (f (a + b * of_real x - a * of_real x) * (b - a)) /\<^sub>R (Re b - Re a))"
using \<open>a \<noteq> b\<close> by (auto simp: field_simps fun_eq_iff scaleR_conv_of_real)
- also have "(\<dots> has_integral I /\<^sub>R (Re b - Re a)) {0..1} \<longleftrightarrow>
+ also have "(\<dots> has_integral I /\<^sub>R (Re b - Re a)) {0..1} \<longleftrightarrow>
((\<lambda>x. f (linepath a b x) * (b - a)) has_integral I) {0..1}" using assms
by (subst has_integral_cmul_iff) (auto simp: linepath_def scaleR_conv_of_real algebra_simps)
also have "\<dots> \<longleftrightarrow> (f has_contour_integral I) (linepath a b)" unfolding has_contour_integral_def
@@ -846,8 +903,7 @@
"\<lbrakk>f contour_integrable_on (linepath a b);
0 \<le> B; \<And>x. x \<in> closed_segment a b \<Longrightarrow> norm(f x) \<le> B\<rbrakk>
\<Longrightarrow> norm(contour_integral (linepath a b) f) \<le> B*norm(b - a)"
- using has_contour_integral_bound_linepath [of f]
- by (auto simp: has_contour_integral_integral)
+ by (meson has_contour_integral_bound_linepath has_contour_integral_integral)
lemma contour_integral_0 [simp]: "contour_integral g (\<lambda>x. 0) = 0"
by (simp add: contour_integral_unique has_contour_integral_0)
@@ -900,6 +956,10 @@
unfolding contour_integrable_on_def
by (metis has_contour_integral_sum)
+lemma contour_integrable_neg_iff:
+ "(\<lambda>x. -f x) contour_integrable_on g \<longleftrightarrow> f contour_integrable_on g"
+ using contour_integrable_neg[of f g] contour_integrable_neg[of "\<lambda>x. -f x" g] by auto
+
lemma contour_integrable_lmul_iff:
"c \<noteq> 0 \<Longrightarrow> (\<lambda>x. c * f x) contour_integrable_on g \<longleftrightarrow> f contour_integrable_on g"
using contour_integrable_lmul[of f g c] contour_integrable_lmul[of "\<lambda>x. c * f x" g "inverse c"]
@@ -952,8 +1012,8 @@
then have "\<And>x. ((k - x) / k) *\<^sub>R a + (x / k) *\<^sub>R c = (1 - x) *\<^sub>R a + x *\<^sub>R b"
using False by (simp add: c' algebra_simps)
then have "((\<lambda>x. f ((1 - x) *\<^sub>R a + x *\<^sub>R b) * (b - a)) has_integral i) {0..k}"
- using k has_integral_affinity01 [OF *, of "inverse k" "0"]
- by (force dest: has_integral_cmul [where c = "inverse k"]
+ using k has_integral_affinity01 [OF *, of "inverse k" "0"]
+ by (force dest: has_integral_cmul [where c = "inverse k"]
simp add: divide_simps mult.commute [of _ "k"] image_affinity_atLeastAtMost c)
} note fi = this
{ assume *: "((\<lambda>x. f ((1 - x) *\<^sub>R c + x *\<^sub>R b) * (b - c)) has_integral j) {0..1}"
@@ -1148,9 +1208,9 @@
lemma reversepath_part_circlepath[simp]:
"reversepath (part_circlepath z r s t) = part_circlepath z r t s"
- unfolding part_circlepath_def reversepath_def linepath_def
+ unfolding part_circlepath_def reversepath_def linepath_def
by (auto simp:algebra_simps)
-
+
lemma has_vector_derivative_part_circlepath [derivative_intros]:
"((part_circlepath z r s t) has_vector_derivative
(\<i> * r * (of_real t - of_real s) * exp(\<i> * linepath s t x)))
@@ -1209,7 +1269,7 @@
lemma path_image_part_circlepath':
"path_image (part_circlepath z r s t) = (\<lambda>x. z + r * cis x) ` closed_segment s t"
proof -
- have "path_image (part_circlepath z r s t) =
+ have "path_image (part_circlepath z r s t) =
(\<lambda>x. z + r * exp(\<i> * of_real x)) ` linepath s t ` {0..1}"
by (simp add: image_image path_image_def part_circlepath_def)
also have "linepath s t ` {0..1} = closed_segment s t"
@@ -1283,7 +1343,7 @@
(simp_all add: cis_conv_exp)
also have "\<dots> \<longleftrightarrow> ((\<lambda>x. f (c + r * exp (\<i> * linepath (of_real a) (of_real b) x)) *
r * \<i> * exp (\<i> * linepath (of_real a) (of_real b) x) *
- vector_derivative (linepath (of_real a) (of_real b))
+ vector_derivative (linepath (of_real a) (of_real b))
(at x within {0..1})) has_integral I) {0..1}"
by (intro has_integral_cong, subst vector_derivative_linepath_within)
(auto simp: part_circlepath_def cis_conv_exp of_real_linepath [symmetric])
@@ -1299,7 +1359,7 @@
assumes "a < b"
shows "f contour_integrable_on (part_circlepath c r a b) \<longleftrightarrow>
(\<lambda>t. f (c + r * cis t) * r * \<i> * cis t) integrable_on {a..b}"
- using assms by (auto simp: contour_integrable_on_def integrable_on_def
+ using assms by (auto simp: contour_integrable_on_def integrable_on_def
has_contour_integral_part_circlepath_iff)
lemma contour_integral_part_circlepath_eq:
@@ -1308,14 +1368,14 @@
integral {a..b} (\<lambda>t. f (c + r * cis t) * r * \<i> * cis t)"
proof (cases "f contour_integrable_on part_circlepath c r a b")
case True
- hence "(\<lambda>t. f (c + r * cis t) * r * \<i> * cis t) integrable_on {a..b}"
+ hence "(\<lambda>t. f (c + r * cis t) * r * \<i> * cis t) integrable_on {a..b}"
using assms by (simp add: contour_integrable_part_circlepath_iff)
with True show ?thesis
using has_contour_integral_part_circlepath_iff[OF assms]
contour_integral_unique has_integral_integrable_integral by blast
next
case False
- hence "\<not>(\<lambda>t. f (c + r * cis t) * r * \<i> * cis t) integrable_on {a..b}"
+ hence "\<not>(\<lambda>t. f (c + r * cis t) * r * \<i> * cis t) integrable_on {a..b}"
using assms by (simp add: contour_integrable_part_circlepath_iff)
with False show ?thesis
by (simp add: not_integrable_contour_integral not_integrable_integral)
@@ -1323,10 +1383,10 @@
lemma contour_integral_part_circlepath_reverse:
"contour_integral (part_circlepath c r a b) f = -contour_integral (part_circlepath c r b a) f"
- by (subst reversepath_part_circlepath [symmetric], subst contour_integral_reversepath) simp_all
+ by (metis contour_integral_reversepath reversepath_part_circlepath valid_path_part_circlepath)
lemma contour_integral_part_circlepath_reverse':
- "b < a \<Longrightarrow> contour_integral (part_circlepath c r a b) f =
+ "b < a \<Longrightarrow> contour_integral (part_circlepath c r a b) f =
-contour_integral (part_circlepath c r b a) f"
by (rule contour_integral_part_circlepath_reverse)
@@ -1382,7 +1442,7 @@
proof -
let ?w = "(y - z)/of_real r / exp(\<i> * of_real s)"
have fin: "finite (of_real -` {z. cmod z \<le> 1 \<and> exp (\<i> * complex_of_real (t - s) * z) = ?w})"
- using \<open>s < t\<close>
+ using \<open>s < t\<close>
by (intro finite_vimageI [OF finite_bounded_log2]) (auto simp: inj_of_real)
show ?thesis
unfolding part_circlepath_def linepath_def vimage_def
@@ -1396,13 +1456,20 @@
vector_derivative (part_circlepath z r s t) (at x)) has_integral i) {0..1}"
by (rule has_integral_spike [OF negligible_finite [OF fin01]]) (use fi has_contour_integral in auto)
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])
+ by (auto intro!: B [unfolded path_image_def image_def])
show ?thesis
apply (rule has_integral_bound [where 'a=real, simplified, OF _ **, simplified])
using assms le * "2" \<open>r > 0\<close> by (auto simp add: norm_mult vector_derivative_part_circlepath)
qed
qed
+corollary contour_integral_bound_part_circlepath_strong:
+ assumes "f contour_integrable_on part_circlepath z r s t"
+ and "finite k" and "0 \<le> B" "0 < r" "s \<le> t"
+ and "\<And>x. x \<in> path_image(part_circlepath z r s t) - k \<Longrightarrow> norm(f x) \<le> B"
+ shows "cmod (contour_integral (part_circlepath z r s t) f) \<le> B * r * (t - s)"
+ using assms has_contour_integral_bound_part_circlepath_strong has_contour_integral_integral by blast
+
lemma 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;
@@ -1414,9 +1481,8 @@
"continuous_on (path_image (part_circlepath z r s t)) f
\<Longrightarrow> f contour_integrable_on (part_circlepath z r s t)"
unfolding 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
+ by (best intro: integrable_continuous_real path_part_circlepath [unfolded path_def] continuous_intros
+ continuous_on_compose2 [where g=f, OF _ _ order_refl])
lemma simple_path_part_circlepath:
"simple_path(part_circlepath z r s t) \<longleftrightarrow> (r \<noteq> 0 \<and> s \<noteq> t \<and> \<bar>s - t\<bar> \<le> 2*pi)"
@@ -1686,7 +1752,7 @@
then show ?thesis
by (simp add: left_diff_distrib [symmetric] norm_mult)
qed
- have le_e: "\<And>x. \<lbrakk>\<forall>xa\<in>{0..1}. 2 * cmod (f x (\<gamma> xa) - l (\<gamma> xa)) < e / B'; f x contour_integrable_on \<gamma>\<rbrakk>
+ have le_e: "\<And>x. \<lbrakk>\<forall>u\<in>{0..1}. 2 * cmod (f x (\<gamma> u) - l (\<gamma> u)) < e / B'; f x contour_integrable_on \<gamma>\<rbrakk>
\<Longrightarrow> cmod (integral {0..1}
(\<lambda>u. f x (\<gamma> u) * vector_derivative \<gamma> (at u) - l (\<gamma> u) * vector_derivative \<gamma> (at u))) < e"
apply (rule le_less_trans [OF integral_norm_bound_integral ie])
@@ -1711,4 +1777,4 @@
"((\<lambda>n. contour_integral (circlepath z r) (f n)) \<longlongrightarrow> contour_integral (circlepath z r) l) F"
using assms by (auto simp: vector_derivative_circlepath norm_mult intro!: contour_integral_uniform_limit)
-end
\ No newline at end of file
+end
--- a/src/HOL/Library/Landau_Symbols.thy Fri Mar 03 11:25:29 2023 +0100
+++ b/src/HOL/Library/Landau_Symbols.thy Fri Mar 03 12:22:07 2023 +0000
@@ -1499,6 +1499,21 @@
shows "(\<lambda>x. sum (\<lambda>y. f y x) A) \<in> O[F](g)"
using assms by (induction A rule: infinite_finite_induct) (auto intro: sum_in_bigo)
+lemma le_imp_bigo_real:
+ assumes "c \<ge> 0" "eventually (\<lambda>x. f x \<le> c * (g x :: real)) F" "eventually (\<lambda>x. 0 \<le> f x) F"
+ shows "f \<in> O[F](g)"
+proof -
+ have "eventually (\<lambda>x. norm (f x) \<le> c * norm (g x)) F"
+ using assms(2,3)
+ proof eventually_elim
+ case (elim x)
+ have "norm (f x) \<le> c * g x" using elim by simp
+ also have "\<dots> \<le> c * norm (g x)" by (intro mult_left_mono assms) auto
+ finally show ?case .
+ qed
+ thus ?thesis by (intro bigoI[of _ c]) auto
+qed
+
context landau_symbol
begin
@@ -2052,6 +2067,17 @@
shows "(\<lambda>x. f1 x / f2 x) \<sim>[F] (\<lambda>x. g1 x / g2 x)"
using asymp_equiv_mult[OF assms(1) asymp_equiv_inverse[OF assms(2)]] by (simp add: field_simps)
+lemma asymp_equivD_strong:
+ assumes "f \<sim>[F] g" "eventually (\<lambda>x. f x \<noteq> 0 \<or> g x \<noteq> 0) F"
+ shows "((\<lambda>x. f x / g x) \<longlongrightarrow> 1) F"
+proof -
+ from assms(1) have "((\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else f x / g x) \<longlongrightarrow> 1) F"
+ by (rule asymp_equivD)
+ also have "?this \<longleftrightarrow> ?thesis"
+ by (intro filterlim_cong eventually_mono[OF assms(2)]) auto
+ finally show ?thesis .
+qed
+
lemma asymp_equiv_compose [asymp_equiv_intros]:
assumes "f \<sim>[G] g" "filterlim h G F"
shows "f \<circ> h \<sim>[F] g \<circ> h"
--- a/src/HOL/Real.thy Fri Mar 03 11:25:29 2023 +0100
+++ b/src/HOL/Real.thy Fri Mar 03 12:22:07 2023 +0000
@@ -1067,11 +1067,7 @@
by (metis floor_divide_of_nat_eq of_int_floor_le of_int_of_nat_eq)
lemma real_of_nat_div3: "real n / real x - real (n div x) \<le> 1" for n x :: nat
-proof (cases "x = 0")
- case False
- then show ?thesis
- by (metis of_int_of_nat_eq real_of_int_div3 zdiv_int)
-qed auto
+ by (metis of_int_of_nat_eq real_of_int_div3 of_nat_div)
lemma real_of_nat_div4: "real (n div x) \<le> real n / real x" for n x :: nat
using real_of_nat_div2 [of n x] by simp
--- a/src/HOL/Series.thy Fri Mar 03 11:25:29 2023 +0100
+++ b/src/HOL/Series.thy Fri Mar 03 12:22:07 2023 +0000
@@ -1023,6 +1023,17 @@
for f :: "nat \<Rightarrow> real"
by (fold real_norm_def) (rule summable_norm)
+lemma norm_suminf_le:
+ assumes "\<And>n. norm (f n :: 'a :: banach) \<le> g n" "summable g"
+ shows "norm (suminf f) \<le> suminf g"
+proof -
+ have *: "summable (\<lambda>n. norm (f n))"
+ using assms summable_norm_comparison_test by blast
+ hence "norm (suminf f) \<le> (\<Sum>n. norm (f n))" by (intro summable_norm) auto
+ also have "\<dots> \<le> suminf g" by (intro suminf_le * assms allI)
+ finally show ?thesis .
+qed
+
lemma summable_zero_power [simp]: "summable (\<lambda>n. 0 ^ n :: 'a::{comm_ring_1,topological_space})"
proof -
have "(\<lambda>n. 0 ^ n :: 'a) = (\<lambda>n. if n = 0 then 0^0 else 0)"
@@ -1054,12 +1065,7 @@
qed
lemma summable_0_powser: "summable (\<lambda>n. f n * 0 ^ n :: 'a::real_normed_div_algebra)"
-proof -
- have A: "(\<lambda>n. f n * 0 ^ n) = (\<lambda>n. if n = 0 then f n else 0)"
- by (intro ext) auto
- then show ?thesis
- by (subst A) simp_all
-qed
+ by simp
lemma summable_powser_split_head:
"summable (\<lambda>n. f (Suc n) * z ^ n :: 'a::real_normed_div_algebra) = summable (\<lambda>n. f n * z ^ n)"
--- a/src/HOL/Transcendental.thy Fri Mar 03 11:25:29 2023 +0100
+++ b/src/HOL/Transcendental.thy Fri Mar 03 12:22:07 2023 +0000
@@ -2492,6 +2492,9 @@
for a x :: "'a::{ln,real_normed_field}"
by (simp add: divide_inverse powr_minus)
+lemma powr_sum: "x \<noteq> 0 \<Longrightarrow> finite A \<Longrightarrow> x powr sum f A = (\<Prod>y\<in>A. x powr f y)"
+ by (simp add: powr_def exp_sum sum_distrib_right)
+
lemma divide_powr_uminus: "a / b powr c = a * b powr (- c)"
for a b c :: real
by (simp add: powr_minus_divide)