src/HOL/Analysis/Cauchy_Integral_Theorem.thy
 author wenzelm Mon Mar 25 17:21:26 2019 +0100 (4 weeks ago) changeset 69981 3dced198b9ec parent 69922 4a9167f377b0 child 70136 f03a01a18c6e permissions -rw-r--r--
more strict AFP properties;
 nipkow@69517 ` 1` ```section \Complex Path Integrals and Cauchy's Integral Theorem\ ``` lp15@60809 ` 2` lp15@61711 ` 3` ```text\By John Harrison et al. Ported from HOL Light by L C Paulson (2015)\ ``` lp15@61711 ` 4` hoelzl@63594 ` 5` ```theory Cauchy_Integral_Theorem ``` hoelzl@63594 ` 6` ```imports Complex_Transcendental Weierstrass_Theorems Ordered_Euclidean_Space ``` lp15@60809 ` 7` ```begin ``` lp15@60809 ` 8` wl302@69423 ` 9` ```subsection%unimportant \Homeomorphisms of arc images\ ``` lp15@62620 ` 10` lp15@62620 ` 11` ```lemma homeomorphism_arc: ``` lp15@62620 ` 12` ``` fixes g :: "real \ 'a::t2_space" ``` lp15@62620 ` 13` ``` assumes "arc g" ``` lp15@62620 ` 14` ``` obtains h where "homeomorphism {0..1} (path_image g) g h" ``` lp15@68339 ` 15` ```using assms by (force simp: arc_def homeomorphism_compact path_def path_image_def) ``` lp15@62620 ` 16` lp15@62620 ` 17` ```lemma homeomorphic_arc_image_interval: ``` lp15@62620 ` 18` ``` fixes g :: "real \ 'a::t2_space" and a::real ``` lp15@62620 ` 19` ``` assumes "arc g" "a < b" ``` lp15@62620 ` 20` ``` shows "(path_image g) homeomorphic {a..b}" ``` lp15@62620 ` 21` ```proof - ``` lp15@62620 ` 22` ``` have "(path_image g) homeomorphic {0..1::real}" ``` lp15@62620 ` 23` ``` by (meson assms(1) homeomorphic_def homeomorphic_sym homeomorphism_arc) ``` lp15@68339 ` 24` ``` also have "\ homeomorphic {a..b}" ``` lp15@62620 ` 25` ``` using assms by (force intro: homeomorphic_closed_intervals_real) ``` lp15@62620 ` 26` ``` finally show ?thesis . ``` lp15@62620 ` 27` ```qed ``` lp15@62620 ` 28` lp15@62620 ` 29` ```lemma homeomorphic_arc_images: ``` lp15@62620 ` 30` ``` fixes g :: "real \ 'a::t2_space" and h :: "real \ 'b::t2_space" ``` lp15@62620 ` 31` ``` assumes "arc g" "arc h" ``` lp15@62620 ` 32` ``` shows "(path_image g) homeomorphic (path_image h)" ``` lp15@62620 ` 33` ```proof - ``` lp15@62620 ` 34` ``` have "(path_image g) homeomorphic {0..1::real}" ``` lp15@62620 ` 35` ``` by (meson assms homeomorphic_def homeomorphic_sym homeomorphism_arc) ``` lp15@68339 ` 36` ``` also have "\ homeomorphic (path_image h)" ``` lp15@62620 ` 37` ``` by (meson assms homeomorphic_def homeomorphism_arc) ``` lp15@62620 ` 38` ``` finally show ?thesis . ``` lp15@62620 ` 39` ```qed ``` lp15@62620 ` 40` lp15@65037 ` 41` ```lemma path_connected_arc_complement: ``` lp15@65037 ` 42` ``` fixes \ :: "real \ 'a::euclidean_space" ``` lp15@65037 ` 43` ``` assumes "arc \" "2 \ DIM('a)" ``` lp15@65037 ` 44` ``` shows "path_connected(- path_image \)" ``` lp15@65037 ` 45` ```proof - ``` lp15@65037 ` 46` ``` have "path_image \ homeomorphic {0..1::real}" ``` lp15@65037 ` 47` ``` by (simp add: assms homeomorphic_arc_image_interval) ``` lp15@65037 ` 48` ``` then ``` lp15@65037 ` 49` ``` show ?thesis ``` lp15@65037 ` 50` ``` apply (rule path_connected_complement_homeomorphic_convex_compact) ``` lp15@65037 ` 51` ``` apply (auto simp: assms) ``` lp15@65037 ` 52` ``` done ``` lp15@65037 ` 53` ```qed ``` lp15@65037 ` 54` lp15@65037 ` 55` ```lemma connected_arc_complement: ``` lp15@65037 ` 56` ``` fixes \ :: "real \ 'a::euclidean_space" ``` lp15@65037 ` 57` ``` assumes "arc \" "2 \ DIM('a)" ``` lp15@65037 ` 58` ``` shows "connected(- path_image \)" ``` lp15@65037 ` 59` ``` by (simp add: assms path_connected_arc_complement path_connected_imp_connected) ``` lp15@65037 ` 60` lp15@65037 ` 61` ```lemma inside_arc_empty: ``` lp15@65037 ` 62` ``` fixes \ :: "real \ 'a::euclidean_space" ``` lp15@65037 ` 63` ``` assumes "arc \" ``` lp15@65037 ` 64` ``` shows "inside(path_image \) = {}" ``` lp15@65037 ` 65` ```proof (cases "DIM('a) = 1") ``` lp15@65037 ` 66` ``` case True ``` lp15@65037 ` 67` ``` then show ?thesis ``` lp15@65037 ` 68` ``` using assms connected_arc_image connected_convex_1_gen inside_convex by blast ``` lp15@65037 ` 69` ```next ``` lp15@65037 ` 70` ``` case False ``` lp15@65037 ` 71` ``` show ?thesis ``` lp15@65037 ` 72` ``` proof (rule inside_bounded_complement_connected_empty) ``` lp15@65037 ` 73` ``` show "connected (- path_image \)" ``` lp15@65037 ` 74` ``` apply (rule connected_arc_complement [OF assms]) ``` lp15@65037 ` 75` ``` using False ``` lp15@65037 ` 76` ``` by (metis DIM_ge_Suc0 One_nat_def Suc_1 not_less_eq_eq order_class.order.antisym) ``` lp15@65037 ` 77` ``` show "bounded (path_image \)" ``` lp15@65037 ` 78` ``` by (simp add: assms bounded_arc_image) ``` lp15@65037 ` 79` ``` qed ``` lp15@65037 ` 80` ```qed ``` lp15@65037 ` 81` lp15@65037 ` 82` ```lemma inside_simple_curve_imp_closed: ``` lp15@65037 ` 83` ``` fixes \ :: "real \ 'a::euclidean_space" ``` lp15@65037 ` 84` ``` shows "\simple_path \; x \ inside(path_image \)\ \ pathfinish \ = pathstart \" ``` lp15@65037 ` 85` ``` using arc_simple_path inside_arc_empty by blast ``` lp15@65037 ` 86` lp15@68493 ` 87` wl302@69423 ` 88` ```subsection%unimportant \Piecewise differentiable functions\ ``` lp15@60809 ` 89` lp15@60809 ` 90` ```definition piecewise_differentiable_on ``` lp15@60809 ` 91` ``` (infixr "piecewise'_differentiable'_on" 50) ``` lp15@60809 ` 92` ``` where "f piecewise_differentiable_on i \ ``` lp15@60809 ` 93` ``` continuous_on i f \ ``` lp15@68284 ` 94` ``` (\S. finite S \ (\x \ i - S. f differentiable (at x within i)))" ``` lp15@60809 ` 95` lp15@60809 ` 96` ```lemma piecewise_differentiable_on_imp_continuous_on: ``` lp15@68284 ` 97` ``` "f piecewise_differentiable_on S \ continuous_on S f" ``` lp15@60809 ` 98` ```by (simp add: piecewise_differentiable_on_def) ``` lp15@60809 ` 99` lp15@60809 ` 100` ```lemma piecewise_differentiable_on_subset: ``` lp15@68284 ` 101` ``` "f piecewise_differentiable_on S \ T \ S \ f piecewise_differentiable_on T" ``` lp15@60809 ` 102` ``` using continuous_on_subset ``` lp15@61190 ` 103` ``` unfolding piecewise_differentiable_on_def ``` lp15@61190 ` 104` ``` apply safe ``` lp15@68339 ` 105` ``` apply (blast elim: continuous_on_subset) ``` lp15@61190 ` 106` ``` by (meson Diff_iff differentiable_within_subset subsetCE) ``` lp15@60809 ` 107` lp15@60809 ` 108` ```lemma differentiable_on_imp_piecewise_differentiable: ``` lp15@60809 ` 109` ``` fixes a:: "'a::{linorder_topology,real_normed_vector}" ``` lp15@60809 ` 110` ``` shows "f differentiable_on {a..b} \ f piecewise_differentiable_on {a..b}" ``` lp15@60809 ` 111` ``` apply (simp add: piecewise_differentiable_on_def differentiable_imp_continuous_on) ``` lp15@61190 ` 112` ``` apply (rule_tac x="{a,b}" in exI, simp add: differentiable_on_def) ``` lp15@61190 ` 113` ``` done ``` lp15@60809 ` 114` lp15@60809 ` 115` ```lemma differentiable_imp_piecewise_differentiable: ``` lp15@68284 ` 116` ``` "(\x. x \ S \ f differentiable (at x within S)) ``` lp15@68284 ` 117` ``` \ f piecewise_differentiable_on S" ``` lp15@61190 ` 118` ```by (auto simp: piecewise_differentiable_on_def differentiable_imp_continuous_on differentiable_on_def ``` lp15@61190 ` 119` ``` intro: differentiable_within_subset) ``` lp15@60809 ` 120` lp15@68284 ` 121` ```lemma piecewise_differentiable_const [iff]: "(\x. z) piecewise_differentiable_on S" ``` paulson@61204 ` 122` ``` by (simp add: differentiable_imp_piecewise_differentiable) ``` paulson@61204 ` 123` lp15@60809 ` 124` ```lemma piecewise_differentiable_compose: ``` lp15@68284 ` 125` ``` "\f piecewise_differentiable_on S; g piecewise_differentiable_on (f ` S); ``` lp15@68284 ` 126` ``` \x. finite (S \ f-`{x})\ ``` lp15@68339 ` 127` ``` \ (g \ f) piecewise_differentiable_on S" ``` lp15@60809 ` 128` ``` apply (simp add: piecewise_differentiable_on_def, safe) ``` lp15@60809 ` 129` ``` apply (blast intro: continuous_on_compose2) ``` lp15@60809 ` 130` ``` apply (rename_tac A B) ``` lp15@68284 ` 131` ``` apply (rule_tac x="A \ (\x\B. S \ f-`{x})" in exI) ``` lp15@65036 ` 132` ``` apply (blast intro!: differentiable_chain_within) ``` lp15@61190 ` 133` ``` done ``` lp15@60809 ` 134` lp15@60809 ` 135` ```lemma piecewise_differentiable_affine: ``` lp15@60809 ` 136` ``` fixes m::real ``` lp15@68284 ` 137` ``` assumes "f piecewise_differentiable_on ((\x. m *\<^sub>R x + c) ` S)" ``` lp15@68339 ` 138` ``` shows "(f \ (\x. m *\<^sub>R x + c)) piecewise_differentiable_on S" ``` lp15@60809 ` 139` ```proof (cases "m = 0") ``` lp15@60809 ` 140` ``` case True ``` lp15@60809 ` 141` ``` then show ?thesis ``` lp15@60809 ` 142` ``` unfolding o_def ``` lp15@60809 ` 143` ``` by (force intro: differentiable_imp_piecewise_differentiable differentiable_const) ``` lp15@60809 ` 144` ```next ``` lp15@60809 ` 145` ``` case False ``` lp15@60809 ` 146` ``` show ?thesis ``` lp15@60809 ` 147` ``` apply (rule piecewise_differentiable_compose [OF differentiable_imp_piecewise_differentiable]) ``` lp15@60809 ` 148` ``` apply (rule assms derivative_intros | simp add: False vimage_def real_vector_affinity_eq)+ ``` lp15@60809 ` 149` ``` done ``` lp15@60809 ` 150` ```qed ``` lp15@60809 ` 151` lp15@60809 ` 152` ```lemma piecewise_differentiable_cases: ``` lp15@60809 ` 153` ``` fixes c::real ``` lp15@60809 ` 154` ``` assumes "f piecewise_differentiable_on {a..c}" ``` lp15@60809 ` 155` ``` "g piecewise_differentiable_on {c..b}" ``` lp15@60809 ` 156` ``` "a \ c" "c \ b" "f c = g c" ``` lp15@60809 ` 157` ``` shows "(\x. if x \ c then f x else g x) piecewise_differentiable_on {a..b}" ``` lp15@60809 ` 158` ```proof - ``` lp15@68284 ` 159` ``` obtain S T where st: "finite S" "finite T" ``` lp15@68284 ` 160` ``` and fd: "\x. x \ {a..c} - S \ f differentiable at x within {a..c}" ``` lp15@68284 ` 161` ``` and gd: "\x. x \ {c..b} - T \ g differentiable at x within {c..b}" ``` lp15@60809 ` 162` ``` using assms ``` lp15@60809 ` 163` ``` by (auto simp: piecewise_differentiable_on_def) ``` lp15@68284 ` 164` ``` have finabc: "finite ({a,b,c} \ (S \ T))" ``` lp15@68284 ` 165` ``` by (metis \finite S\ \finite T\ finite_Un finite_insert finite.emptyI) ``` lp15@60809 ` 166` ``` have "continuous_on {a..c} f" "continuous_on {c..b} g" ``` lp15@60809 ` 167` ``` using assms piecewise_differentiable_on_def by auto ``` lp15@60809 ` 168` ``` then have "continuous_on {a..b} (\x. if x \ c then f x else g x)" ``` lp15@60809 ` 169` ``` using continuous_on_cases [OF closed_real_atLeastAtMost [of a c], ``` lp15@60809 ` 170` ``` OF closed_real_atLeastAtMost [of c b], ``` lp15@60809 ` 171` ``` of f g "\x. x\c"] assms ``` lp15@60809 ` 172` ``` by (force simp: ivl_disj_un_two_touch) ``` lp15@60809 ` 173` ``` moreover ``` lp15@60809 ` 174` ``` { fix x ``` lp15@68284 ` 175` ``` assume x: "x \ {a..b} - ({a,b,c} \ (S \ T))" ``` lp15@61190 ` 176` ``` have "(\x. if x \ c then f x else g x) differentiable at x within {a..b}" (is "?diff_fg") ``` lp15@60809 ` 177` ``` proof (cases x c rule: le_cases) ``` lp15@60809 ` 178` ``` case le show ?diff_fg ``` lp15@68284 ` 179` ``` proof (rule differentiable_transform_within [where d = "dist x c"]) ``` lp15@68284 ` 180` ``` have "f differentiable at x" ``` lp15@68284 ` 181` ``` using x le fd [of x] at_within_interior [of x "{a..c}"] by simp ``` lp15@68284 ` 182` ``` then show "f differentiable at x within {a..b}" ``` lp15@68284 ` 183` ``` by (simp add: differentiable_at_withinI) ``` lp15@63955 ` 184` ``` qed (use x le st dist_real_def in auto) ``` lp15@60809 ` 185` ``` next ``` lp15@60809 ` 186` ``` case ge show ?diff_fg ``` lp15@68284 ` 187` ``` proof (rule differentiable_transform_within [where d = "dist x c"]) ``` lp15@68284 ` 188` ``` have "g differentiable at x" ``` lp15@68284 ` 189` ``` using x ge gd [of x] at_within_interior [of x "{c..b}"] by simp ``` lp15@68284 ` 190` ``` then show "g differentiable at x within {a..b}" ``` lp15@68284 ` 191` ``` by (simp add: differentiable_at_withinI) ``` lp15@63955 ` 192` ``` qed (use x ge st dist_real_def in auto) ``` lp15@60809 ` 193` ``` qed ``` lp15@60809 ` 194` ``` } ``` lp15@68284 ` 195` ``` then have "\S. finite S \ ``` lp15@68284 ` 196` ``` (\x\{a..b} - S. (\x. if x \ c then f x else g x) differentiable at x within {a..b})" ``` lp15@61190 ` 197` ``` by (meson finabc) ``` lp15@60809 ` 198` ``` ultimately show ?thesis ``` lp15@60809 ` 199` ``` by (simp add: piecewise_differentiable_on_def) ``` lp15@60809 ` 200` ```qed ``` lp15@60809 ` 201` lp15@60809 ` 202` ```lemma piecewise_differentiable_neg: ``` lp15@68284 ` 203` ``` "f piecewise_differentiable_on S \ (\x. -(f x)) piecewise_differentiable_on S" ``` lp15@60809 ` 204` ``` by (auto simp: piecewise_differentiable_on_def continuous_on_minus) ``` lp15@60809 ` 205` lp15@60809 ` 206` ```lemma piecewise_differentiable_add: ``` lp15@60809 ` 207` ``` assumes "f piecewise_differentiable_on i" ``` lp15@60809 ` 208` ``` "g piecewise_differentiable_on i" ``` lp15@60809 ` 209` ``` shows "(\x. f x + g x) piecewise_differentiable_on i" ``` lp15@60809 ` 210` ```proof - ``` lp15@68284 ` 211` ``` obtain S T where st: "finite S" "finite T" ``` lp15@68284 ` 212` ``` "\x\i - S. f differentiable at x within i" ``` lp15@68284 ` 213` ``` "\x\i - T. g differentiable at x within i" ``` lp15@60809 ` 214` ``` using assms by (auto simp: piecewise_differentiable_on_def) ``` lp15@68284 ` 215` ``` then have "finite (S \ T) \ (\x\i - (S \ T). (\x. f x + g x) differentiable at x within i)" ``` lp15@60809 ` 216` ``` by auto ``` lp15@60809 ` 217` ``` moreover have "continuous_on i f" "continuous_on i g" ``` lp15@60809 ` 218` ``` using assms piecewise_differentiable_on_def by auto ``` lp15@60809 ` 219` ``` ultimately show ?thesis ``` lp15@60809 ` 220` ``` by (auto simp: piecewise_differentiable_on_def continuous_on_add) ``` lp15@60809 ` 221` ```qed ``` lp15@60809 ` 222` lp15@60809 ` 223` ```lemma piecewise_differentiable_diff: ``` lp15@68284 ` 224` ``` "\f piecewise_differentiable_on S; g piecewise_differentiable_on S\ ``` lp15@68284 ` 225` ``` \ (\x. f x - g x) piecewise_differentiable_on S" ``` lp15@60809 ` 226` ``` unfolding diff_conv_add_uminus ``` lp15@60809 ` 227` ``` by (metis piecewise_differentiable_add piecewise_differentiable_neg) ``` lp15@60809 ` 228` lp15@61190 ` 229` ```lemma continuous_on_joinpaths_D1: ``` lp15@61190 ` 230` ``` "continuous_on {0..1} (g1 +++ g2) \ continuous_on {0..1} g1" ``` nipkow@69064 ` 231` ``` apply (rule continuous_on_eq [of _ "(g1 +++ g2) \ ((*)(inverse 2))"]) ``` lp15@61190 ` 232` ``` apply (rule continuous_intros | simp)+ ``` lp15@61190 ` 233` ``` apply (auto elim!: continuous_on_subset simp: joinpaths_def) ``` lp15@61190 ` 234` ``` done ``` lp15@61190 ` 235` lp15@61190 ` 236` ```lemma continuous_on_joinpaths_D2: ``` lp15@61190 ` 237` ``` "\continuous_on {0..1} (g1 +++ g2); pathfinish g1 = pathstart g2\ \ continuous_on {0..1} g2" ``` lp15@68339 ` 238` ``` apply (rule continuous_on_eq [of _ "(g1 +++ g2) \ (\x. inverse 2*x + 1/2)"]) ``` lp15@61190 ` 239` ``` apply (rule continuous_intros | simp)+ ``` lp15@61190 ` 240` ``` apply (auto elim!: continuous_on_subset simp add: joinpaths_def pathfinish_def pathstart_def Ball_def) ``` lp15@61190 ` 241` ``` done ``` lp15@61190 ` 242` lp15@61190 ` 243` ```lemma piecewise_differentiable_D1: ``` lp15@68284 ` 244` ``` assumes "(g1 +++ g2) piecewise_differentiable_on {0..1}" ``` lp15@68284 ` 245` ``` shows "g1 piecewise_differentiable_on {0..1}" ``` lp15@68284 ` 246` ```proof - ``` lp15@68284 ` 247` ``` obtain S where cont: "continuous_on {0..1} g1" and "finite S" ``` lp15@68284 ` 248` ``` and S: "\x. x \ {0..1} - S \ g1 +++ g2 differentiable at x within {0..1}" ``` lp15@68284 ` 249` ``` using assms unfolding piecewise_differentiable_on_def ``` lp15@68284 ` 250` ``` by (blast dest!: continuous_on_joinpaths_D1) ``` lp15@68284 ` 251` ``` show ?thesis ``` lp15@68284 ` 252` ``` unfolding piecewise_differentiable_on_def ``` lp15@68284 ` 253` ``` proof (intro exI conjI ballI cont) ``` nipkow@69064 ` 254` ``` show "finite (insert 1 (((*)2) ` S))" ``` lp15@68284 ` 255` ``` by (simp add: \finite S\) ``` nipkow@69064 ` 256` ``` show "g1 differentiable at x within {0..1}" if "x \ {0..1} - insert 1 ((*) 2 ` S)" for x ``` lp15@68284 ` 257` ``` proof (rule_tac d="dist (x/2) (1/2)" in differentiable_transform_within) ``` lp15@68296 ` 258` ``` have "g1 +++ g2 differentiable at (x / 2) within {0..1/2}" ``` lp15@68284 ` 259` ``` by (rule differentiable_subset [OF S [of "x/2"]] | use that in force)+ ``` nipkow@69064 ` 260` ``` then show "g1 +++ g2 \ (*) (inverse 2) differentiable at x within {0..1}" ``` haftmann@69661 ` 261` ``` using image_affinity_atLeastAtMost_div [of 2 0 "0::real" 1] ``` lp15@68284 ` 262` ``` by (auto intro: differentiable_chain_within) ``` lp15@68284 ` 263` ``` qed (use that in \auto simp: joinpaths_def\) ``` lp15@68284 ` 264` ``` qed ``` lp15@68284 ` 265` ```qed ``` lp15@61190 ` 266` lp15@61190 ` 267` ```lemma piecewise_differentiable_D2: ``` lp15@68284 ` 268` ``` assumes "(g1 +++ g2) piecewise_differentiable_on {0..1}" and eq: "pathfinish g1 = pathstart g2" ``` lp15@68284 ` 269` ``` shows "g2 piecewise_differentiable_on {0..1}" ``` lp15@68284 ` 270` ```proof - ``` lp15@68284 ` 271` ``` have [simp]: "g1 1 = g2 0" ``` lp15@68284 ` 272` ``` using eq by (simp add: pathfinish_def pathstart_def) ``` lp15@68284 ` 273` ``` obtain S where cont: "continuous_on {0..1} g2" and "finite S" ``` lp15@68284 ` 274` ``` and S: "\x. x \ {0..1} - S \ g1 +++ g2 differentiable at x within {0..1}" ``` lp15@68284 ` 275` ``` using assms unfolding piecewise_differentiable_on_def ``` lp15@68284 ` 276` ``` by (blast dest!: continuous_on_joinpaths_D2) ``` lp15@68284 ` 277` ``` show ?thesis ``` lp15@68284 ` 278` ``` unfolding piecewise_differentiable_on_def ``` lp15@68284 ` 279` ``` proof (intro exI conjI ballI cont) ``` lp15@68284 ` 280` ``` show "finite (insert 0 ((\x. 2*x-1)`S))" ``` lp15@68284 ` 281` ``` by (simp add: \finite S\) ``` lp15@68284 ` 282` ``` show "g2 differentiable at x within {0..1}" if "x \ {0..1} - insert 0 ((\x. 2*x-1)`S)" for x ``` lp15@68284 ` 283` ``` proof (rule_tac d="dist ((x+1)/2) (1/2)" in differentiable_transform_within) ``` lp15@68284 ` 284` ``` have x2: "(x + 1) / 2 \ S" ``` lp15@68284 ` 285` ``` using that ``` lp15@68284 ` 286` ``` apply (clarsimp simp: image_iff) ``` lp15@68527 ` 287` ``` by (metis add.commute add_diff_cancel_left' mult_2 field_sum_of_halves) ``` lp15@68284 ` 288` ``` have "g1 +++ g2 \ (\x. (x+1) / 2) differentiable at x within {0..1}" ``` lp15@68284 ` 289` ``` by (rule differentiable_chain_within differentiable_subset [OF S [of "(x+1)/2"]] | use x2 that in force)+ ``` lp15@68284 ` 290` ``` then show "g1 +++ g2 \ (\x. (x+1) / 2) differentiable at x within {0..1}" ``` lp15@68284 ` 291` ``` by (auto intro: differentiable_chain_within) ``` lp15@68296 ` 292` ``` show "(g1 +++ g2 \ (\x. (x + 1) / 2)) x' = g2 x'" if "x' \ {0..1}" "dist x' x < dist ((x + 1) / 2) (1/2)" for x' ``` lp15@68284 ` 293` ``` proof - ``` lp15@68284 ` 294` ``` have [simp]: "(2*x'+2)/2 = x'+1" ``` lp15@68284 ` 295` ``` by (simp add: divide_simps) ``` lp15@68284 ` 296` ``` show ?thesis ``` lp15@68284 ` 297` ``` using that by (auto simp: joinpaths_def) ``` lp15@68284 ` 298` ``` qed ``` lp15@68284 ` 299` ``` qed (use that in \auto simp: joinpaths_def\) ``` lp15@68284 ` 300` ``` qed ``` lp15@68284 ` 301` ```qed ``` lp15@61190 ` 302` lp15@61190 ` 303` wl302@69423 ` 304` ```subsection\The concept of continuously differentiable\ ``` lp15@61190 ` 305` lp15@62408 ` 306` ```text \ ``` lp15@62408 ` 307` ```John Harrison writes as follows: ``` lp15@62408 ` 308` wenzelm@62456 ` 309` `````The usual assumption in complex analysis texts is that a path \\\ should be piecewise ``` lp15@62408 ` 310` ```continuously differentiable, which ensures that the path integral exists at least for any continuous ``` lp15@62408 ` 311` ```f, since all piecewise continuous functions are integrable. However, our notion of validity is ``` lp15@68341 ` 312` ```weaker, just piecewise differentiability\ldots{} [namely] continuity plus differentiability except on a ``` lp15@68341 ` 313` ```finite set\ldots{} [Our] underlying theory of integration is the Kurzweil-Henstock theory. In contrast to ``` lp15@62408 ` 314` ```the Riemann or Lebesgue theory (but in common with a simple notion based on antiderivatives), this ``` lp15@62408 ` 315` ```can integrate all derivatives.'' ``` lp15@62408 ` 316` lp15@62534 ` 317` ```"Formalizing basic complex analysis." From Insight to Proof: Festschrift in Honour of Andrzej Trybulec. ``` lp15@62408 ` 318` ```Studies in Logic, Grammar and Rhetoric 10.23 (2007): 151-165. ``` lp15@62408 ` 319` lp15@62408 ` 320` ```And indeed he does not assume that his derivatives are continuous, but the penalty is unreasonably ``` lp15@62408 ` 321` ```difficult proofs concerning winding numbers. We need a self-contained and straightforward theorem ``` lp15@62408 ` 322` ```asserting that all derivatives can be integrated before we can adopt Harrison's choice.\ ``` lp15@62408 ` 323` wl302@69423 ` 324` ```definition%important C1_differentiable_on :: "(real \ 'a::real_normed_vector) \ real set \ bool" ``` lp15@61190 ` 325` ``` (infix "C1'_differentiable'_on" 50) ``` lp15@61190 ` 326` ``` where ``` lp15@68296 ` 327` ``` "f C1_differentiable_on S \ ``` lp15@68296 ` 328` ``` (\D. (\x \ S. (f has_vector_derivative (D x)) (at x)) \ continuous_on S D)" ``` lp15@61190 ` 329` lp15@61190 ` 330` ```lemma C1_differentiable_on_eq: ``` lp15@68296 ` 331` ``` "f C1_differentiable_on S \ ``` lp15@68296 ` 332` ``` (\x \ S. f differentiable at x) \ continuous_on S (\x. vector_derivative f (at x))" ``` lp15@68296 ` 333` ``` (is "?lhs = ?rhs") ``` lp15@68296 ` 334` ```proof ``` lp15@68296 ` 335` ``` assume ?lhs ``` lp15@68296 ` 336` ``` then show ?rhs ``` lp15@68296 ` 337` ``` unfolding C1_differentiable_on_def ``` lp15@68296 ` 338` ``` by (metis (no_types, lifting) continuous_on_eq differentiableI_vector vector_derivative_at) ``` lp15@68296 ` 339` ```next ``` lp15@68296 ` 340` ``` assume ?rhs ``` lp15@68296 ` 341` ``` then show ?lhs ``` lp15@68296 ` 342` ``` using C1_differentiable_on_def vector_derivative_works by fastforce ``` lp15@68296 ` 343` ```qed ``` lp15@61190 ` 344` lp15@61190 ` 345` ```lemma C1_differentiable_on_subset: ``` lp15@68296 ` 346` ``` "f C1_differentiable_on T \ S \ T \ f C1_differentiable_on S" ``` lp15@61190 ` 347` ``` unfolding C1_differentiable_on_def continuous_on_eq_continuous_within ``` lp15@61190 ` 348` ``` by (blast intro: continuous_within_subset) ``` lp15@61190 ` 349` lp15@61190 ` 350` ```lemma C1_differentiable_compose: ``` lp15@68296 ` 351` ``` assumes fg: "f C1_differentiable_on S" "g C1_differentiable_on (f ` S)" and fin: "\x. finite (S \ f-`{x})" ``` lp15@68339 ` 352` ``` shows "(g \ f) C1_differentiable_on S" ``` lp15@68296 ` 353` ```proof - ``` lp15@68296 ` 354` ``` have "\x. x \ S \ g \ f differentiable at x" ``` lp15@68296 ` 355` ``` by (meson C1_differentiable_on_eq assms differentiable_chain_at imageI) ``` lp15@68296 ` 356` ``` moreover have "continuous_on S (\x. vector_derivative (g \ f) (at x))" ``` lp15@68296 ` 357` ``` proof (rule continuous_on_eq [of _ "\x. vector_derivative f (at x) *\<^sub>R vector_derivative g (at (f x))"]) ``` lp15@68296 ` 358` ``` show "continuous_on S (\x. vector_derivative f (at x) *\<^sub>R vector_derivative g (at (f x)))" ``` lp15@68296 ` 359` ``` using fg ``` lp15@68296 ` 360` ``` apply (clarsimp simp add: C1_differentiable_on_eq) ``` lp15@68296 ` 361` ``` apply (rule Limits.continuous_on_scaleR, assumption) ``` lp15@68296 ` 362` ``` by (metis (mono_tags, lifting) continuous_at_imp_continuous_on continuous_on_compose continuous_on_cong differentiable_imp_continuous_within o_def) ``` lp15@68296 ` 363` ``` show "\x. x \ S \ vector_derivative f (at x) *\<^sub>R vector_derivative g (at (f x)) = vector_derivative (g \ f) (at x)" ``` lp15@68296 ` 364` ``` by (metis (mono_tags, hide_lams) C1_differentiable_on_eq fg imageI vector_derivative_chain_at) ``` lp15@68296 ` 365` ``` qed ``` lp15@68296 ` 366` ``` ultimately show ?thesis ``` lp15@68296 ` 367` ``` by (simp add: C1_differentiable_on_eq) ``` lp15@68296 ` 368` ```qed ``` lp15@68296 ` 369` lp15@68296 ` 370` ```lemma C1_diff_imp_diff: "f C1_differentiable_on S \ f differentiable_on S" ``` lp15@61190 ` 371` ``` by (simp add: C1_differentiable_on_eq differentiable_at_imp_differentiable_on) ``` lp15@61190 ` 372` lp15@68296 ` 373` ```lemma C1_differentiable_on_ident [simp, derivative_intros]: "(\x. x) C1_differentiable_on S" ``` lp15@61190 ` 374` ``` by (auto simp: C1_differentiable_on_eq continuous_on_const) ``` lp15@61190 ` 375` lp15@68296 ` 376` ```lemma C1_differentiable_on_const [simp, derivative_intros]: "(\z. a) C1_differentiable_on S" ``` lp15@61190 ` 377` ``` by (auto simp: C1_differentiable_on_eq continuous_on_const) ``` lp15@61190 ` 378` lp15@61190 ` 379` ```lemma C1_differentiable_on_add [simp, derivative_intros]: ``` lp15@68296 ` 380` ``` "f C1_differentiable_on S \ g C1_differentiable_on S \ (\x. f x + g x) C1_differentiable_on S" ``` lp15@61190 ` 381` ``` unfolding C1_differentiable_on_eq by (auto intro: continuous_intros) ``` lp15@61190 ` 382` lp15@61190 ` 383` ```lemma C1_differentiable_on_minus [simp, derivative_intros]: ``` lp15@68296 ` 384` ``` "f C1_differentiable_on S \ (\x. - f x) C1_differentiable_on S" ``` lp15@61190 ` 385` ``` unfolding C1_differentiable_on_eq by (auto intro: continuous_intros) ``` lp15@61190 ` 386` lp15@61190 ` 387` ```lemma C1_differentiable_on_diff [simp, derivative_intros]: ``` lp15@68296 ` 388` ``` "f C1_differentiable_on S \ g C1_differentiable_on S \ (\x. f x - g x) C1_differentiable_on S" ``` lp15@61190 ` 389` ``` unfolding C1_differentiable_on_eq by (auto intro: continuous_intros) ``` lp15@61190 ` 390` lp15@61190 ` 391` ```lemma C1_differentiable_on_mult [simp, derivative_intros]: ``` lp15@61190 ` 392` ``` fixes f g :: "real \ 'a :: real_normed_algebra" ``` lp15@68296 ` 393` ``` shows "f C1_differentiable_on S \ g C1_differentiable_on S \ (\x. f x * g x) C1_differentiable_on S" ``` lp15@61190 ` 394` ``` unfolding C1_differentiable_on_eq ``` lp15@61190 ` 395` ``` by (auto simp: continuous_on_add continuous_on_mult continuous_at_imp_continuous_on differentiable_imp_continuous_within) ``` lp15@61190 ` 396` lp15@61190 ` 397` ```lemma C1_differentiable_on_scaleR [simp, derivative_intros]: ``` lp15@68296 ` 398` ``` "f C1_differentiable_on S \ g C1_differentiable_on S \ (\x. f x *\<^sub>R g x) C1_differentiable_on S" ``` lp15@61190 ` 399` ``` unfolding C1_differentiable_on_eq ``` lp15@61190 ` 400` ``` by (rule continuous_intros | simp add: continuous_at_imp_continuous_on differentiable_imp_continuous_within)+ ``` lp15@61190 ` 401` lp15@61190 ` 402` wl302@69423 ` 403` ```definition%important piecewise_C1_differentiable_on ``` lp15@61190 ` 404` ``` (infixr "piecewise'_C1'_differentiable'_on" 50) ``` lp15@61190 ` 405` ``` where "f piecewise_C1_differentiable_on i \ ``` lp15@61190 ` 406` ``` continuous_on i f \ ``` lp15@68296 ` 407` ``` (\S. finite S \ (f C1_differentiable_on (i - S)))" ``` lp15@61190 ` 408` lp15@61190 ` 409` ```lemma C1_differentiable_imp_piecewise: ``` lp15@68296 ` 410` ``` "f C1_differentiable_on S \ f piecewise_C1_differentiable_on S" ``` lp15@61190 ` 411` ``` by (auto simp: piecewise_C1_differentiable_on_def C1_differentiable_on_eq continuous_at_imp_continuous_on differentiable_imp_continuous_within) ``` lp15@61190 ` 412` lp15@61190 ` 413` ```lemma piecewise_C1_imp_differentiable: ``` lp15@61190 ` 414` ``` "f piecewise_C1_differentiable_on i \ f piecewise_differentiable_on i" ``` lp15@61190 ` 415` ``` by (auto simp: piecewise_C1_differentiable_on_def piecewise_differentiable_on_def ``` lp15@61190 ` 416` ``` C1_differentiable_on_def differentiable_def has_vector_derivative_def ``` lp15@67979 ` 417` ``` intro: has_derivative_at_withinI) ``` lp15@61190 ` 418` lp15@61190 ` 419` ```lemma piecewise_C1_differentiable_compose: ``` lp15@68296 ` 420` ``` assumes fg: "f piecewise_C1_differentiable_on S" "g piecewise_C1_differentiable_on (f ` S)" and fin: "\x. finite (S \ f-`{x})" ``` lp15@68339 ` 421` ``` shows "(g \ f) piecewise_C1_differentiable_on S" ``` lp15@68296 ` 422` ```proof - ``` lp15@68296 ` 423` ``` have "continuous_on S (\x. g (f x))" ``` lp15@68296 ` 424` ``` by (metis continuous_on_compose2 fg order_refl piecewise_C1_differentiable_on_def) ``` lp15@68296 ` 425` ``` moreover have "\T. finite T \ g \ f C1_differentiable_on S - T" ``` lp15@68296 ` 426` ``` proof - ``` lp15@68296 ` 427` ``` obtain F where "finite F" and F: "f C1_differentiable_on S - F" and f: "f piecewise_C1_differentiable_on S" ``` lp15@68296 ` 428` ``` using fg by (auto simp: piecewise_C1_differentiable_on_def) ``` lp15@68296 ` 429` ``` obtain G where "finite G" and G: "g C1_differentiable_on f ` S - G" and g: "g piecewise_C1_differentiable_on f ` S" ``` lp15@68296 ` 430` ``` using fg by (auto simp: piecewise_C1_differentiable_on_def) ``` lp15@68296 ` 431` ``` show ?thesis ``` lp15@68296 ` 432` ``` proof (intro exI conjI) ``` lp15@68296 ` 433` ``` show "finite (F \ (\x\G. S \ f-`{x}))" ``` lp15@68296 ` 434` ``` using fin by (auto simp only: Int_Union \finite F\ \finite G\ finite_UN finite_imageI) ``` lp15@68296 ` 435` ``` show "g \ f C1_differentiable_on S - (F \ (\x\G. S \ f -` {x}))" ``` lp15@68296 ` 436` ``` apply (rule C1_differentiable_compose) ``` lp15@68296 ` 437` ``` apply (blast intro: C1_differentiable_on_subset [OF F]) ``` lp15@68296 ` 438` ``` apply (blast intro: C1_differentiable_on_subset [OF G]) ``` lp15@68296 ` 439` ``` by (simp add: C1_differentiable_on_subset G Diff_Int_distrib2 fin) ``` lp15@68296 ` 440` ``` qed ``` lp15@68296 ` 441` ``` qed ``` lp15@68296 ` 442` ``` ultimately show ?thesis ``` lp15@68296 ` 443` ``` by (simp add: piecewise_C1_differentiable_on_def) ``` lp15@68296 ` 444` ```qed ``` lp15@61190 ` 445` lp15@61190 ` 446` ```lemma piecewise_C1_differentiable_on_subset: ``` lp15@68296 ` 447` ``` "f piecewise_C1_differentiable_on S \ T \ S \ f piecewise_C1_differentiable_on T" ``` lp15@61190 ` 448` ``` by (auto simp: piecewise_C1_differentiable_on_def elim!: continuous_on_subset C1_differentiable_on_subset) ``` lp15@61190 ` 449` lp15@61190 ` 450` ```lemma C1_differentiable_imp_continuous_on: ``` lp15@68296 ` 451` ``` "f C1_differentiable_on S \ continuous_on S f" ``` lp15@61190 ` 452` ``` unfolding C1_differentiable_on_eq continuous_on_eq_continuous_within ``` lp15@61190 ` 453` ``` using differentiable_at_withinI differentiable_imp_continuous_within by blast ``` lp15@61190 ` 454` lp15@61190 ` 455` ```lemma C1_differentiable_on_empty [iff]: "f C1_differentiable_on {}" ``` lp15@61190 ` 456` ``` unfolding C1_differentiable_on_def ``` lp15@61190 ` 457` ``` by auto ``` lp15@61190 ` 458` lp15@61190 ` 459` ```lemma piecewise_C1_differentiable_affine: ``` lp15@61190 ` 460` ``` fixes m::real ``` lp15@68296 ` 461` ``` assumes "f piecewise_C1_differentiable_on ((\x. m * x + c) ` S)" ``` lp15@68339 ` 462` ``` shows "(f \ (\x. m *\<^sub>R x + c)) piecewise_C1_differentiable_on S" ``` lp15@61190 ` 463` ```proof (cases "m = 0") ``` lp15@61190 ` 464` ``` case True ``` lp15@61190 ` 465` ``` then show ?thesis ``` lp15@61190 ` 466` ``` unfolding o_def by (auto simp: piecewise_C1_differentiable_on_def continuous_on_const) ``` lp15@61190 ` 467` ```next ``` lp15@61190 ` 468` ``` case False ``` lp15@68296 ` 469` ``` have *: "\x. finite (S \ {y. m * y + c = x})" ``` lp15@68493 ` 470` ``` using False not_finite_existsD by fastforce ``` lp15@61190 ` 471` ``` show ?thesis ``` lp15@61190 ` 472` ``` apply (rule piecewise_C1_differentiable_compose [OF C1_differentiable_imp_piecewise]) ``` lp15@68296 ` 473` ``` apply (rule * assms derivative_intros | simp add: False vimage_def)+ ``` lp15@61190 ` 474` ``` done ``` lp15@61190 ` 475` ```qed ``` lp15@61190 ` 476` lp15@61190 ` 477` ```lemma piecewise_C1_differentiable_cases: ``` lp15@61190 ` 478` ``` fixes c::real ``` lp15@61190 ` 479` ``` assumes "f piecewise_C1_differentiable_on {a..c}" ``` lp15@61190 ` 480` ``` "g piecewise_C1_differentiable_on {c..b}" ``` lp15@61190 ` 481` ``` "a \ c" "c \ b" "f c = g c" ``` lp15@61190 ` 482` ``` shows "(\x. if x \ c then f x else g x) piecewise_C1_differentiable_on {a..b}" ``` lp15@61190 ` 483` ```proof - ``` lp15@68296 ` 484` ``` obtain S T where st: "f C1_differentiable_on ({a..c} - S)" ``` lp15@68296 ` 485` ``` "g C1_differentiable_on ({c..b} - T)" ``` lp15@68296 ` 486` ``` "finite S" "finite T" ``` lp15@61190 ` 487` ``` using assms ``` lp15@61190 ` 488` ``` by (force simp: piecewise_C1_differentiable_on_def) ``` lp15@68296 ` 489` ``` then have f_diff: "f differentiable_on {a..x. if x \ c then f x else g x)" ``` lp15@61190 ` 495` ``` using continuous_on_cases [OF closed_real_atLeastAtMost [of a c], ``` lp15@61190 ` 496` ``` OF closed_real_atLeastAtMost [of c b], ``` lp15@61190 ` 497` ``` of f g "\x. x\c"] assms ``` lp15@61190 ` 498` ``` by (force simp: ivl_disj_un_two_touch) ``` lp15@61190 ` 499` ``` { fix x ``` lp15@68296 ` 500` ``` assume x: "x \ {a..b} - insert c (S \ T)" ``` lp15@61190 ` 501` ``` have "(\x. if x \ c then f x else g x) differentiable at x" (is "?diff_fg") ``` lp15@61190 ` 502` ``` proof (cases x c rule: le_cases) ``` lp15@61190 ` 503` ``` case le show ?diff_fg ``` paulson@62087 ` 504` ``` apply (rule differentiable_transform_within [where f=f and d = "dist x c"]) ``` lp15@61190 ` 505` ``` using x dist_real_def le st by (auto simp: C1_differentiable_on_eq) ``` lp15@61190 ` 506` ``` next ``` lp15@61190 ` 507` ``` case ge show ?diff_fg ``` paulson@62087 ` 508` ``` apply (rule differentiable_transform_within [where f=g and d = "dist x c"]) ``` lp15@61190 ` 509` ``` using dist_nz x dist_real_def ge st x by (auto simp: C1_differentiable_on_eq) ``` lp15@61190 ` 510` ``` qed ``` lp15@61190 ` 511` ``` } ``` lp15@68296 ` 512` ``` then have "(\x \ {a..b} - insert c (S \ T). (\x. if x \ c then f x else g x) differentiable at x)" ``` lp15@61190 ` 513` ``` by auto ``` lp15@61190 ` 514` ``` moreover ``` lp15@68296 ` 515` ``` { assume fcon: "continuous_on ({a<..x. vector_derivative f (at x))" ``` lp15@68296 ` 516` ``` and gcon: "continuous_on ({c<..x. vector_derivative g (at x))" ``` lp15@68296 ` 517` ``` have "open ({a<..x. vector_derivative (\x. if x \ c then f x else g x) (at x))" ``` lp15@68296 ` 520` ``` proof - ``` lp15@68296 ` 521` ``` have "((\x. if x \ c then f x else g x) has_vector_derivative vector_derivative f (at x)) (at x)" ``` lp15@68296 ` 522` ``` if "a < x" "x < c" "x \ S" for x ``` lp15@68296 ` 523` ``` proof - ``` lp15@68296 ` 524` ``` have f: "f differentiable at x" ``` lp15@68296 ` 525` ``` by (meson C1_differentiable_on_eq Diff_iff atLeastAtMost_iff less_eq_real_def st(1) that) ``` lp15@68296 ` 526` ``` show ?thesis ``` lp15@68296 ` 527` ``` using that ``` lp15@68296 ` 528` ``` apply (rule_tac f=f and d="dist x c" in has_vector_derivative_transform_within) ``` lp15@68339 ` 529` ``` apply (auto simp: dist_norm vector_derivative_works [symmetric] f) ``` lp15@68296 ` 530` ``` done ``` lp15@68296 ` 531` ``` qed ``` lp15@68296 ` 532` ``` then show ?thesis ``` lp15@68296 ` 533` ``` by (metis (no_types, lifting) continuous_on_eq [OF fcon] DiffE greaterThanLessThan_iff vector_derivative_at) ``` lp15@68296 ` 534` ``` qed ``` lp15@68296 ` 535` ``` moreover have "continuous_on ({c<..x. vector_derivative (\x. if x \ c then f x else g x) (at x))" ``` lp15@68296 ` 536` ``` proof - ``` lp15@68296 ` 537` ``` have "((\x. if x \ c then f x else g x) has_vector_derivative vector_derivative g (at x)) (at x)" ``` lp15@68296 ` 538` ``` if "c < x" "x < b" "x \ T" for x ``` lp15@68296 ` 539` ``` proof - ``` lp15@68296 ` 540` ``` have g: "g differentiable at x" ``` lp15@68296 ` 541` ``` by (metis C1_differentiable_on_eq DiffD1 DiffI atLeastAtMost_diff_ends greaterThanLessThan_iff st(2) that) ``` lp15@68296 ` 542` ``` show ?thesis ``` lp15@68296 ` 543` ``` using that ``` lp15@68296 ` 544` ``` apply (rule_tac f=g and d="dist x c" in has_vector_derivative_transform_within) ``` lp15@68339 ` 545` ``` apply (auto simp: dist_norm vector_derivative_works [symmetric] g) ``` lp15@68296 ` 546` ``` done ``` lp15@68296 ` 547` ``` qed ``` lp15@68296 ` 548` ``` then show ?thesis ``` lp15@68296 ` 549` ``` by (metis (no_types, lifting) continuous_on_eq [OF gcon] DiffE greaterThanLessThan_iff vector_derivative_at) ``` lp15@68296 ` 550` ``` qed ``` lp15@68296 ` 551` ``` ultimately have "continuous_on ({a<.. T)) ``` lp15@61190 ` 552` ``` (\x. vector_derivative (\x. if x \ c then f x else g x) (at x))" ``` lp15@68296 ` 553` ``` by (rule continuous_on_subset [OF continuous_on_open_Un], auto) ``` lp15@61190 ` 554` ``` } note * = this ``` lp15@68296 ` 555` ``` have "continuous_on ({a<.. T)) (\x. vector_derivative (\x. if x \ c then f x else g x) (at x))" ``` lp15@61190 ` 556` ``` using st ``` lp15@61190 ` 557` ``` by (auto simp: C1_differentiable_on_eq elim!: continuous_on_subset intro: *) ``` lp15@68296 ` 558` ``` ultimately have "\S. finite S \ ((\x. if x \ c then f x else g x) C1_differentiable_on {a..b} - S)" ``` lp15@68296 ` 559` ``` apply (rule_tac x="{a,b,c} \ S \ T" in exI) ``` lp15@61190 ` 560` ``` using st by (auto simp: C1_differentiable_on_eq elim!: continuous_on_subset) ``` lp15@61190 ` 561` ``` with cab show ?thesis ``` lp15@61190 ` 562` ``` by (simp add: piecewise_C1_differentiable_on_def) ``` lp15@61190 ` 563` ```qed ``` lp15@61190 ` 564` lp15@61190 ` 565` ```lemma piecewise_C1_differentiable_neg: ``` lp15@68296 ` 566` ``` "f piecewise_C1_differentiable_on S \ (\x. -(f x)) piecewise_C1_differentiable_on S" ``` lp15@61190 ` 567` ``` unfolding piecewise_C1_differentiable_on_def ``` lp15@61190 ` 568` ``` by (auto intro!: continuous_on_minus C1_differentiable_on_minus) ``` lp15@61190 ` 569` lp15@61190 ` 570` ```lemma piecewise_C1_differentiable_add: ``` lp15@61190 ` 571` ``` assumes "f piecewise_C1_differentiable_on i" ``` lp15@61190 ` 572` ``` "g piecewise_C1_differentiable_on i" ``` lp15@61190 ` 573` ``` shows "(\x. f x + g x) piecewise_C1_differentiable_on i" ``` lp15@61190 ` 574` ```proof - ``` lp15@68296 ` 575` ``` obtain S t where st: "finite S" "finite t" ``` lp15@68296 ` 576` ``` "f C1_differentiable_on (i-S)" ``` lp15@61190 ` 577` ``` "g C1_differentiable_on (i-t)" ``` lp15@61190 ` 578` ``` using assms by (auto simp: piecewise_C1_differentiable_on_def) ``` lp15@68296 ` 579` ``` then have "finite (S \ t) \ (\x. f x + g x) C1_differentiable_on i - (S \ t)" ``` lp15@61190 ` 580` ``` by (auto intro: C1_differentiable_on_add elim!: C1_differentiable_on_subset) ``` lp15@61190 ` 581` ``` moreover have "continuous_on i f" "continuous_on i g" ``` lp15@61190 ` 582` ``` using assms piecewise_C1_differentiable_on_def by auto ``` lp15@61190 ` 583` ``` ultimately show ?thesis ``` lp15@61190 ` 584` ``` by (auto simp: piecewise_C1_differentiable_on_def continuous_on_add) ``` lp15@61190 ` 585` ```qed ``` lp15@61190 ` 586` paulson@61204 ` 587` ```lemma piecewise_C1_differentiable_diff: ``` lp15@68296 ` 588` ``` "\f piecewise_C1_differentiable_on S; g piecewise_C1_differentiable_on S\ ``` lp15@68296 ` 589` ``` \ (\x. f x - g x) piecewise_C1_differentiable_on S" ``` lp15@61190 ` 590` ``` unfolding diff_conv_add_uminus ``` lp15@61190 ` 591` ``` by (metis piecewise_C1_differentiable_add piecewise_C1_differentiable_neg) ``` lp15@61190 ` 592` lp15@61190 ` 593` ```lemma piecewise_C1_differentiable_D1: ``` lp15@61190 ` 594` ``` fixes g1 :: "real \ 'a::real_normed_field" ``` lp15@61190 ` 595` ``` assumes "(g1 +++ g2) piecewise_C1_differentiable_on {0..1}" ``` lp15@61190 ` 596` ``` shows "g1 piecewise_C1_differentiable_on {0..1}" ``` lp15@61190 ` 597` ```proof - ``` lp15@68296 ` 598` ``` obtain S where "finite S" ``` lp15@68296 ` 599` ``` and co12: "continuous_on ({0..1} - S) (\x. vector_derivative (g1 +++ g2) (at x))" ``` lp15@68296 ` 600` ``` and g12D: "\x\{0..1} - S. g1 +++ g2 differentiable at x" ``` lp15@61190 ` 601` ``` using assms by (auto simp: piecewise_C1_differentiable_on_def C1_differentiable_on_eq) ``` nipkow@69064 ` 602` ``` have g1D: "g1 differentiable at x" if "x \ {0..1} - insert 1 ((*) 2 ` S)" for x ``` lp15@68296 ` 603` ``` proof (rule differentiable_transform_within) ``` nipkow@69064 ` 604` ``` show "g1 +++ g2 \ (*) (inverse 2) differentiable at x" ``` lp15@68493 ` 605` ``` using that g12D ``` lp15@68296 ` 606` ``` apply (simp only: joinpaths_def) ``` lp15@68296 ` 607` ``` by (rule differentiable_chain_at derivative_intros | force)+ ``` lp15@68296 ` 608` ``` show "\x'. \dist x' x < dist (x/2) (1/2)\ ``` nipkow@69064 ` 609` ``` \ (g1 +++ g2 \ (*) (inverse 2)) x' = g1 x'" ``` lp15@68339 ` 610` ``` using that by (auto simp: dist_real_def joinpaths_def) ``` lp15@68296 ` 611` ``` qed (use that in \auto simp: dist_real_def\) ``` nipkow@69064 ` 612` ``` have [simp]: "vector_derivative (g1 \ (*) 2) (at (x/2)) = 2 *\<^sub>R vector_derivative g1 (at x)" ``` nipkow@69064 ` 613` ``` if "x \ {0..1} - insert 1 ((*) 2 ` S)" for x ``` lp15@61190 ` 614` ``` apply (subst vector_derivative_chain_at) ``` lp15@61190 ` 615` ``` using that ``` lp15@61190 ` 616` ``` apply (rule derivative_eq_intros g1D | simp)+ ``` lp15@61190 ` 617` ``` done ``` lp15@68296 ` 618` ``` have "continuous_on ({0..1/2} - insert (1/2) S) (\x. vector_derivative (g1 +++ g2) (at x))" ``` lp15@61190 ` 619` ``` using co12 by (rule continuous_on_subset) force ``` nipkow@69064 ` 620` ``` then have coDhalf: "continuous_on ({0..1/2} - insert (1/2) S) (\x. vector_derivative (g1 \ (*)2) (at x))" ``` lp15@68296 ` 621` ``` proof (rule continuous_on_eq [OF _ vector_derivative_at]) ``` nipkow@69064 ` 622` ``` show "(g1 +++ g2 has_vector_derivative vector_derivative (g1 \ (*) 2) (at x)) (at x)" ``` lp15@68296 ` 623` ``` if "x \ {0..1/2} - insert (1/2) S" for x ``` lp15@68296 ` 624` ``` proof (rule has_vector_derivative_transform_within) ``` nipkow@69064 ` 625` ``` show "(g1 \ (*) 2 has_vector_derivative vector_derivative (g1 \ (*) 2) (at x)) (at x)" ``` lp15@68296 ` 626` ``` using that ``` lp15@68296 ` 627` ``` by (force intro: g1D differentiable_chain_at simp: vector_derivative_works [symmetric]) ``` nipkow@69064 ` 628` ``` show "\x'. \dist x' x < dist x (1/2)\ \ (g1 \ (*) 2) x' = (g1 +++ g2) x'" ``` lp15@68296 ` 629` ``` using that by (auto simp: dist_norm joinpaths_def) ``` lp15@68296 ` 630` ``` qed (use that in \auto simp: dist_norm\) ``` lp15@68296 ` 631` ``` qed ``` nipkow@69064 ` 632` ``` have "continuous_on ({0..1} - insert 1 ((*) 2 ` S)) ``` nipkow@69064 ` 633` ``` ((\x. 1/2 * vector_derivative (g1 \ (*)2) (at x)) \ (*)(1/2))" ``` lp15@61190 ` 634` ``` apply (rule continuous_intros)+ ``` lp15@61190 ` 635` ``` using coDhalf ``` lp15@61190 ` 636` ``` apply (simp add: scaleR_conv_of_real image_set_diff image_image) ``` lp15@61190 ` 637` ``` done ``` nipkow@69064 ` 638` ``` then have con_g1: "continuous_on ({0..1} - insert 1 ((*) 2 ` S)) (\x. vector_derivative g1 (at x))" ``` lp15@61190 ` 639` ``` by (rule continuous_on_eq) (simp add: scaleR_conv_of_real) ``` lp15@61190 ` 640` ``` have "continuous_on {0..1} g1" ``` lp15@61190 ` 641` ``` using continuous_on_joinpaths_D1 assms piecewise_C1_differentiable_on_def by blast ``` lp15@68296 ` 642` ``` with \finite S\ show ?thesis ``` lp15@61190 ` 643` ``` apply (clarsimp simp add: piecewise_C1_differentiable_on_def C1_differentiable_on_eq) ``` nipkow@69064 ` 644` ``` apply (rule_tac x="insert 1 (((*)2)`S)" in exI) ``` lp15@61190 ` 645` ``` apply (simp add: g1D con_g1) ``` lp15@61190 ` 646` ``` done ``` lp15@61190 ` 647` ```qed ``` lp15@61190 ` 648` lp15@61190 ` 649` ```lemma piecewise_C1_differentiable_D2: ``` lp15@61190 ` 650` ``` fixes g2 :: "real \ 'a::real_normed_field" ``` lp15@61190 ` 651` ``` assumes "(g1 +++ g2) piecewise_C1_differentiable_on {0..1}" "pathfinish g1 = pathstart g2" ``` lp15@61190 ` 652` ``` shows "g2 piecewise_C1_differentiable_on {0..1}" ``` lp15@61190 ` 653` ```proof - ``` lp15@68296 ` 654` ``` obtain S where "finite S" ``` lp15@68296 ` 655` ``` and co12: "continuous_on ({0..1} - S) (\x. vector_derivative (g1 +++ g2) (at x))" ``` lp15@68296 ` 656` ``` and g12D: "\x\{0..1} - S. g1 +++ g2 differentiable at x" ``` lp15@61190 ` 657` ``` using assms by (auto simp: piecewise_C1_differentiable_on_def C1_differentiable_on_eq) ``` lp15@68296 ` 658` ``` have g2D: "g2 differentiable at x" if "x \ {0..1} - insert 0 ((\x. 2*x-1) ` S)" for x ``` lp15@68296 ` 659` ``` proof (rule differentiable_transform_within) ``` lp15@68296 ` 660` ``` show "g1 +++ g2 \ (\x. (x + 1) / 2) differentiable at x" ``` lp15@68296 ` 661` ``` using g12D that ``` lp15@68296 ` 662` ``` apply (simp only: joinpaths_def) ``` lp15@68296 ` 663` ``` apply (drule_tac x= "(x+1) / 2" in bspec, force simp: divide_simps) ``` lp15@68296 ` 664` ``` apply (rule differentiable_chain_at derivative_intros | force)+ ``` lp15@68296 ` 665` ``` done ``` lp15@68296 ` 666` ``` show "\x'. dist x' x < dist ((x + 1) / 2) (1/2) \ (g1 +++ g2 \ (\x. (x + 1) / 2)) x' = g2 x'" ``` lp15@68296 ` 667` ``` using that by (auto simp: dist_real_def joinpaths_def field_simps) ``` lp15@68296 ` 668` ``` qed (use that in \auto simp: dist_norm\) ``` lp15@61190 ` 669` ``` have [simp]: "vector_derivative (g2 \ (\x. 2*x-1)) (at ((x+1)/2)) = 2 *\<^sub>R vector_derivative g2 (at x)" ``` lp15@68296 ` 670` ``` if "x \ {0..1} - insert 0 ((\x. 2*x-1) ` S)" for x ``` lp15@61190 ` 671` ``` using that by (auto simp: vector_derivative_chain_at divide_simps g2D) ``` lp15@68296 ` 672` ``` have "continuous_on ({1/2..1} - insert (1/2) S) (\x. vector_derivative (g1 +++ g2) (at x))" ``` lp15@61190 ` 673` ``` using co12 by (rule continuous_on_subset) force ``` lp15@68339 ` 674` ``` then have coDhalf: "continuous_on ({1/2..1} - insert (1/2) S) (\x. vector_derivative (g2 \ (\x. 2*x-1)) (at x))" ``` lp15@68296 ` 675` ``` proof (rule continuous_on_eq [OF _ vector_derivative_at]) ``` lp15@68296 ` 676` ``` show "(g1 +++ g2 has_vector_derivative vector_derivative (g2 \ (\x. 2 * x - 1)) (at x)) ``` lp15@68296 ` 677` ``` (at x)" ``` lp15@68296 ` 678` ``` if "x \ {1 / 2..1} - insert (1 / 2) S" for x ``` lp15@68339 ` 679` ``` proof (rule_tac f="g2 \ (\x. 2*x-1)" and d="dist (3/4) ((x+1)/2)" in has_vector_derivative_transform_within) ``` lp15@68296 ` 680` ``` show "(g2 \ (\x. 2 * x - 1) has_vector_derivative vector_derivative (g2 \ (\x. 2 * x - 1)) (at x)) ``` lp15@68296 ` 681` ``` (at x)" ``` lp15@68296 ` 682` ``` using that by (force intro: g2D differentiable_chain_at simp: vector_derivative_works [symmetric]) ``` lp15@68296 ` 683` ``` show "\x'. \dist x' x < dist (3 / 4) ((x + 1) / 2)\ \ (g2 \ (\x. 2 * x - 1)) x' = (g1 +++ g2) x'" ``` lp15@68296 ` 684` ``` using that by (auto simp: dist_norm joinpaths_def add_divide_distrib) ``` lp15@68296 ` 685` ``` qed (use that in \auto simp: dist_norm\) ``` lp15@68296 ` 686` ``` qed ``` lp15@68296 ` 687` ``` have [simp]: "((\x. (x+1) / 2) ` ({0..1} - insert 0 ((\x. 2 * x - 1) ` S))) = ({1/2..1} - insert (1/2) S)" ``` lp15@61190 ` 688` ``` apply (simp add: image_set_diff inj_on_def image_image) ``` lp15@61190 ` 689` ``` apply (auto simp: image_affinity_atLeastAtMost_div add_divide_distrib) ``` lp15@61190 ` 690` ``` done ``` lp15@68296 ` 691` ``` have "continuous_on ({0..1} - insert 0 ((\x. 2*x-1) ` S)) ``` lp15@68339 ` 692` ``` ((\x. 1/2 * vector_derivative (g2 \ (\x. 2*x-1)) (at x)) \ (\x. (x+1)/2))" ``` lp15@61190 ` 693` ``` by (rule continuous_intros | simp add: coDhalf)+ ``` lp15@68296 ` 694` ``` then have con_g2: "continuous_on ({0..1} - insert 0 ((\x. 2*x-1) ` S)) (\x. vector_derivative g2 (at x))" ``` lp15@61190 ` 695` ``` by (rule continuous_on_eq) (simp add: scaleR_conv_of_real) ``` lp15@61190 ` 696` ``` have "continuous_on {0..1} g2" ``` lp15@61190 ` 697` ``` using continuous_on_joinpaths_D2 assms piecewise_C1_differentiable_on_def by blast ``` lp15@68296 ` 698` ``` with \finite S\ show ?thesis ``` lp15@61190 ` 699` ``` apply (clarsimp simp add: piecewise_C1_differentiable_on_def C1_differentiable_on_eq) ``` lp15@68296 ` 700` ``` apply (rule_tac x="insert 0 ((\x. 2 * x - 1) ` S)" in exI) ``` lp15@61190 ` 701` ``` apply (simp add: g2D con_g2) ``` lp15@61190 ` 702` ``` done ``` lp15@61190 ` 703` ```qed ``` lp15@60809 ` 704` lp15@60809 ` 705` ```subsection \Valid paths, and their start and finish\ ``` lp15@60809 ` 706` wl302@69423 ` 707` ```definition%important valid_path :: "(real \ 'a :: real_normed_vector) \ bool" ``` lp15@61190 ` 708` ``` where "valid_path f \ f piecewise_C1_differentiable_on {0..1::real}" ``` lp15@60809 ` 709` lp15@60809 ` 710` ```definition closed_path :: "(real \ 'a :: real_normed_vector) \ bool" ``` lp15@60809 ` 711` ``` where "closed_path g \ g 0 = g 1" ``` lp15@60809 ` 712` wl302@69423 ` 713` ```text\In particular, all results for paths apply\ ``` lp15@60809 ` 714` lp15@60809 ` 715` ```lemma valid_path_imp_path: "valid_path g \ path g" ``` wl302@69423 ` 716` ``` by (simp add: path_def piecewise_C1_differentiable_on_def valid_path_def) ``` lp15@60809 ` 717` lp15@60809 ` 718` ```lemma connected_valid_path_image: "valid_path g \ connected(path_image g)" ``` lp15@60809 ` 719` ``` by (metis connected_path_image valid_path_imp_path) ``` lp15@60809 ` 720` lp15@60809 ` 721` ```lemma compact_valid_path_image: "valid_path g \ compact(path_image g)" ``` lp15@60809 ` 722` ``` by (metis compact_path_image valid_path_imp_path) ``` lp15@60809 ` 723` lp15@60809 ` 724` ```lemma bounded_valid_path_image: "valid_path g \ bounded(path_image g)" ``` lp15@60809 ` 725` ``` by (metis bounded_path_image valid_path_imp_path) ``` lp15@60809 ` 726` lp15@60809 ` 727` ```lemma closed_valid_path_image: "valid_path g \ closed(path_image g)" ``` lp15@60809 ` 728` ``` by (metis closed_path_image valid_path_imp_path) ``` lp15@60809 ` 729` wl302@69423 ` 730` ```lemma valid_path_compose: ``` lp15@62623 ` 731` ``` assumes "valid_path g" ``` lp15@64394 ` 732` ``` and der: "\x. x \ path_image g \ f field_differentiable (at x)" ``` lp15@62540 ` 733` ``` and con: "continuous_on (path_image g) (deriv f)" ``` lp15@68339 ` 734` ``` shows "valid_path (f \ g)" ``` lp15@62408 ` 735` ```proof - ``` lp15@68296 ` 736` ``` obtain S where "finite S" and g_diff: "g C1_differentiable_on {0..1} - S" ``` wenzelm@62837 ` 737` ``` using \valid_path g\ unfolding valid_path_def piecewise_C1_differentiable_on_def by auto ``` lp15@68296 ` 738` ``` have "f \ g differentiable at t" when "t\{0..1} - S" for t ``` lp15@62408 ` 739` ``` proof (rule differentiable_chain_at) ``` wenzelm@62837 ` 740` ``` show "g differentiable at t" using \valid_path g\ ``` lp15@68296 ` 741` ``` by (meson C1_differentiable_on_eq \g C1_differentiable_on {0..1} - S\ that) ``` lp15@62408 ` 742` ``` next ``` lp15@62408 ` 743` ``` have "g t\path_image g" using that DiffD1 image_eqI path_image_def by metis ``` lp15@68493 ` 744` ``` then show "f differentiable at (g t)" ``` lp15@64394 ` 745` ``` using der[THEN field_differentiable_imp_differentiable] by auto ``` lp15@62408 ` 746` ``` qed ``` lp15@68296 ` 747` ``` moreover have "continuous_on ({0..1} - S) (\x. vector_derivative (f \ g) (at x))" ``` lp15@62540 ` 748` ``` proof (rule continuous_on_eq [where f = "\x. vector_derivative g (at x) * deriv f (g x)"], ``` lp15@62540 ` 749` ``` rule continuous_intros) ``` lp15@68296 ` 750` ``` show "continuous_on ({0..1} - S) (\x. vector_derivative g (at x))" ``` lp15@62540 ` 751` ``` using g_diff C1_differentiable_on_eq by auto ``` lp15@62540 ` 752` ``` next ``` lp15@62623 ` 753` ``` have "continuous_on {0..1} (\x. deriv f (g x))" ``` lp15@62623 ` 754` ``` using continuous_on_compose[OF _ con[unfolded path_image_def],unfolded comp_def] ``` wenzelm@62837 ` 755` ``` \valid_path g\ piecewise_C1_differentiable_on_def valid_path_def ``` lp15@62540 ` 756` ``` by blast ``` lp15@68296 ` 757` ``` then show "continuous_on ({0..1} - S) (\x. deriv f (g x))" ``` lp15@62540 ` 758` ``` using continuous_on_subset by blast ``` lp15@62408 ` 759` ``` next ``` lp15@62540 ` 760` ``` show "vector_derivative g (at t) * deriv f (g t) = vector_derivative (f \ g) (at t)" ``` lp15@68296 ` 761` ``` when "t \ {0..1} - S" for t ``` lp15@62540 ` 762` ``` proof (rule vector_derivative_chain_at_general[symmetric]) ``` lp15@62540 ` 763` ``` show "g differentiable at t" by (meson C1_differentiable_on_eq g_diff that) ``` lp15@62540 ` 764` ``` next ``` lp15@62540 ` 765` ``` have "g t\path_image g" using that DiffD1 image_eqI path_image_def by metis ``` lp15@64394 ` 766` ``` then show "f field_differentiable at (g t)" using der by auto ``` lp15@62540 ` 767` ``` qed ``` lp15@62408 ` 768` ``` qed ``` lp15@68339 ` 769` ``` ultimately have "f \ g C1_differentiable_on {0..1} - S" ``` lp15@62408 ` 770` ``` using C1_differentiable_on_eq by blast ``` lp15@68493 ` 771` ``` moreover have "path (f \ g)" ``` lp15@64394 ` 772` ``` apply (rule path_continuous_image[OF valid_path_imp_path[OF \valid_path g\]]) ``` lp15@64394 ` 773` ``` using der ``` lp15@64394 ` 774` ``` by (simp add: continuous_at_imp_continuous_on field_differentiable_imp_continuous_at) ``` lp15@62408 ` 775` ``` ultimately show ?thesis unfolding valid_path_def piecewise_C1_differentiable_on_def path_def ``` lp15@68296 ` 776` ``` using \finite S\ by auto ``` lp15@62408 ` 777` ```qed ``` lp15@68532 ` 778` ``` ``` lp15@68532 ` 779` ```lemma valid_path_uminus_comp[simp]: ``` lp15@68532 ` 780` ``` fixes g::"real \ 'a ::real_normed_field" ``` lp15@68532 ` 781` ``` shows "valid_path (uminus \ g) \ valid_path g" ``` lp15@68532 ` 782` ```proof ``` lp15@68532 ` 783` ``` show "valid_path g \ valid_path (uminus \ g)" for g::"real \ 'a" ``` lp15@68532 ` 784` ``` by (auto intro!: valid_path_compose derivative_intros simp add: deriv_linear[of "-1",simplified]) ``` lp15@68532 ` 785` ``` then show "valid_path g" when "valid_path (uminus \ g)" ``` lp15@68532 ` 786` ``` by (metis fun.map_comp group_add_class.minus_comp_minus id_comp that) ``` lp15@68532 ` 787` ```qed ``` lp15@68532 ` 788` lp15@68532 ` 789` ```lemma valid_path_offset[simp]: ``` lp15@68532 ` 790` ``` shows "valid_path (\t. g t - z) \ valid_path g" ``` lp15@68532 ` 791` ```proof ``` lp15@68532 ` 792` ``` show *: "valid_path (g::real\'a) \ valid_path (\t. g t - z)" for g z ``` lp15@68532 ` 793` ``` unfolding valid_path_def ``` lp15@68532 ` 794` ``` by (fastforce intro:derivative_intros C1_differentiable_imp_piecewise piecewise_C1_differentiable_diff) ``` lp15@68532 ` 795` ``` show "valid_path (\t. g t - z) \ valid_path g" ``` lp15@68532 ` 796` ``` using *[of "\t. g t - z" "-z",simplified] . ``` lp15@68532 ` 797` ```qed ``` lp15@68532 ` 798` ``` ``` lp15@60809 ` 799` lp15@60809 ` 800` ```subsection\Contour Integrals along a path\ ``` lp15@60809 ` 801` lp15@60809 ` 802` ```text\This definition is for complex numbers only, and does not generalise to line integrals in a vector field\ ``` lp15@60809 ` 803` lp15@61190 ` 804` ```text\piecewise differentiable function on [0,1]\ ``` lp15@60809 ` 805` wl302@69423 ` 806` ```definition%important has_contour_integral :: "(complex \ complex) \ complex \ (real \ complex) \ bool" ``` lp15@61738 ` 807` ``` (infixr "has'_contour'_integral" 50) ``` lp15@61738 ` 808` ``` where "(f has_contour_integral i) g \ ``` lp15@60809 ` 809` ``` ((\x. f(g x) * vector_derivative g (at x within {0..1})) ``` lp15@60809 ` 810` ``` has_integral i) {0..1}" ``` lp15@60809 ` 811` wl302@69423 ` 812` ```definition%important contour_integrable_on ``` lp15@61738 ` 813` ``` (infixr "contour'_integrable'_on" 50) ``` lp15@61738 ` 814` ``` where "f contour_integrable_on g \ \i. (f has_contour_integral i) g" ``` lp15@61738 ` 815` wl302@69423 ` 816` ```definition%important contour_integral ``` wenzelm@67613 ` 817` ``` where "contour_integral g f \ SOME i. (f has_contour_integral i) g \ \ f contour_integrable_on g \ i=0" ``` wenzelm@67613 ` 818` wenzelm@67613 ` 819` ```lemma not_integrable_contour_integral: "\ f contour_integrable_on g \ contour_integral g f = 0" ``` lp15@62534 ` 820` ``` unfolding contour_integrable_on_def contour_integral_def by blast ``` lp15@62463 ` 821` lp15@62463 ` 822` ```lemma contour_integral_unique: "(f has_contour_integral i) g \ contour_integral g f = i" ``` lp15@62463 ` 823` ``` apply (simp add: contour_integral_def has_contour_integral_def contour_integrable_on_def) ``` lp15@62463 ` 824` ``` using has_integral_unique by blast ``` lp15@61738 ` 825` wl302@69423 ` 826` ```lemma has_contour_integral_eqpath: ``` lp15@62397 ` 827` ``` "\(f has_contour_integral y) p; f contour_integrable_on \; ``` paulson@62131 ` 828` ``` contour_integral p f = contour_integral \ f\ ``` paulson@62131 ` 829` ``` \ (f has_contour_integral y) \" ``` paulson@62131 ` 830` ```using contour_integrable_on_def contour_integral_unique by auto ``` paulson@62131 ` 831` lp15@61738 ` 832` ```lemma has_contour_integral_integral: ``` lp15@61738 ` 833` ``` "f contour_integrable_on i \ (f has_contour_integral (contour_integral i f)) i" ``` lp15@61738 ` 834` ``` by (metis contour_integral_unique contour_integrable_on_def) ``` lp15@61738 ` 835` lp15@61738 ` 836` ```lemma has_contour_integral_unique: ``` lp15@61738 ` 837` ``` "(f has_contour_integral i) g \ (f has_contour_integral j) g \ i = j" ``` lp15@60809 ` 838` ``` using has_integral_unique ``` lp15@61738 ` 839` ``` by (auto simp: has_contour_integral_def) ``` lp15@61738 ` 840` lp15@61738 ` 841` ```lemma has_contour_integral_integrable: "(f has_contour_integral i) g \ f contour_integrable_on g" ``` lp15@61738 ` 842` ``` using contour_integrable_on_def by blast ``` lp15@60809 ` 843` wl302@69423 ` 844` ```text\Show that we can forget about the localized derivative.\ ``` lp15@60809 ` 845` lp15@60809 ` 846` ```lemma has_integral_localized_vector_derivative: ``` lp15@60809 ` 847` ``` "((\x. f (g x) * vector_derivative g (at x within {a..b})) has_integral i) {a..b} \ ``` lp15@60809 ` 848` ``` ((\x. f (g x) * vector_derivative g (at x)) has_integral i) {a..b}" ``` lp15@60809 ` 849` ```proof - ``` lp15@68296 ` 850` ``` have *: "{a..b} - {a,b} = interior {a..b}" ``` lp15@60809 ` 851` ``` by (simp add: atLeastAtMost_diff_ends) ``` lp15@60809 ` 852` ``` show ?thesis ``` lp15@60809 ` 853` ``` apply (rule has_integral_spike_eq [of "{a,b}"]) ``` lp15@68296 ` 854` ``` apply (auto simp: at_within_interior [of _ "{a..b}"]) ``` lp15@60809 ` 855` ``` done ``` lp15@60809 ` 856` ```qed ``` lp15@60809 ` 857` lp15@60809 ` 858` ```lemma integrable_on_localized_vector_derivative: ``` lp15@60809 ` 859` ``` "(\x. f (g x) * vector_derivative g (at x within {a..b})) integrable_on {a..b} \ ``` lp15@60809 ` 860` ``` (\x. f (g x) * vector_derivative g (at x)) integrable_on {a..b}" ``` lp15@60809 ` 861` ``` by (simp add: integrable_on_def has_integral_localized_vector_derivative) ``` lp15@60809 ` 862` lp15@61738 ` 863` ```lemma has_contour_integral: ``` lp15@61738 ` 864` ``` "(f has_contour_integral i) g \ ``` lp15@60809 ` 865` ``` ((\x. f (g x) * vector_derivative g (at x)) has_integral i) {0..1}" ``` lp15@61738 ` 866` ``` by (simp add: has_integral_localized_vector_derivative has_contour_integral_def) ``` lp15@61738 ` 867` lp15@61738 ` 868` ```lemma contour_integrable_on: ``` lp15@61738 ` 869` ``` "f contour_integrable_on g \ ``` lp15@60809 ` 870` ``` (\t. f(g t) * vector_derivative g (at t)) integrable_on {0..1}" ``` lp15@61738 ` 871` ``` by (simp add: has_contour_integral integrable_on_def contour_integrable_on_def) ``` lp15@60809 ` 872` wl302@69423 ` 873` ```subsection%unimportant \Reversing a path\ ``` lp15@60809 ` 874` lp15@60809 ` 875` ```lemma valid_path_imp_reverse: ``` lp15@60809 ` 876` ``` assumes "valid_path g" ``` lp15@60809 ` 877` ``` shows "valid_path(reversepath g)" ``` lp15@60809 ` 878` ```proof - ``` lp15@68296 ` 879` ``` obtain S where "finite S" and S: "g C1_differentiable_on ({0..1} - S)" ``` lp15@61190 ` 880` ``` using assms by (auto simp: valid_path_def piecewise_C1_differentiable_on_def) ``` lp15@68296 ` 881` ``` then have "finite ((-) 1 ` S)" ``` lp15@68296 ` 882` ``` by auto ``` lp15@68296 ` 883` ``` moreover have "(reversepath g C1_differentiable_on ({0..1} - (-) 1 ` S))" ``` lp15@68296 ` 884` ``` unfolding reversepath_def ``` lp15@61190 ` 885` ``` apply (rule C1_differentiable_compose [of "\x::real. 1-x" _ g, unfolded o_def]) ``` lp15@68296 ` 886` ``` using S ``` lp15@68296 ` 887` ``` by (force simp: finite_vimageI inj_on_def C1_differentiable_on_eq continuous_on_const elim!: continuous_on_subset)+ ``` lp15@68296 ` 888` ``` ultimately show ?thesis using assms ``` lp15@61190 ` 889` ``` by (auto simp: valid_path_def piecewise_C1_differentiable_on_def path_def [symmetric]) ``` lp15@60809 ` 890` ```qed ``` lp15@60809 ` 891` lp15@62540 ` 892` ```lemma valid_path_reversepath [simp]: "valid_path(reversepath g) \ valid_path g" ``` lp15@60809 ` 893` ``` using valid_path_imp_reverse by force ``` lp15@60809 ` 894` lp15@61738 ` 895` ```lemma has_contour_integral_reversepath: ``` lp15@68296 ` 896` ``` assumes "valid_path g" and f: "(f has_contour_integral i) g" ``` lp15@61738 ` 897` ``` shows "(f has_contour_integral (-i)) (reversepath g)" ``` lp15@60809 ` 898` ```proof - ``` lp15@68296 ` 899` ``` { fix S x ``` lp15@68296 ` 900` ``` assume xs: "g C1_differentiable_on ({0..1} - S)" "x \ (-) 1 ` S" "0 \ x" "x \ 1" ``` lp15@68296 ` 901` ``` have "vector_derivative (\x. g (1 - x)) (at x within {0..1}) = ``` lp15@60809 ` 902` ``` - vector_derivative g (at (1 - x) within {0..1})" ``` lp15@68296 ` 903` ``` proof - ``` lp15@68296 ` 904` ``` obtain f' where f': "(g has_vector_derivative f') (at (1 - x))" ``` lp15@68296 ` 905` ``` using xs ``` lp15@68296 ` 906` ``` by (force simp: has_vector_derivative_def C1_differentiable_on_def) ``` lp15@68339 ` 907` ``` have "(g \ (\x. 1 - x) has_vector_derivative -1 *\<^sub>R f') (at x)" ``` lp15@68296 ` 908` ``` by (intro vector_diff_chain_within has_vector_derivative_at_within [OF f'] derivative_eq_intros | simp)+ ``` lp15@68296 ` 909` ``` then have mf': "((\x. g (1 - x)) has_vector_derivative -f') (at x)" ``` lp15@68296 ` 910` ``` by (simp add: o_def) ``` lp15@68296 ` 911` ``` show ?thesis ``` lp15@68296 ` 912` ``` using xs ``` lp15@68296 ` 913` ``` by (auto simp: vector_derivative_at_within_ivl [OF mf'] vector_derivative_at_within_ivl [OF f']) ``` lp15@68296 ` 914` ``` qed ``` lp15@60809 ` 915` ``` } note * = this ``` lp15@68296 ` 916` ``` obtain S where S: "continuous_on {0..1} g" "finite S" "g C1_differentiable_on {0..1} - S" ``` lp15@68296 ` 917` ``` using assms by (auto simp: valid_path_def piecewise_C1_differentiable_on_def) ``` lp15@68296 ` 918` ``` have "((\x. - (f (g (1 - x)) * vector_derivative g (at (1 - x) within {0..1}))) has_integral -i) ``` lp15@68296 ` 919` ``` {0..1}" ``` lp15@68296 ` 920` ``` using has_integral_affinity01 [where m= "-1" and c=1, OF f [unfolded has_contour_integral_def]] ``` lp15@68296 ` 921` ``` by (simp add: has_integral_neg) ``` lp15@68493 ` 922` ``` then show ?thesis ``` lp15@68296 ` 923` ``` using S ``` lp15@68296 ` 924` ``` apply (clarsimp simp: reversepath_def has_contour_integral_def) ``` lp15@68296 ` 925` ``` apply (rule_tac S = "(\x. 1 - x) ` S" in has_integral_spike_finite) ``` lp15@68296 ` 926` ``` apply (auto simp: *) ``` lp15@60809 ` 927` ``` done ``` lp15@60809 ` 928` ```qed ``` lp15@60809 ` 929` lp15@61738 ` 930` ```lemma contour_integrable_reversepath: ``` lp15@61738 ` 931` ``` "valid_path g \ f contour_integrable_on g \ f contour_integrable_on (reversepath g)" ``` lp15@61738 ` 932` ``` using has_contour_integral_reversepath contour_integrable_on_def by blast ``` lp15@61738 ` 933` lp15@61738 ` 934` ```lemma contour_integrable_reversepath_eq: ``` lp15@61738 ` 935` ``` "valid_path g \ (f contour_integrable_on (reversepath g) \ f contour_integrable_on g)" ``` lp15@61738 ` 936` ``` using contour_integrable_reversepath valid_path_reversepath by fastforce ``` lp15@61738 ` 937` lp15@61738 ` 938` ```lemma contour_integral_reversepath: ``` lp15@62463 ` 939` ``` assumes "valid_path g" ``` lp15@62463 ` 940` ``` shows "contour_integral (reversepath g) f = - (contour_integral g f)" ``` lp15@62463 ` 941` ```proof (cases "f contour_integrable_on g") ``` lp15@62463 ` 942` ``` case True then show ?thesis ``` lp15@62463 ` 943` ``` by (simp add: assms contour_integral_unique has_contour_integral_integral has_contour_integral_reversepath) ``` lp15@62463 ` 944` ```next ``` nipkow@69508 ` 945` ``` case False then have "\ f contour_integrable_on (reversepath g)" ``` lp15@62463 ` 946` ``` by (simp add: assms contour_integrable_reversepath_eq) ``` lp15@62463 ` 947` ``` with False show ?thesis by (simp add: not_integrable_contour_integral) ``` lp15@62463 ` 948` ```qed ``` lp15@60809 ` 949` lp15@60809 ` 950` wl302@69423 ` 951` ```subsection%unimportant \Joining two paths together\ ``` lp15@60809 ` 952` lp15@60809 ` 953` ```lemma valid_path_join: ``` lp15@60809 ` 954` ``` assumes "valid_path g1" "valid_path g2" "pathfinish g1 = pathstart g2" ``` lp15@60809 ` 955` ``` shows "valid_path(g1 +++ g2)" ``` lp15@60809 ` 956` ```proof - ``` lp15@60809 ` 957` ``` have "g1 1 = g2 0" ``` lp15@60809 ` 958` ``` using assms by (auto simp: pathfinish_def pathstart_def) ``` lp15@68339 ` 959` ``` moreover have "(g1 \ (\x. 2*x)) piecewise_C1_differentiable_on {0..1/2}" ``` lp15@61190 ` 960` ``` apply (rule piecewise_C1_differentiable_compose) ``` lp15@60809 ` 961` ``` using assms ``` lp15@61190 ` 962` ``` apply (auto simp: valid_path_def piecewise_C1_differentiable_on_def continuous_on_joinpaths) ``` nipkow@69064 ` 963` ``` apply (force intro: finite_vimageI [where h = "(*)2"] inj_onI) ``` lp15@60809 ` 964` ``` done ``` lp15@68339 ` 965` ``` moreover have "(g2 \ (\x. 2*x-1)) piecewise_C1_differentiable_on {1/2..1}" ``` lp15@61190 ` 966` ``` apply (rule piecewise_C1_differentiable_compose) ``` lp15@61190 ` 967` ``` using assms unfolding valid_path_def piecewise_C1_differentiable_on_def ``` lp15@61190 ` 968` ``` by (auto intro!: continuous_intros finite_vimageI [where h = "(\x. 2*x - 1)"] inj_onI ``` lp15@61190 ` 969` ``` simp: image_affinity_atLeastAtMost_diff continuous_on_joinpaths) ``` lp15@60809 ` 970` ``` ultimately show ?thesis ``` lp15@60809 ` 971` ``` apply (simp only: valid_path_def continuous_on_joinpaths joinpaths_def) ``` lp15@61190 ` 972` ``` apply (rule piecewise_C1_differentiable_cases) ``` lp15@60809 ` 973` ``` apply (auto simp: o_def) ``` lp15@60809 ` 974` ``` done ``` lp15@60809 ` 975` ```qed ``` lp15@60809 ` 976` lp15@61190 ` 977` ```lemma valid_path_join_D1: ``` lp15@61190 ` 978` ``` fixes g1 :: "real \ 'a::real_normed_field" ``` lp15@61190 ` 979` ``` shows "valid_path (g1 +++ g2) \ valid_path g1" ``` lp15@61190 ` 980` ``` unfolding valid_path_def ``` lp15@61190 ` 981` ``` by (rule piecewise_C1_differentiable_D1) ``` lp15@60809 ` 982` lp15@61190 ` 983` ```lemma valid_path_join_D2: ``` lp15@61190 ` 984` ``` fixes g2 :: "real \ 'a::real_normed_field" ``` lp15@61190 ` 985` ``` shows "\valid_path (g1 +++ g2); pathfinish g1 = pathstart g2\ \ valid_path g2" ``` lp15@61190 ` 986` ``` unfolding valid_path_def ``` lp15@61190 ` 987` ``` by (rule piecewise_C1_differentiable_D2) ``` lp15@60809 ` 988` lp15@60809 ` 989` ```lemma valid_path_join_eq [simp]: ``` lp15@61190 ` 990` ``` fixes g2 :: "real \ 'a::real_normed_field" ``` lp15@61190 ` 991` ``` shows "pathfinish g1 = pathstart g2 \ (valid_path(g1 +++ g2) \ valid_path g1 \ valid_path g2)" ``` lp15@60809 ` 992` ``` using valid_path_join_D1 valid_path_join_D2 valid_path_join by blast ``` lp15@60809 ` 993` lp15@61738 ` 994` ```lemma has_contour_integral_join: ``` lp15@61738 ` 995` ``` assumes "(f has_contour_integral i1) g1" "(f has_contour_integral i2) g2" ``` lp15@60809 ` 996` ``` "valid_path g1" "valid_path g2" ``` lp15@61738 ` 997` ``` shows "(f has_contour_integral (i1 + i2)) (g1 +++ g2)" ``` lp15@60809 ` 998` ```proof - ``` lp15@60809 ` 999` ``` obtain s1 s2 ``` lp15@60809 ` 1000` ``` where s1: "finite s1" "\x\{0..1} - s1. g1 differentiable at x" ``` lp15@60809 ` 1001` ``` and s2: "finite s2" "\x\{0..1} - s2. g2 differentiable at x" ``` lp15@60809 ` 1002` ``` using assms ``` lp15@61190 ` 1003` ``` by (auto simp: valid_path_def piecewise_C1_differentiable_on_def C1_differentiable_on_eq) ``` lp15@60809 ` 1004` ``` have 1: "((\x. f (g1 x) * vector_derivative g1 (at x)) has_integral i1) {0..1}" ``` lp15@60809 ` 1005` ``` and 2: "((\x. f (g2 x) * vector_derivative g2 (at x)) has_integral i2) {0..1}" ``` lp15@60809 ` 1006` ``` using assms ``` lp15@61738 ` 1007` ``` by (auto simp: has_contour_integral) ``` lp15@60809 ` 1008` ``` have i1: "((\x. (2*f (g1 (2*x))) * vector_derivative g1 (at (2*x))) has_integral i1) {0..1/2}" ``` lp15@60809 ` 1009` ``` and i2: "((\x. (2*f (g2 (2*x - 1))) * vector_derivative g2 (at (2*x - 1))) has_integral i2) {1/2..1}" ``` lp15@60809 ` 1010` ``` using has_integral_affinity01 [OF 1, where m= 2 and c=0, THEN has_integral_cmul [where c=2]] ``` lp15@60809 ` 1011` ``` has_integral_affinity01 [OF 2, where m= 2 and c="-1", THEN has_integral_cmul [where c=2]] ``` lp15@60809 ` 1012` ``` by (simp_all only: image_affinity_atLeastAtMost_div_diff, simp_all add: scaleR_conv_of_real mult_ac) ``` lp15@60809 ` 1013` ``` have g1: "\0 \ z; z*2 < 1; z*2 \ s1\ \ ``` lp15@60809 ` 1014` ``` vector_derivative (\x. if x*2 \ 1 then g1 (2*x) else g2 (2*x - 1)) (at z) = ``` lp15@60809 ` 1015` ``` 2 *\<^sub>R vector_derivative g1 (at (z*2))" for z ``` paulson@62087 ` 1016` ``` apply (rule vector_derivative_at [OF has_vector_derivative_transform_within [where f = "(\x. g1(2*x))" and d = "\z - 1/2\"]]) ``` nipkow@62390 ` 1017` ``` apply (simp_all add: dist_real_def abs_if split: if_split_asm) ``` lp15@60809 ` 1018` ``` apply (rule vector_diff_chain_at [of "\x. 2*x" 2 _ g1, simplified o_def]) ``` lp15@60809 ` 1019` ``` apply (simp add: has_vector_derivative_def has_derivative_def bounded_linear_mult_left) ``` lp15@60809 ` 1020` ``` using s1 ``` lp15@60809 ` 1021` ``` apply (auto simp: algebra_simps vector_derivative_works) ``` lp15@60809 ` 1022` ``` done ``` lp15@60809 ` 1023` ``` have g2: "\1 < z*2; z \ 1; z*2 - 1 \ s2\ \ ``` lp15@60809 ` 1024` ``` vector_derivative (\x. if x*2 \ 1 then g1 (2*x) else g2 (2*x - 1)) (at z) = ``` lp15@60809 ` 1025` ``` 2 *\<^sub>R vector_derivative g2 (at (z*2 - 1))" for z ``` paulson@62087 ` 1026` ``` apply (rule vector_derivative_at [OF has_vector_derivative_transform_within [where f = "(\x. g2 (2*x - 1))" and d = "\z - 1/2\"]]) ``` nipkow@62390 ` 1027` ``` apply (simp_all add: dist_real_def abs_if split: if_split_asm) ``` lp15@60809 ` 1028` ``` apply (rule vector_diff_chain_at [of "\x. 2*x - 1" 2 _ g2, simplified o_def]) ``` lp15@60809 ` 1029` ``` apply (simp add: has_vector_derivative_def has_derivative_def bounded_linear_mult_left) ``` lp15@60809 ` 1030` ``` using s2 ``` lp15@60809 ` 1031` ``` apply (auto simp: algebra_simps vector_derivative_works) ``` lp15@60809 ` 1032` ``` done ``` lp15@60809 ` 1033` ``` have "((\x. f ((g1 +++ g2) x) * vector_derivative (g1 +++ g2) (at x)) has_integral i1) {0..1/2}" ``` nipkow@69064 ` 1034` ``` apply (rule has_integral_spike_finite [OF _ _ i1, of "insert (1/2) ((*)2 -` s1)"]) ``` lp15@60809 ` 1035` ``` using s1 ``` nipkow@69064 ` 1036` ``` apply (force intro: finite_vimageI [where h = "(*)2"] inj_onI) ``` lp15@60809 ` 1037` ``` apply (clarsimp simp add: joinpaths_def scaleR_conv_of_real mult_ac g1) ``` lp15@60809 ` 1038` ``` done ``` lp15@60809 ` 1039` ``` moreover have "((\x. f ((g1 +++ g2) x) * vector_derivative (g1 +++ g2) (at x)) has_integral i2) {1/2..1}" ``` lp15@60809 ` 1040` ``` apply (rule has_integral_spike_finite [OF _ _ i2, of "insert (1/2) ((\x. 2*x-1) -` s2)"]) ``` lp15@60809 ` 1041` ``` using s2 ``` lp15@60809 ` 1042` ``` apply (force intro: finite_vimageI [where h = "\x. 2*x-1"] inj_onI) ``` lp15@60809 ` 1043` ``` apply (clarsimp simp add: joinpaths_def scaleR_conv_of_real mult_ac g2) ``` lp15@60809 ` 1044` ``` done ``` lp15@60809 ` 1045` ``` ultimately ``` lp15@60809 ` 1046` ``` show ?thesis ``` lp15@61738 ` 1047` ``` apply (simp add: has_contour_integral) ``` lp15@60809 ` 1048` ``` apply (rule has_integral_combine [where c = "1/2"], auto) ``` lp15@60809 ` 1049` ``` done ``` lp15@60809 ` 1050` ```qed ``` lp15@60809 ` 1051` lp15@61738 ` 1052` ```lemma contour_integrable_joinI: ``` lp15@61738 ` 1053` ``` assumes "f contour_integrable_on g1" "f contour_integrable_on g2" ``` lp15@60809 ` 1054` ``` "valid_path g1" "valid_path g2" ``` lp15@61738 ` 1055` ``` shows "f contour_integrable_on (g1 +++ g2)" ``` lp15@60809 ` 1056` ``` using assms ``` lp15@61738 ` 1057` ``` by (meson has_contour_integral_join contour_integrable_on_def) ``` lp15@61738 ` 1058` lp15@61738 ` 1059` ```lemma contour_integrable_joinD1: ``` lp15@61738 ` 1060` ``` assumes "f contour_integrable_on (g1 +++ g2)" "valid_path g1" ``` lp15@61738 ` 1061` ``` shows "f contour_integrable_on g1" ``` lp15@60809 ` 1062` ```proof - ``` lp15@60809 ` 1063` ``` obtain s1 ``` lp15@60809 ` 1064` ``` where s1: "finite s1" "\x\{0..1} - s1. g1 differentiable at x" ``` lp15@61190 ` 1065` ``` using assms by (auto simp: valid_path_def piecewise_C1_differentiable_on_def C1_differentiable_on_eq) ``` lp15@60809 ` 1066` ``` have "(\x. f ((g1 +++ g2) (x/2)) * vector_derivative (g1 +++ g2) (at (x/2))) integrable_on {0..1}" ``` lp15@60809 ` 1067` ``` using assms ``` lp15@61738 ` 1068` ``` apply (auto simp: contour_integrable_on) ``` lp15@60809 ` 1069` ``` apply (drule integrable_on_subcbox [where a=0 and b="1/2"]) ``` lp15@60809 ` 1070` ``` apply (auto intro: integrable_affinity [of _ 0 "1/2::real" "1/2" 0, simplified]) ``` lp15@60809 ` 1071` ``` done ``` lp15@60809 ` 1072` ``` then have *: "(\x. (f ((g1 +++ g2) (x/2))/2) * vector_derivative (g1 +++ g2) (at (x/2))) integrable_on {0..1}" ``` lp15@61190 ` 1073` ``` by (auto dest: integrable_cmul [where c="1/2"] simp: scaleR_conv_of_real) ``` lp15@60809 ` 1074` ``` have g1: "\0 < z; z < 1; z \ s1\ \ ``` lp15@60809 ` 1075` ``` vector_derivative (\x. if x*2 \ 1 then g1 (2*x) else g2 (2*x - 1)) (at (z/2)) = ``` lp15@60809 ` 1076` ``` 2 *\<^sub>R vector_derivative g1 (at z)" for z ``` paulson@62087 ` 1077` ``` apply (rule vector_derivative_at [OF has_vector_derivative_transform_within [where f = "(\x. g1(2*x))" and d = "\(z-1)/2\"]]) ``` nipkow@62390 ` 1078` ``` apply (simp_all add: field_simps dist_real_def abs_if split: if_split_asm) ``` lp15@60809 ` 1079` ``` apply (rule vector_diff_chain_at [of "\x. x*2" 2 _ g1, simplified o_def]) ``` lp15@60809 ` 1080` ``` using s1 ``` lp15@60809 ` 1081` ``` apply (auto simp: vector_derivative_works has_vector_derivative_def has_derivative_def bounded_linear_mult_left) ``` lp15@60809 ` 1082` ``` done ``` lp15@60809 ` 1083` ``` show ?thesis ``` lp15@60809 ` 1084` ``` using s1 ``` lp15@61738 ` 1085` ``` apply (auto simp: contour_integrable_on) ``` lp15@60809 ` 1086` ``` apply (rule integrable_spike_finite [of "{0,1} \ s1", OF _ _ *]) ``` lp15@60809 ` 1087` ``` apply (auto simp: joinpaths_def scaleR_conv_of_real g1) ``` lp15@60809 ` 1088` ``` done ``` lp15@60809 ` 1089` ```qed ``` lp15@60809 ` 1090` lp15@61738 ` 1091` ```lemma contour_integrable_joinD2: ``` lp15@61738 ` 1092` ``` assumes "f contour_integrable_on (g1 +++ g2)" "valid_path g2" ``` lp15@61738 ` 1093` ``` shows "f contour_integrable_on g2" ``` lp15@60809 ` 1094` ```proof - ``` lp15@60809 ` 1095` ``` obtain s2 ``` lp15@60809 ` 1096` ``` where s2: "finite s2" "\x\{0..1} - s2. g2 differentiable at x" ``` lp15@61190 ` 1097` ``` using assms by (auto simp: valid_path_def piecewise_C1_differentiable_on_def C1_differentiable_on_eq) ``` lp15@60809 ` 1098` ``` have "(\x. f ((g1 +++ g2) (x/2 + 1/2)) * vector_derivative (g1 +++ g2) (at (x/2 + 1/2))) integrable_on {0..1}" ``` lp15@60809 ` 1099` ``` using assms ``` lp15@61738 ` 1100` ``` apply (auto simp: contour_integrable_on) ``` lp15@60809 ` 1101` ``` apply (drule integrable_on_subcbox [where a="1/2" and b=1], auto) ``` lp15@60809 ` 1102` ``` apply (drule integrable_affinity [of _ "1/2::real" 1 "1/2" "1/2", simplified]) ``` lp15@60809 ` 1103` ``` apply (simp add: image_affinity_atLeastAtMost_diff) ``` lp15@60809 ` 1104` ``` done ``` lp15@60809 ` 1105` ``` then have *: "(\x. (f ((g1 +++ g2) (x/2 + 1/2))/2) * vector_derivative (g1 +++ g2) (at (x/2 + 1/2))) ``` lp15@60809 ` 1106` ``` integrable_on {0..1}" ``` lp15@60809 ` 1107` ``` by (auto dest: integrable_cmul [where c="1/2"] simp: scaleR_conv_of_real) ``` lp15@60809 ` 1108` ``` have g2: "\0 < z; z < 1; z \ s2\ \ ``` lp15@60809 ` 1109` ``` vector_derivative (\x. if x*2 \ 1 then g1 (2*x) else g2 (2*x - 1)) (at (z/2+1/2)) = ``` lp15@60809 ` 1110` ``` 2 *\<^sub>R vector_derivative g2 (at z)" for z ``` paulson@62087 ` 1111` ``` apply (rule vector_derivative_at [OF has_vector_derivative_transform_within [where f = "(\x. g2(2*x-1))" and d = "\z/2\"]]) ``` nipkow@62390 ` 1112` ``` apply (simp_all add: field_simps dist_real_def abs_if split: if_split_asm) ``` lp15@60809 ` 1113` ``` apply (rule vector_diff_chain_at [of "\x. x*2-1" 2 _ g2, simplified o_def]) ``` lp15@60809 ` 1114` ``` using s2 ``` lp15@60809 ` 1115` ``` apply (auto simp: has_vector_derivative_def has_derivative_def bounded_linear_mult_left ``` lp15@60809 ` 1116` ``` vector_derivative_works add_divide_distrib) ``` lp15@60809 ` 1117` ``` done ``` lp15@60809 ` 1118` ``` show ?thesis ``` lp15@60809 ` 1119` ``` using s2 ``` lp15@61738 ` 1120` ``` apply (auto simp: contour_integrable_on) ``` lp15@60809 ` 1121` ``` apply (rule integrable_spike_finite [of "{0,1} \ s2", OF _ _ *]) ``` lp15@60809 ` 1122` ``` apply (auto simp: joinpaths_def scaleR_conv_of_real g2) ``` lp15@60809 ` 1123` ``` done ``` lp15@60809 ` 1124` ```qed ``` lp15@60809 ` 1125` lp15@61738 ` 1126` ```lemma contour_integrable_join [simp]: ``` lp15@60809 ` 1127` ``` shows ``` lp15@60809 ` 1128` ``` "\valid_path g1; valid_path g2\ ``` lp15@61738 ` 1129` ``` \ f contour_integrable_on (g1 +++ g2) \ f contour_integrable_on g1 \ f contour_integrable_on g2" ``` lp15@61738 ` 1130` ```using contour_integrable_joinD1 contour_integrable_joinD2 contour_integrable_joinI by blast ``` lp15@61738 ` 1131` lp15@61738 ` 1132` ```lemma contour_integral_join [simp]: ``` lp15@60809 ` 1133` ``` shows ``` lp15@61738 ` 1134` ``` "\f contour_integrable_on g1; f contour_integrable_on g2; valid_path g1; valid_path g2\ ``` lp15@61738 ` 1135` ``` \ contour_integral (g1 +++ g2) f = contour_integral g1 f + contour_integral g2 f" ``` lp15@61738 ` 1136` ``` by (simp add: has_contour_integral_integral has_contour_integral_join contour_integral_unique) ``` lp15@60809 ` 1137` lp15@60809 ` 1138` wl302@69423 ` 1139` ```subsection%unimportant \Shifting the starting point of a (closed) path\ ``` lp15@60809 ` 1140` lp15@60809 ` 1141` ```lemma shiftpath_alt_def: "shiftpath a f = (\x. if x \ 1-a then f (a + x) else f (a + x - 1))" ``` lp15@60809 ` 1142` ``` by (auto simp: shiftpath_def) ``` lp15@60809 ` 1143` lp15@60809 ` 1144` ```lemma valid_path_shiftpath [intro]: ``` lp15@60809 ` 1145` ``` assumes "valid_path g" "pathfinish g = pathstart g" "a \ {0..1}" ``` lp15@60809 ` 1146` ``` shows "valid_path(shiftpath a g)" ``` lp15@60809 ` 1147` ``` using assms ``` lp15@60809 ` 1148` ``` apply (auto simp: valid_path_def shiftpath_alt_def) ``` lp15@61190 ` 1149` ``` apply (rule piecewise_C1_differentiable_cases) ``` lp15@60809 ` 1150` ``` apply (auto simp: algebra_simps) ``` lp15@61190 ` 1151` ``` apply (rule piecewise_C1_differentiable_affine [of g 1 a, simplified o_def scaleR_one]) ``` lp15@61190 ` 1152` ``` apply (auto simp: pathfinish_def pathstart_def elim: piecewise_C1_differentiable_on_subset) ``` lp15@61190 ` 1153` ``` apply (rule piecewise_C1_differentiable_affine [of g 1 "a-1", simplified o_def scaleR_one algebra_simps]) ``` lp15@61190 ` 1154` ``` apply (auto simp: pathfinish_def pathstart_def elim: piecewise_C1_differentiable_on_subset) ``` lp15@60809 ` 1155` ``` done ``` lp15@60809 ` 1156` lp15@61738 ` 1157` ```lemma has_contour_integral_shiftpath: ``` lp15@61738 ` 1158` ``` assumes f: "(f has_contour_integral i) g" "valid_path g" ``` lp15@60809 ` 1159` ``` and a: "a \ {0..1}" ``` lp15@61738 ` 1160` ``` shows "(f has_contour_integral i) (shiftpath a g)" ``` lp15@60809 ` 1161` ```proof - ``` lp15@60809 ` 1162` ``` obtain s ``` lp15@60809 ` 1163` ``` where s: "finite s" and g: "\x\{0..1} - s. g differentiable at x" ``` lp15@61190 ` 1164` ``` using assms by (auto simp: valid_path_def piecewise_C1_differentiable_on_def C1_differentiable_on_eq) ``` lp15@60809 ` 1165` ``` have *: "((\x. f (g x) * vector_derivative g (at x)) has_integral i) {0..1}" ``` lp15@61738 ` 1166` ``` using assms by (auto simp: has_contour_integral) ``` lp15@60809 ` 1167` ``` then have i: "i = integral {a..1} (\x. f (g x) * vector_derivative g (at x)) + ``` lp15@60809 ` 1168` ``` integral {0..a} (\x. f (g x) * vector_derivative g (at x))" ``` lp15@60809 ` 1169` ``` apply (rule has_integral_unique) ``` lp15@60809 ` 1170` ``` apply (subst add.commute) ``` hoelzl@63594 ` 1171` ``` apply (subst integral_combine) ``` lp15@60809 ` 1172` ``` using assms * integral_unique by auto ``` lp15@60809 ` 1173` ``` { fix x ``` lp15@60809 ` 1174` ``` have "0 \ x \ x + a < 1 \ x \ (\x. x - a) ` s \ ``` lp15@60809 ` 1175` ``` vector_derivative (shiftpath a g) (at x) = vector_derivative g (at (x + a))" ``` lp15@60809 ` 1176` ``` unfolding shiftpath_def ``` paulson@62087 ` 1177` ``` apply (rule vector_derivative_at [OF has_vector_derivative_transform_within [where f = "(\x. g(a+x))" and d = "dist(1-a) x"]]) ``` nipkow@62390 ` 1178` ``` apply (auto simp: field_simps dist_real_def abs_if split: if_split_asm) ``` lp15@60809 ` 1179` ``` apply (rule vector_diff_chain_at [of "\x. x+a" 1 _ g, simplified o_def scaleR_one]) ``` lp15@60809 ` 1180` ``` apply (intro derivative_eq_intros | simp)+ ``` lp15@60809 ` 1181` ``` using g ``` lp15@60809 ` 1182` ``` apply (drule_tac x="x+a" in bspec) ``` lp15@60809 ` 1183` ``` using a apply (auto simp: has_vector_derivative_def vector_derivative_works image_def add.commute) ``` lp15@60809 ` 1184` ``` done ``` lp15@60809 ` 1185` ``` } note vd1 = this ``` lp15@60809 ` 1186` ``` { fix x ``` lp15@60809 ` 1187` ``` have "1 < x + a \ x \ 1 \ x \ (\x. x - a + 1) ` s \ ``` lp15@60809 ` 1188` ``` vector_derivative (shiftpath a g) (at x) = vector_derivative g (at (x + a - 1))" ``` lp15@60809 ` 1189` ``` unfolding shiftpath_def ``` paulson@62087 ` 1190` ``` apply (rule vector_derivative_at [OF has_vector_derivative_transform_within [where f = "(\x. g(a+x-1))" and d = "dist (1-a) x"]]) ``` nipkow@62390 ` 1191` ``` apply (auto simp: field_simps dist_real_def abs_if split: if_split_asm) ``` lp15@60809 ` 1192` ``` apply (rule vector_diff_chain_at [of "\x. x+a-1" 1 _ g, simplified o_def scaleR_one]) ``` lp15@60809 ` 1193` ``` apply (intro derivative_eq_intros | simp)+ ``` lp15@60809 ` 1194` ``` using g ``` lp15@60809 ` 1195` ``` apply (drule_tac x="x+a-1" in bspec) ``` lp15@60809 ` 1196` ``` using a apply (auto simp: has_vector_derivative_def vector_derivative_works image_def add.commute) ``` lp15@60809 ` 1197` ``` done ``` lp15@60809 ` 1198` ``` } note vd2 = this ``` lp15@60809 ` 1199` ``` have va1: "(\x. f (g x) * vector_derivative g (at x)) integrable_on ({a..1})" ``` lp15@60809 ` 1200` ``` using * a by (fastforce intro: integrable_subinterval_real) ``` lp15@60809 ` 1201` ``` have v0a: "(\x. f (g x) * vector_derivative g (at x)) integrable_on ({0..a})" ``` lp15@60809 ` 1202` ``` apply (rule integrable_subinterval_real) ``` lp15@60809 ` 1203` ``` using * a by auto ``` lp15@60809 ` 1204` ``` have "((\x. f (shiftpath a g x) * vector_derivative (shiftpath a g) (at x)) ``` lp15@60809 ` 1205` ``` has_integral integral {a..1} (\x. f (g x) * vector_derivative g (at x))) {0..1 - a}" ``` lp15@60809 ` 1206` ``` apply (rule has_integral_spike_finite ``` lp15@65587 ` 1207` ``` [where S = "{1-a} \ (\x. x-a) ` s" and f = "\x. f(g(a+x)) * vector_derivative g (at(a+x))"]) ``` lp15@60809 ` 1208` ``` using s apply blast ``` lp15@60809 ` 1209` ``` using a apply (auto simp: algebra_simps vd1) ``` lp15@60809 ` 1210` ``` apply (force simp: shiftpath_def add.commute) ``` lp15@60809 ` 1211` ``` using has_integral_affinity [where m=1 and c=a, simplified, OF integrable_integral [OF va1]] ``` lp15@60809 ` 1212` ``` apply (simp add: image_affinity_atLeastAtMost_diff [where m=1 and c=a, simplified] add.commute) ``` lp15@60809 ` 1213` ``` done ``` lp15@60809 ` 1214` ``` moreover ``` lp15@60809 ` 1215` ``` have "((\x. f (shiftpath a g x) * vector_derivative (shiftpath a g) (at x)) ``` lp15@60809 ` 1216` ``` has_integral integral {0..a} (\x. f (g x) * vector_derivative g (at x))) {1 - a..1}" ``` lp15@60809 ` 1217` ``` apply (rule has_integral_spike_finite ``` lp15@65587 ` 1218` ``` [where S = "{1-a} \ (\x. x-a+1) ` s" and f = "\x. f(g(a+x-1)) * vector_derivative g (at(a+x-1))"]) ``` lp15@60809 ` 1219` ``` using s apply blast ``` lp15@60809 ` 1220` ``` using a apply (auto simp: algebra_simps vd2) ``` lp15@60809 ` 1221` ``` apply (force simp: shiftpath_def add.commute) ``` lp15@60809 ` 1222` ``` using has_integral_affinity [where m=1 and c="a-1", simplified, OF integrable_integral [OF v0a]] ``` lp15@60809 ` 1223` ``` apply (simp add: image_affinity_atLeastAtMost [where m=1 and c="1-a", simplified]) ``` lp15@60809 ` 1224` ``` apply (simp add: algebra_simps) ``` lp15@60809 ` 1225` ``` done ``` lp15@60809 ` 1226` ``` ultimately show ?thesis ``` lp15@60809 ` 1227` ``` using a ``` lp15@61738 ` 1228` ``` by (auto simp: i has_contour_integral intro: has_integral_combine [where c = "1-a"]) ``` lp15@60809 ` 1229` ```qed ``` lp15@60809 ` 1230` lp15@61738 ` 1231` ```lemma has_contour_integral_shiftpath_D: ``` lp15@61738 ` 1232` ``` assumes "(f has_contour_integral i) (shiftpath a g)" ``` lp15@60809 ` 1233` ``` "valid_path g" "pathfinish g = pathstart g" "a \ {0..1}" ``` lp15@61738 ` 1234` ``` shows "(f has_contour_integral i) g" ``` lp15@60809 ` 1235` ```proof - ``` lp15@60809 ` 1236` ``` obtain s ``` lp15@60809 ` 1237` ``` where s: "finite s" and g: "\x\{0..1} - s. g differentiable at x" ``` lp15@61190 ` 1238` ``` using assms by (auto simp: valid_path_def piecewise_C1_differentiable_on_def C1_differentiable_on_eq) ``` lp15@60809 ` 1239` ``` { fix x ``` lp15@60809 ` 1240` ``` assume x: "0 < x" "x < 1" "x \ s" ``` lp15@60809 ` 1241` ``` then have gx: "g differentiable at x" ``` lp15@60809 ` 1242` ``` using g by auto ``` lp15@60809 ` 1243` ``` have "vector_derivative g (at x within {0..1}) = ``` lp15@60809 ` 1244` ``` vector_derivative (shiftpath (1 - a) (shiftpath a g)) (at x within {0..1})" ``` lp15@60809 ` 1245` ``` apply (rule vector_derivative_at_within_ivl ``` lp15@60809 ` 1246` ``` [OF has_vector_derivative_transform_within_open ``` lp15@68239 ` 1247` ``` [where f = "(shiftpath (1 - a) (shiftpath a g))" and S = "{0<..<1}-s"]]) ``` lp15@60809 ` 1248` ``` using s g assms x ``` lp15@60809 ` 1249` ``` apply (auto simp: finite_imp_closed open_Diff shiftpath_shiftpath ``` lp15@68296 ` 1250` ``` at_within_interior [of _ "{0..1}"] vector_derivative_works [symmetric]) ``` paulson@62087 ` 1251` ``` apply (rule differentiable_transform_within [OF gx, of "min x (1-x)"]) ``` nipkow@62390 ` 1252` ``` apply (auto simp: dist_real_def shiftpath_shiftpath abs_if split: if_split_asm) ``` lp15@60809 ` 1253` ``` done ``` lp15@60809 ` 1254` ``` } note vd = this ``` lp15@61738 ` 1255` ``` have fi: "(f has_contour_integral i) (shiftpath (1 - a) (shiftpath a g))" ``` lp15@61738 ` 1256` ``` using assms by (auto intro!: has_contour_integral_shiftpath) ``` lp15@60809 ` 1257` ``` show ?thesis ``` lp15@61738 ` 1258` ``` apply (simp add: has_contour_integral_def) ``` lp15@61738 ` 1259` ``` apply (rule has_integral_spike_finite [of "{0,1} \ s", OF _ _ fi [unfolded has_contour_integral_def]]) ``` lp15@60809 ` 1260` ``` using s assms vd ``` lp15@60809 ` 1261` ``` apply (auto simp: Path_Connected.shiftpath_shiftpath) ``` lp15@60809 ` 1262` ``` done ``` lp15@60809 ` 1263` ```qed ``` lp15@60809 ` 1264` lp15@61738 ` 1265` ```lemma has_contour_integral_shiftpath_eq: ``` lp15@60809 ` 1266` ``` assumes "valid_path g" "pathfinish g = pathstart g" "a \ {0..1}" ``` lp15@61738 ` 1267` ``` shows "(f has_contour_integral i) (shiftpath a g) \ (f has_contour_integral i) g" ``` lp15@61738 ` 1268` ``` using assms has_contour_integral_shiftpath has_contour_integral_shiftpath_D by blast ``` lp15@61738 ` 1269` lp15@62463 ` 1270` ```lemma contour_integrable_on_shiftpath_eq: ``` lp15@62463 ` 1271` ``` assumes "valid_path g" "pathfinish g = pathstart g" "a \ {0..1}" ``` lp15@62463 ` 1272` ``` shows "f contour_integrable_on (shiftpath a g) \ f contour_integrable_on g" ``` lp15@62463 ` 1273` ```using assms contour_integrable_on_def has_contour_integral_shiftpath_eq by auto ``` lp15@62463 ` 1274` lp15@61738 ` 1275` ```lemma contour_integral_shiftpath: ``` lp15@60809 ` 1276` ``` assumes "valid_path g" "pathfinish g = pathstart g" "a \ {0..1}" ``` lp15@61738 ` 1277` ``` shows "contour_integral (shiftpath a g) f = contour_integral g f" ``` lp15@62534 ` 1278` ``` using assms ``` lp15@62463 ` 1279` ``` by (simp add: contour_integral_def contour_integrable_on_def has_contour_integral_shiftpath_eq) ``` lp15@60809 ` 1280` lp15@60809 ` 1281` wl302@69423 ` 1282` ```subsection%unimportant \More about straight-line paths\ ``` lp15@60809 ` 1283` lp15@60809 ` 1284` ```lemma has_vector_derivative_linepath_within: ``` lp15@60809 ` 1285` ``` "(linepath a b has_vector_derivative (b - a)) (at x within s)" ``` lp15@60809 ` 1286` ```apply (simp add: linepath_def has_vector_derivative_def algebra_simps) ``` lp15@60809 ` 1287` ```apply (rule derivative_eq_intros | simp)+ ``` lp15@60809 ` 1288` ```done ``` lp15@60809 ` 1289` lp15@60809 ` 1290` ```lemma vector_derivative_linepath_within: ``` lp15@60809 ` 1291` ``` "x \ {0..1} \ vector_derivative (linepath a b) (at x within {0..1}) = b - a" ``` immler@67685 ` 1292` ``` apply (rule vector_derivative_within_cbox [of 0 "1::real", simplified]) ``` lp15@60809 ` 1293` ``` apply (auto simp: has_vector_derivative_linepath_within) ``` lp15@60809 ` 1294` ``` done ``` lp15@60809 ` 1295` lp15@61190 ` 1296` ```lemma vector_derivative_linepath_at [simp]: "vector_derivative (linepath a b) (at x) = b - a" ``` lp15@60809 ` 1297` ``` by (simp add: has_vector_derivative_linepath_within vector_derivative_at) ``` lp15@60809 ` 1298` lp15@61190 ` 1299` ```lemma valid_path_linepath [iff]: "valid_path (linepath a b)" ``` lp15@61190 ` 1300` ``` apply (simp add: valid_path_def piecewise_C1_differentiable_on_def C1_differentiable_on_eq continuous_on_linepath) ``` lp15@61190 ` 1301` ``` apply (rule_tac x="{}" in exI) ``` lp15@61190 ` 1302` ``` apply (simp add: differentiable_on_def differentiable_def) ``` lp15@61190 ` 1303` ``` using has_vector_derivative_def has_vector_derivative_linepath_within ``` lp15@61190 ` 1304` ``` apply (fastforce simp add: continuous_on_eq_continuous_within) ``` lp15@61190 ` 1305` ``` done ``` lp15@61190 ` 1306` lp15@61738 ` 1307` ```lemma has_contour_integral_linepath: ``` lp15@61738 ` 1308` ``` shows "(f has_contour_integral i) (linepath a b) \ ``` lp15@60809 ` 1309` ``` ((\x. f(linepath a b x) * (b - a)) has_integral i) {0..1}" ``` lp15@61738 ` 1310` ``` by (simp add: has_contour_integral vector_derivative_linepath_at) ``` lp15@60809 ` 1311` lp15@60809 ` 1312` ```lemma linepath_in_path: ``` lp15@60809 ` 1313` ``` shows "x \ {0..1} \ linepath a b x \ closed_segment a b" ``` lp15@60809 ` 1314` ``` by (auto simp: segment linepath_def) ``` lp15@60809 ` 1315` lp15@60809 ` 1316` ```lemma linepath_image_01: "linepath a b ` {0..1} = closed_segment a b" ``` lp15@60809 ` 1317` ``` by (auto simp: segment linepath_def) ``` lp15@60809 ` 1318` lp15@60809 ` 1319` ```lemma linepath_in_convex_hull: ``` lp15@60809 ` 1320` ``` fixes x::real ``` lp15@60809 ` 1321` ``` assumes a: "a \ convex hull s" ``` lp15@60809 ` 1322` ``` and b: "b \ convex hull s" ``` lp15@60809 ` 1323` ``` and x: "0\x" "x\1" ``` lp15@60809 ` 1324` ``` shows "linepath a b x \ convex hull s" ``` lp15@60809 ` 1325` ``` apply (rule closed_segment_subset_convex_hull [OF a b, THEN subsetD]) ``` lp15@60809 ` 1326` ``` using x ``` lp15@60809 ` 1327` ``` apply (auto simp: linepath_image_01 [symmetric]) ``` lp15@60809 ` 1328` ``` done ``` lp15@60809 ` 1329` lp15@60809 ` 1330` ```lemma Re_linepath: "Re(linepath (of_real a) (of_real b) x) = (1 - x)*a + x*b" ``` lp15@60809 ` 1331` ``` by (simp add: linepath_def) ``` lp15@60809 ` 1332` lp15@60809 ` 1333` ```lemma Im_linepath: "Im(linepath (of_real a) (of_real b) x) = 0" ``` lp15@60809 ` 1334` ``` by (simp add: linepath_def) ``` lp15@60809 ` 1335` lp15@61738 ` 1336` ```lemma has_contour_integral_trivial [iff]: "(f has_contour_integral 0) (linepath a a)" ``` lp15@61738 ` 1337` ``` by (simp add: has_contour_integral_linepath) ``` lp15@61738 ` 1338` lp15@68296 ` 1339` ```lemma has_contour_integral_trivial_iff [simp]: "(f has_contour_integral i) (linepath a a) \ i=0" ``` lp15@68296 ` 1340` ``` using has_contour_integral_unique by blast ``` lp15@68296 ` 1341` lp15@61738 ` 1342` ```lemma contour_integral_trivial [simp]: "contour_integral (linepath a a) f = 0" ``` lp15@61738 ` 1343` ``` using has_contour_integral_trivial contour_integral_unique by blast ``` lp15@60809 ` 1344` eberlm@68721 ` 1345` ```lemma differentiable_linepath [intro]: "linepath a b differentiable at x within A" ``` eberlm@68721 ` 1346` ``` by (auto simp: linepath_def) ``` eberlm@68721 ` 1347` eberlm@68721 ` 1348` ```lemma bounded_linear_linepath: ``` eberlm@68721 ` 1349` ``` assumes "bounded_linear f" ``` eberlm@68721 ` 1350` ``` shows "f (linepath a b x) = linepath (f a) (f b) x" ``` eberlm@68721 ` 1351` ```proof - ``` eberlm@68721 ` 1352` ``` interpret f: bounded_linear f by fact ``` eberlm@68721 ` 1353` ``` show ?thesis by (simp add: linepath_def f.add f.scale) ``` eberlm@68721 ` 1354` ```qed ``` eberlm@68721 ` 1355` eberlm@68721 ` 1356` ```lemma bounded_linear_linepath': ``` eberlm@68721 ` 1357` ``` assumes "bounded_linear f" ``` eberlm@68721 ` 1358` ``` shows "f \ linepath a b = linepath (f a) (f b)" ``` eberlm@68721 ` 1359` ``` using bounded_linear_linepath[OF assms] by (simp add: fun_eq_iff) ``` eberlm@68721 ` 1360` eberlm@68721 ` 1361` ```lemma cnj_linepath: "cnj (linepath a b x) = linepath (cnj a) (cnj b) x" ``` eberlm@68721 ` 1362` ``` by (simp add: linepath_def) ``` eberlm@68721 ` 1363` eberlm@68721 ` 1364` ```lemma cnj_linepath': "cnj \ linepath a b = linepath (cnj a) (cnj b)" ``` eberlm@68721 ` 1365` ``` by (simp add: linepath_def fun_eq_iff) ``` eberlm@68721 ` 1366` lp15@60809 ` 1367` ```subsection\Relation to subpath construction\ ``` lp15@60809 ` 1368` lp15@60809 ` 1369` ```lemma valid_path_subpath: ``` lp15@60809 ` 1370` ``` fixes g :: "real \ 'a :: real_normed_vector" ``` lp15@60809 ` 1371` ``` assumes "valid_path g" "u \ {0..1}" "v \ {0..1}" ``` lp15@60809 ` 1372` ``` shows "valid_path(subpath u v g)" ``` lp15@60809 ` 1373` ```proof (cases "v=u") ``` lp15@60809 ` 1374` ``` case True ``` lp15@60809 ` 1375` ``` then show ?thesis ``` lp15@61190 ` 1376` ``` unfolding valid_path_def subpath_def ``` lp15@61190 ` 1377` ``` by (force intro: C1_differentiable_on_const C1_differentiable_imp_piecewise) ``` lp15@60809 ` 1378` ```next ``` lp15@60809 ` 1379` ``` case False ``` lp15@68339 ` 1380` ``` have "(g \ (\x. ((v-u) * x + u))) piecewise_C1_differentiable_on {0..1}" ``` lp15@61190 ` 1381` ``` apply (rule piecewise_C1_differentiable_compose) ``` lp15@61190 ` 1382` ``` apply (simp add: C1_differentiable_imp_piecewise) ``` lp15@60809 ` 1383` ``` apply (simp add: image_affinity_atLeastAtMost) ``` lp15@60809 ` 1384` ``` using assms False ``` lp15@61190 ` 1385` ``` apply (auto simp: algebra_simps valid_path_def piecewise_C1_differentiable_on_subset) ``` lp15@60809 ` 1386` ``` apply (subst Int_commute) ``` lp15@60809 ` 1387` ``` apply (auto simp: inj_on_def algebra_simps crossproduct_eq finite_vimage_IntI) ``` lp15@60809 ` 1388` ``` done ``` lp15@60809 ` 1389` ``` then show ?thesis ``` lp15@60809 ` 1390` ``` by (auto simp: o_def valid_path_def subpath_def) ``` lp15@60809 ` 1391` ```qed ``` lp15@60809 ` 1392` lp15@61738 ` 1393` ```lemma has_contour_integral_subpath_refl [iff]: "(f has_contour_integral 0) (subpath u u g)" ``` lp15@61738 ` 1394` ``` by (simp add: has_contour_integral subpath_def) ``` lp15@61738 ` 1395` lp15@61738 ` 1396` ```lemma contour_integrable_subpath_refl [iff]: "f contour_integrable_on (subpath u u g)" ``` lp15@61738 ` 1397` ``` using has_contour_integral_subpath_refl contour_integrable_on_def by blast ``` lp15@61738 ` 1398` lp15@61738 ` 1399` ```lemma contour_integral_subpath_refl [simp]: "contour_integral (subpath u u g) f = 0" ``` lp15@61738 ` 1400` ``` by (simp add: has_contour_integral_subpath_refl contour_integral_unique) ``` lp15@61738 ` 1401` lp15@61738 ` 1402` ```lemma has_contour_integral_subpath: ``` lp15@61738 ` 1403` ``` assumes f: "f contour_integrable_on g" and g: "valid_path g" ``` lp15@60809 ` 1404` ``` and uv: "u \ {0..1}" "v \ {0..1}" "u \ v" ``` lp15@61738 ` 1405` ``` shows "(f has_contour_integral integral {u..v} (\x. f(g x) * vector_derivative g (at x))) ``` lp15@60809 ` 1406` ``` (subpath u v g)" ``` lp15@60809 ` 1407` ```proof (cases "v=u") ``` lp15@60809 ` 1408` ``` case True ``` lp15@60809 ` 1409` ``` then show ?thesis ``` lp15@61738 ` 1410` ``` using f by (simp add: contour_integrable_on_def subpath_def has_contour_integral) ``` lp15@60809 ` 1411` ```next ``` lp15@60809 ` 1412` ``` case False ``` lp15@60809 ` 1413` ``` obtain s where s: "\x. x \ {0..1} - s \ g differentiable at x" and fs: "finite s" ``` lp15@61190 ` 1414` ``` using g unfolding piecewise_C1_differentiable_on_def C1_differentiable_on_eq valid_path_def by blast ``` lp15@60809 ` 1415` ``` have *: "((\x. f (g ((v - u) * x + u)) * vector_derivative g (at ((v - u) * x + u))) ``` lp15@60809 ` 1416` ``` has_integral (1 / (v - u)) * integral {u..v} (\t. f (g t) * vector_derivative g (at t))) ``` lp15@60809 ` 1417` ``` {0..1}" ``` lp15@60809 ` 1418` ``` using f uv ``` lp15@61738 ` 1419` ``` apply (simp add: contour_integrable_on subpath_def has_contour_integral) ``` lp15@60809 ` 1420` ``` apply (drule integrable_on_subcbox [where a=u and b=v, simplified]) ``` lp15@60809 ` 1421` ``` apply (simp_all add: has_integral_integral) ``` lp15@60809 ` 1422` ``` apply (drule has_integral_affinity [where m="v-u" and c=u, simplified]) ``` lp15@60809 ` 1423` ``` apply (simp_all add: False image_affinity_atLeastAtMost_div_diff scaleR_conv_of_real) ``` lp15@60809 ` 1424` ``` apply (simp add: divide_simps False) ``` lp15@60809 ` 1425` ``` done ``` lp15@60809 ` 1426` ``` { fix x ``` lp15@60809 ` 1427` ``` have "x \ {0..1} \ ``` lp15@60809 ` 1428` ``` x \ (\t. (v-u) *\<^sub>R t + u) -` s \ ``` lp15@60809 ` 1429` ``` vector_derivative (\x. g ((v-u) * x + u)) (at x) = (v-u) *\<^sub>R vector_derivative g (at ((v-u) * x + u))" ``` lp15@60809 ` 1430` ``` apply (rule vector_derivative_at [OF vector_diff_chain_at [simplified o_def]]) ``` lp15@60809 ` 1431` ``` apply (intro derivative_eq_intros | simp)+ ``` lp15@60809 ` 1432` ``` apply (cut_tac s [of "(v - u) * x + u"]) ``` lp15@60809 ` 1433` ``` using uv mult_left_le [of x "v-u"] ``` lp15@60809 ` 1434` ``` apply (auto simp: vector_derivative_works) ``` lp15@60809 ` 1435` ``` done ``` lp15@60809 ` 1436` ``` } note vd = this ``` lp15@60809 ` 1437` ``` show ?thesis ``` lp15@60809 ` 1438` ``` apply (cut_tac has_integral_cmul [OF *, where c = "v-u"]) ``` lp15@60809 ` 1439` ``` using fs assms ``` lp15@61738 ` 1440` ``` apply (simp add: False subpath_def has_contour_integral) ``` lp15@65587 ` 1441` ``` apply (rule_tac S = "(\t. ((v-u) *\<^sub>R t + u)) -` s" in has_integral_spike_finite) ``` lp15@60809 ` 1442` ``` apply (auto simp: inj_on_def False finite_vimageI vd scaleR_conv_of_real) ``` lp15@60809 ` 1443` ``` done ``` lp15@60809 ` 1444` ```qed ``` lp15@60809 ` 1445` lp15@61738 ` 1446` ```lemma contour_integrable_subpath: ``` lp15@61738 ` 1447` ``` assumes "f contour_integrable_on g" "valid_path g" "u \ {0..1}" "v \ {0..1}" ``` lp15@61738 ` 1448` ``` shows "f contour_integrable_on (subpath u v g)" ``` lp15@60809 ` 1449` ``` apply (cases u v rule: linorder_class.le_cases) ``` lp15@61738 ` 1450` ``` apply (metis contour_integrable_on_def has_contour_integral_subpath [OF assms]) ``` lp15@60809 ` 1451` ``` apply (subst reversepath_subpath [symmetric]) ``` lp15@61738 ` 1452` ``` apply (rule contour_integrable_reversepath) ``` lp15@60809 ` 1453` ``` using assms apply (blast intro: valid_path_subpath) ``` lp15@61738 ` 1454` ``` apply (simp add: contour_integrable_on_def) ``` lp15@61738 ` 1455` ``` using assms apply (blast intro: has_contour_integral_subpath) ``` lp15@60809 ` 1456` ``` done ``` lp15@60809 ` 1457` lp15@61738 ` 1458` ```lemma has_integral_contour_integral_subpath: ``` lp15@61738 ` 1459` ``` assumes "f contour_integrable_on g" "valid_path g" "u \ {0..1}" "v \ {0..1}" "u \ v" ``` lp15@60809 ` 1460` ``` shows "(((\x. f(g x) * vector_derivative g (at x))) ``` lp15@61738 ` 1461` ``` has_integral contour_integral (subpath u v g) f) {u..v}" ``` lp15@60809 ` 1462` ``` using assms ``` lp15@60809 ` 1463` ``` apply (auto simp: has_integral_integrable_integral) ``` lp15@66507 ` 1464` ``` apply (rule integrable_on_subcbox [where a=u and b=v and S = "{0..1}", simplified]) ``` lp15@61738 ` 1465` ``` apply (auto simp: contour_integral_unique [OF has_contour_integral_subpath] contour_integrable_on) ``` lp15@60809 ` 1466` ``` done ``` lp15@60809 ` 1467` lp15@61738 ` 1468` ```lemma contour_integral_subcontour_integral: ``` lp15@61738 ` 1469` ``` assumes "f contour_integrable_on g" "valid_path g" "u \ {0..1}" "v \ {0..1}" "u \ v" ``` lp15@61738 ` 1470` ``` shows "contour_integral (subpath u v g) f = ``` lp15@60809 ` 1471` ``` integral {u..v} (\x. f(g x) * vector_derivative g (at x))" ``` lp15@61738 ` 1472` ``` using assms has_contour_integral_subpath contour_integral_unique by blast ``` lp15@61738 ` 1473` lp15@61738 ` 1474` ```lemma contour_integral_subpath_combine_less: ``` lp15@61738 ` 1475` ``` assumes "f contour_integrable_on g" "valid_path g" "u \ {0..1}" "v \ {0..1}" "w \ {0..1}" ``` lp15@60809 ` 1476` ``` "u {0..1}" "v \ {0..1}" "w \ {0..1}" ``` lp15@61738 ` 1487` ``` shows "contour_integral (subpath u v g) f + contour_integral (subpath v w g) f = ``` lp15@61738 ` 1488` ``` contour_integral (subpath u w g) f" ``` lp15@60809 ` 1489` ```proof (cases "u\v \ v\w \ u\w") ``` lp15@60809 ` 1490` ``` case True ``` lp15@60809 ` 1491` ``` have *: "subpath v u g = reversepath(subpath u v g) \ ``` lp15@60809 ` 1492` ``` subpath w u g = reversepath(subpath u w g) \ ``` lp15@60809 ` 1493` ``` subpath w v g = reversepath(subpath v w g)" ``` lp15@60809 ` 1494` ``` by (auto simp: reversepath_subpath) ``` lp15@60809 ` 1495` ``` have "u < v \ v < w \ ``` lp15@60809 ` 1496` ``` u < w \ w < v \ ``` lp15@60809 ` 1497` ``` v < u \ u < w \ ``` lp15@60809 ` 1498` ``` v < w \ w < u \ ``` lp15@60809 ` 1499` ``` w < u \ u < v \ ``` lp15@60809 ` 1500` ``` w < v \ v < u" ``` lp15@60809 ` 1501` ``` using True assms by linarith ``` lp15@60809 ` 1502` ``` with assms show ?thesis ``` lp15@61738 ` 1503` ``` using contour_integral_subpath_combine_less [of f g u v w] ``` lp15@61738 ` 1504` ``` contour_integral_subpath_combine_less [of f g u w v] ``` lp15@61738 ` 1505` ``` contour_integral_subpath_combine_less [of f g v u w] ``` lp15@61738 ` 1506` ``` contour_integral_subpath_combine_less [of f g v w u] ``` lp15@61738 ` 1507` ``` contour_integral_subpath_combine_less [of f g w u v] ``` lp15@61738 ` 1508` ``` contour_integral_subpath_combine_less [of f g w v u] ``` lp15@60809 ` 1509` ``` apply simp ``` lp15@60809 ` 1510` ``` apply (elim disjE) ``` lp15@61738 ` 1511` ``` apply (auto simp: * contour_integral_reversepath contour_integrable_subpath ``` lp15@60809 ` 1512` ``` valid_path_reversepath valid_path_subpath algebra_simps) ``` lp15@60809 ` 1513` ``` done ``` lp15@60809 ` 1514` ```next ``` lp15@60809 ` 1515` ``` case False ``` lp15@60809 ` 1516` ``` then show ?thesis ``` lp15@61738 ` 1517` ``` apply (auto simp: contour_integral_subpath_refl) ``` lp15@60809 ` 1518` ``` using assms ``` lp15@61738 ` 1519` ``` by (metis eq_neg_iff_add_eq_0 contour_integrable_subpath contour_integral_reversepath reversepath_subpath valid_path_subpath) ``` lp15@60809 ` 1520` ```qed ``` lp15@60809 ` 1521` lp15@61738 ` 1522` ```lemma contour_integral_integral: ``` lp15@62463 ` 1523` ``` "contour_integral g f = integral {0..1} (\x. f (g x) * vector_derivative g (at x))" ``` lp15@62463 ` 1524` ``` by (simp add: contour_integral_def integral_def has_contour_integral contour_integrable_on) ``` lp15@60809 ` 1525` eberlm@68721 ` 1526` ```lemma contour_integral_cong: ``` eberlm@68721 ` 1527` ``` assumes "g = g'" "\x. x \ path_image g \ f x = f' x" ``` eberlm@68721 ` 1528` ``` shows "contour_integral g f = contour_integral g' f'" ``` eberlm@68721 ` 1529` ``` unfolding contour_integral_integral using assms ``` eberlm@68721 ` 1530` ``` by (intro integral_cong) (auto simp: path_image_def) ``` eberlm@68721 ` 1531` eberlm@68721 ` 1532` eberlm@68721 ` 1533` ```text \Contour integral along a segment on the real axis\ ``` eberlm@68721 ` 1534` eberlm@68721 ` 1535` ```lemma has_contour_integral_linepath_Reals_iff: ``` eberlm@68721 ` 1536` ``` fixes a b :: complex and f :: "complex \ complex" ``` eberlm@68721 ` 1537` ``` assumes "a \ Reals" "b \ Reals" "Re a < Re b" ``` eberlm@68721 ` 1538` ``` shows "(f has_contour_integral I) (linepath a b) \ ``` eberlm@68721 ` 1539` ``` ((\x. f (of_real x)) has_integral I) {Re a..Re b}" ``` eberlm@68721 ` 1540` ```proof - ``` eberlm@68721 ` 1541` ``` from assms have [simp]: "of_real (Re a) = a" "of_real (Re b) = b" ``` eberlm@68721 ` 1542` ``` by (simp_all add: complex_eq_iff) ``` eberlm@68721 ` 1543` ``` from assms have "a \ b" by auto ``` eberlm@68721 ` 1544` ``` have "((\x. f (of_real x)) has_integral I) (cbox (Re a) (Re b)) \ ``` eberlm@68721 ` 1545` ``` ((\x. f (a + b * of_real x - a * of_real x)) has_integral I /\<^sub>R (Re b - Re a)) {0..1}" ``` eberlm@68721 ` 1546` ``` by (subst has_integral_affinity_iff [of "Re b - Re a" _ "Re a", symmetric]) ``` eberlm@68721 ` 1547` ``` (insert assms, simp_all add: field_simps scaleR_conv_of_real) ``` eberlm@68721 ` 1548` ``` also have "(\x. f (a + b * of_real x - a * of_real x)) = ``` eberlm@68721 ` 1549` ``` (\x. (f (a + b * of_real x - a * of_real x) * (b - a)) /\<^sub>R (Re b - Re a))" ``` eberlm@68721 ` 1550` ``` using \a \ b\ by (auto simp: field_simps fun_eq_iff scaleR_conv_of_real) ``` eberlm@68721 ` 1551` ``` also have "(\ has_integral I /\<^sub>R (Re b - Re a)) {0..1} \ ``` eberlm@68721 ` 1552` ``` ((\x. f (linepath a b x) * (b - a)) has_integral I) {0..1}" using assms ``` eberlm@68721 ` 1553` ``` by (subst has_integral_cmul_iff) (auto simp: linepath_def scaleR_conv_of_real algebra_simps) ``` eberlm@68721 ` 1554` ``` also have "\ \ (f has_contour_integral I) (linepath a b)" unfolding has_contour_integral_def ``` eberlm@68721 ` 1555` ``` by (intro has_integral_cong) (simp add: vector_derivative_linepath_within) ``` eberlm@68721 ` 1556` ``` finally show ?thesis by simp ``` eberlm@68721 ` 1557` ```qed ``` eberlm@68721 ` 1558` eberlm@68721 ` 1559` ```lemma contour_integrable_linepath_Reals_iff: ``` eberlm@68721 ` 1560` ``` fixes a b :: complex and f :: "complex \ complex" ``` eberlm@68721 ` 1561` ``` assumes "a \ Reals" "b \ Reals" "Re a < Re b" ``` eberlm@68721 ` 1562` ``` shows "(f contour_integrable_on linepath a b) \ ``` eberlm@68721 ` 1563` ``` (\x. f (of_real x)) integrable_on {Re a..Re b}" ``` eberlm@68721 ` 1564` ``` using has_contour_integral_linepath_Reals_iff[OF assms, of f] ``` eberlm@68721 ` 1565` ``` by (auto simp: contour_integrable_on_def integrable_on_def) ``` eberlm@68721 ` 1566` eberlm@68721 ` 1567` ```lemma contour_integral_linepath_Reals_eq: ``` eberlm@68721 ` 1568` ``` fixes a b :: complex and f :: "complex \ complex" ``` eberlm@68721 ` 1569` ``` assumes "a \ Reals" "b \ Reals" "Re a < Re b" ``` eberlm@68721 ` 1570` ``` shows "contour_integral (linepath a b) f = integral {Re a..Re b} (\x. f (of_real x))" ``` eberlm@68721 ` 1571` ```proof (cases "f contour_integrable_on linepath a b") ``` eberlm@68721 ` 1572` ``` case True ``` eberlm@68721 ` 1573` ``` thus ?thesis using has_contour_integral_linepath_Reals_iff[OF assms, of f] ``` eberlm@68721 ` 1574` ``` using has_contour_integral_integral has_contour_integral_unique by blast ``` eberlm@68721 ` 1575` ```next ``` eberlm@68721 ` 1576` ``` case False ``` eberlm@68721 ` 1577` ``` thus ?thesis using contour_integrable_linepath_Reals_iff[OF assms, of f] ``` eberlm@68721 ` 1578` ``` by (simp add: not_integrable_contour_integral not_integrable_integral) ``` eberlm@68721 ` 1579` ```qed ``` eberlm@68721 ` 1580` eberlm@68721 ` 1581` lp15@60809 ` 1582` lp15@60809 ` 1583` ```text\Cauchy's theorem where there's a primitive\ ``` lp15@60809 ` 1584` lp15@61738 ` 1585` ```lemma contour_integral_primitive_lemma: ``` lp15@60809 ` 1586` ``` fixes f :: "complex \ complex" and g :: "real \ complex" ``` lp15@60809 ` 1587` ``` assumes "a \ b" ``` lp15@60809 ` 1588` ``` and "\x. x \ s \ (f has_field_derivative f' x) (at x within s)" ``` lp15@60809 ` 1589` ``` and "g piecewise_differentiable_on {a..b}" "\x. x \ {a..b} \ g x \ s" ``` lp15@60809 ` 1590` ``` shows "((\x. f'(g x) * vector_derivative g (at x within {a..b})) ``` lp15@60809 ` 1591` ``` has_integral (f(g b) - f(g a))) {a..b}" ``` lp15@60809 ` 1592` ```proof - ``` lp15@61190 ` 1593` ``` obtain k where k: "finite k" "\x\{a..b} - k. g differentiable (at x within {a..b})" and cg: "continuous_on {a..b} g" ``` lp15@60809 ` 1594` ``` using assms by (auto simp: piecewise_differentiable_on_def) ``` lp15@60809 ` 1595` ``` have cfg: "continuous_on {a..b} (\x. f (g x))" ``` lp15@60809 ` 1596` ``` apply (rule continuous_on_compose [OF cg, unfolded o_def]) ``` lp15@60809 ` 1597` ``` using assms ``` lp15@62534 ` 1598` ``` apply (metis field_differentiable_def field_differentiable_imp_continuous_at continuous_on_eq_continuous_within continuous_on_subset image_subset_iff) ``` lp15@60809 ` 1599` ``` done ``` lp15@60809 ` 1600` ``` { fix x::real ``` lp15@60809 ` 1601` ``` assume a: "a < x" and b: "x < b" and xk: "x \ k" ``` lp15@60809 ` 1602` ``` then have "g differentiable at x within {a..b}" ``` lp15@60809 ` 1603` ``` using k by (simp add: differentiable_at_withinI) ``` lp15@60809 ` 1604` ``` then have "(g has_vector_derivative vector_derivative g (at x within {a..b})) (at x within {a..b})" ``` lp15@60809 ` 1605` ``` by (simp add: vector_derivative_works has_field_derivative_def scaleR_conv_of_real) ``` lp15@60809 ` 1606` ``` then have gdiff: "(g has_derivative (\u. u * vector_derivative g (at x within {a..b}))) (at x within {a..b})" ``` lp15@60809 ` 1607` ``` by (simp add: has_vector_derivative_def scaleR_conv_of_real) ``` lp15@60809 ` 1608` ``` have "(f has_field_derivative (f' (g x))) (at (g x) within g ` {a..b})" ``` lp15@60809 ` 1609` ``` using assms by (metis a atLeastAtMost_iff b DERIV_subset image_subset_iff less_eq_real_def) ``` nipkow@69064 ` 1610` ``` then have fdiff: "(f has_derivative (*) (f' (g x))) (at (g x) within g ` {a..b})" ``` lp15@60809 ` 1611` ``` by (simp add: has_field_derivative_def) ``` lp15@60809 ` 1612` ``` have "((\x. f (g x)) has_vector_derivative f' (g x) * vector_derivative g (at x within {a..b})) (at x within {a..b})" ``` lp15@60809 ` 1613` ``` using diff_chain_within [OF gdiff fdiff] ``` lp15@60809 ` 1614` ``` by (simp add: has_vector_derivative_def scaleR_conv_of_real o_def mult_ac) ``` lp15@60809 ` 1615` ``` } note * = this ``` lp15@60809 ` 1616` ``` show ?thesis ``` lp15@60809 ` 1617` ``` apply (rule fundamental_theorem_of_calculus_interior_strong) ``` lp15@60809 ` 1618` ``` using k assms cfg * ``` lp15@66793 ` 1619` ``` apply (auto simp: at_within_Icc_at) ``` lp15@60809 ` 1620` ``` done ``` lp15@60809 ` 1621` ```qed ``` lp15@60809 ` 1622` lp15@61738 ` 1623` ```lemma contour_integral_primitive: ``` lp15@60809 ` 1624` ``` assumes "\x. x \ s \ (f has_field_derivative f' x) (at x within s)" ``` lp15@60809 ` 1625` ``` and "valid_path g" "path_image g \ s" ``` lp15@61738 ` 1626` ``` shows "(f' has_contour_integral (f(pathfinish g) - f(pathstart g))) g" ``` lp15@60809 ` 1627` ``` using assms ``` lp15@61738 ` 1628` ``` apply (simp add: valid_path_def path_image_def pathfinish_def pathstart_def has_contour_integral_def) ``` lp15@61738 ` 1629` ``` apply (auto intro!: piecewise_C1_imp_differentiable contour_integral_primitive_lemma [of 0 1 s]) ``` lp15@60809 ` 1630` ``` done ``` lp15@60809 ` 1631` lp15@60809 ` 1632` ```corollary Cauchy_theorem_primitive: ``` lp15@60809 ` 1633` ``` assumes "\x. x \ s \ (f has_field_derivative f' x) (at x within s)" ``` lp15@60809 ` 1634` ``` and "valid_path g" "path_image g \ s" "pathfinish g = pathstart g" ``` lp15@61738 ` 1635` ``` shows "(f' has_contour_integral 0) g" ``` lp15@60809 ` 1636` ``` using assms ``` lp15@61738 ` 1637` ``` by (metis diff_self contour_integral_primitive) ``` lp15@60809 ` 1638` lp15@60809 ` 1639` ```text\Existence of path integral for continuous function\ ``` lp15@61738 ` 1640` ```lemma contour_integrable_continuous_linepath: ``` lp15@60809 ` 1641` ``` assumes "continuous_on (closed_segment a b) f" ``` lp15@61738 ` 1642` ``` shows "f contour_integrable_on (linepath a b)" ``` lp15@60809 ` 1643` ```proof - ``` lp15@68339 ` 1644` ``` have "continuous_on {0..1} ((\x. f x * (b - a)) \ linepath a b)" ``` lp15@60809 ` 1645` ``` apply (rule continuous_on_compose [OF continuous_on_linepath], simp add: linepath_image_01) ``` lp15@60809 ` 1646` ``` apply (rule continuous_intros | simp add: assms)+ ``` lp15@60809 ` 1647` ``` done ``` lp15@60809 ` 1648` ``` then show ?thesis ``` lp15@61738 ` 1649` ``` apply (simp add: contour_integrable_on_def has_contour_integral_def integrable_on_def [symmetric]) ``` lp15@60809 ` 1650` ``` apply (rule integrable_continuous [of 0 "1::real", simplified]) ``` lp15@60809 ` 1651` ``` apply (rule continuous_on_eq [where f = "\x. f(linepath a b x)*(b - a)"]) ``` lp15@60809 ` 1652` ``` apply (auto simp: vector_derivative_linepath_within) ``` lp15@60809 ` 1653` ``` done ``` lp15@60809 ` 1654` ```qed ``` lp15@60809 ` 1655` lp15@60809 ` 1656` ```lemma has_field_der_id: "((\x. x\<^sup>2 / 2) has_field_derivative x) (at x)" ``` lp15@60809 ` 1657` ``` by (rule has_derivative_imp_has_field_derivative) ``` lp15@60809 ` 1658` ``` (rule derivative_intros | simp)+ ``` lp15@60809 ` 1659` lp15@61738 ` 1660` ```lemma contour_integral_id [simp]: "contour_integral (linepath a b) (\y. y) = (b^2 - a^2)/2" ``` lp15@61738 ` 1661` ``` apply (rule contour_integral_unique) ``` lp15@61738 ` 1662` ``` using contour_integral_primitive [of UNIV "\x. x^2/2" "\x. x" "linepath a b"] ``` lp15@60809 ` 1663` ``` apply (auto simp: field_simps has_field_der_id) ``` lp15@60809 ` 1664` ``` done ``` lp15@60809 ` 1665` lp15@61738 ` 1666` ```lemma contour_integrable_on_const [iff]: "(\x. c) contour_integrable_on (linepath a b)" ``` lp15@61738 ` 1667` ``` by (simp add: continuous_on_const contour_integrable_continuous_linepath) ``` lp15@61738 ` 1668` lp15@61738 ` 1669` ```lemma contour_integrable_on_id [iff]: "(\x. x) contour_integrable_on (linepath a b)" ``` lp15@61738 ` 1670` ``` by (simp add: continuous_on_id contour_integrable_continuous_linepath) ``` lp15@60809 ` 1671` wl302@69423 ` 1672` ```subsection%unimportant \Arithmetical combining theorems\ ``` lp15@60809 ` 1673` lp15@61738 ` 1674` ```lemma has_contour_integral_neg: ``` lp15@61738 ` 1675` ``` "(f has_contour_integral i) g \ ((\x. -(f x)) has_contour_integral (-i)) g" ``` lp15@61738 ` 1676` ``` by (simp add: has_integral_neg has_contour_integral_def) ``` lp15@61738 ` 1677` lp15@61738 ` 1678` ```lemma has_contour_integral_add: ``` lp15@61738 ` 1679` ``` "\(f1 has_contour_integral i1) g; (f2 has_contour_integral i2) g\ ``` lp15@61738 ` 1680` ``` \ ((\x. f1 x + f2 x) has_contour_integral (i1 + i2)) g" ``` lp15@61738 ` 1681` ``` by (simp add: has_integral_add has_contour_integral_def algebra_simps) ``` lp15@61738 ` 1682` lp15@61738 ` 1683` ```lemma has_contour_integral_diff: ``` lp15@61738 ` 1684` ``` "\(f1 has_contour_integral i1) g; (f2 has_contour_integral i2) g\ ``` lp15@61738 ` 1685` ``` \ ((\x. f1 x - f2 x) has_contour_integral (i1 - i2)) g" ``` lp15@66112 ` 1686` ``` by (simp add: has_integral_diff has_contour_integral_def algebra_simps) ``` lp15@61738 ` 1687` lp15@61738 ` 1688` ```lemma has_contour_integral_lmul: ``` lp15@61738 ` 1689` ``` "(f has_contour_integral i) g \ ((\x. c * (f x)) has_contour_integral (c*i)) g" ``` lp15@61738 ` 1690` ```apply (simp add: has_contour_integral_def) ``` lp15@60809 ` 1691` ```apply (drule has_integral_mult_right) ``` lp15@60809 ` 1692` ```apply (simp add: algebra_simps) ``` lp15@60809 ` 1693` ```done ``` lp15@60809 ` 1694` lp15@61738 ` 1695` ```lemma has_contour_integral_rmul: ``` lp15@61738 ` 1696` ``` "(f has_contour_integral i) g \ ((\x. (f x) * c) has_contour_integral (i*c)) g" ``` lp15@61738 ` 1697` ```apply (drule has_contour_integral_lmul) ``` lp15@60809 ` 1698` ```apply (simp add: mult.commute) ``` lp15@60809 ` 1699` ```done ``` lp15@60809 ` 1700` lp15@61738 ` 1701` ```lemma has_contour_integral_div: ``` lp15@61738 ` 1702` ``` "(f has_contour_integral i) g \ ((\x. f x/c) has_contour_integral (i/c)) g" ``` lp15@61738 ` 1703` ``` by (simp add: field_class.field_divide_inverse) (metis has_contour_integral_rmul) ``` lp15@61738 ` 1704` lp15@61738 ` 1705` ```lemma has_contour_integral_eq: ``` lp15@61738 ` 1706` ``` "\(f has_contour_integral y) p; \x. x \ path_image p \ f x = g x\ \ (g has_contour_integral y) p" ``` lp15@61738 ` 1707` ```apply (simp add: path_image_def has_contour_integral_def) ``` lp15@60809 ` 1708` ```by (metis (no_types, lifting) image_eqI has_integral_eq) ``` lp15@60809 ` 1709` lp15@61738 ` 1710` ```lemma has_contour_integral_bound_linepath: ``` lp15@61738 ` 1711` ``` assumes "(f has_contour_integral i) (linepath a b)" ``` lp15@60809 ` 1712` ``` "0 \ B" "\x. x \ closed_segment a b \ norm(f x) \ B" ``` lp15@60809 ` 1713` ``` shows "norm i \ B * norm(b - a)" ``` lp15@60809 ` 1714` ```proof - ``` lp15@60809 ` 1715` ``` { fix x::real ``` lp15@60809 ` 1716` ``` assume x: "0 \ x" "x \ 1" ``` lp15@60809 ` 1717` ``` have "norm (f (linepath a b x)) * ``` lp15@60809 ` 1718` ``` norm (vector_derivative (linepath a b) (at x within {0..1})) \ B * norm (b - a)" ``` lp15@60809 ` 1719` ``` by (auto intro: mult_mono simp: assms linepath_in_path of_real_linepath vector_derivative_linepath_within x) ``` lp15@60809 ` 1720` ``` } note * = this ``` lp15@60809 ` 1721` ``` have "norm i \ (B * norm (b - a)) * content (cbox 0 (1::real))" ``` lp15@60809 ` 1722` ``` apply (rule has_integral_bound ``` lp15@60809 ` 1723` ``` [of _ "\x. f (linepath a b x) * vector_derivative (linepath a b) (at x within {0..1})"]) ``` lp15@61738 ` 1724` ``` using assms * unfolding has_contour_integral_def ``` lp15@60809 ` 1725` ``` apply (auto simp: norm_mult) ``` lp15@60809 ` 1726` ``` done ``` lp15@60809 ` 1727` ``` then show ?thesis ``` lp15@60809 ` 1728` ``` by (auto simp: content_real) ``` lp15@60809 ` 1729` ```qed ``` lp15@60809 ` 1730` lp15@60809 ` 1731` ```(*UNUSED ``` lp15@61738 ` 1732` ```lemma has_contour_integral_bound_linepath_strong: ``` lp15@60809 ` 1733` ``` fixes a :: real and f :: "complex \ real" ``` lp15@61738 ` 1734` ``` assumes "(f has_contour_integral i) (linepath a b)" ``` lp15@60809 ` 1735` ``` "finite k" ``` lp15@60809 ` 1736` ``` "0 \ B" "\x::real. x \ closed_segment a b - k \ norm(f x) \ B" ``` lp15@60809 ` 1737` ``` shows "norm i \ B*norm(b - a)" ``` lp15@60809 ` 1738` ```*) ``` lp15@60809 ` 1739` lp15@61738 ` 1740` ```lemma has_contour_integral_const_linepath: "((\x. c) has_contour_integral c*(b - a))(linepath a b)" ``` lp15@61738 ` 1741` ``` unfolding has_contour_integral_linepath ``` lp15@60809 ` 1742` ``` by (metis content_real diff_0_right has_integral_const_real lambda_one of_real_1 scaleR_conv_of_real zero_le_one) ``` lp15@60809 ` 1743` lp15@61738 ` 1744` ```lemma has_contour_integral_0: "((\x. 0) has_contour_integral 0) g" ``` lp15@61738 ` 1745` ``` by (simp add: has_contour_integral_def) ``` lp15@61738 ` 1746` lp15@61738 ` 1747` ```lemma has_contour_integral_is_0: ``` lp15@61738 ` 1748` ``` "(\z. z \ path_image g \ f z = 0) \ (f has_contour_integral 0) g" ``` lp15@61738 ` 1749` ``` by (rule has_contour_integral_eq [OF has_contour_integral_0]) auto ``` lp15@61738 ` 1750` nipkow@64267 ` 1751` ```lemma has_contour_integral_sum: ``` lp15@61738 ` 1752` ``` "\finite s; \a. a \ s \ (f a has_contour_integral i a) p\ ``` nipkow@64267 ` 1753` ``` \ ((\x. sum (\a. f a x) s) has_contour_integral sum i s) p" ``` lp15@61738 ` 1754` ``` by (induction s rule: finite_induct) (auto simp: has_contour_integral_0 has_contour_integral_add) ``` lp15@60809 ` 1755` wl302@69423 ` 1756` ```subsection%unimportant \Operations on path integrals\ ``` lp15@60809 ` 1757` lp15@61738 ` 1758` ```lemma contour_integral_const_linepath [simp]: "contour_integral (linepath a b) (\x. c) = c*(b - a)" ``` lp15@61738 ` 1759` ``` by (rule contour_integral_unique [OF has_contour_integral_const_linepath]) ``` lp15@61738 ` 1760` lp15@61738 ` 1761` ```lemma contour_integral_neg: ``` lp15@61738 ` 1762` ``` "f contour_integrable_on g \ contour_integral g (\x. -(f x)) = -(contour_integral g f)" ``` lp15@61738 ` 1763` ``` by (simp add: contour_integral_unique has_contour_integral_integral has_contour_integral_neg) ``` lp15@61738 ` 1764` lp15@61738 ` 1765` ```lemma contour_integral_add: ``` lp15@61738 ` 1766` ``` "f1 contour_integrable_on g \ f2 contour_integrable_on g \ contour_integral g (\x. f1 x + f2 x) = ``` lp15@61738 ` 1767` ``` contour_integral g f1 + contour_integral g f2" ``` lp15@61738 ` 1768` ``` by (simp add: contour_integral_unique has_contour_integral_integral has_contour_integral_add) ``` lp15@61738 ` 1769` lp15@61738 ` 1770` ```lemma contour_integral_diff: ``` lp15@61738 ` 1771` ``` "f1 contour_integrable_on g \ f2 contour_integrable_on g \ contour_integral g (\x. f1 x - f2 x) = ``` lp15@61738 ` 1772` ``` contour_integral g f1 - contour_integral g f2" ``` lp15@61738 ` 1773` ``` by (simp add: contour_integral_unique has_contour_integral_integral has_contour_integral_diff) ``` lp15@61738 ` 1774` lp15@61738 ` 1775` ```lemma contour_integral_lmul: ``` lp15@61738 ` 1776` ``` shows "f contour_integrable_on g ``` lp15@61738 ` 1777` ``` \ contour_integral g (\x. c * f x) = c*contour_integral g f" ``` lp15@61738 ` 1778` ``` by (simp add: contour_integral_unique has_contour_integral_integral has_contour_integral_lmul) ``` lp15@61738 ` 1779` lp15@61738 ` 1780` ```lemma contour_integral_rmul: ``` lp15@61738 ` 1781` ``` shows "f contour_integrable_on g ``` lp15@61738 ` 1782` ``` \ contour_integral g (\x. f x * c) = contour_integral g f * c" ``` lp15@61738 ` 1783` ``` by (simp add: contour_integral_unique has_contour_integral_integral has_contour_integral_rmul) ``` lp15@61738 ` 1784` lp15@61738 ` 1785` ```lemma contour_integral_div: ``` lp15@61738 ` 1786` ``` shows "f contour_integrable_on g ``` lp15@61738 ` 1787` ``` \ contour_integral g (\x. f x / c) = contour_integral g f / c" ``` lp15@61738 ` 1788` ``` by (simp add: contour_integral_unique has_contour_integral_integral has_contour_integral_div) ``` lp15@61738 ` 1789` lp15@61738 ` 1790` ```lemma contour_integral_eq: ``` lp15@61738 ` 1791` ``` "(\x. x \ path_image p \ f x = g x) \ contour_integral p f = contour_integral p g" ``` lp15@62463 ` 1792` ``` apply (simp add: contour_integral_def) ``` lp15@62463 ` 1793` ``` using has_contour_integral_eq ``` lp15@62463 ` 1794` ``` by (metis contour_integral_unique has_contour_integral_integrable has_contour_integral_integral) ``` lp15@61738 ` 1795` lp15@61738 ` 1796` ```lemma contour_integral_eq_0: ``` lp15@61738 ` 1797` ``` "(\z. z \ path_image g \ f z = 0) \ contour_integral g f = 0" ``` lp15@61738 ` 1798` ``` by (simp add: has_contour_integral_is_0 contour_integral_unique) ``` lp15@61738 ` 1799` lp15@61738 ` 1800` ```lemma contour_integral_bound_linepath: ``` lp15@60809 ` 1801` ``` shows ``` lp15@61738 ` 1802` ``` "\f contour_integrable_on (linepath a b); ``` lp15@60809 ` 1803` ``` 0 \ B; \x. x \ closed_segment a b \ norm(f x) \ B\ ``` lp15@61738 ` 1804` ``` \ norm(contour_integral (linepath a b) f) \ B*norm(b - a)" ``` lp15@61738 ` 1805` ``` apply (rule has_contour_integral_bound_linepath [of f]) ``` lp15@61738 ` 1806` ``` apply (auto simp: has_contour_integral_integral) ``` lp15@60809 ` 1807` ``` done ``` lp15@60809 ` 1808` lp15@61806 ` 1809` ```lemma contour_integral_0 [simp]: "contour_integral g (\x. 0) = 0" ``` lp15@61738 ` 1810` ``` by (simp add: contour_integral_unique has_contour_integral_0) ``` lp15@61738 ` 1811` nipkow@64267 ` 1812` ```lemma contour_integral_sum: ``` lp15@61738 ` 1813` ``` "\finite s; \a. a \ s \ (f a) contour_integrable_on p\ ``` nipkow@64267 ` 1814` ``` \ contour_integral p (\x. sum (\a. f a x) s) = sum (\a. contour_integral p (f a)) s" ``` nipkow@64267 ` 1815` ``` by (auto simp: contour_integral_unique has_contour_integral_sum has_contour_integral_integral) ``` lp15@61738 ` 1816` lp15@61738 ` 1817` ```lemma contour_integrable_eq: ``` lp15@61738 ` 1818` ``` "\f contour_integrable_on p; \x. x \ path_image p \ f x = g x\ \ g contour_integrable_on p" ``` lp15@61738 ` 1819` ``` unfolding contour_integrable_on_def ``` lp15@61738 ` 1820` ``` by (metis has_contour_integral_eq) ``` lp15@60809 ` 1821` lp15@60809 ` 1822` wl302@69423 ` 1823` ```subsection%unimportant \Arithmetic theorems for path integrability\ ``` lp15@60809 ` 1824` lp15@61738 ` 1825` ```lemma contour_integrable_neg: ``` lp15@61738 ` 1826` ``` "f contour_integrable_on g \ (\x. -(f x)) contour_integrable_on g" ``` lp15@61738 ` 1827` ``` using has_contour_integral_neg contour_integrable_on_def by blast ``` lp15@61738 ` 1828` lp15@61738 ` 1829` ```lemma contour_integrable_add: ``` lp15@61738 ` 1830` ``` "\f1 contour_integrable_on g; f2 contour_integrable_on g\ \ (\x. f1 x + f2 x) contour_integrable_on g" ``` lp15@61738 ` 1831` ``` using has_contour_integral_add contour_integrable_on_def ``` lp15@60809 ` 1832` ``` by fastforce ``` lp15@60809 ` 1833` lp15@61738 ` 1834` ```lemma contour_integrable_diff: ``` lp15@61738 ` 1835` ``` "\f1 contour_integrable_on g; f2 contour_integrable_on g\ \ (\x. f1 x - f2 x) contour_integrable_on g" ``` lp15@61738 ` 1836` ``` using has_contour_integral_diff contour_integrable_on_def ``` lp15@60809 ` 1837` ``` by fastforce ``` lp15@60809 ` 1838` lp15@61738 ` 1839` ```lemma contour_integrable_lmul: ``` lp15@61738 ` 1840` ``` "f contour_integrable_on g \ (\x. c * f x) contour_integrable_on g" ``` lp15@61738 ` 1841` ``` using has_contour_integral_lmul contour_integrable_on_def ``` lp15@60809 ` 1842` ``` by fastforce ``` lp15@60809 ` 1843` lp15@61738 ` 1844` ```lemma contour_integrable_rmul: ``` lp15@61738 ` 1845` ``` "f contour_integrable_on g \ (\x. f x * c) contour_integrable_on g" ``` lp15@61738 ` 1846` ``` using has_contour_integral_rmul contour_integrable_on_def ``` lp15@60809 ` 1847` ``` by fastforce ``` lp15@60809 ` 1848` lp15@61738 ` 1849` ```lemma contour_integrable_div: ``` lp15@61738 ` 1850` ``` "f contour_integrable_on g \ (\x. f x / c) contour_integrable_on g" ``` lp15@61738 ` 1851` ``` using has_contour_integral_div contour_integrable_on_def ``` lp15@60809 ` 1852` ``` by fastforce ``` lp15@60809 ` 1853` nipkow@64267 ` 1854` ```lemma contour_integrable_sum: ``` lp15@61738 ` 1855` ``` "\finite s; \a. a \ s \ (f a) contour_integrable_on p\ ``` nipkow@64267 ` 1856` ``` \ (\x. sum (\a. f a x) s) contour_integrable_on p" ``` lp15@61738 ` 1857` ``` unfolding contour_integrable_on_def ``` nipkow@64267 ` 1858` ``` by (metis has_contour_integral_sum) ``` lp15@60809 ` 1859` lp15@60809 ` 1860` wl302@69423 ` 1861` ```subsection%unimportant \Reversing a path integral\ ``` lp15@60809 ` 1862` lp15@61738 ` 1863` ```lemma has_contour_integral_reverse_linepath: ``` lp15@61738 ` 1864` ``` "(f has_contour_integral i) (linepath a b) ``` lp15@61738 ` 1865` ``` \ (f has_contour_integral (-i)) (linepath b a)" ``` lp15@61738 ` 1866` ``` using has_contour_integral_reversepath valid_path_linepath by fastforce ``` lp15@61738 ` 1867` lp15@61738 ` 1868` ```lemma contour_integral_reverse_linepath: ``` lp15@60809 ` 1869` ``` "continuous_on (closed_segment a b) f ``` lp15@61738 ` 1870` ``` \ contour_integral (linepath a b) f = - (contour_integral(linepath b a) f)" ``` lp15@61738 ` 1871` ```apply (rule contour_integral_unique) ``` lp15@61738 ` 1872` ```apply (rule has_contour_integral_reverse_linepath) ``` lp15@61738 ` 1873` ```by (simp add: closed_segment_commute contour_integrable_continuous_linepath has_contour_integral_integral) ``` lp15@60809 ` 1874` lp15@60809 ` 1875` lp15@60809 ` 1876` ```(* Splitting a path integral in a flat way.*) ``` lp15@60809 ` 1877` lp15@61738 ` 1878` ```lemma has_contour_integral_split: ``` lp15@61738 ` 1879` ``` assumes f: "(f has_contour_integral i) (linepath a c)" "(f has_contour_integral j) (linepath c b)" ``` lp15@60809 ` 1880` ``` and k: "0 \ k" "k \ 1" ``` lp15@60809 ` 1881` ``` and c: "c - a = k *\<^sub>R (b - a)" ``` lp15@61738 ` 1882` ``` shows "(f has_contour_integral (i + j)) (linepath a b)" ``` lp15@60809 ` 1883` ```proof (cases "k = 0 \ k = 1") ``` lp15@60809 ` 1884` ``` case True ``` lp15@60809 ` 1885` ``` then show ?thesis ``` lp15@68296 ` 1886` ``` using assms by auto ``` lp15@60809 ` 1887` ```next ``` lp15@60809 ` 1888` ``` case False ``` lp15@60809 ` 1889` ``` then have k: "0 < k" "k < 1" "complex_of_real k \ 1" ``` lp15@65578 ` 1890` ``` using assms by auto ``` lp15@60809 ` 1891` ``` have c': "c = k *\<^sub>R (b - a) + a" ``` lp15@60809 ` 1892` ``` by (metis diff_add_cancel c) ``` lp15@60809 ` 1893` ``` have bc: "(b - c) = (1 - k) *\<^sub>R (b - a)" ``` lp15@60809 ` 1894` ``` by (simp add: algebra_simps c') ``` lp15@60809 ` 1895` ``` { assume *: "((\x. f ((1 - x) *\<^sub>R a + x *\<^sub>R c) * (c - a)) has_integral i) {0..1}" ``` lp15@60809 ` 1896` ``` have **: "\x. ((k - x) / k) *\<^sub>R a + (x / k) *\<^sub>R c = (1 - x) *\<^sub>R a + x *\<^sub>R b" ``` lp15@68302 ` 1897` ``` using False apply (simp add: c' algebra_simps) ``` lp15@60809 ` 1898` ``` apply (simp add: real_vector.scale_left_distrib [symmetric] divide_simps) ``` lp15@60809 ` 1899` ``` done ``` lp15@60809 ` 1900` ``` have "((\x. f ((1 - x) *\<^sub>R a + x *\<^sub>R b) * (b - a)) has_integral i) {0..k}" ``` lp15@68296 ` 1901` ``` using k has_integral_affinity01 [OF *, of "inverse k" "0"] ``` lp15@68296 ` 1902` ``` apply (simp add: divide_simps mult.commute [of _ "k"] image_affinity_atLeastAtMost ** c) ``` lp15@68296 ` 1903` ``` apply (auto dest: has_integral_cmul [where c = "inverse k"]) ``` lp15@60809 ` 1904` ``` done ``` lp15@60809 ` 1905` ``` } note fi = this ``` lp15@60809 ` 1906` ``` { assume *: "((\x. f ((1 - x) *\<^sub>R c + x *\<^sub>R b) * (b - c)) has_integral j) {0..1}" ``` lp15@60809 ` 1907` ``` have **: "\x. (((1 - x) / (1 - k)) *\<^sub>R c + ((x - k) / (1 - k)) *\<^sub>R b) = ((1 - x) *\<^sub>R a + x *\<^sub>R b)" ``` lp15@60809 ` 1908` ``` using k ``` lp15@60809 ` 1909` ``` apply (simp add: c' field_simps) ``` lp15@60809 ` 1910` ``` apply (simp add: scaleR_conv_of_real divide_simps) ``` lp15@60809 ` 1911` ``` apply (simp add: field_simps) ``` lp15@60809 ` 1912` ``` done ``` lp15@60809 ` 1913` ``` have "((\x. f ((1 - x) *\<^sub>R a + x *\<^sub>R b) * (b - a)) has_integral j) {k..1}" ``` lp15@68296 ` 1914` ``` using k has_integral_affinity01 [OF *, of "inverse(1 - k)" "-(k/(1 - k))"] ``` lp15@68296 ` 1915` ``` apply (simp add: divide_simps mult.commute [of _ "1-k"] image_affinity_atLeastAtMost ** bc) ``` lp15@68296 ` 1916` ``` apply (auto dest: has_integral_cmul [where k = "(1 - k) *\<^sub>R j" and c = "inverse (1 - k)"]) ``` lp15@60809 ` 1917` ``` done ``` lp15@60809 ` 1918` ``` } note fj = this ``` lp15@60809 ` 1919` ``` show ?thesis ``` lp15@60809 ` 1920` ``` using f k ``` lp15@61738 ` 1921` ``` apply (simp add: has_contour_integral_linepath) ``` lp15@60809 ` 1922` ``` apply (simp add: linepath_def) ``` lp15@60809 ` 1923` ``` apply (rule has_integral_combine [OF _ _ fi fj], simp_all) ``` lp15@60809 ` 1924` ``` done ``` lp15@60809 ` 1925` ```qed ``` lp15@60809 ` 1926` lp15@60809 ` 1927` ```lemma continuous_on_closed_segment_transform: ``` lp15@60809 ` 1928` ``` assumes f: "continuous_on (closed_segment a b) f" ``` lp15@60809 ` 1929` ``` and k: "0 \ k" "k \ 1" ``` lp15@60809 ` 1930` ``` and c: "c - a = k *\<^sub>R (b - a)" ``` lp15@60809 ` 1931` ``` shows "continuous_on (closed_segment a c) f" ``` lp15@60809 ` 1932` ```proof - ``` lp15@60809 ` 1933` ``` have c': "c = (1 - k) *\<^sub>R a + k *\<^sub>R b" ``` lp15@60809 ` 1934` ``` using c by (simp add: algebra_simps) ``` lp15@68302 ` 1935` ``` have "closed_segment a c \ closed_segment a b" ``` lp15@68302 ` 1936` ``` by (metis c' ends_in_segment(1) in_segment(1) k subset_closed_segment) ``` lp15@68302 ` 1937` ``` then show "continuous_on (closed_segment a c) f" ``` lp15@68302 ` 1938` ``` by (rule continuous_on_subset [OF f]) ``` lp15@60809 ` 1939` ```qed ``` lp15@60809 ` 1940` lp15@61738 ` 1941` ```lemma contour_integral_split: ``` lp15@60809 ` 1942` ``` assumes f: "continuous_on (closed_segment a b) f" ``` lp15@60809 ` 1943` ``` and k: "0 \ k" "k \ 1" ``` lp15@60809 ` 1944` ``` and c: "c - a = k *\<^sub>R (b - a)" ``` lp15@61738 ` 1945` ``` shows "contour_integral(linepath a b) f = contour_integral(linepath a c) f + contour_integral(linepath c b) f" ``` lp15@60809 ` 1946` ```proof - ``` lp15@60809 ` 1947` ``` have c': "c = (1 - k) *\<^sub>R a + k *\<^sub>R b" ``` lp15@60809 ` 1948` ``` using c by (simp add: algebra_simps) ``` lp15@68302 ` 1949` ``` have "closed_segment a c \ closed_segment a b" ``` lp15@68302 ` 1950` ``` by (metis c' ends_in_segment(1) in_segment(1) k subset_closed_segment) ``` lp15@68302 ` 1951` ``` moreover have "closed_segment c b \ closed_segment a b" ``` lp15@68302 ` 1952` ``` by (metis c' ends_in_segment(2) in_segment(1) k subset_closed_segment) ``` lp15@68302 ` 1953` ``` ultimately ``` lp15@60809 ` 1954` ``` have *: "continuous_on (closed_segment a c) f" "continuous_on (closed_segment c b) f" ``` lp15@68302 ` 1955` ``` by (auto intro: continuous_on_subset [OF f]) ``` lp15@60809 ` 1956` ``` show ?thesis ``` lp15@68302 ` 1957` ``` by (rule contour_integral_unique) (meson "*" c contour_integrable_continuous_linepath has_contour_integral_integral has_contour_integral_split k) ``` lp15@60809 ` 1958` ```qed ``` lp15@60809 ` 1959` lp15@61738 ` 1960` ```lemma contour_integral_split_linepath: ``` lp15@60809 ` 1961` ``` assumes f: "continuous_on (closed_segment a b) f" ``` lp15@60809 ` 1962` ``` and c: "c \ closed_segment a b" ``` lp15@61738 ` 1963` ``` shows "contour_integral(linepath a b) f = contour_integral(linepath a c) f + contour_integral(linepath c b) f" ``` lp15@68302 ` 1964` ``` using c by (auto simp: closed_segment_def algebra_simps intro!: contour_integral_split [OF f]) ``` lp15@60809 ` 1965` lp15@68296 ` 1966` ```text\The special case of midpoints used in the main quadrisection\ ``` lp15@60809 ` 1967` lp15@61738 ` 1968` ```lemma has_contour_integral_midpoint: ``` lp15@61738 ` 1969` ``` assumes "(f has_contour_integral i) (linepath a (midpoint a b))" ``` lp15@61738 ` 1970` ``` "(f has_contour_integral j) (linepath (midpoint a b) b)" ``` lp15@61738 ` 1971` ``` shows "(f has_contour_integral (i + j)) (linepath a b)" ``` lp15@61738 ` 1972` ``` apply (rule has_contour_integral_split [where c = "midpoint a b" and k = "1/2"]) ``` lp15@60809 ` 1973` ``` using assms ``` lp15@60809 ` 1974` ``` apply (auto simp: midpoint_def algebra_simps scaleR_conv_of_real) ``` lp15@60809 ` 1975` ``` done ``` lp15@60809 ` 1976` lp15@61738 ` 1977` ```lemma contour_integral_midpoint: ``` lp15@60809 ` 1978` ``` "continuous_on (closed_segment a b) f ``` lp15@61738 ` 1979` ``` \ contour_integral (linepath a b) f = ``` lp15@61738 ` 1980` ``` contour_integral (linepath a (midpoint a b)) f + contour_integral (linepath (midpoint a b) b) f" ``` lp15@61738 ` 1981` ``` apply (rule contour_integral_split [where c = "midpoint a b" and k = "1/2"]) ``` lp15@60809 ` 1982` ``` apply (auto simp: midpoint_def algebra_simps scaleR_conv_of_real) ``` lp15@60809 ` 1983` ``` done ``` lp15@60809 ` 1984` lp15@60809 ` 1985` lp15@60809 ` 1986` ```text\A couple of special case lemmas that are useful below\ ``` lp15@60809 ` 1987` lp15@60809 ` 1988` ```lemma triangle_linear_has_chain_integral: ``` lp15@61738 ` 1989` ``` "((\x. m*x + d) has_contour_integral 0) (linepath a b +++ linepath b c +++ linepath c a)" ``` lp15@60809 ` 1990` ``` apply (rule Cauchy_theorem_primitive [of UNIV "\x. m/2 * x^2 + d*x"]) ``` lp15@60809 ` 1991` ``` apply (auto intro!: derivative_eq_intros) ``` lp15@60809 ` 1992` ``` done ``` lp15@60809 ` 1993` lp15@60809 ` 1994` ```lemma has_chain_integral_chain_integral3: ``` lp15@61738 ` 1995` ``` "(f has_contour_integral i) (linepath a b +++ linepath b c +++ linepath c d) ``` lp15@61738 ` 1996` ``` \ contour_integral (linepath a b) f + contour_integral (linepath b c) f + contour_integral (linepath c d) f = i" ``` lp15@61738 ` 1997` ``` apply (subst contour_integral_unique [symmetric], assumption) ``` lp15@61738 ` 1998` ``` apply (drule has_contour_integral_integrable) ``` lp15@60809 ` 1999` ``` apply (simp add: valid_path_join) ``` lp15@60809 ` 2000` ``` done ``` lp15@60809 ` 2001` lp15@62397 ` 2002` ```lemma has_chain_integral_chain_integral4: ``` lp15@62397 ` 2003` ``` "(f has_contour_integral i) (linepath a b +++ linepath b c +++ linepath c d +++ linepath d e) ``` lp15@62397 ` 2004` ``` \ contour_integral (linepath a b) f + contour_integral (linepath b c) f + contour_integral (linepath c d) f + contour_integral (linepath d e) f = i" ``` lp15@62397 ` 2005` ``` apply (subst contour_integral_unique [symmetric], assumption) ``` lp15@62397 ` 2006` ``` apply (drule has_contour_integral_integrable) ``` lp15@62397 ` 2007` ``` apply (simp add: valid_path_join) ``` lp15@62397 ` 2008` ``` done ``` lp15@62397 ` 2009` lp15@60809 ` 2010` ```subsection\Reversing the order in a double path integral\ ``` lp15@60809 ` 2011` lp15@60809 ` 2012` ```text\The condition is stronger than needed but it's often true in typical situations\ ``` lp15@60809 ` 2013` lp15@60809 ` 2014` ```lemma fst_im_cbox [simp]: "cbox c d \ {} \ (fst ` cbox (a,c) (b,d)) = cbox a b" ``` lp15@60809 ` 2015` ``` by (auto simp: cbox_Pair_eq) ``` lp15@60809 ` 2016` lp15@60809 ` 2017` ```lemma snd_im_cbox [simp]: "cbox a b \ {} \ (snd ` cbox (a,c) (b,d)) = cbox c d" ``` lp15@60809 ` 2018` ``` by (auto simp: cbox_Pair_eq) ``` lp15@60809 ` 2019` wl302@69423 ` 2020` ```proposition contour_integral_swap: ``` lp15@60809 ` 2021` ``` assumes fcon: "continuous_on (path_image g \ path_image h) (\(y1,y2). f y1 y2)" ``` lp15@60809 ` 2022` ``` and vp: "valid_path g" "valid_path h" ``` lp15@60809 ` 2023` ``` and gvcon: "continuous_on {0..1} (\t. vector_derivative g (at t))" ``` lp15@60809 ` 2024` ``` and hvcon: "continuous_on {0..1} (\t. vector_derivative h (at t))" ``` lp15@61738 ` 2025` ``` shows "contour_integral g (\w. contour_integral h (f w)) = ``` lp15@61738 ` 2026` ``` contour_integral h (\z. contour_integral g (\w. f w z))" ``` lp15@60809 ` 2027` ```proof - ``` lp15@60809 ` 2028` ``` have gcon: "continuous_on {0..1} g" and hcon: "continuous_on {0..1} h" ``` lp15@61190 ` 2029` ``` using assms by (auto simp: valid_path_def piecewise_C1_differentiable_on_def) ``` lp15@68339 ` 2030` ``` have fgh1: "\x. (\t. f (g x) (h t)) = (\(y1,y2). f y1 y2) \ (\t. (g x, h t))" ``` lp15@60809 ` 2031` ``` by (rule ext) simp ``` lp15@68339 ` 2032` ``` have fgh2: "\x. (\t. f (g t) (h x)) = (\(y1,y2). f y1 y2) \ (\t. (g t, h x))" ``` lp15@60809 ` 2033` ``` by (rule ext) simp ``` lp15@60809 ` 2034` ``` have fcon_im1: "\x. 0 \ x \ x \ 1 \ continuous_on ((\t. (g x, h t)) ` {0..1}) (\(x, y). f x y)" ``` lp15@60809 ` 2035` ``` by (rule continuous_on_subset [OF fcon]) (auto simp: path_image_def) ``` lp15@60809 ` 2036` ``` have fcon_im2: "\x. 0 \ x \ x \ 1 \ continuous_on ((\t. (g t, h x)) ` {0..1}) (\(x, y). f x y)" ``` lp15@60809 ` 2037` ``` by (rule continuous_on_subset [OF fcon]) (auto simp: path_image_def) ``` lp15@68302 ` 2038` ``` have "\y. y \ {0..1} \ continuous_on {0..1} (\x. f (g x) (h y))" ``` lp15@68302 ` 2039` ``` by (subst fgh2) (rule fcon_im2 gcon continuous_intros | simp)+ ``` lp15@68302 ` 2040` ``` then have vdg: "\y. y \ {0..1} \ (\x. f (g x) (h y) * vector_derivative g (at x)) integrable_on {0..1}" ``` lp15@68302 ` 2041` ``` using continuous_on_mult gvcon integrable_continuous_real by blast ``` lp15@68339 ` 2042` ``` have "(\z. vector_derivative g (at (fst z))) = (\x. vector_derivative g (at x)) \ fst" ``` lp15@60809 ` 2043` ``` by auto ``` lp15@60809 ` 2044` ``` then have gvcon': "continuous_on (cbox (0, 0) (1, 1::real)) (\x. vector_derivative g (at (fst x)))" ``` lp15@60809 ` 2045` ``` apply (rule ssubst) ``` lp15@60809 ` 2046` ``` apply (rule continuous_intros | simp add: gvcon)+ ``` lp15@60809 ` 2047` ``` done ``` lp15@68339 ` 2048` ``` have "(\z. vector_derivative h (at (snd z))) = (\x. vector_derivative h (at x)) \ snd" ``` lp15@60809 ` 2049` ``` by auto ``` lp15@60809 ` 2050` ``` then have hvcon': "continuous_on (cbox (0, 0) (1::real, 1)) (\x. vector_derivative h (at (snd x)))" ``` lp15@60809 ` 2051` ``` apply (rule ssubst) ``` lp15@60809 ` 2052` ``` apply (rule continuous_intros | simp add: hvcon)+ ``` lp15@60809 ` 2053` ``` done ``` lp15@68339 ` 2054` ``` have "(\x. f (g (fst x)) (h (snd x))) = (\(y1,y2). f y1 y2) \ (\w. ((g \ fst) w, (h \ snd) w))" ``` lp15@60809 ` 2055` ``` by auto ``` lp15@60809 ` 2056` ``` then have fgh: "continuous_on (cbox (0, 0) (1, 1)) (\x. f (g (fst x)) (h (snd x)))" ``` lp15@60809 ` 2057` ``` apply (rule ssubst) ``` lp15@60809 ` 2058` ``` apply (rule gcon hcon continuous_intros | simp)+ ``` lp15@60809 ` 2059` ``` apply (auto simp: path_image_def intro: continuous_on_subset [OF fcon]) ``` lp15@60809 ` 2060` ``` done ``` lp15@61738 ` 2061` ``` have "integral {0..1} (\x. contour_integral h (f (g x)) * vector_derivative g (at x)) = ``` lp15@61738 ` 2062` ``` integral {0..1} (\x. contour_integral h (\y. f (g x) y * vector_derivative g (at x)))" ``` lp15@68302 ` 2063` ``` proof (rule integral_cong [OF contour_integral_rmul [symmetric]]) ``` lp15@68302 ` 2064` ``` show "\x. x \ {0..1} \ f (g x) contour_integrable_on h" ``` lp15@68302 ` 2065` ``` unfolding contour_integrable_on ``` lp15@60809 ` 2066` ``` apply (rule integrable_continuous_real) ``` lp15@60809 ` 2067` ``` apply (rule continuous_on_mult [OF _ hvcon]) ``` lp15@60809 ` 2068` ``` apply (subst fgh1) ``` lp15@60809 ` 2069` ``` apply (rule fcon_im1 hcon continuous_intros | simp)+ ``` lp15@68302 ` 2070` ``` done ``` lp15@68302 ` 2071` ``` qed ``` lp15@68339 ` 2072` ``` also have "\ = integral {0..1} ``` lp15@61738 ` 2073` ``` (\y. contour_integral g (\x. f x (h y) * vector_derivative h (at y)))" ``` lp15@68302 ` 2074` ``` unfolding contour_integral_integral ``` lp15@60809 ` 2075` ``` apply (subst integral_swap_continuous [where 'a = real and 'b = real, of 0 0 1 1, simplified]) ``` lp15@62463 ` 2076` ``` apply (rule fgh gvcon' hvcon' continuous_intros | simp add: split_def)+ ``` lp15@62463 ` 2077` ``` unfolding integral_mult_left [symmetric] ``` lp15@62463 ` 2078` ``` apply (simp only: mult_ac) ``` lp15@60809 ` 2079` ``` done ``` lp15@68339 ` 2080` ``` also have "\ = contour_integral h (\z. contour_integral g (\w. f w z))" ``` lp15@68302 ` 2081` ``` unfolding contour_integral_integral ``` lp15@60809 ` 2082` ``` apply (rule integral_cong) ``` lp15@62463 ` 2083` ``` unfolding integral_mult_left [symmetric] ``` lp15@60809 ` 2084` ``` apply (simp add: algebra_simps) ``` lp15@60809 ` 2085` ``` done ``` lp15@60809 ` 2086` ``` finally show ?thesis ``` lp15@61738 ` 2087` ``` by (simp add: contour_integral_integral) ``` lp15@60809 ` 2088` ```qed ``` lp15@60809 ` 2089` lp15@60809 ` 2090` wl302@69423 ` 2091` ```subsection%unimportant \The key quadrisection step\ ``` lp15@60809 ` 2092` lp15@60809 ` 2093` ```lemma norm_sum_half: ``` lp15@68302 ` 2094` ``` assumes "norm(a + b) \ e" ``` lp15@68302 ` 2095` ``` shows "norm a \ e/2 \ norm b \ e/2" ``` lp15@60809 ` 2096` ```proof - ``` lp15@60809 ` 2097` ``` have "e \ norm (- a - b)" ``` lp15@60809 ` 2098` ``` by (simp add: add.commute assms norm_minus_commute) ``` lp15@60809 ` 2099` ``` thus ?thesis ``` lp15@60809 ` 2100` ``` using norm_triangle_ineq4 order_trans by fastforce ``` lp15@60809 ` 2101` ```qed ``` lp15@60809 ` 2102` lp15@60809 ` 2103` ```lemma norm_sum_lemma: ``` lp15@60809 ` 2104` ``` assumes "e \ norm (a + b + c + d)" ``` lp15@60809 ` 2105` ``` shows "e / 4 \ norm a \ e / 4 \ norm b \ e / 4 \ norm c \ e / 4 \ norm d" ``` lp15@60809 ` 2106` ```proof - ``` lp15@60809 ` 2107` ``` have "e \ norm ((a + b) + (c + d))" using assms ``` lp15@60809 ` 2108` ``` by (simp add: algebra_simps) ``` lp15@60809 ` 2109` ``` then show ?thesis ``` lp15@60809 ` 2110` ``` by (auto dest!: norm_sum_half) ``` lp15@60809 ` 2111` ```qed ``` lp15@60809 ` 2112` lp15@60809 ` 2113` ```lemma Cauchy_theorem_quadrisection: ``` lp15@60809 ` 2114` ``` assumes f: "continuous_on (convex hull {a,b,c}) f" ``` lp15@60809 ` 2115` ``` and dist: "dist a b \ K" "dist b c \ K" "dist c a \ K" ``` lp15@60809 ` 2116` ``` and e: "e * K^2 \ ``` lp15@61738 ` 2117` ``` norm (contour_integral(linepath a b) f + contour_integral(linepath b c) f + contour_integral(linepath c a) f)" ``` lp15@60809 ` 2118` ``` shows "\a' b' c'. ``` lp15@60809 ` 2119` ``` a' \ convex hull {a,b,c} \ b' \ convex hull {a,b,c} \ c' \ convex hull {a,b,c} \ ``` lp15@60809 ` 2120` ``` dist a' b' \ K/2 \ dist b' c' \ K/2 \ dist c' a' \ K/2 \ ``` lp15@61738 ` 2121` ``` e * (K/2)^2 \ norm(contour_integral(linepath a' b') f + contour_integral(linepath b' c') f + contour_integral(linepath c' a') f)" ``` lp15@68302 ` 2122` ``` (is "\x y z. ?\ x y z") ``` lp15@60809 ` 2123` ```proof - ``` lp15@60809 ` 2124` ``` note divide_le_eq_numeral1 [simp del] ``` wenzelm@63040 ` 2125` ``` define a' where "a' = midpoint b c" ``` wenzelm@63040 ` 2126` ``` define b' where "b' = midpoint c a" ``` wenzelm@63040 ` 2127` ``` define c' where "c' = midpoint a b" ``` lp15@60809 ` 2128` ``` have fabc: "continuous_on (closed_segment a b) f" "continuous_on (closed_segment b c) f" "continuous_on (closed_segment c a) f" ``` lp15@60809 ` 2129` ``` using f continuous_on_subset segments_subset_convex_hull by metis+ ``` lp15@60809 ` 2130` ``` have fcont': "continuous_on (closed_segment c' b') f" ``` lp15@60809 ` 2131` ``` "continuous_on (closed_segment a' c') f" ``` lp15@60809 ` 2132` ``` "continuous_on (closed_segment b' a') f" ``` lp15@60809 ` 2133` ``` unfolding a'_def b'_def c'_def ``` lp15@68302 ` 2134` ``` by (rule continuous_on_subset [OF f], ``` lp15@60809 ` 2135` ``` metis midpoints_in_convex_hull convex_hull_subset hull_subset insert_subset segment_convex_hull)+ ``` lp15@61738 ` 2136` ``` let ?pathint = "\x y. contour_integral(linepath x y) f" ``` lp15@60809 ` 2137` ``` have *: "?pathint a b + ?pathint b c + ?pathint c a = ``` lp15@60809 ` 2138` ``` (?pathint a c' + ?pathint c' b' + ?pathint b' a) + ``` lp15@60809 ` 2139` ``` (?pathint a' c' + ?pathint c' b + ?pathint b a') + ``` lp15@60809 ` 2140` ``` (?pathint a' c + ?pathint c b' + ?pathint b' a') + ``` lp15@60809 ` 2141` ``` (?pathint a' b' + ?pathint b' c' + ?pathint c' a')" ``` lp15@68302 ` 2142` ``` by (simp add: fcont' contour_integral_reverse_linepath) (simp add: a'_def b'_def c'_def contour_integral_midpoint fabc) ``` lp15@60809 ` 2143` ``` have [simp]: "\x y. cmod (x * 2 - y * 2) = cmod (x - y) * 2" ``` lp15@60809 ` 2144` ``` by (metis left_diff_distrib mult.commute norm_mult_numeral1) ``` lp15@60809 ` 2145` ``` have [simp]: "\x y. cmod (x - y) = cmod (y - x)" ``` lp15@60809 ` 2146` ``` by (simp add: norm_minus_commute) ``` lp15@60809 ` 2147` ``` consider "e * K\<^sup>2 / 4 \ cmod (?pathint a c' + ?pathint c' b' + ?pathint b' a)" | ``` lp15@60809 ` 2148` ``` "e * K\<^sup>2 / 4 \ cmod (?pathint a' c' + ?pathint c' b + ?pathint b a')" | ``` lp15@60809 ` 2149` ``` "e * K\<^sup>2 / 4 \ cmod (?pathint a' c + ?pathint c b' + ?pathint b' a')" | ``` lp15@60809 ` 2150` ``` "e * K\<^sup>2 / 4 \ cmod (?pathint a' b' + ?pathint b' c' + ?pathint c' a')" ``` lp15@68302 ` 2151` ``` using assms unfolding * by (blast intro: that dest!: norm_sum_lemma) ``` lp15@60809 ` 2152` ``` then show ?thesis ``` lp15@60809 ` 2153` ``` proof cases ``` lp15@68302 ` 2154` ``` case 1 then have "?\ a c' b'" ``` lp15@60809 ` 2155` ``` using assms ``` lp15@68302 ` 2156` ``` apply (clarsimp simp: c'_def b'_def midpoints_in_convex_hull hull_subset [THEN subsetD]) ``` lp15@68302 ` 2157` ``` apply (auto simp: midpoint_def dist_norm scaleR_conv_of_real divide_simps) ``` lp15@68302 ` 2158` ``` done ``` lp15@68302 ` 2159` ``` then show ?thesis by blast ``` lp15@68302 ` 2160` ``` next ``` lp15@68302 ` 2161` ``` case 2 then have "?\ a' c' b" ``` lp15@68302 ` 2162` ``` using assms ``` lp15@68302 ` 2163` ``` apply (clarsimp simp: a'_def c'_def midpoints_in_convex_hull hull_subset [THEN subsetD]) ``` lp15@60809 ` 2164` ``` apply (auto simp: midpoint_def dist_norm scaleR_conv_of_real divide_simps) ``` lp15@60809 ` 2165` ``` done ``` lp15@68302 ` 2166` ``` then show ?thesis by blast ``` lp15@60809 ` 2167` ``` next ``` lp15@68302 ` 2168` ``` case 3 then have "?\ a' c b'" ``` lp15@60809 ` 2169` ``` using assms ``` lp15@68302 ` 2170` ``` apply (clarsimp simp: a'_def b'_def midpoints_in_convex_hull hull_subset [THEN subsetD]) ``` lp15@60809 ` 2171` ``` apply (auto simp: midpoint_def dist_norm scaleR_conv_of_real divide_simps) ``` lp15@60809 ` 2172` ``` done ``` lp15@68302 ` 2173` ``` then show ?thesis by blast ``` lp15@60809 ` 2174` ``` next ``` lp15@68302 ` 2175` ``` case 4 then have "?\ a' b' c'" ``` lp15@60809 ` 2176` ``` using assms ``` lp15@68302 ` 2177` ``` apply (clarsimp simp: a'_def c'_def b'_def midpoints_in_convex_hull hull_subset [THEN subsetD]) ``` lp15@60809 ` 2178` ``` apply (auto simp: midpoint_def dist_norm scaleR_conv_of_real divide_simps) ``` lp15@60809 ` 2179` ``` done ``` lp15@68302 ` 2180` ``` then show ?thesis by blast ``` lp15@60809 ` 2181` ``` qed ``` lp15@60809 ` 2182` ```qed ``` lp15@60809 ` 2183` wl302@69423 ` 2184` ```subsection%unimportant \Cauchy's theorem for triangles\ ``` lp15@60809 ` 2185` lp15@60809 ` 2186` ```lemma triangle_points_closer: ``` lp15@60809 ` 2187` ``` fixes a::complex ``` lp15@60809 ` 2188` ``` shows "\x \ convex hull {a,b,c}; y \ convex hull {a,b,c}\ ``` lp15@60809 ` 2189` ``` \ norm(x - y) \ norm(a - b) \ ``` lp15@60809 ` 2190` ``` norm(x - y) \ norm(b - c) \ ``` lp15@60809 ` 2191` ``` norm(x - y) \ norm(c - a)" ``` lp15@60809 ` 2192` ``` using simplex_extremal_le [of "{a,b,c}"] ``` lp15@60809 ` 2193` ``` by (auto simp: norm_minus_commute) ``` lp15@60809 ` 2194` lp15@60809 ` 2195` ```lemma holomorphic_point_small_triangle: ``` lp15@68302 ` 2196` ``` assumes x: "x \ S" ``` lp15@68302 ` 2197` ``` and f: "continuous_on S f" ``` lp15@68302 ` 2198` ``` and cd: "f field_differentiable (at x within S)" ``` lp15@60809 ` 2199` ``` and e: "0 < e" ``` lp15@60809 ` 2200` ``` shows "\k>0. \a b c. dist a b \ k \ dist b c \ k \ dist c a \ k \ ``` lp15@68302 ` 2201` ``` x \ convex hull {a,b,c} \ convex hull {a,b,c} \ S ``` lp15@61738 ` 2202` ``` \ norm(contour_integral(linepath a b) f + contour_integral(linepath b c) f + ``` lp15@61738 ` 2203` ``` contour_integral(linepath c a) f) ``` lp15@60809 ` 2204` ``` \ e*(dist a b + dist b c + dist c a)^2" ``` lp15@60809 ` 2205` ``` (is "\k>0. \a b c. _ \ ?normle a b c") ``` lp15@60809 ` 2206` ```proof - ``` lp15@60809 ` 2207` ``` have le_of_3: "\a x y z. \0 \ x*y; 0 \ x*z; 0 \ y*z; a \ (e*(x + y + z))*x + (e*(x + y + z))*y + (e*(x + y + z))*z\ ``` lp15@60809 ` 2208` ``` \ a \ e*(x + y + z)^2" ``` lp15@60809 ` 2209` ``` by (simp add: algebra_simps power2_eq_square) ``` lp15@60809 ` 2210` ``` have disj_le: "\x \ a \ x \ b \ x \ c; 0 \ a; 0 \ b; 0 \ c\ \ x \ a + b + c" ``` lp15@60809 ` 2211` ``` for x::real and a b c ``` lp15@60809 ` 2212` ``` by linarith ``` lp15@61738 ` 2213` ``` have fabc: "f contour_integrable_on linepath a b" "f contour_integrable_on linepath b c" "f contour_integrable_on linepath c a" ``` lp15@68302 ` 2214` ``` if "convex hull {a, b, c} \ S" for a b c ``` lp15@60809 ` 2215` ``` using segments_subset_convex_hull that ``` lp15@61738 ` 2216` ``` by (metis continuous_on_subset f contour_integrable_continuous_linepath)+ ``` lp15@61738 ` 2217` ``` note path_bound = has_contour_integral_bound_linepath [simplified norm_minus_commute, OF has_contour_integral_integral] ``` lp15@60809 ` 2218` ``` { fix f' a b c d ``` lp15@60809 ` 2219` ``` assume d: "0 < d" ``` lp15@68302 ` 2220` ``` and f': "\y. \cmod (y - x) \ d; y \ S\ \ cmod (f y - f x - f' * (y - x)) \ e * cmod (y - x)" ``` lp15@60809 ` 2221` ``` and le: "cmod (a - b) \ d" "cmod (b - c) \ d" "cmod (c - a) \ d" ``` lp15@60809 ` 2222` ``` and xc: "x \ convex hull {a, b, c}" ``` lp15@68302 ` 2223` ``` and S: "convex hull {a, b, c} \ S" ``` lp15@61738 ` 2224` ``` have pa: "contour_integral (linepath a b) f + contour_integral (linepath b c) f + contour_integral (linepath c a) f = ``` lp15@61738 ` 2225` ``` contour_integral (linepath a b) (\y. f y - f x - f'*(y - x)) + ``` lp15@61738 ` 2226` ``` contour_integral (linepath b c) (\y. f y - f x - f'*(y - x)) + ``` lp15@61738 ` 2227` ``` contour_integral (linepath c a) (\y. f y - f x - f'*(y - x))" ``` lp15@68302 ` 2228` ``` apply (simp add: contour_integral_diff contour_integral_lmul contour_integrable_lmul contour_integrable_diff fabc [OF S]) ``` lp15@60809 ` 2229` ``` apply (simp add: field_simps) ``` lp15@60809 ` 2230` ``` done ``` lp15@60809 ` 2231` ``` { fix y ``` lp15@60809 ` 2232` ``` assume yc: "y \ convex hull {a,b,c}" ``` lp15@60809 ` 2233` ``` have "cmod (f y - f x - f' * (y - x)) \ e*norm(y - x)" ``` lp15@68302 ` 2234` ``` proof (rule f') ``` lp15@68302 ` 2235` ``` show "cmod (y - x) \ d" ``` lp15@68302 ` 2236` ``` by (metis triangle_points_closer [OF xc yc] le norm_minus_commute order_trans) ``` lp15@68302 ` 2237` ``` qed (use S yc in blast) ``` lp15@68339 ` 2238` ``` also have "\ \ e * (cmod (a - b) + cmod (b - c) + cmod (c - a))" ``` lp15@60809 ` 2239` ``` by (simp add: yc e xc disj_le [OF triangle_points_closer]) ``` lp15@60809 ` 2240` ``` finally have "cmod (f y - f x - f' * (y - x)) \ e * (cmod (a - b) + cmod (b - c) + cmod (c - a))" . ``` lp15@60809 ` 2241` ``` } note cm_le = this ``` lp15@60809 ` 2242` ``` have "?normle a b c" ``` lp15@68302 ` 2243` ``` unfolding dist_norm pa ``` lp15@60809 ` 2244` ``` apply (rule le_of_3) ``` lp15@68302 ` 2245` ``` using f' xc S e ``` lp15@60809 ` 2246` ``` apply simp_all ``` lp15@60809 ` 2247` ``` apply (intro norm_triangle_le add_mono path_bound) ``` lp15@61738 ` 2248` ``` apply (simp_all add: contour_integral_diff contour_integral_lmul contour_integrable_lmul contour_integrable_diff fabc) ``` lp15@60809 ` 2249` ``` apply (blast intro: cm_le elim: dest: segments_subset_convex_hull [THEN subsetD])+ ``` lp15@60809 ` 2250` ``` done ``` lp15@60809 ` 2251` ``` } note * = this ``` lp15@60809 ` 2252` ``` show ?thesis ```